Hi there
We are trying to evaluate the interest of adding non builtin notations into proofgeneral default indentation mechanism.
Is there some common monadic notation used by almost everyone in Coq?
I know of these two:

x <- e ;;
y <- e;;
e

and

do x <- e;
do x <- e;
e

Are these common enough to deserve being builtin in pg?

More generally are you annoyed by some other syntax not correctly indented in pg?

I too use ext-lib, and find the lack of indentation support frustrating! I donāt care too much if itās built in or not, but I think itās important to have good support for this. Monad notations are the main pain that I have had with proof general (most other notations I have seen are used for single-line expressions and so indentation is less of a pain point there).

(I kicked off this discussion with the pull request, for transparency)

Notation "x ā y ; z" := (y ā«= (Ī» x : _, z))
(at level 20, y at level 100, z at level 200, only parsing) : stdpp_scope.
Notation "' x1 .. xn ā y ; z" := (y ā«= (Ī» x1, .. (Ī» xn, z) .. ))
(at level 20, x1 binder, xn binder, y at level 100, z at level 200,
only parsing, right associativity) : stdpp_scope.
Notation "x ;; z" := (x ā«= Ī» _, z)
(at level 100, z at level 200, only parsing, right associativity): stdpp_scope.

Of the top of my head, the following two indentation issues with tactic notation come to my bind:

ssreflect-style by (sometimes?) leads to an indentation on the next line. IIRC e.g. after something like foo; last by eauto.

We have some notation that involves a forall, and that screws up indentation badly: iInduction lemma as ... forall (a b c), meaning āgeneralize a, b, c for the induction hypothesisā, but then PG makes the next line indented all the way to the position of the forall, which is not at all what we want.

Judging by previous responses there might not be a common syntax. I can report that Mtac2 uses x <- t1; t2 for bind t1 (fun x => t2), t1;; t2 for _ <- t; t2 and also supports 'pat <- t1; t2 for irrefutable let bindings.

Mtac2 code gets mangled quite badly by the indentation algorithm in proof general. We have use a lot of keywords that also come up in coq proper (for example, mmatch ... as ... in ... return ... with ... end). Terms like those will be indented in various weird ways, probably owed to how exactly PG determines when to indent based on, I think, mostly just one isolated keyword?

I wonder if the long-term fix for this would be to query coq for the format of user-defined notation? I know this would only work for printing notation (i.e. not only parsing notation) but it would be a great help still.

Support for this would have to be added to Coq, obviously. And if we are already doing that, letās keep in mind a coqfmt tool? I donāt mind my code looking ugly while I write it as long as there is a consistent way to format it automatically once I am done with my changes. Obviously, I am just dreaming hereā¦

I usually use either x <- e ;; e' (employed in MetaCoq notations for instance) or simply x <- e; e'. Indentation in PG has a few quirks but it somewhat work.

I have a lot of troubles combining PG and the syntax used by Equations:

Equations foo a b :=
foo (A0 _) (B0 _ _) := branch0 ;
foo _ _ := branch1 .

I often find myself fighting with PG to get a reasonable indentation and thatās an important (and rather stupid) reason making me hesitate to use equations.

To be precise we have a very complex lexer that performs non trivial toekn detection (by looking around and guessing basically) and simple grammar using the smie library by Stefan Monnier. The lexer is very difficult to maintain. The grammar is simple to maintain but cannot really correspond to coqās grammar because smie is based on a notion of grammar that is too simple. Anyway it is better than nothing I hope.

This idea has been in the air for a long time. It would be nice indeed. A independant stand-alone coqindent program would be perhaps be better.

The coq-prelude package yet to be published to Opam propose the following notation based on the recent custom entry mechanism:

Declare Custom Entry monad.
Notation "'do' p 'end'" := p (p custom monad at level 10) : prelude_scope
Notation "p ';' q" := (bind p%monad (fun _ => q%monad))
(in custom monad at level 10, q at level 10, right associativity, only
parsing).
Notation "'let*' a ':=' p 'in' q" := (bind p%monad (fun a => q%monad))
(in custom monad at level 0, a ident, p constr, q at level 10, right associativity, only parsing).
Notation "'let' a ':=' p 'in' q" := (let a := p in q%monad)
(in custom monad at level 5, a ident, p constr, q at level 10, right associativity, only parsing).
Notation "x" := x%monad (in custom monad at level 0, x constr at level 200, only parsing).

The idea is to be very analogous to OCaml monadic let.

Basically I am the only user of this notation yet, and I would be surprised to see PG support it explicitly, but eh, it exists!

I like the idea of using OCaml let* notation! Many people here using ExtLib. Perhaps to popularize them the first step is to add it to ExtLib as alternative notations.

I, too, like the OCaml syntax and I am planning propose it as an alternative or even the default syntax for Mtac2 soon. I just havenāt gotten around to writing the code yet. (I would prefer not having do .. end blocks, though.)