docs(handoff): correct worktree paths after tree relocation; v0.2.0 is published

[AsafMah]

Important

Merge this after #137. §7 states that the two runTests skip guards were removed in #137. Those guards are still present on dev (SubtypeTest.kt, InputLogicTest.kt) until #137 lands, so merging this first would put a document on dev that describes code dev doesn't have yet.

Corrects docs/HANDOFF.md, which had gone stale in several independent ways.

1. The worktree paths were wrong (§11)

The repo tree moved from C:/Users/mahle/ to C:/Users/mahle/programming/. Git's per-worktree admin records still pointed at the old absolute paths, so git worktree list marked all 24 secondary worktrees prunable — a relocation artifact, not abandonment. git worktree repair with the new paths re-linked every one.

With them visible again, all 24 were triaged (branch, ahead/behind vs origin/dev, merge status, remote containment, PR state, dirty working tree, disk size) and 13 fully-merged worktrees were removed, reclaiming ~5.6 GB. Every branch was kept, so each is restorable with git worktree add <dir> <branch>.

§11 now records the resulting set:

• Kept: bksp (PR Add source-key action target slides #106), two-thumb-pr (LeanBitLab PR feat(gestures): add step-one tap and gesture combining LeanBitLab/LeanType#240), and three baseline checkouts. check-origin-dev and check-origin-main were re-pointed to current origin/dev/origin/main (5 merges and 2 releases stale). check-upstream-main is documented as tracking whichever upstream tag is currently being integrated — now v4.1.2.
• Unfinished: six worktrees, since backed up to origin. The section keeps a narrower warning, because a branch push captures commits but not working trees: LeanType-b7a and LeanType-swipe still hold uncommitted changes that exist nowhere else.

Two traps are now documented, both hit during the cleanup:

• Never reach for git worktree prune when a relocation makes everything look prunable — it drops the admin records and orphans live work. repair is the tool.
• core.longpaths=true is now set on the repo. Without it git worktree remove dies with Filename too long on worktrees carrying deep Gradle build output, leaving a de-registered but half-deleted directory behind. That happened to two worktrees here; their branches were confirmed intact and merged before the orphans were purged.

2. v0.2.0 shipped, so the headline claim was wrong (§1, §2.3, §5)

The document led with "the single open task: publish the signed v0.2.0 release", blocked on a CI runner outage. That release went out on 2026-08-20 — verified against the API: published, not draft, marked latest, 4 signed APKs; Release run 31128748928 succeeded 2026-08-06 22:04 UTC.

§5 keeps its recipe verbatim — still the correct procedure for the next release — but is reframed from "THE OPEN TASK" to release procedure, generalised to vX.Y.Z, with the outage signature retained so a recurrence is recognised rather than re-debugged.

Also corrected: the stale dev SHA in the §1 table (2c1c828c4 → 6ac372de3), the open-PR row (now #106, #134, #136, #137), and §2.3's "signed artifacts were never produced".

3. Both inherited upstream defects are fixed (§7, §12)

§7 described two tests that fail on pristine upstream and are guarded with the runTests skip. Upstream v4.1.2 fixes both, and #137 removes the guards. Verified from raw JUnit XML: pristine v4.1.2 → SubtypeTest 3 tests / 0 failures; merged tree → the regex test passing; e46454efb removes exactly those two guards and no others.

§7 is kept as history rather than deleted, because the reusable lesson is the technique: reproduce a merge failure on a pristine upstream checkout before blaming your own merge. Neither defect needs reporting upstream; the emoji accelerated-delete bug is reported as LeanBitLab/LeanType#423.

4. §6's failure list is now measured on both sides

The old §6 gave one blanket failure list. It was accurate for dev and wrong for the merge branch. Rather than swap one asserted list for another, both baselines were actually run on the same machine minutes apart:

Baseline	Result
origin/dev (6ac372de3)	320 tests, 12 failed
v4.1.2 merge branch	324 tests, 5 failed

The merge-branch set — the autospace-indicator test plus the same four ParserTest failures the CI variant reports — is documented as the current expectation.

Attribution of the seven resolved failures is split by confidence rather than claimed wholesale: the two §7 defects and the Hangul case are safely merge-attributable; StringUtilsTest ×2 and ParserTest > backgroundType are plausible (bundled data/assets do change here) but unconfirmed; XLinkTest > otherLinks makes a live network call and is explicitly not counted as a fix. Same-machine runs control for toolchain, locale and machine state — not for a remote host being reachable.

5. Self-correction before merge

Statements written earlier in this same PR went stale within the hour and were fixed in 44dde85cb rather than shipped as fresh staleness — which would rather defeat the point: the two workflow runs §5 called "still stuck in queued" have since been cancelled, and check-upstream-main had already moved off v4.0.8. Likewise 70ba02846, after the six unfinished branches gained origin backups.

Note on authorship: the asafmah-fix-backspace-paragraph-delete session made the same §5 correction concurrently, landing c35c821a9 here 18 seconds after my own commit. Its effective diff was one additive line — adding #136 to the open-PR row, which I had missed. Reviewed and kept.

Testing

The document is prose, but its testing claims are measured, not asserted: :app:testOfflineDebugUnitTest was run on both origin/dev and the v4.1.2 merge branch, and every figure quoted here comes from the resulting JUnit XML. Other claims were checked against git, the GitHub API, or the filesystem; the repo was scanned to confirm no old-path references remain.