From 6f3ac8a94634913740d121ca42203cb974e35ed4 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 3 May 2023 17:26:45 -0600 Subject: [PATCH] Setup for local navigation between Lean index and LaTeX. --- Bookshelf/Real/Sequence.tex | 31 ++--- .../Enderton/Chapter0.tex | 15 +-- MockMockingbird/Aviary.tex | 8 +- OneVariableCalculus/Apostol/Chapter_I_3.tex | 117 ++++++++---------- README.md | 13 +- build.mk4 | 26 ++++ lakefile.lean | 5 +- 7 files changed, 124 insertions(+), 91 deletions(-) create mode 100644 build.mk4 diff --git a/Bookshelf/Real/Sequence.tex b/Bookshelf/Real/Sequence.tex index 15e2cd7..dc22d73 100644 --- a/Bookshelf/Real/Sequence.tex +++ b/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$. - Then for some $n \in \mathbb{N}$, - $$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$ - -\end{theorem} +Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$. +Then for some $n \in \mathbb{N}$, +$$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$ \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$. - Then for some $n \in \mathbb{N}$, - $$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$ - -\end{theorem} +Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$. +Then for some $n \in \mathbb{N}$, +$$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$ \begin{proof} - \href{Sequence/Geometric.lean}{Bookshelf.Real.Sequence.Geometric.sum_recursive_closed} + \linkG{Real.Geometric.sum\_recursive\_closed} \end{proof} diff --git a/MathematicalIntroductionLogic/Enderton/Chapter0.tex b/MathematicalIntroductionLogic/Enderton/Chapter0.tex index 24fbaf9..b139025 100644 --- a/MathematicalIntroductionLogic/Enderton/Chapter0.tex +++ b/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$. - Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$. - -\end{theorem} +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$. \begin{proof} - \href{Chapter0.lean}{Enderton.Chapter0.lemma_0a} + \link{lemma\_0a} \end{proof} diff --git a/MockMockingbird/Aviary.tex b/MockMockingbird/Aviary.tex index 6caba30..b056501 100644 --- a/MockMockingbird/Aviary.tex +++ b/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)$ diff --git a/OneVariableCalculus/Apostol/Chapter_I_3.tex b/OneVariableCalculus/Apostol/Chapter_I_3.tex index 0892ac0..dffca3d 100644 --- a/OneVariableCalculus/Apostol/Chapter_I_3.tex +++ b/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 - is, there is a real number $L$ such that $L = \inf{S}$. - -\end{xtheorem} +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}$. \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$. - -\end{xtheorem} +For every real $x$ there exists a positive integer $n$ such that $n > x$. \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 - integer $n$ such that $nx > y$. - -\end{xtheorem} +If $x > 0$ and if $y$ is an arbitrary real number, there exists a positive +integer $n$ such that $nx > y$. \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 - $$a \leq x \leq a + \frac{y}{n}$$ - for every integer $n \geq 1$, then $x = a$. - -\end{xtheorem} +If three real numbers $a$, $x$, and $y$ satisfy the inequalities +$$a \leq x \leq a + \frac{y}{n}$$ +for every integer $n \geq 1$, then $x = a$. \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. - \begin{enumerate}[(a)] - \item If $S$ has a supremum, then for some $x$ in $S$ we have - $$x > \sup{S} - h.$$ - \item If $S$ has an infimum, then for some $x$ in $S$ we have - $$x < \inf{S} + h.$$ - \end{enumerate} - -\end{xtheorem} +Let $h$ be a given positive number and let $S$ be a set of real numbers. +\begin{enumerate}[(a)] + \item If $S$ has a supremum, then for some $x$ in $S$ we have + $$x > \sup{S} - h.$$ + \item If $S$ has an infimum, then for some $x$ in $S$ we have + $$x < \inf{S} + h.$$ +\end{enumerate} \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 \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.inf_imp_exists_lt_inf_add_delta} + \item \link{Real.sup\_imp\_exists\_gt\_sup\_sub\_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 - $$C = \{a + b : a \in A, b \in B\}.$$ +Given nonempty subsets $A$ and $B$ of $\mathbb{R}$, let $C$ denote the set +$$C = \{a + b : a \in A, b \in B\}.$$ - \begin{enumerate}[(a)] - \item If each of $A$ and $B$ has a supremum, then $C$ has a supremum, and - $$\sup{C} = \sup{A} + \sup{B}.$$ - \item If each of $A$ and $B$ has an infimum, then $C$ has an infimum, and - $$\inf{C} = \inf{A} + \inf{B}.$$ - \end{enumerate} - -\end{xtheorem} +\begin{enumerate}[(a)] + \item If each of $A$ and $B$ has a supremum, then $C$ has a supremum, and + $$\sup{C} = \sup{A} + \sup{B}.$$ + \item If each of $A$ and $B$ has an infimum, then $C$ has an infimum, and + $$\inf{C} = \inf{A} + \inf{B}.$$ +\end{enumerate} \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 \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.inf_minkowski_sum_eq_inf_add_inf} + \item \link{Real.sup\_minkowski\_sum\_eq\_sup\_add\_sup} + \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 - $$s \leq 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 - $$\sup{S} \leq \inf{T}.$$ - -\end{xtheorem} +Given two nonempty subsets $S$ and $T$ of $\mathbb{R}$ such that +$$s \leq 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 +$$\sup{S} \leq \inf{T}.$$ \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} diff --git a/README.md b/README.md index 90ac946..4b59f05 100644 --- a/README.md +++ b/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 {} +``` diff --git a/build.mk4 b/build.mk4 new file mode 100644 index 0000000..97d0ba7 --- /dev/null +++ b/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) diff --git a/lakefile.lean b/lakefile.lean index 727f406..c29a406 100644 --- a/lakefile.lean +++ b/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