v1.4.8 — Add a Python companion notebook
Added lean_book/python-companion/python_companion.ipynb, collecting
every “Programmer’s corner (Python)” snippet in the book (8 snippets
across 6 chapters) into one runnable notebook that opens directly in
Google Colab, no Lean installation required. Each snippet is verified to
run and produce the output the book’s comments claim. Linked from the
book’s README reference list.
v1.4.8 — Full-book review pass for plain academic prose
Follow-up to the “Why Lean?” rewording: a full read-through of every
chapter’s prose turned up 7 further passages using a simile, metaphor,
or rhetorical framing in place of a direct statement of fact — a
“smallest possible dose” metaphor for Fin being a minimal dependent
type, a “referee” simile for why this book uses structure instead of
class, a “beating heart” metaphor for the path category being the
essential content of the path-algebra construction, a “training wheels”
metaphor for exercises without worked-example guidance, and two
rhetorical framings (“exactly the wrong thing to hide,” “keeps… and
deliberately breaks…”) in the Mathlib note. Each was rewritten as a
plain, direct statement. Everything else in the book was already in
this register.
v1.4.8 — Plainer prose in “Why Lean?”
Reworded the opening paragraph of Chapter 0 §2 (“Why Lean?”), which used a simile (“the way a compiler checks types”) in place of a direct statement — flagged as reading as performative rather than academic. Rewritten as a plain, direct statement of what Lean is and how proof checking works.
v1.4.8 — Fix scrambled Unicode symbols in code listings ({α → α{, etc.)
Found while proofreading a rendered page: Chapter 1’s
def identity {α : Type} (x : α) : α := x example rendered as
identity α{ : Type} ... – the opening brace and the following symbol
visually swapped. Isolating this in minimal standalone test files (same
technique used for the two listings bugs below) showed it’s much
broader than that one example: listings, under XeTeX, scrambles
character order and drops surrounding whitespace whenever two of this
book’s newunicodechar-mapped symbols sit near each other with nothing
but a space between them and no plain ASCII character in between –
e.g. α → Vec (from Chapter 1’s Vec.replicate example) rendered as
α→ Vec. This reproduced identically regardless of columns=fixed vs
flexible (the previous entry’s fix), regardless of whether the
substitution went through newunicodechar or a listings literate
rule, and even with a font that has native glyphs for these symbols and
no substitution mechanism at all – so it’s a listings/XeTeX column-
bookkeeping bug specific to non-ASCII characters, not fixable by tuning
any of listings’ own options.
The fix: every occurrence of one of these symbols inside a
\begin{lstlisting} body is now routed through listings’
escapeinside={(*}{*)} as real LaTeX (e.g. α becomes
(*$\alpha$*)), so listings treats it as an opaque pre-rendered span
instead of a character it measures and positions itself –
build_latex.py’s new escape_lstlisting_unicode(). newunicodechar
remains in place for every other context (inline `code` spans,
table cells), where it already worked correctly.