Skip to content

[Merged by Bors] - chore: update/remove heart beat bumps#6860

Closed
mattrobball wants to merge 2 commits intomasterfrom
mrb/clean_up_bumps
Closed

[Merged by Bors] - chore: update/remove heart beat bumps#6860
mattrobball wants to merge 2 commits intomasterfrom
mrb/clean_up_bumps

Conversation

@mattrobball
Copy link
Copy Markdown
Contributor

@mattrobball mattrobball commented Aug 30, 2023

We clean up heart beat bumps after #6474.

Open in Gitpod

@mattrobball
Squashed commit of the following:
0420003 
commit ce8dea4
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Aug 29 20:19:34 2023 -0400

    remove comments

commit 1e47611
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Aug 29 20:16:44 2023 -0400

    remove comments

commit 4a33a0e
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Aug 29 20:08:02 2023 -0400

    restore

commit 60486c5
Merge: 51e3570 7df583c
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Aug 29 19:37:47 2023 -0400

    Merge branch 'master' into mrb/universes

commit 51e3570
Merge: c17ce8bae 32de3f6
Author: Eric Wieser <wieser.eric@gmail.com>
Date:   Thu Aug 10 22:01:45 2023 +0000

    Merge branch 'master' into mrb/universes

commit c17ce8b
Merge: 43a7236 c4190b4
Author: Eric Wieser <wieser.eric@gmail.com>
Date:   Thu Aug 10 22:00:24 2023 +0000

    Merge branch 'master' (early part) into mrb/universes

commit 43a7236
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Aug 8 21:00:45 2023 -0400

    remove notes and update author

commit 9c65527
Merge: 29fa063 ffeae88
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Aug 8 20:47:11 2023 -0400

    Merge branch 'master' into mrb/universes

commit 29fa063
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Aug 8 17:04:00 2023 -0400

    restore bumps

commit 6fbf296
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Aug 8 15:14:23 2023 -0400

    comment out bumps again

commit b5ec8c8
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Aug 7 23:23:17 2023 -0400

    lint

commit cde37ba
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Aug 7 23:06:36 2023 -0400

    fix errors

commit 914e9e1
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Aug 7 20:44:37 2023 -0400

    Sort _ -> Sort*

commit 5e7bd9a
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Aug 7 20:42:28 2023 -0400

    move Type* and Sort* and set imports

    now in `Mathlib.Tactic.Basic`

commit 79c6822
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Aug 7 16:01:02 2023 -0400

    revisit all places where Type* fails

commit e02809f
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Aug 6 23:09:29 2023 -0400

    restore necessary bumps

commit c06e819
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Aug 6 20:38:42 2023 -0400

    comment out all bumps

commit 75c10e6
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Aug 6 10:12:59 2023 -0400

    Merge remote-tracking branch 'refs/remotes/origin/mrb/universes' into mrb/universes

commit 3c0e5c2
Merge: 00d53f8 466a8a7
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Aug 6 20:10:23 2023 -0400

    Merge branch 'mrb/universes_2' into mrb/universes

commit 00d53f8
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Aug 6 10:12:59 2023 -0400

    Merge remote-tracking branch 'refs/remotes/origin/mrb/universes' into mrb/universes

commit 466a8a7
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Aug 4 14:36:30 2023 -0400

    lint

commit ced8c9b
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Aug 4 14:29:04 2023 -0400

    long lines

commit 8064173
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Aug 4 14:26:02 2023 -0400

    build

commit 9095a38
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Aug 4 13:41:49 2023 -0400

    fix more

commit b1dfc8c
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Aug 4 12:36:14 2023 -0400

    fix some files

commit 0c9345f
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Aug 4 10:08:12 2023 -0400

    remove

commit 2637c7e
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Aug 4 10:07:33 2023 -0400

    type _ -> type*
@mattrobball mattrobball added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Aug 30, 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 Aug 30, 2023
ericrbg
ericrbg reviewed Aug 30, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@ericrbg ericrbg left a comment

Choose a reason for hiding this comment

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

not sure if all of these comments should be removed, but just in case they were missed:

Mathlib/Analysis/InnerProductSpace/Spectrum.lean Outdated
@@ -139,7 +139,6 @@ theorem orthogonalComplement_iSup_eigenspaces_eq_bot' :
#align linear_map.is_symmetric.orthogonal_supr_eigenspaces_eq_bot' LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot'

-- porting note: a modest increast in the `synthInstance.maxHeartbeats`, but we should still fix it.
Copy link
Copy Markdown
Contributor

@ericrbg ericrbg Aug 30, 2023

Choose a reason for hiding this comment

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

Suggested change
-- porting note: a modest increast in the `synthInstance.maxHeartbeats`, but we should still fix it.

Mathlib/Analysis/Convolution.lean Outdated
@@ -1198,7 +1198,7 @@ variable [IsROrC 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace
(L : E →L[𝕜] E' →L[𝕜] F)

-- porting note: the lemma is slow, added `set_option maxHeartbeats 300000 in`
Copy link
Copy Markdown
Contributor

@ericrbg ericrbg Aug 30, 2023

Choose a reason for hiding this comment

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

Suggested change
-- porting note: the lemma is slow, added `set_option maxHeartbeats 300000 in`
-- porting note: the lemma is slow, added `set_option maxHeartbeats 250000 in`

Mathlib/LinearAlgebra/Matrix/Determinant.lean Outdated
@@ -148,7 +148,6 @@ theorem det_mul_aux {M N : Matrix n n R} {p : n → n} (H : ¬Bijective p) :
#align matrix.det_mul_aux Matrix.det_mul_aux

-- Porting note: need to bump for last simp; new after #3414 (reenableeta)
Copy link
Copy Markdown
Contributor

@ericrbg ericrbg Aug 30, 2023

Choose a reason for hiding this comment

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

Suggested change
-- Porting note: need to bump for last simp; new after #3414 (reenableeta)

@mattrobball
Copy link
Copy Markdown
Contributor Author

mattrobball commented Aug 30, 2023

I should have caught those all with the others I deleted.

jcommelin
jcommelin approved these changes Sep 6, 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 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 6, 2023
bors bot pushed a commit that referenced this pull request Sep 6, 2023
@mattrobball
chore: update/remove heart beat bumps (#6860)
a885e0d 
We clean up heart beat bumps after #6474.
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 6, 2023
@mattrobball
chore: update/remove heart beat bumps (#6860)
c95f05b 
We clean up heart beat bumps after #6474.
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 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 chore: update/remove heart beat bumps [Merged by Bors] - chore: update/remove heart beat bumps Sep 6, 2023
@bors bors bot closed this Sep 6, 2023
@bors bors bot deleted the mrb/clean_up_bumps branch September 6, 2023 13:05
ebab pushed a commit that referenced this pull request Sep 11, 2023
@mattrobball @ebab
chore: update/remove heart beat bumps (#6860)
6eab746 
We clean up heart beat bumps after #6474.
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@mattrobball @kodyvajjha
chore: update/remove heart beat bumps (#6860)
36ce2d4 
We clean up heart beat bumps after #6474.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ericrbg ericrbg ericrbg left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

Labels

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.

3 participants

@mattrobball @jcommelin @ericrbg