Skip to content

fix: finish reports the thresholds of its own configuration - #16340

Closed
sgraf812 wants to merge 1 commit into
leanprover:masterfrom
sgraf812:sg/grind-finish-threshold-config
Closed

sgraf812 wants to merge 1 commit into
leanprover:masterfrom
sgraf812:sg/grind-finish-threshold-config

Conversation

@sgraf812

@sgraf812 sgraf812 commented Nov 7, 2026

Copy link
Copy Markdown
Member

This PR makes the failure message of grind's finish name the thresholds of its own configuration items. For example, grind => finish (instances := 5) now reports that it reached (instances := 5), where it used to report the default thresholds.

🤖 Generated with Claude Code

`mkResult` records the configuration of the `GrindM` context, which
`finish`, `finish?` and `set_config` set from their configuration items,
in place of the configuration of `Params`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QPKmiUooPkkAEYh2giBqfH
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 7, 2026
@sgraf812 sgraf812 closed this Nov 7, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant