A new quite naive question once again. Although not perfect and sometimes a bit slow, PG is quite decent at indenting your code at the stroke of a tab. In VsCoq, there appears to have no support for this at all, and the following issue (https://github.com/coq-community/vscoq/issues/158) that sounded sensible to me was deemed unrelated to VsCoq itself, an argument that I don't quite understand.
Could anyone clarify what is currently missing to have support for code formattin in VsCoq Comparable to what PG provides?
What does PG provide besides Emacs auto-indenting feature? I remember that it wasn't working well and that I had to disable it.
In general it seems hard to indent proof scripts with bullets or pattern matching.
I am completely naive as to what is PG specific and what is emacs generic, but it handles bullets and matches quite satisfyingly for sure
was deemed unrelated to VsCoq itself, an argument that I don't quite understand
Sorry for having voiced that opinion. Clearly it's not unrelated to VsCoq to have feature parity with PG. It just seemed to me that the user opening this issue just hoped for an auto-formatter for Coq, as there exists in other languages (e.g.
ocamlformat for OCaml). This goes well beyond VsCoq. But if the question is good tab key management, then it doesn't (of course). Maybe that would be worth a separate issue?
I remember that it wasn't working well and that I had to disable it.
IIRC PG works quite well for bullet indenting, but only if you use the following order for the bullets:
- followed by
+ followed by
Thanks for the answer Théo! I'll indeed open a new issue to discuss if some of the PG-style indenting can be obtained in VSCoq then.
It would be nice and probably not that hard (?) to pull out this simple bullet and match indentation into a standalone program (in Python, Ocaml, whatever). Then all the IDEs can just call that and not have to keep reinventing the wheel. At least it would be pretty easy in Vim, I don't know how easy it is in VsCode or Emacs to filter text through an external program but I assume they have a way of doing it.
As the author of indentation for coq in pg (which is decent but indeed far from perfect) I can give one advice: don’t expect this to be simple, coq syntax is a nightmare. The only simple way of doing it would be to have coq itself doing the parsing.
I agree. I wrote the indentation for Coqtail and it's just a mess of regex and heuristics that works for the most part. But at least if it were an external program it could be a consistent mess across all the IDEs.
True:-) and I think coq is the only tool able to a Good job at it. Maybe not by reformatting it’s own syntax but at least by providing parsing informations.
May I ask (one year later) if anything towards handling of bullets has improved? I often go through big legacy .v files and work on the bulleting. ProofGeneral is really excellent for that - to adapt all subsequent indentation after, e.g., changing the depth of such a bullet tree.
VsCoq has no automatic Coq-specific indentation; I just use vim keybindings, select text, and increase/decrease indent with >>/<<.
Thanks for this clarification. The usual keybinding for working on the indenting level is Ctrl-[/Ctrl-] on Linux. However, when writing the proof script, I can have some indentation set automatically with the following additions to settings.json:
The last line is required by the second one to be effective.
Maybe you (@Paolo Giarrusso) used this anyway and only spoke about later work on .v files.
Oh, thanks for the correction! I'll check this out, but what I'd love is a good auto indentation for Coq terms :grinning:
I have a follow-up question: In the settings for VSCoq, I can control the variable
coq.format.indentAfterBullet. I cannot understand the description of the difference between value "indent" and value "align". I tried both values, and for what I am normally doing, they seem to be equivalent.
Last updated: Jan 30 2023 at 18:04 UTC