From 2683f9a2035162f5ce1f7371bc548c230ff2d6b5 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 9 Apr 2024 02:42:23 +0900
Subject: [PATCH] fix issue on mdbook config

The current directory should not be specified as the src directory. This causes a problem where the `.git` directory is copied into the `book` directory.
---
 .github/workflows/book.yml |  2 +-
 .gitignore                 |  6 +++---
 SUMMARY.md                 | 32 --------------------------------
 book.toml                  |  2 +-
 md/SUMMARY.md              | 32 ++++++++++++++++++++++++++++++++
 5 files changed, 37 insertions(+), 37 deletions(-)
 delete mode 100644 SUMMARY.md
 create mode 100644 md/SUMMARY.md

diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml
index 1bf7a52..ce41b35 100644
--- a/.github/workflows/book.yml
+++ b/.github/workflows/book.yml
@@ -31,7 +31,7 @@ jobs:
 
     - name: Build Some LaTeX
       run: |
-        pandoc --to latex md/cover.md $(grep -o '\(md/.*\.md\)' SUMMARY.md | tr -d '(' | tr -d ')') --toc --template ./eisvogel.latex --top-level-division=chapter -V documentclass=book -V classoption=oneside --no-highlight |
+        pandoc --to latex md/cover.md $(grep -o '\(md/.*\.md\)' md/SUMMARY.md | tr -d '(' | tr -d ')') --toc --template ./eisvogel.latex --top-level-division=chapter -V documentclass=book -V classoption=oneside --no-highlight |
           sed -e 's/\\begin{verbatim}/\\begin{minted}{Lean}/' -e 's/{verbatim}/{minted}/' -e's/% Listings/\\usepackage{minted}\n\\newmintinline[lean]{pygments\/lean4.py:Lean4Lexer -x}{bgcolor=white}\n\\newminted[leancode]{pygments\/lean4.py:Lean4Lexer -x}{fontsize=\\footnotesize}\n\\setminted{fontsize=\\footnotesize, breaklines}\n/' >out.tex
 
     - name: Build a PDF
diff --git a/.gitignore b/.gitignore
index 0c1dd39..190be4d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,4 @@
-/build
 .lake/
-book
-md/
\ No newline at end of file
+/book
+/md/*
+!/md/SUMMARY.md
\ No newline at end of file
diff --git a/SUMMARY.md b/SUMMARY.md
deleted file mode 100644
index 34cca69..0000000
--- a/SUMMARY.md
+++ /dev/null
@@ -1,32 +0,0 @@
-# Summary
-
-# Main
-
-- [Introduction](md/main/01_intro.md)
-- [Overview](md/main/02_overview.md)
-- [Expressions](md/main/03_expressions.md)
-- [MetaM](md/main/04_metam.md)
-- [Syntax](md/main/05_syntax.md)
-- [Macros](md/main/06_macros.md)
-- [Elaboration](md/main/07_elaboration.md)
-- [Embedding DSLs By Elaboration](md/main/08_dsls.md)
-- [Tactics](md/main/09_tactics.md)
-- [Lean4 Cheat-sheet](md/main/10_cheat-sheet.md)
-
-# Extra
-
-- [Options](md/extra/01_options.md)
-- [Attributes]()
-- [Pretty Printing](md/extra/03_pretty-printing.md)
-
-# Solutions
-
-- [Introduction]()
-- [Overview]()
-- [Expressions](md/solutions/03_expressions.md)
-- [`MetaM`](md/solutions/04_metam.md)
-- [`Syntax`](md/solutions/05_syntax.md)
-- [Macros]()
-- [Elaboration](md/solutions/07_elaboration.md)
-- [DSLs]()
-- [Tactics](md/solutions/09_tactics.md)
diff --git a/book.toml b/book.toml
index cfd8de7..5a46334 100644
--- a/book.toml
+++ b/book.toml
@@ -2,7 +2,7 @@
 authors = ["Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, Siddharth Bhat"]
 language = "en"
 multilingual = false
-src = "."
+src = "md"
 title = "Metaprogramming in Lean 4"
 
 [output.html]
diff --git a/md/SUMMARY.md b/md/SUMMARY.md
new file mode 100644
index 0000000..59477ec
--- /dev/null
+++ b/md/SUMMARY.md
@@ -0,0 +1,32 @@
+# Summary
+
+# Main
+
+- [Introduction](./main/01_intro.md)
+- [Overview](./main/02_overview.md)
+- [Expressions](./main/03_expressions.md)
+- [MetaM](./main/04_metam.md)
+- [Syntax](./main/05_syntax.md)
+- [Macros](./main/06_macros.md)
+- [Elaboration](./main/07_elaboration.md)
+- [Embedding DSLs By Elaboration](./main/08_dsls.md)
+- [Tactics](./main/09_tactics.md)
+- [Lean4 Cheat-sheet](./main/10_cheat-sheet.md)
+
+# Extra
+
+- [Options](./extra/01_options.md)
+- [Attributes]()
+- [Pretty Printing](./extra/03_pretty-printing.md)
+
+# Solutions
+
+- [Introduction]()
+- [Overview]()
+- [Expressions](./solutions/03_expressions.md)
+- [`MetaM`](./solutions/04_metam.md)
+- [`Syntax`](./solutions/05_syntax.md)
+- [Macros]()
+- [Elaboration](./solutions/07_elaboration.md)
+- [DSLs]()
+- [Tactics](./solutions/09_tactics.md)