Add set_option pp.explicit false in Weak Head Normal Form example
#152
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Book | |
| on: | |
| pull_request: | |
| push: | |
| branches: | |
| - master | |
| workflow_dispatch: | |
| jobs: | |
| book: | |
| runs-on: ubuntu-latest | |
| 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 | |
| - name: build markdown files by mdgen | |
| 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 | |
| - name: Download the Book Template | |
| run: | | |
| curl -L https://github.com/Wandmalfarbe/pandoc-latex-template/releases/download/v2.0.0/Eisvogel.tar.gz | tar -xz eisvogel.latex | |
| - name: Build Some LaTeX | |
| run: | | |
| 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 | |
| # Running twice appears to be necessary to not get a blank TOC?! | |
| run: lualatex -shell-escape out.tex && lualatex -shell-escape out.tex | |
| - name: Rename | |
| # Minted doesn't like filenames with spaces in them unfortunately, so we mv. | |
| run: mv out.tex 'Metaprogramming in Lean 4.tex' && mv out.pdf 'Metaprogramming in Lean 4.pdf' | |
| - name: Upload PDF to artifact storage | |
| if: github.ref != 'refs/heads/master' | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: "Metaprogramming in Lean 4" | |
| path: "Metaprogramming in Lean 4.pdf" | |
| - uses: "marvinpinto/action-automatic-releases@latest" | |
| if: github.ref == 'refs/heads/master' | |
| with: | |
| repo_token: "${{ secrets.GITHUB_TOKEN }}" | |
| automatic_release_tag: "latest" | |
| title: "Metaprogramming in Lean 4" | |
| files: | | |
| Metaprogramming in Lean 4.tex | |
| Metaprogramming in Lean 4.pdf |