Add support for TLAPS (TLA Proof System)

[andylokandy]

Is it possible to have vscode-tlaplus run tlapm to check the proofs and even to decompose the proofs?

[lemmy]

Here is a high-level description of what is needed:

Must

• Extension settings to set tlapm path
• Invoke tlapm from vscode extension
• Parse tlapm output and annotate editor accordingly

Should

• Pipe tlapm to a console
• Dialog to configure tlapm flags per invocation
• Editor coloring similar to Toolbox
• Refactor and extract decompose proof command out of Toolbox into standalone library
• Integrate decompose proof command in extension

Nice to have

• Settings to change color mapping

[dricketts]

Proof folding and the associated hiding commands from the Toolbox would also be nice to have.

[lemmy]

@dricketts It occurred to me that I would find it useful if all facts were visually annotated in the module that appear in the BY DEF statements of the current proof step. I hope that it would help make it easier to spot missing facts. What's your take?

[dricketts]

@lemmy I'm not sure I understand what you mean. Suppose a step has BY <2>3, Lemma1 DEF Foo. Would this feature visually annotate step <2>3, Lemma1, and Foo?

[lemmy]

It would annotate the definition of Lemma1 and Foo where they appear in the spec.

[dricketts]

I don't think the annotations would help me debug a proof step. What I usually miss is a way to drop into a procedural proof mode (like tactic-based proofs in Coq) in order to understand what's missing. This wouldn't be a replacement for structured TLA+ proofs - procedural proofs are unreadable and difficult to maintain. But I think it would be a faster way to figure out what definitions and facts are missing, or whether the proof just needs to be broken down further.

Of course, such a mode is much more difficult to implement than annotating definitions. So if others think that feature would be valuable, I'm all for it.

[will62794]

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. I started poking around a bit to see what would be needed to implement a minimum viable solution in the VS Code extension. I suppose @dricketts would have some of the best insights here since it seems he implemented a good portion of the initial TLAPS functionality in the Toolbox, if my understanding is correct.

One particular thing I am curious about, which seems a potentially larger hurdle to straightforward implementation, is whether coloring of proof steps in the Toolbox requires use of the SANY parse tree. From looking at a few files it seems that it does, but I am not certain based only on a cursory reading of the code. If this is the case, I was wondering if the new tree-sitter parser from @ahelwer would be useful here, if we need richer information about the parse tree to implement proof step coloring properly inside the VSCode extension. As I understand it, SANY does have some kind of XML export feature, but I don't know if it is maintained, or if it works for TLAPS proofs.

[ahelwer]

@will62794 yeah the tree-sitter grammar properly parses proofs with levels and so forth. Proof folding/hiding is implemented in Neovim already through the nvim-treesitter plugin. What is this coloring you refer to? Like regular syntax highlighting? Or coloring to mark a proof step as proven or not?

[will62794]

@ahelwer Yeah, the tree-sitter grammar looks awesome. I tried out the online demo and it seems to parse TLAPS proofs just fine (e.g. a basic sample proof). It seems you already have a demo that works in TypeScript, so presumably it could be used directly from within the VS Code extension, if needed.

What is this coloring you refer to? Like regular syntax highlighting? Or coloring to mark a proof step as proven or not?

The latter i.e. the coloring the Toolbox shows to indicate whether a proof step is "proved", "failed", "in progress", etc. To my knowledge, the TLA+ proof manager handles proving the necessary proof obligations and reporting the status back to the Toolbox, but the information it reports doesn't seem sufficient to generate the coloring information that is currently shown in the Toolbox. There seems to be a more involved computation for determining the coloring of proof steps based on the results of the proof obligations returned by TLAPM e.g. see here. Part of this computation seems to rely on knowledge of the syntax tree. I will let @dricketts or @lemmy correct me if any of this is inaccurate.

Also, I suppose the extension does already have some parsing capabilities, which it seems to rely on for syntax highlighting, but this may be too basic to provide detailed information about TLAPS proof trees.

[lemmy]

IIRC the proof coloring is exclusively implemented in the Toolbox. The same goes for the proof decomposition functionality. Perhaps more of this functionality should be moved out of the Toolbox and pushed downwards into, e.g., TLAPS.

/cc @johnyf

[kape1395]

Do you know if there is any progress on this? I want to work on the TLAPS integration this summer and wonder if that overlaps with others.

[lemmy]

@kape1395 Thanks for your contribution! I'm not aware of any other efforts to add TLAPS support to VSCode. Would you like to join the upcoming TLA+ project meeting on 6/13 at 8 am PDT to collaborate with others if any?

/cc @muenchnerkindl