LeanMgr Cache Manager

Use LeanMgr as a local project-fleet tool for Lean 4 cache lifecycle work.

Rules

• Treat .lake as disposable, recoverable cache.
• Do not modify Lean source files unless the user explicitly asks.
• Do not rewrite Git history.
• Run dry-runs before destructive cleanup.
• Prefer leanmgr doctor, leanmgr size, and leanmgr clean --dry-run before deletion.
• Prefer leanmgr gc --dry-run for fleet-wide reclamation; it skips unrecoverable caches (no lake-manifest.json, no lakefile.toml/ lakefile.lean, or empty lean-toolchain) unless --include-unrecoverable is given.
• With a size budget, pair --target with --unused-days (for example leanmgr gc --target 20GiB --unused-days 14 --dry-run); --target alone takes the largest caches first even if the user is working in them.
• leanmgr doctor also reports shared caches (Mathlib downloads, elan toolchains) and toolchains elan toolchain gc considers unused. Suggest elan toolchain gc --delete or lake exe cache clean! only as commands for the user to run; LeanMgr never deletes shared caches itself.
• Use leanmgr restore to call lake exe cache get after cache deletion. It only runs for Mathlib and projects that depend on it; other projects and missing paths are skipped with a reason (they rebuild with lake build). Preview with leanmgr restore ... --dry-run.
• Use leanmgr gitignore to ensure .lake/ is ignored before recommending cleanup.
• A project selector must name an indexed project; clean, restore, size, remove, and gitignore <project> error out on an unknown selector rather than no-op.
• When leanmgr list shows missing in the STATUS column, suggest leanmgr remove --missing --dry-run first. It only edits the index, but a project on an unmounted drive also looks missing, so let the user confirm.

Workflow

1. Inspect indexed projects (and find unindexed ones elan knows about):

leanmgr list
leanmgr size --all
leanmgr doctor
leanmgr scan --from-elan

2. Check project hygiene:

leanmgr gitignore --all --dry-run
leanmgr toolchain check
leanmgr worktree doctor
leanmgr worktree prune --dry-run

leanmgr worktree doctor and worktree prune operate across every indexed project, so they surface and clear stale worktrees fleet-wide, not just in the current directory. Projects sharing one repository are audited once; missing paths and directories outside Git are listed as skipped, not as failures. Without --force, worktree prune shows Git's dry run and asks before pruning.

3. Plan cleanup before deleting:

leanmgr clean --tag archived --level hard --dry-run
leanmgr clean <project> --level soft --dry-run
leanmgr gc --unused-days 90 --dry-run
leanmgr gc --target 20GiB --dry-run

4. Execute only after the user accepts the plan or explicitly requests execution:

leanmgr clean --tag archived --level hard

5. Restore cache when returning to a project:

leanmgr restore --tag active --dry-run
leanmgr restore <project>
leanmgr restore --tag active

6. Keep the index tidy after projects are moved or deleted:

leanmgr remove --missing --dry-run

AI Context

Use AI-oriented context output before making recommendations:

leanmgr ai context --format codex
leanmgr ai context --format claude
leanmgr ai context --format json

Prefer --format json for programmatic pipelines and --format codex or --format claude for coding-agent prompts.

Skill Installation

leanmgr ai skill show --format <codex|claude> adapts this SKILL.md body to the receiving agent's task contract header. The codex flag ensures the body opens with # Codex Task Contract; claude opens with # Claude Code Task Context. If the body already starts with the matching header it is passed through; a different leading heading is replaced; a missing leading heading is prepended.

Boundaries

LeanMgr complements official tools:

• Lake owns build, dependency, and artifact cache behavior.
• Elan owns Lean toolchain installation and selection.
• Git owns repositories and worktrees.
• LeanMgr owns cross-project indexing, reporting, dry-run cleanup planning, and safe orchestration.

Do not propose shared local mathlib or symlinked .lake/packages/mathlib as a default fix. That belongs in an explicit experimental workflow because it can break reproducibility across projects pinned to different Lean or mathlib versions.