From d12f0c857e2fa8b4f5380d6d5a44eae94e10f796 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 7 Oct 2024 04:36:49 +0900 Subject: [PATCH] =?UTF-8?q?mdbook=20=E7=94=A8=E3=81=AE=20markdown=20?= =?UTF-8?q?=E3=83=95=E3=82=A1=E3=82=A4=E3=83=AB=E3=82=92=E6=A0=BC=E7=B4=8D?= =?UTF-8?q?=E3=81=99=E3=82=8B=E3=83=87=E3=82=A3=E3=83=AC=E3=82=AF=E3=83=88?= =?UTF-8?q?=E3=83=AA=E3=81=AE=E5=90=8D=E5=89=8D=E3=82=92=20`booksrc`=20?= =?UTF-8?q?=E3=81=AB=E5=A4=89=E3=81=88=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/CONTRIBUTING.md | 2 +- .gitignore | 12 ++++++------ README.md | 4 ++-- assets/filePlay.js | 4 ++-- book.toml | 2 +- {src => booksrc}/404.md | 0 {src => booksrc}/README.md | 0 {src => booksrc}/SUMMARY.md | 0 {src => booksrc}/image/project_image.png | Bin {src => booksrc}/image/proxima.svg | 0 {src => booksrc}/links.md | 0 lakefile.lean | 4 ++-- scripts/Build.ps1 | 4 ++-- 13 files changed, 16 insertions(+), 16 deletions(-) rename {src => booksrc}/404.md (100%) rename {src => booksrc}/README.md (100%) rename {src => booksrc}/SUMMARY.md (100%) rename {src => booksrc}/image/project_image.png (100%) rename {src => booksrc}/image/proxima.svg (100%) rename {src => booksrc}/links.md (100%) diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 86708179..0d274cb0 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -24,7 +24,7 @@ * 地の文はですます調とし、コード例の中の文章は常体とします。 * 読点には `、` を、句点には `。` を使用します。ただし例外として、直前の文字が半角文字であるときには `、` の代わりに半角カンマ `,` を使用します。 * 見出し語 `foo` に対して、目次の中での記事の名前は `foo: (日本語による一言説明)` とします。可能な限り１行に収まるようにしてください。 -* 目次である `src/SUMMARY.md` の内の記事は、カテゴリごとにアルファベット昇順に並べてください。VSCode だと [Tyriar.sort-lines](https://marketplace.visualstudio.com/items?itemName=Tyriar.sort-lines) という拡張機能があって、並び替えを自動で行うことができます。 +* 目次である `booksrc/SUMMARY.md` の内の記事は、カテゴリごとにアルファベット昇順に並べてください。VSCode だと [Tyriar.sort-lines](https://marketplace.visualstudio.com/items?itemName=Tyriar.sort-lines) という拡張機能があって、並び替えを自動で行うことができます。 * Lean コードは、コンパイルが通るようにして `Examples` 配下に配置します。 * 「エラーになる例」を紹介したいときであっても `try` や `#guard_msgs` や `fail_if_success` などを使ってコンパイルが通るようにしてください。コード例が正しいかチェックする際にその方が楽だからです。 * Lean ファイルのファイル名は、パスカルケースで命名して下さい。 diff --git a/.gitignore b/.gitignore index 31937a44..6925bd34 100644 --- a/.gitignore +++ b/.gitignore @@ -9,11 +9,11 @@ book Draft/ -/src/* -!src/image -!src/links.md -!src/README.md -!src/404.md -!src/SUMMARY.md +/booksrc/* +!booksrc/image +!booksrc/links.md +!booksrc/README.md +!booksrc/404.md +!booksrc/SUMMARY.md *.olean diff --git a/README.md b/README.md index b56601ad..9f97e95f 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # README -[![repo logo](./src/image/project_image.png)]() +[![repo logo](./booksrc/image/project_image.png)]() [![workflow](https://github.com/lean-ja/lean-by-example/actions/workflows/ci.yml/badge.svg)](https://github.com/lean-ja/lean-by-example/blob/main/.github/workflows/ci.yml) [![workflow](https://github.com/lean-ja/lean-by-example/actions/workflows/deploy.yml/badge.svg)](https://github.com/lean-ja/lean-by-example/blob/main/.github/workflows/deploy.yml) [![workflow](https://github.com/lean-ja/lean-by-example/actions/workflows/update.yml/badge.svg)](https://github.com/lean-ja/lean-by-example/blob/main/.github/workflows/update.yml) [![workflow](https://github.com/lean-ja/lean-by-example/actions/workflows/devcontainer.yml/badge.svg)](https://github.com/lean-ja/lean-by-example/blob/main/.github/workflows/devcontainer.yml) [![discord](https://dcbadge.limes.pink/api/server/p32ZfnVawh?style=flat)](https://discord.gg/p32ZfnVawh) @@ -45,6 +45,6 @@ If you use this book for your work, please cite it as follows: このプロジェクトは [Proxima Technology](https://proxima-ai-tech.com/) 様よりご支援を頂いています。 -![logo of Proxima Technology](./src/image/proxima.svg) +![logo of Proxima Technology](./booksrc/image/proxima.svg) Proxima Technology（プロキシマテクノロジー）は数学の社会実装を目指し、その⼀環としてモデル予測制御の民主化を掲げているAIスタートアップ企業です。数理科学の力で社会を変えることを企業の使命としています。 diff --git a/assets/filePlay.js b/assets/filePlay.js index 44bc892e..00fcb816 100644 --- a/assets/filePlay.js +++ b/assets/filePlay.js @@ -14,8 +14,8 @@ function filePlay() { // 拡張子が `.md` になっているので `.lean` に修正する editButtonLink.href = editButtonLink.href.replace(/\.md$/, ".lean"); - // Lean ファイルがあるのは `src` ではなく `Examples` ディレクトリ - editButtonLink.href = editButtonLink.href.replace("/src/", "/Examples/"); + // Lean ファイルがあるのは `booksrc` ではなく `Examples` ディレクトリ + editButtonLink.href = editButtonLink.href.replace("/booksrc/", "/Examples/"); // 演習問題のファイルのみ、`Examples` ディレクトリではなくて `Exercise` ディレクトリにある editButtonLink.href = editButtonLink.href.replace( diff --git a/book.toml b/book.toml index aa94fd81..c3cbbc05 100644 --- a/book.toml +++ b/book.toml @@ -2,7 +2,7 @@ authors = ["Seasawher"] language = "ja" multilingual = false -src = "src" +src = "booksrc" # 単に src とすると検索ノイズが多くなることを考慮 title = "Lean by Example" description = "プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。" diff --git a/src/404.md b/booksrc/404.md similarity index 100% rename from src/404.md rename to booksrc/404.md diff --git a/src/README.md b/booksrc/README.md similarity index 100% rename from src/README.md rename to booksrc/README.md diff --git a/src/SUMMARY.md b/booksrc/SUMMARY.md similarity index 100% rename from src/SUMMARY.md rename to booksrc/SUMMARY.md diff --git a/src/image/project_image.png b/booksrc/image/project_image.png similarity index 100% rename from src/image/project_image.png rename to booksrc/image/project_image.png diff --git a/src/image/proxima.svg b/booksrc/image/proxima.svg similarity index 100% rename from src/image/proxima.svg rename to booksrc/image/proxima.svg diff --git a/src/links.md b/booksrc/links.md similarity index 100% rename from src/links.md rename to booksrc/links.md diff --git a/lakefile.lean b/lakefile.lean index 6de1449f..a841f3af 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -68,8 +68,8 @@ script build do runCmd "lake exe mk_exercise Examples/Solution Exercise" with_time running "mdgen" - runCmd "lake exe mdgen Examples src"; - runCmd "lake exe mdgen Exercise src/Exercise" + runCmd "lake exe mdgen Examples booksrc"; + runCmd "lake exe mdgen Exercise booksrc/Exercise" with_time running "mdbook" runCmd "mdbook build" diff --git a/scripts/Build.ps1 b/scripts/Build.ps1 index a634d9e5..a3519bd6 100644 --- a/scripts/Build.ps1 +++ b/scripts/Build.ps1 @@ -5,7 +5,7 @@ lake を介することなく実行ファイルを直接叩く。 #> ./.lake/packages/mk-exercise/.lake/build/bin/mk_exercise.exe Examples/Solution Exercise -./.lake/packages/mdgen/.lake/build/bin/mdgen.exe Exercise src/Exercise -./.lake/packages/mdgen/.lake/build/bin/mdgen.exe Examples src +./.lake/packages/mdgen/.lake/build/bin/mdgen.exe Exercise booksrc/Exercise +./.lake/packages/mdgen/.lake/build/bin/mdgen.exe Examples booksrc mdbook build