Development and releases

LeanMFG releases tie the library, dependency versions, verification evidence, and documentation to one source commit.

Development workflow

Development branch → PR checks → main → candidate checks → annotated tag → release.

Each change updates the implementation, relevant checks, documentation, and changelog. Follow the contribution guide for module placement and proof conventions.

What CI checks

The CI gate depends on the applicable checks. Documentation-only PRs build the library and site and run the documented Lean example. Changes to library code, dependencies, scripts, or tests run the full suite above, as do pushes to main and release runs. The scope table and local commands distinguish general theorems from finite numerical tests. Solver convergence and general numerical equilibrium certification are outside the current guarantee.

One-time repository settings

After the workflows are merged, a repository administrator must:

1. Require pull requests and the CI gate status check for main. Require the branch to be current before merging; prevent direct pushes and bypasses according to the project's maintainer policy.
2. Restrict creation of v* tags to release maintainers; prevent updates and deletion of published tags.
3. Set GitHub Pages' source to GitHub Actions. If github-pages restricts deployment refs, permit main.

These are GitHub settings, not guarantees imposed by the files in this repository. A new checkout or fork must configure them separately.

Version policy

LeanMFG versions independently of Lean: the library version identifies its features and interfaces, while the Lean version identifies the required toolchain. Multiple LeanMFG releases may use the same Lean version.

Each published release specifies one tested combination of Lean, mathlib, and FloatLib. The README compatibility table records these combinations. The pinned files and source.json release attachment provide the complete dependency revisions.

• The package version in lakefile.toml, docs/package.json, and the root entries in docs/package-lock.json must agree: MAJOR.MINOR.PATCH.
• During 0.x, increment MINOR for substantial new features, breaking APIs, or incompatible Lean/mathlib/FloatLib changes. PATCH is for compatible fixes. Document theorem hypothesis changes and numerical behavior changes even when names are unchanged.
• Pin the Lean release, direct dependency commits, and complete Lake/npm locks. Toolchain compatibility is part of the release contract; do not promise arbitrary combinations of Lean dependencies.
• Track stable Lean releases. Before publishing support for a new toolchain, migrate the dependency set and pass the full candidate checks, including numerical verification and fresh downstream installation. A newer Lean release alone does not establish compatibility.
• Include both versions in the GitHub Release title, for example LeanMFG v0.1.0 — Lean 4.34.0. The release workflow derives the Lean version from the verified source.json artifact; the Git tag remains v0.1.0.
• Add user-visible changes under CHANGELOG.md's Unreleased heading. Do not label unreleased work as a published version. Never move a published tag.

Prepare a candidate

1. Make the version changes in a PR. Move the intended Unreleased entries to ## [X.Y.Z] - YYYY-MM-DD, retaining an Unreleased heading. Include added capabilities, fixes, API changes, migration requirements, and known limitations.
2. Update the verification scope, install instructions, and relevant MDX pages, and add the intended release's tested dependency set to the README compatibility table. Run the required checks and merge only after CI gate succeeds.
3. From main, run the Release workflow manually with candidate tag vX.Y.Z. Manual runs only validate and upload artifacts; they do not create tags, Releases, or Pages deployments.
4. Record the candidate run's exact commit. Confirm both jobs and the gate passed. Download verification-<SHA> and documentation-<SHA> if needed. source.json identifies the code, dependencies, and fixture/document hashes; the other files contain audit, numerical, and downstream-client logs.

The candidate gate requires a clean checkout whose commit is on origin/main, matching versions, and a dated changelog entry. Unreleased local work deliberately does not satisfy it.

Publish the verified commit

From a clean maintainer checkout, use the exact candidate commit, not a moving branch tip:

git fetch origin main --tags
git tag -a vX.Y.Z CANDIDATE_SHA -m "LeanMFG vX.Y.Z"
git push origin vX.Y.Z

The tag workflow reruns the same CI workflow at the tagged commit. It also requires an annotated tag matching the package version and checkout. After success it:

• Creates a GitHub Release with the changelog section and verification evidence.
• Attaches leanmfg-docs-vX.Y.Z.tar.gz, built from that same commit.
• Records the release commit in the archived documentation's footer, build-info.json, and Lean source links.

Publish the documentation site

The official site tracks main. The Documentation site workflow builds and checks the MDX site after each push to main, then deploys the static output to GitHub Pages. It can also be rerun manually from main.

The live site identifies its source commit and labels untagged builds as development documentation. Publishing the site does not create a library release. Tagged documentation remains available in each GitHub Release's archive.

Failures and corrections

A failed gate blocks publication. Fix code through a PR and run a new candidate. If an existing tag is wrong, do not force-update it: use a new version. For a Pages configuration failure, fix the repository setting and rerun the failed Documentation site job. Rerun failed Release jobs rather than attempting to recreate an already published Release.

The workflows are based on Lean Action, reusable GitHub workflows, and GitHub Pages deployment. Top-level action references are pinned to commits and should be reviewed when updated.

Read a version's documentation

The page footer identifies the package version, commit, and whether a local build contains uncommitted changes. Repository source links point to that commit. build-info.json records the same identity for automated checks.

The hosted site presents the latest deployed main commit. Versioned documentation archives remain attached to their GitHub Releases.

Native binary distributions and bit-for-bit reproducible builds are not provided yet.

To install that exact library version, follow Getting started and pin its source commit and toolchain.