max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: refine mdbook docs

Browse source
This commit is contained in:
Sebastian Ullrich 2022-09-19 13:08:57 +02:00 • committed by Leonardo de Moura
parent 800938065a
commit 3ef1baae4a
1 changed files with 11 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
doc/dev/mdbook.md
View file

@ -1,7 +1,7 @@
# Documentation
The Lean `doc` folder contains the [Lean Manual](https://leanprover.github.io/lean4/doc/) and is
authored in a combination of markdown (*.md) files and literate Lean files. The .lean files are
authored in a combination of markdown (`*.md`) files and literate Lean files. The .lean files are
preprocessed using a tool called [LeanInk](https://github.com/leanprover/leanink) and
[Alectryon](https://github.com/Kha/alectryon) which produces a generated markdown file. We then run
`mdbook` on the result to generate the html pages.
@ -53,25 +53,28 @@ Then run the following:
cargo install --git https://github.com/leanprover/mdBook mdbook
```
1. Clone https://github.com/leanprover/LeanInk.git and run `lake build` then copy the resulting
executable to your `$HOME/.elan/bin` folder or `%USERPROFILE%\.elan\bin` so Alectryon can find it
there.
1. Clone https://github.com/leanprover/LeanInk.git and run `lake build` then make the resulting
binary available to Alectryon using e.g.
```bash
# make `leanInk` available in the current shell
export PATH=$PWD/build/bin:$PATH
```
1. Create a Python 3.10 environment.
1. Install the following packages:
1. Install Alectryon:
```
python3 -m pip install git+https://github.com/Kha/alectryon.git@typeid
```
1. Now you are ready to process the *.lean files using Alectryon as follows:
1. Now you are ready to process the `*.lean` files using Alectryon as follows:
```
cd lean4/doc
alectryon --frontend lean4+markup examples\palindromes.lean --backend webpage -o palindromes.lean.md
alectryon --frontend lean4+markup examples/palindromes.lean --backend webpage -o palindromes.lean.md
```
And repeat this for the other .lean files you care about or write a script to process them all.
Repeat this for the other .lean files you care about or write a script to process them all.
1. Now you can build the book using:
```