Conversation
|
@erikmd @hoheinzollern @CohenCyril apparently we don't have the Docker images for 2.4.0, did something went wrong during the release process? |
|
@erikmd @hoheinzollern some progress but we still get |
|
Normally this is |
|
OK I saw the issue, the PR I had approved too-quickly mentioned 9.00 instead of 9.0, will fix this. |
|
FYI @proux01, you'll need to wait that this issue is closed: math-comp/docker-mathcomp#35 (See also this comment for more details: math-comp/docker-mathcomp#35 (comment) ) |
|
Thanks, didn't notice that, no hurry |
This comment was marked as outdated.
This comment was marked as outdated.
|
FYI @proux01 :
|
Maybe HB 1.9.1 is not compatible with Coq 8.19? In which case we should update the opam package? |
Certainly, I was thinking about this kind of issue BTW comparing the failing build https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/5694374 Cc @gares according to the CI of hierarchical-builder, |
|
Strange, I'm not able to reproduce locally, on my 8.19 switch |
|
@erikmd that being said, the Docker CI of HB seems completely broken: https://github.com/math-comp/hierarchy-builder/actions/runs/14796943582/job/41546267124 Maybe the images should pin coq-core/rocq-runtime rather than coq? |
|
Thanks for the feedback, BTW it'd be good to understand why, using almost the same versions (in your local switch and in the docker-mathcomp job), HB 1.9.1 fails to build from source saying |
Which difference did you spot? The versions of elpi and coq-elpi seem to be the same |
|
Sorry for my vague wording: yes there are no differences, so I'm puzzled that Coq did not find the elpi namespace at that point. |
|
Meanwhile, despite the full-blown renaming, docker-coq only pins the coq package, but maybe it'd be safer to also pin these core dependencies! So meanwhile, even if I don't have an immediate answer to the question I asked in my previous comment, I propose to: |
|
Apparently yes, they need to be pinned. I guess the issue didn't manifest until recently due to the coq-core package being virtually useless and everybody actually depending on coq? |
|
yes, this pinning is certainly necessary! as https://github.com/LPCIC/coq-elpi/blob/master/coq-elpi.opam doesn't depend on coq, but on coq-core… so if only coq is pinned (not coq-core), bad things happen! ❌ ; Thanks again, Pierre! |
This patch happens to be necessary for coq/opam projects that depend on coq-core (for example), and not on coq directly. See-also: rocq-community/gaia#27 (comment)
This patch happens to be necessary for rocq/opam projects that depend on rocq-core (for example), and not on rocq-prover directly. See-also: rocq-community/gaia#27 (comment)
This patch happens to be necessary for coq/opam projects that depend on coq-core (for example), and not on coq directly. See-also: rocq-community/gaia#27 (comment)
|
Not there yet :( |
|
Hi @proux01, I believe all the required building blocks for supporting Coq+Rocq with mathcomp stable and dev are now OK. And, thanks for your patience - it took a bit of time just because, as we may have expected, the prover's renaming have had a non-trivial impact on the whole infrastructure. |
|
No, I guess we de-facto gave up |
|
@pi8027 Nope, I'm really sorry for the delay… this is something I definitely want to look at and fix! it just happens it's the end of the teaching semester, and I've been swamped with exams' grading :-| so I'll try to look at this closely this week (ideally on Thursday)… stay tuned 👍 |
|
@erikmd Don't worry. I was just wondering whether I should remove it from a CI config for the moment, and it's not a critical issue for me. Thanks a lot for your work in any case! |
3 participants
Adding Rocq 9.0 and MC 2.4