---
name: Lean ファイルは commit 前に必ず lake env lean で実ビルド検証
description: 2026-04-21 発見 — Sonnet が STEP 950-967 を build 未確認で commit、19中14が compile error
type: feedback
originSessionId: 80a567c3-c92a-4757-ac12-f814a062c754
---
Lean 4 ファイルを書いて commit する前に、必ず `lake env lean <file>` で実ビルドを通す。`native_decide` の挙動は Lean を実行しないと分からない。型エラー・API 不在・false 返しは見た目のコードからは判別できない。

**Why:** 2026-04-21、Sonnet セッションが STEP 950-967 (18ファイル) を「axiom→proper types」改善として 6 commit で push したが、Opus に切り替えてビルド検証したところ 19中 5 ファイル (26%) しか build せず。残り 14 ファイルは:
- `List.bind` 不在 (Mathlib v4.27 で削除→`List.flatMap`)
- `Nat.popcount`/`Nat.factors`/`Submodule.isPrincipal` API 不在
- `Real.exp`/`Real.log` の noncomputable 漏れ
- 証人数値ミスで `native_decide` が false を返す
- コメント末尾 `/--` の parse error
等の理由で破綻。藤本さんに「19中5しかビルドしない」と正直に報告する事態になった。

**How to apply:**
- **自動化済 (2026-04-22)**: `scripts/git-hooks/pre-commit` が staged な `data/lean4-mathlib/**.lean` に `lake env lean` を自動実行。インストール: `bash scripts/git-hooks/install.sh` (既に済)
- 重い `native_decide` ファイル (例 Step950 = 37 分) は先頭 30 行以内に `[skip-precommit]` マーカーを入れて pre-commit ではスキップ、GitHub Actions (`.github/workflows/lean-verify.yml`) で完全ビルド
- 緊急バイパス: `SKIP_LEAN_VERIFY=1 git commit ...`
- hook が欠落している環境 (新規 clone 直後等) では手動で `cd data/lean4-mathlib && lake env lean CollatzRei/StepNNN....lean` を実行してから `git add`
- 原則: exit code 0 かつエラー出力ゼロを確認してから commit
- Sonnet/Opus 関係なく hook が強制実行 (LLM のコード生成は Mathlib バージョン差を見逃しやすいので機械的ゲートが必須)