Stream: Elpi users & devs

Topic: coq-elpi dev failing

view this post on Zulip Karl Palmskog (Aug 07 2023 at 07:42):

We are seeing a bunch of failed Docker jobs for mathcomp-dev image due to some issue with coq-elpi.dev:

-> installed elpi.1.16.10
  Error:  The compilation of coq-elpi.dev failed at "make COQBIN=/home/coq/.opam/4.13.1+flambda/bin/ ELPIDIR=/home/coq/.opam/4.13.1+flambda/lib/elpi OCAMLWARN=".

  #=== ERROR while compiling coq-elpi.dev =======================================#
  # context              2.1.3 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.13.1+options | https://coq.inria.fr/opam/extra-dev#2023-08-06 15:50
  # path                 ~/.opam/4.13.1+flambda/.opam-switch/build/coq-elpi.dev
  # command              /usr/bin/make COQBIN=/home/coq/.opam/4.13.1+flambda/bin/ ELPIDIR=/home/coq/.opam/4.13.1+flambda/lib/elpi OCAMLWARN=
  # exit-code            2
  # env-file             ~/.opam/log/coq-elpi-974-04ae6c.env
  # output-file          ~/.opam/log/coq-elpi-974-04ae6c.out
  ### output ###
  # Error: This expression has type
  # [...]
  #          list
  #        Type
  #          (Constrexpr.notation_entry_relative_level * ('a list * 'b list)) *
  #          Names.Id.Set.t * Notation_term.notation_var_instance_type
  #        is not compatible with type
  #          Notation_term.extended_subscopes *
  #          Notation_term.notation_var_instance_type
  # make[2]: *** [Makefile.coq:752: src/coq_elpi_builtins.cmo] Error 2
  # make[1]: *** [Makefile:50: build-core] Error 2
  # make[1]: Leaving directory '/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-elpi.dev'
  # make: *** [Makefile:42: all] Error 2

Is this something that is transient (hopefully) or does some PR need to be merged?

Example failing job: https://github.com/coq-community/fourcolor/actions/runs/5781258981/job/15666113549

view this post on Zulip Enrico Tassi (Aug 07 2023 at 09:01):

Seems so, but I don't see the overlay pr.
I'll lake a look after lunch.

view this post on Zulip Karl Palmskog (Feb 16 2024 at 08:51):

so builds with the mathcomp-dev Docker image are failing left and right, with the coq-elpi.dev opam package seemingly being the culprit:

  # File "src/coq_elpi_coercion_hook.mlg", line 16, characters 6-19:
  # Error: Unbound constructor Coercion.Type
  # make[3]: *** [Makefile.coq:765: src/coq_elpi_coercion_hook.cmx] Error 2
  # make[2]: *** [Makefile.coq:417: all] Error 2
  # make[1]: *** [Makefile:15: build] Error 2
  # make[1]: Leaving directory '/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-elpi.dev/apps/coercion'
  # make: *** [Makefile:57: build-apps] Error 2

See an example failing build here. What can be done to fix?

view this post on Zulip Gaëtan Gilbert (Feb 16 2024 at 09:10):

I guess the docker image did not yet get the coq commit for https://github.com/coq/coq/pull/18236

view this post on Zulip Karl Palmskog (Feb 16 2024 at 09:12):

oh, so there was a breaking change. Let's see if the error persists tomorrow then, before we do anything.

Last updated: Oct 13 2024 at 01:02 UTC