FYI math-comp's GitLab CI goes live fully anew, i.e. each PR is checked using coq-{8.16,8.17,8.18,dev}.
However the coq-dev now fails, blocking any docker-mathcomp deploy from the master branch of math-comp:
https://gitlab.inria.fr/math-comp/math-comp/-/jobs/3393876
#8 268.3 # File "src/coq_elpi_builtins.ml", line 2887, characters 65-92:
#8 268.3 # 2887 | Hints.add_hints ~locality [db] Hints.(Hints.HintsResolveEntry[info, true, hint_globref gr]);
#8 268.3 # ^^^^^^^^^^^^^^^^^^^^^^^^^^^
#8 268.3 # Error: This expression has type 'a * 'b * 'c
#8 268.3 # but an expression was expected of type
#8 268.3 # Typeclasses.hint_info * Hints.hnf * Hints.hints_path_atom *
#8 268.3 # Hints.hint_term
#8 268.3 # make[1]: *** [Makefile.coq:752: src/coq_elpi_builtins.cmo] Error 2
#8 268.3 # make: *** [Makefile:50: build-core] Error 2
I saw a related overlay was merged in coq-elpi:
https://github.com/LPCIC/coq-elpi/pull/494/files
but it does not seem enough.
Ideas to fix this upstream? Cc @Enrico Tassi @Pierre Roux @Cyril Cohen
Looks like this is not building on an up to date Coq, can you try to rebuild the "base" Docker image with Coq itself?
Good point!
See this comment by Théo:
So, the mathcomp GitLab CI pipeline is green anew :check:
Anyway, it is always possible to inspect a docker-coq or docker-mathcomp image without pulling it:
see this other comment of mine:
Nice (although I'm afraid I'll likely have forgotten that by the time I need it again)
Yes… I'm going to add it in the Docker-Coq wiki.
Done: https://github.com/coq-community/docker-coq/wiki#how-to-inspect-a-tag
Last updated: Oct 13 2024 at 01:02 UTC