Fix #757 indentation of "\in"

[Matafou]

The lexer now glues a "" to an immediately following word if it is itself preceded by a space.

Note that for really good indentation you should try to add something like this to your configuration:

(setq coq-smie-user-tokens '(("\in" . "=")))

to tell the indentation grammar that \in has the same precedence as "=".

[Matafou]

The problem was that \in was lexed as "" "in" and that "in" is a (pretty crowdedly overloaded) reserved keyword for let in, Let in,..

I will wait a feedback from #757 before merging this.

[erikmd]

Hi @Matafou, thanks a lot for this fix!

I tested it successfully on another file of mine, as well as on your test file and it worked-out-of-the-box™ (using Emacs 28.2 on Debian 12)

[erikmd]

@Matafou Thanks a lot for this fix, which will be important for ssreflect & mathcomp users.

I'd say that maybe, this fix + your previous fix #782 alone (!) would deserve to prepare a release soonish.
(The main missing ingredient would be an up-to-date CHANGES file.
Then maybe also some cleanup of the make release command, taking into account this comment.)

@hendriktews @Matafou WDYT?

[Matafou]

I don't know the exact use of \xxx in mathcomp, are all these \symbols non associative infix operators?

Note that without the coq-smie-user-tokens trick these tokens will be considered with a default rule, precedence and associativity (@monnier can you tell what are these for a token not appearing in the rules and grammar, starting with a \). This can lead to strange indentation maybe. @vzaliva tell us if it is the case it should be easy to fix.

[erikmd]

I don't know the exact use of \xxx in mathcomp,

Basically, the default notation convention in the mathcomp core library is to only use ASCII operators, not UTF-8 or so, and typically it relies on notations very close to those from LaTeX. E.g.:

• x \notin E
• f \o g \o h
• \sum_(0 <= i < n) (i + 1)
• etc., see also https://www-sop.inria.fr/teams/marelle/MC-2022/cheatsheet.pdf

are all these \symbols non associative

not exactly, cf. the \o operator for function composition.

infix operators?

You also have \sum_i, \prod_i, \bigcap_i, \bigcup_i and a few others.

IIUC your PR code, the fix is not specific to \in 👍
so it should also work for the \notin and \o infixes for example (I didn't test)

[Matafou]

OK, I was hoping for something simple. How naive I am :-).

If we can come up with a decent coq-smie-user-tokens declaration for usual ssreflect operators we could put them into coq-standard-token-synonyms.

It would look like:

(setq coq-smie-user-tokens '(("\in" . "=") ("\notin" . "=") ("\o" . "+") ... )) 

(I guess \sum() is lexed/parsed as a standard function application and that's ok).

Maybe this already exists somewhere?

[Matafou]

Yes the fix is for any token starting with \. But indentation is not the same for a infix associative operator and a prefix one.

[erikmd]

OK thanks!

So IIUC, in addition to this PR, it just suffices to provide a relevant (setq coq-smie-user-tokens '(…)) list so indenting ssreflect would work out-of-the-box?

BTW I tested (setq coq-smie-user-tokens '(("\in" . "=")) vs. (setq coq-smie-user-tokens '(("\in" . "+")) and didn't notice a specific change in the indentation; could you help by providing a minimal complete example where the two infixes are indented differently?

[Matafou]

The difference can be subtle and this is very fragile, but here is a difference between + and = (that would reflect on \in):

Lemma foo:
  forall x y,
    y
    =
      z
    = y.

Lemma foo:
  forall x y,
    y
    =
      z
      + y.

[Matafou]

Note that this is a bit wrong since = is not associative, but that is the idea.

[erikmd]

OK thanks @Matafou !

So I'll try to come up with a comprehensive list of the \in | \notin | … mathcomp symbols this WE.

Question: can/should this PR be merged beforehand? or implementing the coq-standard-token-synonyms list you mentioned will require a non-trivial refactoring of this PR's code?

[Matafou]

I think we can merge.