Karl Palmskog (Oct 18 2021 at 10:18): Karl Palmskog (Oct 18 2021 at 10:18):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 mathcomp-dev)
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
Erik Martin-Dorel (Oct 18 2021 at 10:40):Thanks @Karl Palmskog but it seems it's not the issue you believe:
the image 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
Karl Palmskog (Oct 18 2021 at 10:42):oh OK, thanks for catching that!
Erik Martin-Dorel (Oct 18 2021 at 10:57):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.
Karl Palmskog (Oct 18 2021 at 15:45):@Erik Martin-Dorel whoops, I think I wasn't supposed to merge the archive PR yet? Should we revert the commit?
Erik Martin-Dorel (Oct 18 2021 at 18:18):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: Oct 13 2024 at 01:02 UTC