/bug-report
Draft a bug report issue for lean4-skills
> /plugin marketplace add cameronfreer/lean4-skillsHow it fires
How this command gets triggered: by you, by Claude, or both.
- Fires itselfClaude auto-loads it when your prompt matches the work.
- You can call itInvoke it directly when you want it.
- Slash command
/bug-report
Context preview
What this command does when you run it.
Draft a bug report issue for lean4-skills
Command definition
bug-report.mdname: bug-report
description: Draft a bug report issue for lean4-skills
Bug Report
Draft and submit a bug report as a GitHub issue on `cameronfreer/lean4-skills`.
Precondition
Invoke this command only if the user explicitly ran it or explicitly agreed to draft a bug report. If invoked without prior opt-in, ask:
> This looks like a lean4-skills bug. Want me to draft a bug report?
If the user explicitly ran `/lean4-contribute:bug-report`, treat that as opt-in. Do not proceed unless the user confirms. Do not mine git diff, gather diagnostics, or ask structured questions until consent is given.
Gathering Context
Collect the following from the user and the current session. Ask for anything you cannot infer:
1. **Summary** — One-line description of the bug 2. **Expected behavior** — What should happen 3. **Actual behavior** — What happens instead 4. **Repro steps** — Numbered steps to reproduce 5. **Minimal Lean snippet** — Smallest code that triggers the bug (strip project-specific details) 6. **Environment / toolchain** — Lean version (`lean --version`), lake version, OS, plugin version, relevant MCP servers 7. **Diagnostics / build output** — Compiler errors, lake build output, or LSP messages (redact paths and usernames) 8. **Possible fix** (optional) — If you have a local fix, write a short **prose summary** of what the fix does (1–3 sentences). Do **not** include a raw diff by default. If the user explicitly asks to include a patch excerpt, include only the minimal relevant hunk (not the whole diff), strip file paths and surrounding context, and require a separate confirmation: > This draft includes a code patch. Review it for unrelated code or secrets. > **Include this patch?** (yes / remove it / edit) 9. **Privacy / redaction check** — Before showing the draft, scan for filesystem paths, usernames, API keys, or other sensitive data and redact them. Flag anything you redacted so the user can verify.
Drafting the Issue
Compose the issue using this template:
Title: [Bug] <summary>
Labels: bug
## Summary
<summary>
## Expected Behavior
<expected behavior>
## Actual Behavior
<actual behavior>
## Steps to Reproduce
<numbered repro steps>
## Minimal Example
```lean
<minimal Lean snippet>
Environment
- Lean: <version>
- Lake: <version>
- OS: <os>
- Plugin: <version>
- MCP: <servers if relevant>
Diagnostics
<build output / compiler errors>
Possible Fix
<prose summary of fix; minimal patch excerpt only if user confirmed>
--- *Drafted via [lean4-contribute](https://github.com/cameronfreer/lean4-skills)*
## Showing the Draft
Display the **complete** issue draft to the user — title, labels, and full body.
Ask:
> Here is the bug report I will submit. Review it carefully — it may contain
> code snippets from your project.
>
> By submitting, you agree that this content may be edited, rearranged, or
> incorporated into lean4-skills in any form under its
> [MIT license](https://github.com/cameronfreer/lean4-skills/blob/main/LICENSE).
>
> **Submit this issue?** (yes / edit / cancel)
Do **not** proceed unless the user explicitly confirms.
## Submitting
After confirmation, submit using the first available method:
1. **`gh` CLI** — Try: `gh issue create --repo cameronfreer/lean4-skills --title "<title>" --body "<body>" --label bug`.
If the label fails (e.g. `bug` doesn't exist on the repo), retry without
`--label` and note that the label was advisory only.
If `gh` fails for auth or network reasons, **stop** — do not retry. Fall
through to the browser or email path immediately.
2. **Browser fallback** — Provide a prefilled GitHub URL:
`https://github.com/cameronfreer/lean4-skills/issues/new?title=<url-encoded-title>&body=<url-encoded-body>&labels=bug`
(the `labels=` param is best-effort; GitHub ignores unknown labels silently)
3. **Email fallback** — Draft an email to `lean4skills@gmail.com` with subject
`[Bug] <summary>` and the full issue body, for the user to send manually.
Report the result (issue URL, fallback URL, or email draft) and confirm
completion.
Read more
name: bug-report description: Draft a bug report issue for lean4-skills
Bug Report
Draft and submit a bug report as a GitHub issue on `cameronfreer/lean4-skills`.
Precondition
Invoke this command only if the user explicitly ran it or explicitly agreed to draft a bug report. If invoked without prior opt-in, ask:
> This looks like a lean4-skills bug. Want me to draft a bug report?
If the user explicitly ran `/lean4-contribute:bug-report`, treat that as opt-in. Do not proceed unless the user confirms. Do not mine git diff, gather diagnostics, or ask structured questions until consent is given.
Gathering Context
Collect the following from the user and the current session. Ask for anything you cannot infer:
1. **Summary** — One-line description of the bug 2. **Expected behavior** — What should happen 3. **Actual behavior** — What happens instead 4. **Repro steps** — Numbered steps to reproduce 5. **Minimal Lean snippet** — Smallest code that triggers the bug (strip project-specific details) 6. **Environment / toolchain** — Lean version (`lean --version`), lake version, OS, plugin version, relevant MCP servers 7. **Diagnostics / build output** — Compiler errors, lake build output, or LSP messages (redact paths and usernames) 8. **Possible fix** (optional) — If you have a local fix, write a short **prose summary** of what the fix does (1–3 sentences). Do **not** include a raw diff by default. If the user explicitly asks to include a patch excerpt, include only the minimal relevant hunk (not the whole diff), strip file paths and surrounding context, and require a separate confirmation: > This draft includes a code patch. Review it for unrelated code or secrets. > **Include this patch?** (yes / remove it / edit) 9. **Privacy / redaction check** — Before showing the draft, scan for filesystem paths, usernames, API keys, or other sensitive data and redact them. Flag anything you redacted so the user can verify.
Drafting the Issue
Compose the issue using this template:
Title: [Bug] <summary> Labels: bug ## Summary <summary> ## Expected Behavior <expected behavior> ## Actual Behavior <actual behavior> ## Steps to Reproduce <numbered repro steps> ## Minimal Example ```lean <minimal Lean snippet>
Environment
- Lean: <version>
- Lake: <version>
- OS: <os>
- Plugin: <version>
- MCP: <servers if relevant>
Diagnostics
<build output / compiler errors>
Possible Fix
<prose summary of fix; minimal patch excerpt only if user confirmed>
--- *Drafted via [lean4-contribute](https://github.com/cameronfreer/lean4-skills)*
## Showing the Draft Display the **complete** issue draft to the user — title, labels, and full body. Ask: > Here is the bug report I will submit. Review it carefully — it may contain > code snippets from your project. > > By submitting, you agree that this content may be edited, rearranged, or > incorporated into lean4-skills in any form under its > [MIT license](https://github.com/cameronfreer/lean4-skills/blob/main/LICENSE). > > **Submit this issue?** (yes / edit / cancel) Do **not** proceed unless the user explicitly confirms. ## Submitting After confirmation, submit using the first available method: 1. **`gh` CLI** — Try: `gh issue create --repo cameronfreer/lean4-skills --title "<title>" --body "<body>" --label bug`. If the label fails (e.g. `bug` doesn't exist on the repo), retry without `--label` and note that the label was advisory only. If `gh` fails for auth or network reasons, **stop** — do not retry. Fall through to the browser or email path immediately. 2. **Browser fallback** — Provide a prefilled GitHub URL: `https://github.com/cameronfreer/lean4-skills/issues/new?title=<url-encoded-title>&body=<url-encoded-body>&labels=bug` (the `labels=` param is best-effort; GitHub ignores unknown labels silently) 3. **Email fallback** — Draft an email to `lean4skills@gmail.com` with subject `[Bug] <summary>` and the full issue body, for the user to send manually. Report the result (issue URL, fallback URL, or email draft) and confirm completion.
Lean 4 workflow pack for AI coding agents. Gives your agent a structured prove/review/golf loop, mathlib search, axiom checking, and safety guardrails.
Other commands on lean4-skills.
- /feature-request
Draft a feature request issue for lean4-skills
Open command - /share-insight
Draft a shareable insight from your session as a GitHub issue
Open command - /autoformalize
Autonomous end-to-end formalization from informal sources
Open command - /autoprove
Autonomous multi-cycle theorem proving with explicit stop budgets
Open command - /checkpoint
Save progress with a safe commit checkpoint
Open command - /diagnose
Diagnostics, cleanup, and migration help
Open command