Proof decomposition by template. - #268
Open
kape1395 wants to merge 9 commits into
Open
Conversation
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
Collaborator
Author
|
@uguryavuz, that's the branch I was working on. The match function is implemented only partially, for a PoC. Tried to rewrite it using existing visitors, but probably will stick with explicit traversal using a recursive function. |
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
kape1395
marked this pull request as ready for review
August 10, 2026 21:04
wkirschenmann
pushed a commit
to wkirschenmann/tlapm
that referenced
this pull request
Aug 21, 2026
… and survey them Two fixes to the upstream section. **tlaplus#286 is ours**, not an external reference, and the plan now says so plainly: same team, opened 2026-07-27, still unanswered, and its four patch families ARE our items 3, 6, 14, 15 and 20 -- already-public proposals re-implemented, not contributions of this branch. What the branch adds on them is what tlaplus#286 could not offer: single-topic reviewable commits with stated invariants and mechanical gates, and attribution per commit instead of per patch set. **Other people's PRs get their own section**, after checking upstream: `master` is at 4600b24, exactly this branch's base, so nothing has landed since the fork and only the open PRs matter. * tlaplus#284 (open, LGTM) kills orphaned provers via `exec setpriv --pdeathsig KILL` when *tlapm dies*. Same family as our item 2, complementary failure mode: ours covers tlapm alive but its kill ignored (SIGHUP set to SIG_IGN by nohup, inherited through exec). Neither subsumes the other, and tlaplus#284 supplies the SIGKILL escalation our fix lacks -- reference it, do not duplicate it. * tlaplus#285 (open) modifies `let_normalize`/`except_normalize`, the two functions item 15 calls per hypothesis. Textual conflict certain; the per-hypothesis equivalence argument must be re-established with the oracle afterwards. Kept in the survey for that reason only. * tlaplus#275 (open) makes SANY an opt-in parser, so item 7 keeps its value -- but the editor floor is now 95 % parse, and SANY does semantic analysis inside "parsing", which item 19 does not assume. * tlaplus#268 (open, extends the merged tlaplus#241) is the feature items 18-19 currently break: the decomposition code actions locate steps by range, and scoped re-elaboration leaves inner positions stale. This is why those modes stay flag-gated. * tlaplus#283 (merged) gives a deterministic Z3 budget -- worth adopting in measurement protocol P2 to remove prover-side variance. * tlaplus#266 (open) changes an SMT axiom, so item 3's subset gate must be re-run against it; tlaplus#248 (open) upgrades Z3 and invalidates absolutes. * tlaplus#264 closed without adopting an LLM policy -- escalated to the TLA+ Foundation board. The stated maintainer position (human first contact, per-commit disclosure of models used) is the one to assume, and the 441-lines-for-most-of-the-gain framing is what answers the review-workload concern behind it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CUUoeEmuL3jsYhUb3UrhJH
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Extensible proof decomposition rules.