Stream: Elpi users & devs

Topic: coq-elpi on coq.dev again

view this post on Zulip Karl Palmskog (May 13 2022 at 12:50):

So it seems there are coq-elpi issues again on coq.dev:

# CAMLC -c src/coq_elpi_utils.mli
  # CAMLC -c src/coq_elpi_HOAS.mli
  # File "src/coq_elpi_HOAS.mli", line 100, characters 62-86:
  # Error: Unbound module ComInductive.Mind_decl
  # make[2]: *** [Makefile.coq:725: src/coq_elpi_HOAS.cmi] Error 2
  # make[1]: *** [Makefile:50: build-core] Error 2
  # make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-elpi.dev'
  # make: *** [Makefile:42: all] Error 2

See for example this build. Is this known, or can one do something?

view this post on Zulip Karl Palmskog (May 13 2022 at 12:52):

hmm, I'm confused about the OCaml version here... could that be the issue? the mathcomp-dev:coq-dev Docker image is not up to date, and some old Coq master is used?

Last updated: Feb 05 2023 at 13:02 UTC