Setup for local navigation between Lean index and LaTeX.

Bookshelf/Real/Sequence.tex

@@ -1,34 +1,35 @@
 \documentclass{article}
 
-\input{../../preamble}
+\input{preamble}
+
+\newcommand{\linkA}[1]{\href{/doc/Bookshelf/Real/Sequence/Arithmetic.html\##1}{#1}}
+\newcommand{\linkG}[1]{\href{/doc/Bookshelf/Real/Sequence/Geometric.html\##1}{#1}}
 
 \begin{document}
 
-\begin{theorem}[Sum of Arithmetic Series]
+\section*{Sum of Arithmetic Series}%
+\label{sec:sum-arithmetic-series}
 
-  Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$.
+Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$.
-  Then for some $n \in \mathbb{N}$,
+Then for some $n \in \mathbb{N}$,
-  $$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$
+$$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$
-
-\end{theorem}
 
 \begin{proof}
 
-  \href{Sequence/Arithmetic.lean}{Bookshelf.Real.Sequence.Arithmetic.sum_recursive_closed}
+  \linkA{Real.Arithmetic.sum\_recursive\_closed}
 
 \end{proof}
 
-\begin{theorem}[Sum of Geometric Series]
+\section*{Sum of Geometric Series}%
+\label{sec:sum-geometric-series}
 
-  Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$.
+Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$.
-  Then for some $n \in \mathbb{N}$,
+Then for some $n \in \mathbb{N}$,
-  $$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$
+$$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$
-
-\end{theorem}
 
 \begin{proof}
 
-  \href{Sequence/Geometric.lean}{Bookshelf.Real.Sequence.Geometric.sum_recursive_closed}
+  \linkG{Real.Geometric.sum\_recursive\_closed}
 
 \end{proof}
 

MathematicalIntroductionLogic/Enderton/Chapter0.tex

@@ -1,19 +1,20 @@
 \documentclass{article}
 
-\input{../../preamble}
+\input{preamble}
+
+\newcommand{\link}[1]{\href{/doc/MathematicalIntroductionLogic/Enderton/Chapter0.html\##1}{#1}}
 
 \begin{document}
 
-\begin{theorem}[Lemma 0A]
+\section*{Lemma 0A}%
+\label{sec:lemma-0a}
 
-  Assume that $\langle x_1, \ldots, x_m \rangle = \langle y_1, \ldots, y_m, \ldots, y_{m+k} \rangle$.
+Assume that $\langle x_1, \ldots, x_m \rangle = \langle y_1, \ldots, y_m, \ldots, y_{m+k} \rangle$.
-  Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$.
+Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$.
-
-\end{theorem}
 
 \begin{proof}
 
-  \href{Chapter0.lean}{Enderton.Chapter0.lemma_0a}
+  \link{lemma\_0a}
 
 \end{proof}
 

MockMockingbird/Aviary.tex

@@ -1,14 +1,16 @@
 \documentclass{article}
 
-\input{../preamble}
+\input{preamble}
 
 \begin{document}
 
 \newcommand{\bird}[1]{\item{\makebox[5cm][l]{\textbf{#1:}}}}
 
-A list of birds as defined in \textit{To Mock a Mockingbird}.
+\section*{Aviary}%
+\label{sec:aviary}
 
-Refer to \href{Aviary.lean}{Smullyan/Aviary.lean} for implementation examples.
+A list of birds as defined in \textit{To Mock a Mockingbird}.
+Refer to \href{/doc/MockMockingbird/Aviary.html}{MockMockingbird/Aviary} for implementation examples.
 
 \begin{itemize}
   \bird{Bald Eagle} $\hat{E}xy_1y_2y_3z_1z_2z_3 = x(y_1y_2y_3)(z_1z_2z_3)$

OneVariableCalculus/Apostol/Chapter_I_3.tex

@@ -1,123 +1,114 @@
 \documentclass{article}
 \usepackage[shortlabels]{enumitem}
 
-\input{../../../preamble}
+\input{preamble}
+
+\newcommand{\link}[1]{\href{/doc/OneVariableCalculus/Apostol/Chapter_I_3.html\##1}{#1}}
 
 \begin{document}
 
-\begin{xtheorem}{I.27}
+\section*{Theorem I.27}%
+\label{sec:theorem-i.27}
 
-  Every nonempty set $S$ that is bounded below has a greatest lower bound; that
+Every nonempty set $S$ that is bounded below has a greatest lower bound; that
-  is, there is a real number $L$ such that $L = \inf{S}$.
+is, there is a real number $L$ such that $L = \inf{S}$.
-
-\end{xtheorem}
 
 \begin{proof}
 
-  \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.exists_isGLB}
+  \link{Real.exists\_isGLB}
 
 \end{proof}
 
-\begin{xtheorem}{I.29}
+\section*{Theorem I.29}%
+\label{sec:theorem-i.29}
 
-  For every real $x$ there exists a positive integer $n$ such that $n > x$.
+For every real $x$ there exists a positive integer $n$ such that $n > x$.
-
-\end{xtheorem}
 
 \begin{proof}
 
-  \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.exists_pnat_geq_self}
+  \link{Real.exists\_pnat\_geq\_self}
 
 \end{proof}
 
-\begin{xtheorem}{I.30}[Archimedean Property of the Reals]
+\section*{Theorem I.30 (Archimedean Property of the Reals)}%
+\label{sec:theorem-i.30}
 
-  If $x > 0$ and if $y$ is an arbitrary real number, there exists a positive
+If $x > 0$ and if $y$ is an arbitrary real number, there exists a positive
-  integer $n$ such that $nx > y$.
+integer $n$ such that $nx > y$.
-
-\end{xtheorem}
 
 \begin{proof}
 
-  \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.exists_pnat_mul_self_geq_of_pos}
+  \link{Real.exists\_pnat\_mul\_self\_geq\_of\_pos}
 
 \end{proof}
 
-\begin{xtheorem}{I.31}
+\section*{Theorem I.31}%
+\label{sec:theorem-i.31}
 
-  If three real numbers $a$, $x$, and $y$ satisfy the inequalities
+If three real numbers $a$, $x$, and $y$ satisfy the inequalities
-  $$a \leq x \leq a + \frac{y}{n}$$
+$$a \leq x \leq a + \frac{y}{n}$$
-  for every integer $n \geq 1$, then $x = a$.
+for every integer $n \geq 1$, then $x = a$.
-
-\end{xtheorem}
 
 \begin{proof}
 
-  \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.forall_pnat_leq_self_leq_frac_imp_eq}
+  \link{Real.forall\_pnat\_leq\_self\_leq\_frac\_imp\_eq}
 
 \end{proof}
 
-\begin{xtheorem}{I.32}
+\section*{Theorem I.32}%
+\label{sec:theorem-i.32}
 
-  Let $h$ be a given positive number and let $S$ be a set of real numbers.
+Let $h$ be a given positive number and let $S$ be a set of real numbers.
-  \begin{enumerate}[(a)]
+\begin{enumerate}[(a)]
-    \item If $S$ has a supremum, then for some $x$ in $S$ we have
+  \item If $S$ has a supremum, then for some $x$ in $S$ we have
-      $$x > \sup{S} - h.$$
+    $$x > \sup{S} - h.$$
-    \item If $S$ has an infimum, then for some $x$ in $S$ we have
+  \item If $S$ has an infimum, then for some $x$ in $S$ we have
-      $$x < \inf{S} + h.$$
+    $$x < \inf{S} + h.$$
-  \end{enumerate}
+\end{enumerate}
-
-\end{xtheorem}
 
 \begin{proof}
 
-  \  % Force space prior to *Proof.*
-
   \begin{enumerate}[(a)]
-    \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.sup_imp_exists_gt_sup_sub_delta}
+    \item \link{Real.sup\_imp\_exists\_gt\_sup\_sub\_delta}
-    \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.inf_imp_exists_lt_inf_add_delta}
+    \item \link{Real.inf\_imp\_exists\_lt\_inf\_add\_delta}
   \end{enumerate}
 
 \end{proof}
 
-\begin{xtheorem}{I.33}[Additive Property]
+\section*{Theorem I.33 (Additive Property)}%
+\label{sec:theorem-i.33}
 
-  Given nonempty subsets $A$ and $B$ of $\mathbb{R}$, let $C$ denote the set
+Given nonempty subsets $A$ and $B$ of $\mathbb{R}$, let $C$ denote the set
-  $$C = \{a + b : a \in A, b \in B\}.$$
+$$C = \{a + b : a \in A, b \in B\}.$$
 
-  \begin{enumerate}[(a)]
+\begin{enumerate}[(a)]
-    \item If each of $A$ and $B$ has a supremum, then $C$ has a supremum, and
+  \item If each of $A$ and $B$ has a supremum, then $C$ has a supremum, and
-      $$\sup{C} = \sup{A} + \sup{B}.$$
+    $$\sup{C} = \sup{A} + \sup{B}.$$
-    \item If each of $A$ and $B$ has an infimum, then $C$ has an infimum, and
+  \item If each of $A$ and $B$ has an infimum, then $C$ has an infimum, and
-      $$\inf{C} = \inf{A} + \inf{B}.$$
+    $$\inf{C} = \inf{A} + \inf{B}.$$
-  \end{enumerate}
+\end{enumerate}
-
-\end{xtheorem}
 
 \begin{proof}
 
-  \  % Force space prior to *Proof.*
-
   \begin{enumerate}[(a)]
-    \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.sup_minkowski_sum_eq_sup_add_sup}
+    \item \link{Real.sup\_minkowski\_sum\_eq\_sup\_add\_sup}
-    \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.inf_minkowski_sum_eq_inf_add_inf}
+    \item \link{Real.inf\_minkowski\_sum\_eq\_inf\_add\_inf}
   \end{enumerate}
 
 \end{proof}
 
-\begin{xtheorem}{I.34}
+\section*{Theorem I.34}%
+\label{sec:theorem-i.34}
 
-  Given two nonempty subsets $S$ and $T$ of $\mathbb{R}$ such that
+Given two nonempty subsets $S$ and $T$ of $\mathbb{R}$ such that
-  $$s \leq t$$
+$$s \leq t$$
-  for every $s$ in $S$ and every $t$ in $T$. Then $S$ has a supremum, and $T$
+for every $s$ in $S$ and every $t$ in $T$. Then $S$ has a supremum, and $T$
-  has an infimum, and they satisfy the inequality
+has an infimum, and they satisfy the inequality
-  $$\sup{S} \leq \inf{T}.$$
+$$\sup{S} \leq \inf{T}.$$
-
-\end{xtheorem}
 
 \begin{proof}
 
-  \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.forall_mem_le_forall_mem_imp_sup_le_inf}
+  \link{Real.forall\_mem\_le\_forall\_mem\_imp\_sup\_le\_inf}
 
 \end{proof}
 

README.md

@@ -26,4 +26,15 @@ Run the following to build and serve this:
 
 This assumes you have `python3` available in your `$PATH`. To change how the
 server behaves, refer to the `.env` file located in the root directory of this
-project.
+project. To also serve the corresponding LaTeX files scattered throughout this
+project, first install the following:
+
+- `tex4ht`
+- `make4ht`
+- `luaxml`
+
+Afterward, you can generate the necessary HTML via:
+
+```bash
+> find . -name '*.tex' | grep -v preamble | xargs -I {} make4ht -e build.mk4 {}
+```

build.mk4

@@ -0,0 +1,26 @@
+local mkutils = require 'mkutils'
+
+local function get_parent_dir(file)
+  local handle = io.popen(assert('dirname ' .. file))
+  local dir = handle:read('a')
+  handle:close()
+  return dir:gsub('^%s*(.-)%s*$', '%1')
+end
+
+local dir = get_parent_dir(arg[3])
+local outdir = 'build/tex/' .. dir .. '/' .. settings.input
+os.execute('mkdir -p ' .. outdir)
+
+settings.input = outdir .. '/' .. settings.input
+settings.latex_par = '-output-directory=' .. outdir
+
+Make:match('.css$', 'mv ${filename} ' .. outdir .. '/${filename}')
+Make:match('.png$', 'mv ${filename} ' .. outdir .. '/${filename}')
+Make:match('.tmp$', 'rm ${filename}')
+
+Make:match('tmp$', function(filename)
+  local basename = mkutils.remove_extension(filename)
+  for _, ext in ipairs { 'aux', 'xref', '4ct', '4tc', 'dvi', 'idv', 'lg', 'log', 'tmp' } do
+    os.remove(outdir .. '/' .. basename .. '.' .. ext)
+  end
+end)

lakefile.lean

@@ -56,9 +56,10 @@ USAGE:
 -/
 script «doc-server» (_args) do
   let ((), config) <- StateT.run readConfig {}
-  IO.println s!"Running on `http://localhost:{config.port}`"
+  IO.println s!"Running Lean on `http://localhost:{config.port}/doc`"
+  IO.println s!"Running LaTeX on `http://localhost:{config.port}/tex`"
   _ <- IO.Process.run {
     cmd := "python3",
-    args := #["-m", "http.server", toString config.port, "-d", "build/doc"],
+    args := #["-m", "http.server", toString config.port, "-d", "build"],
   }
   return 0