Recall the problem with out-of-date Docker images from this issue:
# File "./src/./NSsrMultinomials_xfinmap.native", line 14, characters 14-108: # Error: Unbound module Nmathcomp_bigenough_bigenough # Error: Native compiler exited with status 2
I'm now having these errors for another
mathcomp-dev Docker image: https://github.com/coq-community/coqeal/pull/52/checks?check_run_id=3925271236 (for 8.12,
coq-8.12 tag in
Could I maybe get some help to rebuild this image? The instructions are in the issue above, but to my knowledge I don't have the access right.
@Erik Martin-Dorel @Cyril Cohen
Thanks @Karl Palmskog but it seems it's not the issue you believe:
mathcomp/mathcomp-dev:coq-8.12 has been automatically rebuilt 17h ago (with the last merge in math-comp), cf. https://hub.docker.com/r/mathcomp/mathcomp-dev/tags ; the issue is that the PR I had opened to fix coq-native support only updated coq/released, not extra-dev (nor mathcomp-dev). I'll try to open two PRs ASAP
oh OK, thanks for catching that!
I opened the two PRs that should solve this:
BTW @Cyril Cohen, PR 1. should be merged first (maybe PR 2. should be closed/reopened to restart the CI that could have failed meanwhile), then the merge of PR 2. will be enough so that the mathcomp-dev images are rebuilt.
@Erik Martin-Dorel whoops, I think I wasn't supposed to merge the archive PR yet? Should we revert the commit?
Hi @Karl Palmskog, no worries! there were absolutely no constraint on the time of merging the archive PR.
I was just saying that the math-comp one had to be merged afterwards. So that's fine.
Last updated: Dec 07 2023 at 06:38 UTC