William Schultz

@lemmy Is the support for this in TLC complete?

@lemmy What is the intended usage of the command line trace explorer functionality? There seem to be a few different ways to invoke it i.e. ``` java -cp tla2tools.jar tlc2.TraceExplorer...

On a related note, would it be possible to add functionality for formatting block comments in the same way that the Toolbox allows? e.g. ```tla (***************************************************************************) (* The following lemma...

I was recently working on some TLAPS proofs and it would have been nice to have this feature. Even if it was only able to check proofs and nothing else....

@ahelwer Yeah, the tree-sitter grammar looks awesome. I tried out the [online demo](https://tlaplus-community.github.io/tree-sitter-tlaplus/) and it seems to parse TLAPS proofs just fine (e.g. a basic [sample proof](https://raw.githubusercontent.com/will62794/logless-reconfig/master/proofs/BasicQuorumsLib.tla)). It seems you...

Sounds good, thanks!

As I recall, the order of the given sequence should simply correspond to the order that SVG elements are [appended as children](https://github.com/tlaplus/CommunityModules/blob/dd647242998a8694846a17874344bf7299c43f56/modules/tlc2/overrides/SVG.java#L88-L91) to the `` SVG element. From a [quick...

@lemmy Just pushed some fixes to address this. I believe one issue was that the interpreter was not short-circuiting implication evaluation where possible. Pushed a [change](https://github.com/will62794/tla-web/commit/ecca49a57e163d263510e297c13df170e6e68047) for this. I think...

@lemmy For which spec are you observing the behavior shown in that screenshot?

+1. I also encountered this as a minor annoyance when checking a larger inductive invariant.