Add tlaplus-formatter support

[FedericoPonzi]

Add support for the tlaplus-formatter to the vscode-extension. It is enabled by default. It reuses the module search paths that the user has configured. After each formatting, the formatter verifies the ast is valid and matches the one from before - if the check fails the old spec is produced in output, so it's safe to use. It can be disabled via settings, and it's enabled by default.

[younes-io]

what is the status quo on this one?

[FedericoPonzi]

I don't think there is much to do here until the tlaplus formatter package (or other formatters) gets into a more mature state and becomes worth integrating into the plugin.

[lemmy]

@FedericoPonzi A couple of months have passed, and it appears that you’re preparing a 0.1 release. Perhaps it’s time to revisit this PR?

[lemmy]

The formatter can’t come soon enough. Critics have argued that TLA+ hasn’t kept up with modern tooling standards, and the lack of a formatter is often mentioned as a concrete example.

[younes-io]

I also was looking for a commit and couldn't find it; so not sure if history in this branch was re-written..

[FedericoPonzi]

I usually amend and work on the same commit. I've added a new commit to address your last comment now, thank you!

[younes-io]

LGTM. Thank you @FedericoPonzi

[lemmy]

Can't wait to give this a spin. :-) Should also be on the list at tlaplus/tlaplus#1311

[FedericoPonzi]

I'm happy to see the initial version merged finally :) I know it's not perfect yet, so please do share feedback and it can be improved over time

[lemmy]

• For a spec that extends some CommunityModule that are packaged as part of the extension:

Formatter error: Exception in thread "main" me.fponzi.tlaplusformatter.exceptions.SanySyntaxException: 
*** Errors: 1 Unknown location Cannot find source file for module Functions imported in module DieHardest. at
me.fponzi.tlaplusformatter.SANYWrapper.ThrowOnError(SANYWrapper.java:98) at
me.fponzi.tlaplusformatter.SANYWrapper.loadSpecObject(SANYWrapper.java:85) at
me.fponzi.tlaplusformatter.SANYWrapper.load(SANYWrapper.java:42) at
me.fponzi.tlaplusformatter.TLAPlusFormatter.<init>(TLAPlusFormatter.java:41) at
me.fponzi.tlaplusformatter.Main.mainWrapper(Main.java:99) at me.fponzi.tlaplusformatter.Main.main(Main.java:134)

• The formatter appears to inserts a whitespace after the box operator, causing [][Next] to be reformatted to [] [Next]. This is rather unusual formatting.

[FedericoPonzi]

• Addressed in Fix formatter failing on specs that EXTENDS CommunityModules #496
• Fixed in latest release (0.2.1): https://github.com/FedericoPonzi/tlaplus-formatter/releases/tag/v0.2.1