Stream: math-comp devs

Topic: Trigger rebuilds of mathcomp-dev Docker images


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Oct 18 2021 at 10:42):

oh OK, thanks for catching that!

view this post on Zulip Erik Martin-Dorel (Oct 18 2021 at 10:57):

I opened the two PRs that should solve this:

  1. https://github.com/coq/opam-coq-archive/pull/1869
  2. https://github.com/math-comp/math-comp/pull/804

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.

view this post on Zulip 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?

view this post on Zulip 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: Aug 11 2022 at 01:03 UTC