Leanのインストール方法・elanとLakeの使い方

by aconite

このドキュメントは有志による非公式資料です。

Leanのインストール方法と、LeanのバージョンマネージャelanとパッケージマネージャLakeの使い方を紹介します。Leanやelanをアップデートする方法、Mathlibを使用するLeanプロジェクトを作る方法を含みます。

この資料はMIT Licenseに基づいてLean Community ページの一部を翻訳した派生成果物と、Apache License 2.0に基づいてLean Manualの一部を翻訳した派生成果物を含みます。

この資料のソースはGitHubリポジトリから入手可能です。また、ページ右上端のGitHubマークを押してGitHubリポジトリに移動することもできます。この資料の全ページとソースはApache License 2.0の下で公開されています。

誤字脱字、内容の誤りの指摘、フォークからのPull Request、フォークによる資料の改変等は歓迎いたします。基本的に、ご指摘はGitHubリポジトリのIssuesで受け付けます。

各ページの下部に参考資料の一覧を掲載しています。主な参考資料はLean CommunityのInstallationカテゴリです。主な翻訳元には「翻訳元」と明記しています。また、信頼性の目安となることを想定し、ドメイン名と筆者情報に依って公式情報と判断したものには「公式」と明記していますが、本資料は「公式」と明記した資料が公式情報であることも、「公式」と明記していない資料が非公式情報であることも保証いたしません。

この資料を参考にしてMacOSへのLeanのインストールを希望される方は、節「注意とお願い」を必ずお読みください。

mdBook付属の検索機能に関して、今のところ日本語検索は非対応です。お手数ですがページ内検索をご活用ください。

英語資料の翻訳に際して、機械翻訳サービスDeepL翻訳を参考にしました。