Conversation
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
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
wkirschenmann
pushed a commit
to wkirschenmann/tlapm
that referenced
this pull request
Aug 22, 2026
…self Asked why I had not installed Isabelle, I had no good answer. deps/isabelle/dune.mk pins Isabelle2025 with a SHA-256; the bundle is 1.08 GB, 1.5 GB on disk after the pruning the makefile already specifies, and the Pure and TLA+ heaps build in 31 seconds on four cores. It is installed now, and every gate in this branch is re-verified against it. test/fast 40 of 48 -> 47 of 48 dune runtest lsp 23 of 23 (unchanged) Seven of the eight failures were Isabelle's absence. So the claim repeated in all 26 commit messages -- "40 of 48 pass in an environment without Isabelle; a change to which eight fail would be a regression" -- attributed them to the right cause but presented a crippled environment as the gate. The messages are rewritten (content untouched: git diff between the old and new tips is empty) to state the real invariant: the fail-set is identical to main's, and the one remaining failure is named. That failure is fast/fingerprint/FingerprintVariablesParameters_test.tla. It expects 1 of 2 obligations to fail and gets 2 of 2, because Z3 4.8.9 does not prove \E y : y # x here. Verified to fail the same way on main, which is why the gate is "fail-set identical to main's" rather than a pass count -- upstream issue tlaplus#248 proposes upgrading Z3, and that is the kind of change this test is sensitive to. PROVERS.md records the install, and one trap worth writing down: putting isabelle on PATH is not enough and fails like a proof failure rather than a missing backend. tlapm finds the executable and then invokes it with a session root under its own backends directory, so a tree built with `dune build src` needs the installation linked there. The symptom is "Bad session root directory" buried above ordinary "obligations failed" errors. 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.
Some tests are still failing; therefore, that's a draft.