Yannick Zakowski (Jun 23 2021 at 07:56): Yannick Zakowski (Jun 23 2021 at 07:56):Hello,
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?
Théo Winterhalter (Jun 23 2021 at 08:03):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.
Yannick Zakowski (Jun 23 2021 at 08:04):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
Théo Winterhalter (Jun 23 2021 at 08:04):Oh ok.
Théo Zimmermann (Jun 23 2021 at 09:17):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?
Théo Zimmermann (Jun 23 2021 at 09:18):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 *.
Yannick Zakowski (Jun 23 2021 at 17:05):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.
Wolf Honore (Jun 23 2021 at 20:48):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.
Pierre Courtieu (Jul 03 2021 at 14:09):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.
Wolf Honore (Jul 03 2021 at 14:43):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.
Pierre Courtieu (Jul 11 2021 at 15:19):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.
Ralph Matthes (Jul 13 2022 at 15:27):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.
Paolo Giarrusso (Jul 13 2022 at 16:42):VsCoq has no automatic Coq-specific indentation; I just use vim keybindings, select text, and increase/decrease indent with >>/<<.
Ralph Matthes (Jul 13 2022 at 17:23):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:
"coq.format.indentAfterBullet": "indent",
"coq.format.unindentOnCloseProof": true,
"coq.format.indentAfterOpenProof": true,
"editor.formatOnType": true
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.
Paolo Giarrusso (Jul 13 2022 at 19:42):Oh, thanks for the correction! I'll check this out, but what I'd love is a good auto indentation for Coq terms :grinning:
Ralph Matthes (Jul 15 2022 at 11:13):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: Jun 04 2023 at 23:30 UTC