No results found

LeanBlueprintExample

LeanBlueprintExample

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

  1. Install elan

  2. 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.

  1. 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"
  1. Change the current directory to YourProject then run the following on command line:
lake update
lake exe cache get
lake build

  1. Copy the dummy file LeanBlueprintExample/Basic.lean from LeanBlueprintExample to YourProject/YourProject/Basic.lean

  2. Copy everything in blueprint, .github from LeanBlueprintExample to your project and change every "LeanBlueprintExample" to "YourProject", also make adjustments to suit your project.

  3. 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

  1. Push to GitHub and enable GitHub Pages following Publishing with a custom GitHub Actions workflow.

  2. 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.