Stream: Elpi users & devs

Topic: coq-elpi fails to build on coqorg/coq:dev docker image


view this post on Zulip Christian Doczkal (Nov 30 2020 at 15:15):

As the title says, I'm getting build failures trying to install coq-elpi on the coqorg:coq:dev docker image, breaking CI on one of my projects which is using hierachy-builder.

#=== ERROR while compiling coq-elpi.dev =======================================#
# context              2.0.7 | linux/x86_64 | ocaml-base-compiler.4.05.0 | https://coq.inria.fr/opam/extra-dev#2020-11-30 04:30
[...]
# File "src/coq_elpi_vernacular.ml", line 51, characters 6-15:
# Error: Unbound value EC.extend

view this post on Zulip Enrico Tassi (Nov 30 2020 at 15:18):

the docker image is using a version of elpi which is too old

view this post on Zulip Enrico Tassi (Nov 30 2020 at 15:18):

pick 1.12.0

view this post on Zulip Enrico Tassi (Nov 30 2020 at 15:18):

(not coq-elpi, really elpi)

view this post on Zulip Enrico Tassi (Nov 30 2020 at 15:19):

I don't know where to signalfix this

view this post on Zulip Christian Doczkal (Nov 30 2020 at 15:31):

This is weird, on the dev image I indeed get:

   - install elpi                    1.10.2
    - install coq-elpi                dev
    - install coq-hierarchy-builder   dev

According to what I see in the version constraints in the coq-elpi repository, this violates the version constraint in coq-elpi.opam. :confused:

view this post on Zulip Christian Doczkal (Nov 30 2020 at 15:33):

Is there anyone other than @Erik Martin-Dorel who might know what's going on with the docker image?

view this post on Zulip Enrico Tassi (Nov 30 2020 at 15:37):

I did fix the one we use in the CI of Coq (it installs elpi via opam, easy). But I've no idea where that one comes from (where the dockerfile is).

view this post on Zulip Christian Doczkal (Nov 30 2020 at 15:39):

That's the thing: the coqorg/coq:dev image has no elpi installed and it tries to install it vial opam. I don't see how it can pick elpi-10.2.

view this post on Zulip Christian Doczkal (Nov 30 2020 at 15:42):

I mean, here is the log: https://github.com/coq-community/graph-theory/pull/6/checks?check_run_id=1474475472

view this post on Zulip Enrico Tassi (Nov 30 2020 at 15:45):

This file was recently updated (maybe friday) https://github.com/LPCIC/coq-elpi/blob/coq-master/coq-elpi.opam
dunno how often it's regenerated

view this post on Zulip Christian Doczkal (Nov 30 2020 at 15:51):

Generated where? The log says:

 [coq-elpi.dev] synchronised from git+https://github.com/LPCIC/coq-elpi.git#coq-master

I thought the .dev packages would result in direct clones.


Last updated: Mar 28 2024 at 18:02 UTC