Use relative links and offload generation to bookshelf-docgen.

finite-set-exercises
Joshua Potter 2023-05-04 11:50:19 -06:00
parent 3cea5a2883
commit 8c7d6d3941
8 changed files with 20 additions and 57 deletions

View File

@ -16,25 +16,15 @@ LaTeX when not.
## Documentation ## Documentation
To generate Lean documentation, we use [doc-gen4](https://github.com/leanprover/doc-gen4). To generate Lean documentation, we use [bookshelf-docgen](https://github.com/jrpotter/bookshelf-docgen).
Run the following to build and serve this: Refer to this project on prerequisites and the run the following to build and
serve files locally:
```bash ```bash
> lake build Bookshelf:docs > lake build Bookshelf:docs
> lake run doc-server > lake run server
``` ```
This assumes you have `python3` available in your `$PATH`. To change how the 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 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.
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
```

View File

@ -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)

View File

@ -14,11 +14,11 @@
"name": "lake", "name": "lake",
"inputRev?": "master"}}, "inputRev?": "master"}},
{"git": {"git":
{"url": "https://github.com/leanprover/doc-gen4", {"url": "https://github.com/jrpotter/bookshelf-docgen.git",
"subDir?": null, "subDir?": null,
"rev": "cf86cb481501e9f03dce5b0cb362b19cdba1824f", "rev": "3facb4b93ec5b9227b013287de8c837912e814ef",
"name": "doc-gen4", "name": "doc-gen4",
"inputRev?": "cf86cb481501e9f03dce5b0cb362b19cdba1824f"}}, "inputRev?": "3facb4b93ec5b9227b013287de8c837912e814ef"}},
{"git": {"git":
{"url": "https://github.com/mhuisi/lean4-cli", {"url": "https://github.com/mhuisi/lean4-cli",
"subDir?": null, "subDir?": null,
@ -52,7 +52,7 @@
{"git": {"git":
{"url": "https://github.com/fgdorais/lean4-unicode-basic", {"url": "https://github.com/fgdorais/lean4-unicode-basic",
"subDir?": null, "subDir?": null,
"rev": "be1f061688faa1dbb224773c54901661253fb4b8", "rev": "ce508dcd1fd49ba15675861aafd864572a0b8252",
"name": "UnicodeBasic", "name": "UnicodeBasic",
"inputRev?": "main"}}, "inputRev?": "main"}},
{"git": {"git":

View File

@ -11,8 +11,8 @@ require std4 from git
"https://github.com/leanprover/std4.git" @ "https://github.com/leanprover/std4.git" @
"6006307d2ceb8743fea7e00ba0036af8654d0347" "6006307d2ceb8743fea7e00ba0036af8654d0347"
require «doc-gen4» from git require «doc-gen4» from git
"https://github.com/leanprover/doc-gen4" @ "https://github.com/jrpotter/bookshelf-docgen.git" @
"cf86cb481501e9f03dce5b0cb362b19cdba1824f" "3facb4b93ec5b9227b013287de8c837912e814ef"
@[default_target] @[default_target]
lean_lib «Bookshelf» { lean_lib «Bookshelf» {
@ -53,14 +53,13 @@ documentation has already been generated prior via
``` ```
USAGE: USAGE:
lake run doc-server lake run server
-/ -/
script «doc-server» (_args) do script server (_args) do
let ((), config) <- StateT.run readConfig {} let ((), config) <- StateT.run readConfig {}
IO.println s!"Running Lean on `http://localhost:{config.port}/doc`" IO.println s!"Running Lean on `http://localhost:{config.port}`"
IO.println s!"Running LaTeX on `http://localhost:{config.port}/tex`"
_ <- IO.Process.run { _ <- IO.Process.run {
cmd := "python3", cmd := "python3",
args := #["-m", "http.server", toString config.port, "-d", "build"], args := #["-m", "http.server", toString config.port, "-d", "build/doc"],
} }
return 0 return 0

View File

@ -2,8 +2,8 @@
\input{preamble} \input{preamble}
\newcommand{\linkA}[1]{\href{/doc/Bookshelf/Real/Sequence/Arithmetic.html\##1}{#1}} \newcommand{\linkA}[1]{\href{../../../../Bookshelf/Real/Sequence/Arithmetic.html\##1}{#1}}
\newcommand{\linkG}[1]{\href{/doc/Bookshelf/Real/Sequence/Geometric.html\##1}{#1}} \newcommand{\linkG}[1]{\href{../../../../Bookshelf/Real/Sequence/Geometric.html\##1}{#1}}
\begin{document} \begin{document}

View File

@ -2,7 +2,7 @@
\input{preamble} \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} \begin{document}

View File

@ -10,7 +10,7 @@
\label{sec:aviary} \label{sec:aviary}
A list of birds as defined in \textit{To Mock a Mockingbird}. 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} \begin{itemize}
\bird{Bald Eagle} $\hat{E}xy_1y_2y_3z_1z_2z_3 = x(y_1y_2y_3)(z_1z_2z_3)$ \bird{Bald Eagle} $\hat{E}xy_1y_2y_3z_1z_2z_3 = x(y_1y_2y_3)(z_1z_2z_3)$

View File

@ -3,7 +3,7 @@
\input{preamble} \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} \begin{document}