Stream: Coq devs & plugin devs

Topic: coq-bench for opam


view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 16:59):

As some of you know @Guillaume Claret has been maintaining coq.io for a whlle, see https://github.com/coq/coq/issues/10418 for more information; please provide feedback here or in the issue as to what you think the integration of coq.io with coq dev tools should be.

view this post on Zulip Guillaume Claret (Sep 16 2020 at 17:03):

Thanks for opening the thread. More precisely this is https://coq-bench.github.io/ , with the OPAM bench system (Coq.io being the website of the coq-io library).

view this post on Zulip Karl Palmskog (Sep 16 2020 at 17:06):

not sure if this falls into current scope, but it would be great with OPAM bench system integration with the Zulip chat

view this post on Zulip Guillaume Claret (Sep 16 2020 at 17:07):

Yes, that is what I just proposed to do in the issue.

view this post on Zulip Karl Palmskog (Sep 16 2020 at 17:07):

ah, I see this is already mentioned in the issue. For me, it's not so important to migrate logs, but to have new updates.

view this post on Zulip Karl Palmskog (Sep 16 2020 at 17:10):

I think Coq-bench is great for seeing the general impact of OCaml versions on Coq packages, for example, I have no idea today which plugins don't work on 4.11

view this post on Zulip Karl Palmskog (Sep 16 2020 at 17:14):

one nice thing that could be done is explorative but systematic checking of extra-dev packages, that are simply impossible to maintain otherwise. We have a serious issue that many of them have flaws, but are the only way to install many projects. If a maintained extra-dev package fails, the Coq bot may be able to open an issue in the original repo and so on.

view this post on Zulip Karl Palmskog (Sep 16 2020 at 17:16):

more generally, there are many avenues for integration with the Coq bot

view this post on Zulip Karl Palmskog (Sep 16 2020 at 17:23):

also, I think it would be nice with a dashboard summarizing "Coq package health" on different versions of Coq and OCaml

view this post on Zulip Karl Palmskog (Sep 16 2020 at 17:25):

ah, and for some 8.11-limited packages, it should be possible to do "explorative testing" on 8.12 and so on, so we don't have to manually figure out whether some package/project is compatible with a new version (opam's ignore-constraint-on for the Coq version)

view this post on Zulip Karl Palmskog (Sep 16 2020 at 17:31):

@Guillaume Claret but how are you setting up the respective environments right now in the bench? Is it scripts on top of some specific Linux distribution? Ideally, this would use the same containers as we do for Docker Coq CI for reproducibility

view this post on Zulip Guillaume Claret (Sep 16 2020 at 19:51):

Karl Palmskog said:

also, I think it would be nice with a dashboard summarizing "Coq package health" on different versions of Coq and OCaml

There are some colored numbers on the columns to quickly see the status of a Coq version given an OCaml version, but one has to click on each OCaml version to get the data
image.png

view this post on Zulip Guillaume Claret (Sep 16 2020 at 19:54):

Karl Palmskog said:

ah, and for some 8.11-limited packages, it should be possible to do "explorative testing" on 8.12 and so on, so we don't have to manually figure out whether some package/project is compatible with a new version (opam's ignore-constraint-on for the Coq version)

That could be like a good idea to add, like a special platform, where it fails only if the package pretends to be incompatible but installs with ignore-constraint.

view this post on Zulip Guillaume Claret (Sep 16 2020 at 19:57):

Also having more packages with open Coq version boundaries could help. We could also run a script just once to test which packages are actually compatible when a new Coq version is out.

view this post on Zulip Guillaume Claret (Sep 16 2020 at 20:02):

Karl Palmskog said:

Guillaume Claret but how are you setting up the respective environments right now in the bench? Is it scripts on top of some specific Linux distribution? Ideally, this would use the same containers as we do for Docker Coq CI for reproducibility

I use specific Docker images as described in https://github.com/coq-bench/run/blob/master/Dockerfile.erb I never though about using the Docker Coq CI images. I think I would not be able to have an arbitrary combination of Coq version + OCaml version with the Docker Coq CI images.

view this post on Zulip Guillaume Claret (Sep 16 2020 at 20:04):

For the explorative testing, I wonder if this could be systematic. When a package pretends to be incompatible, we still try to install it and report an error if it installs.

view this post on Zulip Karl Palmskog (Sep 16 2020 at 20:39):

the versions of Coq and OCaml are actually parameters in those Docker images, so I think you could use something similar. In any case, I think one should think about uniformity of testing Coq packages on Linux at some point, so as to rule out distro-specific problem

view this post on Zulip Coq opam bench (Sep 17 2020 at 14:07):

Summary of the past 3 hours:

0 package installations, 0 errors, 0.00% errors :check:

view this post on Zulip Guillaume Claret (Sep 17 2020 at 14:25):

OK, so the mechanism to send messages seems to work, we will see by 72 hours if we have the next report

view this post on Zulip Guillaume Claret (Sep 17 2020 at 14:30):

Karl Palmskog said:

the versions of Coq and OCaml are actually parameters in those Docker images, so I think you could use something similar. In any case, I think one should think about uniformity of testing Coq packages on Linux at some point, so as to rule out distro-specific problem

OK, so I add that on my TODO-list.

view this post on Zulip Guillaume Claret (Sep 18 2020 at 16:09):

For the next Coq call https://github.com/coq/coq/wiki/Coq-Call-2020-09-23 I talk about how to open the opam bench infrastructure

view this post on Zulip Guillaume Claret (Sep 18 2020 at 16:10):

For now everything is on GitHub, but the machine is privately owned so that is probably the main blocker to open the development

view this post on Zulip Théo Zimmermann (Sep 19 2020 at 09:45):

@Guillaume Claret Please edit the wiki page to add your topic to the list.

view this post on Zulip Guillaume Claret (Sep 19 2020 at 10:31):

OK, done!

view this post on Zulip Coq opam bench (Sep 21 2020 at 15:11):

Summary of the past 72 hours:

0 package installations, 0 errors, 0.00% errors :check:

view this post on Zulip Guillaume Claret (Sep 21 2020 at 15:11):

OK, so the bench did fail (0 tests), I restarted the server

view this post on Zulip Guillaume Claret (Sep 21 2020 at 15:12):

(and fixed the bug)

view this post on Zulip Coq opam bench (Sep 24 2020 at 15:14):

Summary of the past 72 hours:

3190 package installations, 2 errors, 0.06% errors

view this post on Zulip Guillaume Claret (Sep 25 2020 at 08:26):

remnants of previous errors (fixed by the author)

view this post on Zulip Coq opam bench (Sep 27 2020 at 15:16):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Sep 27 2020 at 15:16):

* Coq 8.11.1, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies)
* Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
* Coq 8.8.1, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
* Coq 8.9.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies) * switch.1.0.2:
* Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)

14418 package installations, 10 errors, 0.07% errors

view this post on Zulip Guillaume Claret (Sep 28 2020 at 09:30):

OK, one of the error is - /bin/sh: 1: time: not found

view this post on Zulip Guillaume Claret (Sep 28 2020 at 09:31):

I will update the Docker images so that this utility is there

view this post on Zulip Guillaume Claret (Sep 28 2020 at 09:31):

I hope that the timeout errors (for Geocoq) do not persist

view this post on Zulip Coq opam bench (Sep 30 2020 at 15:19):

Summary of the past 72 hours:

9685 package installations, 1 error, 0.01% errors

view this post on Zulip Guillaume Claret (Sep 30 2020 at 15:21):

OK, so this is a very long timeout for coq-intuitionistic-nuprl (10 hours), but it should terminate

view this post on Zulip Karl Palmskog (Sep 30 2020 at 15:23):

@Guillaume Claret I would suggest blacklisting that project. This is an ancient release, unfortunately the maintainer has not done releases in many years now

view this post on Zulip Guillaume Claret (Sep 30 2020 at 15:23):

I have a feeling that the bench is now slower, this may be due to us testing more OCaml versions

view this post on Zulip Guillaume Claret (Sep 30 2020 at 15:23):

OK I will blacklist

view this post on Zulip Guillaume Claret (Sep 30 2020 at 15:24):

(actually when it succeeds it does not install anything, as there is a bug in the make install)

view this post on Zulip Karl Palmskog (Sep 30 2020 at 15:25):

see discussion in https://github.com/coq-community/manifesto/issues/60 - I did propose to get the project hosted in coq-community to get this and other issues fixed, but no luck.

view this post on Zulip Guillaume Claret (Sep 30 2020 at 15:27):

:ok:

view this post on Zulip Bas Spitters (Sep 30 2020 at 15:43):

I've pinged Vincent in the issue.

view this post on Zulip Karl Palmskog (Sep 30 2020 at 15:45):

thanks! I think just adding Set Default Proof Using "Type" and using make vos would make casual CI feasible for projects like NuPrl these days. It's interesting that Ralf Jung said that 4.5h of Iris a few years back was a turning point (which made them stop using unbundled type classes), in my mind Coq should be able to handle several days worth of proving just fine with the right CI tooling

view this post on Zulip Coq opam bench (Oct 03 2020 at 15:21):

Summary of the past 72 hours:

17787 package installations, 8 errors, 0.04% errors

view this post on Zulip Karl Palmskog (Oct 05 2020 at 10:20):

@Guillaume Claret the MetaCoq errors are due to a missing conf-time dependency. I can do the PR after I confirm the issue with MetaCoq devs.

view this post on Zulip Guillaume Claret (Oct 05 2020 at 12:06):

:ok:

view this post on Zulip Coq opam bench (Oct 06 2020 at 15:24):

Summary of the past 72 hours:

24255 package installations, 10 errors, 0.04% errors

view this post on Zulip Coq opam bench (Oct 09 2020 at 15:27):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Oct 09 2020 at 15:27):

19417 package installations, 12 errors, 0.06% errors

view this post on Zulip Coq opam bench (Oct 12 2020 at 15:29):

Summary of the past 72 hours:

14592 package installations, 5 errors, 0.03% errors

view this post on Zulip Coq opam bench (Oct 15 2020 at 15:32):

Summary of the past 72 hours:

16238 package installations, 10 errors, 0.06% errors

view this post on Zulip Coq opam bench (Oct 18 2020 at 15:35):

Summary of the past 72 hours:

16266 package installations, 6 errors, 0.04% errors

view this post on Zulip Karl Palmskog (Oct 18 2020 at 19:06):

ping @Li-yao that Ceres 0.3.0 is not actually compatible with Coq 8.8(.0) as per: https://coq-bench.github.io/clean/Linux-x86_64-4.08.1-2.0.5/released/8.8.0/ceres/0.3.0.html

File "./theories/CeresRoundtrip.v", line 296, characters 26-37:
- Error: No applicable tactic.

view this post on Zulip Karl Palmskog (Oct 18 2020 at 19:10):

@Guillaume Claret you may want to install time on the coq-bench machine:

The packages you requested declare the following system dependencies. Please make sure they are installed before retrying:
    time

view this post on Zulip Guillaume Claret (Oct 18 2020 at 19:48):

OK, I thought I did that (installing time), I will check the servers

view this post on Zulip Guillaume Claret (Oct 19 2020 at 15:27):

Indeed, the server did not restart as I expected for the time package; should be fixed for the next iteration

view this post on Zulip Coq opam bench (Oct 21 2020 at 15:38):

Summary of the past 72 hours:

6521 package installations, 3 errors, 0.05% errors

view this post on Zulip Coq opam bench (Oct 24 2020 at 15:41):

Summary of the past 72 hours:

16351 package installations, 3 errors, 0.02% errors

view this post on Zulip Guillaume Claret (Oct 25 2020 at 10:34):

I added Python3 for metacoq-translations.1.0~beta1+8.11

view this post on Zulip Coq opam bench (Oct 27 2020 at 15:42):

Summary of the past 72 hours:

1637 attempted package installations (including incompatible packages), 2 errors, 0.12% errors

view this post on Zulip Coq opam bench (Oct 30 2020 at 15:43):

Summary of the past 72 hours:

0 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Nov 02 2020 at 15:45):

Summary of the past 72 hours:

0 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Karl Palmskog (Nov 02 2020 at 15:47):

ping @Guillaume Claret I think the Coq opam bench has grind to a halt, is this maybe for maintenance, or is there an error? ("0 attempted package installations")

view this post on Zulip Guillaume Claret (Nov 02 2020 at 15:48):

Indeed, I have seen that and forgot to act on it

view this post on Zulip Guillaume Claret (Nov 02 2020 at 15:48):

thanks for the reminder

view this post on Zulip Guillaume Claret (Nov 02 2020 at 17:25):

I restarted the servers

view this post on Zulip Coq opam bench (Nov 05 2020 at 15:48):

Summary of the past 72 hours:

3280 attempted package installations (including incompatible packages), 1 error, 0.03% errors

view this post on Zulip Coq opam bench (Nov 08 2020 at 15:51):

Summary of the past 72 hours:

18040 attempted package installations (including incompatible packages), 7 errors, 0.04% errors

view this post on Zulip Coq opam bench (Nov 11 2020 at 15:53):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Nov 11 2020 at 15:53):

18040 attempted package installations (including incompatible packages), 15 errors, 0.08% errors

view this post on Zulip Coq opam bench (Nov 14 2020 at 15:56):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Nov 14 2020 at 15:56):

* Coq 8.7.1+2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies)
* Coq 8.8.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies) * infotheo.0.1.1:
* Coq 8.11.1, OCaml 4.11.1 :cross_mark: (error)
* Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error) * infotheo.0.1.2:
* Coq 8.11.1, OCaml 4.11.1 :cross_mark: (error)
* Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error) * infotheo.0.2:
* Coq 8.11.1, OCaml 4.11.1 :cross_mark: (error)
* Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error) * monae.0.1.1:
* Coq 8.11.1, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies) * monae.0.1.2:
* Coq 8.11.1, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies) * monae.0.2:
* Coq 8.11.1, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)

view this post on Zulip Coq opam bench (Nov 14 2020 at 15:56):

21324 attempted package installations (including incompatible packages), 31 errors, 0.15% errors

view this post on Zulip Karl Palmskog (Nov 14 2020 at 17:27):

@Guillaume Claret some of the failures are due to the absence of system libraries for conf-pkg-config. Maybe you could ensure those are installed?

view this post on Zulip Karl Palmskog (Nov 14 2020 at 17:29):

I think everything else just above except chick-blog will be fixed by recent PRs

view this post on Zulip Guillaume Claret (Nov 15 2020 at 13:39):

OK, indeed, I restarted the servers adding this package to the dependencies!

view this post on Zulip Coq opam bench (Nov 15 2020 at 13:39):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Nov 15 2020 at 13:39):

14766 attempted package installations (including incompatible packages), 25 errors, 0.17% errors

view this post on Zulip Coq opam bench (Nov 18 2020 at 13:42):

Summary of the past 72 hours:

0 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Nov 21 2020 at 13:45):

Summary of the past 72 hours:

18053 attempted package installations (including incompatible packages), 8 errors, 0.04% errors

view this post on Zulip Coq opam bench (Nov 24 2020 at 13:48):

Summary of the past 72 hours:

16439 attempted package installations (including incompatible packages), 4 errors, 0.02% errors

view this post on Zulip Karl Palmskog (Nov 24 2020 at 13:54):

@Guillaume Claret I really don't think we should keep testing with OCaml 4.04. It has a huge number of bugs, and even Coq 8.5.3 supports 4.05.0.

view this post on Zulip Karl Palmskog (Nov 24 2020 at 13:54):

for example: https://coq-bench.github.io/clean/Linux-x86_64-4.04.2-2.0.5/released/8.9.1/metacoq-pcuic/1.0~alpha1%2B8.9.html

view this post on Zulip Guillaume Claret (Nov 24 2020 at 15:39):

Indeed, there are still bugs from time to time

view this post on Zulip Guillaume Claret (Nov 24 2020 at 15:40):

I added this one to the blacklist https://github.com/coq-bench/make-html/blob/master/black_list.rb#L15

view this post on Zulip Guillaume Claret (Nov 24 2020 at 15:42):

I try to still test the old versions to preserve history. Indeed the fact that 8.5.3 works with 4.05 is an argument

view this post on Zulip Coq opam bench (Nov 27 2020 at 13:51):

Summary of the past 72 hours:

14804 attempted package installations (including incompatible packages), 2 errors, 0.01% errors

view this post on Zulip Coq opam bench (Nov 30 2020 at 13:54):

Summary of the past 72 hours:

14824 attempted package installations (including incompatible packages), 4 errors, 0.03% errors

view this post on Zulip Coq opam bench (Dec 03 2020 at 13:57):

Summary of the past 72 hours:

19863 attempted package installations (including incompatible packages), 9 errors, 0.05% errors

view this post on Zulip Guillaume Claret (Dec 04 2020 at 13:13):

For CompCert, error due to the instability of old OCaml compilers (again), I added this error for this package to the black-list

view this post on Zulip Coq opam bench (Dec 06 2020 at 14:00):

Summary of the past 72 hours:

16586 attempted package installations (including incompatible packages), 9 errors, 0.05% errors

view this post on Zulip Guillaume Claret (Dec 07 2020 at 12:12):

tactician-dummy is a new package, I will wait for more errors before to fix it

view this post on Zulip Guillaume Claret (Dec 07 2020 at 12:12):

other errors are due to timeout in dependency resolution

view this post on Zulip Coq opam bench (Dec 09 2020 at 14:03):

Summary of the past 72 hours:

18334 attempted package installations (including incompatible packages), 4 errors, 0.02% errors

view this post on Zulip Coq opam bench (Dec 12 2020 at 14:07):

Summary of the past 72 hours:

16686 attempted package installations (including incompatible packages), 3 errors, 0.02% errors

view this post on Zulip Guillaume Claret (Dec 13 2020 at 11:54):

Waiting for more errors to fix tactician-dummy

view this post on Zulip Coq opam bench (Dec 15 2020 at 14:10):

Summary of the past 72 hours:

18378 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Dec 18 2020 at 14:13):

Summary of the past 72 hours:

21760 attempted package installations (including incompatible packages), 3 errors, 0.01% errors

view this post on Zulip Coq opam bench (Dec 21 2020 at 14:16):

Summary of the past 72 hours:

10078 attempted package installations (including incompatible packages), 1 error, 0.01% errors

view this post on Zulip Coq opam bench (Dec 24 2020 at 14:19):

Summary of the past 72 hours:

15135 attempted package installations (including incompatible packages), 1 error, 0.01% errors

view this post on Zulip Coq opam bench (Dec 27 2020 at 14:22):

Summary of the past 72 hours:

18513 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Dec 30 2020 at 14:25):

Summary of the past 72 hours:

18513 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Jan 02 2021 at 14:29):

Summary of the past 72 hours:

18536 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Jan 05 2021 at 14:32):

Summary of the past 72 hours:

16884 attempted package installations (including incompatible packages), 2 errors, 0.01% errors

view this post on Zulip Coq opam bench (Jan 08 2021 at 14:35):

Summary of the past 72 hours:

13532 attempted package installations (including incompatible packages), 5 errors, 0.04% errors

view this post on Zulip Guillaume Claret (Jan 10 2021 at 14:26):

It seems like camlp5 now requires Perl, I will add it to the bench Dockerfile

view this post on Zulip Guillaume Melquiond (Jan 10 2021 at 14:45):

Note that this is a new major version of Camlp5. Perhaps you should stick to version 7, which does not require Perl. (No idea how much Camlp5 8.0 breaks compatibility.)

view this post on Zulip Karl Palmskog (Jan 10 2021 at 14:51):

not only does it require Perl itself, but also some non-standard Perl modules

view this post on Zulip Karl Palmskog (Jan 10 2021 at 14:52):

seemingly, our whole ecosystem is suddenly dependent on Perl version 5 (Coq is via zarith), a dying and nearly unmaintained language

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 14:53):

Given that camlp5 is hardly used anymore, it is even weirder to think that a fresh 8.0 branch was released.

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 14:53):

Does anybody know the motivation behind it?

view this post on Zulip Karl Palmskog (Jan 10 2021 at 14:54):

nope, all I know is that Chet Murthy seems to have taken over maintenance from Daniel recently

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 14:54):

Maintenance is a fairly different thing from major release though

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 14:55):

What Coq developments are relying on camlp5?

view this post on Zulip Karl Palmskog (Jan 10 2021 at 14:55):

it looked like Chet spearheaded the new release

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 14:55):

one of the reason for the integration of the gramlib library into Coq was precisely to sever the dependency to camlp5

view this post on Zulip Karl Palmskog (Jan 10 2021 at 14:56):

now we seemingly reap the rewards of that decision

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 14:57):

Last time I heard the last major package using camlp5 was elpi, but @Enrico Tassi worked on it, so I don't know the current status

view this post on Zulip Karl Palmskog (Jan 10 2021 at 14:58):

it could be that the camlp5 changes are behind the opam dependency resolution taking 2+ mins for coq-elpi on 4.05

view this post on Zulip Guillaume Melquiond (Jan 10 2021 at 14:59):

coq-coq-in-coq.8.10.0, coq-founify.8.5.0, coq-founify.8.10.0, coq-gappa.1.4.2+8.11, coq-graphs.8.10.0, coq-pts.8.10.0 have explicit dependencies on Camlp5; but I am pretty sure several other packages have implicit dependencies on it through Coq; in fact, Coq is presumably the largest user of Camlp5 (until the gramlib change, I mean)

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 15:00):

Gappa uses camlp5???

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 15:00):

Lord have mercy...

view this post on Zulip Karl Palmskog (Jan 10 2021 at 15:00):

Coq 8.9 is still used heavily and uses camlp5

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 15:00):

Unfortunately, indeed.

view this post on Zulip Guillaume Melquiond (Jan 10 2021 at 15:01):

notice the +8.11 in the version number, so that is not mine; but otherwise yes, Gappa has been using Camlp5 for as long as Coq has used it

view this post on Zulip Guillaume Melquiond (Jan 10 2021 at 15:02):

note that the goal was not to do any kind of parser modification, it was just so that the OCaml could compile with different versions of Coq; nowadays the library just uses cpp for preprocessing the OCaml code

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 15:03):

Somewhat ironic but much more reasonable, I believe.

view this post on Zulip Pierre-Marie Pédrot (Jan 10 2021 at 15:04):

According to the doc, camlp5-8 seems to be quite different from camlp5-7 which will be maintained separately, so it may make sense to stick to that old branch

view this post on Zulip Enrico Tassi (Jan 10 2021 at 16:55):

Elpi still depends on camlp5

view this post on Zulip Enrico Tassi (Jan 10 2021 at 16:57):

Hey, I got an ATD approved, and one of the tasks was to rewrite the parser. But covid stopped everything.

view this post on Zulip Coq opam bench (Jan 11 2021 at 14:39):

Summary of the past 72 hours:

15239 attempted package installations (including incompatible packages), 2 errors, 0.01% errors

view this post on Zulip Coq opam bench (Jan 14 2021 at 14:42):

Summary of the past 72 hours:

10218 attempted package installations (including incompatible packages), 3 errors, 0.03% errors

view this post on Zulip Coq opam bench (Jan 17 2021 at 14:45):

Summary of the past 72 hours:

15346 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Jan 20 2021 at 14:48):

Summary of the past 72 hours:

17100 attempted package installations (including incompatible packages), 5 errors, 0.03% errors

view this post on Zulip Lasse (Jan 21 2021 at 00:00):

See https://github.com/ocaml/dune/issues/4142 for the cause of the failures above.

With Coq 8.9.1, after upgrading to dune 2.8.1, compiling coq files does not seem to work anymore (due to unsupported command-line arguments it seems). Expected Behavior It works. Actual Behavior It...

view this post on Zulip Enrico Tassi (Jan 21 2021 at 07:22):

The problem is specific to dune and old coq versions, cc @Emilio Jesús Gallego Arias

view this post on Zulip Karl Palmskog (Jan 21 2021 at 07:28):

I don't think there is any sensible way to solve this at the opam level. Basically, we will realistically not be able to make everybody who uses Dune for Coq use some specific arcane set of requirements on the Coq and Dune versions

view this post on Zulip Karl Palmskog (Jan 21 2021 at 07:29):

Dune itself should inspect the Coq version to figure out which coqc options are available.

view this post on Zulip Guillaume Melquiond (Jan 21 2021 at 07:58):

I am not advocating for it, but you could always write in the opam file something like depends: [ ("dune" {< "2.8"} & "coq" {< "8.13"}) | ("dune" & "coq" {>= "8.13"}) ]

view this post on Zulip Guillaume Melquiond (Jan 21 2021 at 08:00):

(But again, I am certainly not advocating for it. It is just so that people are not left with the impression Opam could not handle it.)

view this post on Zulip Enrico Tassi (Jan 21 2021 at 08:05):

I'm worried that your (no) constraint on dune for 8.13 is too permissive, otherwise I don't get why the commit I link in the issue would have been added in the first place.

view this post on Zulip Enrico Tassi (Jan 21 2021 at 08:05):

(I don't get the commit contents either, but that is another story)

view this post on Zulip Guillaume Melquiond (Jan 21 2021 at 08:07):

Isn't any version of Dune compatible with Coq 8.13? (wth) If not, then sure, a constraint should be put on Dune.

view this post on Zulip Enrico Tassi (Jan 21 2021 at 08:08):

This was my recollection as well, no compat problems. But the commit must have had a motive

view this post on Zulip Enrico Tassi (Jan 21 2021 at 08:09):

I guess we can wait for @Emilio Jesús Gallego Arias to shed some light on this issue

view this post on Zulip Théo Zimmermann (Jan 21 2021 at 08:09):

@Enrico Tassi This commit is part of a bigger PR that adds support for native-compilation.

view this post on Zulip Théo Zimmermann (Jan 21 2021 at 08:10):

Previous versions of Dune do not have this PR at all and should be fully compatible with Coq 8.13.

view this post on Zulip Enrico Tassi (Jan 21 2021 at 08:10):

Right, but this does not explain why it is needed

view this post on Zulip Enrico Tassi (Jan 21 2021 at 08:11):

It seems a sort of defensive setup (from the commit message)

view this post on Zulip Enrico Tassi (Jan 21 2021 at 08:11):

But apparently breaks coq < 8.13

view this post on Zulip Karl Palmskog (Jan 21 2021 at 08:17):

fortunately the Docker images will continue to work with Dune+Coq<8.13 and 8.13, since they are using a pinned earlier version of Dune (2.5.1 I think)

view this post on Zulip Coq opam bench (Jan 23 2021 at 14:52):

Summary of the past 72 hours:

17106 attempted package installations (including incompatible packages), 9 errors, 0.05% errors

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2021 at 20:50):

This is a bug in the dune support as my commit didn't take into account the language versioning, will try to fix asap. The plan is that coq lang 0.2 will be compatible with most Coq versions, users bumping to coq lang 0.3 will indeed drop compatiblity with 8.9

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2021 at 20:51):

The reason we are explicit on the options is to still provide a fast compilation in dev profile.

view this post on Zulip Coq opam bench (Jan 26 2021 at 14:55):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Jan 26 2021 at 14:55):

18832 attempted package installations (including incompatible packages), 12 errors, 0.06% errors

view this post on Zulip Guillaume Claret (Jan 27 2021 at 15:49):

@Emilio Jesús Gallego Arias so you mean that in a future dune release these packages will magically get fixed, as opam should always install the latest dune version?

view this post on Zulip Guillaume Claret (Jan 27 2021 at 15:49):

(the packages failing with Coq 8.13 are now fixed)

view this post on Zulip Emilio Jesús Gallego Arias (Jan 27 2021 at 18:01):

Yes @Guillaume Claret , these packages should get working again.

view this post on Zulip Guillaume Claret (Jan 28 2021 at 08:56):

Top, thanks!

view this post on Zulip Coq opam bench (Jan 29 2021 at 14:58):

Summary of the past 72 hours:

13696 attempted package installations (including incompatible packages), 9 errors, 0.07% errors

view this post on Zulip Coq opam bench (Feb 01 2021 at 15:02):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Feb 01 2021 at 15:02):

* Coq 8.9.0, OCaml 4.05.0 :cross_mark: (error)
* Coq 8.9.1, OCaml 4.02.3 :cross_mark: (error) * type-infer.0.1.0:
* Coq 8.8.1, OCaml 4.08.1 :cross_mark: (error)
* Coq 8.9.0, OCaml 4.05.0 :cross_mark: (error)
* Coq 8.9.1, OCaml 4.02.3 :cross_mark: (error)

18967 attempted package installations (including incompatible packages), 15 errors, 0.08% errors

view this post on Zulip Guillaume Claret (Feb 04 2021 at 14:42):

I reported the metacoq issue there: https://github.com/MetaCoq/metacoq/issues/541

view this post on Zulip Guillaume Claret (Feb 04 2021 at 14:42):

fixing coq-switch, for tactician-dummy and type-infer I am waiting for the dune update

view this post on Zulip Coq opam bench (Feb 04 2021 at 15:06):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Feb 04 2021 at 15:06):

* Coq 8.9.0, OCaml 4.02.3 :cross_mark: (error) * vst-32.2.7:
* Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)
* Coq 8.13.0, OCaml 4.09.1 :cross_mark: (error)

19064 attempted package installations (including incompatible packages), 15 errors, 0.08% errors

view this post on Zulip Coq opam bench (Feb 07 2021 at 15:09):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Feb 07 2021 at 15:09):

* Coq 8.8.0, OCaml 4.03.0 :cross_mark: (error)
* Coq 8.9.1, OCaml 4.05.0 :cross_mark: (error) * type-infer.0.1.0:
* Coq 8.8.0, OCaml 4.02.3 :cross_mark: (error)
* Coq 8.8.0, OCaml 4.03.0 :cross_mark: (error)
* Coq 8.9.1, OCaml 4.05.0 :cross_mark: (error) * vst-32.2.7:
* Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error)
* Coq 8.12.1, OCaml 4.11.1 :cross_mark: (error) * vst.2.7:
* Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error)

15616 attempted package installations (including incompatible packages), 18 errors, 0.12% errors

view this post on Zulip Coq opam bench (Feb 10 2021 at 15:13):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Feb 10 2021 at 15:13):

* Coq 8.9.1, OCaml 4.06.1 :cross_mark: (error) * type-infer.0.1.0:
* Coq 8.8.2, OCaml 4.08.1 :cross_mark: (error)
* Coq 8.8.2, OCaml 4.09.1 :cross_mark: (error)
* Coq 8.9.1, OCaml 4.06.1 :cross_mark: (error) * vst-32.2.7:
* Coq 8.11.2, OCaml 4.11.1 :cross_mark: (error)
* Coq 8.13.0, OCaml 4.10.1 :cross_mark: (error) * vst.2.7:
* Coq 8.11.2, OCaml 4.11.1 :cross_mark: (error)

17363 attempted package installations (including incompatible packages), 18 errors, 0.10% errors

view this post on Zulip Coq opam bench (Feb 13 2021 at 15:16):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Feb 13 2021 at 15:16):

* Coq 8.11.1, OCaml 4.10.1 :cross_mark: (error)

20870 attempted package installations (including incompatible packages), 12 errors, 0.06% errors

view this post on Zulip Coq opam bench (Feb 16 2021 at 15:20):

Summary of the past 72 hours:

17416 attempted package installations (including incompatible packages), 8 errors, 0.05% errors

view this post on Zulip Coq opam bench (Feb 19 2021 at 15:23):

Summary of the past 72 hours:

15687 attempted package installations (including incompatible packages), 8 errors, 0.05% errors

view this post on Zulip Coq opam bench (Feb 22 2021 at 15:27):

Summary of the past 72 hours:

17460 attempted package installations (including incompatible packages), 10 errors, 0.06% errors

view this post on Zulip Coq opam bench (Feb 25 2021 at 15:31):

Summary of the past 72 hours:

15726 attempted package installations (including incompatible packages), 10 errors, 0.06% errors

view this post on Zulip Coq opam bench (Feb 28 2021 at 15:34):

Summary of the past 72 hours:

13997 attempted package installations (including incompatible packages), 7 errors, 0.05% errors

view this post on Zulip Guillaume Claret (Mar 01 2021 at 10:10):

For these errors, tactician-dummy.1.0~beta1 and type-infer.0.1.0 are known and related to dune which should be updated, corn is new and I wait for it to appear again, vst-32 is a timeout

view this post on Zulip Guillaume Melquiond (Mar 01 2021 at 10:17):

The error with bignums (used by corn) seems to be a race condition.

view this post on Zulip Guillaume Claret (Mar 01 2021 at 10:21):

OK thanks

view this post on Zulip Guillaume Claret (Mar 01 2021 at 10:22):

(so probably not worth to be fixed unless it appears again)

view this post on Zulip Guillaume Melquiond (Mar 01 2021 at 10:39):

It is actually easy to reproduce if your ocaml interpreter is slow.

view this post on Zulip Guillaume Claret (Mar 01 2021 at 10:40):

OK

view this post on Zulip Guillaume Melquiond (Mar 01 2021 at 10:42):

I am going to submit a pull request so that it gets fixed for the next releases, but I am not sure what the plan is for the older ones.

view this post on Zulip Guillaume Claret (Mar 01 2021 at 10:44):

:ok: For me it is fine if this is not fixed for the older versions, and then I can add it to the error messages black-list if it appears again too much

view this post on Zulip Guillaume Melquiond (Mar 01 2021 at 11:05):

Actually, due to an unrelated change to coq_makefile in Coq 8.8, the data race cannot occur. So, only Bignums for 8.7 is impacted by this issue.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2021 at 12:31):

The patch for dune has been merged, but not yet in a release , hopefully it happens soon.

view this post on Zulip Coq opam bench (Mar 03 2021 at 15:38):

Summary of the past 72 hours:

17513 attempted package installations (including incompatible packages), 8 errors, 0.05% errors

view this post on Zulip Coq opam bench (Mar 06 2021 at 15:42):

Summary of the past 72 hours:

17536 attempted package installations (including incompatible packages), 6 errors, 0.03% errors

view this post on Zulip Coq opam bench (Mar 09 2021 at 15:45):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Mar 09 2021 at 15:45):

* Coq 8.9.0, OCaml 4.03.0 :cross_mark: (error)
* Coq 8.9.1, OCaml 4.09.1 :cross_mark: (error) * vst-32.2.7:
* Coq 8.12.1, OCaml 4.10.1 :cross_mark: (error)

19339 attempted package installations (including incompatible packages), 17 errors, 0.09% errors

view this post on Zulip Coq opam bench (Mar 12 2021 at 15:49):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Mar 12 2021 at 15:49):

* Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)
* Coq 8.13.0, OCaml 4.07.1 :cross_mark: (error)

17590 attempted package installations (including incompatible packages), 13 errors, 0.07% errors

view this post on Zulip Coq opam bench (Mar 15 2021 at 15:53):

Summary of the past 72 hours:

19353 attempted package installations (including incompatible packages), 8 errors, 0.04% errors

view this post on Zulip Coq opam bench (Mar 18 2021 at 15:56):

Summary of the past 72 hours:

15840 attempted package installations (including incompatible packages), 5 errors, 0.03% errors

view this post on Zulip Coq opam bench (Mar 21 2021 at 16:00):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Mar 21 2021 at 16:00):

* Coq 8.13.0, OCaml 4.11.1 :cross_mark: (error) * vst-32.2.7:
* Coq 8.13.0, OCaml 4.11.1 :cross_mark: (error)

15879 attempted package installations (including incompatible packages), 13 errors, 0.08% errors

view this post on Zulip Guillaume Claret (Mar 24 2021 at 14:14):

I am looking at fixing Monae

view this post on Zulip Coq opam bench (Mar 24 2021 at 16:04):

Summary of the past 72 hours:

14150 attempted package installations (including incompatible packages), 2 errors, 0.01% errors

view this post on Zulip Reynald Affeldt (Mar 24 2021 at 16:26):

@Guillaume Claret the errors I can see in the above Coq opam bench are due to the use of a too recent version of mathcomp-analysis; 0.3.6 and above cannot be used with monae 0.2 :-(

view this post on Zulip Reynald Affeldt (Mar 24 2021 at 16:27):

should I PR to fix the incriminated releases?

view this post on Zulip Guillaume Claret (Mar 24 2021 at 19:16):

OK. I just merged this pull-request https://github.com/coq/opam-coq-archive/pull/1663 which should help

view this post on Zulip Reynald Affeldt (Mar 25 2021 at 01:33):

Thank you!

view this post on Zulip Coq opam bench (Mar 26 2021 at 21:06):

Summary of the past 72 hours:

14152 attempted package installations (including incompatible packages), 2 errors, 0.01% errors

view this post on Zulip Coq opam bench (Mar 29 2021 at 21:10):

Summary of the past 72 hours:

3550 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Apr 01 2021 at 21:13):

Summary of the past 72 hours:

17754 attempted package installations (including incompatible packages), 6 errors, 0.03% errors

view this post on Zulip Coq opam bench (Apr 04 2021 at 21:17):

Summary of the past 72 hours:

14212 attempted package installations (including incompatible packages), 6 errors, 0.04% errors

view this post on Zulip Coq opam bench (Apr 07 2021 at 21:21):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Apr 07 2021 at 21:21):

* Coq 8.12.1, OCaml 4.09.1 :cross_mark: (error)

12459 attempted package installations (including incompatible packages), 12 errors, 0.10% errors

view this post on Zulip Coq opam bench (Apr 10 2021 at 21:25):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Apr 10 2021 at 21:25):

* Coq 8.11.1, OCaml 4.09.1 :cross_mark: (error)
* Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)
* Coq 8.13.0, OCaml 4.10.1 :cross_mark: (error) * hierarchy-builder-shim.1.1.0:
* Coq 8.5.0~camlp4, OCaml 4.03.0 :cross_mark: (error)
* Coq 8.5.2~camlp4, OCaml 4.02.3 :cross_mark: (error)
* Coq 8.6, OCaml 4.02.3 :cross_mark: (error)
* Coq 8.6, OCaml 4.05.0 :cross_mark: (error)
* Coq 8.7.0, OCaml 4.04.2 :cross_mark: (error)
* Coq 8.7.0, OCaml 4.05.0 :cross_mark: (error)
* Coq 8.7.1, OCaml 4.08.1 :cross_mark: (error) * intuitionistic-nuprl.8.6.0:
* Coq 8.6, OCaml 4.02.3 :cross_mark: (error)
* Coq 8.6, OCaml 4.05.0 :cross_mark: (error) * vst-32.2.7:
* Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)
* Coq 8.13.0, OCaml 4.10.1 :cross_mark: (error)

21364 attempted package installations (including incompatible packages), 25 errors, 0.12% errors

view this post on Zulip Guillaume Claret (Apr 10 2021 at 22:46):

All errors should be fixed or related to some kind of instability (still, that is a lot of instability now)

view this post on Zulip Guillaume Claret (Apr 10 2021 at 22:46):

(I should probably restart the servers with some fixes)

view this post on Zulip Guillaume Claret (Apr 10 2021 at 22:47):

In particular to remove the uninstallation errors, which should now be impossible with the automatic file tracking of opam

view this post on Zulip Guillaume Claret (Apr 10 2021 at 22:47):

and the timeout errors (the timeouts need to be increased)

view this post on Zulip Coq opam bench (Apr 13 2021 at 21:29):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Apr 13 2021 at 21:29):

10695 attempted package installations (including incompatible packages), 9 errors, 0.08% errors

view this post on Zulip Coq opam bench (Apr 16 2021 at 21:33):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Apr 16 2021 at 21:33):

23180 attempted package installations (including incompatible packages), 15 errors, 0.06% errors

view this post on Zulip Guillaume Claret (Apr 17 2021 at 19:30):

the errors with elpi should be fixed I think, as the package got updated; I also increased the installation timeout for vst

view this post on Zulip Coq opam bench (Apr 19 2021 at 21:36):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Apr 19 2021 at 21:36):

view this post on Zulip Coq opam bench (Apr 19 2021 at 21:36):

view this post on Zulip Coq opam bench (Apr 19 2021 at 21:36):

view this post on Zulip Coq opam bench (Apr 19 2021 at 21:36):

8928 attempted package installations (including incompatible packages), 47 errors, 0.53% errors

view this post on Zulip Guillaume Claret (Apr 20 2021 at 14:05):

OK so there seems to be an architectural bug in the coq-bench, I need to investigate that

view this post on Zulip Coq opam bench (Apr 22 2021 at 21:39):

Summary of the past 72 hours:

12511 attempted package installations (including incompatible packages), 7 errors, 0.06% errors

view this post on Zulip Guillaume Claret (Apr 22 2021 at 21:44):

All these errors should be fixed now

view this post on Zulip Coq opam bench (Apr 25 2021 at 21:42):

Summary of the past 72 hours:

14306 attempted package installations (including incompatible packages), 9 errors, 0.06% errors

view this post on Zulip Guillaume Claret (Apr 26 2021 at 08:38):

Fixes ongoing for the errors listed there

view this post on Zulip Coq opam bench (Apr 28 2021 at 21:45):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Apr 28 2021 at 21:45):

* Coq 8.13.0, OCaml 4.09.1 :large_orange_diamond: (error with dependencies)
* Coq 8.13.1, OCaml 4.12.0 :large_orange_diamond: (error with dependencies) * vst-64.2.6:
* Coq 8.12.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.12.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies)

19678 attempted package installations (including incompatible packages), 18 errors, 0.09% errors

view this post on Zulip Coq opam bench (May 01 2021 at 21:48):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (May 01 2021 at 21:48):

* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * elpi.1.9.3:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * elpi.1.9.4:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * elpi.1.9.5:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * elpi.1.9.6:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * elpi.1.9.7:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * freespec-core.0.3:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * graph-theory.0.8:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * hierarchy-builder.1.0.0:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * hierarchy-builder.1.1.0:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * http.0.1.0:

view this post on Zulip Coq opam bench (May 01 2021 at 21:48):

* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * infotheo.0.3:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * infotheo.0.3.1:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * infotheo.0.3.2:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * itree-io.0.1.0:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * itree.4.0.0:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * mathcomp-analysis.0.3.5:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * mathcomp-analysis.0.3.6:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * mathcomp-analysis.0.3.7:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * mathcomp-multinomials.1.5.4:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * min-imports.1.0.0:

view this post on Zulip Coq opam bench (May 01 2021 at 21:48):

* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * min-imports.1.0.1:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * min-imports.1.0.2:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * monae.0.3:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * monae.0.3.1:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * monae.0.3.2:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * of-ocaml.2.0.0:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * tactician-dummy.1.0~beta1:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * type-infer.0.1.0:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * vst-32.2.7.1:
* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * vst.2.7.1:

view this post on Zulip Coq opam bench (May 01 2021 at 21:48):

* Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)

17890 attempted package installations (including incompatible packages), 40 errors, 0.22% errors

view this post on Zulip Guillaume Claret (May 02 2021 at 10:58):

Adding these ZArith errors to the black-list (this is due to an issue in the bench system to properly re-install dependencies of Coq)

view this post on Zulip Coq opam bench (May 02 2021 at 11:00):

Summary of the past 72 hours:

17890 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (May 05 2021 at 11:04):

Summary of the past 72 hours:

19680 attempted package installations (including incompatible packages), 1 error, 0.01% errors

view this post on Zulip Coq opam bench (May 08 2021 at 11:07):

Summary of the past 72 hours:

17901 attempted package installations (including incompatible packages), 1 error, 0.01% errors

view this post on Zulip Coq opam bench (May 11 2021 at 11:11):

Summary of the past 72 hours:

12536 attempted package installations (including incompatible packages), 4 errors, 0.03% errors

view this post on Zulip Coq opam bench (May 14 2021 at 11:14):

Summary of the past 72 hours:

16120 attempted package installations (including incompatible packages), 5 errors, 0.03% errors

view this post on Zulip Coq opam bench (May 17 2021 at 11:17):

Summary of the past 72 hours:

14335 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (May 20 2021 at 11:21):

Summary of the past 72 hours:

16128 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (May 23 2021 at 11:24):

Summary of the past 72 hours:

14346 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (May 26 2021 at 11:28):

Summary of the past 72 hours:

5385 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (May 29 2021 at 11:31):

Summary of the past 72 hours:

19758 attempted package installations (including incompatible packages), 2 errors, 0.01% errors

view this post on Zulip Coq opam bench (Jun 01 2021 at 11:35):

Summary of the past 72 hours:

19760 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Jun 04 2021 at 11:39):

Summary of the past 72 hours:

10776 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Jun 07 2021 at 11:42):

Summary of the past 72 hours:

17966 attempted package installations (including incompatible packages), 12 errors, 0.07% errors

view this post on Zulip Coq opam bench (Jun 10 2021 at 11:46):

Summary of the past 72 hours:

14376 attempted package installations (including incompatible packages), 10 errors, 0.07% errors

view this post on Zulip Coq opam bench (Jun 13 2021 at 11:49):

Summary of the past 72 hours:

19892 attempted package installations (including incompatible packages), 3 errors, 0.02% errors

view this post on Zulip Coq opam bench (Jun 16 2021 at 11:53):

Summary of the past 72 hours:

14488 attempted package installations (including incompatible packages), 1 error, 0.01% errors

view this post on Zulip Coq opam bench (Jun 19 2021 at 11:57):

Summary of the past 72 hours:

16330 attempted package installations (including incompatible packages), 3 errors, 0.02% errors

view this post on Zulip Coq opam bench (Jun 22 2021 at 12:00):

Summary of the past 72 hours:

16364 attempted package installations (including incompatible packages), 1 error, 0.01% errors

view this post on Zulip Coq opam bench (Jun 25 2021 at 12:04):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Jun 25 2021 at 12:04):

view this post on Zulip Coq opam bench (Jun 25 2021 at 12:04):

16386 attempted package installations (including incompatible packages), 26 errors, 0.16% errors

view this post on Zulip Coq opam bench (Jun 28 2021 at 12:08):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Jun 28 2021 at 12:08):

* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * compcert.3.7~coq-platform:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * compcert.3.7~coq-platform~open-source:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * compcert.3.8:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * compcert.3.9:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * flocq.3.4.1:
* Coq 8.11.1, OCaml 4.10.2 :cross_mark: (error)
* Coq 8.11.2, OCaml 4.06.1 :cross_mark: (error) * gappa.1.4.3:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * gappa.1.4.4:

view this post on Zulip Coq opam bench (Jun 28 2021 at 12:08):

* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * gappa.1.4.5:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * gappa.1.4.6:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * hydra-battles.0.4:
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
* Coq 8.12.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies) * interval.3.4.2:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * interval.4.0.0:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * interval.4.1.0:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)

view this post on Zulip Coq opam bench (Jun 28 2021 at 12:08):

view this post on Zulip Coq opam bench (Jun 28 2021 at 12:08):

* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * vst-64.2.6:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies) * vst.2.6:
* Coq 8.11.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
* Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)

12761 attempted package installations (including incompatible packages), 56 errors, 0.44% errors

view this post on Zulip Coq opam bench (Jul 01 2021 at 12:12):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Jul 01 2021 at 12:12):

view this post on Zulip Coq opam bench (Jul 01 2021 at 12:12):

18240 attempted package installations (including incompatible packages), 28 errors, 0.15% errors

view this post on Zulip Guillaume Claret (Jul 01 2021 at 13:50):

OK, it seems the error is from before the update of coq-flocq, it should be fixed now

view this post on Zulip Guillaume Claret (Jul 01 2021 at 13:50):

That shows that many packages are using coq-flocq!

view this post on Zulip Guillaume Melquiond (Jul 01 2021 at 14:00):

But not all of them. It seems hydra-battle fails because equations does not depend on ocamlfind (@Matthieu Sozeau ). As for waterproof, it simply fails.

view this post on Zulip Guillaume Claret (Jul 01 2021 at 14:44):

OK, good catch, I haven't seen for hydra-battle! I fixed waterproof.

view this post on Zulip Matthieu Sozeau (Jul 01 2021 at 15:11):

Hmm, didn't know about that problem, @Guillaume Claret can you add the dependency?

view this post on Zulip Guillaume Claret (Jul 01 2021 at 15:18):

Matthieu Sozeau said:

Hmm, didn't know about that problem, Guillaume Claret can you add the dependency?

OK

view this post on Zulip Guillaume Melquiond (Jul 01 2021 at 15:24):

Just to be clear, that is how I interpret the error message, but perhaps there is a more fundamental issue. (And since Github is down, I cannot check the structure of Equations and whether it really uses Ocamlfind.)

view this post on Zulip Guillaume Melquiond (Jul 01 2021 at 15:26):

Okay, it is back up, and yes, Equations explicitly uses Ocamlfind.

view this post on Zulip Matthieu Sozeau (Jul 01 2021 at 16:10):

I think it does in the doc target or configure?

view this post on Zulip Guillaume Claret (Jul 01 2021 at 18:22):

After looking at it, it seems that coq_makefile generates OCaml rules which use ocamlfind, like CAMLOPTC ?= "$(OCAMLFIND)" opt -c

view this post on Zulip Coq opam bench (Jul 04 2021 at 12:15):

Summary of the past 72 hours:

16430 attempted package installations (including incompatible packages), 3 errors, 0.02% errors

view this post on Zulip Coq opam bench (Jul 07 2021 at 12:19):

Summary of the past 72 hours:

18270 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Matthieu Sozeau (Jul 07 2021 at 12:27):

Guillaume Claret said:

After looking at it, it seems that coq_makefile generates OCaml rules which use ocamlfind, like CAMLOPTC ?= "$(OCAMLFIND)" opt -c

Indeed, ocamlfind is used because we have a rule that requires it to build a toplevel with equations for debugging. I'll try to remove that seldom used dependency in the future.

view this post on Zulip Gaëtan Gilbert (Jul 07 2021 at 12:29):

don't we use ocamlfind to build plugins in general?

view this post on Zulip Guillaume Melquiond (Jul 07 2021 at 12:51):

Yes, removing the dependency on Ocamlfind does not bring much to the user. It just needs to be documented in the Opam packages of relevant Coq libraries, so that Opam reinstalls it in case the user (accidentally) removed it.

view this post on Zulip Coq opam bench (Jul 10 2021 at 12:23):

Summary of the past 72 hours:

16443 attempted package installations (including incompatible packages), 2 errors, 0.01% errors

view this post on Zulip Coq opam bench (Jul 13 2021 at 12:27):

Summary of the past 72 hours:

20097 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Jul 16 2021 at 12:30):

Summary of the past 72 hours:

16447 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Jul 19 2021 at 12:34):

Summary of the past 72 hours:

14624 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Jul 22 2021 at 12:38):

Summary of the past 72 hours:

14624 attempted package installations (including incompatible packages), 2 errors, 0.01% errors

view this post on Zulip Coq opam bench (Jul 25 2021 at 12:42):

Summary of the past 72 hours:

14624 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Jul 28 2021 at 12:45):

Summary of the past 72 hours:

16452 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Jul 31 2021 at 12:49):

Summary of the past 72 hours:

16452 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Aug 03 2021 at 12:53):

Summary of the past 72 hours:

10978 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Aug 06 2021 at 12:57):

Summary of the past 72 hours:

10998 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Aug 09 2021 at 13:00):

Summary of the past 72 hours:

16537 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Aug 12 2021 at 13:04):

Summary of the past 72 hours:

20230 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Aug 15 2021 at 13:08):

Summary of the past 72 hours:

16567 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Aug 18 2021 at 13:12):

Summary of the past 72 hours:

14741 attempted package installations (including incompatible packages), 4 errors, 0.03% errors

view this post on Zulip Coq opam bench (Aug 21 2021 at 13:17):

Summary of the past 72 hours:

12901 attempted package installations (including incompatible packages), 2 errors, 0.02% errors

view this post on Zulip Coq opam bench (Aug 24 2021 at 13:21):

Summary of the past 72 hours:

18432 attempted package installations (including incompatible packages), 4 errors, 0.02% errors

view this post on Zulip Coq opam bench (Aug 27 2021 at 13:25):

Summary of the past 72 hours:

12929 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Aug 30 2021 at 13:29):

Summary of the past 72 hours:

18480 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Sep 02 2021 at 13:33):

Summary of the past 72 hours:

16632 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Sep 05 2021 at 13:37):

Summary of the past 72 hours:

20333 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Sep 08 2021 at 13:41):

Summary of the past 72 hours:

12943 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Sep 11 2021 at 13:45):

Summary of the past 72 hours:

16643 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Sep 14 2021 at 12:47):

Summary of the past 72 hours:

18500 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Sep 17 2021 at 12:51):

Summary of the past 72 hours:

0 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Karl Palmskog (Sep 17 2021 at 14:24):

ping @Guillaume Claret looks like there might be something wrong with the Coq opam bench (no package installation attempts for 3+ days)

view this post on Zulip Guillaume Claret (Sep 17 2021 at 15:28):

Yes, indeed, I restarted everything for upgrades, thanks for the ping

view this post on Zulip Coq opam bench (Sep 20 2021 at 12:55):

Summary of the past 72 hours:

14800 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Sep 23 2021 at 12:59):

Summary of the past 72 hours:

9250 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Sep 26 2021 at 13:03):

Summary of the past 72 hours:

16650 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Sep 29 2021 at 13:07):

Summary of the past 72 hours:

14831 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Oct 02 2021 at 13:11):

Summary of the past 72 hours:

14875 attempted package installations (including incompatible packages), 2 errors, 0.01% errors

view this post on Zulip Coq opam bench (Oct 05 2021 at 13:15):

Summary of the past 72 hours:

13055 attempted package installations (including incompatible packages), 1 error, 0.01% errors

view this post on Zulip Coq opam bench (Oct 08 2021 at 13:20):

Summary of the past 72 hours:

16846 attempted package installations (including incompatible packages), 4 errors, 0.02% errors

view this post on Zulip Coq opam bench (Oct 11 2021 at 13:23):

Summary of the past 72 hours:

15004 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:

view this post on Zulip Coq opam bench (Oct 14 2021 at 13:28):

Summary of the past 72 hours:

15028 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:


Last updated: Oct 15 2021 at 19:03 UTC