Stream: Elpi users & devs

Topic: Running issues


view this post on Zulip Nikola Katić (Aug 18 2022 at 11:49):

Hi, could someone help me run this simple example @Enrico Tassi gave me a few weeks ago.

From elpi Require Import elpi.

Elpi Command let_name.
Elpi Accumulate lp:{{ (* EXECUTION HANGS HERE *)

  pred extract-let-name i:term, o:string.
  extract-let-name (let N _ _ _) ID :- coq.name->id N ID.
  extract-let-name T _ :- coq.error "not a let:" {coq.term->string T}.

  main [trm T] :- extract-let-name T ID, coq.say ID.
}}.
Elpi Typecheck.
Elpi Export let_name.

let_name (let x := 3 in _).
let_name (let y := 3 in _).
let_name (bool).

It is the same with the official reflexive_tactic example.
In that case execution stops at line 170, i.e. Elpi Db monoid.db lp:{{

view this post on Zulip Pierre Roux (Aug 18 2022 at 11:51):

Did you try to run it with coqc or in an interactive interface? The {{ syntax is known to be unsupported by proofgenral for instance.

view this post on Zulip Pierre Roux (Aug 18 2022 at 11:52):

To develop in elpi with emacs, I tend to use separate files witl Elpi Accumulate File instead (not very confortable but I'm more used to emacs than to vscode).

view this post on Zulip Nikola Katić (Aug 18 2022 at 11:58):

That makes sense then -- I tried it using proofgeneral. I'll probably separate code the way you described.

view this post on Zulip Enrico Tassi (Aug 18 2022 at 12:31):

Indeed, PG has a known issue. CoqIDE should work.

With may hat of 10+ years vim user, I do recommend to try vscode (not just for this little issue). You might be surprised :-)


Last updated: Feb 05 2023 at 14:02 UTC