vscode-tlaplus
vscode-tlaplus copied to clipboard
tlaplus
Feature/update vars command
This PR implements the update vars feature requested in #364.
TLA+: Update vars tuplecommand that syncs your vars tuple with VARIABLES declarations
- Handles single/multi-line VARIABLES, multiple declarations, and VARIABLE/VARIABLES keywords
- Preserves your multi-line formatting style (2, 3, 4+ items per line)
- Auto-converts long single-line vars to multi-line for readability
- Maintains indentation patterns
- Lightbulb 💡 appears when cursor is on vars == line
- One-click update without opening command palette
- (kind of) PlusCal support : Detects --algorithm and --fair algorithm
- New setting: tlaplus.refactor.includePlusCalVariables (default: true)
- Handles pc and stack variables based on the user's preference (VS Code settings)
https://github.com/user-attachments/assets/18bbc295-3777-4596-99ad-9dfa98699823
I use this file for manual tests (in debug mode):
---- MODULE TestModule ----
VARIABLES aleph, beh, teh, theh, jeem, hah, khah, dal, thal, ra, zay, seen
VARIABLES sheen, sad, dad, tah, zah, ain, ghain, fa, qaf, kaf, lam, meem, noon, ha, waw, ya
VARIABLE single
vars == <<>>
Init == x = 0 /\ y = 0 /\ z = 0 /\ t = 5
Next == x' = x + 1 /\ y' = y + 1 /\ z' = z + 1 /\ t' = t + 2
Spec == Init /\ [][Next]_vars
====
Note: This PR does NOT implement all the expectations :)
for PlusCal (very basic for now):
https://github.com/user-attachments/assets/75f16fc4-feb5-44ac-b365-d821a9065476
@hwayne You requested this feature—could you take a look and help with the review?
I would like to abandon this PR and replace it with a new clean one (& use the tree-sitter). It will be cleaner and more reliable, I think.
Your thoughts? @lemmy @ahelwer
I'm certainly happy to support the VS Code extension's use of tree-sitter-tlaplus from the side of developing tree-sitter-tlaplus, so file issues if there are any features you need.
I would like to abandon this PR and replace it with a new clean one (& use the tree-sitter). It will be cleaner and more reliable, I think.
Your thoughts? @lemmy @ahelwer
I have reservations about adding yet another parser to the VSCode extension. There are already subtle inconsistencies in parse results between SANY (the standard parser) and the TLAPS parser when TLAPS is activated.
in this case, I keep this PR as-is for now, sticking to the existing code pattern: hybrid approach: SANY/XMLExport, and regex as fallback.
(I just thought that tree-sitter could be an efficient replacement for these regex & custom parsing algos, for reliability, TLA+ syntax coverage, etc. Of course, we would still use SANY just as we do today for semantics)
https://github.com/user-attachments/assets/1c19e3b0-3c0c-4f9b-a1c3-af75072230ec
I have reservations about adding yet another parser to the VSCode extension. There are already subtle inconsistencies in parse results between SANY (the standard parser) and the TLAPS parser when TLAPS is activated.
I would argue the inconsistencies between regexes and SANY are far, far larger than any inconsistency between tree-sitter and SANY, since both conform almost entirely to the syntactic test corpus.
I would argue the inconsistencies between regexes and SANY are far, far larger than any inconsistency between tree-sitter and SANY, since both conform almost entirely to the syntactic test corpus.
Replacing all regular expressions (syntax highlighting) with tree-sitter sounds like a good idea to me. We should use SANY wherever it's capable of handling the job (recovery mode should be assumed to occur eventually in SANY).
Architecturally, will tree-sitter work in the VSCode browser mode on e.g. github.dev?
I don't know how to check that but in terms of toolchain requirements tree-sitter-tlaplus is a large generated C file. The NPM package contains pre-built binaries of tree-sitter-tlaplus for x64 and arm64, so users of the package don't need to have a C compiler installed. tree-sitter-tlaplus can be compiled to webassembly (which is what Spectacle uses) but that has a different API than the NPM package I think.
tree-sitter-tlaplus can be compiled to webassembly (which is what Spectacle uses) but that has a different API than the NPM package I think.
@ahelwer Are there any disadvantages to using the WebAssembly API?
Not that I know of, although I have never used it personally. You're thinking you would run webassembly even locally?
@ahelwer Are there any disadvantages to using the WebAssembly API?
@ahelwer Are there any disadvantages to using WebAssembly locally?
Hmm, also have never tried, but my understanding is you would need to bundle a WebAssembly runtime engine (idk how big that is) and it would almost definitely be slower than a natively-compiled tree-sitter grammar. Probably would still be fine for usability? Also don't know what TypeScript -> WebAssembly interop looks like.
It seems to me that tree-sitter-tlaplus brings quite a bit of overhead. I don’t think we want to end up with an extension that’s either platform-specific or significantly larger than its current size of under 10 MB.
VS Code certainly supports platform-specific extensions where you can conditionally bundle native pre-compiled build artifacts for the specific target platform. A compiled tree-sitter-tlaplus grammar is currently around 4.7 MB - LR(1) parser tables can get quite large for ambiguous languages like TLA+!
If you want to be able to support both native and web-based execution of the extension (do the bundled Java tools work in that scenario?) you'll likely need to use the webassembly version, which uses different API bindings as far as I know.
@younes-io are you able to join the monthly community calls? It is a good way to push & resolve issues which are not getting attention. You are a great developer and it would be a shame to lose you due to stalled PRs!
@ahelwer Thank you for the kind words! I'd be happy to join the community call on Sept. I also understand the architectural considerations are important to get right