Nikola Katić (Aug 18 2022 at 11:49): 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:{{
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.
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).
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.
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: Oct 13 2024 at 01:02 UTC