after recent changes to Elpi/Coq-Elpi, MathComp dev opam packages and Dockers can no longer be built (example).

This is probably related to changes referenced in https://github.com/coq/coq/pull/18437

It is probably a bad dependency in coq-elpi.dev

Yes, it should require elpi >= 1.18.1, not < 1.18.0

I installed the latest `elpi`

via opam, then I did this:

```
$ opam install coq-elpi.dev --ignore-constraints-on=elpi
The following actions will be performed:
∗ install coq-elpi dev
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved coq-elpi.dev (git+https://github.com/LPCIC/coq-elpi.git#coq-master)
#=== ERROR while compiling coq-elpi.dev =======================================#
# context 2.1.4 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.5.1.0+options | https://coq.inria.fr/opam/extra-dev#2023-12-29 19:52
# path ~/.opam/5.1.0+flambda+coq.dev/.opam-switch/build/coq-elpi.dev
# command ~/.opam/opam-init/hooks/sandbox.sh build make build COQBIN=/home/palmskog/.opam/5.1.0+flambda+coq.dev/bin/ ELPIDIR=/home/palmskog/.opam/5.1.0+flambda+coq.dev/lib/elpi OCAMLWARN=
# exit-code 2
# env-file ~/.opam/log/coq-elpi-908718-65fc27.env
# output-file ~/.opam/log/coq-elpi-908718-65fc27.out
### output ###
# [...]
# CAMLC -c src/coq_elpi_utils.ml
# CAMLC -c src/coq_elpi_HOAS.ml
# CAMLC -c src/coq_elpi_name_quotation.ml
# CAMLC -c src/coq_elpi_glob_quotation.ml
# CAMLC -c src/coq_elpi_arg_HOAS.ml
# File "src/coq_elpi_arg_HOAS.ml", line 49, characters 6-34:
# 49 | | CLocalAssum(nl,Default bk,_) -> nl |> List.map (fun n -> n.CAst.v,bk,None,mkGHole)
# ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
# Error: The constructor CLocalAssum expects 4 argument(s),
# but is applied here to 3 argument(s)
# make[1]: *** [Makefile.coq:760: src/coq_elpi_arg_HOAS.cmo] Error 2
# make: *** [Makefile:50: build-core] Error 2
```

That is a mismatch with coq, which version did you get?

I built `coq.dev`

via opam yesterday

```
$ opam upgrade coq-core
<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-core.dev] synchronised (no changes)
Already up-to-date.
Nothing to do.
```

I have `elpi.1.18.1`

installed

I can update the `coq-elpi.dev`

opam package, but we need to confirm it's possible to get a fully working build of MathComp dev and friends...

I guess there was a race condition with https://github.com/LPCIC/coq-elpi/pull/563

I'll make a fix

should work now

can confirm locally, I submitted https://github.com/coq/opam/pull/2885

@Erik Martin-Dorel sorry for untimely ping, but when you have time, can you trigger a rebuild of the MathComp `dev`

Docker image(s)? Note that OCaml 4.10.0 and later and `elpi.1.18.1`

are now required for `coq-elpi.dev`

...

Last updated: Jul 23 2024 at 20:01 UTC