From 5c35f42bafffb2a3dd8321050a826789dd67c7a4 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Fri, 17 May 2024 01:49:10 -0500
Subject: [PATCH] compile

---
 Makefile                       | 11 +++++++++++
 html/.gitignore                |  3 +++
 html/book.toml                 |  9 +++++++++
 html/src/SUMMARY.md            |  7 +++++++
 html/src/generated/.gitkeep    |  0
 html/style.css                 | 13 +++++++++++++
 src/HottBook/Chapter2.lagda.md | 12 ++++++------
 7 files changed, 49 insertions(+), 6 deletions(-)
 create mode 100644 Makefile
 create mode 100644 html/.gitignore
 create mode 100644 html/book.toml
 create mode 100644 html/src/SUMMARY.md
 create mode 100644 html/src/generated/.gitkeep
 create mode 100644 html/style.css

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..9d857fe
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/html/.gitignore b/html/.gitignore
new file mode 100644
index 0000000..882e309
--- /dev/null
+++ b/html/.gitignore
@@ -0,0 +1,3 @@
+book
+src/generated/*
+!src/generated/.gitkeep
\ No newline at end of file
diff --git a/html/book.toml b/html/book.toml
new file mode 100644
index 0000000..8e59a01
--- /dev/null
+++ b/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"]
diff --git a/html/src/SUMMARY.md b/html/src/SUMMARY.md
new file mode 100644
index 0000000..22b9b34
--- /dev/null
+++ b/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)
\ No newline at end of file
diff --git a/html/src/generated/.gitkeep b/html/src/generated/.gitkeep
new file mode 100644
index 0000000..e69de29
diff --git a/html/style.css b/html/style.css
new file mode 100644
index 0000000..c66e210
--- /dev/null
+++ b/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;
+}
\ No newline at end of file
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 16f3fca..6399a63 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/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>