mdbook setup

.github/workflows/book.yml

@@ -8,6 +8,15 @@ jobs:
     steps:
     - uses: actions/checkout@v3
 
+    - name: install elan
+      run: |
+        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
+
     - 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
 

.github/workflows/deploy.yml

@@ -0,0 +1,56 @@
+name: Deploy to github pages
+
+on: [push, pull_request]
+
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued.
+# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete.
+concurrency:
+  group: "pages"
+  cancel-in-progress: false
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+
+      - name: install elan
+        run: |
+          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
+
+      - name: setup mdBook
+        uses: peaceiris/actions-mdbook@v1
+        with:
+          mdbook-version: '0.4.32'
+
+      - name: build html from markdown
+        run: mdbook build
+
+      - name: upload artifact
+        uses: actions/upload-pages-artifact@v2
+        with:
+          path: ./book
+
+  deploy:
+    if: github.ref == 'refs/heads/master'
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    needs: build
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v3

.gitignore

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

book.toml

@@ -0,0 +1,9 @@
+[book]
+authors = ["Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, Siddharth Bhat"]
+language = "en"
+multilingual = false
+src = "md"
+title = "Metaprogramming in Lean 4"
+
+[output.html]
+git-repository-url = "https://github.com/leanprover-community/lean4-metaprogramming-book"

md/SUMMARY.md

@@ -0,0 +1,18 @@
+# Summary
+
+- [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)