Add new formatter / linter tasks #17
Conversation
A new DafnyFormatTask is added that can run as either a passive checker / linter task "checkFormatDafny", or an active formatter task "formatDafny". Both are disabled by default. Enabling the linter will fail a build on badly formatted source code, whereas enabling the formatter will ensure source is always correctly formatted prior to compilation.
There was a problem hiding this comment.
Thanks for this contribution as well!
I've been debating what the right integration into the standard Gradle graph should be for these tasks. I think we should have checking the format automatically triggered somehow from the build task, but actually applying the formatter as a separate step to be triggered manually.
After digging into the most popular approaches to this, I actually think we should submit support for Dafny to Spotless: https://github.com/diffplug/spotless/tree/main?tab=readme-ov-file#current-feature-matrix. It looks like that takes very little code and they are open to just accepting a formatter for only one build system. That will get us exactly the UX I'm looking for, and get a bit more visibility for Dafny to boot. :)
If that's too much of an ask, I'm happy to do at least some of the work myself.
|
Closing as a Spotless component is likely a better solution |
A new DafnyFormatTask is added that can run as either a passive checker / linter task "checkFormatDafny", or an active formatter task "formatDafny". Both are disabled by default.
Enabling the linter will fail a build on badly formatted source code, whereas enabling the formatter will ensure source is always correctly formatted prior to compilation.