演習問題フォルダの場所を変える

.github/workflows/sync.yml

@@ -9,7 +9,7 @@ on:
     branches:
       - main
     paths:
-      - 'Examples/Exercise/**'
+      - 'Exercise/**'
       - 'Examples/Solution/**'
       - '.github/workflows/sync.yml'
       - 'lakefile.lean'
@@ -18,7 +18,7 @@ on:
     branches:
       - main
     paths:
-      - 'Examples/Exercise/**'
+      - 'Exercise/**'
       - 'Examples/Solution/**'
       - '.github/workflows/sync.yml'
       - 'lakefile.lean'
@@ -48,13 +48,13 @@ jobs:
       # いったん演習ファイルを全て削除している
       - name: run mk_exercise
         run: |
-          rm -r Examples/Exercise
+          rm -r Exercise
           lake run mk_exercise
 
       - name: detect diff
         id: diff
         run: |
-          git add -N Examples/Exercise
+          git add -N Exercise
           git diff --name-only --exit-code
         continue-on-error: true
 
@@ -63,6 +63,6 @@ jobs:
         run: |
           git config user.name "GitHub Action"
           git config user.email "[email protected]"
-          git add Examples/Exercise
+          git add Exercise
           git commit -m "generated by GitHub Action"
           git push origin HEAD:${{ github.event.pull_request.head.ref }}

CONTRIBUTING.md

@@ -17,7 +17,7 @@
 ## 開発の流れ
 
 * このリポジトリは mathlib に依存しているので、このリポジトリを clone した後に `lake exe cache get` を実行してください。
-* `Examples/Exercise` 配下のファイルは `mk_exercise` により `Examples/Solution` の内容から自動生成されるので、手動で編集しないでください。
+* `Exercise` ディレクトリ配下のファイルは `mk_exercise` により `Examples/Solution` の内容から自動生成されるので、手動で編集しないでください。
 * 本文の markdown ファイルは [mdgen](https://github.com/Seasawher/mdgen) を用いて Lean ファイルから生成します。Lean ファイルを編集した後、`lake run build` コマンドを実行すれば mk_exercise の実行と markdown の生成と `mdbook build` が一括実行されます。
 
 ## ルール

assets/filePlay.js

@@ -21,6 +21,9 @@
   // Lean ファイルがあるのは `src` ではなく `Examples` ディレクトリ
   editButtonLink.href = editButtonLink.href.replace('/src/', '/Examples/');
 
+  // 演習問題のファイルのみ、`Examples` ディレクトリではなくて `Exercise` ディレクトリにある
+  editButtonLink.href = editButtonLink.href.replace('/Examples/Exercise/', '/Exercise/');
+
   // ボタンをクリックしたときに以下を実行
   editButtonLink.addEventListener('click', async function (e) {
     // デフォルトの挙動をキャンセル

lakefile.lean

@@ -20,13 +20,7 @@ require mathlib from git
 lean_lib Examples where
   -- `lake build` の実行時にビルドされるファイルの設定
   -- `.submodules` と指定すると、そのディレクトリ以下の全ての Lean ファイルがビルドされる
-  -- ここでは `Examples/Exercise` 以外の、`Examples` ディレクトリの内容を指定
-  globs := #[
-    .submodules `Examples.Command,
-    .submodules `Examples.Solution,
-    .submodules `Examples.Tactic,
-    .submodules `Examples.Term
-  ]
+  globs := #[.submodules `Examples]
 
 section Script
 
@@ -48,7 +42,7 @@ section Script
 /-- mk_exercise を実行し、演習問題の解答に
 解答部分を sorry に置き換えるなどの処理を施して演習問題ファイルを生成する。-/
 script mk_exercise do
-  runCmd "lake exe mk_exercise Examples/Solution Examples/Exercise"
+  runCmd "lake exe mk_exercise Examples/Solution Exercise"
   return 0
 
 syntax (name := with_time) "with_time" "running" str doElem : doElem
@@ -67,10 +61,11 @@ script build do
 
   -- `lake run mk_exercise` を使用すると遅くなってしまうのでコピペしている
   with_time running "mk_exercise"
-    runCmd "lake exe mk_exercise Examples/Solution Examples/Exercise"
+    runCmd "lake exe mk_exercise Examples/Solution Exercise"
 
   with_time running "mdgen"
-    runCmd "lake exe mdgen Examples src"
+    runCmd "lake exe mdgen Examples src";
+    runCmd "lake exe mdgen Exercise src/Exercise"
 
   with_time running "mdbook"
     runCmd "mdbook build"