Stream: Coq devs & plugin devs

Topic: -beautify


view this post on Zulip Gaëtan Gilbert (May 01 2023 at 17:21):

Does anyone use -beautify? The code it produces is basically garbage so I guess not.
Shall we remove it?

view this post on Zulip Karl Palmskog (May 01 2023 at 17:24):

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.

view this post on Zulip Emilio Jesús Gallego Arias (May 01 2023 at 21:38):

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: Jun 13 2024 at 04:03 UTC