stdlib2
stdlib2 copied to clipboard
coq
Policy for the superficial layout (spacing, newlines, ...).
I would like to mention an approach which has been useful in uniformizing the layout of files of the standard library and giving a feeling of homogeneity of style, which is the use of a standardized pretty-printer (aka "beautifier").
@gmalecha The beautifier is one but in its current state it produces quite horrible output. However, we could consider working on it again to make it a good formatter. It would typically be the kind of thing that should be available in a Coq language server (cc @ejgallego). Code formatters are a very trendy approach these days (gofmt, elm-format, etc.) to making sure that discussions on formatting do not interfere with other works and to "reducing cognitive load".
You can indeed use SerAPI to print a whole file in a slightly more controlled way, however this uses the same printer than the "beautifier", so you won't get terribly different output even if you could perform some additional tweaks thanks the to extra control.
Of course, you can parse the JSON/SEXP representation of the AST in any other language and print as you'd like.
Eelis van der Weegen once wrote: http://www.eelis.net/coqindent/ "coqindent is a small crude Python script that indents Coq proof scripts. It works by scanning coqtop's output for "# subgoals" strings and other cues that proofs have begun/ended, which is obviously an entirely fragile and irresponsible way to do it. Nevertheless, it mostly works, so perhaps it might be of use to others."
On Fri, Sep 28, 2018 at 3:15 PM Emilio Jesús Gallego Arias < [email protected]> wrote:
You can indeed use SerAPI to print a whole file in a slightly more controlled way, however this uses the same printer than the "beautifier", so you won't get terribly different output even if you could perform some additional tweaks thanks the to extra control.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/coq/stdlib2/issues/11#issuecomment-425432030, or mute the thread https://github.com/notifications/unsubscribe-auth/AAM2zsYl__zfAskKJI_PzClhqyMztx5Iks5ufiEKgaJpZM4W-UUD .
@spitters thanks for the link, you could implement that kind of script today in a robust way using SerAPI.