Split blueprint into several files

Signed-off-by: zeramorphic <[email protected]>

blueprint/src/chapters/auxiliary.tex

@@ -1,6 +1,6 @@
 \section{Relations}
 
-\begin{definition-no-bp}
+\begin{definition}
   \label{def:relation_props}
   Let \( R : \sigma \to \tau \to Prop \).
   We define
@@ -29,8 +29,9 @@ \section{Relations}
   \end{itemize}
   We also define the \emph{graph} of a function \( f : \sigma \to \tau \) to be the functional relation \( R : \sigma \to \tau \to \Prop \) given by \( (x, y) \in R \) if and only if \( f(x) = y \).
   Most of these definitions are from \url{https://www.kylem.net/math/relations.html}, and most of these are in mathlib under \texttt{Mathlib.Logic.Relator}.
-\end{definition-no-bp}
-\begin{proposition-no-bp}\mbox\negthinspace
+\end{definition}
+\begin{proposition}\mbox\negthinspace
+  \uses{def:relation_props}
   \label{prop:relation_results}
   \begin{enumerate}
     \item \( R : \tau \to \tau \to \Prop \) is permutative if and only if it is one-to-one and for all \( x : \tau \), there exists \( y \) such that \( x \mathrel{R} y \) if and only if there exists \( y \) such that \( y \mathrel{R} x \).
@@ -39,7 +40,7 @@ \section{Relations}
     \item If \( R \) is permutative, then \( \coim R^n = \coim R = \im R = \im R^n \) for any natural number or integer \( n \).
     \item If \( R \) is permutative and \( s_1, s_2 \subseteq \coim R \), then the image of \( R \) on \( s_1 \) is equal to \( s_2 \) if and only if the coimage of \( R \) on \( s_2 \) is equal to \( s_1 \).
   \end{enumerate}
-\end{proposition-no-bp}
+\end{proposition}
 \begin{definition}
   \label{def:OrbitRestriction}
   Let \( s : \Set \tau \).
@@ -92,11 +93,11 @@ \section{Relations}
 
 \section{Cardinal arithmetic}
 
-\begin{lemma-no-bp}[mathlib]
+\begin{lemma}[mathlib]
   \label{prop:card_subset_card_lt_cof}
   Let \( \#\mu \) be a strong limit cardinal.
   Then there are precisely \( \#\mu \)-many subsets of \( \mu \) of size strictly less than \( \cof(\ord(\#\mu)) \).
-\end{lemma-no-bp}
+\end{lemma}
 \begin{proof}
   Endow \( \mu \) with its initial well-ordering.
   Each such subset is bounded in \( \mu \) with respect to this well-ordering as its size is less than \( \cof(\ord(\#\mu)) \).

blueprint/src/macro/web.tex

@@ -1,3 +1,11 @@
 \newcommand{\symmdiff}{\mathrel{\triangle}}
 \newcommand{\coloneq}{:=}
 \newcommand{\pcomp}{\mathbin{\cdot}} % path composition
+
+\graphcolor{stated}{#187A2A}{Green}
+\graphcolor{can_state}{#184F7A}{Blue}
+\graphcolor{not_ready}{#FFAA33}{Orange}
+\graphcolor{proved}{#9CEC8B}{Green}
+\graphcolor{can_prove}{#A3D6FF}{Blue}
+\graphcolor{defined}{#B0ECA3}{Light green}
+\graphcolor{fully_proved}{#1CAC78}{Dark green}

blueprint/src/plastex.cfg

@@ -9,7 +9,7 @@ toc-non-files=True
 
 [files]
 directory=../web/
-split-level=0
+split-level=1
 
 [html5]
 localtoc-level=0

blueprint/src/web.tex

@@ -16,7 +16,7 @@
 	urlcolor=magenta!70!black,
 }
 
-\usepackage[showmore,dep_graph, project=../../]{blueprint}
+\usepackage[showmore, dep_graph, coverage, project=../../, dep_by=chapter]{blueprint}
 
 \input{macro/common}
 

blueprint/tasks.py

@@ -1,5 +1,6 @@
 import os
 import random
+import re
 from pathlib import Path
 import http.server
 import socketserver
@@ -25,18 +26,48 @@ def web(ctx):
     os.chdir(BP_DIR/'src')
     run('plastex -c plastex.cfg web.tex')
     os.chdir(BP_DIR/'web')
-    with open('dep_graph_document.html', 'r') as f:
-        s = f.read()
-    with open('dep_graph_document.html', 'w') as f:
-        def replace(line):
-            if ".renderDot" in line:
-                return line.replace('[', '[fontname="Open Sans",')
-            elif "theme-white.css" in line:
-                return line + '\n<link rel="stylesheet" href="styles/extra_styles.css" />'
-            else:
-                return line
-        s = '\n'.join(replace(line) for line in s.split('\n'))
-        f.write(s)
+
+    nonempty_graphs = []
+    for file in os.listdir('.'):
+        filename = os.fsdecode(file)
+        if filename.startswith("dep_graph"):
+            with open(filename, 'r') as f:
+                s = f.read()
+                for line in s.split('\n'):
+                    if ".renderDot" in line:
+                        if re.search('"[a-zA-Z]', line):
+                            # This is a good heuristic for whether a graph has a node or not.
+                            nonempty_graphs.append(filename)
+            with open(filename, 'w') as f:
+                def replace(line):
+                    if ".renderDot" in line:
+                        # Replace the font with Open Sans.
+                        return line.replace('[', '[fontname="Open Sans",')
+                    elif "theme-white.css" in line:
+                        return line + '\n<link rel="stylesheet" href="styles/extra_styles.css" />'
+                    else:
+                        return line
+                s = '\n'.join(replace(line) for line in s.split('\n'))
+                f.write(s)
+
+    for file in os.listdir('.'):
+        filename = os.fsdecode(file)
+        if filename.endswith(".html"):
+            with open(filename, 'r') as f:
+                s = f.read()
+            with open(filename, 'w') as f:
+                # Remove empty dependency graphs.
+                to_remove = []
+                for match in re.finditer(r'<li ><a href="([a-zA-Z0-9_.]*)">Chapter [a-zA-Z0-9]* graph<\/a><\/li>', s):
+                    if match.group(1) not in nonempty_graphs:
+                        to_remove.append(match.group(0))
+                for item in to_remove:
+                    s = s.replace(item, '')
+
+                # Replace "Chapter A" with "Appendix A".
+                s = re.sub(r"Chapter ([A-Z])", r"Appendix \1", s)
+                f.write(s)
+
     os.chdir(cwd)
 
 @task