r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity
Document generator for my Bookshelf project
323 Commits
1 Branch
0 Tags
861 KiB
Lean 57.2%
CSS 27.2%
JavaScript 15.1%
Shell 0.5%
 
 
 
 
Go to file
Jeremy Salwen 1575eeedd2 Add definition doc string to search result page. 
Adds a two-column table to the search results so you can see the doc string next to
the result.  The doc string is not parsed/converted to markdown yet, but that could
be done later.
 		2023-01-28 23:00:53 +01:00
.github/workflows chore: QoL updates for deploy_docs.sh 2023-01-05 00:02:41 +01:00
DocGen4 Add a search page to the docs. 2023-01-28 23:00:53 +01:00
static Add definition doc string to search result page. 2023-01-28 23:00:53 +01:00
.gitignore chore: update toolchain 2022-12-02 17:55:27 +01:00
DocGen4.lean chore: update toolchain and dependencies 2022-08-09 23:30:43 +02:00
LICENSE Initial commit 2021-11-10 17:41:28 -08:00
Main.lean style: refactor process to Lean 4 compiler style 2023-01-01 19:30:28 +01:00
README.md Add section to README about development of doc-gen4 2023-01-25 18:32:45 +01:00
deploy_docs.sh chore: QoL updates for deploy_docs.sh 2023-01-05 00:02:41 +01:00
lake-manifest.json chore: update toolchain 2022-12-23 18:20:56 +01:00
lakefile.lean Add a search page to the docs. 2023-01-28 23:00:53 +01:00
lean-toolchain feat: use mathlib4 build cache 2023-01-04 23:25:35 +01:00

README.md

doc-gen4

Document Generator for Lean 4

Usage

doc-gen4 is the easiest to use via its custom Lake facet, in order to do this you have to add it to your lakefile.lean like this:

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

Then you can generate documentation for an entire library using:

lake -Kenv=dev build Test:docs

If you have multiple libraries you want to generate documentation for the recommended way right now is to run it for each library.

Development of doc-gen4

You can build docs using a modified doc-gen4 as follows: Replace the from git "..." @ "main" in the lakefile.lean with just from "..." using the path to the modified version of doc-gen4. E.g. if the path to the modified version of doc-gen4 is ../doc-gen4, it would be:

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from "../doc-gen4"

The root of the built docs will be build/docs/index.html. However, due to the "Same Origin Policy", the generated website will be partially broken if you just open the generated html files in your browser. You need to serve them from a proper http server for it to work. An easy way to do that is to run python3 -m http.server from the build/docs directory.