Does anyone use -beautify? The code it produces is basically garbage so I guess not.
Shall we remove it?
with coq-lsp/VsCoq2, there can finally be intelligent general Coq formatters that use the proof state and are integrated into GUIs. Would be good to flag up to the community this is the most reasonable way forward with code formatting.
I have been tempted to remove it a few times, however the impact is not so big so I didn't bother.
There are some infra that only beautify uses (like the comments lexer tracker IIRC) that seems useful beyond, YMMV.
Last updated: Nov 29 2023 at 21:01 UTC