Skip to content

LSP: Proof decomposition code actions.#241

Merged
kape1395 merged 52 commits intomainfrom
lsp-decompose-proof
Apr 11, 2026
Merged

LSP: Proof decomposition code actions.#241
kape1395 merged 52 commits intomainfrom
lsp-decompose-proof

Conversation

@kape1395
Copy link
Copy Markdown
Collaborator

@kape1395 kape1395 commented Oct 14, 2025 •
edited
Loading

To try this out, build and install (make all install) TLAPM from this branch. The existing VSCode extension works without changes.

The majority of the decomposition suggestions are proposed for a QED step.

Please report your impressions on what could be improved.

kape1395 added 30 commits April 27, 2025 12:40
@kape1395
Initial ideas on proof decomposition.
4bf0b21 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Use visitor to construct the proof steps in the LSP.
5e5707e 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Some proof decompositions work already, but messy.
44e26de 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Code formatting of decomposed steps improved.
d1efcb5 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Basic decomp for \E.
4d16345 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Cleanup.
9bf23ae 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Normalize the obligation before analysis.
131b8c9 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Name clashes are now resolved when decomposing \E and \A.
f5ccffe 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Cleanup in tlapm code.
39f12e2 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Fixing odoc format.
c966acb 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Fixing the proof step status.
afa473b 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Proof step statuses are now fixed.
04e6ee6 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Cleanup.
8d359f7 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Have I fixed the ix'es?
e5ed589 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Minor tuning.
f75aa65 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Expand names. Conj improved.
6c51aba 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Cleanup.
06a5bf9 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Split to sub-modules.
9426dc8 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Basic case-split.
34e33cb 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Case-split improved.
a1c69e2 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Cleanup.
df19b69 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Split conj assm.
42799d1 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Don't list defs from hidden facts.
d1775f7 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Case split: add the CASE assm to the used facts.
642e0c3 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Decomp: use "=>" assm.
4f069d7 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Decomp: small fixes.
4e9461a 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Use quoted strings for the tests.
4015ffa 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Decomp: use \E assm.
95ef663 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Decomp: Use \A assm.
95ab136 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
A bit of testing.
175f2cb 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
kape1395 added 18 commits October 12, 2025 22:23
@kape1395
Decomp: less hacky "to sub-steps".
7412e3f 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Should start working on the tests.
95feeff 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Some tests for LSP.
013d46e 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Apply text edit in the test.
124cf80 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Fix the CI build?
3e50732 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Fix the CI build?
c415668 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Fix the CI build?
d91f00b 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Fix the CI build?
67f79b0 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Fix the CI build?
ce284ac 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Multiline text diff for tests.
7e3b9ce 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Some test cases.
17c4387 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
More tests.
718da54 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Test for Expand DEF.
6e5dca7 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Tests for using assms.
09fb135 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Preparing for capturing printed ranges.
016f385 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
ocaml formatter updated.
72006b3 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Merge remote-tracking branch 'origin/main' into lsp-decompose-proof
0d27fc7
@kape1395
Cleanup.
fc081c4 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395 kape1395 marked this pull request as ready for review January 12, 2026 21:07
@kape1395 kape1395 mentioned this pull request Feb 20, 2026
Closed
damiendoligez
damiendoligez approved these changes Mar 17, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@damiendoligez damiendoligez left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me, only a couple of small remarks.

Comment thread lsp/lib/analysis/step_decompose/of_assm.ml Outdated
Comment thread lsp/lib/analysis/step_decompose/of_goal.ml
kape1395 added 2 commits April 9, 2026 20:14
@kape1395
Decompose Disjunction as a contradiction.
231a2fb 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Wording fixed.
59d3460 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395 kape1395 force-pushed the lsp-decompose-proof branch from 3aae826 to 59d3460 Compare April 9, 2026 17:16
@kape1395
Add copies of community modules for tests to pass.
66f3794 
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Copy link
Copy Markdown
Collaborator Author

kape1395 commented Apr 10, 2026

@muenchnerkindl, the build is now failing because of the missing Functions.tla? Maybe I should re-add that file for now, until a better resolution for the dependencies is found? Or should I merge this PR as is?

@kape1395 kape1395 merged commit 8c72a8c into main Apr 11, 2026
5 checks passed
@ahelwer ahelwer mentioned this pull request Apr 13, 2026
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@muenchnerkindl muenchnerkindl muenchnerkindl left review comments

@damiendoligez damiendoligez damiendoligez approved these changes

Assignees

No one assigned

Labels

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@kape1395 @damiendoligez @muenchnerkindl