Stream: Elpi users & devs

Topic: Assertion failed on calling coq.term->string in coq_elpi_HOA

Luko van der Maas (Jan 24 2024 at 16:14):

I am getting the following error: Anomaly "File "src/coq_elpi_HOAS.ml", line 1299, characters 12-18: Assertion failed." on the newest coq-elpi from master. I am wondering when this would happen. It only seems to happen when I call coq.term->string on specific terms

Enrico Tassi (Jan 24 2024 at 21:35):

Hum, it is again related to sections... but it may just be that a proof variable was cleared... hard to tell without some more details.

Luko van der Maas (Jan 29 2024 at 15:16):

It is in the middle of my pretty large codebase at the moment, but after some reduction of the test case I managed to suddenly get another error: Not Yet Implemented: (glob)HOAS if-then-else It is on the following term:

EI.ind
  Inductive twp2 `{!irisGS_gen hlc Λ Σ} (s : stuckness) : coPset -> expr Λ -> (val Λ -> iProp Σ) -> iProp Σ :=
    | twp2_none E e1 Φ P : ⌜if P s then False else True⌝ -∗ twp2 s E e1 Φ.

Where I call coq.term->string { coq.arity->term Arity } on every constructor. The command takes in the inductive as raw.

Last updated: Oct 13 2024 at 01:02 UTC