-
Notifications
You must be signed in to change notification settings - Fork 331
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: adapt to multiple goal linter 1 #12338
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.
You didn't mark this ready for review yet. I still decided to leave a few comments; hope they helpful.
To my eye, most of these look like clear improvements that should be uncontroversial. I commented on other that might require more thought or where follow-up golfing is possible.
@@ -355,7 +355,7 @@ def gluedCover : Scheme.GlueData.{u} where | |||
This is an isomorphism, as witnessed by an `IsIso` instance. -/ | |||
def fromGlued : 𝒰.gluedCover.glued ⟶ X := by | |||
fapply Multicoequalizer.desc | |||
exact fun x => 𝒰.map x | |||
· exact fun x => 𝒰.map x |
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.
Can you move this into the fapply
? If possible, I'd find this even nicer.
exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.2⟩ | ||
repeat' erw [WithBot.coe_eq_coe] | ||
exact add_eq_zero_iff' (zero_le _) (zero_le _) | ||
repeat (· exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩) |
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'm on the fence if the any_goals
=> repeat
change is better.
rw [List.eq_replicate.2 ⟨_, h⟩, prod_replicate, one_pow] | ||
· exact (length l) | ||
· rfl⟩ |
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.
rw [List.eq_replicate.2 ⟨_, h⟩, prod_replicate, one_pow] | |
· exact (length l) | |
· rfl⟩ | |
rw [List.eq_replicate.mpr ⟨rfl, h⟩, prod_replicate, one_pow]⟩ |
@@ -129,7 +129,7 @@ theorem hasFDerivAt_integral_of_dominated_loc_of_lip' {F' : α → H →L[𝕜] | |||
exact ((hF_meas _ x_in).sub (hF_meas _ x₀_in)).sub (hF'_meas.apply_continuousLinearMap _) | |||
· refine mem_of_superset h_ball fun x hx ↦ ?_ | |||
apply (h_diff.and h_lipsch).mono | |||
rintro a ⟨-, ha_bound⟩ | |||
on_goal 1 => rintro a ⟨-, ha_bound⟩ |
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 get why this was linted this way, but it seems unnecessary. The 2nd goal is just a bounding function waiting to get described by the next line.
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 have been using on_goal
sometimes as a place-holder for something where maybe the linter should be manually silenced. I'll leave this comment visible, in case someone else wants to chime in.
on_goal 1 => let b : Finset ℂ := ?_ | ||
on_goal 1 => let c : Finset ℂ := ?_ |
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.
Perhaps the linter shouldn't add on_goal
when the additional goals are terms of Type
and not Prop
.
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.
This is probably a good heuristic, though I would limit the use of this heuristic to theorems. Again, I'll leave this up for further comments.
@@ -649,15 +649,15 @@ theorem cont_eval_fix {f k v} (fok : Code.Ok f) : | |||
obtain ⟨v'', h₁, h₂⟩ := this | |||
rw [reaches_eval] at h₂ | |||
swap | |||
exact ReflTransGen.single rfl | |||
· exact ReflTransGen.single rfl |
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.
Could be on_goal 2 => exact ReflTransGen.single rfl
removing the previous swap
.
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 tried to recycle as much as possible the original syntax. I would prefer this change to be a separate PR.
!bench |
Here are the benchmark results for commit 68a02d1. |
Co-authored-by: Ruben Van de Velde <[email protected]>
bors d+ |
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Pull request successfully merged into master. Build succeeded: |
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560. This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834. A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339. This should be the last of the adaptations.
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560. This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834. A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339. This should be the last of the adaptations.
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560. This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834. A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339. This should be the last of the adaptations.
A linter that makes sure that, when multiple goals are present, they are enclosed in `·`s. Adaptations (the order is chronological, there should be no dependency among them): * #12338, * #12361, * #12372, * #12560, * #12834, * #12381, * #12908, * #14939, plus many many more that this comment is too small to contain. Co-authored-by: Michael Rothgang <[email protected]>
A PR accompanying #12339.
Zulip discussion