Contributing

Work on a branch and open a pull request with the code, relevant checks, and documentation. The repository's contribution guide describes module placement and licensing.

For questions or help choosing a first contribution, join the community discussion on Lean Zulip or WeChat.

Check a library change

lake exe cache get
lake build LeanMFG mfglib_check mfglib
lake env lean scripts/Audit.lean
lake exe mfglib_check

The verification guide also lists the downstream-installation and release-metadata checks. State whether a change is supported by a general theorem, a numerical comparison, or an executable example.

Work on the documentation

Use the Node version in .node-version. From the repository root:

cd docs
npm ci
npm run dev

Open http://localhost:3000. Pages are MDX files under docs/app/. Navigation labels live in docs/lib/navigation.ts.

npm run build

The build checks TypeScript, MDX, repository links, and exported internal links. It also generates the search index and records the source commit. Set NEXT_PUBLIC_BASE_PATH=/LeanMFG to check the GitHub Pages path.

MDX components

Component	Use
`LeanSnippet`	Display a Lean source file, or an excerpt selected by unique markers.
`Declaration`	Display a source-backed signature with parameters, results, and a source link.
`Tabs`	Present alternative instructions, such as repository and package installation.
`SourceLink` / `RepositoryLink`	Link to a file at the documentation's source commit.

Markdown code fences receive copy buttons. Section headings receive stable anchors and populate the page contents. Use native details and summary elements for supplementary assumptions or derivations; keep information needed to use an interface in the main text.

Write each page around a reader's task. An API entry should explain its inputs, return value, errors, and an example. Place proposed work in issues; document available interfaces and their current limitations here.

The documentation example is checked with:

lake env lean --run docs/examples/Solve.lean

Release changes

Record user-visible changes in the changelog. The release procedure covers candidate checks, tags, documentation artifacts, and publication.