Stream: Elpi users & devs

Topic: Compilation of coq-elpi on Coq master


view this post on Zulip Karl Palmskog (Jan 08 2023 at 15:50):

coq-elpi.dev is seemingly broken with some versions of OCaml/packages:

# CAMLC -c src/coq_elpi_builtins.mli
# CAMLC -c src/coq_elpi_vernacular.ml
# CAMLC -c src/coq_elpi_utils.ml
# CAMLC -c src/coq_elpi_HOAS.ml
# File "src/coq_elpi_HOAS.ml", line 176, characters 6-17:
# 176 |     | Sorts.QSort _ -> Format.fprintf fmt "Type");
#             ^^^^^^^^^^^
# Error: Unbound constructor Sorts.QSort

Some dependency issue?

view this post on Zulip Karl Palmskog (Jan 08 2023 at 16:24):

happens on OCaml 4.14.0 and 5.0.0, but not 4.11.1.

view this post on Zulip Enrico Tassi (Jan 09 2023 at 20:22):

I was late merging an overlay PR, it should be fine now

view this post on Zulip Karl Palmskog (Jan 18 2023 at 09:00):

I'm guessing this is also due to pending overlay:

  # CAMLC -c src/coq_elpi_utils.ml
  # File "src/coq_elpi_utils.ml", line 226, characters 42-60:
  # 226 |     options (Detyping.detype Detyping.Now Names.Id.Set.empty env sigma) t in
  #                                                 ^^^^^^^^^^^^^^^^^^
  # Error: This expression has type Names.Id.Set.t
  #        but an expression was expected of type bool

view this post on Zulip Enrico Tassi (Jan 18 2023 at 19:16):

I think I've merged the overlay for that one already: https://github.com/LPCIC/coq-elpi/pull/425#event-8240961694
Can you please retry?

view this post on Zulip Karl Palmskog (Jan 18 2023 at 19:35):

works now, thanks


Last updated: May 24 2024 at 22:02 UTC