Compilation of coq-elpi on Coq master · Elpi users & devs

Stream: Elpi users & devs

Topic: Compilation of coq-elpi on Coq master

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?

Karl Palmskog (Jan 08 2023 at 16:24):

happens on OCaml 4.14.0 and 5.0.0, but not 4.11.1.

Enrico Tassi (Jan 09 2023 at 20:22):

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

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

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?

Karl Palmskog (Jan 18 2023 at 19:35):

works now, thanks

Cyril Cohen (Aug 14 2024 at 09:03):

Hi @Enrico Tassi which version of coq-elpi is supposed to compile with coq's master nowadays? I just tried to use the master branch too and it did not work:

Error: This expression has type
         (string option *
          ([> `After | `Before | `Replace ] * string) option *
          Elpi.API.Data.term)
         list
       but an expression was expected of type
         (string option * ([ `After | `Before ] * string) option *
          Elpi.API.Data.term)
         list
       The second variant type does not allow tag(s) `Replace

Would you have a drop in replacement?

Pierre Roux (Aug 14 2024 at 09:22):

It's indeed the master branch, but requires some version of elpi (1.19.4 works here).

Pierre Roux (Aug 14 2024 at 09:23):

The error looks like your elpi is too old.

Cyril Cohen (Aug 14 2024 at 09:31):

Thanks for the fast diagnosis

Last updated: Oct 13 2024 at 01:02 UTC