v1.6.1 — Companion-project verification and history backfill

Changelog — v1.6.1

← Changelog index

---

v1.6.1 — Companion-project verification and history backfill

A follow-up to v1.6.0, closing loose ends discovered while auditing it.
No book text or worked example changed; this release covers the
companion Lean project and repository meta-documentation only.

Fixes

• lean_project gaps closed. Two code blocks the book claims are
  "ported into lean_project/ and verified with lake build" had never
  actually been ported: the Chapter 3 exercise solutions
  (Rectangle/area, Box/unwrap, ColoredRectangle) added in
  v1.6.0, and the Chapter 1, Section 3 vecLen/vecLen' comparison.
  Both are now in lean_project/LeanProject/, and every #eval/#check
  output was checked to match the book exactly.
• Full project build verified. A complete lake build (8681 jobs,
  including every Mathlib-dependent module) passes clean against
  master post-Chapter-1-split, resolving issue
  #246.
  This also resolves issue
  #242.
• Closed issue #243
  (cutting a standalone v1.5.4 release), superseded by v1.6.0.
• Root README off-by-one. "Mathlib equivalent" boxes actually start
  in Chapter 7 (07-groups/), not Chapter 6 as the README said in two
  places, the same pre-split-regression pattern already fixed for the
  checkpoint-project reference in v1.6.0.

Housekeeping

• PROJECT-HISTORY.md backfilled. Its merged-PR table had stopped
  at #159; added the 34 PRs merged since (through v1.6.0/#247), updated
  the issue/PR counts (97 issues → 148, 63 PRs → 97), and added a
  summary bullet for the v1.6.0 work.

Compare v1.6.0...v1.6.1

---

← Changelog index