コンテンツにスキップ

Lean 4 環境構築ガイド

「数学系エンドユーザーのための Lean 入門」講義の事前準備用ガイドです．

概要

  • 公式のLeanインストール手順に沿って環境構築をします
  • GitHub アカウントはなくても動かせます．ただし，
    • バックアップ環境（Codespaces）を利用する際に必要となります
    • アカウント作成・設定には時間がかかりますので，なるべく事前に準備しておいてください
  • ローカル環境が構築できなかった場合のバックアップは2通りあります
  • Lean はバージョン指定が違うと動きません
    • 講義では安定版（stable）を使います 
      leanprover/lean4:v4.30.0
    • 最新版（latest, nightly）ではないので，不用意に update しないでください
  • Mathlib のビルドには時間がかかるので，ビルド済みのキャッシュを取得します 
    lake exe cache get   --- まずキャッシュ取得
lake build           --- そのあとビルド

目標

各自の PC で次ができる状態を目指します

  1. 講義資料の GitHub リポジトリ をローカルに clone できる 
    git clone https://github.com/shosonoda/lean-math-note.git
  2. VS Code と Lean 4 拡張機能がインストールされている
  3. Lean のバージョンマネージャ elan が lean-toolchain で指定された Lean バージョンを選べる 
    cd lean-math-note
elan show
  4. Mathlib 付き Lean プロジェクトを build できる 
    lake exe cache get
lake build
  5. VS Code で .lean ファイルを開くと Lean Infoview が動く．
  6. （オプション）VS Code で Markdown のプレビューを表示できる．

利用例

  • VS Code + Markdown Preview + Lean InfoView

VS Code + Markdown Preview + Lean InfoView

Chrome 分割ビュー + 講義資料 + Lean Playground

手順

  1. 公式のLeanインストール手順に沿って環境構築を試みてください
  2. 確認チェックリスト で足りないものを確認してください
  3. 足りないものがあるとき
  4. うまく動かないとき
  5. ローカルの環境構築をしない場合
    • Codespaces 利用手順 を使って，ブラウザ上の VS Code で Mathlib 付き Lean プロジェクトを動かせます
    • LeanPlayground にコードをコピペして動作確認することもできます

想定環境

  • OS
    • macOS
    • Windows 10/11
  • VS Code
  • Lean 4
  • Mathlib
  • Git / GitHub CLI

GitHub アカウントについて

公開リポジトリを HTTPS で clone してローカルで実行するだけなら，GitHub アカウントは不要です．GitHub CLI のログイン，Codespaces，自分のリポジトリへの保存には GitHub アカウントが必要です．

作業フォルダ名の注意

Windows では，作業フォルダ名に日本語・空白・特殊記号を入れない方が安全です．例: C:\Users\ユーザー名\LeanProjects よりも，可能なら C:\LeanProjects のようにします．

参考リンク