[Merged by Bors] - chore: adapt to multiple goal linter 1 by adomani · Pull Request #12338 · leanprover-community/mathlib4

adomani · 2024-04-22T12:01:31Z

A PR accompanying #12339.

grunweg

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.

grunweg · 2024-04-22T13:52:36Z

Mathlib/AlgebraicGeometry/Gluing.lean

 def fromGlued : 𝒰.gluedCover.glued ⟶ X := by
  fapply Multicoequalizer.desc
-  exact fun x => 𝒰.map x
+  · exact fun x => 𝒰.map x


Can you move this into the fapply? If possible, I'd find this even nicer.

Mathlib/Data/Seq/Parallel.lean

Mathlib/Data/Seq/Seq.lean

Mathlib/AlgebraicGeometry/Gluing.lean

Mathlib/Algebra/Order/Group/Abs.lean

Mathlib/Data/Int/Bitwise.lean

Mathlib/Data/List/Permutation.lean

Mathlib/Data/List/Zip.lean

grunweg · 2024-04-22T14:03:37Z

Mathlib/Data/Nat/WithBot.lean

-  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⟩)


I'm on the fence if the any_goals => repeat change is better.

rosborn · 2024-04-23T02:03:24Z

Mathlib/Algebra/Order/BigOperators/Group/List.lean

+    rw [List.eq_replicate.2 ⟨_, h⟩, prod_replicate, one_pow]
+    · exact (length l)
+    · rfl⟩


Suggested change

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]⟩

rosborn · 2024-04-23T02:34:07Z

Mathlib/Analysis/Calculus/ParametricIntegral.lean

  · 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⟩


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.

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.

rosborn · 2024-04-23T02:41:41Z

Mathlib/Analysis/Complex/Polynomial.lean

+  on_goal 1 => let b : Finset ℂ := ?_
+  on_goal 1 => let c : Finset ℂ := ?_


Perhaps the linter shouldn't add on_goal when the additional goals are terms of Type and not Prop.

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.

rosborn · 2024-04-23T02:59:56Z

Mathlib/Computability/TMToPartrec.lean

      rw [reaches_eval] at h₂
      swap
-      exact ReflTransGen.single rfl
+      · exact ReflTransGen.single rfl


Could be on_goal 2 => exact ReflTransGen.single rfl removing the previous swap.

I tried to recycle as much as possible the original syntax. I would prefer this change to be a separate PR.

adomani · 2024-04-23T12:26:35Z

!bench

leanprover-bot · 2024-04-23T12:57:46Z

Here are the benchmark results for commit 68a02d1.
There were no significant changes against commit 5b96848.

Mathlib/Data/List/Basic.lean

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

jcommelin · 2024-04-30T04:30:34Z

bors d+

mathlib-bors · 2024-04-30T04:30:36Z

✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

adomani · 2024-04-30T06:03:07Z

bors r+

A PR accompanying #12339. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20against.20.22multi-goal.20proofs.22)

mathlib-bors · 2024-04-30T07:18:44Z

Pull request successfully merged into master.

Build succeeded:

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

A PR accompanying #12339. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20against.20.22multi-goal.20proofs.22)

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

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 PR accompanying #12339. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20against.20.22multi-goal.20proofs.22)

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

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 <rothgami@math.hu-berlin.de>

adomani added 2 commits April 22, 2024 13:53

chore: a batch of cdot usage

80b39f4

remove import

54ea495

adomani mentioned this pull request Apr 22, 2024

[Merged by Bors] - feat: the multiGoal linter #12339

Closed

grunweg reviewed Apr 22, 2024

View reviewed changes

adomani added 4 commits April 22, 2024 16:44

another batch of cdot usage

72f529a

airplane batch

12e2a5e

more replacements

7617048

reversals

603322b

adomani added the awaiting-review label Apr 23, 2024

3 more

68a02d1

rosborn reviewed Apr 23, 2024

View reviewed changes

This was referenced Apr 23, 2024

[Merged by Bors] - chore: adapt to multiple goal linter 2 #12361

Closed

[Merged by Bors] - chore: adapt to multiple goal linter 3 #12372

Closed

adomani mentioned this pull request Apr 23, 2024

[Merged by Bors] - chore: adapt to multiple goal linter 4 #12381

Closed

adomani changed the title ~~chore: a batch of cdot usage~~ chore: adapt to multiple goal linter 1 Apr 23, 2024

Ruben-VandeVelde approved these changes Apr 23, 2024

View reviewed changes

Mathlib/Data/List/Basic.lean Outdated Show resolved Hide resolved

Ruben's indentation

69469c8

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 24, 2024

Merge remote-tracking branch 'origin/master' into adomani/use_cdots

d6a2820

ghost 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 Apr 25, 2024

Merge remote-tracking branch 'origin/master' into adomani/use_cdots

8ec445a

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 26, 2024

github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Apr 30, 2024

mathlib-bors bot changed the title ~~chore: adapt to multiple goal linter 1~~ [Merged by Bors] - chore: adapt to multiple goal linter 1 Apr 30, 2024

mathlib-bors bot closed this Apr 30, 2024

mathlib-bors bot deleted the adomani/use_cdots branch April 30, 2024 07:18

mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024

chore: adapt to multiple goal linter 3 (#12372)

ce2e171

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024

chore: adapt to multiple goal linter 2 (#12361)

fe96aa4

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024

chore: adapt to multiple goal linter 3 (#12372)

d29b378

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

apnelson1 pushed a commit that referenced this pull request May 12, 2024

chore: adapt to multiple goal linter 1 (#12338)

83abaca

A PR accompanying #12339. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20against.20.22multi-goal.20proofs.22)

apnelson1 pushed a commit that referenced this pull request May 12, 2024

chore: adapt to multiple goal linter 2 (#12361)

c38d260

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

apnelson1 pushed a commit that referenced this pull request May 12, 2024

chore: adapt to multiple goal linter 3 (#12372)

986e06d

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

callesonne pushed a commit that referenced this pull request May 16, 2024

chore: adapt to multiple goal linter 1 (#12338)

50eef27

A PR accompanying #12339. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20against.20.22multi-goal.20proofs.22)

callesonne pushed a commit that referenced this pull request May 16, 2024

chore: adapt to multiple goal linter 2 (#12361)

de4ab15

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

callesonne pushed a commit that referenced this pull request May 16, 2024

chore: adapt to multiple goal linter 3 (#12372)

863d5c2

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

		on_goal 1 => let b : Finset ℂ := ?_
		on_goal 1 => let c : Finset ℂ := ?_

Conversation

adomani commented Apr 22, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

adomani commented Apr 23, 2024

Uh oh!

leanprover-bot commented Apr 23, 2024

Uh oh!

Uh oh!

jcommelin commented Apr 30, 2024

Uh oh!

mathlib-bors bot commented Apr 30, 2024

Uh oh!

adomani commented Apr 30, 2024

Uh oh!

mathlib-bors bot commented Apr 30, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

adomani commented Apr 22, 2024 •

edited

Loading

grunweg left a comment •

edited

Loading