LeanBlueprintExample
[!WARNING]
This example project is very outdated, please check out the latest https://github.com/PatrickMassot/leanblueprint instead.
-
Create your project on command line using something like (replace all "YourProject" to your project name in all the following commands)
lake +leanprover-community/mathlib4:lean-toolchain new YourProject math
which ensures that your project uses the same Lean version as mathlib and will be able to use mathlib as a dependency.
- Add
doc-gen4
dependency tolakefile.lean
following doc-gen4 Usage:
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"
- Change the current directory to
YourProject
then run the following on command line:
lake update
lake exe cache get
lake build
-
Copy the dummy file
LeanBlueprintExample/Basic.lean
fromLeanBlueprintExample
toYourProject/YourProject/Basic.lean
-
Copy everything in
blueprint
,.github
fromLeanBlueprintExample
to your project and change every "LeanBlueprintExample" to "YourProject", also make adjustments to suit your project. -
Run the following to test locally:
# Installs doc-gen4
lake -Kenv=dev update
# Builds docs to build/doc
lake -Kenv=dev build YourProject:docs
# Builds blueprint website to blueprint/web
inv all
-
Push to GitHub and enable GitHub Pages following Publishing with a custom GitHub Actions workflow.
-
CI will run around 10 minutes at
https://github.com/<your-github-username>/YourProject/actions
, when it turns green, check out your blueprint athttps://<your-github-username>.github.io/YourProject/blueprint
and your doc athttps://<your-github-username>.github.io/YourProject/doc
, then definitions and theorems in the blueprint should be able to jump to the corresponding doc pages, for example, the definitions ofone
,two
and the theorem ofone_plus_one_eq_two
in the demo.