Stream: math-comp devs

Topic: question on coq-elpi.coq-master + coq.master


view this post on Zulip Erik Martin-Dorel (Sep 05 2023 at 18:17):

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

view this post on Zulip Pierre Roux (Sep 05 2023 at 19:06):

Looks like this is not building on an up to date Coq, can you try to rebuild the "base" Docker image with Coq itself?

view this post on Zulip Erik Martin-Dorel (Sep 06 2023 at 12:42):

Good point!

See this comment by Théo:

https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/docker.20image.20MIA/near/389373181

So, the mathcomp GitLab CI pipeline is green anew :check:

view this post on Zulip Erik Martin-Dorel (Sep 06 2023 at 12:43):

Anyway, it is always possible to inspect a docker-coq or docker-mathcomp image without pulling it:

see this other comment of mine:

https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/docker.20image.20MIA/near/389410978

view this post on Zulip Pierre Roux (Sep 06 2023 at 12:46):

Nice (although I'm afraid I'll likely have forgotten that by the time I need it again)

view this post on Zulip Erik Martin-Dorel (Sep 06 2023 at 12:54):

Yes… I'm going to add it in the Docker-Coq wiki.

view this post on Zulip Erik Martin-Dorel (Sep 06 2023 at 13:11):

Done: https://github.com/coq-community/docker-coq/wiki#how-to-inspect-a-tag


Last updated: Jun 18 2024 at 00:02 UTC