From 11154991b402fa16549ebccab61515944df5ca0f Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 20 Oct 2026 20:44:45 -0700 Subject: [PATCH 1/2] Read a format sample's bare commodity symbol C++ Ledger now lets a commodity block's format sub-directive spell the block's symbol bare, as the commodity header does, although an amount must quote it (ledger/ledger#3312): `commodity N1` with `format 1,000.00 N1` declares the display precision of N1. This reader took the bare N1 for a malformed commodity and skipped the format line, so N1 kept the precision its postings had taught it. Before parseAmount reads the sample, quote a bare occurrence of the block's symbol at either end of it, under the C++ conditions: the symbol needs quotes by the C++ table (commodity.cc invalid_chars, which is not this reader's validCommodity), the sample quotes nothing itself, and the symbol does not run into the number between two characters of a number. The witness is regress/3312, whose N1 balance rounds to the format's two places only under this rule. Verified as follows. `nix build .#oracle` exits 0, so every proof checks. test/semantic/check_all.py, run with the fixed C++ build against this oracle over the whole C++ suite, reports 3800 PASS and 0 FAIL (491 negative, 77 without a journal, 2 with Python). The same run against f5d891e fails on exactly regress/3312, where the oracle keeps 1234.567 N1 and C++ rounds to 1234.57. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01CBCCbSZ9jNESexSR5iwBDC --- Ledger/Journal.lean | 6 ++++-- Ledger/Parse.lean | 40 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 44 insertions(+), 2 deletions(-) diff --git a/Ledger/Journal.lean b/Ledger/Journal.lean index 3508666..3d715c2 100644 --- a/Ledger/Journal.lean +++ b/Ledger/Journal.lean @@ -1614,8 +1614,10 @@ def run (input0 : String) (dcDefault : Bool := false) continue else if body.startsWith "format " then -- the format subdirective DECLARES the display precision - -- and locks it against migration (opt-round, 1795, 628) - let sample := trimS (body.drop "format ".length).toString + -- and locks it against migration (opt-round, 1795, 628); + -- it may spell the block's symbol bare (3312) + let sample := + quoteBareSymbol (trimS (body.drop "format ".length).toString) comm match (parseAmount st.amt n sample) with | .ok r => st := lockPrecision st diff --git a/Ledger/Parse.lean b/Ledger/Parse.lean index ecd48c2..4e49492 100644 --- a/Ledger/Parse.lean +++ b/Ledger/Parse.lean @@ -349,6 +349,46 @@ def resolveCommodity (line : Nat) (raw : String) : Except String String := do if validCommodity raw then pure raw else err line s!"malformed commodity '{raw}'" +/-- Does an amount have to quote this symbol? The C++ table, not this + reader's `validCommodity`: commodity.cc `invalid_chars`, the + characters that end a bare symbol there. -/ +def symbolNeedsQuotes (s : String) : Bool := + s.toList.any fun c => + c.isDigit || c == ' ' || c == '\t' || c == '\n' || c == '\r' + || c.toNat == 127 || "!&()*+,-./:;<=>?@[]^{|}~".toList.contains c + +/-- Would a bare symbol and a number that meet at characters `a` and + `b` run together? Only when both are characters `parse_quantity` + reads as part of a number (amount.cc). -/ +def runsTogether (a b : Char) : Bool := + let inNumber (c : Char) : Bool := + c.isDigit || c == '.' || c == ',' || c == '\'' + inNumber a && inNumber b + +/-- A `format` sample may spell its block's symbol bare, as the + `commodity` header does, though an amount must quote it: + `commodity N1` with `format 1,000.00 N1` (regress/3312; + textual_directives.cc `quote_bare_symbol`). The bare symbol is + quoted at either end of the sample, unless the sample quotes + already or the symbol runs into the number (`N11,000.00`), where + nothing marks where it ends. -/ +def quoteBareSymbol (sample sym : String) : String := + if !symbolNeedsQuotes sym || sample.contains '"' then sample else + let s := sample.toList + let y := sym.toList + let n := y.length + let quoted := "\"" ++ sym ++ "\"" + let touches (a b : Option Char) : Bool := + match a, b with + | some a, some b => runsTogether a b + | _, _ => false + if s.take n == y && !touches y.getLast? (s.drop n).head? then + quoted ++ String.ofList (s.drop n) + else if s.length > n && s.drop (s.length - n) == y + && !touches (s.take (s.length - n)).getLast? y.head? then + String.ofList (s.take (s.length - n)) ++ quoted + else sample + /-! ## Amounts -/ /-- Style/definition context threaded through amount parsing. -/ From 8342e12109fc7654c542efa1b9d12333088bee91 Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Wed, 21 Oct 2026 22:36:59 -0700 Subject: [PATCH 2/2] End an account header's name at a hard-separated comment The journal engine took the whole remainder of an `account` line as the name it declares, so `account Expenses:Food ; groceries` declared `Expenses:Food ; groceries`. The fix for ledger/ledger#3320 has the C++ reader end the name at the first `;` that follows a hard separator, a tab or two or more spaces, which begins a comment there as it does after the payee on a transaction's first line (`split_inline_note` in utils.h, called by `account_directive_body`). A `;` after a single space, or after none, stays part of the name, as it does in a posting's account. The two readings differed only when such a header's block held an `alias`, `payee` or `default` line, which then named a different account on each side. `headerAccount` applies that rule to the `account` header, to its deprecated `@account` and `!account` spellings, and to a nested `account` line inside an account block, after skipping the blanks before the name as C++ does, so `account ; x` still names `; x`. The witness is regress/3320_3 on the ledger branch johnw/fix-3320. With this oracle and that branch, test/semantic/check_all.py reported 3802 PASS and 0 FAIL over 4374 test files, with both ratchet bins empty, and with this oracle and ledger main at d39fccd8b it reported 3799 PASS and 0 FAIL over 4370. With the oracle at f5d891e, the branch failed exactly regress/3320_3. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01FypysHp6zVrvs3VFThm468 --- Ledger/Journal.lean | 11 ++++++++--- Ledger/Parse.lean | 18 ++++++++++++++++++ 2 files changed, 26 insertions(+), 3 deletions(-) diff --git a/Ledger/Journal.lean b/Ledger/Journal.lean index 3d715c2..5c46a68 100644 --- a/Ledger/Journal.lean +++ b/Ledger/Journal.lean @@ -1578,7 +1578,9 @@ def run (input0 : String) (dcDefault : Bool := false) let frames := frames.filter fun (i, _) => i < ind let name := ((frames.head?).map (·.2)).getD "" if body.startsWith "account " then - let nm := trimS (body.drop "account ".length).toString + -- a nested name ends before a hard-separated `;` comment, as + -- a top-level one does (regress/3320) + let nm := headerAccount (body.drop "account ".length).toString let nm := (unquote nm).getD nm let full := if name.isEmpty then nm else name ++ ":" ++ nm st := { st with pending := .acctBlock ((ind, full) :: frames) } @@ -1757,14 +1759,17 @@ def run (input0 : String) (dcDefault : Bool := false) || t.startsWith "b " then continue -- historical timelog compatibility: ignored else if t.startsWith "@account " || t.startsWith "!account " then - let nm := trimS (t.drop "@account ".length).toString + -- read as a plain `account` header (regress/3320_3) + let nm := headerAccount (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 (headerSymbol nm) } else if t.startsWith "account " || t.startsWith "account\t" then - let nm := trimS (t.drop "account ".length).toString + -- the name ends before a `;` that follows a hard separator, + -- which begins a comment (regress/3320, regress/3320_3) + let nm := headerAccount (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 diff --git a/Ledger/Parse.lean b/Ledger/Parse.lean index 4e49492..e8a1f08 100644 --- a/Ledger/Parse.lean +++ b/Ledger/Parse.lean @@ -183,6 +183,24 @@ def splitField (s : String) : String × Option String := def trimS (s : String) : String := s.trimAscii.toString +/-- The account that an `account` line names: the text up to the first + `;` that follows a hard separator (a tab, or two or more spaces), + which begins a comment, as a note begins after a transaction's + payee. A `;` after a single space, or after none, is part of the + name, as it is in a posting (C++ `split_inline_note` in utils.h, + called by `account_directive_body`; regress/3320). -/ +def headerAccount (s : String) : String := + let rec go (spaces : Nat) (tab : Bool) : List Char → List Char + | [] => [] + | ';' :: rest => + if tab || spaces ≥ 2 then [] else ';' :: go 0 false rest + | ' ' :: rest => ' ' :: go (spaces + 1) tab rest + | '\t' :: rest => '\t' :: go spaces true rest + | c :: rest => c :: go 0 false rest + -- the scan starts at the name, as C++ skips the blanks before it + let cs := s.toList.dropWhile fun c => c == ' ' || c == '\t' + trimS (String.ofList (go 0 false cs)) + /-! ## Numbers under commodity styles -/ private def digitsVal (cs : List Char) : ℕ :=