Christian Doczkal (Apr 14 2021 at 06:56): Christian Doczkal (Apr 14 2021 at 06:56):It appears that coq-elpi.dev no longer builds against coq.dev. This breaks the CI for coq-graph-theory: https://github.com/coq-community/graph-theory/actions/runs/747187030 :
# File "src/coq_elpi_HOAS.ml", line 643, characters 33-112:
# Error: This expression has type
# (string Elpi.Builtin.unspec * string Elpi.Builtin.unspec) option
# but an expression was expected of type
# (string unspec * string unspec) option
# Type string Elpi.Builtin.unspec is not compatible with type
# string unspec
thanks for reporting, I'll fix it
Enrico Tassi (Apr 14 2021 at 07:14):Yesterday I've released elpi and coq-elpi, today I'll update the dev packages, but they point to branches also used by Coq, so I need to update Coq's docker as well https://github.com/coq/coq/pull/14111 , so it may take a day or two
Enrico Tassi (Apr 15 2021 at 08:10):I should be fixed now, but I guess you need docker images to be regenerated which may take one day
Christian Doczkal (Apr 22 2021 at 08:31):Here is another build failure:
# File "src/coq_elpi_glob_quotation.ml", line 92, characters 2-9771:
# Error (warning 8): this pattern-matching is not exhaustive.
# Here is an example of a case that is not matched:
# GCast (_, CastCoerce)
see: https://github.com/coq-community/graph-theory/runs/2402024928?check_suite_focus=true
Enrico Tassi (Apr 22 2021 at 08:55):There was a PR merged yesterday on Coq which had an overlay in elpi. IMO the docker image did not regenerate yet. But this also makes me think the .dev package of elpi does not have this fix applied:
-build: [ make "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
+build: [ make "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" "OCAMLWARN=" ]
done https://github.com/coq/opam-coq-archive/pull/1695
Enrico Tassi (Apr 22 2021 at 08:58):The next time you hear me saying that "fatal warnings" is stupid, you know why
Christian Doczkal (Apr 22 2021 at 10:18):Well, one can argue about fatal warning in ones own CI, but it's not something that should be enabled when shipping code to clients.
As for the dev package of elpi, I don't think that's of much concern to Coq users, as even coq-elpi.dev depends on a stable version of elpi.
Christian Doczkal (Apr 22 2021 at 10:22):Enrico Tassi said:
There was a PR merged yesterday on Coq which had an overlay in elpi. IMO the docker image did not regenerate yet.
Oh, I just noticed that this CI failure was from yesterday evening, while my nightly at 5am was indeed working. So the image had already been rebuilt. In any event, your fix seems reasonable nonetheless.
Christian Doczkal (Apr 24 2021 at 11:57):And give us today our nightly coq-elpi.dev build failure:
# File "src/coq_elpi_vernacular_syntax.mlg", line 70, characters 49-58:
# Error: This expression has type 'a -> Tok.t Stream.t -> unit
# but an expression was expected of type 'b Pcoq.Entry.parser_fun
https://github.com/coq-community/graph-theory/runs/2425370422?check_suite_focus=true
Enrico Tassi (Apr 24 2021 at 12:35):Same problem, I merge the pr fixing the compat with coq CI as soon as the pr is merged in coq. Until docker picks up the commit in coq you get this.
Enrico Tassi (Apr 24 2021 at 12:36):https://github.com/coq/coq/pull/14075
Christian Doczkal (Apr 24 2021 at 14:02):Do you have any suggestions, other than moving from the mathcomp-dev/coq-dev image to the mathcomp-dev/coq-8.13 image and not testing development versions of Coq and HB?
Enrico Tassi (Apr 25 2021 at 07:54):As we do CI in coq, there are races. Even if you switch to nix which is not cached by a Cron, you still have a race.
Enrico Tassi (Apr 25 2021 at 07:55):I think it is up to you. How many times did the CI job for coq master gave you valuable feedback?
Last updated: Apr 18 2024 at 07:02 UTC