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] - feat: port Analysis.NormedSpace.OperatorNorm #3903
Conversation
This PR/issue depends on:
|
Can we rewrite the history on this PR, to make it easier to review? I would like to get the diff between mathport output and the HEAD of the PR. |
|
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
29c042b
to
c6804d4
Compare
Done. |
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.
Thanks so much for cleaning up the git history! And for all the valiant work on this monster PR!
-- Porting FIXME: replacing `(algebra : Algebra 𝕜 (E →L[𝕜] E))` with | ||
-- just `algebra` below causes a massive timeout. |
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.
Is this still true?
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.
It's either this or set_option maxHeartbeats 2000000
(2 million). 1 million is not enough.
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.
Thanks for confirming!
set_option maxHeartbeats 300000 in | ||
set_option synthInstance.maxHeartbeats 25000 in |
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.
Is this still needed?
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 can confirm that all heartbeat settings in the file as it stands now are needed; the declaration here suffers from both a defeq timeout and a synth-instance timeout, so both set_option
s are needed.
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.
Thanks for confirming!
Thanks 🎉 bors merge |
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Mauricio Collares <mauricio@collares.org> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
This is the pushout of #3708 and the reenableeta branch #3414, to verify that even though #3708 is taking over 6 hours in CI, it is no problem with reenableeta.