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 semorrison
Loading

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

Fixes: #2953

Supersedes PR #1862

@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

@semorrison
Copy link
Collaborator

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.

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

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
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
@semorrison
Copy link
Collaborator

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

@semorrison semorrison 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
8 checks passed
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

@semorrison semorrison Awaiting requested review from semorrison semorrison 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 @semorrison @leodemoura