Stream: math-comp devs

Topic: MathComp dev opam and Docker breaking


view this post on Zulip Karl Palmskog (Dec 31 2023 at 09:48):

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

view this post on Zulip Enrico Tassi (Dec 31 2023 at 11:01):

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

view this post on Zulip Enrico Tassi (Dec 31 2023 at 11:03):

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

view this post on Zulip Karl Palmskog (Dec 31 2023 at 11:40):

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

view this post on Zulip Enrico Tassi (Dec 31 2023 at 12:22):

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

view this post on Zulip Karl Palmskog (Dec 31 2023 at 12:27):

I built coq.dev via opam yesterday

view this post on Zulip Karl Palmskog (Dec 31 2023 at 12:28):

$ opam upgrade coq-core

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-core.dev] synchronised (no changes)

Already up-to-date.
Nothing to do.

view this post on Zulip Karl Palmskog (Dec 31 2023 at 12:30):

I have elpi.1.18.1 installed

view this post on Zulip Karl Palmskog (Dec 31 2023 at 12:31):

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...

view this post on Zulip Enrico Tassi (Dec 31 2023 at 14:23):

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

view this post on Zulip Enrico Tassi (Dec 31 2023 at 14:25):

I'll make a fix

view this post on Zulip Enrico Tassi (Dec 31 2023 at 14:55):

should work now

view this post on Zulip Karl Palmskog (Dec 31 2023 at 15:01):

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

view this post on Zulip Karl Palmskog (Dec 31 2023 at 17:08):

@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