---
name: LeanCopilot Windows MSYS2 ct2.o build failure (STEP 866 + 1008 retry の root cause)
description: ★★★ LeanCopilot v4.27.0 の native CTranslate2 binding が MSYS2 mingw-w64 ヘッダ取得 URL 壊れで失敗. Lean/Mathlib の問題ではなく Windows 外部依存. 代替は lean-auto + Duper.
type: feedback
originSessionId: 8eb7dbb6-afb1-40b9-ad4e-df044a874edd
---
# LeanCopilot v4.27.0 Windows build 失敗の root cause + 復旧 path

## ルール

LeanCopilot を再有効化しようとする時:
1. lakefile.toml の require は **デフォルトでコメントアウト維持**
2. 試行する場合は **WSL2 Linux 上のみ** (Windows native は MSYS2 trap)
3. または **lean-auto + Duper** (本日 STEP 1009 で動作確認済) を継続使用

## Why

**STEP 866 (2026 早期) の失敗 + STEP 1008 retry (2026-04-28) で root cause 判明**:

```
✓ lake update LeanCopilot       — SUCCESS (v4.27.0 tag clones)
✗ lake build LeanCopilot         — FAIL at LeanCopilot/ct2.o
```

詳細:
- LeanCopilot は CTranslate2 (C++ ML inference engine) の native binding を使用
- ビルド時に `mingw-w64-clang-x86_64-headers-git-12.0.0.r81.g90abf784a-1` パッケージを `repo.msys2.org` から取得しようとする
- **その URL が壊れて 153 byte の HTML エラーページを返す**
- → `tar: Unrecognized archive format` で ct2.o build 失敗

**これは Windows 外部依存 (MSYS2 mirror) の URL 問題で、Lean 4 / Mathlib 側の問題ではない**.

## How to apply

### LeanCopilot は disabled で維持

`data/lean4-mathlib/lakefile.toml` の以下 stanza は **コメントアウトのまま**:
```toml
#[[require]]
#name = "LeanCopilot"
#git = "https://github.com/lean-dojo/LeanCopilot.git"
#rev = "v4.27.0"
```

### 代替 path (本日 STEP 1009 で動作確認済)

```toml
[[require]]
name = "auto"
git = "https://github.com/leanprover-community/lean-auto.git"
rev = "v4.27.0-hammer"

[[require]]
name = "Duper"
git = "https://github.com/leanprover-community/duper.git"
rev = "v4.27.0"
```

- Duper は pure-Lean superposition ATP, native binding 不要
- 使用例: `data/lean4-mathlib/CollatzRei/AutoDemo.lean` (9 theorem, 0 sorry, 0 axiom)
- 注意: lean-auto + Duper bridge は API 型 mismatch で disable. **Duper 単体で利用**.

### 将来 LeanCopilot 復旧したい場合の 4 option

1. **(a) MSYS2 ヘッダ手動 download** — 該当 package を Windows に手動配置
2. **(b) WSL2 / Linux で build** — MSYS2 不使用の Linux native build (推奨)
3. **(c) Upstream 修正待ち** — Lean Dojo に issue 提出 + 時間
4. **(d) lean-auto 継続** — 現状で十分なら何もしない

私の推奨は (d) → (b) の順. (a) は brittle, (c) は受動的.

## 関連 commit / file

- STEP 1008 commit `1f07c42d`: 詳細 retry 結果 + 復旧 option 列挙
- STEP 1009 commit `94b29ef7`: lean-auto + Duper 統合
- `docs/lean-hammer-integration-plan.md`: Stage 1-4 ロードマップ
- `data/lean4-mathlib/CollatzRei/AutoDemo.lean`: Duper 動作 demo