このドキュメントは有志個人による非公式資料です。
Leanのインストール方法と、LeanのバージョンマネージャelanとパッケージマネージャLakeの使い方を紹介します。主な参考資料はLean CommunityのInstallationカテゴリです。参考資料の一覧は各ページの最後に掲載します。
このドキュメントはmdBookのLean向けフォークを使って生成されました。
Rustがインストールされていることを前提とします。
このドキュメントをビルドするには、まずmdBookのLean向けフォークをインストールしてください。
cargo install --git https://github.com/leanprover/mdBook mdbook次に、このREADMEが置かれているフォルダで以下のコマンドを実行してください。
mdbook build./out フォルダにhtmlファイル群が生成されます。
次のコマンドでデプロイできます。
./deploy.sh
デプロイ deploy.sh を実行する際は、あらかじめpush先のリポジトリをご自身のフォークリポジトリに変更することをお勧めします。