Skip to content

feat: improve set_option error messages #9496

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 2 commits into from
Jul 26, 2025
Merged

feat: improve set_option error messages #9496

merged 2 commits into from
Jul 26, 2025

Conversation

jrr6
Copy link
Contributor

@jrr6 jrr6 commented Jul 23, 2025

This PR improves the error messages produced by the set_option command.

@jrr6 jrr6 added the changelog-language Language features, tactics, and metaprograms label Jul 23, 2025
@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 Jul 24, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jul 24, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e134cfea8fa42a6007bef76ecdff136d905150e3 --onto cdab726e3d289b80860ae9f5a7de21d990c8b95f. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-24 00:32:38)
  • ✅ Mathlib branch lean-pr-testing-9496 has successfully built against this PR. (2025-07-24 02:20:13) View Log

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jul 24, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e134cfea8fa42a6007bef76ecdff136d905150e3 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-24 00:32:40)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-07-18 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. (2025-07-24 01:32:00)

@jrr6 jrr6 force-pushed the set-option-errors branch from ac6cb52 to d819d1a Compare July 24, 2025 00:38
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 24, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#9496
d78496b
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 24, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#9496
3e8cc9c
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jul 24, 2025
@jrr6 jrr6 added this pull request to the merge queue Jul 26, 2025
Merged via the queue into leanprover:master with commit 30afb0d Jul 26, 2025
23 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@jrr6 @leanprover-community-bot @leanprover-bot