v1.4.23 — Add dbg_trace tracing to every genuinely recursive Lean block
Completes the dbg_trace initiative: every Lean code block in the book
was surveyed chapter by chapter, and every genuine recursion found now
has a dbg_trace-annotated sibling definition showing the computation
unwind one step at a time, with prose explaining what each printed line
means.
Chapter 1 (01-basics/) is the pattern-setting installment. Surveyed
all 28 Lean code blocks across the chapter’s six files first. Only three
have real recursion: Vec.replicate, Vec.dot (recursing on two Vecs
at once, accumulating a running total — this also needed a genuine
same-length worked example added, since the book had previously only
ever shown its type-error case), and double (recursion hidden inside
Nat.rec rather than a visible self-call).
A real limitation was found and documented rather than glossed over:
myLength (computed via List.rec under #reduce, since its code
generator can’t compile List.rec directly) cannot be traced with
dbg_trace at all — verified empirically that kernel-level reduction
silently skips the trace’s side effect entirely, unlike #eval.
Chapter 10 (10-modules/): natSmul, recursion on Nat via
Group.op, verified against the real intGroup (Chapter 6).
Chapter 11 (11-path-algebras/): Path.append and Path.length.
Path has no Repr instance, so Path.append’s recursion can’t be
observed in isolation — traced together with Path.length in the
checkpoint project, the one place both exist together, with a
forward-pointing note added where Path.append is first defined.
Chapter 14 (14-appendix-solutions/): Vec.toList (mirroring
Chapter 1) and the duplicate Path.length/Path.append worked solution
(mirroring Chapter 11’s checkpoint project).
Chapters confirmed to need no changes at all (surveyed and found to
contain only structure/instance declarations, tactic-mode
induction/cases proofs, and single-step pattern matches, none of
which are traceable or benefit from dbg_trace): 2, 3, 4, 5, 6, 7, 8, 9,
12, 13, and the rest of 14.
All Lean snippets verified directly against the toolchain pinned in this
repository’s lean_project/lean-toolchain (v4.31.0), run as one
cumulative script matching how each chapter’s snippets actually
accumulate.