scaffold-lean-library

Scaffold Lean Library

Generate a Lean 4 library repository with Lake, Mathlib or PFR dependencies, compile-time API regression tests, local Makefile targets, GitHub Actions CI, text linting, and agent instructions.

Workflow

1. Gather Project Information

If the user provided values in the request, use them and do not ask again. Derive safe defaults from context only when they are unambiguous.

Ask for any missing values:

• Project name: kebab-case repository and Lake package name, for example entropy-inequalities.
• Short description: one sentence for README, marketplace-style summaries, and agent instructions.
• Top-level Lean namespace: UpperCamelCase, for example EntropyInequalities. Derive from the project name when the result is readable; ask if acronyms or domain terms make the derivation ambiguous.
• Lean toolchain version: the exact lean-toolchain content, for example leanprover/lean4:v4.25.0.
• Dependency family: Mathlib or PFR.
• Dependency git ref: a Mathlib tag/ref or a PFR git ref.
• Paper-backed mode: whether to add references/ stubs and Pandoc-academic lint ignores for formalizations tied to papers or transcriptions.
• GitHub username: for repository URLs.
• Copyright holder: for LICENSE and source headers.

Detect the GitHub username and full name when possible:

gh api user -q .login

git config user.name

If either command fails or returns an empty value, ask the user.

2. Resolve Dependency Ref

For Mathlib projects:

1. If the user supplied a dependency ref, use it.

2. Otherwise, if the Lean toolchain is exactly leanprover/lean4:vX.Y.Z or vX.Y.Z, derive the Mathlib ref vX.Y.Z.

3. Verify the derived ref exists before using it:

   git ls-remote --tags https://github.com/leanprover-community/mathlib4.git refs/tags/vX.Y.Z
   

4. If the tag does not exist, or if the Lean toolchain is nightly, a branch, or otherwise not a clean stable version, ask the user for the Mathlib ref.