Skip to content

fix: nondeterminism in grind ring#9867

Merged
leodemoura merged 1 commit intomasterfrom
grind_ring_nondet
Aug 12, 2025
Merged

fix: nondeterminism in grind ring#9867
leodemoura merged 1 commit intomasterfrom
grind_ring_nondet

Conversation

@leodemoura
Copy link
Copy Markdown
Member

@leodemoura leodemoura commented Aug 12, 2025

This PR fixes a nondeterministic behavior in grind ring.

Closes #9825

@leodemoura
fix: nondeterminism in grind ring
446f0f2 
This PR fixes a nondeterministic behavior in `grind ring`.

Closes #9825
@leodemoura leodemoura added the changelog-language Language features and metaprograms label Aug 12, 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 Aug 12, 2025
@ghost
Copy link
Copy Markdown

ghost commented Aug 12, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bf348ae60f5bace12f79576c9e0bb03b538f261b --onto e0fcaf5e7ddab2fcab51be8c403446d84a8a0d45. You can force Mathlib CI using the force-mathlib-ci label. (2025-08-12 05:56:54)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 12, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bf348ae60f5bace12f79576c9e0bb03b538f261b --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-08-12 05:56:55)

@leodemoura leodemoura added this pull request to the merge queue Aug 12, 2025
Merged via the queue into master with commit 54dce21 Aug 12, 2025
22 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

changelog-language Language features 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.

grind is generating nondeterministic proofs

2 participants

@leodemoura @leanprover-bot