ceps
ceps copied to clipboard
coq
Indentation based bullet behavior
Rendered https://github.com/proux01/ceps/blob/bullet-indent/text/108-bullet-indent.md
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.
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.
+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.
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.
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...
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;
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.