Skip to content

[Merged by Bors] - feat: port Analysis.NormedSpace.OperatorNorm#3903

Closed
kim-em wants to merge 22 commits intomasterfrom
reenableeta_OperatorNorm
Closed

[Merged by Bors] - feat: port Analysis.NormedSpace.OperatorNorm#3903
kim-em wants to merge 22 commits intomasterfrom
reenableeta_OperatorNorm

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented May 11, 2023 •
edited by Parcly-Taxel
Loading

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.

Open in Gitpod

@kim-em kim-em changed the title feat: port Analysis.NormedSpace.OperatorNorm, with reenableeta feat: port Analysis.NormedSpace.OperatorNorm May 16, 2023
@kim-em kim-em marked this pull request as ready for review May 16, 2023 03:57
@kim-em kim-em added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels May 16, 2023
@kim-em kim-em mentioned this pull request May 16, 2023
Closed
@kim-em kim-em added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels May 16, 2023
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented May 16, 2023

This PR/issue depends on:

@kim-em kim-em added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels May 16, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 16, 2023
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented May 17, 2023

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.

@Parcly-Taxel
Copy link
Copy Markdown
Collaborator

Parcly-Taxel commented May 17, 2023 •
edited
Loading

I'm gonna try…

@Ruben-VandeVelde Ruben-VandeVelde force-pushed the reenableeta_OperatorNorm branch from 29c042b to c6804d4 Compare May 17, 2023 12:08
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

Ruben-VandeVelde commented May 17, 2023

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.

Done.

@Ruben-VandeVelde Ruben-VandeVelde added the mathlib-port This is a port of a theory file from mathlib. label May 17, 2023
@Parcly-Taxel
Clean up
73cf2e0 
and also compress the final steps of `prodMapL`
jcommelin
jcommelin reviewed May 17, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a 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!

Mathlib/Analysis/NormedSpace/OperatorNorm.lean
Comment on lines +471 to +472
-- Porting FIXME: replacing `(algebra : Algebra 𝕜 (E →L[𝕜] E))` with
-- just `algebra` below causes a massive timeout.
Copy link
Copy Markdown
Member

@jcommelin jcommelin May 17, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this still true?

Copy link
Copy Markdown
Collaborator

@Parcly-Taxel Parcly-Taxel May 17, 2023

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.

Copy link
Copy Markdown
Member

@jcommelin jcommelin May 17, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for confirming!

Mathlib/Analysis/NormedSpace/OperatorNorm.lean
Comment on lines +811 to +812
set_option maxHeartbeats 300000 in
set_option synthInstance.maxHeartbeats 25000 in
Copy link
Copy Markdown
Member

@jcommelin jcommelin May 17, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this still needed?

Copy link
Copy Markdown
Collaborator

@Parcly-Taxel Parcly-Taxel May 17, 2023 •
edited
Loading

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_options are needed.

Copy link
Copy Markdown
Member

@jcommelin jcommelin May 17, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for confirming!

@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented May 17, 2023

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 17, 2023
bors bot pushed a commit that referenced this pull request May 17, 2023
@kim-em @Ruben-VandeVelde
@Parcly-Taxel @arienmalec @jcommelin @collares
feat: port Analysis.NormedSpace.OperatorNorm (#3903)
9ab4016 


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>
@bors
Copy link
Copy Markdown

bors bot commented May 17, 2023

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: port Analysis.NormedSpace.OperatorNorm [Merged by Bors] - feat: port Analysis.NormedSpace.OperatorNorm May 17, 2023
@bors bors bot closed this May 17, 2023
@bors bors bot deleted the reenableeta_OperatorNorm branch May 17, 2023 20:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

+1 more reviewer

@Parcly-Taxel Parcly-Taxel Parcly-Taxel left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@kim-em @jcommelin @Parcly-Taxel @Ruben-VandeVelde @arienmalec @collares