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.
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
[Merged by Bors] - fix(*): add missing classical
tactics and decidable
arguments
#18277
Conversation
Thanks 🎉 If CI passes, please remove the label bors d+ |
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
…nto eric-wieser/classical-leakage-fixes
…nto eric-wieser/classical-leakage-fixes
…nto eric-wieser/classical-leakage-fixes
…nto eric-wieser/classical-leakage-fixes
…nto eric-wieser/classical-leakage-fixes
bors merge |
…8277) As discussed in [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60classical.60.20attribute.20leakage/near/282726128), the `classical` tactic is buggy in Mathlib3, and "leaks" into subsequent declarations. This doesn't port well, as the bug is fixed in lean 4. This PR installs a temporary hack to contain these leaks, fixes (some of) the correponding breakages, then reverts the hack. The result is that the new `classical` tactics in the diff are not needed in Lean 3, but will be needed in Lean 4. In a future PR, I will try committing the hack itself; but in the meantime, these files are very close to (if not beyond) the port, so the sooner they are fixed the better.
…nto eric-wieser/classical-leakage-fixes
Canceled. |
bors merge (that last commit only adds two files which I'm optimistic about) |
…8277) As discussed in [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60classical.60.20attribute.20leakage/near/282726128), the `classical` tactic is buggy in Mathlib3, and "leaks" into subsequent declarations. This doesn't port well, as the bug is fixed in lean 4. This PR installs a temporary hack to contain these leaks, fixes all of the correponding breakages, then reverts the hack. The result is that the new `classical` tactics in the diff are not needed in Lean 3, but will be needed in Lean 4. In a future PR, I will try committing the hack itself; but in the meantime, these files are very close to (if not beyond) the port, so the sooner they are fixed the better.
Pull request successfully merged into master. Build succeeded: |
classical
tactics and decidable
argumentsclassical
tactics and decidable
arguments
This forward-ports: * leanprover-community/mathlib#18277. No action is needed as the proof was already fixed during porting. * leanprover-community/mathlib#18337. This was forward-ported in #1970 but the SHA was not updated. See the diff here: * [`data.fintype.basic`@`9003f28797c0664a49e4179487267c494477d853`..`d78597269638367c3863d40d45108f52207e03cf`](https://leanprover-community.github.io/mathlib-port-status/file/data/fintype/basic?range=9003f28797c0664a49e4179487267c494477d853..d78597269638367c3863d40d45108f52207e03cf)
This forward-ports: * leanprover-community/mathlib#18277. No action is needed as the proof was already fixed during porting. * leanprover-community/mathlib#18337. This was forward-ported in #1970 but the SHA was not updated. See the diff here: * [`data.fintype.basic`@`9003f28797c0664a49e4179487267c494477d853`..`d78597269638367c3863d40d45108f52207e03cf`](https://leanprover-community.github.io/mathlib-port-status/file/data/fintype/basic?range=9003f28797c0664a49e4179487267c494477d853..d78597269638367c3863d40d45108f52207e03cf)
leanprover-community/mathlib#18277 backported a bug about classical which is already fixed in mathlib4, so these diffs simpy need a SHA update. (Comment: This might not be the full PR #18277 yet, as I worked on a file-by-file base)
As discussed in this Zulip thread, the
classical
tactic is buggy in Mathlib3, and "leaks" into subsequent declarations.This doesn't port well, as the bug is fixed in lean 4.
This PR installs a temporary hack to contain these leaks, fixes all of the correponding breakages, then reverts the hack.
The result is that the new
classical
tactics in the diff are not needed in Lean 3, but will be needed in Lean 4.In a future PR, I will try committing the hack itself; but in the meantime, these files are very close to (if not beyond) the port, so the sooner they are fixed the better.