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
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
I should be fixed now, but I guess you need docker images to be regenerated which may take one day
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
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
The next time you hear me saying that "fatal warnings" is stupid, you know why
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
.
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.
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
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.
https://github.com/coq/coq/pull/14075
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?
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.
I think it is up to you. How many times did the CI job for coq master gave you valuable feedback?
Last updated: Oct 13 2024 at 01:02 UTC