Repository navigation
Restore main's exact gain, swap costs, per-group balancing, and glob escapes after the merge - #12
Merged
Merged
Conversation
commBlock names, and glob literal escapes after the merge The merge commit 37d7f9d resolved Ledger/Journal.lean and Ledger/Driver.lean by splicing the branch engine wholesale, which silently dropped four behaviors of main that the engine region overlapped: the exact lot-basis gain of 5376d29, the swap-cost plumbing of 6c6942e, the commodity-block name fix of the 3313 series, and the literal-escape reading of include glob patterns. Cross-oracle comparison against main's oracle (bbd5478) over its whole regress corpus also exposed that the series engine predated the per-group balancing of C++ PR 3317, five regress files of which the branch corpus never contained. This commit ports each behavior into the branch architecture and witnesses every one against the C++ main binary (5f9855cef, which contains PR 3317 and the fix of issue 3258). Exact gain and swap cost. `AnnotTail.lot` grows the recorded price decimals, a new `AnnotTail.costLotAmt` carries the per-unit cost and its decimals out of the annotation loop, and `gainVal` books the exact residual `(p.q * a.q) - c.q`, or `(p.q * a.q) - (cp.q * c.q)` when a swap rewrote the cost into another commodity, where the former merge had stubbed the swap cost as declared but never set or read. `costVal` takes the widened basis when a gain is booked and the transaction is not periodic, `swapCostVal` is set whenever the recorded cost and the cost value name different commodities, and `balancePool` adds a posting's gain into its own pool. Witness: `10 GAL {$2.00} @@ $25.30` balances to $-20 as main's oracle prints, and test/regress/3258, 3258_computed, 1773, 2975, 3013 and 1217 of main's corpus print identically on both sides again. Per-group balancing. Both balancing passes now infer the exchange rate from each pool against the whole transaction, not the real pool alone, and the second pass no longer refuses pools that hold no real amount, which is the behavior C++ PR 3317 introduced after the series engine was written. Witnesses: main's regress/3314_fixated, 3314_parens, 3314_exchange, 3314_exchange_elided and 3314_inference_order, each of which the C++ binary accepts or rejects as the merged oracle now does, printed identically to main's oracle. Commodity block names. The `commodity` directive registers the block under the bare symbol its header parses (`headerSymbol`), not under the full directive text, so that amounts priced in the commodity match its learned precision. Witness: regress/3313 prints `USD|-10|Equity` as C++ does. Include glob escapes. `splice` no longer strips backslashes from the pattern before resolution, since a backslash makes the next character literal and `globComponent` already reads one that way (textual_directives.cc:370); the walk normalizes the joined path's components as the branch did. Witnesses: regress/include-glob-escapes, include-glob-literals, include-glob-diacritics and cov9-include-glob print identically to main's oracle, and the C++ binary resolves the same six escaped includes of the first. Whole-corpus check. The merged oracle and main's oracle were run over every file of main's test/regress corpus (4417 files); exactly five differ, and on each the C++ binary sides with the merged oracle: 1029 and 1114 (rejected as unbalanced, which C++ rejects too, "Unbalanced remainder is:"), 1036 (rejection named as a missing directive argument, as C++ names it), and 1660 and 1670 (a missing include reported, which C++ reports and regress/1670 pins, where main's engine, which handles no include directive, accepts the file silently). The five divergences are departures of main's oracle from C++ that the series engine already recorded, not regressions of the merge. The axiom budget is unchanged: `#print axioms Ledger.Journal.run` names propext, Classical.choice and Quot.sound only, and `nix build .#oracle` is green. Co-Authored-By: GLM (Z.ai) via pi <noreply@z.ai> Pi-Session: 01a163ec-1792677793
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
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.
Follow-up to #11. The merge commit 37d7f9d resolved the engine regions by splicing the branch engine wholesale, which dropped four behaviors of main: the exact lot-basis gain (5376d29), the swap-cost plumbing (6c6942e, stubbed as declared but never set or read), the commBlock name fix (3313 series), and literal-escape reading of include glob patterns. Cross-oracle comparison over main's whole regress corpus also exposed that the series engine predated the per-group balancing of C++ PR 3317.
This commit ports each behavior into the branch architecture and witnesses every one against the C++ main binary (5f9855cef, containing PR 3317 and the fix of issue 3258):
10 GAL {$2.00} @@ $25.30balances to$-20; regress/3258, 3258_computed, 1773, 2975, 3013, 1217 print identically to main's oracle.USD|-10|Equityas C++ does.Whole-corpus check: the merged oracle and main's oracle were run over every file of main's test/regress corpus (4417 files); exactly five differ, and on each the C++ binary sides with the merged oracle: 1029 and 1114 (rejected as unbalanced, which C++ rejects), 1036 (rejection named as a missing directive argument, as C++ names it), 1660 and 1670 (a missing include reported, which C++ reports and regress/1670 pins, where main's engine, which handles no include directive, accepts the file silently). These five are departures of main's oracle from C++, not regressions of the merge.
The axiom budget is unchanged (propext, Classical.choice, Quot.sound) and
nix build .#oracleis green.