feat: Take advantage of the coq-native package (CEP 048, item 3) #1835
Conversation
* href: https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#regarding-item-3 * Only update coq-mathcomp-multinomials.dev's deps and mathcomp.1.12.0 (some similar PRs could be opened for other deps if need be).
* can be reverted anytime after the merge of coq/opam#1835 and the rebuild of `mathcomp/mathcomp:1.12.0-coq-8.12`
* For details, see: - https://opam.ocaml.org/packages/coq-native/ - CEP 48 <https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#note-to-library-developers-and-package-maintainers> * can be reverted anytime after the merge of coq/opam#1835 and the rebuild of `mathcomp/mathcomp:1.12.0-coq-8.12`
|
FTR, even if the two main jobs timed out: 4.05.0, 4.11.2, it can be noted that the compilation did not raise any failure, see e.g.: So I guess that the PR could be merged as is? Anyway, let me know if you need more tests (maybe on a longer pipeline I'd run on a fork…), or if you'd like that #1504 is finalized beforehand. Actually AFAICT, the tests that were run in this pipeline already confirm that adding the predicate |
|
This pull request is fine with me. Unless @gares objects, I will merge it. |
|
I'm fine with it. Note that you can re-run CI skipping previously checked packages, see https://github.com/coq/opam-coq-archive#continuous-integration |
|
I did re-run it with a larger timeout, see https://gitlab.com/coq/opam-coq-archive/-/pipelines/386997682 . It should suffice. |
|
Dear @coq/ci-maintainers it seems pyrolise is no more available to opam-coq-archive. It is listed as a new runner, which did not connect yet, and is locked which I don't know what that means. Can you shed some light? |
|
I talked about this during a recent Coq Call: https://github.com/coq/coq/wiki/Coq-Call-2021-09-08 |
|
Just FTR (to illustrate the impact of this PR, using the opam pinned from the dev version of coq-mathcomp-multinomials), … coq 8.12.0 pinned to version 8.12.0 coq-bignums 8.12.0 Bignums, the Coq library of arbitrary large numbers coq-mathcomp-algebra 1.12.0 Mathematical Components Library on Algebra coq-mathcomp-bigenough 1.0.0 A small library to do epsilon - N reasonning coq-mathcomp-fingroup 1.12.0 Mathematical Components Library on finite groups coq-mathcomp-finmap 1.5.1 Finite sets, finite maps, finitely supported functions coq-mathcomp-multinomials 1.5.4 pinned to version 1.5.4 at git+https://github.com/math-comp/multi coq-mathcomp-ssreflect 1.12.0 Small Scale Reflection coq-native 1 Package flag enabling coq's native-compiler flag cppo 1.6.6 Code preprocessor like cpp for OCaml csexp 1.3.2 Parsing and printing of S-expressions in Canonical form dot-merlin-reader 3.4.1 Reads config files for merlin dune 2.8.0 Fast, portable, and opinionated build system easy-format 1.3.2 High-level and functional interface to the Format module of the O merlin 3.4.1 Editor helper, provides completion, typing and source browsing in … and to check this I've just did a local test: (Cc @proux01 FYI) |
|
It seems we did get some kind of consensus to merge in spite of CI issues, so therefore I will merge. |
|
It looks that this breaks several CIs relying on
CC @thery @erikmd |
|
Given the log, it seems like you are not compiling SSReflect but using a precompiled one (from before this pull request). It will keep failing until this precompiled SSReflect is recompiled. |
It's the one from docker... so you're saying I just need to rebuild the docker image? |
|
Yes, whoever is the maintainer of the Docker images you are using in your continuous integration should rebuild them (after disabling the cache). |
|
Indeed, that's exactly what @silene said: it's not a bug but an expected failure to be solved by recompiling these mathcomp stable images since this PR was merged yesterday (sorry for not doing this earlier today). |
|
Just FTR @CohenCyril, I did this by following this doc https://gitlab.com/erikmd/docker-keeper/-/wikis/home#how-to-trigger-builds |
|
BTW it seems this line should be removed: |
|
Thanks @erikmd !! |
* Follow-up of math-comp@52988b6 * Now possible after the merge of coq/opam#1835
* Follow-up of 52988b6 * Now possible after the merge of coq/opam#1835
* Follow-up of PR coq#1835
* For details, see: - https://opam.ocaml.org/packages/coq-native/ - CEP 48 <https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#note-to-library-developers-and-package-maintainers> * can be reverted anytime after the merge of coq/opam#1835 and the rebuild of `mathcomp/mathcomp:1.12.0-coq-8.12`
* Follow-up of math-comp@52988b6 * Now possible after the merge of coq/opam#1835
href: https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#regarding-item-3
Only update coq-mathcomp-multinomials.dev's deps and mathcomp.1.12.0
(some similar PRs could be opened for other deps if need be).
Cc @proux01 @CohenCyril @strub