8000 chore: add failing grind tests by wkrozowski · Pull Request #8518 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

chore: add failing grind tests #8518

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
Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

chore: add failing grind tests #8518

wants to merge 2 commits into from

Conversation

wkrozowski
Copy link
Contributor
@wkrozowski wkrozowski commented May 28, 2025 •
edited by kim-em
Loading

This PR adds a failing test involving the grind tactic, where induction ... grind works but fun_induction ... grind doesn't.

@wkrozowski wkrozowski added the changelog-language Language features, tactics, and metaprograms label May 28, 2025
@wkrozowski wkrozowski requested a review from leodemoura May 28, 2025 15:48
@wkrozowski wkrozowski marked this pull request as ready for review May 28, 2025 15:49
@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 May 28, 2025
@leanprover-community-bot
Copy link
Collaborator
leanprover-community-bot commented May 28, 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 88078930a92aa55089e936a5fe8e99ec65ab2ceb --onto 3af9ab64ed79a667fb8989f7a0c258b018aba371. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-28 16:20:38)
  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-05-29 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-29 10:21:43)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 020da5bffbd2bd83498a6c9279e20fb97e0773d7 --onto 72141b05fd9a3328c1e5d99211dc4da4495cbd42. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-30 00:31:53)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3fdaf24b49ccc1392c53afe50480a211a285e31f --onto 72141b05fd9a3328c1e5d99211dc4da4495cbd42. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-30 01:20:16)

@kim-em kim-em mentioned this pull request May 29, 2025
Merged
@kim-em kim-em force-pushed the wkrozowski/add_grind_tests branch from d3c40e3 to ef17a89 Compare May 29, 2025 09:31
kim-em
kim-em reviewed May 29, 2025
View reviewed changes
tests/lean/grind/fun_induction_fail.lean
Comment on lines +327 to +333
#guard_msgs in
theorem issue4 : ∀ fuel s c s',
cexec_bounded fuel s c = .some s'
→ cexec s c s' := by
intros
fun_induction cexec_bounded
all_goals grind
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@wkrozowski, could you try to work out how to get to a contradiction from the state grind reached here? I think this example is too big to do much with otherwise.

github-merge-queue bot pushed a commit that referenced this pull request May 29, 2025
@kim-em @wkrozowski
chore: failing grind tests (subset of #8518) (#8526)
22d4c1d 
This is a subset of tests from #8518 that are fully minimized. I'll
merge this first.

---------

Co-authored-by: Wojciech Rozowski <wojciech@lean-fro.org>
@kim-em kim-em force-pushed the wkrozowski/add_grind_tests branch from 4a53d7e to 7317baa Compare May 29, 2025 23:46
@kim-em kim-em mentioned this pull request May 29, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request May 30, 2025
@kim-em
chore: add test case where grind causes a PANIC (#8538)
77e1640 
Minimized from #8518, thanks @wkrozowski!
@kim-em kim-em force-pushed the wkrozowski/add_grind_tests branch from 53144a3 to 6e9adec Compare May 30, 2025 00:53
@kim-em kim-em added the awaiting-author Waiting for PR author to address issues label May 30, 2025
@wkrozowski wkrozowski marked this pull request as draft May 30, 2025 11:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

@leodemoura leodemoura Awaiting requested review from leodemoura

Assignees
No one assigned
Labels
awaiting-author Waiting for PR author to address issues 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
@wkrozowski @leanprover-community-bot @kim-em
0