/diagnose

name: diagnose
description: Diagnostics, cleanup, and migration help
user_invocable: true

Lean4 Diagnostics

Diagnostics, troubleshooting, and migration assistance for the Lean4 plugin.

Usage

/lean4:diagnose                    # Full diagnostic (plugin + workspace)
/lean4:diagnose env                # Environment only
/lean4:diagnose migrate            # Detect legacy installs (read-only)
/lean4:diagnose migrate --global   # Include user-level ~/.claude scan
/lean4:diagnose cleanup            # Show stale files + removal commands
/lean4:diagnose cleanup --apply    # Actually remove stale files
/lean4:diagnose <pasted error>     # Error triage: match against known patterns

Inputs

| Arg | Required | Description | |-----|----------|-------------| | mode | No | `env`, `migrate`, `cleanup`, or full (default) | | --global | No | Include user-level paths (~/); migrate only | | --apply | No | Execute removals; cleanup only | | error text | No | Positional text whose first token is not a recognized mode is treated as pasted diagnostic text for error triage |

**Dispatch** is decided by the **first positional token** only:

• a recognized mode (`env`, `migrate`, `cleanup`) or no positional token → existing mode behavior (default full diagnostic when absent);
• otherwise → treat the positional text as pasted diagnostic input for error triage.

Mode-specific flags (`--global`, `--apply`) remain flags in every case — they are never treated as error text.

**Error triage precedence:** pasted text is matched against the specific patterns in [compilation-errors.md](../skills/lean4/references/compilation-errors.md) (Quick Reference Table first), including the module-system patterns below, **before** falling back to the generic `Build fails → lake update && lake clean && lake build` row. A specific match wins over the generic remediation.

Actions

1. Environment Check

| Tool | Check | Required | |------|-------|----------| | `lean` | `lean --version` | Yes | | `lake` | `lake --version` | Yes | | `python3` | `python3 --version` | For scripts | | `git` | `git --version` | For commits | | `rg` | `rg --version` | Optional (faster search) |

Persistent-environment hosts use `LEAN4_PLUGIN_ROOT`, `LEAN4_SCRIPTS`, `LEAN4_REFS`, and `LEAN4_PYTHON_BIN`. Trusted native Codex installs instead receive absolute SessionStart paths; those values are not shell exports.

Run the shared preflight **without depending on PATH**, which may be absent.

**Native Codex plugin:** use the literal absolute SessionStart `preflight` value:

/absolute/plugin/root/bin/lean4-skills-preflight --codex

If trusted context is missing, report this canonical recovery block:

1. Review and trust the lean4 plugin hooks in /hooks.
2. Start a new Codex task (re-runs the SessionStart hook).
3. Run the absolute <plugin-root>/bin/lean4-skills-preflight --codex command; if it is missing, reinstall the plugin.

**Persistent environment (including Claude Code):**

if command -v lean4-skills-preflight >/dev/null 2>&1; then
    lean4-skills-preflight
elif [[ -n "${LEAN4_PLUGIN_ROOT:-}" && -x "$LEAN4_PLUGIN_ROOT/bin/lean4-skills-preflight" ]]; then
    "$LEAN4_PLUGIN_ROOT/bin/lean4-skills-preflight"
else
    echo "Lean4 bootstrap environment is not fully set up in this Claude Code session." >&2
    echo "  Recovery:" >&2
    echo "    1. Run /lean4:diagnose env for a full diagnosis." >&2
    echo "    2. Restart the Claude Code session (re-runs the SessionStart bootstrap hook)." >&2
    echo "    3. If it persists, check the plugin hook/bootstrap state (hooks.json, bootstrap.sh)." >&2
fi

The persistent preflight checks `LEAN4_*`, PATH, and wrappers. Codex checks the installed tree and absolute wrappers. Each has a canonical recovery block.

1b. MCP Tools

| Check | Detection | Status | |-------|-----------|--------| | Lean LSP MCP | `lean_goal` tool available in this session | Optional (sub-second feedback) | `✓ … available` or `⚠ … unavailable — see INSTALLATION.md`

2. Plugin Check

Verify structure and permissions:

plugins/lean4/
├── .claude-plugin/plugin.json
├── .codex-plugin/plugin.json
├── commands/     (*.md command files)
├── hooks/        (Claude + Codex hook configs; executable hooks)
├── skills/lean4/ (SKILL.md + references/)
├── agents/       (4 files)
├── bin/          (lean4-skills-* wrappers; absolute under Codex, on PATH under Claude)
└── lib/scripts/  (executable .py / .sh internals)

3. Project Check

• `lakefile.lean` and `lean-toolchain` present
• `lake build` passes
• Sorry count reported

4. Migration Detection (read-only)

Detects legacy v3 artifacts without making changes.

**Legacy plugin installs:**

~/.claude/plugins/lean4-theorem-proving/
~/.claude/plugins/lean4-subagents/
~/.claude/plugins/lean4-memories/

**Stale environment variables:**

• `LEAN4_PLUGIN_ROOT` pointing to old path (e.g., `lean4-theorem-proving`)
• `LEAN4_SCRIPTS` not under current plugin
• `LEAN4_REFS` not under current plugin

**Name mapping (v3 → v4):**

| V3 | V4 | |----|-----| | `lean4-theorem-proving` | `lean4` | | `lean4-memories` | Removed | | `lean4-subagents` | Integrated | | `/lean4-theorem-proving:*` | `/lean4:*` |

**With `--global`:** Also scans user-level `~/.claude/` for duplicates or stale plugin versions. Only when explicitly requested.

5. Cleanup

Detects and optionally removes obsolete artifacts.

**Workspace paths checked:**

.claude/tools/lean4/
.claude/docs/lean4/
.claude/lean4-*/           # Any lean4-* directories

**User-level paths (with --global):**

~/.claude/plugins/lean4-theorem-proving/
~/.claude/plugins/lean4-subagents/
~/.claude/plugins/lean4-memories/

**Behavior:**

• Default: Report findings, show `rm -rf` commands, do NOT execute
• With `--apply`: Interactive per-item confirmation

**Interactive prompt (`--apply`):**

Found 3 items to clean:
  [1] .claude/tools/lean4/
  [2] .claude/docs/lean4/
  [3]