compile

Makefile

@@ -0,0 +1,11 @@
+GENDIR := html/src/generated
+build-to-html:
+	find src/HottBook \( -name "*.agda" -o -name "*.lagda.md" \) -print0 \
+	  | rust-parallel -0 agda --html --html-dir=$(GENDIR) --html-highlight=auto || true
+	fd --no-ignore "html$$" $(GENDIR) -x rm
+
+deploy: build-to-html
+	mdbook build html
+	rsync -azrP html/book/ root@veil:/home/blogDeploy/public/hott-book
+
+.PHONY: build-to-html deploy

html/.gitignore

@@ -0,0 +1,3 @@
+book
+src/generated/*
+!src/generated/.gitkeep

html/book.toml

@@ -0,0 +1,9 @@
+[book]
+authors = ["Michael Zhang"]
+language = "en"
+multilingual = false
+src = "src"
+title = "HoTT Book"
+
+[output.html]
+additional-css = ["src/generated/Agda.css", "style.css"]

html/src/SUMMARY.md

@@ -0,0 +1,7 @@
+# Summary
+
+- [Chapter 1](./generated/HottBook.Chapter1.md)
+- [Chapter 2](./generated/HottBook.Chapter2.md)
+- [Chapter 3](./generated/HottBook.Chapter3.md)
+- [Chapter 4](./generated/HottBook.Chapter4.md)
+- [Chapter 5](./generated/HottBook.Chapter5.md)

html/style.css

@@ -0,0 +1,13 @@
+
+@font-face {
+    font-family: "PragmataPro Mono Liga";
+    src:
+      url("/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2") format("woff2"),
+      url("https://mzhang.io/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2")
+        format("woff2");
+  }
+    
+
+pre.Agda  {
+    font-family: "PragmataPro Mono Liga", monospace;
+}

src/HottBook/Chapter2.lagda.md

@@ -1,13 +1,13 @@
 <details>
   <summary>Imports</summary>
 
-  ```
-  module HottBook.Chapter2 where
+```
+module HottBook.Chapter2 where
 
-  open import Agda.Primitive
-  open import HottBook.Chapter1
-  open import HottBook.Util
-  ```
+open import Agda.Primitive
+open import HottBook.Chapter1
+open import HottBook.Util
+```
 
 </details>