Merge pull request #130 from Seasawher/add-solutions

Add solutions

Author: Julian

.github/workflows/book.yml

@@ -1,6 +1,11 @@
 name: Book
 
-on: [push, pull_request]
+on:
+  pull_request:
+  push:
+    branches:
+      - master
+  workflow_dispatch:
 
 jobs:
   book:
@@ -26,7 +31,7 @@ jobs:
 
     - name: Build Some LaTeX
       run: |
-        pandoc --to latex md/cover.md $(grep -o '\(md/.*\.md\)' CONTENTS.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 | 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

.github/workflows/deploy.yml

@@ -1,6 +1,11 @@
 name: Deploy to github pages
 
-on: [push, pull_request]
+on:
+  pull_request:
+  push:
+    branches:
+      - master
+  workflow_dispatch:
 
 # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:

.gitignore

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

CONTENTS.md

@@ -2,7 +2,7 @@
 
 Authors: Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, Siddharth Bhat
 
-* Tha textbook in html format is [here](https://leanprover-community.github.io/lean4-metaprogramming-book/).
+* The textbook in html format is [here](https://leanprover-community.github.io/lean4-metaprogramming-book/).
 
 * A PDF is [available here for download](../../releases/download/latest/Metaprogramming.in.Lean.4.pdf) (and is rebuilt on each change).
 

README.md

@@ -0,0 +1,32 @@
+# 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)

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 = "md"
+src = "."
 title = "Metaprogramming in Lean 4"
 
 [output.html]