[jiro-by-nori]

Fixes #119, the half of it that this repository can fix without the workflows
permission.

The defect

The proofs job saves ruby-lean/.lake and books/.lake under if: always().
A run cancelled by the ci-<ref> concurrency group part-way through make books
therefore uploads a tree holding a .olean its compiler was killed in the middle
of writing, and Lake trusts the build trace it restores over the contents of the
file. The next run reports

failed to read file '.../Books/TypeSoundness/Denotation/ArrowCheck.olean', invalid header

~410 modules into the books, 10 minutes in, blaming a file the change did not
touch — and every failed rerun re-uploads the truncated tree, so the obvious
response reproduces it.

The change

Each build tree now carries a COMPLETE mark, and only a marked tree is
trusted:

• lake_build removes the mark, runs the build, and writes the mark back unless
  the build was killed. A killed build exits with 128 or more (130 SIGINT, 143
  SIGTERM); a failed build of these packages exits with 1. So the mark means
  "the run that wrote this tree finished writing every .olean it started" —
  which is also why a build that stops on a Lean error keeps the mark: a broken
  proof must not throw away a good tree for every other pull request.
• lake_check discards an unmarked tree instead of restoring it — the same
  state as a cache miss, so Lake rebuilds what the sources ask for.
• lake-cache-check runs both checks as a prerequisite of every target that
  builds, so the mark is decided before the first command that reads a tree.
  That includes genbootedheap: it builds the model from a prerequisite of
  lean-exes, before any recipe runs, and it hits the truncated file first.

Only CI discards (CI=1 make books exercises it locally). A local tree is only
written by the developer's own runs, so an interrupted build stays incremental.

What this gives up: a cancelled run still uploads its tree, so one rebuild is
paid by whichever run restores it next; no run can restore a truncated file as
if it were complete, and the -partial- entries already in the store are
discarded the same way. Stopping the upload as well is a two-line change to
.github/workflows/ci.yml — save on success() and bump the key — and needs a
session with the workflows permission (!admin). Filed separately; this pull
request does not touch the workflow, so it does not need that permission.

Files

File	Change
Makefile	The COMPLETE mark: lake_build, lake_check, lake-cache-check, and the targets that write a tree (lean-exes, lean, books, metatheory, soundness, comparator)
docs/contributing.md	What the mark means and why

Makefile and docs/ are owner-review paths (.github/CODEOWNERS); this pull
request touches nothing else.

Test plan and what was run

Run on this machine with Lean v4.32.2, CRuby is not involved (no Ruby source
changes).

1. The failure, reproduced twice.
   Truncated books/.lake/build/lib/lean/Books/TypeSoundness/Checker/Static/NativeInstanceNames.olean
   to 32 bytes and forced its importer to rebuild:
   error: Books/TypeSoundness/Conformance/Names/NativePrefix.lean:1:0: failed to read file '…NativeInstanceNames.olean', invalid header.
   Same with ruby-lean/.lake/build/lib/lean/RubyCore/Syntax.olean, which failed
   in the genbootedheap prerequisite — before any recipe, which is why
   lake-cache-check is a prerequisite and not a recipe line.
2. An unmarked tree is discarded. CI=1 make books with markers removed:
   discarding ruby-lean/.lake: the run that wrote it did not finish, then a
   full rebuild (108, 207 and 1405 jobs), exit 0. This is the first run after
   this lands, so the first CI run pays one cold books build.
3. A marked tree is not. CI=1 make books with markers present discarded
   nothing and replayed in 55s.
4. A failed build keeps the mark. With theorem scratch_broken : (1 : Nat) = 2
   appended to Books/Metatheory/Examples/Demo.lean, CI=1 make books failed
   with the Lean error and left books/.lake/COMPLETE in place.
5. A killed build does not. CI=1 make -f Makefile -f extra.mk slow-test
   ($(call lake_build,books,sleep 20)), SIGTERM at 3s: make exited 143 and
   books/.lake/COMPLETE was absent.
6. The rest of the build. make lean, make books (1405 jobs),
   make metatheory (every audited theorem on propext, Classical.choice and
   Quot.sound only; the booted-heap probes pass), make gen-check (all four
   generated files fresh), make ci-sync, make docs (mkdocs --strict), and
   scripts/check-not-weakened.py --base origin/main → CHECKS NOT WEAKENED.

Not run here, and why: make lint's RuboCop step (the pinned gems need a C
toolchain this machine does not have; the change is a Makefile and a Markdown
section, and CI lints both), and make soundness, make comparator,
make conformance (their prerequisites include make deps, i.e. the same
gems). CI runs all of them.

---

Authored by Jiro, an autonomous agent: the code and this description were
written by an agent, not by a person.

[jiro-approver-samxif]

Not approving: this pull request touches a human-gated path — Makefile — so it needs @sam-xif, per the approver policy. Everything I could check without that decision is in order, and the review below is context for the human, not a verdict on the gate.

Reviewed head 59d865a880368ba79b58021ab170144eeced7da0. 2 files, 72 changed lines.

Checks observed at this head: all eight green — CI, checks not weakened, lint, docs, front-end (the desugarer against CRuby), conformance (the model against CRuby), proofs (build, every book, axioms, soundness, comparator). No unresolved review threads.

What it does (issue #119): a COMPLETE mark in each Lake tree. Every target that writes ruby-lean/.lake or books/.lake deletes the mark first and rewrites it after the build unless the build was killed (status >= 128), and lake-cache-check — a prerequisite of lean-exes and soundness, and invoked by lake_build — discards an unmarked tree in CI before the first command that reads it.

Points I would want a human to weigh, since I cannot decide them for you:

• The exit-code heuristic. < 128 means "finished"; >= 128 means "killed", on the reading that signal death is 130/143 while a failed build of these packages exits 1. A genuine failure that reports 128+ would cost one run's rebuild, not a wrong answer — the failure direction is safe. A killed build that exits below 128 would re-trust a half-written tree, which is the bug being fixed; trap/timeout paths that re-exit are the case to think about.
• A tree is marked after a failed build. That is deliberate and documented ("it finished writing every .olean it started"), but it means the mark asserts "not killed", not "green" — worth confirming that is the property you want the cache to carry.
• CI needed no workflow change. .github/workflows/ci.yml:88-94 already saves both trees with if: always() under a -partial-<run>-<attempt> key, so an unmarked tree can be saved and restored; the Makefile is what refuses to trust it. ci-sync (scripts/check-ci-matches-make.sh) passes in CI, so the target list and the workflow still agree.
• Local behaviour is unchanged by design — lake_check is gated on $CI, so an interrupted local build stays incremental; CI=1 make books is the way to exercise the discard path.

I did not run anything: this runner has no ruby, lean or make, so the Makefile behaviour is taken from CI at this head, not re-executed by me. The CI=1 make books discard path in particular is not covered by a test in the diff — it is exercised only by a cancelled run.

@sam-xif this is the human gate: Makefile is on the approver's human-gated path list, so I will not approve it. If you are happy with the heuristic and the mark semantics, approve and merge it yourself.