API: change default aux dir to .tlacache - #20
Merged
Conversation
Closed
Contributor
Author
|
Thank you for reviewing and merging this pull request. |
wkirschenmann
pushed a commit
to wkirschenmann/tlapm
that referenced
this pull request
Aug 19, 2026
Real-solver FfiGrpc runs, fixed RSS sampler, binaries chosen just before and after each expected transition. Records the full curve: base 1.6 verdicts/s truncated; tlaplus#17 unlocks x8 then OOMs at 13.9 GB (as does tlaplus#19); tlaplus#20 is what makes the run finish (5.1 GB); tlaplus#21 buys x3.5 throughput; phase 4 flattens RSS to 439 MB at unchanged wall. End to end: unfinishable -> 3.5 min at 439 MB, 48 verdicts/s sustained, above the 43 v/s chunked-run target. Co-Authored-By: Claude <noreply@anthropic.com>
wkirschenmann
pushed a commit
to wkirschenmann/tlapm
that referenced
this pull request
Aug 19, 2026
The corpus that motivated the effort, measured across the transition binaries with real solvers: before the expand_defs unlock every binary OOMs early; tlaplus#20 collapses 77 -> 11.6 v/s as its heap walks to 13.6 GB and dies 380 verdicts short; tlaplus#21/tlaplus#24 finish with ~1 GB of margin on a 15 GB container while phase 4 does the same run at 1.39 GB flat and ~20 % faster in every quartile -- the user's measured GC coupling, reproduced and then removed. On the user's 7.7 GB machine only the phase-4 binary can finish: from '17 hours then OOM at 58 %' to 7.5 minutes. Co-Authored-By: Claude <noreply@anthropic.com>
wkirschenmann
pushed a commit
to wkirschenmann/tlapm
that referenced
this pull request
Aug 21, 2026
…dencies The ranked table did not have the granularity it implied, and the "recommended path" section restated it instead of adding to it. **Granularity.** The table now says explicitly that one row is one pull request, with a `commits` column: eight rows are groups that must land together (tlaplus#3 is 2 commits, tlaplus#15 is 3, tlaplus#17 is 2, tlaplus#18 is 3, tlaplus#19 is 6, tlaplus#20 is 5), twelve are a single commit. Item 17 also notes that the branch holds an add-then-revert pair there -- the prover-slot-division hypothesis, refuted by measurement -- which must not be replayed. **Two rows were missing entirely**, and the question exposed it: the measurement instrumentation (17 commits, 22 files, +876/-92) and the harness (5 commits, 9 files, +698) buy no performance, but T1/T2 *are* the checker and P1/P2/P3 *are* the probes -- an optimization landed before them ships unverifiable. They are now rows 0 and 0b, marked as prerequisites rather than ranked. **The step ladder is gone.** Its six invented steps were the same items regrouped, with diffstat totals that restated the table; the batching advice it carried was already one sentence in the summary. Replaced by what it should have been -- dependencies: * hard, in code: tlaplus#3's two commits in order; tlaplus#11 requires tlaplus#15 (the memo attaches to the expansion fold's shared states); tlaplus#15's three commits in order; tlaplus#19 requires tlaplus#5 (it patches the tree tlaplus#5 rebuilt); #0/#0b before any protocol; * hard by measurement, and easy to miss: tlaplus#3 must not ship without tlaplus#15 on INSTANCE-heavy specs -- alone it takes preparation 458 -> 842 s while cutting peak memory 13.9 -> 5.1 GB; * soft: tlaplus#6+#12 for the x49 elaboration clock, tlaplus#10+tlaplus#16 for the memory unlock, tlaplus#18/tlaplus#19 adjacent but independent. Plus three review-coherent batches, stated as such rather than as a path. The protocol section is renamed to say what it is. 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
2 participants
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.
This change makes
.tlacachethe default auxiliary directory, following #16.In the future, a command-line option could be added for specifying the auxiliary directory.