From 0a743b64b7df1e8b637549cf9507514e0941df1e Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 20 Oct 2026 21:10:25 -0700 Subject: [PATCH] Read a commodity header's symbol as its first token 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 Claude-Session: https://claude.ai/code/session_01Mbne6AZZDzKMQcQV6Cp9Sn --- Ledger/Journal.lean | 11 ++++++++--- Ledger/Parse.lean | 35 +++++++++++++++++++++++++++++++++++ 2 files changed, 43 insertions(+), 3 deletions(-) diff --git a/Ledger/Journal.lean b/Ledger/Journal.lean index 17113e2..43654ca 100644 --- a/Ledger/Journal.lean +++ b/Ledger/Journal.lean @@ -1599,7 +1599,9 @@ def run (input0 : String) (dcDefault : Bool := false) | .commBlock comm => let body := trimS t if body.startsWith "alias " then - let al := trimS (body.drop "alias ".length).toString + -- a `;` outside quotes begins a comment (regress/3313_2) + let al := trimS (stripCommodityComment + (body.drop "alias ".length).toString) let al := (unquote al).getD al st := { st with commAliases := (al, comm) :: st.commAliases } continue @@ -1749,14 +1751,17 @@ def run (input0 : String) (dcDefault : Bool := false) let nm := trimS (t.drop "@account ".length).toString st := { st with pending := .acctBlock [(0, (unquote nm).getD nm)] } else if t.startsWith "@commodity " || t.startsWith "!commodity " then + -- read as a plain `commodity` header (regress/3313) let nm := trimS (t.drop "@commodity ".length).toString - st := { st with pending := .commBlock ((unquote nm).getD nm) } + st := { st with pending := .commBlock (headerSymbol nm) } else if t.startsWith "account " || t.startsWith "account\t" then let nm := trimS (t.drop "account ".length).toString st := { st with pending := .acctBlock [(0, (unquote nm).getD nm)] } else if t.startsWith "commodity " || t.startsWith "commodity\t" then + -- the symbol is the first token, and a `;` ends a bare one + -- (regress/3313) let nm := trimS (t.drop "commodity ".length).toString - st := { st with pending := .commBlock ((unquote nm).getD nm) } + st := { st with pending := .commBlock (headerSymbol nm) } else if t.startsWith "payee " || t.startsWith "tag " then st := { st with pending := .ignoreBlock } -- label declarations else if t.startsWith "@" || t.startsWith "!" then diff --git a/Ledger/Parse.lean b/Ledger/Parse.lean index 763ff77..ecd48c2 100644 --- a/Ledger/Parse.lean +++ b/Ledger/Parse.lean @@ -297,6 +297,41 @@ def unquote (s : String) : Option String := else none | _ => none +/-- The commodity that a `commodity` header names: a quoted symbol up + to its closing quote, or else the leading run of characters up to + whitespace or a `;`, which begins a comment. As in an amount, a + backslash puts the character after it into the run, so `A\;B` names + `A;B`, and the rest of the line is ignored (C++ + `commodity_t::parse_symbol(char*&)`, regress/3313). -/ +def headerSymbol (s : String) : String := + match s.toList with + | '"' :: rest => String.ofList (rest.takeWhile (ยท != '"')) + | cs => + let rec go : List Char โ†’ List Char + | [] => [] + | '\\' :: c :: rest => c :: go rest + | c :: rest => + if c == ' ' || c == '\t' || c == ';' then [] else c :: go rest + String.ofList (go cs) + +/-- Cut the comment from the argument of a commodity block's `alias` + line. It begins at the first `;` that is neither inside a quoted + symbol nor escaped with a backslash, the only places that a + commodity symbol can hold one (C++ `strip_commodity_comment` in + textual_directives.cc, regress/3313_2). -/ +def stripCommodityComment (s : String) : String := + let rec go (quoted : Bool) : List Char โ†’ List Char + | [] => [] + | '"' :: rest => '"' :: go (!quoted) rest + | ';' :: rest => if quoted then ';' :: go quoted rest else [] + | '\\' :: rest => + if quoted then '\\' :: go quoted rest + else match rest with + | c :: rest' => '\\' :: c :: go quoted rest' + | [] => ['\\'] + | c :: rest => c :: go quoted rest + String.ofList (go false s.toList) + /-- Time-unit commodities canonicalize to seconds. -/ def timeFactor (s : String) : Option โ„š := if s == "s" then some 1