Skip to content
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

fix: omit fvars from simp_all? theorem list #2969

Merged
merged 1 commit into from
Dec 12, 2023
Merged

fix: omit fvars from simp_all? theorem list #2969

merged 1 commit into from
Dec 12, 2023

Conversation

JLimperg
Copy link
Contributor

@JLimperg JLimperg commented Nov 27, 2023 •
edited by kim-em
Loading

Removes local hypotheses from the simp theorem list generated by simp_all?.

Fixes: #2953

Supersedes PR #1862

@JLimperg JLimperg requested a review from kim-em as a code owner November 27, 2023 21:14
@JLimperg
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Nov 27, 2023
@JLimperg JLimperg mentioned this pull request Nov 27, 2023
Closed
@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 27, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Nov 27, 2023 •
edited
Loading

  • ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-27 22:04:23)
  • ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-28' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-28 10:20:44)
  • ✅ Mathlib branch lean-pr-testing-2969 has successfully built against this PR. (2023-11-29 02:41:18) View Log
  • 🟡 Mathlib branch lean-pr-testing-2969 build this PR didn't complete normally. (2023-12-12 01:06:36) View Log

@kim-em
Copy link
Collaborator

kim-em commented Nov 28, 2023

Perhaps for the future, if usedSimps has no local hypotheses, we could suggest replacing simp_all with simp. But perhaps there aare strange corner cases where this is not correct.

@kim-em kim-em added awaiting-author Waiting for PR author to address issues will-merge-soon …unless someone speaks up labels Nov 28, 2023
@kim-em
Copy link
Collaborator

kim-em commented Nov 28, 2023

Could you please rebase onto origin/nightly (alternatively origin/nightly-with-mathlib), so we can get a Mathlib CI run, just to be sure?

@JLimperg JLimperg force-pushed the trace-simp_all-omit-hyps branch from a533dfb to 3c37ddf Compare November 28, 2023 09:34
@JLimperg
Copy link
Contributor Author

Looks green on nightly as well. :)

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-review Waiting for someone to review the PR awaiting-author Waiting for PR author to address issues labels Nov 28, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 29, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2969
bc8fa54
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Nov 29, 2023
@leodemoura leodemoura removed the awaiting-review Waiting for someone to review the PR label Dec 1, 2023
@kim-em kim-em force-pushed the trace-simp_all-omit-hyps branch from 8c5dfe7 to 4669a51 Compare December 11, 2023 23:52
@kim-em
Copy link
Collaborator

kim-em commented Dec 11, 2023

Rebasing this onto nightly, so our updated CI is happy.

@kim-em kim-em enabled auto-merge December 11, 2023 23:53
@kim-em kim-em added this pull request to the merge queue Dec 12, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 12, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2969
09ebcc3
Merged via the queue into leanprover:master with commit e2f9571 Dec 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@leodemoura leodemoura leodemoura approved these changes

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

simp_all? suggests wrong/misleading simp_all only [...]
4 participants
@JLimperg @leanprover-community-mathlib4-bot @kim-em @leodemoura