Merge pull request #137 from Seasawher/fix-mdbook-setting

fix issue on mdbook config

Author: Julian

.github/workflows/book.yml

@@ -18,9 +18,8 @@ jobs:
         curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)
         echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-    # note: `lake run build` raise an error in GitHub Action
     - name: build markdown files by mdgen
-      run: lake exe mdgen lean md
+      run: lake run build
 
     - name: Install Dependencies
       run: sudo apt update && sudo apt install -y pandoc texlive-latex-base texlive-latex-extra texlive-latex-recommended texlive-luatex fonts-dejavu python3-pygments
@@ -31,7 +30,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/SUMMARY.md | sed 's/^/md/') --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

.github/workflows/deploy.yml

@@ -31,9 +31,8 @@ jobs:
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      # note: `lake run build` raise an error in GitHub Action
       - name: build markdown files by mdgen
-        run: lake exe mdgen lean md
+        run: lake run build
 
       - name: setup mdBook
         uses: peaceiris/actions-mdbook@v1

.gitignore

@@ -1,4 +1,4 @@
-/build
 .lake/
-book
-md/
+/book
+/md/*
+!/md/SUMMARY.md

SUMMARY.md

@@ -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]

book.toml

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