LeanBlueprintExample

Warning

This example project is very outdated, please check out the latest https://github.com/PatrickMassot/leanblueprint instead.

Install elan
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 to lakefile.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 from LeanBlueprintExample to YourProject/YourProject/Basic.lean
Copy everything in blueprint, .github from LeanBlueprintExample 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 at https://<your-github-username>.github.io/YourProject/blueprint and your doc at https://<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 of one, two and the theorem of one_plus_one_eq_two in the demo.

utensil/LeanBlueprintExample

LeanBlueprintExample