This repository contains a blueprint for formalizing definitions within the L-functions and modular forms database. You can view the rendered version here.

The process for updating the contents of this blueprint is different than most other blueprints, because it is built to improve the integration between Mathlib and the LMFDB. While there is some framing content manually written in content.tex, most of the blueprint is generated from the LMFDB's knowl database using the update script.

Thus most of the work in updating this blueprint takes the following form:

1. Adding definitions and theorems to mathlib

2. Linking definitions in LMFDB knowls to mathlib using the DEFINES macro, and linking theorems using the cite command. Editing and creating knowls requires an account on the LMFDB; contact David Roe or Andrew Sutherland on Zulip (either LMFDB or Lean) if you want to get involved.

3. Once definitions have been added to mathlib and linked in the corresponding knowl, run the update script to update the knowl folder and make a PR to this repository.

1. Ensure that you have a functioning Lean 4 installation. If you do not, please follow the Lean installation guide.

2. To clone this repository to your local machine, please refer to the relevant section of the GitHub documentation here.

3. If you don't have a Python environment, you can install one by following the instructions in the Python installation guide.

4. You will need to install PyGraphViz, following the instructions in the installation guide.

5. If you want to run the update script, you will need to install Networkx using

pip install networkx

and psycopg2 using

pip install psycopg2-binary

1. Install LeanBlueprint by running:

pip install leanblueprint

If you have an existing installation of LeanBlueprint, you can upgrade to the latest version by running:

pip install -U leanblueprint

1. You can use leanblueprint to build the blueprint locally. The available commands are:

• leanblueprint pdf to build the pdf version (this requires a TeX installation of course).
• leanblueprint web to build the web version
• leanblueprint checkdecls to check that every Lean declaration name that appear in the blueprint exist in the project (or in a dependency of the project such as Mathlib). This requires a compiled Lean project, so make sure to run lake build beforehand.
• leanblueprint all to run the previous three commands.
• leanblueprint serve to start a local webserver showing your local blueprint (this sounds silly but web browsers paranoia makes it impossible to simply open the generated html pages without serving them). The url you should use in your browser will be displayed and will probably be https://0.0.0.0:8000/, unless the port 8000 is already in use.

The template repository is organized as follows (listing the main folders and files):

• .github contains GitHub-specific configuration files and workflows.
  • workflows contains GitHub Actions workflow files.
    • build-project.yml defines the workflow for building the Lean project on pushes, pull requests, and manual triggers. This is a minimalistic build workflow which is not necessary if you decide to generate a blueprint (see instructions below) and can be manually disabled by clicking on the Actions tab, selecting Build Project in the left sidebar, then clicking the horizontal triple dots (⋯) on the right, and choosing Disable workflow.
    • create-release.yml: defines the workflow for creating a new Git tag and GitHub release when the lean-toolchain file is updated in the main branch. Ensure the following settings are configured under Settings > Actions > General > Workflow permissions: "Read and write permissions" and "Allow GitHub Actions to create and approve pull requests".
    • update.yml is the dependency update workflow to be triggered manually by default. [It's not documented yet, but it will be soon.]
  • dependabot.yml is the configuration file to automate CI dependency updates.
• .vscode contains Visual Studio Code configuration files
  • extensions.json recommends VS Code extensions for the project.
  • settings.json defines the project-specific settings for VS Code.
• Project should contain the Lean code files.
  • Mathlib should contain .lean files with declarations missing from the current version of Mathlib.
  • Example.lean is a sample Lean file.
• scripts contains scripts to update Mathlib ensuring that the latest version is fetched and integrated into the development environment.
• .gitignore specifies files and folders to be ignored by Git. and environment.
• CODE_OF_CONDUCT.md should contain the code of conduct for the project.
• CONTRIBUTING.md should provide the guidelines for contributing to the project.
• lakefile.toml is the configuration file for the Lake build system used in Lean projects.
• lean-toolchain specifies the Lean version and toolchain used for the project.

For more details about the LeanBlueprint package and its commands, please refer to its documentation.

After pushing changes, please wait for the GitHub Action workflow to finish. You can keep track of the progress in the Actions tab of your repository.