開発には以下のようなツールを主に利用しています。環境構築済みの DevContainer / GitHub Codespace を用意してありますので、Lean の環境構築をスキップしたい方はそちらを利用してください。
- mdbook を使用して markdown ファイルから HTML を生成しています。以下のプラグインを使用しています。
- mdbook-admonish を使用してカードを表示させています。
Important
開発に使用する mdbook のバージョンは 0.4.35 に固定してください。0.4.35 以外のバージョンではレイアウトが崩れます。
- mdgen を Lean ファイルから markdown ファイルを生成するために使用しています。
- mk_exercise を使い、Lean の解答ファイルから演習問題ファイルを生成しています。
- このリポジトリは mathlib に依存しているので、このリポジトリを clone した後に
lake exe cache getを実行してください。 LeanByExample/Tutorial/Exerciseディレクトリ配下のファイルはmk_exerciseによりLeanByExample/Solutionの内容から自動生成されるので、手動で編集しないでください。- 本文の markdown ファイルは mdgen を用いて Lean ファイルから生成します。Lean ファイルを編集した後、
lake run buildコマンドを実行すれば mk_exercise の実行と markdown の生成とmdbook buildが一括実行されます。
- 地の文はですます調とし、コード例の中の文章は常体とします。
- 読点には
、を、句点には。を使用します。ただし例外として、直前の文字が半角文字であるときには、の代わりに半角カンマ,を使用します。 - 見出し語
fooに対して、目次の中での記事の名前はfoo: (日本語による一言説明)とします。可能な限り１行に収まるようにしてください。 - 目次である
booksrc/SUMMARY.mdの内の記事は、カテゴリごとにアルファベット昇順に並べてください。VSCode だと Tyriar.sort-lines という拡張機能があって、並び替えを自動で行うことができます。 - Lean コードは、コンパイルが通るようにして
LeanByExample配下に配置します。- 「エラーになる例」を紹介したいときであっても
tryや#guard_msgsやfail_if_successなどを使ってコンパイルが通るようにしてください。コード例が正しいかチェックする際にその方が楽だからです。 - Lean ファイルのファイル名は、パスカルケースで命名して下さい。
- ファイル名は、大文字が連続しないようにします。例外として、
READMEはすべて大文字です。またHDivなど元々大文字が連続しているものはそのままで構いません。
- 「エラーになる例」を紹介したいときであっても