Stream: Elpi users & devs

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

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

Enrico Tassi (Nov 30 2020 at 15:18):

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

Enrico Tassi (Nov 30 2020 at 15:18):

pick 1.12.0

Enrico Tassi (Nov 30 2020 at 15:18):

(not coq-elpi, really elpi)

Enrico Tassi (Nov 30 2020 at 15:19):

I don't know where to signalfix this

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:

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?

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

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.

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

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

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: Oct 13 2024 at 01:02 UTC