leanprover-community/hopscotch

Identify upstream breaking commits (bisect) and/or open a bump PR to keep a Lean 4 downstream pinned to the latest passing revision. Works with any GitHub-hosted Lean dependency — not tied to mathlib4.

View on GitHub

Trust Signals

Scorecard Score: not yet scored
Maintenance Recency: Activelast commit May 25, 2026
License: Apache 2.0

Pinned Snippet

workflow.ymlSHA-pinned

uses: leanprover-community/hopscotch-action@89d470a8815bffe8452bca70ae32a942e9229d7d # v1.0.0

tags can be moved; commit SHAs can't. why a SHA?

Inputs

name	description	required	default
dependency	The lakefile require name, e.g. "mathlib" or "batteries".	yes	—
from	Exclusive lower bound for the bisect range. Defaults to the current rev in lake-manifest.json for the named dependency.	no	""
to	Inclusive upper bound. Defaults to the upstream default-branch HEAD (resolved automatically by hopscotch when omitted).	no	""
project-dir	Path to the Lean project root. Defaults to the repository root.	no	.
extra-args	Additional arguments passed verbatim to `hopscotch dep`. Accepts single- or multi-line input; each line is word-split on whitespace, so you can group related flags across lines: extra-args: \| --scan-mode linear --allow-dirty-workspace	no	""
hopscotch-version	hopscotch release tag (e.g. "v1.4.0") or "latest" to resolve the newest release automatically. Pinning to a specific version is recommended for reproducibility.	no	v1.4.0
max-window-size	Abort if the commit range contains more than this many commits. Guards against runaway runs on ancient pins. Raise or remove if you intentionally need a large window.	no	3000
pin-to	Which commit the manifest should end up pinned to when an incompatibility is found. One of: last-good (default) — bump PR advances the manifest to the last passing commit (single force-pushed branch). The tracking issue surfaces the FKB. first-bad — fix PR pins the manifest to the first-known-bad commit on a per-FKB-SHA branch so maintainers can `gh pr checkout` and reproduce the break. No tracking issue is opened in this mode. Two invocations (one per mode) on the same workflow give you both a bump PR and a fix PR; running only one mode is fine.	no	last-good
open-pr	Open or update a PR when the manifest pin changes.	no	true
pr-branch	Branch name for the PR. In `pin-to: last-good` mode, this is the literal force-pushed branch (default `hopscotch/bump`). In `pin-to: first-bad` mode, this is a prefix and the actual branch is `<prefix>-<fkb-short7>` so fix PRs at different FKB SHAs don't collide (default `hopscotch/fix`).	no	""
pr-base	Base branch for the PR. Defaults to the repository default branch.	no	""
pr-labels	Comma-separated list of labels to apply to the PR.	no	""
reviewers	Comma-separated list of GitHub usernames or team slugs to request review from on the PR (passed to `gh pr create --reviewer`).	no	""
open-issue	Open a GitHub issue when a culprit is found; update it on subsequent failures; close it automatically when the downstream recovers. Ignored (forced false) in `pin-to: first-bad` mode — the fix PR itself carries the FKB context.	no	true
issue-labels	Comma-separated list of labels to apply to the tracking issue.	no	""
github-token	GitHub token for API calls and gh CLI operations (PR, issue, release resolution). Defaults to the job token.	no	${{ github.token }}
pr-token	Token used to push the PR branch. Defaults to `github-token`. The default `GITHUB_TOKEN` does NOT trigger downstream workflow runs on the PR it creates — so if you want CI to run on the bump / fix PR, pass a GitHub App installation token here.	no	""
git-user-name	git user.name for the bump / fix commit.	no	github-actions[bot]
git-user-email	git user.email for the bump / fix commit.	no	41898282+github-actions[bot]@users.noreply.github.com

Outputs

name	description
outcome	"passed" \| "incompatible" \| "skipped" \| "tool-error"
culprit-commit	SHA of the first failing upstream commit (non-empty when outcome=incompatible).
last-good-commit	SHA of the last passing upstream commit.
target-commit	SHA that the --to ref resolved to.
previous-pin	The dependency rev in lake-manifest.json before this run.
new-pin	The dependency rev in lake-manifest.json after this run.
pr-number	PR number (empty when no PR was opened).
pr-url	PR URL (empty when no PR was opened).
pr-action	"created", "updated", "up-to-date", or "none".
issue-number	Tracking issue number (empty when not opened).
issue-url	Tracking issue URL (empty when not opened).
summary-md	Markdown summary from .lake/hopscotch/summary.md.