fawadha1der/churnbot
Bump a Lean dependency (mathlib by default), auto-repair the fallout using only compiler-evidenced fixes, and open a reviewable pull request with a full report. Never inserts `sorry`; never claims success unless `lake build` is green.
View on GitHubTrust Signals
- Scorecard Score
- not yet scored
- Maintenance Recency
- Stale
- License
- None
Inputs
| name | description | required | default |
|---|---|---|---|
| dependency | Lake dependency to bump | — | mathlib |
| mode | Fixer set: conservative (deprecations only), standard (adds simp-list maintenance and simp?-driven re-squeezing), or aggressive (also recovers deleted term proofs via exact? library search — opt in deliberately). | — | standard |
| engine | Suggestion engine for the re-squeeze/recovery fixers: auto (REPL when acquirable, else one-shot elaboration), repl, or oneshot. | — | auto |
| cache-command | Command to fetch build caches after the bump. "auto" means `lake exe cache get` when the dependency is mathlib, nothing otherwise; "none" disables caching entirely. | — | auto |
| pr-branch | Branch to push repairs to | — | churnbot/dependency-bump |
| base-branch | PR base branch (defaults to the repository default branch) | — | "" |
| labels | Comma-separated labels for the PR | — | churnbot |
| token | GitHub token used to push and open the PR | — | ${{ github.token }} |
| install-elan | Install elan (set to 'false' if your workflow already did) | — | true |
| dry-run | Report only; do not push or open a PR | — | false |
Outputs
| name | description |
|---|---|
| green | 'true' if the build was green after repair |
| report-path | Path to the generated markdown report |