search

metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
77 stars 25 forks source link

Formatting the code #123

Open benjub opened 1 year ago

benjub commented 1 year ago

I think that to ensure consistent coding style, we should agree on a code formatter to use (and even make it part of CI ?). Are there standard tools to format/indent C code ?

I saw AStyle and clang-format mentioned on https://stackoverflow.com/questions/841075/best-c-code-formatter-beautifier. Or simply GNU indent ?

digama0 commented 1 year ago

Lean uses Google style guide and the page also mentions a style linter that we could borrow for our own use. I would try to set all the config options to match the current style as close as you can, and then enable it in CI.

benjub commented 1 year ago

I don't have much expertise, here. Plus, to enable it in CI (that is, not only check formatting, but actually perform it), one needs special rights for the repository. Unfortunately, I cannot do it, though I think that having such an automated formatting would simplify some tasks in #17.

digama0 commented 1 year ago

FWIW, in lean it's not actually auto-applied, it's a CI check which is run as if it were a test case. The intended workflow is for developers to run the tests and manually correct any flagged issues. We probably want an auto-formatter for the initial pass though, and it would also be helpful so that people can enable it using some run-on-save functionality in their editors.

Unfortunately I don't have the time to investigate and test these formatters. If you don't either I don't mind leaving this issue open for a while.