🦿
VSCode DevContainerでLean 4の環境構築
はじめに
Lean 4は、定理証明支援系としてだけでなく、関数型プログラミング言語としても注目を集めています。
そこで、軽量のLean 4開発環境テンプレートを作成しました。
このテンプレートの特徴
🎯 軽量設計
- ベースイメージに
debian:bookworm-slimを使用 - 最終イメージサイズ約500MB（一般的なDevContainer環境の半分程度）
- 必要最小限のパッケージのみをインストール
🐳 即座に使える環境
- リポジトリをクローンしてVSCodeで開くだけ
- 初回ビルド後は数秒で起動
- Lean 4拡張機能とLSPが自動設定済み
- もちろんlocalでのlakeと共存可能
🔧 柔軟なカスタマイズ性
- Leanバージョンは
lean-toolchainファイルで簡単に変更可能 - 外部ライブラリ（mathlibなど）の追加も容易
- Docker/Podman両対応
👥 UID/GID自動マッチング
- ホストユーザーとコンテナユーザーのUID/GIDを自動同期
- ファイルパーミッション問題を解決
- 複数人での開発に最適
使い方
前提条件
- Visual Studio Code
- Docker Desktop（またはPodman）
- Dev Containers拡張機能
セットアップ手順
- リポジトリをクローン
git clone https://github.com/chantakan/lean4-devcontainer-template.git
cd lean4-devcontainer-template
- VSCodeで開く
code .
- コンテナで再オープン
VSCodeが起動すると、「Reopen in Container」の通知が表示されるので、クリックします。
または：
-
F1またはCtrl+Shift+P（Windows/Linux）/Cmd+Shift+P（Mac） - 「Dev Containers: Reopen in Container」を選択
- Enter
初回ビルドは数分かかりますが、2回目以降は数秒で起動します。
- 動作確認
コンテナが起動したら、統合ターミナルで以下を実行：
# バージョン確認
lean --version
lake --version
# サンプルプログラムの実行
lake build
lake exe lean4-project
Hello, Lean 4! と表示されれば成功です！
プロジェクト構成の解説
ディレクトリ構造
.
├── .devcontainer/
│ ├── devcontainer.json # DevContainer設定
│ └── Dockerfile # Dockerイメージ定義
├── .gitignore
├── lakefile.lean # Lakeビルド設定
├── lean-toolchain # Leanバージョン指定
├── Main.lean # メインエントリポイント
└── README.md
devcontainer.jsonの重要ポイント
{
"name": "Lean 4",
"build": {
"dockerfile": "Dockerfile"
},
// UID/GIDの自動マッチング
"features": {
"ghcr.io/devcontainers/features/common-utils:2": {
"installZsh": false,
"installOhMyZsh": false,
"upgradePackages": false,
"username": "vscode",
"userUid": "automatic",
"userGid": "automatic"
}
},
// 拡張機能の自動インストール
"customizations": {
"vscode": {
"extensions": [
"leanprover.lean4"
]
}
},
// コンテナ作成後の初期化
"postCreateCommand": "elan default $(cat lean-toolchain) && lake update",
"remoteUser": "vscode"
}
ポイント：
-
common-utilsフィーチャーで非rootユーザーを自動作成 -
userUid: "automatic"により、ホストユーザーとUID/GIDを同期 -
postCreateCommandで、指定バージョンのLeanを自動インストール
Dockerfileの最適化戦略
FROM debian:bookworm-slim
# 必要最小限のパッケージのみインストール
RUN apt-get update && apt-get install -y --no-install-recommends \
curl \
ca-certificates \
git \
build-essential \
sudo \
&& rm -rf /var/lib/apt/lists/* \
&& apt-get clean
# elan（Leanバージョン管理ツール）のグローバルインストール
ENV ELAN_HOME=/usr/local/elan \
PATH=/usr/local/elan/bin:$PATH
RUN mkdir -p $ELAN_HOME && chmod 777 $ELAN_HOME
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \
| sh -s -- -y --no-modify-path --default-toolchain none \
&& chmod -R a+w $ELAN_HOME \
&& elan --version
最適化のポイント：
-
軽量ベースイメージ:
debian:bookworm-slim（約70MB） -
不要なキャッシュ削除:
rm -rf /var/lib/apt/lists/* -
レイヤーの最小化: 関連コマンドを
&&で連結 - グローバルelanインストール: 複数ユーザーでの共有を可能に
サンプルコードの解説
Main.leanには、Lean 4の基本的な機能を示すサンプルが含まれています：
def main : IO Unit :=
IO.println "Hello, Lean 4!"
-- 加法の交換法則の証明（帰納法を使用）
theorem add_comm (a b : Nat) : a + b = b + a := by
induction a with
| zero =>
rw [Nat.zero_add]
rw [Nat.add_zero]
| succ n ih =>
rw [Nat.succ_add, Nat.add_succ, ih]
-- より簡潔な証明（omegaタクティックを使用）
theorem add_comm_simple (a b : Nat) : a + b = b + a := by
omega
-- その他の例
example (x y : Nat) : x + y = y + x := by omega
example (x : Nat) : x + 0 = x := by omega
このサンプルでは：
-
IOアクション:
main関数でコンソール出力 - 定理証明: 自然数の加法交換法則を2通りの方法で証明
- omegaタクティック: 線形算術を自動で解決する強力なタクティック
カスタマイズ方法
Leanバージョンの変更
lean-toolchainファイルを編集：
leanprover/lean4:stable # 安定版
leanprover/lean4:nightly # 最新版
leanprover/lean4:v4.8.0 # 特定バージョン
変更後、コンテナを再ビルド：
Dev Containers: Rebuild Container
外部ライブラリの追加（mathlib4など）
lakefile.leanに依存関係を追加：
import Lake
open Lake DSL
package «lean4-project» where
-- package configuration
-- mathlib4を追加
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
lean_lib «Lean4Project» where
-- library configuration
@[default_target]
lean_exe «lean4-project» where
root := `Main
コンテナ内でlake updateを実行すると、依存関係が自動でインストールされます。
追加のVSCode拡張機能
devcontainer.jsonのextensions配列に追加：
"extensions": [
"leanprover.lean4",
"GitHub.copilot", // 例：GitHub Copilot
"MS-CEINTL.vscode-language-pack-ja" // 例：日本語パック
]
トラブルシューティング
Dockerが起動しない
- Docker Desktopが起動しているか確認
- インターネット接続を確認
- コンテナを再ビルド：
Dev Containers: Rebuild Container
Lean拡張機能が動作しない
- コンテナ内で開いているか確認（VSCode左下に「Dev Container: Lean 4」と表示）
- ウィンドウをリロード：
Developer: Reload Window
メモリ不足エラー
- Docker Desktopの設定でメモリ割り当てを増やす
- 推奨：最低4GB RAM
ファイルのパーミッションエラー
-
common-utilsフィーチャーのUID/GID自動マッチング機能により、通常は発生しません - 問題が発生した場合は、コンテナを再ビルド
まとめ
このテンプレートを使用することで：
✅ Lean 4の環境構築が1分で完了
✅ チーム全体で統一された開発環境を維持
✅ 軽量で高速な開発体験
✅ クリーンなホスト環境を保持
Lean 4での定理証明や関数型プログラミングに興味がある方は、ぜひこのテンプレートを試してみてください！
Discussion