From 8ae23453728daf413a865bfd70faca04b8402292 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Sat, 13 Jun 2026 23:39:09 +0900 Subject: [PATCH 1/4] =?UTF-8?q?`booksrc`=20=E3=81=AE=E4=B8=AD=E3=82=92?= =?UTF-8?q?=E5=85=A8=E3=81=A6=20ignore=20=E3=81=99=E3=82=8B=E3=80=82?= =?UTF-8?q?=E5=BF=85=E8=A6=81=E3=81=AA=E3=83=95=E3=82=A1=E3=82=A4=E3=83=AB?= =?UTF-8?q?=E3=81=AF=20`LeanByExample`=20=E3=83=87=E3=82=A3=E3=83=AC?= =?UTF-8?q?=E3=82=AF=E3=83=88=E3=83=AA=E3=81=AE=E4=B8=AD=E3=81=8B=E3=82=89?= =?UTF-8?q?=E3=82=B3=E3=83=94=E3=83=BC=E3=81=97=E3=81=A6=E3=81=8F=E3=82=8B?= =?UTF-8?q?=E3=81=8B=E3=80=81=E3=81=82=E3=82=8B=E3=81=84=E3=81=AF=E7=94=9F?= =?UTF-8?q?=E6=88=90=E3=81=97=E3=81=A6=E3=81=8F=E3=82=8B=E3=81=93=E3=81=A8?= =?UTF-8?q?=E3=81=AB=E3=81=99=E3=82=8B=E3=80=82?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .gitignore | 5 +---- booksrc/404.md => LeanByExample/404.lean | 4 ++-- booksrc/SUMMARY.md => LeanByExample/SUMMARY.lean | 4 ++-- {booksrc => LeanByExample}/image/project_image.png | Bin .../image/proxima.inkscape.svg | 0 lake-manifest.json | 2 +- lakefile.lean | 2 +- 7 files changed, 7 insertions(+), 10 deletions(-) rename booksrc/404.md => LeanByExample/404.lean (65%) rename booksrc/SUMMARY.md => LeanByExample/SUMMARY.lean (99%) rename {booksrc => LeanByExample}/image/project_image.png (100%) rename {booksrc => LeanByExample}/image/proxima.inkscape.svg (100%) diff --git a/.gitignore b/.gitignore index cfa26076..646b848b 100644 --- a/.gitignore +++ b/.gitignore @@ -1,9 +1,6 @@ # mdbook に関連するもの book -/booksrc/* -!booksrc/image -!booksrc/404.md -!booksrc/SUMMARY.md +booksrc/* # macOS leaves these files everywhere: .DS_Store # Created by `lake exe cache get` if no home directory is available diff --git a/booksrc/404.md b/LeanByExample/404.lean similarity index 65% rename from booksrc/404.md rename to LeanByExample/404.lean index 24e41695..4fb592d3 100644 --- a/booksrc/404.md +++ b/LeanByExample/404.lean @@ -1,5 +1,5 @@ -# 404 エラー +/- # 404 エラー お探しのページが見つかりませんでした。 -URL が変更された可能性があります。ご迷惑をおかけして申し訳ございません。 +URL が変更された可能性があります。ご迷惑をおかけして申し訳ございません。 -/ diff --git a/booksrc/SUMMARY.md b/LeanByExample/SUMMARY.lean similarity index 99% rename from booksrc/SUMMARY.md rename to LeanByExample/SUMMARY.lean index 3ff2cd33..3dae3fd0 100644 --- a/booksrc/SUMMARY.md +++ b/LeanByExample/SUMMARY.lean @@ -1,4 +1,4 @@ -# Summary +/- # Summary [はじめに](./README.md) @@ -301,4 +301,4 @@ - [嫉妬深い夫たちの川渡りパズル](./EXTRA/Jealous.md) - [天使と悪魔の論理パズル](./EXTRA/AngelAndDevil.md) - [末尾再帰](./EXTRA/TailRec.md) - - [クワイン](./EXTRA/Quine.md) + - [クワイン](./EXTRA/Quine.md) -/ diff --git a/booksrc/image/project_image.png b/LeanByExample/image/project_image.png similarity index 100% rename from booksrc/image/project_image.png rename to LeanByExample/image/project_image.png diff --git a/booksrc/image/proxima.inkscape.svg b/LeanByExample/image/proxima.inkscape.svg similarity index 100% rename from booksrc/image/proxima.inkscape.svg rename to LeanByExample/image/proxima.inkscape.svg diff --git a/lake-manifest.json b/lake-manifest.json index 82cf11d3..616a69e5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e061a86b0e168c6d37f535595d719899b7f131fb", + "rev": "c003ac1229883b25d3b9e5df2fc0b2da453d3c8a", "name": "mdgen", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.lean b/lakefile.lean index 6d5ad6e7..7b8d9c7d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -45,7 +45,7 @@ def runCmd (input : String) : IO Unit := do /-- mdgen と mdbook を順に実行し、 Lean ファイルから Markdown ファイルと HTML ファイルを生成する。-/ script build do - runCmd "lake exe mdgen LeanByExample booksrc --count" + runCmd "lake exe mdgen LeanByExample booksrc --count --copy" runCmd "mdbook build" -- SEO用のメタデータの更新。ローカルでは動作させる必要がないが、CI上では実行するべき From f3b015309cb45cdb9dcd81811858bd72bc599584 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Sun, 14 Jun 2026 00:03:39 +0900 Subject: [PATCH 2/4] =?UTF-8?q?`booksrc`=20=E3=82=92=E3=83=AA=E3=83=8D?= =?UTF-8?q?=E3=83=BC=E3=83=A0=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/CONTRIBUTING.md | 2 +- README.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 08ae188e..a529d327 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -23,7 +23,7 @@ * 地の文はですます調とし、コード例の中の文章は常体とします。 * 読点には `、` を、句点には `。` を使用します。ただし例外として、直前の文字が半角文字であるときには `、` の代わりに半角カンマ `,` を使用します。 * 見出し語 `foo` に対して、目次の中での記事の名前は `foo: (日本語による一言説明)` とします。可能な限り１行に収まるようにしてください。 -* 目次である `booksrc/SUMMARY.md` の内の記事は、カテゴリごとにアルファベット昇順に並べてください。VSCode だと [Tyriar.sort-lines](https://marketplace.visualstudio.com/items?itemName=Tyriar.sort-lines) という拡張機能があって、並び替えを自動で行うことができます。 +* 目次である `LeanByExample/SUMMARY.lean` の内の記事は、カテゴリごとにアルファベット昇順に並べてください。VSCode だと [Tyriar.sort-lines](https://marketplace.visualstudio.com/items?itemName=Tyriar.sort-lines) という拡張機能があって、並び替えを自動で行うことができます。 * Lean コードは、コンパイルが通るようにして `LeanByExample` 配下に配置します。 * 「エラーになる例」を紹介したいときであっても `try` や `#guard_msgs` や `fail_if_success` などを使ってコンパイルが通るようにしてください。コード例が正しいかチェックする際にその方が楽だからです。 * Lean ファイルのファイル名は、パスカルケースで命名して下さい。 diff --git a/README.md b/README.md index dc7cb5f1..9580fa98 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # README -[![repo logo](./booksrc/image/project_image.png)]() +[![repo logo](./LeanByExample/image/project_image.png)]() プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。 @@ -47,6 +47,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](./booksrc/image/proxima.inkscape.svg) +![logo of Proxima Technology](./LeanByExample/image/proxima.inkscape.svg) Proxima Technology（プロキシマテクノロジー）は数学の社会実装を目指し、その⼀環としてモデル予測制御の民主化を掲げているAIスタートアップ企業です。数理科学の力で社会を変えることを企業の使命としています。 From ea0ad208e48cc48fd636ae73ec0f19e4e1251e9d Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Sun, 14 Jun 2026 00:04:52 +0900 Subject: [PATCH 3/4] =?UTF-8?q?=E3=83=A9=E3=83=B3=E3=83=80=E3=83=A0?= =?UTF-8?q?=E3=83=9A=E3=83=BC=E3=82=B8=E8=A1=A8=E7=A4=BA=E3=83=AD=E3=82=B8?= =?UTF-8?q?=E3=83=83=E3=82=AF=E3=82=92=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- assets/randomPage.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/assets/randomPage.js b/assets/randomPage.js index ab886646..1f85ff8f 100644 --- a/assets/randomPage.js +++ b/assets/randomPage.js @@ -6,7 +6,7 @@ document.addEventListener('DOMContentLoaded', function() { } else { siteBaseUrl = "https://lean-ja.github.io/lean-by-example/"; } - const summaryMdUrl = "https://raw.githubusercontent.com/lean-ja/lean-by-example/main/booksrc/SUMMARY.md"; + const summaryMdUrl = "https://raw.githubusercontent.com/lean-ja/lean-by-example/main/LeanByExample/SUMMARY.lean"; // キャッシュ用の変数 let summaryLinks = null; From 839f10c5eb45286e9eec32f14ec68e0f38cc93d3 Mon Sep 17 00:00:00 2001 From: Seasawher <47292598+Seasawher@users.noreply.github.com> Date: Sun, 14 Jun 2026 00:12:50 +0900 Subject: [PATCH 4/4] =?UTF-8?q?URL=20=E7=94=9F=E6=88=90=E5=87=A6=E7=90=86?= =?UTF-8?q?=E3=81=AE=E5=BE=AE=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- assets/randomPage.js | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/assets/randomPage.js b/assets/randomPage.js index 1f85ff8f..dd970db5 100644 --- a/assets/randomPage.js +++ b/assets/randomPage.js @@ -90,8 +90,8 @@ document.addEventListener('DOMContentLoaded', function() { continue; } - // 最終的に本番サイトのURLとして構築 - const fullUrl = siteBaseUrl + processedUrl; + // 最終的にサイト内のURLとして構築し、`./` などを正規化する + const fullUrl = new URL(processedUrl, siteBaseUrl).href; // 本番サイトのURLとしてリンクを追加 links.push(fullUrl);