First attempt of fixing elpi syntax by Philip Kaludercic.

[Matafou]

A first attempt proposed by @phikal (if I am not mistaken) some years ago, at supporting the elpi syntax, which can contain the usual command ender (. ).

Example of such syntax:

From elpi Require Import elpi.

Elpi Tactic show.
Elpi Accumulate lp:{{

  solve (goal Ctx _Trigger Type Proof _) _ :-
    coq.say "Goal:" Ctx "|-" Proof ":" Type.

}}.

[Matafou]

This is not correct (tests fail) because forward-sexp is redefined in proof-general and might jump over whole bunches of commands.

For instance

Lemma false_proof : forall A B : bool, A = B. 
Proof.
  intros A B.
  destruct A.
  destruct B.
  reflexivity. (*error*)
  reflexivity.
Qed. (*test-lemma2*)
  

when point is on Proof and we eval forward-sexp we end up after the Qed.

[phikal]

Have you tried binding forward-sexp-function to nil, so that PG doesn't use the SMIE interpretation of Sexps, but falls back to the default (which should just do counting for opening and closing symbols)?

[Matafou]

I will test this. Not sure what this will do with comments though.

[monnier]

Pierre Courtieu [2025-11-03 06:33:17] wrote:

A first attempt proposed by @phikal (if I am not mistaken) some years ago, at supporting the elpi syntax, which can contain the usual command ender (`. `).

(while (and (setq foundend (let ((start (point))) (forward-sexp) (if (re-search-forward coq-end-command-regexp-forward limit t) (match-end 1) (goto-char start)))) As @phikal suggested, you probably want to let-bind `forward-sexp-function` to nil around the call to `forward-sexp`. But the above code looks really odd: in one branch of the `if` you just return a position, while in the other you `goto-char`. To me, this looks very suspicious (like a kind of type-error), so if it's really what you intended to do, I suggest you write it as (if (re-search-forward coq-end-command-regexp-forward limit t) (match-end 1) (goto-char start) start) to make it crystal clear (and to save the reader from having to remember what is the return value of `goto-char`). Nitpick: I'd pass an explicit 1 (and -1 to go backward, rather than use `backward-sexp` which is designed more as a command than a function) to `forward-sexp`. Oh, and one more thing: (and (not (or (string-equal (match-string 1) ".") (string-equal (match-string 1) "..."))) This is now a bit dodgy because you use `match-string` after an `re-search-forward` which may have failed (in which case the match-data is inherited from the previous successful regexp match, which could be completely unrelated). And while you're there: could you replace this `or+equal` with a `member` so as to allocate the (match-string 1) only once?

[Matafou]

A new attempt, with a small refactoring relying more on syntax-ppss than before.
There are still a strange behavior of coq-script-parse-cmdend-forward/backqard wrt to bullets and {, }, but no more than before. So for now I will experiment with this.