From 8c7d6d394112c7dafce3d5987175f85522a9f33a Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 4 May 2023 11:50:19 -0600 Subject: [PATCH] Use relative links and offload generation to bookshelf-docgen. --- README.md | 20 ++++---------- build.mk4 | 26 ------------------- lake-manifest.json | 8 +++--- lakefile.lean | 13 +++++----- src/Bookshelf/Real/Sequence.tex | 4 +-- .../Enderton/Chapter0.tex | 2 +- src/MockMockingbird/Aviary.tex | 2 +- .../Apostol/Chapter_I_3.tex | 2 +- 8 files changed, 20 insertions(+), 57 deletions(-) delete mode 100644 build.mk4 diff --git a/README.md b/README.md index b1116ee..82ee060 100644 --- a/README.md +++ b/README.md @@ -16,25 +16,15 @@ LaTeX when not. ## Documentation -To generate Lean documentation, we use [doc-gen4](https://github.com/leanprover/doc-gen4). -Run the following to build and serve this: +To generate Lean documentation, we use [bookshelf-docgen](https://github.com/jrpotter/bookshelf-docgen). +Refer to this project on prerequisites and the run the following to build and +serve files locally: ```bash > lake build Bookshelf:docs -> lake run doc-server +> lake run server ``` 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. 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 -n 1 make4ht -e build.mk4 -``` +project. diff --git a/build.mk4 b/build.mk4 deleted file mode 100644 index 8a688c9..0000000 --- a/build.mk4 +++ /dev/null @@ -1,26 +0,0 @@ -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]):sub(#"./src/") -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/lake-manifest.json b/lake-manifest.json index 043e52f..580bec3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -14,11 +14,11 @@ "name": "lake", "inputRev?": "master"}}, {"git": - {"url": "https://github.com/leanprover/doc-gen4", + {"url": "https://github.com/jrpotter/bookshelf-docgen.git", "subDir?": null, - "rev": "cf86cb481501e9f03dce5b0cb362b19cdba1824f", + "rev": "3facb4b93ec5b9227b013287de8c837912e814ef", "name": "doc-gen4", - "inputRev?": "cf86cb481501e9f03dce5b0cb362b19cdba1824f"}}, + "inputRev?": "3facb4b93ec5b9227b013287de8c837912e814ef"}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli", "subDir?": null, @@ -52,7 +52,7 @@ {"git": {"url": "https://github.com/fgdorais/lean4-unicode-basic", "subDir?": null, - "rev": "be1f061688faa1dbb224773c54901661253fb4b8", + "rev": "ce508dcd1fd49ba15675861aafd864572a0b8252", "name": "UnicodeBasic", "inputRev?": "main"}}, {"git": diff --git a/lakefile.lean b/lakefile.lean index 26a5182..b69cc27 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -11,8 +11,8 @@ require std4 from git "https://github.com/leanprover/std4.git" @ "6006307d2ceb8743fea7e00ba0036af8654d0347" require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ - "cf86cb481501e9f03dce5b0cb362b19cdba1824f" + "https://github.com/jrpotter/bookshelf-docgen.git" @ + "3facb4b93ec5b9227b013287de8c837912e814ef" @[default_target] lean_lib «Bookshelf» { @@ -53,14 +53,13 @@ documentation has already been generated prior via ``` USAGE: - lake run doc-server + lake run server -/ -script «doc-server» (_args) do +script server (_args) do let ((), config) <- StateT.run readConfig {} - IO.println s!"Running Lean on `http://localhost:{config.port}/doc`" - IO.println s!"Running LaTeX on `http://localhost:{config.port}/tex`" + IO.println s!"Running Lean on `http://localhost:{config.port}`" _ <- IO.Process.run { cmd := "python3", - args := #["-m", "http.server", toString config.port, "-d", "build"], + args := #["-m", "http.server", toString config.port, "-d", "build/doc"], } return 0 diff --git a/src/Bookshelf/Real/Sequence.tex b/src/Bookshelf/Real/Sequence.tex index dc22d73..ee233ce 100644 --- a/src/Bookshelf/Real/Sequence.tex +++ b/src/Bookshelf/Real/Sequence.tex @@ -2,8 +2,8 @@ \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}} +\newcommand{\linkA}[1]{\href{../../../../Bookshelf/Real/Sequence/Arithmetic.html\##1}{#1}} +\newcommand{\linkG}[1]{\href{../../../../Bookshelf/Real/Sequence/Geometric.html\##1}{#1}} \begin{document} diff --git a/src/MathematicalIntroductionLogic/Enderton/Chapter0.tex b/src/MathematicalIntroductionLogic/Enderton/Chapter0.tex index b139025..be231c6 100644 --- a/src/MathematicalIntroductionLogic/Enderton/Chapter0.tex +++ b/src/MathematicalIntroductionLogic/Enderton/Chapter0.tex @@ -2,7 +2,7 @@ \input{preamble} -\newcommand{\link}[1]{\href{/doc/MathematicalIntroductionLogic/Enderton/Chapter0.html\##1}{#1}} +\newcommand{\link}[1]{\href{/../../../MathematicalIntroductionLogic/Enderton/Chapter0.html\##1}{#1}} \begin{document} diff --git a/src/MockMockingbird/Aviary.tex b/src/MockMockingbird/Aviary.tex index b056501..fa9d65d 100644 --- a/src/MockMockingbird/Aviary.tex +++ b/src/MockMockingbird/Aviary.tex @@ -10,7 +10,7 @@ \label{sec:aviary} A list of birds as defined in \textit{To Mock a Mockingbird}. -Refer to \href{/doc/MockMockingbird/Aviary.html}{MockMockingbird/Aviary} for implementation examples. +Refer to \href{../../../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/src/OneVariableCalculus/Apostol/Chapter_I_3.tex b/src/OneVariableCalculus/Apostol/Chapter_I_3.tex index dffca3d..95ae44b 100644 --- a/src/OneVariableCalculus/Apostol/Chapter_I_3.tex +++ b/src/OneVariableCalculus/Apostol/Chapter_I_3.tex @@ -3,7 +3,7 @@ \input{preamble} -\newcommand{\link}[1]{\href{/doc/OneVariableCalculus/Apostol/Chapter_I_3.html\##1}{#1}} +\newcommand{\link}[1]{\href{/../../../../OneVariableCalculus/Apostol/Chapter_I_3.html\##1}{#1}} \begin{document}