Proof scripts indentation checking

[proux01]

Rendered https://github.com/proux01/ceps/blob/bullet-indent/text/108-bullet-indent.md

[CohenCyril]

Thank you so much!

[Zimmi48]

The description of the stack mechanism is a little hard to follow and would benefit from being illustrated with an example.

[Zimmi48]

It could be any kind of sentence, not just a tactic, no? And it has to be the beginning of a sentence.

[proux01]

I'm not sure about that one. Most non-tactic sentences in proofs are likely to be some kind of debugging temporary thing, maybe it's more convenient to not enforce indentation for them? It might also be easier implementationwise? No strong opinion here.

[Zimmi48]

You could have clarified in the detail design section that this will be guarded behind a new bullet behavior, and thus off by default.
That being said, most well-structured proof scripts could work with the new bullet behavior. It would be interesting to evaluate how much of the CI would pass with the new bullet behavior activated for everyone.

[proux01]

This will indeed be an interesting experiment. I'd expect that this will essentially fail on old style proofs without any bullet nor indentation. This is still a significant part of the CI, but not sure how much.

[aspiwack]

As a card-carrying hater of everything indentation dependent I don't much like this (but you don't care of course, I don't have stake in this anymore, so feel free to do things I dislike). I thought I'd share a bit of historic perspective.

When I was working on the new tactic engine back when, @herbelin asked me to look at the bullets from Ssreflect, I think, but I'm not entirely sure, he's the one who suggested having an executable semantics for bullets.

Anyway, the truth of the matter is that I couldn't figure how to give a proper semantics to how bullets were used. So I chose a semantics for the new bullets which made sense to me, and I thought decently approximated the use in Ssreflect. But of course, in this case, decently approximated meant: absolutely incompatible. At the time, I thought that was unavoidable though, because I didn't think bullets as used in Mathcomp were regular enough to be codified. Maybe indentation is a solution, but (this is the leitmotiv, isn't it?) this is a tool I've always forbidden myself to use, so I didn't even consider this option.

[aspiwack]

I hope nobody writes proofs this way 😱 . Side-conditions was why I introduced {/} at the time. So I would expect such a proof to be written

Goal True /\ True /\ True /\ True /\ True.
Proof.
split.
{ exact I. }
split.
{ exact I. }
split.
{ exact I. }
split.
- exact I.
- exact I.
Qed.

It's fine if you don't like it, but you that's what you want to compare against.

(As I was saying, I personally much prefer this explicitly bracketed style to an indentation-dependent style.)

[proux01]

I hope nobody writes proofs this way 😱 .

Well, that's what you're forced to do if you want to actually use bullets.

Side-conditions was why I introduced {/} at the time. So I would expect such a proof to be written

Goal True /\ True /\ True /\ True /\ True.
Proof.
split.
{ exact I. }
split.
{ exact I. }
split.
{ exact I. }
split.
- exact I.
- exact I.
Qed.

That kinda shows the point: you can't really use bullets.

(As I was saying, I personally much prefer this explicitly bracketed style to an indentation-dependent style.)

I'm fine with the brackets but that's just not what is used in a large, neat and successfull, code base and can arguably be considered too heavy.

[SkySkimmer]

I did write proofs that way when I semi-automatically ported the stdlib to strict focusing ;)

That kinda shows the point: you can't really use bullets.

I don't understand the point then. What's wrong with mixing bullets and braces?

[proux01]

C.f. above: brackets are, understandably, considered by many as uselessly heavy.

[TheoWinterhalter]

I would personally use goal selectors for side conditions rather than brackets.

Goal True /\ True /\ True /\ True /\ True.
Proof.
split. 1: exact I.
split. 1: exact I.
split. 1: exact I.
split. 1: exact I.
- exact I.
- exact I.
Qed.

But here the structure of the proof is not actually that, so I would probably write:

Goal True /\ True /\ True /\ True /\ True.
Proof.
split. 2: split. 3: split. 4: split.
- exact I.
- exact I.
- exact I.
- exact I.
- exact I.
Qed.

[aspiwack]

I did write proofs that way when I semi-automatically ported the stdlib to strict focusing ;)

I guess if they're this way but only semi-written that's more ok 😛 ?

[aspiwack]

C.f. above: brackets are, understandably, considered by many as uselessly heavy.

If that's the case, then this is what must be argued in the RFC, rather what is currently in, which can be considered a bit of a straw man. Still as a bystander, I confess that I'd be interested to see, scientifically as it were, to see this particular hypothesis documented. I suppose you got this impression, that some (many?) consider {/} as too heavy, from somewhere, but it's invisible to me today.

[SkySkimmer]

IMO it's not particularly heavy syntactically (certainly better than indentation) but does require a bit more thought than just going new goal -> new bullet.

[ejgallego]

I hope nobody writes proofs this way 😱 . Side-conditions was why I introduced {/} at the time. So I would expect such a proof to be written

Goal True /\ True /\ True /\ True /\ True.
Proof.
split.
{ exact I. }
split.
{ exact I. }
split.
{ exact I. }
split.
- exact I.
- exact I.
Qed.

It's fine if you don't like it, but you that's what you want to compare against.

This is very close to math-comp style, adding the braces is just extra typing / two less spaces for the line:

Goal True /\ True /\ True /\ True /\ True.
Proof.
split.
  exact I.
split.
  exact I.
split.
  exact I.
split.
  exact I.
by exact I.
Qed.

Tho I think better style in this case is:

Proof
split first by exact I.
split first by exact I.
split first by exact I.
split first by exact I.
by exact I.
Qed.

But indeed, I think examples from the real world illustrate the difference better.

[proux01]

Thanks for the historical perspective. Indeed, my experience of MathComp is that bullets are almost anecdotical there. Most of the "proof block separation" there is done by indentation. Thus indentation simply can't be ignored.

[TheoWinterhalter]

I'm personally against anything based on white-space, soon you end up escaping newlines (like LaTeX, Python or Makefile).
While it's nice to encourage users to indent properly, this is the opposite of compositional (and if you want to automatically generate code, this becomes a nightmare within the first seconds). I agree that the current set up is not very compositional either though, unless you place every bullet list in braces to allow using - at every depth.

The mathcomp style of indenting without even using bullets is very hard to read, so I wouldn't want to generalise this behaviour as encouraged.

In my mind, all of this is the job of a linter, or even better should be handled implicitly for the user by the IDE.

Of course, like Arnaud, this is only my opinion.

[ppedrot]

+1 for extremely strong opinion against semantic indentation, the fact it has such a stronghold in Python is a clear argument that this is a defective design choice.

[Zimmi48]

you forget about Haskell XD

[ejgallego]

Glad you submitted this RFC, it is long overdue !

This part may not be so easy to implement tho, given the status of the higher-layers.

A possibility that would help inform implementation choices betters is to write a linter first.

I was thinking about how to do this in coq-lsp and I think I got a clear design. Let me know if you are interested and we can give it a go.

[ejgallego]

you forget about Haskell XD

and Lean!

[Zimmi48]

To share my own perspective, I too am very reluctant with significant indentation, but the fact that a whole part of the Rocq ecosystem renounces to use semantic bullets / goal focusing because of this historical design choice is a sufficiently strong argument to support this proposal. If the MathComp ecosystem developers can be convinced to switch to braces instead of indentation, then this proposal is moot. But if they cannot, then I prefer to introduce (optional) significant indentation in Rocq rather than leaving them in this poor state.

The fact that this new bullet mode would be compatible with most correctly indented proof scripts is an additional incentive to me. In particular, this would allow me (e.g., by activating this bullet mode, but only in CI) to check that my proofs are correctly indented. (Rocq becomes a linter that way, but this is also what one can already do with options such as Mangle Names.)

I believe that it is important to make a difference between this proposal (which introduces optional significant indentation) and most languages where it is significant, but not optional at all, because here, you have the choice to disable it if you encounter issues because of it.

[ejgallego]

the fact that a whole part of the Rocq ecosystem renounces to use semantic bullets / goal focusing because of this historical design choice

In my case, I use space-based, math-comp style indentation not because of a "historical design choice", but because, as outlined in my message above, it has some advantages over braces / bullets, in particular regarding line-width, etc...

[gares]

I think there is a subtle difference between semantic indentation and checking for consistent indentation.

The former is the python/make thing, if you don't indent your lines the program changes meaning.
The latter is about checking for a style, and if for example a proof breaks (an extra goal is left over) you get an early warning that the text does not conform to the style while it used to do so.

It is not so clear to me where this RFC stands, but I personally would love the latter.
If you programmed in OCaml and you made this mistake, you should agree :-)

if condition then
  let msg = bla bla in
  Printf.eprintf "error: %s\n" msg;
x := y;

[TheoWinterhalter]

Isn't that linting / prettifying?

[gares]

In a way yes, but that are usually totally optional (like in external tools). I'd like to have it part of Rocq execution phase, and in my use case I don't want it to change the indentation but rather warn me that the indentation is off.

[TheoWinterhalter]

Yes, I agree this would be useful.

[proux01]

Updated the proposal following comments, to turn it into a fully optional indentation checking through warnings. Warnings can then be silenced by uninterested users or turned to errors for users wanting strict enforcement.