Repository navigation
Conversation
The journal engine took the whole remainder of a `commodity` line as the symbol it declares, so `commodity USD dollars` declared `USD dollars` and `commodity N1 ; foo` declared `N1 ; foo`. The C++ reader has only ever taken the first token there, in commodity_t::parse_symbol(char*&), and the fix for ledger/ledger#3313 also ends a bare symbol at a `;`, which begins a comment, as a `;` does after an amount in a posting. The two readings differed only when a header carried trailing text and its block declared an alias, which then named a different commodity on each side. The same issue has the C++ side strip a `;` comment from the argument of a commodity block's `alias`, which the oracle kept as part of the alias. `headerSymbol` reads a quoted symbol up to its closing quote, or else the leading run up to whitespace or a `;`, where a backslash puts the next character into the run, as in an amount and as C++ now does, so `A\;B` names `A;B`. `stripCommodityComment` cuts an alias argument at the first `;` that is neither inside a quoted symbol nor escaped. The account block is unchanged, because an account name may contain a `;`, and the `format` branch is unchanged, because `parseAmount` already leaves a trailing comment in the unread tail. The witnesses are regress/3313 and regress/3313_2 on the ledger branch johnw/fix-3313. With this oracle and that branch, test/semantic/check_all.py reported 3802 PASS and 0 FAIL over 4373 test files, with both ratchet bins empty. With the oracle at f5d891e, the same branch failed exactly those two files. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Mbne6AZZDzKMQcQV6Cp9Sn
This was referenced Oct 21, 2026
4 tasks done
igbanam
pushed a commit
to igbanam/ledger
that referenced
this pull request
Oct 31, 2026
The oracle took the whole remainder of a `commodity` line as the symbol it declares, so `commodity USD dollars` declared `USD dollars` there but `USD` in C++, and it kept a `; comment` as part of the alias in a commodity block's `alias` line. ledger/ledger-semantics#6 reads the header's first token, ending a bare symbol at a `;` as the next commit makes C++ do, and strips such a comment from an alias, as the commit after it does in C++. The bisimulation then agrees with C++ on regress/3313 and regress/3313_2, added with those commits. Both pins move together, as the flake comment requires: the flake input and the lean/ submodule now name ledger-semantics 0a743b6, the head of that pull request, one commit on top of f5d891e. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Mbne6AZZDzKMQcQV6Cp9Sn
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.
Summary
commodityheader now names the commodity of its first token: a quoted symbol up to its closing quote, or else the leading run up to whitespace or a;, which begins a comment, where a backslash puts the next character into the run as in an amount (headerSymbol). The engine took the whole remainder of the line, socommodity USD dollarsdeclaredUSD dollarsandcommodity N1 ; foodeclaredN1 ; foo, while C++ has only ever taken the first token (commodity_t::parse_symbol(char*&)). The two readings differed only when the header carried trailing text and its block declared an alias, which then named a different commodity on each side.;comment is cut from the argument of a commodity block'salias(stripCommodityComment): the first;that is neither inside a quoted symbol nor escaped. The account block is unchanged, because an account name may contain a;, and theformatbranch is unchanged, becauseparseAmountalready leaves a trailing comment in the unread tail.commoditydirective is weird:;treatment ledger#3313, wherecommodity N1; foodeclared a commodity namedN1;. C++ now ends a bare directive symbol at a;and strips such a comment fromaliasandformatarguments.test/regress/3313.test(plain,@and!headers with trailing comments, each block binding an alias) andtest/regress/3313_2.test(commentedaliaslines) in ledger/ledger. Each rule's comment cites its test and the C++ function it mirrors.ledger/ledger#3318, which fixes C++, moves both pins (the flake input and the
lean/submodule) to this branch's commit,0a743b6. The change for ledger/ledger#3312 (ledger/ledger#3316, with #5 here) edits only the commodity block'sformatbranch, so the two compose; whichever ledger pull request merges second re-pins to amainthat holds both rules. Please merge this with a merge commit, as #1 and #2 were, so that commit stays reachable frommain.Test plan
nix build .#oracle -L: the build completes, so every proof checks and no warning was raisedtest/semantic/check_all.py): 3802 PASS, 0 FAIL, 0 out-of-scope, 0 cpp-parse (492 negative, 77 no-journal, 2 python)f5d891e, the same run fails on exactly3313.testand3313_2.test(for exampleonly_oracle: N1 ; foo|1234.5|Assets:Cash,only_cpp: N1|1234.5|Assets:Cash)🤖 Generated with Claude Code
https://claude.ai/code/session_01Mbne6AZZDzKMQcQV6Cp9Sn