ProofGeneral
Indentation issue: "forall"
The following code:
Proof.
iIntros (<-) "Hvs". iInduction vs as [|v vs] "IH" forall (l)=> //=.
rewrite big_opM_union; last first.
gets auto-indented (select it, and hit "Tab") to
Proof.
iIntros (<-) "Hvs". iInduction vs as [|v vs] "IH" forall (l)=> //=.
rewrite big_opM_union; last first.
Looks like PG tries to align tactics with the forall in our custom tactic notation, which makes little sense.
Is there an easy way to distinguish real foralls from the ones and that are part of the custom notation?
I am not sure how sophisticated the parser is. The notation foralls only appear in "notation scope", i.e. in the Proof. ... Qed. part of the file.
Yes, but presumably your tactic notation can be used in parentheses, too, right?
But maybe the second case isn't relevant anymore? (Is ; associative now?)
exact ltac:(…).
I see... maybe that's niche enough to not be so important. Certainly, I don't think anyone would use our tactic in tactics-in-terms.
destruct x; (…; …).
There are some rare cases where this is needed, true.
But maybe the second case isn't relevant anymore? (Is
;associative now?)
They always can, parenthesis are just prenthesis. Like in repeat (intro).
But a term inside a tactic must have parenthesis, so it may be possible to make the pg lexer detect this and consider 2 kinds of forall. In this particlar case however there is another problem: the lexer itself currently relies heavily on the unicity of forall for other disambiguations (the pair forall, ',' is considered as some parenthesis, like let,ìn etc). So I guess this is a bit complex to fix.
For the record: due to the use of the smie library for indentation there is no limit to the complexity of the lexer (arbitrary code in coq/coq-smie.el functions: like coq-smie-backward-token) but the parser (coq-smie-grammar) must remain simple.
On the other hand this problem is made worse by something that hits me every now and then: indentation of a command should never indent relatively to the inside of a command, but it does because of the way the "." is dealt with smie grammar. I did not find a way to prevent that yet.
I discussed once with @monnier the possibility to have a grammar with 2 layers. One layer to indent commands (that we would trigger when indenting the first line of a command. The other for indenting inside a command (triggered otherwise).
That would make things 1) much simpler 2) probably much more robust to crazy ultra-redondant notations.
Of course the other possibility would be to have a coq-indent external program similar to ocaml-indent. This is however more complex than with ocaml mainly due to the import commands which may modify the parsing rules on the fly (so to indent a file, all imported files should be compiled and loaded).
