leanblueprint

The leanblueprint command line tool automates the creation of a blueprint for a Lean project.

Prerequisites:

1. A Lean project created using lake.
2. A Git repository with at least one commit.
3. A configured GitHub remote.
4. GitHub Pages configured to use GitHub Actions as the source (found in Repository Settings > Pages).

Steps:

1. Navigate to your project folder.
2. Run leanblueprint new.
3. Answer the configuration questions (you can press Enter to accept defaults). Note that you must explicitly answer y/n for the confirmation to create the blueprint and the proposal to commit to your git repository.

Once created, pushing to GitHub will trigger GitHub Actions to build and deploy your blueprint to:

• Web version: https://<user_name>.github.io/<repo_name>/blueprint/
• PDF version: https://<user_name>.github.io/<repo_name>/blueprint.pdf
• API documentation: https://<user_name>.github.io/<repo_name>/docs/

The blueprint package automatically calculates the formalization status of nodes in your dependency graph based on the commands used in your LaTeX source. This status affects the colors and styles of the nodes in the generated graph.

Status Logic

• leanok: When \leanok is used, the node is considered 'stated'.
• mathlibok: When \mathlibok is used, the node is marked as being in Mathlib.
• notready: When \notready is used, the node is marked as needing more work.
• can_state: A node is ready to be formalized if all its prerequisites are marked as leanok and it is not marked as notready.
• can_prove: A node is ready for a proof if all its prerequisites are leanok and it has a valid proof structure.
• fully_proved: A node and all its ancestors are considered fully formalized if they are all marked as proved or are definitions.

Visual Indicators

The package uses specific colors for these states (which can be customized via \graphcolor):

• Mathlib: Dark green border.
• Stated: Green border.
• Can State: Blue border.
• Not Ready: Orange border.
• Proved: Green border or background.
• Can Prove: Blue background.
• Fully Proved: Dark green background.

While most configuration is handled during blueprint creation via the leanblueprint client, you can customize specific metadata and dependency graph styling by editing the LaTeX preamble in the web version of LaTeX. If you are using the default layout, this is located in the web.tex file.

Project Metadata

Use these macros to define links for the project's web presence:

• \home{url}: The URL of the project's home page.
• \github{url}: The URL of the project's Git repository.
• \dochome{url}: The URL of the project's doc-gen API documentation.

Dependency Graph Styling

You can customize the colors and legend descriptions for the dependency graph using the \graphcolor macro. This allows you to change how specific node types are visually represented and how they appear in the legend.

% Example of configuring project links
\home{https://example.com}
\github{https://github.com/user/repo}
\dochome{https://docs.example.com}

% Example of customizing a graph color
% Syntax: \graphcolor{node_type}{color}{description}
\graphcolor{not_ready}{red}{Critical}

Run the new command from within your Lean project directory to initialize a blueprint. The command will guide you through an interactive setup to configure:

• General Information: Project title, Lean library name, author, GitHub repository URL, project website, and API documentation URL.
• LaTeX Settings: Document class, paper size, and PDF generation options.
• Web Settings: HTML version options like table of contents depth and file splitting.
• CI/CD: Option to create a GitHub Actions workflow for continuous compilation.
• Home Page: Option to create a Jekyll-based home page.

Requirements & Side Effects:

• The repository must be a valid Git repository and must not have uncommitted changes.
• It will automatically detect lakefile.lean or lakefile.toml.
• It may modify your lakefile to add requirements for checkdecls and doc-gen4.
• It will attempt to commit the new blueprint/ folder, lakefile, and lake-manifest.json to your Git repository.

leanblueprint new

To link your LaTeX content to your Lean 4 code, use the following macros within your TeX files:

Example usage:

\begin{theorem}[Smale 1958]
  \label{thm:sphere_eversion}
  \lean{sphere_eversion}
  \leanok
  \uses{def:immersion}
  There is a homotopy of immersions of $𝕊^2$ into $ℝ^3$ from the inclusion map to
  the antipodal map $a : q ↦ -q$.
\end{theorem}
  
\begin{proof}
  \leanok
  \uses{thm:open_ample, lem:open_ample_immersion}
  This obviously follows from what we did so far.
\end{proof}