Skip to content

feat: add cbv.maxSteps option to control step limit#12788

Merged
wkrozowski merged 3 commits intoleanprover:masterfrom
wkrozowski:feat/cbv-max-steps
Mar 4, 2026
Merged

feat: add cbv.maxSteps option to control step limit#12788
wkrozowski merged 3 commits intoleanprover:masterfrom
wkrozowski:feat/cbv-max-steps

Conversation

@wkrozowski
Copy link
Copy Markdown
Contributor

This PR adds a set_option cbv.maxSteps N option that controls the maximum
number of simplification steps the cbv tactic performs. Previously the limit
was hardcoded to the Sym.Simp.Config default of 100,000 with no way for
users to override it. The option is threaded through cbvCore, cbvEntry,
cbvGoal, and cbvDecideGoal.

🤖 Generated with Claude Code

This PR adds a `set_option cbv.maxSteps N` option that controls the maximum
number of simplification steps the `cbv` tactic performs. Previously the limit
was hardcoded to the `Sym.Simp.Config` default of 100,000 with no way for
users to override it. The option is threaded through `cbvCore`, `cbvEntry`,
`cbvGoal`, and `cbvDecideGoal`.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@wkrozowski wkrozowski requested a review from leodemoura as a code owner March 4, 2026 12:42
@wkrozowski wkrozowski added the changelog-tactics User facing tactics label Mar 4, 2026
@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 Mar 4, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 4, 2026

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-04 13:37:39)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 551086c85480eb69b85b7a59de8e75208c74984a --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-04 16:08:30)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 4, 2026

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-04 13:37:41)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 551086c85480eb69b85b7a59de8e75208c74984a --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-04 16:08:32)

@wkrozowski wkrozowski added this pull request to the merge queue Mar 4, 2026
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Mar 4, 2026
@wkrozowski wkrozowski added this pull request to the merge queue Mar 4, 2026
Merged via the queue into leanprover:master with commit 2f3d0ee Mar 4, 2026
17 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-tactics User facing tactics 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.

2 participants