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
359 Commits
1 Branch
0 Tags
861 KiB
Lean 57.2%
CSS 27.2%
JavaScript 15.1%
Shell 0.5%
 
 
 
 
Go to file
Calvin Lee 76a137dabc fix colors if media set to dark 
This commit fixes a few edge-cases. First, if you `prefers-color-scheme`
is dark, your background will no longer be dark in light mode.
Furthermore, switching from dark to system theme now works. It did not
before, as we queried our iframe for color-scheme instead of the parent
window (our iframe inherited the color-scheme from the parent document).
Finally, the navbar iframe has its color-scheme set separately, which
caused issues in a few cases.
 		2023-06-09 23:39:59 +02:00
.github/workflows chore: cleanup CI after partial migration to mathlib4 2023-04-22 01:01:19 +02:00
DocGen4 hide color-changer if javascript is disabled 2023-06-09 23:39:59 +02:00
static fix colors if media set to dark 2023-06-09 23:39:59 +02: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 feat: show versions in index HTML 2023-03-09 21:46:38 +01:00
README.md Improve installation instructions 2023-05-26 12:07:57 +02:00
lake-manifest.json chore: update toolchain 2023-06-04 02:48:14 +02:00
lakefile.lean add colorscheme toggle 2023-06-09 23:39:59 +02:00
lean-toolchain chore: update toolchain 2023-06-04 02:48:14 +02:00
test_docs.sh feat: don't copy .git folders in test 2023-05-24 01:17:51 +02: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 update your dependencies:

lake -Kenv=dev update

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.

Note that if you modify the .js or .css files in doc-gen4, they won't necessarily be copied over when you rebuild the documentation. You can manually copy the changes to the build/docs directory to make sure the changes appear, or just do a full recompilation (lake clean and lake build inside the doc-gen4 directory.)