Max-testing pass, steps 2-4. Spec-blind tests (rank 1-2): four agents, each given only the specs and the public interface (doc comments and signatures, every body removed, never src/ or the existing tests), wrote tests/spec_reports.rs (62), spec_ledger.rs (72), spec_arap.rs (42), spec_assets_payroll.rs (50): hand-computed examples per scenario and a proptest law per invariant (conservation, partition, invariance, scaling, reversal cancels, "a refusal leaves the books unchanged" over random invalid commands). They found: 1. A refused payroll run changed the books: an all-zero run passed validation, then failed at post after creating seven payroll accounts and using up an entry id. validate_payroll_lines now refuses a run with no gross pay. 2. A refused add_account used up an account id (empty code, duplicate, unknown parent). The id is now taken only when the account is added. 3. Stale prose: close_period_to and members_equity still described the old last-member rounding. 4. Open (left #[ignore]d pending Stephen): depreciation_schedule's doc says "through the month containing" the date; the code prorates that month by days. GnuCash oracle (rank 3, an oracle never the spec): `just oracle` builds GnuCash 5.10 in a container pinned by base digest and package versions (oracle/gnucash/) and runs tests/oracle_gnucash.rs: 200 seeded random books built through wanderbooks (entries, foreign lines, reversals, monthly closes), every account's balance at month ends and random dates and each month's P&L, compared exactly: 15,800 comparisons. First run: 4,724 differences, all from foreign lines; without them, zero. Adjudicated from principles (rules.md B-3): wanderbooks booked foreign * rate unrounded ($108.34567); a ledger in one money holds no fractions of its smallest unit, and its cash must match a bank. Stephen decided: book in the base currency's minor unit, half away from zero. add_line_fx now rounds; minor units per ISO 4217 list one (2026-09-17, SIX), generated into Currency::minor_units and recorded in docs/spec/sources/iso-4217.md. Replay now takes the journaled base amount (replay_add_line_fx), so lines booked before replay exactly as booked (contract: books_written_under_older_rules_still_open). Now: zero differences, foreign lines included. Tests: 449, from 223. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX
86 lines
3.3 KiB
Makefile
86 lines
3.3 KiB
Makefile
# wanderbooks repo recipes. `just` lists them.
|
|
|
|
set shell := ["bash", "-cu"]
|
|
|
|
# The Netlify CLI, fetched on demand.
|
|
netlify := "npx --yes netlify-cli@27"
|
|
|
|
# List recipes
|
|
default:
|
|
@just --list
|
|
|
|
# Everything CI should check: format, clippy and rustdoc (zero warnings), tests
|
|
check:
|
|
cargo fmt --all --check
|
|
cargo clippy --workspace --all-targets -- -D warnings
|
|
RUSTDOCFLAGS="-D warnings" cargo doc --workspace --no-deps --quiet
|
|
cargo test --workspace
|
|
|
|
# Formal proofs: Kani on the accounting kernel, Lean for books of any size (docs/verification.md)
|
|
prove:
|
|
#!/usr/bin/env bash
|
|
set -euo pipefail
|
|
# Capped: a harness that blows up should fail, not eat the machine.
|
|
log=$(mktemp)
|
|
(ulimit -v 12000000; cd crates/ledger-core &&
|
|
timeout 1800 cargo kani -j "$(nproc)" --output-format terse | tee "$log")
|
|
# A cover that can't be satisfied means a proof is vacuous.
|
|
if grep -E "\*\* [0-9]+ of [0-9]+ cover properties satisfied" "$log" |
|
|
awk '{ if ($2 != $4) bad = 1 } END { exit !bad }'; then
|
|
echo "Kani: an unsatisfiable cover; some proof is vacuous" >&2
|
|
exit 1
|
|
fi
|
|
rm -f "$log"
|
|
cd verify/lean
|
|
lake build
|
|
audit=$(lake env lean Audit.lean)
|
|
if grep -v -E "depends on axioms: \[(propext|Quot.sound|Classical.choice)(, (propext|Quot.sound|Classical.choice))*\]$|does not depend on any axioms" <<<"$audit"; then
|
|
echo "Lean audit: a theorem rests on something beyond the standard axioms" >&2
|
|
exit 1
|
|
fi
|
|
echo "Lean: $(wc -l <<<"$audit") headline theorems, standard axioms only"
|
|
|
|
# Cross-check against GnuCash (an oracle, never the spec): random books through
|
|
# wanderbooks and through GnuCash 5.10 in a pinned container. Needs Docker.
|
|
oracle:
|
|
docker build -q -t wanderbooks-gnucash-oracle oracle/gnucash
|
|
cargo test -p ledger-core --test oracle_gnucash -- --ignored --nocapture
|
|
|
|
# Build the release binaries (CLI, MCP server, GUI)
|
|
build:
|
|
cargo build --release -p ledger-cli -p ledger-mcp -p ledger-gui
|
|
|
|
# Install the binaries from this checkout into ~/.cargo/bin
|
|
install:
|
|
for c in ledger-cli ledger-mcp ledger-gui; do cargo install --locked --path crates/$c; done
|
|
|
|
# Open the GUI on the demo company
|
|
demo:
|
|
cargo run --release -p ledger-gui -- --demo
|
|
|
|
# Regenerate the website's screenshots (dark) from the demo company
|
|
site-shots:
|
|
#!/usr/bin/env bash
|
|
set -euo pipefail
|
|
tmp=$(mktemp -d)
|
|
SHOT_DIR="$tmp" SHOT_DARK=1 SHOT_LIVE=1 SHOT_ONLY=overview,pnl,cash cargo test -p ledger-gui --test screens
|
|
# The hero's viewer pane: taller, to sit beside the session.
|
|
SHOT_DIR="$tmp" SHOT_DARK=1 SHOT_LIVE=1 SHOT_ONLY=entry SHOT_ENTRY=245 SHOT_HEIGHT=1150 cargo test -p ledger-gui --test screens
|
|
for f in overview entry pnl cash; do cp "$tmp/$f.png" site/assets/; done
|
|
rm -f site/assets/overview-dark.png
|
|
rm -rf "$tmp"
|
|
|
|
# Assemble the website in site/dist (index.html, install.sh, assets)
|
|
site:
|
|
rm -rf site/dist && mkdir -p site/dist
|
|
cp site/index.html install.sh site/dist/
|
|
cp -r site/assets site/dist/
|
|
|
|
# Deploy the website to wanderbooks.ai (Netlify; `netlify login` once first)
|
|
deploy: site
|
|
{{netlify}} deploy --prod --dir site/dist --no-build
|
|
|
|
# Deploy a preview of the website and print its URL
|
|
deploy-preview: site
|
|
{{netlify}} deploy --dir site/dist --no-build
|