coq / opam Goto Github PK

View Code? Open in Web Editor NEW

121.0 19.0 163.0 11.53 MB

Archive for all Coq related OPAM packages organized in various repositories

Home Page: https://coq.inria.fr/opam/www/

License: GNU Lesser General Public License v2.1

Makefile 3.44% Shell 42.52% Nix 2.76% OCaml 50.46% HTML 0.82%

coq opam-repository opam

opam's Introduction

opam archive for Coq

All opam repositories for Coq packages live here. Packages are organized according to the layout:

released: packages for officially released versions of Coq libraries and Coq extensions.
core-dev: packages for development versions of Coq.
extra-dev: packages for development versions of Coq libraries and Coq extensions.

We welcome pull requests to the released repository adding any Coq-related package that is compatible with a released version of Coq. Besides libraries of general interest, this also includes paper artifacts and other specialized formalizations that are not necessarily expected to be immediately reusable by others.

Usage

To activate the repositories:

released (recommended default):

opam repo add coq-released https://coq.inria.fr/opam/released

core-dev:

opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev

extra-dev:

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

Adding packages

See the documentation for how to add a package. You can also look at existing pull requests to see how others are adding packages.

Coq Platform

The released opam archive is a key component of the Coq Platform, a distribution of Coq together with a curated set of libraries and plugins. After installing the Platform using scripts (as opposed to via a binary installer), additional packages in the released opam archive can be installed manually without the need for repository activation.

Website and opam metadata

The scripts/archive2web.ml program generates the JSON file coq-packages.json by looking at the opam files.

In particular, it uses the tags field of an opam file as follows:

strings beginning with keyword: are considered as keywords
strings beginning with category: are considered as categories
a string beginning with logpath: is considered the Coq logical path prefix
a string beginning with date: is the date the software was last updated (not the package definition)

Example:

tags: [
  "keyword:cool"
  "keyword:stuff"
  "category:Miscellaneous/Coq Use Examples"
  "logpath:MyPrefix"
  "date:1992-12-22"
]

The homepage:, author:, maintainer:, and doc: fields are also used to generate the package entry.

The JSON file is generated during continuous integration and copied to the website. JavaScript code on the website then loads it to dynamically generate the content of the website on the client side.

Continuous integration

Incoming pull requests are tested on GitLab CI. @coqbot pushes any opened or synchonized pull request to a branch named pr-<number> on GitLab. It will trigger a CI build. If the CI build runs for too long and times out, any member of the Coq organization of GitLab can start it again using the "Run Pipeline" green button at https://gitlab.com/coq/opam-coq-archive/pipelines. This will then build only on runners without pre-set timeouts (the Coq Pyrolyse server). It may still time out if the build takes longer than the GitLab project's timeout setting (24 hours). To skip some packages the first PR message can contain a line such as ci-skip: p1.v1 p2.v2 where p1 and p2 are package names, and v1 and v2 are versions.

opam's People

Contributors

Stargazers

Watchers

Forkers

mattam82 gmalecha amintimany elfi geocoq cogumbreiro smtcoq thery tebbi herbelin artart78 mereogeometry osavaryb damien-pous ybertot jasongross aa755 clarus jnarboux ejgallego spitters thtuerk fpottier relrod ankitku gares palmskog ralfjung boulme maximedenes ppedrot xavierleroy zimmi48 silene tuong cohencyril beta-ziliani querycert tchajed lthms lastland pedagand anton-trunov lemonidas skyskimmer vzaliva arthuraa tweerwag lysxia jhjourdan armael fajb yforster llee454 shym chdoc bollu erikmd proux01 richardlford minkiminki gilhur alokat matafou xldenis affeldt-aist digamma-ai amiloradovsky liyishuai blaisorblade xuanruiqi floriangru piyush-kurur arvidj picojulien gstew5 volodeyka msoegtropimc alizter amahboubi kiranandcode ivanbakel olaure01 mandel kevorr barry-jay-personal clayrat samuelgruetter aerabi lasseblaauwbroek fakusb fetburner cocti mohit-kumar-tekriwal dongjaelee1 pi8027 logicalatomist rafoo hmc-alpaqa nifrec

opam's Issues

coq-coqide.dev broken

The problem seems commit 419e7cac23d7b8ac97d46a6c0d3228d591273d2b that removed target coqide-binaries.

The error obtained when compiling is
no rule to make target coqide-binaries

coq-flocq does not install sources

The install target of coq-flocq does not install sources. Most opam-installed coq libraries install sources (.v files) along with compiled versions (.vo). This is convenient as it allows to examine definitions from IDE (ProofGeneral) during development.

Provide a flag to compile only CoqIDE

Currently, opam install coqide recompiles the entire standard library. That's just silly. There should be a ./configure -coqide only flag, or similar.

Clarifying the purpose of the coq package?

I wonder whether it is not disturbing that the "coq" package is in the list of coq packages at https://coq.inria.fr/opam/www/

Wouldn't it be clearer to remove core-dev from the list generated to build the index page?

I wonder what others think?

coq-mathcomp-ssreflect package for Coq 8.8.0

With Coq 8.8.0 the following works perfectly:

opam install --ignore-constraints-on=coq coq-mathcomp-ssreflect.dev

Basic instructions?

For someone without experience with OPAM, installing coq is not the most intuitive. I've heard a lot about using OPAM to install Coq 8.5 rc1, so I naively ran

opam init
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam install coq

but this offered Hott/Coq. So I did opam search coq and got

# Existing packages for system:
coq          --  HoTT/Coq stable branch
coq-shell    --  Simplified OPAM shell for Coq
coqide       --  IDE of the coq formal proof management system
ott          --  Ott is a tool for writing definitions of programming languages and calculi
sibylfs-lem  --  SibylFS fork of Lightweight Executable Mathematics for large-scale semantics
zenon        --  Automated theorem prover for first order classical logic (with equality), based on the tableau method

It would be great to have a quick pointer to the right command. The instructions on https://coq.inria.fr/howto-opam say:

To install Coq:

opam install -j4 -v coq

To install a package:

opam install coq:that-super-package

To add the repository of development packages (use it at your own risks):

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

To add the repository of development versions of Coq (use it at your own risks):

opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev

TODO: talk about the distribution mechanism.

But opam install -j4 -v coq definitely doesn't do the right thing :/

`repo` file needs to be added to `index.tar.gz`

For better opam 2 compatibility, the repositories should have a repo file. With #261 all our repos have such a file, but it doesn't have the intended effect because it is not included in the https://coq.inria.fr/opam/released/index.tar.gz.

Seems like the website generation needs to be updated. Is it enough to change https://github.com/coq/opam-coq-archive/blob/master/scripts/refresh-opam-indexes?

CI: Test that uninstall really uninstalls everything

Our CI could test that opam unimstall really uninstalls everything that got installed (and nothing more).

8.5~beta2 is smaller than 8.5

According to the Debian / OPAM ordering, 8.5~beta2 is a smaller version than 8.5:

dpkg --compare-versions 8.5~beta2 lt 8.5; echo $?

returns 0.

The problem: how do we state that a package is only compatible with the 8.4 branch? The solution used so far is to add the dependency:

"coq" {>= "8.4.5" & < "8.5"}

but this includes 8.5~beta2 in the range. This means that most stable packages are currently broken. This bug was not detected by the bench because it only tests the 8.5.dev version.

A possible solution: rename the beta as 8.5.0~beta2.

no (working) smtp on the machine serving the opam archive

Now the archive is updated again, but I did receive no notification that it stopped working.

The update script uses mail to send a mail to root (and myself), but is seems not to work since I received no email.

Again, I don't have access to that machine, so I cannot fix nor investigate the issue.

mtac2 not supported by 8.7.1

what fraction of opam-coq supports 8.7 generally?
should i switch to a previous release of ocaml and use 8.6?

Since 8.7~ coq byte is no more built/installed

Indexes not correctly updatd

Look here:
https://coq.inria.fr/opam/core-dev/
the packages directory has a time stamp more recent than the index one, indeed the index contains an outdated version of the packages.

coq.inria.fr/opam not synchronized

I just added the package coq:coqide.8.5~beta2 one hour ago. Since it is not available on coq.inria.fr/opam/released yet whereas the update delay is of 10 minutes, I am afraid that the synchronization mechanism may be broken.

Colons in package names

I am very sorry about this since I took part in advising it ; but it turns out this is a terrible idea for Windows support, as package names need to appear in file names, and Windows really doesn't like colons in file names.

See ocaml/opam#2320 for the original discussion on colons, package names and Windows.

is there a coq-mtac for 8.6 yet?

coq-color.1.1.0 does not install with coq.8.4.6

nemo ~$ opam install -j4 coq-color.1.1.0
The following actions will be performed:
  ∗  install coq-color 1.1.0

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq-color] Archive in cache

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] The compilation of coq-color failed at "make -j4".
Processing  1/1: [coq-color: rm]
#=== ERROR while installing coq-color.1.1.0 ===================================#
# opam-version 1.2.2
# os           linux
# command      make -j4
# path         /home/lord/.opam/4.02.3.coq.8.4/build/coq-color.1.1.0
# compiler     4.02.3
# exit-code    2
# env-file     /home/lord/.opam/4.02.3.coq.8.4/build/coq-color.1.1.0/coq-color-25541-1872ec.env
# stdout-file  /home/lord/.opam/4.02.3.coq.8.4/build/coq-color.1.1.0/coq-color-25541-1872ec.out
# stderr-file  /home/lord/.opam/4.02.3.coq.8.4/build/coq-color.1.1.0/coq-color-25541-1872ec.err
### stdout ###
# [...]
# "coqc"  -q  -R . CoLoR   Util/Nat/Log2
# File "/home/lord/.opam/4.02.3.coq.8.4/build/coq-color.1.1.0/Util/Bool/BoolUtil.v", line 16, characters 19-33:
# Error: The reference orb_false_elim was not found in the current environment.
# Makefile.coq:407: recipe for target 'Util/Bool/BoolUtil.vo' failed
# Identifier 'o' now a keyword
# File "/home/lord/.opam/4.02.3.coq.8.4/build/coq-color.1.1.0/Util/Nat/Log2.v", line 19, characters 13-19:
# Error: The reference le_n_S was not found in the current environment.
# Makefile.coq:407: recipe for target 'Util/Nat/Log2.vo' failed
# make[1]: Leaving directory '/home/lord/.opam/4.02.3.coq.8.4/build/coq-color.1.1.0'
# Makefile:17: recipe for target 'default' failed
### stderr ###
# make[1]: *** [Util/Bool/BoolUtil.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make[1]: *** [Util/Nat/Log2.vo] Error 1
# make: *** [default] Error 2



=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
  ∗  install coq-color 1.1.0
No changes have been performed
nemo ~$ opam list
# Installed packages for 4.02.3.coq.8.4:
base-bigarray     base  Bigarray library distributed with the OCaml compiler
base-ocamlbuild   base  OCamlbuild binary and libraries distributed with the OCa
base-threads      base  Threads library distributed with the OCaml compiler
base-unix         base  Unix library distributed with the OCaml compiler
camlp5            6.14  Preprocessor-pretty-printer of OCaml
coq              8.4.6 (pinned)  Formal proof management system.
coq-ext-lib      0.9.1  A library of Coq definitions, theorems, and tactics.
ocamlbuild           0  Build system distributed with the OCaml compiler since O
nemo ~$

Coq 8.7+beta2 missing

Will 8.7+beta2 be added to the opam-repository?

coqide vs coq:coqide

There are currently two packages for CoqIDE:

coqide on the OCaml repository
coq:coqide on the Coq repository

Proposal:

rename coq:coqide to coqide
put the stable versions of CoqIDE on the OCaml repository, the non-stable ones on extra-dev

This does not completely follows our conventions for Coq packages (naming, ...), but is justified for historical compatibility.

No maintainers for `coq:coqprime`

The following packages have no maintainers (field maintainer empty in the opam files):

coq:coqprime.1.0.0
coq:coqprime.dev

I copy to @thery. By the way, I just reported a bug about CoqPrime with the new Coq 8.5~beta3: https://coq.inria.fr/bugs/show_bug.cgi?id=4419

Coq is not uninstalled completely

When doing opam uninstall coq (I had version 8.7.dev installed), there are some files left in the opam directories:

./man/man1/coqdoc.1
./man/man1/coqdep.1
./man/man1/coqwc.1
./man/man1/coqtop.1
./man/man1/coqmktop.1
./man/man1/coq_makefile.1
./man/man1/coqc.1
./man/man1/coq-tex.1
./man/man1/coqtop.opt.1
./man/man1/coqide.1
./man/man1/coqchk.1
./man/man1/coqtop.byte.1
./bin/coqtop.byte
./share/texmf/tex/latex/misc/coqdoc.sty
./share/emacs/site-lisp/coqdoc.sty
./share/emacs/site-lisp/coq-font-lock.el
./share/emacs/site-lisp/coq-inferior.el

opam 2.0 switch

We should try opam 2.0 at some point, the release candidate is out:
https://opam.ocaml.org/blog/opam-2-0-0-rc/

This should be the parent of mattam82/coq-opam-archive, not a fork of it

You can get the github devs to fix this by contacting GitHub support. (You might need to have @mattam82 do this, since his is the parent repo.)

wrong version of coq-ext-lib installed

When I try install coq-ext-lib with coq-8.6 it attempts to install 0.9.3 instead of 0.9.5:
More info:

I have a fresh opam switch with following packages installed:

max1 ~/coq/math-classes$ opam list
# Installed packages for 4.04.0.coq.8.6:
base-bigarray   base  Bigarray library distributed with the OCaml compiler
base-threads    base  Threads library distributed with the OCaml compiler
base-unix       base  Unix library distributed with the OCaml compiler
camlp5          6.17  Preprocessor-pretty-printer of OCaml
conf-m4            1  Virtual package relying on m4
coq              8.6  Formal proof management system.
coq-dpdgraph   0.6.1  Compute dependencies between Coq objects (definitions, theorems)
ocamlfind      1.7.1  A library manager for OCaml
ocamlgraph     1.8.7  A generic graph library for OCaml

I did opam update at it have all versions of the package:

max1 ~/coq/math-classes$ opam info coq-ext-lib
             package: coq-ext-lib
             version: 1.0.0~beta2
          repository: coq-released
        upstream-url: https://github.com/coq-ext-lib/coq-ext-lib/archive/v1.0.0-beta2.tar.gz
       upstream-kind: http
   upstream-checksum: a5ba82316433760606fa17535591382a
            homepage: https://github.com/coq-ext-lib/coq-ext-lib
         bug-reports: https://github.com/coq-ext-lib/coq-ext-lib/issues
            dev-repo: https://github.com/coq-ext-lib/coq-ext-lib.git#8.5
              author: Gregory Malecha
             license: BSD
             depends: coq (>= 8.5~beta2 & < 8.5~beta3)
   installed-version: 
  available-versions: 0.9.0~beta3, 0.9.0, 0.9.1, 0.9.2, 0.9.3, 0.9.4, 0.9.5, 1.0.0~beta2
         description: A library of Coq definitions, theorems, and tactics.

I have nothing pinned. However when I try to install it picks up older version:

max1 ~/coq/math-classes$ opam instal coq-ext-lib
The following actions will be performed:
  ∗  install coq-ext-lib 0.9.3

Which is incompatible with coq-8.6 and the installation fails.

shouldn't 8.6 be moved to the released category?

Proposal for a default web page for contribs

Example at http://pauillac.inria.fr/~herbelin/tmp//aac-tactics/

Advantages:

more welcoming than the github page
possibility to browse files with links to stdlib and other packages from coq-contribs

Inconvenients:

some redundancies with the info at https://coq.inria.fr/opam/www/ (but maybe not more than for packages which have an ad hoc web page)

I'm not web expert at all. Feel free to improve.

The objective, jointly with Enrico, is to commit these pages as github pages.

In the absence of comments, I'm going to commit these pages and the building scripts within a few days.

Categories Libraries, Plugin, End result ?

I feel it would be useful to add tags such as

Libraries (e.g. corn, mathcomp-algebra, ...)
Plugins (e.g. aac-tactics, mathcomp-ssreflect, ...)
End result (e.g. godel, mathcomp-odd_order, ...)

Anyone interested in adding such an improvement?

CompCert package version update

When installing CompCert via OPAM, it reports that the latest available version is 3.0.1. Could it get updated to reflect the release of v3.1?

problem when installing coq.8.0.dev

Hello,

On a machine running fedora 21, I get the following error message

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] The compilation of coq failed at "make world".

=== ERROR while installing coq.8.0.dev =======================================

opam-version 1.2.2

os linux

command make world

path /user/bertot/home/tmp/certicartes/infra/opam/4.02.3/build/coq.8.0.dev

compiler 4.02.3

exit-code 2

env-file /user/bertot/home/tmp/certicartes/infra/opam/4.02.3/build/coq.8.0.dev/coq-3147-05296d.env

stdout-file /user/bertot/home/tmp/certicartes/infra/opam/4.02.3/build/coq.8.0.dev/coq-3147-05296d.out

stderr-file /user/bertot/home/tmp/certicartes/infra/opam/4.02.3/build/coq.8.0.dev/coq-3147-05296d.err

stdout

[...]

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/romega/ReflOmegaCore

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/romega/ROmega

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/NArithRing

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring_theory

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring_normalize

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/cc/CCSolve

bin/coqtop.opt -boot -compile ide/utf8

OCAMLC ide/utils/okey.mli

Makefile:580: recipe for target 'ide/utils/okey.cmi' failed

stderr

[...]

Warning: unable to ensure the correctness of the translation of an if-then-else

Warning: pattern step is understood as a pattern variable

File "ide/utils/okey.mli", line 33, characters 16-33:

Error: Unbound module Gdk

make: *** [ide/utils/okey.cmi] Error 2

=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
\u2217 install coq 8.0.dev
No changes have been performed

As extra information I can also give information about the current opam set up:
Here are a few results of commands:

opam --version
1.2.2
opam list --root $INFRA/opam

Installed packages for 4.02.3:

base-bigarray base Bigarray library distributed with the OCaml compiler
base-ocamlbuild base OCamlbuild binary and libraries distributed with the OC
base-threads base Threads library distributed with the OCaml compiler
base-unix base Unix library distributed with the OCaml compiler
camlp4 4.02+6 Camlp4 is a system for writing extensible parsers for p
camlp5 6.14 Preprocessor-pretty-printer of OCaml
lablgtk 2.18.3 OCaml interface to GTK+
ocamlbuild 0 Build system distributed with the OCaml compiler since
ocamlfind 1.5.6 A library manager for OCaml

opam repo --root $INFRA/opam
10 [http] core-dev https://coq.inria.fr/opam/core-dev
0 [http] default https://opam.ocaml.org

Unsynchronized web repository

It feels to me that the released repository, as available with:

opam repo add coq-released https://coq.inria.fr/opam/released

is not synchronized any more, since the new version 2.2.1 of coq-interval is not available.

CI: Automatically build some `*.dev` packages nightly

We should look into Travis' cron jobs to automatically build some of our *.dev packages every night, so that we can detect build failure incurred from Coq changes.

Issues in compiling coq:extraction:lwt:ocaml and coq:concurrency:pluto

Hi, I don't know if this is the right place for reporting bugs in installing opam packages for Coq, but I fell on two problems:

In installing coq:extraction:lwt:ocaml, I got an "Unbound value Lwt.fail_with" (script follows below).

In trying to install coq:concurrency:pluto, I got: "Your request can't be satisfied: - No package matches coq:concurrency:pluto".

Debugging output (which I don't know how to interpret accurately) gives:

00:01.386  031289  HEURISTIC               state-of-request: install:(coq%3aconcurrency%3asystem & coq & camlp5 & base-unix & base-threads & base-bigarray) remove:() upgrade:(coq%3aconcurrency%3apluto) criteria:"-removed,-notuptodate,-changed" CONFLICT!
00:01.386  031289  CUDF                    resolve request=install:(coq%3aconcurrency%3asystem & coq & camlp5 & base-unix & base-threads & base-bigarray) remove:() upgrade:(coq%3aconcurrency%3apluto) criteria:"-removed,-notuptodate,-changed"
00:01.386  031289  CLIENT                  conflict!
Your request can't be satisfied:
  - No package matches coq:concurrency:pluto.

Report for coq:extraction:lwt:ocaml is

.#=== ERROR while installing coq:extraction:lwt:ocaml.dev ======================#
# opam-version 1.2.0
# os           linux
# command      make -j1
# path         /home/herbelin/COQ/git/v8.5/opam/system/build/coq:extraction:lwt:ocaml.dev
# compiler     system (3.12.1)
# exit-code    2
# env-file     /home/herbelin/COQ/git/v8.5/opam/system/build/coq:extraction:lwt:ocaml.dev/coq:extraction:lwt:ocaml-1222-7afd23.env
# stdout-file  /home/herbelin/COQ/git/v8.5/opam/system/build/coq:extraction:lwt:ocaml.dev/coq:extraction:lwt:ocaml-1222-7afd23.out
# stderr-file  /home/herbelin/COQ/git/v8.5/opam/system/build/coq:extraction:lwt:ocaml.dev/coq:extraction:lwt:ocaml-1222-7afd23.err
### stdout ###
# ocamlbuild extractionLwt.cma extractionLwt.cmxa -use-ocamlfind -package lwt,lwt.unix,num
# ocamlfind ocamldep -package lwt,lwt.unix,num -modules extractionLwt.ml > extractionLwt.ml.depends
# ocamlfind ocamlc -c -package lwt,lwt.unix,num -o extractionLwt.cmo extractionLwt.ml
# + ocamlfind ocamlc -c -package lwt,lwt.unix,num -o extractionLwt.cmo extractionLwt.ml
# File "extractionLwt.ml", line 14, characters 13-26:
# Error: Unbound value Lwt.fail_with
# Command exited with code 2.
### stderr ###
# make: *** [default] Erreur 10

coq.dev has outdated license, maintainer and build rules

CompCert 64-bit versions

I've noticed that all CompCert versions in the repo have only ia-32 builds enabled. The CompCert manual states that one should be able to compile native 64-bit versions of the compiler, using x86_64-<OS> configure flags. Could this be added?

Fix version constraints

The large number of red boxes here https://coq-bench.github.io/clean/Linux-x86_64-4.05.0-1.2.2/released/ seems to indicate that a number of packages in released do not correctly state their Coq version constraints. This should be fix but I've no will to do it myself.

The quick guide on https://coq.inria.fr/opam/www/using.html doesn't work

Operating system

Ubuntu 18.04

Description of the problem

The guide on https://coq.inria.fr/opam/www/using.html doesn't work on my Ubuntu 18.04. I installed the opam from Ubuntu distro. The command you give

opam init -n --comp=ocaml-base-compiler.4.02.3 -j 2 # 2 is the number of CPU cores

fails with

Cannot find /home/maksr/opam-coq.8.8.2/compilers/ocaml-base-compiler.4.02.3/ocaml-base-compiler.4.02.3/ocaml-base-compiler.4.02.3.comp: ocaml-base-compiler.4.02.3 is not a valid compiler name.

Searching the web I found that I must give the following command and this one worked for me:

opam init -n --comp 4.02.3

The last of the four commands

opam install coq.8.8.2 && opam pin add coq 8.8.2

failed as well, with

[ERROR] No package matches coq.8.8.2.

Using opam show coq I found the last version in http://coq.inria.fr/opam/released is 8.8.1 (today is October, 27th, 2018).

So I deleted the ~/opam-coq.8.8.2 and repeated the commands with 8.8.1 which seems to be working.

failure to install mirror-core

$ opam install coq-mirror-core
The following actions will be performed:
  ∗  install coq-ext-lib      0.9.5           [required by coq-mirror-core]
  ∗  install coq-plugin-utils 1.1.0           [required by coq-mirror-core]
  ∗  install coq-mirror-core  1.0.2

the error message was


=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫
∗  installed coq-ext-lib.0.9.5
[ERROR] The compilation of coq-plugin-utils failed at "make -j1".
Processing  2/3: [coq-plugin-utils: rm]
#=== ERROR while installing coq-plugin-utils.1.1.0 ============================#
# opam-version 1.2.2
# os           darwin
# command      make -j1
# path         /Users/carter/.opam/system/build/coq-plugin-utils.1.1.0
# compiler     system (4.05.0)
# exit-code    2
# env-file     /Users/carter/.opam/system/build/coq-plugin-utils.1.1.0/coq-plugin-utils-45157-335865.env
# stdout-file  /Users/carter/.opam/system/build/coq-plugin-utils.1.1.0/coq-plugin-utils-45157-335865.out
# stderr-file  /Users/carter/.opam/system/build/coq-plugin-utils.1.1.0/coq-plugin-utils-45157-335865.err
### stdout ###
# [...]
# CAMLDEP src/term_match.mli
# CAMLDEP src/coqstd.mli
# COQDEP src/plugin_utils.mlpack
# CAMLDEP src/use_ltac.ml
# CAMLDEP src/term_match.ml
# CAMLDEP src/coqstd.ml
# CAMLDEP -pp src/plugin_utils_plugin.ml4
# COQDEP theories/PluginUtils.v
# CAMLC -c src/use_ltac.mli
# CAMLC -c src/use_ltac.ml
### stderr ###
# File "src/use_ltac.ml", line 16, characters 20-38:
# Error: Unbound constructor Tacexpr.TacDynamic
# make[1]: *** [src/use_ltac.cmo] Error 2
# make: *** [plugin] Error 2



=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫
The following actions were aborted
  ∗  install coq-mirror-core 1.0.2
The following actions failed
  ∗  install coq-plugin-utils 1.1.0
The following changes have been performed
  ∗  install coq-ext-lib 0.9.5

The former state can be restored with:
    opam switch import "~/.opam/system/backup/state-20170625203344.export"

Compilation of 8.5 fails on clean VM

I ran the following on a clean Ubuntu Vivid 64 bits:

apt-get update
apt-get install make m4 patch unzip git aspcud ocaml ocaml-native-compilers camlp4-extra opam 

opam init
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam install coq.8.5~rc1

and got the following message:

#=== ERROR while installing coq.8.5~rc1 =======================================#
# opam-version 1.2.0
# os           linux
# command      make -j2
# path         /home/vagrant/.opam/system/build/coq.8.5~rc1
# compiler     system (4.01.0)
# exit-code    2
# env-file     /home/vagrant/.opam/system/build/coq.8.5~rc1/coq-17959-a71bb4.env
# stdout-file  /home/vagrant/.opam/system/build/coq.8.5~rc1/coq-17959-a71bb4.out
# stderr-file  /home/vagrant/.opam/system/build/coq.8.5~rc1/coq-17959-a71bb4.err
### stdout ###
# ...[truncated]
# COQC      theories/Wellfounded/Union.v
# COQC      theories/Sets/Cpo.v
# COQC      theories/Sets/Finite_sets.v
# COQC      theories/Sets/Powerset.v
# COQC      theories/Sets/Relations_3_facts.v
# COQC      theories/Classes/Morphisms.v
# COQC      theories/Classes/CMorphisms.v
# Makefile.build:1040: recipe for target 'theories/Classes/Morphisms.vo' failed
# make[1]: Leaving directory '/home/vagrant/.opam/system/build/coq.8.5~rc1'
# Makefile:158: recipe for target 'submake' failed
### stderr ###
# ...[truncated]
# File "/usr/lib/ocaml/str.cma", line 1:
# Warning 31: files /usr/lib/ocaml/str.cma and /usr/lib/ocaml/str.cma both define a module named Str
# File "lib/lib.cma(Errors)", line 1:
# Warning 31: files lib/lib.cma(Errors) and /usr/lib/ocaml/compiler-libs/ocamlbytecomp.cma(Errors) both define a module named Errors
# File "parsing/parsing.cma(Lexer)", line 1:
# Warning 31: files parsing/parsing.cma(Lexer) and /usr/lib/ocaml/compiler-libs/ocamlcommon.cma(Lexer) both define a module named Lexer
# Error: Could not compile the library to native code.
# make[1]: *** [theories/Classes/Morphisms.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [submake] Error 2

In this expected? Did I do something wrong?

ssreflect.8.7.dev

Hi @MatejKosik @gares ,
I'm surprised to find such a package description. Maybe I missed a discussion? What is it for?
https://github.com/coq/opam-coq-archive/blob/cd8e83337b2c1701a290fd5667e52ddcd4250aa8/extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.8.7.dev/opam#L3
Cheers

coq 8.6 build fails

After recent opam update it wanted to recompile my installed coq due to dependencies. Unfortunately the build fails, leaving me without working coq.

#=== ERROR while installing coq.8.6 ===========================================#
# opam-version 1.2.2
# os           linux
# command      make -j4
# path         /home/lord/.opam/4.04.1/build/coq.8.6
# compiler     4.04.1
# exit-code    2
# env-file     /home/lord/.opam/4.04.1/build/coq.8.6/coq-11839-d2c37b.env
# stdout-file  /home/lord/.opam/4.04.1/build/coq.8.6/coq-11839-d2c37b.out
# stderr-file  /home/lord/.opam/4.04.1/build/coq.8.6/coq-11839-d2c37b.err
### stdout ###
# [...]
# COQC      plugins/setoid_ring/Ring.v
# COQC      plugins/setoid_ring/ZArithRing.v
# COQC      plugins/setoid_ring/ArithRing.v
# COQC      plugins/setoid_ring/NArithRing.v
# COQC      plugins/setoid_ring/Field_theory.v
# COQC      theories/Numbers/Integer/NatPairs/ZNatPairs.v
# ocamlopt.opt got signal and exited
# Makefile.build:652: recipe for target 'plugins/romega/ReflOmegaCore.vo' failed
# make[1]: Leaving directory '/home/lord/.opam/4.04.1/build/coq.8.6'
# Makefile:153: recipe for target 'submake' failed
### stderr ###
# [...]
# this constructor's arguments. They are only for information
# and may change in future versions. (See manual section 8.5)
# File "./plugins/romega/ReflOmegaCore.v", line 3167, characters 0-36:
# Warning: Native compiler exited with status 2
# [native-compiler-failed,native-compiler]
# Warning: Removed file ./plugins/romega/ReflOmegaCore.vo
# Error: Could not compile the library to native code.
# make[1]: *** [plugins/romega/ReflOmegaCore.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [submake] Error 2

logs.zip

Repo contains strange versions of coq-iris

I just saw via opam show that opam knows about some very strange versions of Iris that we never published: 8.7.dev and dev. It took me a while to realize that this repository is where they are coming from. It seems these strange versions were added by @MatejKosik a month ago.

What is the rationale for this? I would prefer for these versions to be removed. First of all, there is no "Iris 8.7", so having a version 8.7.dev of Iris available in opam is at beast misleading. Second, all of these versions are actually just aliases for Iris 3.0.0. This is pretty bad; it means that if we release an Iris 3.1.0, opam upgrade will actually replace that version of Iris with 8.7.dev, effectively downgrading Iris to 3.0.0. And finally, the dev version also is not really the dev version but instead yet another alias for Iris 3.0.0.

My current guess is that you are using these versions in your CI, but then you should really use a dedicated opam archive for that purpose. I have extra-dev added to all my opam instances to obtain the latest version of ssreflect, that should not automatically inflict version numbers that only make sense internally to your CI on coq-iris in my opam installations.

Packages for 8.7.dev and 8.7 beta differ

The diffed in the license for example.

Outdated tar.gz

This issue was raised by @mlasson. The problem is that the tar.gz archive of coq.dev is two months old. As mentioned by @silene and @gares, the generation of tar.gz could be disabled, using:

opam admin make --index

instead of:

opam admin make

I am OK with that. Here are the links of the directories which would (should?) become empty:

released/archives (maybe we can keep this one)
extra-dev/archives
core-dev/archives

Invalid contrib homepages

Hi,

The following packages do not seem to have a valid homepage, and may be referring to the wrong sources:

projective-geometry.8.5.0: https://github.com/coq-contrib/projective-geometry
regexp.8.5.0: https://github.com/coq-contrib/regexp
tait.8.5.0: https://github.com/coq-contrib/tait
tortoise-hare-algorithm.8.5.0: https://github.com/coq-contrib/tortoise-hare-algorithm

coq 8.6.dev missing dependency on ocamlfind

Doing opam pin add coq 8.6.dev results in the following error:

#=== ERROR while installing coq.8.6.dev =======================================#
# opam-version 1.2.2
# os           linux
# command      ./configure -configdir /home/r/.opam/coq-8.6/lib/coq/config -mandir /home/r/.opam/coq-8.6/man -with-doc no -prefix /home/r/.opam/coq-8.6 -usecamlp5 -camlp5dir /home/r/.opam/coq-8.6/lib/camlp5 -coqide no -debug
# path         /home/r/.opam/coq-8.6/build/coq.8.6.dev
# compiler     system (4.02.3)
# exit-code    1
# env-file     /home/r/.opam/coq-8.6/build/coq.8.6.dev/coq-15699-8c0dd3.env
# stdout-file  /home/r/.opam/coq-8.6/build/coq.8.6.dev/coq-15699-8c0dd3.out
# stderr-file  /home/r/.opam/coq-8.6/build/coq.8.6.dev/coq-15699-8c0dd3.err
### stderr ###
# Error: cannot find 'ocamlfind' in your path!
# Please adjust your path or use the -ocamlfind option of ./configure
# Configuration script failed!

I guess this means that a dependency is missing?

nemo ~/.opam/packages/coq-math-classes/coq-math-classes.1.0.6$ cat url
http: "https://github.com/math-classes/math-classes/archive/v8.6.zip"
checksum: "3d932d601b9a89e810ef3458a70900d9"
nemo ~/.opam/packages/coq-math-classes/coq-math-classes.1.0.6$ wget "https://github.com/math-classes/math-classes/archive/v8.6.zip" -O -  | md5sum
6d8aa78decdbf5a4d53ead3c64bc70cd  -
nemo ~/.opam/packages/coq-math-classes/coq-math-classes.1.0.6$

This is causing installation error (reported by @gmalecha :

downloaded 
[ERROR] Bad checksum for 
       /home/gmalecha/.opam/packages.dev/coq-math-classes.1.0.6/v8.6.zip: 
         - 3d932d601b9a89e810ef3458a70900d9 [expected result] 
         - 6d8aa78decdbf5a4d53ead3c64bc70cd [actual result] 
       This may be fixed by running `opam update`.

P.S. Not sure if it should be filed here or at https://github.com/math-classes/math-classes

Install instructions need updating

This page is still about 8.7.2.
https://coq.inria.fr/opam/www/using.html

coq.dev install is failing

$ opam install coq.dev
The following actions will be performed:
  ∗  install coq dev

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq] https://github.com/coq/coq#master already up-to-date

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] Installation of coq.dev failed
Processing  1/1: [coq: rm]
#=== ERROR while installing coq.dev ===========================================#
Some files in ~/.opam/4.05.0/install/coq.install couldn't be installed:
  - /home/theo/.opam/4.05.0/build/coq.dev/bin/coqmktop to /home/theo/.opam/4.05.0/bin

This might be related to coq/coq#6475 (coqmktop cannot be installed because it was removed) cc @ejgallego.
The strange thing is that I didn't manage to reproduce outside of the OPAM package.

coq / opam Goto Github PK

opam's Introduction

opam archive for Coq

Usage

Adding packages

Coq Platform

Website and opam metadata

Continuous integration

opam's People

Contributors

Stargazers

Watchers

Forkers

opam's Issues

=== ERROR while installing coq.8.0.dev =======================================

opam-version 1.2.2

os linux

command make world

path /user/bertot/home/tmp/certicartes/infra/opam/4.02.3/build/coq.8.0.dev

compiler 4.02.3

exit-code 2

env-file /user/bertot/home/tmp/certicartes/infra/opam/4.02.3/build/coq.8.0.dev/coq-3147-05296d.env

stdout-file /user/bertot/home/tmp/certicartes/infra/opam/4.02.3/build/coq.8.0.dev/coq-3147-05296d.out

stderr-file /user/bertot/home/tmp/certicartes/infra/opam/4.02.3/build/coq.8.0.dev/coq-3147-05296d.err

stdout

[...]

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/romega/ReflOmegaCore

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/romega/ROmega

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/NArithRing

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring_theory

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring_normalize

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring

bin/coqtop.opt -boot -translate -strict-implicit -compile contrib7/cc/CCSolve

bin/coqtop.opt -boot -compile ide/utf8

OCAMLC ide/utils/okey.mli

Makefile:580: recipe for target 'ide/utils/okey.cmi' failed

stderr

[...]

Warning: unable to ensure the correctness of the translation of an if-then-else

Warning: unable to ensure the correctness of the translation of an if-then-else

Warning: unable to ensure the correctness of the translation of an if-then-else

Warning: pattern step is understood as a pattern variable

Warning: pattern step is understood as a pattern variable

Warning: pattern step is understood as a pattern variable

Warning: pattern step is understood as a pattern variable

File "ide/utils/okey.mli", line 33, characters 16-33:

Error: Unbound module Gdk

make: *** [ide/utils/okey.cmi] Error 2

Installed packages for 4.02.3:

Operating system

Description of the problem

Recommend Projects

Recommend Topics

Recommend Org