Skip to content

Commit

Permalink
fix issue on mdbook config
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Seasawher committed Apr 8, 2024
1 parent 3ef475b commit 2683f9a
Show file tree
Hide file tree
Showing 5 changed files with 37 additions and 37 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/book.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
/build
.lake/
book
md/
/book
/md/*
!/md/SUMMARY.md
32 changes: 0 additions & 32 deletions SUMMARY.md

This file was deleted.

2 changes: 1 addition & 1 deletion book.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
32 changes: 32 additions & 0 deletions md/SUMMARY.md
Original file line number Diff line number Diff line change
@@ -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)

0 comments on commit 2683f9a

Please sign in to comment.