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 Blaauwbroek (Jan 21 2021 at 00:00):

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

coqc: ondemand: no such file or directory · Issue #4142 · ocaml/dune
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:

view this post on Zulip Coq opam bench (Oct 17 2021 at 13:32):

Summary of the past 72 hours:

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

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

Summary of the past 72 hours:

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

* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * list-string.2.1.0:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * list-string.2.1.1:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * menhirlib.20200525:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * menhirlib.20200612:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * menhirlib.20200619:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * menhirlib.20200624:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * menhirlib.20201122:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * menhirlib.20201201:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * menhirlib.20201214:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * menhirlib.20201216:

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

* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * moment.1.1.0:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * moment.1.2.0:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * semantics.8.11.1:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error) * waterproof.1.0.0:
* Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error)

20707 attempted package installations (including incompatible packages), 24 errors, 0.12% errors

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

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Oct 26 2021 at 13:45):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Oct 29 2021 at 13:49):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Nov 01 2021 at 13:53):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Nov 01 2021 at 13:53):

view this post on Zulip Coq opam bench (Nov 01 2021 at 13:53):

20865 attempted package installations (including incompatible packages), 19 errors, 0.09% errors

view this post on Zulip Guillaume Claret (Nov 01 2021 at 19:07):

Most errors for 8.14 are now fixed

view this post on Zulip Guillaume Claret (Nov 01 2021 at 19:07):

(remnants of previous builds)

view this post on Zulip Guillaume Claret (Nov 01 2021 at 19:07):

A bench process is also running with OCaml 4.13 now

view this post on Zulip Coq opam bench (Nov 04 2021 at 13:57):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Nov 04 2021 at 13:57):

7621 attempted package installations (including incompatible packages), 16 errors, 0.21% errors

view this post on Zulip Coq opam bench (Nov 07 2021 at 14:01):

Summary of the past 72 hours:

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

view this post on Zulip Karl Palmskog (Nov 07 2021 at 16:22):

the 4.13 process is probably going to have tons and tons of errors, I don't think plugins have been fixed yet. So I don't think we should add upper bounds excluding 4.13 until this has been decided as the only way to go.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:30):

8.14.0 is fixed

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 16:32):

No need to modify thousands of packages, just put the fix in the coq packages that need it IMO

view this post on Zulip Coq opam bench (Nov 12 2021 at 13:32):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Nov 12 2021 at 13:32):

* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * coinduction.1.1:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * coinduction.1.2:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * coinduction.1.3:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * color.1.8.1:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * compcert-32.3.8:
* Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error :fire:)
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * compcert-32.3.9:
* Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error :fire:)

view this post on Zulip Coq opam bench (Nov 12 2021 at 13:32):

* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * compcert-64.3.7+8.12~coq_platform:
* Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error :fire:) * compcert-64.3.7+8.12~coq_platform~open_source:
* Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error :fire:) * compcert.3.7+8.12~coq_platform:
* Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error :fire:) * compcert.3.7+8.12~coq_platform~open_source:
* Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error :fire:) * coqeal.1.0.5:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * coqeal.1.0.6:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * coqeal.1.1.0:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * coqprime.1.0.6:

view this post on Zulip Coq opam bench (Nov 12 2021 at 13:32):

* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * corn.8.13.0:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * dpdgraph.0.6.9:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * dpdgraph.1.0+8.13:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * equations.1.2.3+8.13:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * equations.1.2.4+8.13:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * equations.1.3~beta1+8.13:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)

view this post on Zulip Coq opam bench (Nov 12 2021 at 13:32):

view this post on Zulip Coq opam bench (Nov 12 2021 at 13:32):

* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * hammer-tactics.1.3.2+8.13:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * hammer.1.3.1+8.13:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * hammer.1.3.2+8.13:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * hydra-battles.0.4:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * hydra-battles.0.5:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * interval.4.0.0:
* Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error :fire:) * interval.4.1.0:

view this post on Zulip Coq opam bench (Nov 12 2021 at 13:32):

* Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error :fire:)
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * interval.4.1.1:
* Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error :fire:)
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * interval.4.2.0:
* Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error :fire:)
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * interval.4.3.0:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * itauto.8.13:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * katamaran.0.1.0:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)

view this post on Zulip Coq opam bench (Nov 12 2021 at 13:32):

view this post on Zulip Coq opam bench (Nov 12 2021 at 13:32):

* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * pi-agm.1.2.6:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * quickchick.1.5.0:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * quickchick.1.5.1:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * reduction-effects.0.1.2:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * reduction-effects.0.1.3:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * relation-algebra.1.7.5:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * smpl.8.13:

view this post on Zulip Coq opam bench (Nov 12 2021 at 13:32):

* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * switch.1.0.5:
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * unicoq.1.5+8.13:
* Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
* Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:) * vst-32.2.7:
* Coq 8.12.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * vst-32.2.7.1:
* Coq 8.12.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:) * vst-32.2.8:
* Coq 8.12.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
* Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)

view this post on Zulip Coq opam bench (Nov 12 2021 at 13:32):

21100 attempted package installations (including incompatible packages), 135 errors, 0.64% errors

view this post on Zulip Karl Palmskog (Nov 12 2021 at 13:33):

@Emilio Jesús Gallego Arias @Enrico Tassi so how should we tackle 8.13 and 8.12 errors according to above?

view this post on Zulip Karl Palmskog (Nov 12 2021 at 13:35):

personally I wouldn't mind doing this for 8.12 and 8.13, but they have 3 opam packages each: https://github.com/ocaml/opam-repository/commit/37a6ba42b79fd5e6c15604d5f1ef45170449fb3e

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 14:15):

@Karl Palmskog adapting the patch for 8.14 should work

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 14:15):

annoying but easy I think

view this post on Zulip Karl Palmskog (Nov 12 2021 at 14:17):

OK, but then should we ask for help from opam repo maintainers? six packages changed with tons of deps and reverse deps is bound to get stuck...

view this post on Zulip Guillaume Claret (Nov 14 2021 at 22:01):

I think only 8.13 is impacted, and 8.12 errors above are related to something else

view this post on Zulip Guillaume Claret (Nov 14 2021 at 22:02):

We can try to fix 8.13.2 first and see how it goes

view this post on Zulip Guillaume Claret (Nov 15 2021 at 09:21):

I added a PR for Coq 8.13.2: https://github.com/ocaml/opam-repository/pull/20025

view this post on Zulip Coq opam bench (Nov 15 2021 at 13:36):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Nov 15 2021 at 13:36):

view this post on Zulip Coq opam bench (Nov 15 2021 at 13:36):

view this post on Zulip Coq opam bench (Nov 15 2021 at 13:36):

view this post on Zulip Coq opam bench (Nov 15 2021 at 13:36):

view this post on Zulip Coq opam bench (Nov 15 2021 at 13:36):

view this post on Zulip Coq opam bench (Nov 15 2021 at 13:36):

view this post on Zulip Coq opam bench (Nov 15 2021 at 13:36):

15376 attempted package installations (including incompatible packages), 78 errors, 0.51% errors

view this post on Zulip Guillaume Claret (Nov 17 2021 at 17:17):

https://github.com/ocaml/opam-repository/pull/20051 should fix issues for Coq 8.13.0 and 8.13.1. After that bench errors should only be due to updates propagating.

view this post on Zulip Karl Palmskog (Nov 17 2021 at 17:18):

but isn't 8.12.2 affected as well?

view this post on Zulip Guillaume Claret (Nov 18 2021 at 12:35):

It should be fine as it is not compatible with OCaml 4.13

view this post on Zulip Coq opam bench (Nov 18 2021 at 13:41):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Nov 18 2021 at 13:41):

view this post on Zulip Coq opam bench (Nov 18 2021 at 13:41):

view this post on Zulip Coq opam bench (Nov 18 2021 at 13:41):

view this post on Zulip Coq opam bench (Nov 18 2021 at 13:41):

view this post on Zulip Coq opam bench (Nov 18 2021 at 13:41):

view this post on Zulip Coq opam bench (Nov 18 2021 at 13:41):

11541 attempted package installations (including incompatible packages), 61 errors, 0.53% errors

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

Summary of the past 72 hours:

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

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

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

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

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

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

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

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

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

15393 attempted package installations (including incompatible packages), 122 errors, 0.79% errors

view this post on Zulip Coq opam bench (Nov 24 2021 at 13:49):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Nov 27 2021 at 13:54):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Nov 27 2021 at 13:54):

view this post on Zulip Coq opam bench (Nov 27 2021 at 13:54):

view this post on Zulip Coq opam bench (Nov 27 2021 at 13:54):

view this post on Zulip Coq opam bench (Nov 27 2021 at 13:54):

view this post on Zulip Coq opam bench (Nov 27 2021 at 13:54):

view this post on Zulip Coq opam bench (Nov 27 2021 at 13:54):

view this post on Zulip Coq opam bench (Nov 27 2021 at 13:54):

23152 attempted package installations (including incompatible packages), 99 errors, 0.43% errors

view this post on Zulip Karl Palmskog (Nov 27 2021 at 14:01):

@Michael Soegtrop you may want to be aware that we have opam archive failures for some CompCert packages due to Flocq 4, see for example here for CompCert 3.7: https://coq-bench.github.io/clean/Linux-x86_64-4.08.1-2.0.5/released/8.12.0/compcert-64/3.7%2B8.12~coq_platform.html

There is also a very mystifying Gappa failure for 8.12:

Error: The reference Build_radix was not found in the current environment.

We will work on setting upper bounds for the packages over time, but it won't happen overnight.

view this post on Zulip Guillaume Claret (Nov 28 2021 at 18:45):

I have made pull-requests to fix most of the bugs (except Gappa). We will see the results once they are merged.

view this post on Zulip Michael Soegtrop (Nov 29 2021 at 10:27):

I will take care of gappa.

view this post on Zulip Michael Soegtrop (Nov 30 2021 at 10:31):

@Karl Palmskog : regarding the failure of coq-gappa.1.4.4: I can't reproduce this in Coq Platform, but I am using Coq 8.12.2 not Coq 8.12.0. Why do we run CI with 8.12.0 rather than 8.12.2? I don't think it would be desirable to somehow patch gappa 1.4.4 to make it compatible to Coq 8.12.0 when it is compatible with Coq 8.12.2.

@Guillaume Melquiond : FYI.

view this post on Zulip Karl Palmskog (Nov 30 2021 at 10:40):

pinging @Guillaume Claret since he runs the coq opam bench. I believe he tests with many Coq versions over time, so both 8.12.0 and 8.12.2 should be included. Maybe it is the case that the Gappa problem is only on 8.12.0 (and 8.12.1)?

view this post on Zulip Karl Palmskog (Nov 30 2021 at 10:42):

if we can't reproduce on 8.12.2, then we can just mark gappa.1.4.4 as 8.12.0 incompatible.

view this post on Zulip Karl Palmskog (Nov 30 2021 at 10:52):

@Michael Soegtrop did you try the following on 8.12.2:

Then, I get a failure, so this may all be due to Flocq 4 in the end, and we may only need to adjust the Flocq bound (to < 4)

view this post on Zulip Guillaume Claret (Nov 30 2021 at 11:01):

Yes indeed, I am testing all the Coq versions so that we do not miss anything. Statistically, when a package fails it should fail with many versions at the same time so we do not miss much I guess from testing everything.

view this post on Zulip Guillaume Claret (Nov 30 2021 at 11:03):

For Gappa, changing the bound for Flocq is also what @Guillaume Melquiond thinks https://github.com/coq/opam-coq-archive/pull/1963#issuecomment-981318512 and I actually did the change in https://github.com/coq/opam-coq-archive/pull/1965

view this post on Zulip Karl Palmskog (Nov 30 2021 at 11:03):

I think we can just add the < 4 in coq-gappa.1.4.4 and see how it goes, I can do that

view this post on Zulip Guillaume Claret (Nov 30 2021 at 11:03):

Yes, I have done that already :) https://github.com/coq/opam-coq-archive/pull/1965

view this post on Zulip Karl Palmskog (Nov 30 2021 at 11:06):

so then I guess Michael has already validated that it works (I was using an old opam repo state)

view this post on Zulip Guillaume Claret (Nov 30 2021 at 11:07):

ah OK, yes!

view this post on Zulip Michael Soegtrop (Nov 30 2021 at 13:10):

I was about to say that coq-gappa.1.4.4 has "coq-flocq" {>= "3.0" & < "4~"}, but I see that this is just since yesterday.

@Guillaume Claret : so is this fixed now in CI or not?

view this post on Zulip Guillaume Claret (Nov 30 2021 at 13:16):

Yes this is fixed

view this post on Zulip Coq opam bench (Nov 30 2021 at 13:58):

Summary of the past 72 hours:

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

view this post on Zulip Michael Soegtrop (Nov 30 2021 at 14:10):

Btw.: is there an overview over all failures of all latest builds somewhere?

view this post on Zulip Karl Palmskog (Nov 30 2021 at 16:01):

I think the only "latest" overview is in this Zulip topic

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

Summary of the past 72 hours:

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

view this post on Zulip Guillaume Claret (Dec 05 2021 at 17:40):

The homepage of the project https://coq-bench.github.io/ also gives a global overview, but does not directly point to the latest failures

view this post on Zulip Coq opam bench (Dec 06 2021 at 14:09):

Summary of the past 72 hours:

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

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

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Dec 12 2021 at 14:18):

Summary of the past 72 hours:

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

view this post on Zulip Karl Palmskog (Dec 12 2021 at 14:26):

@Guillaume Claret you need to install the libtool system package on the opam bench server for coqprime-generator to install properly.

view this post on Zulip Guillaume Claret (Dec 12 2021 at 14:51):

OK, thanks for the notice, I added this package!

view this post on Zulip Coq opam bench (Dec 15 2021 at 14:23):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Dec 18 2021 at 14:28):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Dec 21 2021 at 14:32):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Dec 24 2021 at 14:37):

Summary of the past 72 hours:

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

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

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Dec 30 2021 at 14:47):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jan 02 2022 at 14:52):

Summary of the past 72 hours:

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

view this post on Zulip Guillaume Claret (Jan 04 2022 at 13:32):

OK, I do not really know why the uninstallation did not work, maybe an error in the bench system itself.

view this post on Zulip Karl Palmskog (Jan 04 2022 at 13:33):

yeah no idea from the log, could it be something like no space on drive?

view this post on Zulip Karl Palmskog (Jan 04 2022 at 13:33):

I guess we will see if it goes away.

view this post on Zulip Guillaume Claret (Jan 04 2022 at 13:34):

The disk is fine

view this post on Zulip Guillaume Melquiond (Jan 04 2022 at 15:03):

That said, there is something wrong going on. The list of installed files does not match at all what should have been installed in the first place, as far as I can tell. So, I am not surprised the uninstallation step complains.

view this post on Zulip Coq opam bench (Jan 05 2022 at 14:57):

Summary of the past 72 hours:

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

view this post on Zulip Karl Palmskog (Jan 05 2022 at 15:00):

ping @Reynald Affeldt it looks here like infotheo 0.3.4 is not compatible with the recently-released analysis 0.3.12.

view this post on Zulip Karl Palmskog (Jan 05 2022 at 15:02):

I guess Guillaume or I will fix it eventually, but just flagging it up in the meantime.

view this post on Zulip Reynald Affeldt (Jan 06 2022 at 01:01):

Thanks for the ping. I pushed a fix.

view this post on Zulip Coq opam bench (Jan 08 2022 at 15:02):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jan 11 2022 at 15:07):

Summary of the past 72 hours:

9787 attempted package installations (including incompatible packages), 5 errors, 0.05% errors

view this post on Zulip Coq opam bench (Jan 14 2022 at 15:12):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jan 17 2022 at 15:17):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Jan 17 2022 at 15:17):

view this post on Zulip Coq opam bench (Jan 17 2022 at 15:17):

21581 attempted package installations (including incompatible packages), 29 errors, 0.13% errors

view this post on Zulip Coq opam bench (Jan 20 2022 at 15:22):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Jan 20 2022 at 15:22):

15734 attempted package installations (including incompatible packages), 19 errors, 0.12% errors

view this post on Zulip Coq opam bench (Jan 23 2022 at 15:27):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Jan 23 2022 at 15:27):

19732 attempted package installations (including incompatible packages), 11 errors, 0.06% errors

view this post on Zulip Karl Palmskog (Jan 23 2022 at 15:58):

ping @Guillaume Claret it looks like coq-bonsai.1.0.0 and coq-chick-blog.1.0.1 don't work on 8.15, can you adjust the packages?

view this post on Zulip Karl Palmskog (Jan 23 2022 at 15:58):

(all others should be fixed very soon)

view this post on Zulip Guillaume Claret (Jan 23 2022 at 20:42):

OK indeed, thanks for the ping, fixing it

view this post on Zulip Coq opam bench (Jan 26 2022 at 15:32):

Summary of the past 72 hours:

5951 attempted package installations (including incompatible packages), 1 error, 0.02% errors

view this post on Zulip Guillaume Claret (Jan 26 2022 at 16:18):

OK, it seems you already solved this CFML error @Karl Palmskog so we are all good

view this post on Zulip Coq opam bench (Jan 29 2022 at 15:37):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Feb 01 2022 at 15:43):

Summary of the past 72 hours:

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

view this post on Zulip Karl Palmskog (Feb 01 2022 at 17:40):

ping @Guillaume Claret the io-system package doesn't work on 8.15 and later.

view this post on Zulip Karl Palmskog (Feb 01 2022 at 17:40):

(I took care of itauto)

view this post on Zulip Karl Palmskog (Feb 02 2022 at 10:41):

hmm, I think there might be some weird custom remove clause in an old package related to CFML that is causing uninstallation issues. I'll take a look at it at some point...

view this post on Zulip Coq opam bench (Feb 04 2022 at 15:48):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Feb 07 2022 at 15:53):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Feb 10 2022 at 15:58):

Summary of the past 72 hours:

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

view this post on Zulip Karl Palmskog (Feb 10 2022 at 16:05):

ping @Pierre Roux looks like coq-validsdp.1.0.0 fails on Coq 8.12.2 due to some dependency problem: https://coq-bench.github.io/clean/Linux-x86_64-4.10.2-2.0.6/released/8.12.2/validsdp/1.0.0.html

Could you take a look? Not trivial to figure out the exact problem without domain knowledge.

view this post on Zulip Guillaume Melquiond (Feb 10 2022 at 17:03):

It seems like the archive for ValidSDP is corrupted. It contains outdated configure scripts.

view this post on Zulip Pierre Roux (Feb 10 2022 at 17:14):

Thanks for pinging me, looks like I forgot to rerun autoconf before distributing the archive. I just updated it and it should work now.

view this post on Zulip Karl Palmskog (Feb 10 2022 at 17:18):

but then I think the checksum will have changed, right? I think we need to update the package

view this post on Zulip Karl Palmskog (Feb 10 2022 at 17:19):

@Pierre Roux should I do it?

view this post on Zulip Coq opam bench (Feb 13 2022 at 16:03):

Summary of the past 72 hours:

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

view this post on Zulip Guillaume Claret (Feb 15 2022 at 12:40):

The issue with Unimath is that it is taking too much time to install (more than 4h). I do not know if this is good for a package to take too long to compile, I am opening an issue on their repository.

view this post on Zulip Guillaume Claret (Feb 15 2022 at 12:44):

https://github.com/UniMath/UniMath/issues/1459

view this post on Zulip Coq opam bench (Feb 16 2022 at 16:09):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Feb 19 2022 at 16:14):

Summary of the past 72 hours:

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

view this post on Zulip Karl Palmskog (Feb 19 2022 at 18:15):

@Guillaume Claret maybe you could add unimath.20220204 to the blacklist? It's pretty clear it takes way too long to test.

view this post on Zulip Guillaume Claret (Feb 20 2022 at 16:00):

OK done (I increased the timeout for it)

view this post on Zulip Coq opam bench (Feb 22 2022 at 16:19):

Summary of the past 72 hours:

6064 attempted package installations (including incompatible packages), 2 errors, 0.03% errors

view this post on Zulip Coq opam bench (Feb 25 2022 at 16:24):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Feb 28 2022 at 16:29):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Mar 03 2022 at 16:35):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Mar 06 2022 at 16:40):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Mar 09 2022 at 16:46):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Mar 12 2022 at 16:51):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Mar 12 2022 at 16:51):

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

view this post on Zulip Coq opam bench (Mar 15 2022 at 16:56):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Mar 18 2022 at 17:01):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Mar 21 2022 at 17:07):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Mar 24 2022 at 17:12):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Mar 27 2022 at 17:18):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Mar 30 2022 at 17:23):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Apr 02 2022 at 17:29):

Summary of the past 72 hours:

10214 attempted package installations (including incompatible packages), 5 errors, 0.05% errors

view this post on Zulip Coq opam bench (Apr 05 2022 at 17:35):

Summary of the past 72 hours:

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

view this post on Zulip Guillaume Claret (Apr 05 2022 at 22:19):

I added OCaml 4.14 to the test suite

view this post on Zulip Coq opam bench (Apr 08 2022 at 17:40):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Apr 11 2022 at 17:46):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Apr 14 2022 at 17:51):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Apr 17 2022 at 17:57):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Apr 20 2022 at 18:02):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Apr 23 2022 at 18:08):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Apr 26 2022 at 18:14):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Apr 29 2022 at 18:20):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (May 02 2022 at 18:26):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (May 05 2022 at 18:32):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (May 08 2022 at 18:38):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (May 11 2022 at 18:45):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (May 14 2022 at 18:51):

Summary of the past 72 hours:

14490 attempted package installations (including incompatible packages), 8 errors, 0.06% errors

view this post on Zulip Coq opam bench (May 17 2022 at 18:57):

Summary of the past 72 hours:

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

view this post on Zulip Karl Palmskog (May 20 2022 at 18:30):

I see the following which should probably be fixed:

W: multiple date tag in released/packages/coq-lc/coq-lc.8.10.0/opam
W: multiple date tag in released/packages/coq-lc/coq-lc.8.9.0/opam
W: multiple date tag in released/packages/coq-lc/coq-lc.8.8.0/opam
W: multiple date tag in released/packages/coq-lc/coq-lc.8.7.0/opam
W: multiple date tag in released/packages/coq-lc/coq-lc.8.6.0/opam

view this post on Zulip Coq opam bench (May 20 2022 at 19:03):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (May 23 2022 at 19:10):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (May 26 2022 at 19:16):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (May 29 2022 at 19:22):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jun 01 2022 at 19:28):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jun 04 2022 at 19:34):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Jun 04 2022 at 19:34):

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

view this post on Zulip Jason Gross (Jun 05 2022 at 16:27):

fiat-crypto is failing with

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of conf-jq failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build jq --version".
-> installed coq-bignums.8.15.0
-> installed coq-coqutil.0.0.1
-> installed coq-coqprime.1.2.0
-> installed coq-bedrock2.0.0.1
-> installed coq-rupicola.0.0.4
-> installed coq-rewriter.0.0.2
#=== ERROR while compiling conf-jq.1 ==========================================#
# context              2.0.10 | linux/x86_64 | ocaml-base-compiler.4.14.0 | https://opam.ocaml.org#40f3586d
# path                 ~/.opam/ocaml-base-compiler.4.14.0/.opam-switch/build/conf-jq.1
# command              ~/.opam/opam-init/hooks/sandbox.sh build jq --version
# exit-code            1
# env-file             ~/.opam/log/conf-jq-28250-ab22a1.env
# output-file          ~/.opam/log/conf-jq-28250-ab22a1.out
### output ###
# bwrap: execvp jq: No such file or directory

Can jq be installed on the runner machines?

view this post on Zulip Guillaume Claret (Jun 06 2022 at 15:28):

Yes, I am adding it!

view this post on Zulip Guillaume Claret (Jun 06 2022 at 21:23):

(done)

view this post on Zulip Coq opam bench (Jun 07 2022 at 19:40):

Summary of the past 72 hours:

10421 attempted package installations (including incompatible packages), 8 errors, 0.08% errors

view this post on Zulip Coq opam bench (Jun 10 2022 at 19:46):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jun 13 2022 at 19:51):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jun 16 2022 at 19:57):

Summary of the past 72 hours:

10439 attempted package installations (including incompatible packages), 4 errors, 0.04% errors

view this post on Zulip Coq opam bench (Jun 19 2022 at 20:03):

Summary of the past 72 hours:

8352 attempted package installations (including incompatible packages), 6 errors, 0.07% errors

view this post on Zulip Coq opam bench (Jun 22 2022 at 20:08):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jun 25 2022 at 20:14):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jun 28 2022 at 20:19):

Summary of the past 72 hours:

6267 attempted package installations (including incompatible packages), 6 errors, 0.10% errors

view this post on Zulip Coq opam bench (Jul 01 2022 at 20:25):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jul 04 2022 at 20:31):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jul 07 2022 at 20:37):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jul 10 2022 at 20:42):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jul 13 2022 at 20:48):

Summary of the past 72 hours:

6326 attempted package installations (including incompatible packages), 1 error, 0.02% errors

view this post on Zulip Coq opam bench (Jul 16 2022 at 20:53):

Summary of the past 72 hours:

10584 attempted package installations (including incompatible packages), 4 errors, 0.04% errors

view this post on Zulip Coq opam bench (Jul 19 2022 at 20:59):

Summary of the past 72 hours:

8480 attempted package installations (including incompatible packages), 7 errors, 0.08% errors

view this post on Zulip Coq opam bench (Jul 22 2022 at 21:04):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Jul 22 2022 at 21:04):

8483 attempted package installations (including incompatible packages), 18 errors, 0.21% errors

view this post on Zulip Coq opam bench (Jul 25 2022 at 21:09):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Jul 28 2022 at 21:15):

Summary of the past 72 hours:

6370 attempted package installations (including incompatible packages), 6 errors, 0.09% errors

view this post on Zulip Coq opam bench (Jul 31 2022 at 21:20):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Aug 03 2022 at 21:25):

Summary of the past 72 hours:

4254 attempted package installations (including incompatible packages), 1 error, 0.02% errors

view this post on Zulip Coq opam bench (Aug 06 2022 at 21:31):

Summary of the past 72 hours:

4254 attempted package installations (including incompatible packages), 1 error, 0.02% errors

view this post on Zulip Coq opam bench (Aug 09 2022 at 21:36):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Aug 12 2022 at 21:41):

Summary of the past 72 hours:

6384 attempted package installations (including incompatible packages), 1 error, 0.02% errors

view this post on Zulip Coq opam bench (Aug 15 2022 at 21:47):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Aug 18 2022 at 21:52):

Summary of the past 72 hours:

4262 attempted package installations (including incompatible packages), 2 errors, 0.05% errors

view this post on Zulip Coq opam bench (Aug 21 2022 at 21:58):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Aug 24 2022 at 22:03):

Summary of the past 72 hours:

6402 attempted package installations (including incompatible packages), 1 error, 0.02% errors

view this post on Zulip Coq opam bench (Aug 27 2022 at 22:09):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Aug 30 2022 at 22:14):

Summary of the past 72 hours:

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

view this post on Zulip Coq opam bench (Sep 02 2022 at 22:20):

Summary of the past 72 hours:

2143 attempted package installations (including incompatible packages), 4 errors, 0.19% errors

view this post on Zulip Coq opam bench (Sep 05 2022 at 22:25):

Summary of the past 72 hours:

6430 attempted package installations (including incompatible packages), 2 errors, 0.03% errors

view this post on Zulip Coq opam bench (Sep 08 2022 at 22:32):

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 (Sep 11 2022 at 22:38):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Sep 11 2022 at 22:38):

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

view this post on Zulip Coq opam bench (Sep 14 2022 at 22:45):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Sep 14 2022 at 22:45):

view this post on Zulip Coq opam bench (Sep 14 2022 at 22:45):

10748 attempted package installations (including incompatible packages), 26 errors, 0.24% errors

view this post on Zulip Coq opam bench (Sep 17 2022 at 22:50):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Sep 17 2022 at 22:50):

view this post on Zulip Coq opam bench (Sep 17 2022 at 22:50):

view this post on Zulip Coq opam bench (Sep 17 2022 at 22:50):

view this post on Zulip Coq opam bench (Sep 17 2022 at 22:50):

view this post on Zulip Coq opam bench (Sep 17 2022 at 22:50):

view this post on Zulip Coq opam bench (Sep 17 2022 at 22:50):

view this post on Zulip Coq opam bench (Sep 17 2022 at 22:50):

view this post on Zulip Coq opam bench (Sep 17 2022 at 22:50):

view this post on Zulip Coq opam bench (Sep 17 2022 at 22:50):

17336 attempted package installations (including incompatible packages), 103 errors, 0.59% errors

view this post on Zulip Coq opam bench (Sep 20 2022 at 22:56):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Sep 20 2022 at 22:56):

view this post on Zulip Coq opam bench (Sep 20 2022 at 22:56):

view this post on Zulip Coq opam bench (Sep 20 2022 at 22:56):

view this post on Zulip Coq opam bench (Sep 20 2022 at 22:56):

view this post on Zulip Coq opam bench (Sep 20 2022 at 22:56):

view this post on Zulip Coq opam bench (Sep 20 2022 at 22:56):

view this post on Zulip Coq opam bench (Sep 20 2022 at 22:56):

15244 attempted package installations (including incompatible packages), 79 errors, 0.52% errors

view this post on Zulip Coq opam bench (Sep 23 2022 at 23:02):

Summary of the past 72 hours:

view this post on Zulip Coq opam bench (Sep 23 2022 at 23:02):

view this post on Zulip Coq opam bench (Sep 23 2022 at 23:02):

view this post on Zulip Coq opam bench (Sep 23 2022 at 23:02):