booksrc ディレクトリの中身を空っぽにする

.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 ファイルのファイル名は、パスカルケースで命名して下さい。

.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

booksrc/404.md → LeanByExample/404.lean

@@ -1,5 +1,5 @@
-# 404 エラー
+/- # 404 エラー
 
 お探しのページが見つかりませんでした。
 
-URL が変更された可能性があります。ご迷惑をおかけして申し訳ございません。
+URL が変更された可能性があります。ご迷惑をおかけして申し訳ございません。 -/

booksrc/SUMMARY.md → 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) -/

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スタートアップ企業です。数理科学の力で社会を変えることを企業の使命としています。

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;
@@ -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);

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e061a86b0e168c6d37f535595d719899b7f131fb",
+   "rev": "c003ac1229883b25d3b9e5df2fc0b2da453d3c8a",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

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上では実行するべき