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.
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).
not sure if this falls into current scope, but it would be great with OPAM bench system integration with the Zulip chat
Yes, that is what I just proposed to do in the issue.
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.
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
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.
more generally, there are many avenues for integration with the Coq bot
also, I think it would be nice with a dashboard summarizing "Coq package health" on different versions of Coq and OCaml
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)
@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
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
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
.
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.
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.
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.
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
Summary of the past 3 hours:
0 package installations, 0 errors, 0.00% errors :check:
OK, so the mechanism to send messages seems to work, we will see by 72 hours if we have the next report
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.
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
For now everything is on GitHub, but the machine is privately owned so that is probably the main blocker to open the development
@Guillaume Claret Please edit the wiki page to add your topic to the list.
OK, done!
Summary of the past 72 hours:
0 package installations, 0 errors, 0.00% errors :check:
OK, so the bench did fail (0 tests), I restarted the server
(and fixed the bug)
Summary of the past 72 hours:
- switch.1.0.1:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies)
- Coq 8.5.3, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
3190 package installations, 2 errors, 0.06% errors
remnants of previous errors (fixed by the author)
Summary of the past 72 hours:
- geocoq-pof.2.4.0:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- Coq 8.9.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- metacoq-translations.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)
- metacoq.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- switch.1.0.1:
* 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
OK, one of the error is - /bin/sh: 1: time: not found
I will update the Docker images so that this utility is there
I hope that the timeout errors (for Geocoq) do not persist
Summary of the past 72 hours:
- intuitionistic-nuprl.8.6.0:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (error)
9685 package installations, 1 error, 0.01% errors
OK, so this is a very long timeout for coq-intuitionistic-nuprl
(10 hours), but it should terminate
@Guillaume Claret I would suggest blacklisting that project. This is an ancient release, unfortunately the maintainer has not done releases in many years now
I have a feeling that the bench is now slower, this may be due to us testing more OCaml versions
OK I will blacklist
(actually when it succeeds it does not install anything, as there is a bug in the make install
)
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.
:ok:
I've pinged Vincent in the issue.
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
Summary of the past 72 hours:
- ceres.0.3.0:
- Coq 8.8.0, OCaml 4.09.1 :cross_mark: (error)
- intuitionistic-nuprl.8.6.0:
- Coq 8.6, OCaml 4.02.3 :cross_mark: (error)
- metacoq-translations.1.0~beta1+8.11:
- Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error)
- metacoq-translations.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)
- metacoq.1.0~beta1+8.11:
- Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- switch.1.0.2:
- Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error)
- Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)
17787 package installations, 8 errors, 0.04% errors
@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.
:ok:
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.10.1, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- metacoq-translations.1.0~beta1+8.11:
- Coq 8.11.1, OCaml 4.10.1 :cross_mark: (error)
- Coq 8.11.2, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.11.2, OCaml 4.11.1 :cross_mark: (error)
- metacoq.1.0~beta1+8.11:
- Coq 8.11.1, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- Coq 8.11.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- Coq 8.11.2, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- switch.1.0.2:
- Coq 8.11.1, OCaml 4.10.1 :cross_mark: (error)
- Coq 8.11.2, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.11.2, OCaml 4.11.1 :cross_mark: (error)
24255 package installations, 10 errors, 0.04% errors
Summary of the past 72 hours:
- metacoq-translations.1.0~beta1+8.11:
- Coq 8.11.1, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.11.1, OCaml 4.11.1 :cross_mark: (error)
- Coq 8.11.2, OCaml 4.08.1 :cross_mark: (error)
- metacoq-translations.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta1+8.11:
- Coq 8.11.1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies)
- Coq 8.11.1, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- Coq 8.11.2, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- switch.1.0.2:
- Coq 8.11.1, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.11.1, OCaml 4.11.1 :cross_mark: (error)
- Coq 8.11.2, OCaml 4.08.1 :cross_mark: (error)
- Coq 8.12.0, OCaml 4.10.1 :cross_mark: (error)
19417 package installations, 12 errors, 0.06% errors
Summary of the past 72 hours:
- ceres.0.3.0:
- Coq 8.8.0, OCaml 4.05.0 :cross_mark: (error)
- Coq 8.8.0, OCaml 4.07.1 :cross_mark: (error)
- metacoq-translations.1.0~beta1+8.11:
- Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta1+8.11:
- Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- switch.1.0.2:
- Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error)
14592 package installations, 5 errors, 0.03% errors
Summary of the past 72 hours:
- intuitionistic-nuprl.8.6.0:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (error)
- metacoq-translations.1.0~beta1+8.11:
- 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.11.2, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- metacoq-translations.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta1+8.11:
- 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.11.2, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- switch.1.0.2:
- Coq 8.11.1, OCaml 4.10.1 :cross_mark: (error)
16238 package installations, 10 errors, 0.06% errors
Summary of the past 72 hours:
- ceres.0.3.0:
- Coq 8.8.0, OCaml 4.08.1 :cross_mark: (error)
- chick-blog.1.0.0:
- Coq 8.9.0, OCaml 4.03.0 :large_orange_diamond: (error with dependencies)
- metacoq-translations.1.0~beta1+8.11:
- Coq 8.11.1, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- metacoq-translations.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta1+8.11:
- Coq 8.11.1, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
16266 package installations, 6 errors, 0.04% errors
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.
@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
OK, I thought I did that (installing time), I will check the servers
Indeed, the server did not restart as I expected for the time
package; should be fixed for the next iteration
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.9.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- metacoq-translations.1.0~beta1+8.11:
- Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta1+8.11:
- Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
6521 package installations, 3 errors, 0.05% errors
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.9.0, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- metacoq-translations.1.0~beta1+8.11:
- Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error)
- metacoq.1.0~beta1+8.11:
- Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
16351 package installations, 3 errors, 0.02% errors
I added Python3 for metacoq-translations.1.0~beta1+8.11
Summary of the past 72 hours:
- metacoq-translations.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.10.1 :cross_mark: (error)
- metacoq.1.0~beta1+8.12:
- Coq 8.12.0, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
1637 attempted package installations (including incompatible packages), 2 errors, 0.12% errors
Summary of the past 72 hours:
0 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
0 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
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")
Indeed, I have seen that and forgot to act on it
thanks for the reminder
I restarted the servers
Summary of the past 72 hours:
- chick-blog.1.0.1:
- Coq 8.6.1, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
3280 attempted package installations (including incompatible packages), 1 error, 0.03% errors
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.5.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.9.0, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- chick-blog.1.0.1:
- Coq 8.11.1, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- Coq 8.5.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.7.1+1, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- Coq 8.7.1+2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.9.0, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
18040 attempted package installations (including incompatible packages), 7 errors, 0.04% errors
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.5.0, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.6.1, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.7.0, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- Coq 8.7.1+1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- Coq 8.8.1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies)
- chick-blog.1.0.1:
- Coq 8.10.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- Coq 8.11.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- Coq 8.11.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- Coq 8.11.2, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- Coq 8.5.0, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.6.1, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.7.0, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- Coq 8.7.1+1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- Coq 8.8.1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies)
- qcert.2.1.0:
- Coq 8.11.2, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
18040 attempted package installations (including incompatible packages), 15 errors, 0.08% errors
Summary of the past 72 hours:
- algorand.1.2:
- Coq 8.11.1, OCaml 4.11.1 :cross_mark: (error)
- Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error)
- chick-blog.1.0.0:
- Coq 8.5.3, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- Coq 8.6.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- 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)
- chick-blog.1.0.1:
- Coq 8.10.0, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- Coq 8.10.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- Coq 8.10.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- Coq 8.10.2, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- 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)
- Coq 8.12.0, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- Coq 8.5.3, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- Coq 8.6.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
* 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)
- qcert.2.1.0:
- Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- Coq 8.12.0, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
21324 attempted package installations (including incompatible packages), 31 errors, 0.15% errors
@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?
I think everything else just above except chick-blog will be fixed by recent PRs
OK, indeed, I restarted the servers adding this package to the dependencies!
Summary of the past 72 hours:
- algorand.1.2:
- Coq 8.11.1, OCaml 4.11.1 :cross_mark: (error)
- Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error)
- chick-blog.1.0.0:
- Coq 8.7.1+1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies)
- Coq 8.8.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.8.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- chick-blog.1.0.1:
- Coq 8.10.0, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- Coq 8.10.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- 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)
- Coq 8.7.1+1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies)
- Coq 8.8.1, OCaml 4.04.2 :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)
- qcert.2.1.0:
- Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
14766 attempted package installations (including incompatible packages), 25 errors, 0.17% errors
Summary of the past 72 hours:
0 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.5.1, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.9.0, OCaml 4.03.0 :large_orange_diamond: (error with dependencies)
- Coq 8.9.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- chick-blog.1.0.1:
- Coq 8.5.1, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.6, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- coq-in-coq.8.10.0:
- Coq 8.10.1, OCaml 4.06.1 :cross_mark: (error)
- intuitionistic-nuprl.8.6.0:
- Coq 8.6, OCaml 4.02.3 :cross_mark: (error)
- metacoq-pcuic.1.0~alpha1+8.9:
- Coq 8.9.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
18053 attempted package installations (including incompatible packages), 8 errors, 0.04% errors
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.11.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- chick-blog.1.0.1:
- Coq 8.11.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.6, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.9.1, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
16439 attempted package installations (including incompatible packages), 4 errors, 0.02% errors
@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.
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
Indeed, there are still bugs from time to time
I added this one to the blacklist https://github.com/coq-bench/make-html/blob/master/black_list.rb#L15
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
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.6.1, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- chick-blog.1.0.1:
- Coq 8.6.1, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
14804 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.7.0, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- Coq 8.9.0, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- chick-blog.1.0.1:
- Coq 8.7.0, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- Coq 8.9.0, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
14824 attempted package installations (including incompatible packages), 4 errors, 0.03% errors
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.5.0, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.5.3, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.6, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.8.2, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- chick-blog.1.0.1:
- Coq 8.5.0, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.5.3, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.6, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.8.2, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- compcert.3.0.1:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (error)
19863 attempted package installations (including incompatible packages), 9 errors, 0.05% errors
For CompCert, error due to the instability of old OCaml compilers (again), I added this error for this package to the black-list
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.12.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.5.0~camlp4, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- Coq 8.5.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.8.0, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- chick-blog.1.0.1:
- Coq 8.5.0~camlp4, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- Coq 8.5.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.8.0, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- hierarchy-builder.0.9.1:
- Coq 8.5.0~camlp4, OCaml 4.02.3 :large_orange_diamond: (error with dependencies)
- tactician-dummy.1.0~beta1:
- Coq 8.5.0~camlp4, OCaml 4.02.3 :cross_mark: (error)
16586 attempted package installations (including incompatible packages), 9 errors, 0.05% errors
tactician-dummy
is a new package, I will wait for more errors before to fix it
other errors are due to timeout in dependency resolution
Summary of the past 72 hours:
- finger-tree.8.8.0:
- Coq 8.8.2, OCaml 4.05.0 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.4.6~camlp4, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.5.0, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.5.3, OCaml 4.03.0 :cross_mark: (error)
18334 attempted package installations (including incompatible packages), 4 errors, 0.02% errors
Summary of the past 72 hours:
- chick-blog.1.0.1:
- Coq 8.7.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- tactician-dummy.1.0~beta1:
- Coq 8.5.2~camlp4, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.6, OCaml 4.03.0 :cross_mark: (error)
16686 attempted package installations (including incompatible packages), 3 errors, 0.02% errors
Waiting for more errors to fix tactician-dummy
Summary of the past 72 hours:
18378 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- metacoq.1.0~alpha1+8.9:
- Coq 8.9.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- tactician-dummy.1.0~beta1:
- Coq 8.5.0, OCaml 4.03.0 :cross_mark: (error)
- Coq 8.5.2, OCaml 4.02.3 :cross_mark: (error)
21760 attempted package installations (including incompatible packages), 3 errors, 0.01% errors
Summary of the past 72 hours:
- tactician-dummy.1.0~beta1:
- Coq 8.5.0~camlp4, OCaml 4.03.0 :cross_mark: (error)
10078 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- tactician-dummy.1.0~beta1:
- Coq 8.5.2, OCaml 4.04.2 :cross_mark: (error)
15135 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
18513 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
18513 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
18536 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- founify.8.5.0:
- Coq 8.5.0~camlp4, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- Coq 8.5.2~camlp4, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
16884 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
- coq-in-coq.8.10.0:
- Coq 8.10.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- founify.8.10.0:
- Coq 8.10.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- founify.8.5.0:
- Coq 8.5.2~camlp4, OCaml 4.04.2 :large_orange_diamond: (error with dependencies)
- graphs.8.10.0:
- Coq 8.10.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- pts.8.10.0:
- Coq 8.10.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
13532 attempted package installations (including incompatible packages), 5 errors, 0.04% errors
It seems like camlp5 now requires Perl, I will add it to the bench Dockerfile
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.)
not only does it require Perl itself, but also some non-standard Perl modules
seemingly, our whole ecosystem is suddenly dependent on Perl version 5 (Coq is via zarith), a dying and nearly unmaintained language
Given that camlp5 is hardly used anymore, it is even weirder to think that a fresh 8.0 branch was released.
Does anybody know the motivation behind it?
nope, all I know is that Chet Murthy seems to have taken over maintenance from Daniel recently
Maintenance is a fairly different thing from major release though
What Coq developments are relying on camlp5?
it looked like Chet spearheaded the new release
one of the reason for the integration of the gramlib library into Coq was precisely to sever the dependency to camlp5
now we seemingly reap the rewards of that decision
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
it could be that the camlp5 changes are behind the opam dependency resolution taking 2+ mins for coq-elpi on 4.05
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)
Gappa uses camlp5???
Lord have mercy...
Coq 8.9 is still used heavily and uses camlp5
Unfortunately, indeed.
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
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
Somewhat ironic but much more reasonable, I believe.
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
Elpi still depends on camlp5
Hey, I got an ATD approved, and one of the tasks was to rewrite the parser. But covid stopped everything.
Summary of the past 72 hours:
- founify.8.5.0:
- Coq 8.5.0~camlp4, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- gappa.1.4.2+8.11:
- Coq 8.11.0, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
15239 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
- functional-algebra.1.0.2:
- Coq 8.13.0, OCaml 4.05.0 :cross_mark: (error)
- hoare-tut.8.11.1:
- Coq 8.13.0, OCaml 4.05.0 :cross_mark: (error)
- tlc.20200328:
- Coq 8.13.0, OCaml 4.05.0 :cross_mark: (error)
10218 attempted package installations (including incompatible packages), 3 errors, 0.03% errors
Summary of the past 72 hours:
15346 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- tactician-dummy.1.0~beta1:
- Coq 8.7.1, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.7.1, OCaml 4.03.0 :cross_mark: (error)
- Coq 8.7.2, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.9.1, OCaml 4.07.1 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.9.1, OCaml 4.07.1 :cross_mark: (error)
17100 attempted package installations (including incompatible packages), 5 errors, 0.03% errors
See https://github.com/ocaml/dune/issues/4142 for the cause of the failures above.
The problem is specific to dune and old coq versions, cc @Emilio Jesús Gallego Arias
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
Dune itself should inspect the Coq version to figure out which coqc
options are available.
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"}) ]
(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.)
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.
(I don't get the commit contents either, but that is another story)
Isn't any version of Dune compatible with Coq 8.13? (wth) If not, then sure, a constraint should be put on Dune.
This was my recollection as well, no compat problems. But the commit must have had a motive
I guess we can wait for @Emilio Jesús Gallego Arias to shed some light on this issue
@Enrico Tassi This commit is part of a bigger PR that adds support for native-compilation.
Previous versions of Dune do not have this PR at all and should be fully compatible with Coq 8.13.
Right, but this does not explain why it is needed
It seems a sort of defensive setup (from the commit message)
But apparently breaks coq < 8.13
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)
Summary of the past 72 hours:
- functional-algebra.1.0.2:
- Coq 8.13.0, OCaml 4.10.1 :cross_mark: (error)
- hoare-tut.8.11.1:
- Coq 8.13.0, OCaml 4.10.1 :cross_mark: (error)
- qcert.2.1.0:
- Coq 8.13.0, OCaml 4.10.1 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.7.1+2, OCaml 4.08.1 :cross_mark: (error)
- Coq 8.8.0, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.09.1 :cross_mark: (error)
- tlc.20200328:
- Coq 8.13.0, OCaml 4.10.1 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.8.0, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.09.1 :cross_mark: (error)
17106 attempted package installations (including incompatible packages), 9 errors, 0.05% errors
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
The reason we are explicit on the options is to still provide a fast compilation in dev profile.
Summary of the past 72 hours:
- functional-algebra.1.0.2:
- Coq 8.13.0, OCaml 4.11.1 :cross_mark: (error)
- hoare-tut.8.11.1:
- Coq 8.13.0, OCaml 4.11.1 :cross_mark: (error)
- qcert.2.1.0:
- Coq 8.13.0, OCaml 4.11.1 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.7.0, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.7.1+1, OCaml 4.08.1 :cross_mark: (error)
- Coq 8.7.1+2, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.7.1+2, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.8.1, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.03.0 :cross_mark: (error)
- tlc.20200328:
- Coq 8.13.0, OCaml 4.11.1 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.8.1, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.03.0 :cross_mark: (error)
18832 attempted package installations (including incompatible packages), 12 errors, 0.06% errors
@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?
(the packages failing with Coq 8.13 are now fixed)
Yes @Guillaume Claret , these packages should get working again.
Top, thanks!
Summary of the past 72 hours:
- tactician-dummy.1.0~beta1:
- Coq 8.7.1, OCaml 4.08.1 :cross_mark: (error)
- Coq 8.8.1, OCaml 4.03.0 :cross_mark: (error)
- Coq 8.8.1, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.9.1, OCaml 4.04.2 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.8.1, OCaml 4.03.0 :cross_mark: (error)
- Coq 8.8.1, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.9.1, OCaml 4.04.2 :cross_mark: (error)
13696 attempted package installations (including incompatible packages), 9 errors, 0.07% errors
Summary of the past 72 hours:
- metacoq-erasure.1.0~beta2+8.11:
- Coq 8.11.1, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- metacoq-erasure.1.0~beta2+8.12:
- Coq 8.12.1, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- metacoq-safechecker.1.0~beta2+8.11:
- Coq 8.11.1, OCaml 4.11.1 :cross_mark: (error)
- metacoq-safechecker.1.0~beta2+8.12:
- Coq 8.12.1, OCaml 4.10.1 :cross_mark: (error)
- metacoq.1.0~beta2+8.11:
- Coq 8.11.1, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta2+8.12:
- Coq 8.12.1, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- switch.1.0.4:
- Coq 8.12.1, OCaml 4.10.1 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.7.0, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.7.1+2, OCaml 4.03.0 :cross_mark: (error)
- 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) * 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
I reported the metacoq issue there: https://github.com/MetaCoq/metacoq/issues/541
fixing coq-switch, for tactician-dummy and type-infer I am waiting for the dune update
Summary of the past 72 hours:
- metacoq-erasure.1.0~beta2+8.12:
- Coq 8.12.0, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- Coq 8.12.0, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- metacoq-safechecker.1.0~beta2+8.12:
- Coq 8.12.0, OCaml 4.10.1 :cross_mark: (error)
- Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)
- metacoq.1.0~beta2+8.12:
- Coq 8.12.0, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- Coq 8.12.0, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- switch.1.0.4:
- Coq 8.12.0, OCaml 4.10.1 :cross_mark: (error)
- Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.09.1 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.7.0, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.02.3 :cross_mark: (error)
- type-infer.0.1.0:
* 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
Summary of the past 72 hours:
- metacoq-erasure.1.0~beta2+8.11:
- Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- metacoq-erasure.1.0~beta2+8.12:
- Coq 8.12.1, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- metacoq-safechecker.1.0~beta2+8.11:
- Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error)
- metacoq-safechecker.1.0~beta2+8.12:
- Coq 8.12.1, OCaml 4.11.1 :cross_mark: (error)
- metacoq.1.0~beta2+8.11:
- Coq 8.11.2, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta2+8.12:
- Coq 8.12.1, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- switch.1.0.4:
- Coq 8.12.1, OCaml 4.11.1 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.7.1+1, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.7.1, OCaml 4.06.1 :cross_mark: (error)
- 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) * 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
Summary of the past 72 hours:
- metacoq-erasure.1.0~beta2+8.11:
- Coq 8.11.2, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- metacoq-erasure.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- metacoq-safechecker.1.0~beta2+8.11:
- Coq 8.11.2, OCaml 4.11.1 :cross_mark: (error)
- metacoq-safechecker.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.10.1 :cross_mark: (error)
- metacoq.1.0~beta2+8.11:
- Coq 8.11.2, OCaml 4.11.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- tactician-dummy.1.0~beta1:
- Coq 8.7.0, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.7.2, OCaml 4.03.0 :cross_mark: (error)
- Coq 8.7.2, OCaml 4.07.1 :cross_mark: (error)
- 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) * 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
Summary of the past 72 hours:
- metacoq-erasure.1.0~beta2+8.11:
- Coq 8.11.1, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- metacoq-safechecker.1.0~beta2+8.11:
- Coq 8.11.1, OCaml 4.10.1 :cross_mark: (error)
- metacoq.1.0~beta2+8.11:
- Coq 8.11.1, OCaml 4.10.1 :large_orange_diamond: (error with dependencies)
- tactician-dummy.1.0~beta1:
- Coq 8.7.1+1, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.8.0, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.05.0 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.8.0, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.05.0 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.11.1, OCaml 4.10.1 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.11.1 :cross_mark: (error)
- vst.2.7:
* Coq 8.11.1, OCaml 4.10.1 :cross_mark: (error)
20870 attempted package installations (including incompatible packages), 12 errors, 0.06% errors
Summary of the past 72 hours:
- tactician-dummy.1.0~beta1:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (error)
- Coq 8.7.0, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.7.1+2, OCaml 4.05.0 :cross_mark: (error)
- Coq 8.7.1, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.7.2, OCaml 4.09.1 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.12.1, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.08.1 :cross_mark: (error)
17416 attempted package installations (including incompatible packages), 8 errors, 0.05% errors
Summary of the past 72 hours:
- intuitionistic-nuprl.8.6.0:
- Coq 8.6, OCaml 4.02.3 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.7.1+1, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.7.1, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.08.1 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.9.0, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.08.1 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.12.1, OCaml 4.10.1 :cross_mark: (error)
15687 attempted package installations (including incompatible packages), 8 errors, 0.05% errors
Summary of the past 72 hours:
- intuitionistic-nuprl.8.6.0:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.7.1+1, OCaml 4.03.0 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.06.1 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.8.2, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.06.1 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.12.0, OCaml 4.10.1 :cross_mark: (error)
- Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)
17460 attempted package installations (including incompatible packages), 10 errors, 0.06% errors
Summary of the past 72 hours:
- intuitionistic-nuprl.8.6.0:
- Coq 8.6, OCaml 4.04.2 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.7.2, OCaml 4.05.0 :cross_mark: (error)
- Coq 8.8.1, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.9.1, OCaml 4.03.0 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.8.1, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.9.1, OCaml 4.03.0 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.11.1 :cross_mark: (error)
15726 attempted package installations (including incompatible packages), 10 errors, 0.06% errors
Summary of the past 72 hours:
- corn.8.12.0:
- Coq 8.7.2, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- tactician-dummy.1.0~beta1:
- Coq 8.7.1+2, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.7.2, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.7.2, OCaml 4.08.1 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.03.0 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.8.2, OCaml 4.03.0 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.12.0, OCaml 4.07.1 :cross_mark: (error)
13997 attempted package installations (including incompatible packages), 7 errors, 0.05% errors
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
The error with bignums
(used by corn
) seems to be a race condition.
OK thanks
(so probably not worth to be fixed unless it appears again)
It is actually easy to reproduce if your ocaml
interpreter is slow.
OK
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.
: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
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.
The patch for dune has been merged, but not yet in a release , hopefully it happens soon.
Summary of the past 72 hours:
- monae.0.3:
- Coq 8.13.0, OCaml 4.11.1 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.7.1+1, OCaml 4.05.0 :cross_mark: (error)
- Coq 8.7.1+2, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.7.2, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.8.1, OCaml 4.04.2 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.8.1, OCaml 4.04.2 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.12.0, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error)
17513 attempted package installations (including incompatible packages), 8 errors, 0.05% errors
Summary of the past 72 hours:
- tactician-dummy.1.0~beta1:
- Coq 8.6.1, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.6.1, OCaml 4.05.0 :cross_mark: (error)
- Coq 8.7.1+1, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.7.1, OCaml 4.03.0 :cross_mark: (error)
- Coq 8.8.0, OCaml 4.09.1 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.8.0, OCaml 4.09.1 :cross_mark: (error)
17536 attempted package installations (including incompatible packages), 6 errors, 0.03% errors
Summary of the past 72 hours:
- dijkstra.0.1.0:
- Coq 8.8.1, OCaml 4.05.0 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.03.0 :cross_mark: (error)
- monae.0.2.2:
- Coq 8.11.1, OCaml 4.11.1 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.10.1 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.7.0, OCaml 4.08.1 :cross_mark: (error)
- Coq 8.7.2, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.8.0, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.8.1, OCaml 4.05.0 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.03.0 :cross_mark: (error)
- Coq 8.9.1, OCaml 4.09.1 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.8.0, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.8.1, OCaml 4.05.0 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.06.1 :cross_mark: (error)
* 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
Summary of the past 72 hours:
- dijkstra.0.1.0:
- Coq 8.9.1, OCaml 4.08.1 :cross_mark: (error)
- monae.0.2.2:
- Coq 8.12.0, OCaml 4.10.1 :cross_mark: (error)
- Coq 8.12.0, OCaml 4.11.1 :cross_mark: (error)
- monae.0.3:
- Coq 8.13.0, OCaml 4.07.1 :cross_mark: (error)
- monae.0.3.1:
- Coq 8.13.0, OCaml 4.07.1 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.7.1+1, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.7.1+2, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.7.1, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.9.1, OCaml 4.08.1 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.9.1, OCaml 4.08.1 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.12.0, OCaml 4.10.1 :cross_mark: (error)
* 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
Summary of the past 72 hours:
- dijkstra.0.1.0:
- Coq 8.8.0, OCaml 4.05.0 :cross_mark: (error)
- monae.0.2.2:
- Coq 8.11.2, OCaml 4.10.1 :cross_mark: (error)
- Coq 8.12.0, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.11.1 :cross_mark: (error)
- tactician-dummy.1.0~beta1:
- Coq 8.8.0, OCaml 4.05.0 :cross_mark: (error)
- type-infer.0.1.0:
- Coq 8.8.0, OCaml 4.05.0 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.12.0, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.11.1 :cross_mark: (error)
19353 attempted package installations (including incompatible packages), 8 errors, 0.04% errors
Summary of the past 72 hours:
- monae.0.2.2:
- Coq 8.11.2, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.11.2, OCaml 4.11.1 :cross_mark: (error)
- monae.0.3:
- Coq 8.13.0, OCaml 4.10.1 :cross_mark: (error)
- monae.0.3.1:
- Coq 8.13.0, OCaml 4.10.1 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.13.0, OCaml 4.10.1 :cross_mark: (error)
15840 attempted package installations (including incompatible packages), 5 errors, 0.03% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (uninstallation error)
- cfml.20181201:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (uninstallation error)
- coqeal.1.0.5:
- Coq 8.10.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- Coq 8.11.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.11.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- monae.0.2.1:
- Coq 8.11.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.11.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- monae.0.2.2:
- Coq 8.11.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.11.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- Coq 8.11.1, OCaml 4.10.1 :cross_mark: (error)
- monae.0.3:
- Coq 8.13.0, OCaml 4.11.1 :cross_mark: (error)
- monae.0.3.1:
* 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
I am looking at fixing Monae
Summary of the past 72 hours:
- monae.0.2.2:
- Coq 8.11.0, OCaml 4.08.1 :cross_mark: (error)
- Coq 8.11.0, OCaml 4.09.1 :cross_mark: (error)
14150 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
@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 :-(
should I PR to fix the incriminated releases?
OK. I just merged this pull-request https://github.com/coq/opam-coq-archive/pull/1663 which should help
Thank you!
Summary of the past 72 hours:
- monae.0.2.2:
- Coq 8.12.1, OCaml 4.10.1 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.12.1, OCaml 4.10.1 :cross_mark: (error)
14152 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
3550 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- coqeal.1.0.5:
- Coq 8.12.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- monae.0.2.1:
- Coq 8.12.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- monae.0.2.2:
- Coq 8.12.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- vst-32.2.7:
- Coq 8.12.0, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.11.1 :cross_mark: (error)
17754 attempted package installations (including incompatible packages), 6 errors, 0.03% errors
Summary of the past 72 hours:
- coqeal.1.0.5:
- Coq 8.11.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- hierarchy-builder-shim.1.1.0:
- Coq 8.7.1+2, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.03.0 :cross_mark: (error)
- monae.0.2.1:
- Coq 8.11.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- monae.0.2.2:
- Coq 8.11.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- vst-32.2.7:
- Coq 8.12.0, OCaml 4.10.1 :cross_mark: (error)
14212 attempted package installations (including incompatible packages), 6 errors, 0.04% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error)
- cfml.20181201:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error)
- chick-blog.1.0.0:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error)
- chick-blog.1.0.1:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error)
- graph-theory.0.8:
- Coq 8.11.1, OCaml 4.11.1 :cross_mark: (error)
- Coq 8.11.2, OCaml 4.08.1 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.09.1 :cross_mark: (error)
- hierarchy-builder-shim.1.1.0:
- Coq 8.5.0~camlp4, OCaml 4.04.2 :cross_mark: (error)
- Coq 8.5.1, OCaml 4.02.3 :cross_mark: (error)
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (error)
- Coq 8.8.2, OCaml 4.06.1 :cross_mark: (error)
- vst-32.2.7:
* Coq 8.12.1, OCaml 4.09.1 :cross_mark: (error)
12459 attempted package installations (including incompatible packages), 12 errors, 0.10% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (uninstallation error)
- Coq 8.7.0, OCaml 4.04.2 :cross_mark: (uninstallation error)
- Coq 8.7.0, OCaml 4.05.0 :cross_mark: (uninstallation error)
- cfml.20181201:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (uninstallation error)
- Coq 8.7.0, OCaml 4.04.2 :cross_mark: (uninstallation error)
- Coq 8.7.0, OCaml 4.05.0 :cross_mark: (uninstallation error)
- chick-blog.1.0.0:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (uninstallation error)
- chick-blog.1.0.1:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (uninstallation error)
- coqeal.1.0.5:
- Coq 8.10.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- Coq 8.10.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- firing-squad.8.6.0:
- Coq 8.6, OCaml 4.02.3 :cross_mark: (error)
- graph-theory.0.8:
* 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
All errors should be fixed or related to some kind of instability (still, that is a lot of instability now)
(I should probably restart the servers with some fixes)
In particular to remove the uninstallation errors, which should now be impossible with the automatic file tracking of opam
and the timeout errors (the timeouts need to be increased)
Summary of the past 72 hours:
- aac-tactics.8.13.0:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- cfml.20180525:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (uninstallation error)
- cfml.20181201:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (uninstallation error)
- elpi.1.9.0:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- elpi.1.9.1:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- elpi.1.9.2:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- intuitionistic-nuprl.8.6.0:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- vst-32.2.7.1:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
10695 attempted package installations (including incompatible packages), 9 errors, 0.08% errors
Summary of the past 72 hours:
- elpi.1.9.3:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- elpi.1.9.4:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- elpi.1.9.5:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- hierarchy-builder.1.1.0:
- Coq 8.13.0, OCaml 4.12.0 :large_orange_diamond: (error with dependencies)
- infotheo.0.3:
- Coq 8.13.0, OCaml 4.12.0 :large_orange_diamond: (error with dependencies)
- infotheo.0.3.1:
- Coq 8.13.0, OCaml 4.12.0 :large_orange_diamond: (error with dependencies)
- infotheo.0.3.2:
- Coq 8.13.0, OCaml 4.12.0 :large_orange_diamond: (error with dependencies)
- mathcomp-analysis.0.3.7:
- Coq 8.13.0, OCaml 4.12.0 :large_orange_diamond: (error with dependencies)
- monae.0.3.2:
- Coq 8.13.0, OCaml 4.12.0 :large_orange_diamond: (error with dependencies)
- vst-32.2.7:
- Coq 8.12.1, OCaml 4.10.1 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.11.1 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- vst-32.2.7.1:
- Coq 8.12.1, OCaml 4.10.1 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.11.1 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
23180 attempted package installations (including incompatible packages), 15 errors, 0.06% errors
the errors with elpi
should be fixed I think, as the package got updated; I also increased the installation timeout for vst
Summary of the past 72 hours:
- chick-blog.1.0.1:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- compcert-32.3.8:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- compcert.3.8:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- coqeal.1.0.5:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- dijkstra.0.1.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- elpi.1.8.1:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- elpi.1.9.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- elpi.1.9.1:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- elpi.1.9.2:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- elpi.1.9.3:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- elpi.1.9.4:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- elpi.1.9.5:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- elpi.1.9.6:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- elpi.1.9.7:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- freespec-core.0.3:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- graph-theory.0.8:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- hierarchy-builder.1.0.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- hierarchy-builder.1.1.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- http.0.1.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- infotheo.0.3:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- infotheo.0.3.1:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- infotheo.0.3.2:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- itree-io.0.1.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- itree.4.0.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- mathcomp-analysis.0.3.5:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- mathcomp-analysis.0.3.6:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- mathcomp-analysis.0.3.7:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- mathcomp-multinomials.1.5.4:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- min-imports.1.0.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- min-imports.1.0.1:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- min-imports.1.0.2:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- monae.0.3:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- monae.0.3.1:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- monae.0.3.2:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- of-ocaml.2.0.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- of-ocaml.2.1.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- quickchick.1.5.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- tactician-dummy.1.0~beta1:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- type-infer.0.1.0:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- vst-32.2.7:
- Coq 8.12.1, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- Coq 8.13.2, OCaml 4.12.0 :cross_mark: (error)
- vst-32.2.7.1:
- Coq 8.12.1, OCaml 4.06.1 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- vst.2.7:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- Coq 8.13.2, OCaml 4.12.0 :cross_mark: (error)
- vst.2.7.1:
- Coq 8.13.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
8928 attempted package installations (including incompatible packages), 47 errors, 0.53% errors
OK so there seems to be an architectural bug in the coq-bench
, I need to investigate that
Summary of the past 72 hours:
- compcert-32.3.8:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error)
- compcert.3.8:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error)
- coqeal.1.0.5:
- Coq 8.11.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- vst-32.2.7:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies)
- vst-32.2.7.1:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies)
- vst.2.7:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies)
- vst.2.7.1:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies)
12511 attempted package installations (including incompatible packages), 7 errors, 0.06% errors
All these errors should be fixed now
Summary of the past 72 hours:
- compcert-32.3.8:
- Coq 8.12.0, OCaml 4.11.2 :cross_mark: (error)
- Coq 8.9.0, OCaml 4.06.1 :cross_mark: (error)
- compcert-64.3.7+8.12~coq_platform:
- Coq 8.12.0, OCaml 4.11.2 :cross_mark: (error)
- coqeal.1.0.5:
- Coq 8.11.1, OCaml 4.05.0 :large_orange_diamond: (error with dependencies)
- Coq 8.11.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- hierarchy-builder-shim.1.1.0:
- Coq 8.9.0, OCaml 4.06.1 :cross_mark: (error)
- vst-32.2.7:
- Coq 8.12.0, OCaml 4.11.2 :large_orange_diamond: (error with dependencies)
- vst-32.2.7.1:
- Coq 8.12.0, OCaml 4.11.2 :large_orange_diamond: (error with dependencies)
- vst-64.2.6:
- Coq 8.12.0, OCaml 4.11.2 :large_orange_diamond: (error with dependencies)
14306 attempted package installations (including incompatible packages), 9 errors, 0.06% errors
Fixes ongoing for the errors listed there
Summary of the past 72 hours:
- compcert-32.3.8:
- Coq 8.10.1, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.11.1, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.10.2 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.11.2 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.12.0 :cross_mark: (error)
- compcert-64.3.7+8.12~coq_platform:
- Coq 8.12.1, OCaml 4.10.2 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.11.2 :cross_mark: (error)
- vst-32.2.7:
- 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)
- 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-32.2.7.1:
- 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)
* 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
Summary of the past 72 hours:
- chick-blog.1.0.1:
- Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- compcert-32.3.8:
- Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- Coq 8.8.1, OCaml 4.06.1 :cross_mark: (error)
- compcert.3.8:
- Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- coqeal.1.0.5:
- Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- dijkstra.0.1.0:
- Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- elpi.1.8.1:
- Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- elpi.1.9.0:
- Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- elpi.1.9.1:
- Coq 8.13.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies)
- elpi.1.9.2:
* 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:
* 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:
* 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:
* 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
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)
Summary of the past 72 hours:
17890 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- hardware.8.5.0:
- Coq 8.5.2, OCaml 4.02.3 :cross_mark: (error)
19680 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- metacoq-pcuic.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
17901 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- metacoq-erasure.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- metacoq-pcuic.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.08.1 :cross_mark: (error)
- metacoq-safechecker.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- metacoq.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
12536 attempted package installations (including incompatible packages), 4 errors, 0.03% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error)
- cfml.20181201:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error)
- chick-blog.1.0.0:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error)
- chick-blog.1.0.1:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error)
- metacoq-pcuic.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.10.2 :cross_mark: (error)
16120 attempted package installations (including incompatible packages), 5 errors, 0.03% errors
Summary of the past 72 hours:
14335 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
16128 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
14346 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
5385 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error)
- chick-blog.1.0.1:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error)
19758 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
19760 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
10776 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- infotheo.0.3:
- Coq 8.13.0, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.10.2 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.12.0 :cross_mark: (error)
- infotheo.0.3.1:
- Coq 8.13.0, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.10.2 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.12.0 :cross_mark: (error)
- infotheo.0.3.2:
- Coq 8.13.0, OCaml 4.09.1 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.10.2 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.12.0 :cross_mark: (error)
- monae.0.3.2:
- Coq 8.13.0, OCaml 4.09.1 :large_orange_diamond: (error with dependencies)
- Coq 8.13.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- Coq 8.13.1, OCaml 4.12.0 :large_orange_diamond: (error with dependencies)
17966 attempted package installations (including incompatible packages), 12 errors, 0.07% errors
Summary of the past 72 hours:
- infotheo.0.2.2:
- Coq 8.11.0, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.12.0, OCaml 4.10.2 :cross_mark: (error)
- infotheo.0.3:
- Coq 8.13.0, OCaml 4.11.2 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- infotheo.0.3.1:
- Coq 8.13.0, OCaml 4.11.2 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- infotheo.0.3.2:
- Coq 8.13.0, OCaml 4.11.2 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
- monae.0.3.2:
- Coq 8.13.0, OCaml 4.11.2 :large_orange_diamond: (error with dependencies)
- Coq 8.13.0, OCaml 4.12.0 :large_orange_diamond: (error with dependencies)
14376 attempted package installations (including incompatible packages), 10 errors, 0.07% errors
Summary of the past 72 hours:
- infotheo.0.2.2:
- Coq 8.11.2, OCaml 4.11.2 :cross_mark: (error)
- Coq 8.12.1, OCaml 4.10.2 :cross_mark: (error)
- Coq 8.12.2, OCaml 4.08.1 :cross_mark: (error)
19892 attempted package installations (including incompatible packages), 3 errors, 0.02% errors
Summary of the past 72 hours:
- infotheo.0.2.2:
- Coq 8.12.2, OCaml 4.11.2 :cross_mark: (error)
14488 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.7.0, OCaml 4.07.1 :cross_mark: (uninstallation error)
- chick-blog.1.0.1:
- Coq 8.7.0, OCaml 4.07.1 :cross_mark: (uninstallation error)
- monae.0.3.2:
- Coq 8.13.1, OCaml 4.12.0 :cross_mark: (error)
16330 attempted package installations (including incompatible packages), 3 errors, 0.02% errors
Summary of the past 72 hours:
- approx-models.1.0:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
16364 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- algorand.1.2:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- compcert-32.3.8:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- compcert-32.3.9:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- compcert-64.3.7~coq-platform:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- compcert-64.3.7~coq-platform~open-source:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- compcert.3.7~coq-platform:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- compcert.3.7~coq-platform~open-source:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- compcert.3.8:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- compcert.3.9:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- flocq.3.4.1:
- Coq 8.11.1, OCaml 4.08.1 :cross_mark: (error)
- gappa.1.4.3:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- gappa.1.4.4:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- gappa.1.4.5:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- gappa.1.4.6:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- interval.3.4.2:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- interval.4.0.0:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- interval.4.1.0:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- interval.4.1.1:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- interval.4.2.0:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- interval.4.3.0:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- libvalidsdp.0.7.0:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- pi-agm.1.2.4:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- pi-agm.1.2.5:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- validsdp.0.7.0:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- vst-64.2.6:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
- vst.2.6:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
16386 attempted package installations (including incompatible packages), 26 errors, 0.16% errors
Summary of the past 72 hours:
- algorand.1.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)
- chick-blog.1.0.0:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error)
- chick-blog.1.0.1:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error)
- compcert-32.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-32.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)
- compcert-64.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-64.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.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:
* 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)
- interval.4.1.1:
- 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.2.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.3.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)
- libvalidsdp.0.7.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)
- pi-agm.1.2.4:
- 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)
- pi-agm.1.2.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)
- validsdp.0.7.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) * 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
Summary of the past 72 hours:
- algorand.1.2:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- compcert-32.3.8:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- compcert-32.3.9:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- compcert-64.3.7~coq-platform:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- compcert-64.3.7~coq-platform~open-source:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- compcert.3.7~coq-platform:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- compcert.3.7~coq-platform~open-source:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- compcert.3.8:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- compcert.3.9:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- flocq.3.4.1:
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error)
- gappa.1.4.3:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- gappa.1.4.4:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- gappa.1.4.5:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- gappa.1.4.6:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- hydra-battles.0.4:
- Coq 8.12.0, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
- interval.3.4.2:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- interval.4.0.0:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- interval.4.1.0:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- interval.4.1.1:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- interval.4.2.0:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- interval.4.3.0:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- libvalidsdp.0.7.0:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- pi-agm.1.2.4:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- pi-agm.1.2.5:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- validsdp.0.7.0:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- vst-64.2.6:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- vst.2.6:
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- waterproof.1.0.0:
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error)
18240 attempted package installations (including incompatible packages), 28 errors, 0.15% errors
OK, it seems the error is from before the update of coq-flocq
, it should be fixed now
That shows that many packages are using coq-flocq
!
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.
OK, good catch, I haven't seen for hydra-battle
! I fixed waterproof
.
Hmm, didn't know about that problem, @Guillaume Claret can you add the dependency?
Matthieu Sozeau said:
Hmm, didn't know about that problem, Guillaume Claret can you add the dependency?
OK
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.)
Okay, it is back up, and yes, Equations explicitly uses Ocamlfind.
I think it does in the doc target or configure?
After looking at it, it seems that coq_makefile
generates OCaml rules which use ocamlfind
, like CAMLOPTC ?= "$(OCAMLFIND)" opt -c
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error)
- chick-blog.1.0.1:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error)
- waterproof.1.0.0:
- Coq 8.11.0, OCaml 4.08.1 :cross_mark: (error)
16430 attempted package installations (including incompatible packages), 3 errors, 0.02% errors
Summary of the past 72 hours:
18270 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Guillaume Claret said:
After looking at it, it seems that
coq_makefile
generates OCaml rules which useocamlfind
, likeCAMLOPTC ?= "$(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.
don't we use ocamlfind to build plugins in general?
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.
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error)
- chick-blog.1.0.1:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error)
16443 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
20097 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
16447 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
14624 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- chick-blog.1.0.0:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error)
- chick-blog.1.0.1:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error)
14624 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
14624 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
16452 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
16452 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
10978 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
10998 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
16537 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
20230 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
16567 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- infotheo.0.3.3:
- Coq 8.13.0, OCaml 4.10.2 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.09.1 :cross_mark: (error)
- monae.0.3.4:
- Coq 8.13.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- Coq 8.13.1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies)
14741 attempted package installations (including incompatible packages), 4 errors, 0.03% errors
Summary of the past 72 hours:
- infotheo.0.3.3:
- Coq 8.13.0, OCaml 4.07.1 :cross_mark: (error)
- monae.0.3.4:
- Coq 8.13.0, OCaml 4.07.1 :large_orange_diamond: (error with dependencies)
12901 attempted package installations (including incompatible packages), 2 errors, 0.02% errors
Summary of the past 72 hours:
- infotheo.0.3.3:
- Coq 8.13.1, OCaml 4.12.0 :cross_mark: (error)
- Coq 8.13.2, OCaml 4.08.1 :cross_mark: (error)
- monae.0.3.4:
- Coq 8.13.1, OCaml 4.12.0 :large_orange_diamond: (error with dependencies)
- Coq 8.13.2, OCaml 4.08.1 :large_orange_diamond: (error with dependencies)
18432 attempted package installations (including incompatible packages), 4 errors, 0.02% errors
Summary of the past 72 hours:
12929 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
18480 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
16632 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
20333 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
12943 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
16643 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
18500 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
0 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
ping @Guillaume Claret looks like there might be something wrong with the Coq opam bench (no package installation attempts for 3+ days)
Yes, indeed, I restarted everything for upgrades, thanks for the ping
Summary of the past 72 hours:
14800 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
9250 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
16650 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
14831 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- graph-theory.0.8:
- Coq 8.13.0, OCaml 4.08.1 :cross_mark: (error)
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
14875 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
- graph-theory.0.8:
- Coq 8.13.2, OCaml 4.12.0 :cross_mark: (error)
13055 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- graph-theory.0.8:
- Coq 8.13.1, OCaml 4.07.1 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.10.2 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.12.0 :cross_mark: (error)
- Coq 8.13.2, OCaml 4.11.2 :cross_mark: (error)
16846 attempted package installations (including incompatible packages), 4 errors, 0.02% errors
Summary of the past 72 hours:
15004 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
15028 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- graph-theory.0.8:
- Coq 8.13.0, OCaml 4.12.0 :cross_mark: (error)
15039 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- chick-blog.1.0.1:
- Coq 8.14.0, OCaml 4.09.1 :large_orange_diamond: (error with dependencies)
- coqprime.1.0.6:
- Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error)
- coquelicot.3.1.0:
- Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error)
- fourcolor.1.2.3:
- Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error)
- graph-theory.0.8:
- Coq 8.13.2, OCaml 4.10.2 :cross_mark: (error)
- Coq 8.13.2, OCaml 4.12.0 :cross_mark: (error)
- interval.4.1.0:
- Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error)
- interval.4.1.1:
- Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error)
- itauto.8.13:
- Coq 8.14.0, OCaml 4.09.1 :cross_mark: (error)
- list-string.2.0.0:
* 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:
* 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
Summary of the past 72 hours:
- graph-theory.0.8:
- Coq 8.13.0, OCaml 4.11.2 :cross_mark: (error)
- Coq 8.13.1, OCaml 4.12.0 :cross_mark: (error)
15152 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
- graph-theory.0.8:
- Coq 8.13.1, OCaml 4.09.1 :cross_mark: (error)
11374 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- graph-theory.0.8:
- Coq 8.13.1, OCaml 4.08.1 :cross_mark: (error)
15168 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- chick-blog.1.0.1:
- Coq 8.14.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies)
- coqprime.1.0.6:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- fourcolor.1.2.3:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- itauto.8.13:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- list-string.2.0.0:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- list-string.2.1.0:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- list-string.2.1.1:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- menhirlib.20200525:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- menhirlib.20200612:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- menhirlib.20200619:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- menhirlib.20200624:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- menhirlib.20201122:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- menhirlib.20201201:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- menhirlib.20201214:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- menhirlib.20201216:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- moment.1.1.0:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- moment.1.2.0:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- semantics.8.11.1:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
- waterproof.1.0.0:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error)
20865 attempted package installations (including incompatible packages), 19 errors, 0.09% errors
Most errors for 8.14 are now fixed
(remnants of previous builds)
A bench process is also running with OCaml 4.13 now
Summary of the past 72 hours:
- chick-blog.1.0.1:
- Coq 8.14.0, OCaml 4.12.0 :large_orange_diamond: (error with dependencies)
- coqprime.1.0.6:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- list-string.2.0.0:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- list-string.2.1.0:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- list-string.2.1.1:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- menhirlib.20200525:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- menhirlib.20200612:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- menhirlib.20200619:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- menhirlib.20200624:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- menhirlib.20201122:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- menhirlib.20201201:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- menhirlib.20201214:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- menhirlib.20201216:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- metacoq-erasure.1.0~alpha1+8.9:
- Coq 8.9.0, OCaml 4.03.0 :large_orange_diamond: (error with dependencies)
- moment.1.1.0:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
- moment.1.2.0:
- Coq 8.14.0, OCaml 4.12.0 :cross_mark: (error)
7621 attempted package installations (including incompatible packages), 16 errors, 0.21% errors
Summary of the past 72 hours:
17202 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
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.
8.14.0 is fixed
No need to modify thousands of packages, just put the fix in the coq packages that need it IMO
Summary of the past 72 hours:
- aac-tactics.8.13.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:)
- aac-tactics.8.13.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:)
- addition-chains.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:)
- addition-chains.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:)
- approx-models.1.0:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- bignums.8.13.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:)
- coinduction.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:) * 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:)
* 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:
* 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:)
- equations.1.3~beta2+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:)
- gaia-hydras.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:)
- gappa.1.4.4:
- Coq 8.12.1, OCaml 4.08.1 :cross_mark: (error :fire:)
- gappa.1.4.5:
- 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:)
- gappa.1.4.6:
- 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:)
- goedel.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:)
- hammer-tactics.1.3.1+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-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:
* 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:)
- math-classes.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:)
- metacoq-pcuic.1.0~beta2+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:)
- metacoq-template.1.0~beta2+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:)
- metacoq-translations.1.0~beta2+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:)
- mtac2.1.4+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:)
- paramcoq.1.1.2+coq8.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:)
- paramcoq.1.1.3+coq8.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:) * 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:
* 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:)
- vst-64.2.6:
- Coq 8.12.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- vst.2.6:
- Coq 8.12.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
21100 attempted package installations (including incompatible packages), 135 errors, 0.64% errors
@Emilio Jesús Gallego Arias @Enrico Tassi so how should we tackle 8.13 and 8.12 errors according to above?
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
@Karl Palmskog adapting the patch for 8.14 should work
annoying but easy I think
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...
I think only 8.13 is impacted, and 8.12 errors above are related to something else
We can try to fix 8.13.2 first and see how it goes
I added a PR for Coq 8.13.2: https://github.com/ocaml/opam-repository/pull/20025
Summary of the past 72 hours:
- aac-tactics.8.13.1:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- aac-tactics.8.13.2:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- addition-chains.0.4:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- addition-chains.0.5:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- bignums.8.13.0:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.0:
- Coq 8.13.0, 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:)
- coinduction.1.2:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.3:
- Coq 8.13.0, 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:)
- compcert-32.3.8:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.11.2 :cross_mark: (error :fire:)
- compcert-32.3.9:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.11.2 :cross_mark: (error :fire:)
- coqeal.1.0.5:
- Coq 8.13.0, 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:)
- coqeal.1.1.0:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- coqprime.1.0.6:
- Coq 8.13.0, 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:)
- dpdgraph.0.6.9:
- Coq 8.13.0, 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:)
- equations.1.2.3+8.13:
- Coq 8.13.0, 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:)
- equations.1.3~beta1+8.13:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- equations.1.3~beta2+8.13:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- gaia-hydras.0.5:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- gappa.1.4.5:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.11.2 :cross_mark: (error :fire:)
- gappa.1.4.6:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.11.2 :cross_mark: (error :fire:)
- goedel.8.13.0:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hammer-tactics.1.3.1+8.13:
- Coq 8.13.0, 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:)
- hammer.1.3.1+8.13:
- Coq 8.13.0, 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:)
- hydra-battles.0.4:
- Coq 8.13.0, 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:)
- interval.4.1.0:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.1, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.11.2 :cross_mark: (error :fire:)
- interval.4.1.1:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.1, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.11.2 :cross_mark: (error :fire:)
- interval.4.2.0:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.1, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.11.2 :cross_mark: (error :fire:)
- interval.4.3.0:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.3.1:
- Coq 8.13.0, 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:)
- katamaran.0.1.0:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- math-classes.8.13.0:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq-pcuic.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq-template.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq-translations.1.0~beta2+8.13:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- mtac2.1.4+8.13:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- paramcoq.1.1.2+coq8.13:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- paramcoq.1.1.3+coq8.13:
- Coq 8.13.0, 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:)
- quickchick.1.5.0:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- quickchick.1.5.1:
- Coq 8.13.0, 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:)
- reduction-effects.0.1.3:
- Coq 8.13.0, 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:)
- smpl.8.13:
- Coq 8.13.0, 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:)
- unicoq.1.5+8.13:
- Coq 8.13.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- vst-32.2.7:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- vst-32.2.7.1:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- vst-32.2.8:
- Coq 8.13.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
15376 attempted package installations (including incompatible packages), 78 errors, 0.51% errors
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.
but isn't 8.12.2 affected as well?
It should be fine as it is not compatible with OCaml 4.13
Summary of the past 72 hours:
- aac-tactics.8.13.1:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- aac-tactics.8.13.2:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- addition-chains.0.4:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- addition-chains.0.5:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- approx-models.1.0:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- bignums.8.13.0:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.0:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- coinduction.1.1:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.2:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.3:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- color.1.8.1:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- compcert-32.3.8:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- compcert-32.3.9:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coqeal.1.0.5:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- coqeal.1.0.6:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- coqeal.1.1.0:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- coqprime.1.0.6:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- corn.8.13.0:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- dpdgraph.0.6.9:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- dpdgraph.1.0+8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- equations.1.2.3+8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- equations.1.2.4+8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- equations.1.3~beta1+8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- equations.1.3~beta2+8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- gaia-hydras.0.5:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- gappa.1.4.5:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- gappa.1.4.6:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- goedel.8.13.0:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hammer-tactics.1.3.1+8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- hammer-tactics.1.3.2+8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- hammer.1.3.1+8.13:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hammer.1.3.2+8.13:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hydra-battles.0.4:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hydra-battles.0.5:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.1.0:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.1.1:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.2.0:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.3.0:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.3.1:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- itauto.8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- katamaran.0.1.0:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- math-classes.8.13.0:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq-pcuic.1.0~beta2+8.13:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq-template.1.0~beta2+8.13:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq-translations.1.0~beta2+8.13:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- mtac2.1.4+8.13:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- paramcoq.1.1.2+coq8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- paramcoq.1.1.3+coq8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- pi-agm.1.2.6:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- quickchick.1.5.0:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- quickchick.1.5.1:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- reduction-effects.0.1.2:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- reduction-effects.0.1.3:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- relation-algebra.1.7.5:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- smpl.8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- switch.1.0.5:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- unicoq.1.5+8.13:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- vst-32.2.7.1:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- vst-32.2.8:
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.14.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
11541 attempted package installations (including incompatible packages), 61 errors, 0.53% errors
Summary of the past 72 hours:
- aac-tactics.8.13.1:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- aac-tactics.8.13.2:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- addition-chains.0.4:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- addition-chains.0.5:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- approx-models.1.0:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- bignums.8.13.0:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.0:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- coinduction.1.1:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.2:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.3:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- color.1.8.1:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- compcert-64.3.7+8.12~coq_platform:
- Coq 8.12.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.09.1 :cross_mark: (error :fire:)
- compcert-64.3.7+8.12~coq_platform~open_source:
- Coq 8.12.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.09.1 :cross_mark: (error :fire:)
- compcert.3.7+8.12~coq_platform:
- Coq 8.12.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.09.1 :cross_mark: (error :fire:)
- compcert.3.7+8.12~coq_platform~open_source:
- Coq 8.12.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.09.1 :cross_mark: (error :fire:)
- coqeal.1.0.5:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- coqeal.1.0.6:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- coqeal.1.1.0:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- coqprime.1.0.6:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- corn.8.13.0:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- dpdgraph.0.6.9:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- dpdgraph.1.0+8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- equations.1.2.3+8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- equations.1.2.4+8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- equations.1.3~beta1+8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- equations.1.3~beta2+8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- gaia-hydras.0.5:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- gappa.1.4.4:
- Coq 8.12.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.09.1 :cross_mark: (error :fire:)
- goedel.8.13.0:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hammer-tactics.1.3.1+8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- hammer-tactics.1.3.2+8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- hammer.1.3.1+8.13:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hammer.1.3.2+8.13:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hydra-battles.0.4:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hydra-battles.0.5:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.0.0:
- Coq 8.12.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.09.1 :cross_mark: (error :fire:)
- interval.4.1.0:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.1.1:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.2.0:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.3.0:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.3.1:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- itauto.8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- katamaran.0.1.0:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- math-classes.8.13.0:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq-pcuic.1.0~beta2+8.13:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq-template.1.0~beta2+8.13:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq-translations.1.0~beta2+8.13:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- mtac2.1.4+8.13:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- paramcoq.1.1.2+coq8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- paramcoq.1.1.3+coq8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- pi-agm.1.2.6:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- quickchick.1.5.0:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- quickchick.1.5.1:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- reduction-effects.0.1.2:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- reduction-effects.0.1.3:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- relation-algebra.1.7.5:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- smpl.8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- switch.1.0.5:
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- unicoq.1.5+8.13:
- Coq 8.13.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- vst-64.2.6:
- Coq 8.12.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.12.0, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- vst.2.6:
- Coq 8.12.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.12.0, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
15393 attempted package installations (including incompatible packages), 122 errors, 0.79% errors
Summary of the past 72 hours:
- mathcomp-analysis.0.3.10:
- Coq 8.14.0, OCaml 4.11.2 :cross_mark: (error :fire:)
13486 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- algorand.1.2:
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- algorand.1.3:
- Coq 8.12.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- compcert-64.3.7+8.12~coq_platform:
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- compcert-64.3.7+8.12~coq_platform~open_source:
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- compcert.3.7+8.12~coq_platform:
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- compcert.3.7+8.12~coq_platform~open_source:
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- gappa.1.4.4:
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- infotheo.0.1.1:
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- infotheo.0.1.2:
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.12.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- infotheo.0.2:
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.12.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- infotheo.0.2.1:
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.12.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- infotheo.0.2.2:
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.12.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- infotheo.0.3:
- Coq 8.13.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- infotheo.0.3.1:
- Coq 8.13.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- infotheo.0.3.2:
- Coq 8.13.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- infotheo.0.3.3:
- Coq 8.13.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.0.0:
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.1:
- Coq 8.11.2, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.10:
- Coq 8.11.2, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.09.1 :cross_mark: (error :fire:)
- Coq 8.14.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.2:
- Coq 8.11.2, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.3:
- Coq 8.11.2, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.4:
- Coq 8.11.2, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.5:
- Coq 8.11.2, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.09.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.6:
- Coq 8.11.2, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.09.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.7:
- Coq 8.11.2, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.09.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.8:
- Coq 8.11.2, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.09.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.9:
- Coq 8.11.2, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.11.2, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.09.1 :cross_mark: (error :fire:)
- monae.0.1.1:
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- monae.0.1.2:
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.12.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- monae.0.2:
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.12.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- monae.0.2.1:
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.12.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- monae.0.2.2:
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.12.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- monae.0.3:
- Coq 8.13.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- monae.0.3.1:
- Coq 8.13.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- monae.0.3.2:
- Coq 8.13.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- monae.0.3.3:
- Coq 8.13.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- monae.0.3.4:
- Coq 8.13.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- vst-64.2.6:
- Coq 8.12.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- vst.2.6:
- Coq 8.12.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
23152 attempted package installations (including incompatible packages), 99 errors, 0.43% errors
@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.
I have made pull-requests to fix most of the bugs (except Gappa). We will see the results once they are merged.
I will take care of gappa.
@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.
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)?
if we can't reproduce on 8.12.2, then we can just mark gappa.1.4.4 as 8.12.0 incompatible.
@Michael Soegtrop did you try the following on 8.12.2:
coq-flocq.4.0.0
(it is compatible)coq-gappa.1.4.4
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
)
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.
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
I think we can just add the < 4
in coq-gappa.1.4.4 and see how it goes, I can do that
Yes, I have done that already :) https://github.com/coq/opam-coq-archive/pull/1965
so then I guess Michael has already validated that it works (I was using an old opam repo state)
ah OK, yes!
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?
Yes this is fixed
Summary of the past 72 hours:
- mathcomp-analysis.0.3.1:
- Coq 8.10.2, OCaml 4.09.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.2:
- Coq 8.10.2, OCaml 4.09.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.3:
- Coq 8.10.2, OCaml 4.09.1 :cross_mark: (error :fire:)
11589 attempted package installations (including incompatible packages), 3 errors, 0.03% errors
Btw.: is there an overview over all failures of all latest builds somewhere?
I think the only "latest" overview is in this Zulip topic
Summary of the past 72 hours:
- mathcomp-analysis.0.3.1:
- Coq 8.10.2, OCaml 4.08.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.2:
- Coq 8.10.2, OCaml 4.08.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.3.3:
- Coq 8.10.2, OCaml 4.08.1 :cross_mark: (error :fire:)
- of-ocaml.1.2.1:
- Coq 8.14.0, OCaml 4.05.0 :cross_mark: (error :fire:)
21270 attempted package installations (including incompatible packages), 4 errors, 0.02% errors
The homepage of the project https://coq-bench.github.io/ also gives a global overview, but does not directly point to the latest failures
Summary of the past 72 hours:
13544 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
17415 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- coqprime-generator.1.1.1:
- Coq 8.14.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.14.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.7.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
11616 attempted package installations (including incompatible packages), 3 errors, 0.03% errors
@Guillaume Claret you need to install the libtool
system package on the opam bench server for coqprime-generator
to install properly.
OK, thanks for the notice, I added this package!
Summary of the past 72 hours:
- coqprime-generator.1.1.1:
- Coq 8.10.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.0, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.7.1+1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
19374 attempted package installations (including incompatible packages), 4 errors, 0.02% errors
Summary of the past 72 hours:
- coqprime-generator.1.1.1:
- Coq 8.13.1, OCaml 4.12.1 :large_orange_diamond: (error with dependencies :fire_truck:)
15529 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
21393 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
19500 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- itree-io.0.1.0:
- Coq 8.11.2, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- itree.3.2.0:
- Coq 8.11.2, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- itree.4.0.0:
- Coq 8.11.2, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- paco.4.1.2:
- Coq 8.11.2, OCaml 4.11.2 :cross_mark: (error :fire:)
17564 attempted package installations (including incompatible packages), 4 errors, 0.02% errors
Summary of the past 72 hours:
11712 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- io-hello-world.1.2.0:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.1.0:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.3.0:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.4.1:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
19525 attempted package installations (including incompatible packages), 4 errors, 0.02% errors
OK, I do not really know why the uninstallation did not work, maybe an error in the bench system itself.
yeah no idea from the log, could it be something like no space on drive?
I guess we will see if it goes away.
The disk is fine
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.
Summary of the past 72 hours:
- infotheo.0.3.4:
- Coq 8.14.1, OCaml 4.12.1 :cross_mark: (error :fire:)
15637 attempted package installations (including incompatible packages), 1 error, 0.01% errors
ping @Reynald Affeldt it looks here like infotheo 0.3.4 is not compatible with the recently-released analysis 0.3.12.
I guess Guillaume or I will fix it eventually, but just flagging it up in the meantime.
Thanks for the ping. I pushed a fix.
Summary of the past 72 hours:
- infotheo.0.3.4:
- Coq 8.13.0, OCaml 4.12.1 :cross_mark: (error :fire:)
17602 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (error :fire:)
- cfml.20181201:
- Coq 8.10.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (error :fire:)
- Coq 8.9.0, OCaml 4.04.2 :cross_mark: (error :fire:)
- Coq 8.9.0, OCaml 4.06.1 :cross_mark: (error :fire:)
9787 attempted package installations (including incompatible packages), 5 errors, 0.05% errors
Summary of the past 72 hours:
21548 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- approx-models.1.0:
- Coq 8.15.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.15.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- bonsai.1.0.0:
- Coq 8.15.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- cfml-stdlib.20220112:
- Coq 8.14.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- cfml.20180525:
- Coq 8.7.1, OCaml 4.04.2 :cross_mark: (error :fire:)
- cfml.20181201:
- Coq 8.10.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.10.2, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.7.1, OCaml 4.04.2 :cross_mark: (error :fire:)
- cfml.20220112:
- Coq 8.14.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- chick-blog.1.0.1:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.1:
- Coq 8.15.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.2:
- Coq 8.15.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.3:
- Coq 8.15.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- flocq.3.4.1:
- Coq 8.15.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- flocq.3.4.2:
- Coq 8.15.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- interval.4.3.0:
- Coq 8.15.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- interval.4.3.1:
- Coq 8.15.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- pi-agm.1.2.6:
- Coq 8.15.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.15.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- relation-algebra.1.7.6:
- Coq 8.15.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
21581 attempted package installations (including incompatible packages), 29 errors, 0.13% errors
Summary of the past 72 hours:
- bonsai.1.0.0:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- cfml-stdlib.20220112:
- Coq 8.10.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.12.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.9.0, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- cfml.20180525:
- Coq 8.6, OCaml 4.04.2 :cross_mark: (error :fire:)
- cfml.20181201:
- Coq 8.10.2, OCaml 4.07.1 :cross_mark: (error :fire:)
- Coq 8.6, OCaml 4.04.2 :cross_mark: (error :fire:)
- Coq 8.9.0, OCaml 4.03.0 :cross_mark: (error :fire:)
- cfml.20220112:
- Coq 8.10.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.13.2, OCaml 4.12.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.9.0, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- chick-blog.1.0.1:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.0:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.1:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.2:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.3:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- flocq.3.4.1:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- flocq.3.4.2:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- relation-algebra.1.7.6:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
15734 attempted package installations (including incompatible packages), 19 errors, 0.12% errors
Summary of the past 72 hours:
- bonsai.1.0.0:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- cfml.20180525:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (error :fire:)
- Coq 8.7.1, OCaml 4.05.0 :cross_mark: (error :fire:)
- cfml.20181201:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (error :fire:)
- Coq 8.7.1, OCaml 4.05.0 :cross_mark: (error :fire:)
- chick-blog.1.0.1:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.0:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.1:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.2:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- coinduction.1.3:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- relation-algebra.1.7.6:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
19732 attempted package installations (including incompatible packages), 11 errors, 0.06% errors
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?
(all others should be fixed very soon)
OK indeed, thanks for the ping, fixing it
Summary of the past 72 hours:
- cfml.20181201:
- Coq 8.9.0, OCaml 4.07.1 :cross_mark: (error :fire:)
5951 attempted package installations (including incompatible packages), 1 error, 0.02% errors
OK, it seems you already solved this CFML error @Karl Palmskog so we are all good
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.7.0, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.7.0, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
19948 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
- io-system.2.1.0:
- Coq 8.15.0, OCaml 4.09.1 :cross_mark: (error :fire:)
- itauto.8.14.0:
- Coq 8.15.0, OCaml 4.09.1 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.12.1 :cross_mark: (error :fire:)
20037 attempted package installations (including incompatible packages), 3 errors, 0.01% errors
ping @Guillaume Claret the io-system
package doesn't work on 8.15 and later.
(I took care of itauto)
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...
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
14033 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.7.0, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.7.0, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
20063 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
- validsdp.1.0.0:
- Coq 8.12.2, OCaml 4.10.2 :cross_mark: (error :fire:)
14060 attempted package installations (including incompatible packages), 1 error, 0.01% errors
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.
It seems like the archive for ValidSDP is corrupted. It contains outdated configure scripts.
Thanks for pinging me, looks like I forgot to rerun autoconf before distributing the archive. I just updated it and it should work now.
but then I think the checksum will have changed, right? I think we need to update the package
@Pierre Roux should I do it?
Summary of the past 72 hours:
- unimath.20220204:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
18109 attempted package installations (including incompatible packages), 1 error, 0.01% errors
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.
https://github.com/UniMath/UniMath/issues/1459
Summary of the past 72 hours:
- unimath.20220204:
- Coq 8.13.0, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- validsdp.1.0.0:
- Coq 8.12.2, OCaml 4.09.1 :cross_mark: (error :fire:)
18141 attempted package installations (including incompatible packages), 4 errors, 0.02% errors
Summary of the past 72 hours:
- unimath.20220204:
- Coq 8.13.1, OCaml 4.12.1 :cross_mark: (error :fire:)
- Coq 8.14.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
16148 attempted package installations (including incompatible packages), 3 errors, 0.02% errors
@Guillaume Claret maybe you could add unimath.20220204
to the blacklist? It's pretty clear it takes way too long to test.
OK done (I increased the timeout for it)
Summary of the past 72 hours:
- unimath.20220204:
- Coq 8.14.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.10.2 :cross_mark: (error :fire:)
6064 attempted package installations (including incompatible packages), 2 errors, 0.03% errors
Summary of the past 72 hours:
- elpi.1.3.0:
- Coq 8.10.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hierarchy-builder.0.9.0:
- Coq 8.10.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- mtac2.1.0.0+8.7:
- Coq 8.7.1+2, OCaml 4.05.0 :cross_mark: (error :fire:)
20230 attempted package installations (including incompatible packages), 3 errors, 0.01% errors
Summary of the past 72 hours:
10119 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
14168 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- Coq 8.7.0, OCaml 4.06.1 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- Coq 8.7.0, OCaml 4.06.1 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.0:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.1:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
16210 attempted package installations (including incompatible packages), 6 errors, 0.04% errors
Summary of the past 72 hours:
- hierarchy-builder.0.9.0:
- Coq 8.11.2, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
16222 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- Coq 8.7.0, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- Coq 8.7.0, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.0:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.1:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- io-hello-world.1.2.0:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.1.0:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.3.0:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.4.1:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
14204 attempted package installations (including incompatible packages), 10 errors, 0.07% errors
Summary of the past 72 hours:
- elpi.1.0.0:
- Coq 8.10.2, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- elpi.1.1.0:
- Coq 8.10.2, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- elpi.1.2.0:
- Coq 8.10.2, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- elpi.1.3.0:
- Coq 8.10.2, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hierarchy-builder.0.9.0:
- Coq 8.10.2, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
12179 attempted package installations (including incompatible packages), 5 errors, 0.04% errors
Summary of the past 72 hours:
- elpi.1.3.1:
- Coq 8.11.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- hierarchy-builder.0.9.0:
- Coq 8.11.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
12180 attempted package installations (including incompatible packages), 2 errors, 0.02% errors
Summary of the past 72 hours:
16248 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- cfml.20181201:
- Coq 8.7.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
18288 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- elpi.1.3.1:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hierarchy-builder.0.9.0:
- Coq 8.11.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.11.2, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
16278 attempted package installations (including incompatible packages), 4 errors, 0.02% errors
Summary of the past 72 hours:
16329 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- io-hello-world.1.2.0:
- Coq 8.15.1, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.3.0:
- Coq 8.15.1, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.4.1:
- Coq 8.15.1, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
10214 attempted package installations (including incompatible packages), 5 errors, 0.05% errors
Summary of the past 72 hours:
- elpi.1.3.1:
- Coq 8.11.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hierarchy-builder.0.9.0:
- Coq 8.11.2, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
12295 attempted package installations (including incompatible packages), 2 errors, 0.02% errors
I added OCaml 4.14 to the test suite
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.7.0, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.7.0, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
14385 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
- fiat-crypto.0.0.13:
- Coq 8.15.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
14387 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- elpi.1.3.1:
- Coq 8.11.1, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- hierarchy-builder.0.9.0:
- Coq 8.11.1, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq.1.0~alpha1+8.9:
- Coq 8.9.0, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
24685 attempted package installations (including incompatible packages), 3 errors, 0.01% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.0:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.1:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
12347 attempted package installations (including incompatible packages), 4 errors, 0.03% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
14409 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
- fiat-crypto.0.0.13:
- Coq 8.15.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.15.1, OCaml 4.12.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.15.1, OCaml 4.14.0 :large_orange_diamond: (error with dependencies :fire_truck:)
18531 attempted package installations (including incompatible packages), 3 errors, 0.02% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6.1, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6.1, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
- fiat-crypto.0.0.13:
- Coq 8.15.0, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
12359 attempted package installations (including incompatible packages), 3 errors, 0.02% errors
Summary of the past 72 hours:
- fiat-crypto.0.0.13:
- Coq 8.15.0, OCaml 4.14.0 :large_orange_diamond: (error with dependencies :fire_truck:)
16480 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
14425 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- fiat-crypto.0.0.13:
- Coq 8.15.1, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
16503 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- fiat-crypto.0.0.13:
- Coq 8.15.0, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.15.0, OCaml 4.12.1 :large_orange_diamond: (error with dependencies :fire_truck:)
20642 attempted package installations (including incompatible packages), 2 errors, 0.01% errors
Summary of the past 72 hours:
10349 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.0:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.1:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- io-hello-world.1.2.0:
- Coq 8.14.1, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.1.0:
- Coq 8.14.1, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.3.0:
- Coq 8.14.1, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.4.1:
- Coq 8.14.1, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
14490 attempted package installations (including incompatible packages), 8 errors, 0.06% errors
Summary of the past 72 hours:
20700 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
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
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- Coq 8.7.0, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- Coq 8.7.0, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
16561 attempted package installations (including incompatible packages), 4 errors, 0.02% errors
Summary of the past 72 hours:
14497 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- fiat-crypto.0.0.13:
- Coq 8.15.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
16568 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- fiat-crypto.0.0.13:
- Coq 8.15.0, OCaml 4.13.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.15.1, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- mi-cho-coq.0.1:
- Coq 8.15.0, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.15.1, OCaml 4.10.2 :cross_mark: (error :fire:)
14514 attempted package installations (including incompatible packages), 4 errors, 0.03% errors
Summary of the past 72 hours:
- fiat-crypto.0.0.13:
- Coq 8.15.1, OCaml 4.14.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- gaia-hydras.0.5:
- Coq 8.13.1, OCaml 4.12.1 :cross_mark: (error :fire:)
- mi-cho-coq.0.1:
- Coq 8.14.1, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.15.1, OCaml 4.14.0 :cross_mark: (error :fire:)
14536 attempted package installations (including incompatible packages), 4 errors, 0.03% errors
Summary of the past 72 hours:
- fiat-crypto.0.0.13:
- Coq 8.15.0, OCaml 4.14.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- gaia-hydras.0.5:
- Coq 8.14.0, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.14.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- http.0.1.0:
- Coq 8.14.0, OCaml 4.06.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.14.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.14.0 :cross_mark: (error :fire:)
- mi-cho-coq.0.1:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.14.1, OCaml 4.13.1 :cross_mark: (error :fire:)
- Coq 8.15.0, OCaml 4.14.0 :cross_mark: (error :fire:)
- qcert.2.2.0:
- Coq 8.14.0, OCaml 4.10.2 :cross_mark: (error :fire:)
18735 attempted package installations (including incompatible packages), 12 errors, 0.06% errors
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?
Yes, I am adding it!
(done)
Summary of the past 72 hours:
- gaia-hydras.0.5:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- http.0.1.0:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- mi-cho-coq.0.1:
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- qcert.2.2.0:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- vst-32.2.9:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
10421 attempted package installations (including incompatible packages), 8 errors, 0.08% errors
Summary of the past 72 hours:
- metacoq-translations.1.0~alpha2+8.10:
- Coq 8.10.1, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
12517 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- gaia-hydras.0.5:
- Coq 8.14.1, OCaml 4.09.1 :cross_mark: (error :fire:)
- http.0.1.0:
- Coq 8.14.1, OCaml 4.09.1 :cross_mark: (error :fire:)
- qcert.2.2.0:
- Coq 8.14.1, OCaml 4.09.1 :cross_mark: (error :fire:)
12523 attempted package installations (including incompatible packages), 5 errors, 0.04% errors
Summary of the past 72 hours:
- fiat-crypto.0.0.13:
- Coq 8.15.1, OCaml 4.05.0 :cross_mark: (error :fire:)
- gaia-hydras.0.5:
- Coq 8.13.2, OCaml 4.14.0 :cross_mark: (error :fire:)
- http.0.1.0:
- Coq 8.13.2, OCaml 4.14.0 :cross_mark: (error :fire:)
- Coq 8.15.1, OCaml 4.05.0 :cross_mark: (error :fire:)
10439 attempted package installations (including incompatible packages), 4 errors, 0.04% errors
Summary of the past 72 hours:
- fiat-crypto.0.0.13:
- Coq 8.15.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- http.0.1.0:
- Coq 8.15.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- io-hello-world.1.2.0:
- Coq 8.15.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.3.0:
- Coq 8.15.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.4.1:
- Coq 8.15.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- of-ocaml.1.2.1:
- Coq 8.5.2~camlp4, OCaml 4.05.0 :cross_mark: (error :fire:)
8352 attempted package installations (including incompatible packages), 6 errors, 0.07% errors
Summary of the past 72 hours:
- of-ocaml.1.2.1:
- Coq 8.5.0~camlp4, OCaml 4.05.0 :cross_mark: (error :fire:)
8353 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- of-ocaml.1.2.1:
- Coq 8.5.1, OCaml 4.05.0 :cross_mark: (error :fire:)
10443 attempted package installations (including incompatible packages), 1 error, 0.01% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.0:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.1:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
6267 attempted package installations (including incompatible packages), 6 errors, 0.10% errors
Summary of the past 72 hours:
- of-ocaml.1.1.1:
- Coq 8.4.6~camlp4, OCaml 4.02.3 :cross_mark: (error :fire:)
- of-ocaml.1.2.1:
- Coq 8.10.2, OCaml 4.05.0 :cross_mark: (error :fire:)
10445 attempted package installations (including incompatible packages), 2 errors, 0.02% errors
Summary of the past 72 hours:
- of-ocaml.1.1.1:
- Coq 8.5.0, OCaml 4.02.3 :cross_mark: (error :fire:)
- of-ocaml.1.2.1:
- Coq 8.7.2, OCaml 4.05.0 :cross_mark: (error :fire:)
10451 attempted package installations (including incompatible packages), 2 errors, 0.02% errors
Summary of the past 72 hours:
4196 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
8404 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- of-ocaml.1.2.1:
- Coq 8.12.2, OCaml 4.05.0 :cross_mark: (error :fire:)
6326 attempted package installations (including incompatible packages), 1 error, 0.02% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
- of-ocaml.1.1.1:
- Coq 8.5.3, OCaml 4.02.3 :cross_mark: (error :fire:)
- of-ocaml.1.2.1:
- Coq 8.6, OCaml 4.05.0 :cross_mark: (error :fire:)
10584 attempted package installations (including incompatible packages), 4 errors, 0.04% errors
Summary of the past 72 hours:
- actuary.2.2:
- Coq 8.14.1, OCaml 4.05.0 :cross_mark: (error :fire:)
- actuary.2.3:
- Coq 8.14.1, OCaml 4.05.0 :cross_mark: (error :fire:)
- cfml.20180525:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.7.0, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- gaia-hydras.0.5:
- Coq 8.14.1, OCaml 4.05.0 :cross_mark: (error :fire:)
- http.0.1.0:
- Coq 8.14.1, OCaml 4.05.0 :cross_mark: (error :fire:)
- of-ocaml.1.1.1:
- Coq 8.4.6, OCaml 4.02.3 :cross_mark: (error :fire:)
8480 attempted package installations (including incompatible packages), 7 errors, 0.08% errors
Summary of the past 72 hours:
- actuary.2.2:
- Coq 8.13.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- actuary.2.3:
- Coq 8.13.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- gaia-hydras.0.5:
- Coq 8.13.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- http.0.1.0:
- Coq 8.13.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- infotheo.0.3.7:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- io-hello-world.1.2.0:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.1.0:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.3.0:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- io-system.2.4.1:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (uninstallation error :tornado:️)
- monae.0.4.1:
- Coq 8.14.0, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- of-ocaml.1.1.1:
- Coq 8.4.5, OCaml 4.02.3 :cross_mark: (error :fire:)
- switch.1.0.5:
- Coq 8.14.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- vst-32.2.10:
- Coq 8.13.0, OCaml 4.08.1 :cross_mark: (error :fire:)
- vst.2.10:
- Coq 8.13.0, OCaml 4.08.1 :cross_mark: (error :fire:)
8483 attempted package installations (including incompatible packages), 18 errors, 0.21% errors
Summary of the past 72 hours:
2121 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- Coq 8.7.0, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- Coq 8.7.0, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.0:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.1:
- Coq 8.6.1, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
6370 attempted package installations (including incompatible packages), 6 errors, 0.09% errors
Summary of the past 72 hours:
6378 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- of-ocaml.1.1.1:
- Coq 8.5.1, OCaml 4.02.3 :cross_mark: (error :fire:)
4254 attempted package installations (including incompatible packages), 1 error, 0.02% errors
Summary of the past 72 hours:
- of-ocaml.1.1.1:
- Coq 8.5.0~camlp4, OCaml 4.02.3 :cross_mark: (error :fire:)
4254 attempted package installations (including incompatible packages), 1 error, 0.02% errors
Summary of the past 72 hours:
6384 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- of-ocaml.1.1.1:
- Coq 8.5.2~camlp4, OCaml 4.02.3 :cross_mark: (error :fire:)
6384 attempted package installations (including incompatible packages), 1 error, 0.02% errors
Summary of the past 72 hours:
6390 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
4262 attempted package installations (including incompatible packages), 2 errors, 0.05% errors
Summary of the past 72 hours:
2132 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- of-ocaml.1.1.1:
- Coq 8.5.2, OCaml 4.02.3 :cross_mark: (error :fire:)
6402 attempted package installations (including incompatible packages), 1 error, 0.02% errors
Summary of the past 72 hours:
6411 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
4282 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.0:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
- chick-blog.1.0.1:
- Coq 8.6, OCaml 4.03.0 :cross_mark: (uninstallation error :tornado:️)
2143 attempted package installations (including incompatible packages), 4 errors, 0.19% errors
Summary of the past 72 hours:
- cfml.20180525:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
- cfml.20181201:
- Coq 8.6.1, OCaml 4.04.2 :cross_mark: (uninstallation error :tornado:️)
6430 attempted package installations (including incompatible packages), 2 errors, 0.03% errors
Summary of the past 72 hours:
0 attempted package installations (including incompatible packages), 0 errors, 0.00% errors :check:
Summary of the past 72 hours:
- actuary.2.2:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- actuary.2.3:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- gaia-hydras.0.5:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- http.0.1.0:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- of-ocaml.1.2.1:
- Coq 8.5.3, OCaml 4.05.0 :cross_mark: (error :fire:)
- vlsm.1.1:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- vst-32.2.10:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- vst-zlist.2.11:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
- vst.2.10:
- Coq 8.13.2, OCaml 4.13.1 :cross_mark: (error :fire:)
15008 attempted package installations (including incompatible packages), 9 errors, 0.06% errors
Summary of the past 72 hours:
- actuary.2.2:
- Coq 8.13.1, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- actuary.2.3:
- Coq 8.13.1, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- compcert.3.9:
- Coq 8.13.1, OCaml 4.08.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- gaia-hydras.0.5:
- Coq 8.13.1, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- http.0.1.0:
- Coq 8.13.1, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- infotheo.0.3.7:
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- monae.0.4.2:
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- mtac2.1.4+8.14:
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- of-ocaml.1.2.1:
- Coq 8.5.1, OCaml 4.05.0 :cross_mark: (error :fire:)
- qcert.2.1.1:
- Coq 8.12.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- quickchick.1.6.2:
- Coq 8.14.0, OCaml 4.12.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- vlsm.1.1:
- Coq 8.13.1, OCaml 4.08.1 :cross_mark: (error :fire:)
- Coq 8.14.0, OCaml 4.12.1 :cross_mark: (error :fire:)
- vst-32.2.10:
- Coq 8.12.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.08.1 :cross_mark: (error :fire:)
- vst-zlist.2.11:
- Coq 8.12.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.08.1 :cross_mark: (error :fire:)
- vst.2.10:
- Coq 8.12.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- Coq 8.12.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.08.1 :cross_mark: (error :fire:)
10748 attempted package installations (including incompatible packages), 26 errors, 0.24% errors
Summary of the past 72 hours:
- actuary.2.2:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.14.0 :cross_mark: (error :fire:)
- Coq 8.15.1, OCaml 4.09.1 :cross_mark: (error :fire:)
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- actuary.2.3:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.14.0 :cross_mark: (error :fire:)
- Coq 8.15.1, OCaml 4.09.1 :cross_mark: (error :fire:)
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- async-test.0.1.0:
- Coq 8.16.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- ceres.0.3.0:
- Coq 8.9.0, OCaml 4.03.0 :cross_mark: (error :fire:)
- cfml-stdlib.20220102:
- Coq 8.13.1, OCaml 4.14.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- cfml.20180525:
- Coq 8.7.0, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
- Coq 8.7.2, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- cfml.20181201:
- Coq 8.7.0, OCaml 4.05.0 :cross_mark: (uninstallation error :tornado:️)
- checker.8.9.0:
- Coq 8.7.2, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- compcert-64.3.7~coq-platform:
- Coq 8.10.0, OCaml 4.06.1 :cross_mark: (error :fire:)
- compcert.3.10:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- compcert.3.11:
- Coq 8.15.1, OCaml 4.09.1 :cross_mark: (error :fire:)
- coqeal.1.0.1:
- Coq 8.9.0, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- coqeal.1.0.2:
- Coq 8.9.0, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- coqeal.1.1.0:
- Coq 8.10.0, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.15.1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- coqeal.1.1.1:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- coqprime.1.1.0:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- coqprime.1.1.1:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- coqtail.8.14:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- corn.8.13.0:
- Coq 8.7.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- dijkstra.0.1.0:
- Coq 8.10.0, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- elpi.1.15.1:
- Coq 8.16.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- elpi.1.15.2:
- Coq 8.16.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- elpi.1.15.5:
- Coq 8.16.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- elpi.1.15.6:
- Coq 8.16.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- elpi.1.2.0:
- Coq 8.10.0, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- elpi.1.3.0:
- Coq 8.10.0, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- ext-lib.0.11.5:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- fiat-crypto.0.0.13:
- Coq 8.15.1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.16.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- fourcolor.1.2.1:
- Coq 8.7.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- gaia-hydras.0.5:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.14.0 :cross_mark: (error :fire:)
- gaia-theory-of-sets.1.14:
- Coq 8.15.1, OCaml 4.09.1 :cross_mark: (error :fire:)
- http.0.1.0:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.14.0 :cross_mark: (error :fire:)
- Coq 8.15.1, OCaml 4.09.1 :cross_mark: (error :fire:)
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- infotheo.0.3.7:
- Coq 8.15.1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.4.5.2:
- Coq 8.13.1, OCaml 4.14.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- io-hello-world.1.2.0:
- Coq 8.16.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- io-list.1.0.0:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- io-list.1.1.0:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- io-system.2.4.1:
- Coq 8.16.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- io.4.0.0:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- json.0.1.0:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- libvalidsdp.0.5:
- Coq 8.7.2, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- math-classes.8.9.1:
- Coq 8.7.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-algebra.1.10.0:
- Coq 8.7.2, OCaml 4.04.2 :cross_mark: (error :fire:)
- mathcomp-algebra.1.13.0:
- Coq 8.15.1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-analysis.0.3.13:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-analysis.0.4.0:
- Coq 8.15.1, OCaml 4.09.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.5.0:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.15.1, OCaml 4.09.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.5.1:
- Coq 8.15.1, OCaml 4.09.1 :cross_mark: (error :fire:)
- mathcomp-analysis.0.5.2:
- Coq 8.15.1, OCaml 4.09.1 :cross_mark: (error :fire:)
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- mathcomp-apery.1.0.1:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-character.1.6.2:
- Coq 8.7.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-dioid.0.2:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-field.1.11.0:
- Coq 8.10.0, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-field.1.14.0:
- Coq 8.13.1, OCaml 4.14.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-field.1.9.0:
- Coq 8.7.2, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-multinomials.1.3:
- Coq 8.10.0, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-odd-order.1.7.0:
- Coq 8.7.2, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-real-closed.1.0.3:
- Coq 8.7.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-real-closed.1.0.4:
- Coq 8.9.0, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-solvable.1.9.0:
- Coq 8.9.0, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq-erasure.1.0+8.16:
- Coq 8.16.0, OCaml 4.10.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq.1.0+8.15:
- Coq 8.15.1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- min-imports.1.0.2:
- Coq 8.13.1, OCaml 4.14.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- monae.0.4.1:
- Coq 8.15.1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- of-ocaml.1.2.1:
- Coq 8.7.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- of-ocaml.2.0.0:
- Coq 8.10.0, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- qcert.2.2.0:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- quickchick.1.2.1:
- Coq 8.10.0, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- reduction-effects.0.1.2:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- reduction-effects.0.1.3:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- reduction-effects.0.1.4:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- stalmarck.8.10.0:
- Coq 8.10.0, OCaml 4.06.1 :cross_mark: (error :fire:)
- topology.10.0.1:
- Coq 8.10.0, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- unimath.20210807:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- unimath.20220204:
- Coq 8.16.0, OCaml 4.10.2 :cross_mark: (error :fire:)
- vlsm.1.1:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.14.0 :cross_mark: (error :fire:)
- vst-32.2.10:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.14.0 :cross_mark: (error :fire:)
- vst-32.2.8:
- Coq 8.13.1, OCaml 4.14.0 :cross_mark: (error :fire:)
- vst-32.2.9:
- Coq 8.13.1, OCaml 4.14.0 :cross_mark: (error :fire:)
- vst-zlist.2.11:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.14.0 :cross_mark: (error :fire:)
- vst.2.10:
- Coq 8.13.1, OCaml 4.11.2 :cross_mark: (error :fire:)
- Coq 8.13.1, OCaml 4.14.0 :cross_mark: (error :fire:)
- vst.2.11:
- Coq 8.15.1, OCaml 4.09.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- vst.2.7:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- vst.2.8:
- Coq 8.13.1, OCaml 4.11.2 :large_orange_diamond: (error with dependencies :fire_truck:)
17336 attempted package installations (including incompatible packages), 103 errors, 0.59% errors
Summary of the past 72 hours:
- aac-tactics.8.13.1:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- cfml.20180525:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- cfml.20181201:
- Coq 8.8.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- chick-blog.1.0.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- coinductive-examples.8.9.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- color.1.5.0:
- Coq 8.8.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- compcert-32.3.8:
- Coq 8.8.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- compcert.3.2.0:
- Coq 8.8.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- concurrency-system.1.1.0:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- constructive-geometry.8.7.0:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- corn.8.12.0:
- Coq 8.8.1, OCaml 4.07.1 :cross_mark: (error :fire:)
- corn.8.8.1:
- Coq 8.8.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- dep-map.8.9.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- disel.2.0:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- ext-lib.0.10.1:
- Coq 8.8.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- extensible-records.1.0.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- flocq.3.1.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- gappa.1.2.1:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- geocoq-main.2.4.0:
- Coq 8.8.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- geocoq.2.4.0:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- hammer.1.3+8.10:
- Coq 8.8.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- historical-examples.8.8.0:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- huffman.8.9.0:
- Coq 8.7.1, OCaml 4.06.1 :cross_mark: (error :fire:)
- icharate.8.10.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.3.2.0:
- Coq 8.5.1, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- interval.3.3.0:
- Coq 8.8.0, OCaml 4.05.0 :cross_mark: (error :fire:)
- interval.4.4.0:
- Coq 8.8.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- io-hello-world.1.1.0:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- io-system-ocaml.2.2.0:
- Coq 8.8.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- iris.3.5.0:
- Coq 8.5.1, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- kildall.8.5.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :cross_mark: (error :fire:)
- libvalidsdp.0.5:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.8.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-algebra.1.6.2:
- Coq 8.5.1, OCaml 4.03.0 :cross_mark: (error :fire:)
- mathcomp-analysis.0.1.0:
- Coq 8.8.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-bigenough.1.0.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-character.1.6:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-character.1.6.2:
- Coq 8.5.2~camlp4, OCaml 4.02.3 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-character.1.7.0:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-character.1.8.0:
- Coq 8.7.1, OCaml 4.06.1 :cross_mark: (error :fire:)
- mathcomp-character.1.9.0:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-field.1.11.0:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-field.1.6.4:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-finmap.1.5.2:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-multinomials.1.0:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-multinomials.1.3:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-odd-order.1.10.0:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-odd-order.1.12.0:
- Coq 8.8.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-odd-order.1.6.2:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-real-closed.1.0.1:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- mathcomp-ssreflect.1.12.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- metacoq-safechecker.1.0~alpha1+8.9:
- Coq 8.8.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- mi-cho-coq.0.1:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- min-imports.1.0.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- min-imports.1.0.1:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.8.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- min-imports.1.0.2:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.8.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- of-ocaml.1.1.1:
- Coq 8.5.2~camlp4, OCaml 4.02.3 :cross_mark: (error :fire:)
- of-ocaml.1.2.1:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- opam-website.1.1.0:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- ott.0.30:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- paco.2.0.0:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- paramcoq.1.1.2+coq8.10:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- pi-calc.8.5.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :cross_mark: (error :fire:)
- plouffe.1.2.1:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :cross_mark: (error :fire:)
- ppsimpl.8.8.0:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- ptsatr.8.5.0:
- Coq 8.5.2~camlp4, OCaml 4.02.3 :cross_mark: (error :fire:)
- qarith.8.5.0:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- simple-io.1.4.0:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- smc.8.8.0:
- Coq 8.8.1, OCaml 4.07.1 :cross_mark: (error :fire:)
- stdpp.1.2.1:
- Coq 8.7.1, OCaml 4.06.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- sudoku.8.5.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :cross_mark: (error :fire:)
- sum-of-two-square.8.5.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :cross_mark: (error :fire:)
- type-infer.0.1.0:
- Coq 8.8.0, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.8.1, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- zf.8.10.0:
- Coq 8.5.2~camlp4, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
15244 attempted package installations (including incompatible packages), 79 errors, 0.52% errors
Summary of the past 72 hours:
- aac-tactics.8.10.0:
- Coq 8.5.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- aac-tactics.8.13.0:
- Coq 8.5.2, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- aac-tactics.8.5.0:
- Coq 8.5.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- aac-tactics.8.5.1:
- Coq 8.5.2, OCaml 4.03.0 :cross_mark: (error :fire:)
- Coq 8.5.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- actuary.2.1:
- Coq 8.5.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- actuary.2.2:
- Coq 8.13.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- actuary.2.3:
- Coq 8.13.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- additions.8.5.0:
- Coq 8.5.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- amm11262.8.10.0:
- Coq 8.5.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- atbr.8.5.0:
- Coq 8.5.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- automata.8.5.0:
- Coq 8.13.0, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- bdds.8.5.0:
- Coq 8.5.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- bdds.8.9.0:
- Coq 8.5.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- bedrock2.0.0.1:
- Coq 8.5.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- bits.1.0.0:
- Coq 8.9.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- buchberger.8.11.0:
- Coq 8.10.2, OCaml 4.09.1 :cross_mark: (error :fire:)
- buchberger.8.7.0:
- Coq 8.13.0, OCaml 4.07.1 :large_orange_diamond: (error with dependencies :fire_truck:)
- buchberger.8.8.0:
- Coq 8.8.2, OCaml 4.02.3 :cross_mark: (error :fire:)
- bytestring.0.9.0:
- Coq 8.5.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- Coq 8.9.1, OCaml 4.04.2 :large_orange_diamond: (error with dependencies :fire_truck:)
- canon-bdds.8.5.0:
- Coq 8.5.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- cfgv.8.10.0:
- Coq 8.5.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- charge-core.1.0.1:
- Coq 8.5.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- chinese.8.5.0:
- Coq 8.5.2, OCaml 4.05.0 :cross_mark: (error :fire:)
- coalgebras.8.5.0:
- Coq 8.8.2, OCaml 4.02.3 :large_orange_diamond: (error with dependencies :fire_truck:)
- coinduction.1.2:
- Coq 8.5.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- color.1.8.1:
- Coq 8.13.0, OCaml 4.07.1 :cross_mark: (error :fire:)
- color.1.8.2:
- Coq 8.5.2, OCaml 4.03.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- compcert.2.7.1:
- Coq 8.5.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- compcert.3.0.0:
- Coq 8.5.2, OCaml 4.03.0 :cross_mark: (error :fire:)
- Coq 8.5.2, OCaml 4.05.0 :large_orange_diamond: (error with dependencies :fire_truck:)
- compcert.3.5:
- Coq 8.9.1, OCaml 4.04.2 :cross_mark: (error :fire:)
- concurrency-pluto.1.0.0:
- Coq 8.5.2, O