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: May 19 2024 at 16:02 UTC