-
Notifications
You must be signed in to change notification settings - Fork 234
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] - chore(AlgebraicGeometry/Gluing): fix soon-to-be-broken proof #11838
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't like it much, but it's no worse than before.
maintainer merge
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
bors merge I adjusted the title to make clear that the proof is not yet broken |
This proof had two `change`s added during porting, and these produce a massive timeout after the changes in leanprover/lean4#3807. This PR replace the `change` with the appropriate `erw`, and is now fast before and after the change. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This proof had two `change`s added during porting, and these produce a massive timeout after the changes in leanprover/lean4#3807. This PR replace the `change` with the appropriate `erw`, and is now fast before and after the change. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This proof had two `change`s added during porting, and these produce a massive timeout after the changes in leanprover/lean4#3807. This PR replace the `change` with the appropriate `erw`, and is now fast before and after the change. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This proof had two `change`s added during porting, and these produce a massive timeout after the changes in leanprover/lean4#3807. This PR replace the `change` with the appropriate `erw`, and is now fast before and after the change. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This proof had two `change`s added during porting, and these produce a massive timeout after the changes in leanprover/lean4#3807. This PR replace the `change` with the appropriate `erw`, and is now fast before and after the change. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This proof had two
change
s added during porting, and these produce a massive timeout after the changes in leanprover/lean4#3807.This PR replace the
change
with the appropriateerw
, and is now fast before and after the change.