Skip to content

draft: combining the multiple goal linter and the current modifications#12352

Closed
adomani wants to merge 132 commits intomasterfrom
adomani/multiple_goals_and_modifications
Closed

draft: combining the multiple goal linter and the current modifications#12352
adomani wants to merge 132 commits intomasterfrom
adomani/multiple_goals_and_modifications

Conversation

@adomani
Copy link
Copy Markdown
Contributor

@adomani adomani commented Apr 22, 2024

Open in Gitpod

adomani added 7 commits April 22, 2024 13:53
@adomani
chore: a batch of cdot usage
80b39f4
@adomani
feat: the multiGoal linter
dfe64d6
@adomani
import at bottom and imports
475c98a
@adomani
remove import
54ea495
@adomani
another batch of cdot usage
72f529a
@adomani
airplane batch
12e2a5e
@adomani
Squashed commit of the following:
484da43 
commit 12e2a5e
Author: Damiano Testa <adomani@gmail.com>
Date:   Mon Apr 22 22:37:58 2024 +0200

    airplane batch

commit 72f529a
Author: adomani <adomani@gmail.com>
Date:   Mon Apr 22 16:44:06 2024 +0200

    another batch of cdot usage

commit 54ea495
Author: adomani <adomani@gmail.com>
Date:   Mon Apr 22 14:01:54 2024 +0200

    remove import

commit 80b39f4
Author: adomani <adomani@gmail.com>
Date:   Mon Apr 22 13:53:56 2024 +0200

    chore: a batch of cdot usage
@adomani adomani marked this pull request as draft April 22, 2024 22:14
adomani added 22 commits April 23, 2024 00:51
@adomani
more replacements
7617048
@adomani
Merge branch 'adomani/use_cdots' into adomani/multiple_goals_and_modi…
e3bc97e 
…fications
@adomani
reversals
603322b
@adomani
Merge branch 'adomani/use_cdots' into adomani/multiple_goals_and_modi…
e0d0dd4 
…fications
@adomani
more exclude/ignore
c6e3489
@adomani
Merge branch 'adomani/lint_multiple_goals' into adomani/multiple_goal…
3a9cb1f 
…s_and_modifications
@adomani
chore: more cdots
d820f45
@adomani
long lines
c17b20d
@adomani
Merge branch 'adomani/use_cdots_again' into adomani/multiple_goals_an…
317ec06 
…d_modifications
@adomani
ignore conv_lhs/rhs
97a7d06
@adomani
add test file
1821772
@adomani
linterate
31d0e2a
@adomani
chore: more cdots 3
d3aacd5
@adomani
Merge branch 'master' into adomani/use_cdots_3
fd4c234
@adomani
repeat'
fa6d4dd
@adomani
case'
dc3f312
@adomani
Merge branch 'adomani/use_cdots_3' into adomani/multiple_goals_and_mo…
823125c 
…difications
@adomani
Merge branch 'adomani/lint_multiple_goals' into adomani/multiple_goal…
abbd269 
…s_and_modifications
@adomani
Merge branch 'master' into adomani/use_cdots_again
a8faf70
@adomani
yet another batch
62dfcfc
@adomani
yet another batch
96e76e9
@adomani
yet another small batch
73ad519
adomani and others added 17 commits May 13, 2024 12:00
@adomani
another missing space
7f1e100
@adomani
Apply Sébastien's suggestions
cf9b4fa
@adomani @sgouezel
Update Mathlib/Topology/Homotopy/HomotopyGroup.lean
846a758 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@adomani
Merge branch 'adomani/use_cdots_4' of github.com:leanprover-community…
f268d4d 
…/mathlib4 into adomani/use_cdots_4
@adomani
Merge branch 'adomani/use_cdots_4' into adomani/multiple_goals_and_mo…
00dd42c 
…difications
@adomani
Merge branch 'master' into adomani/multiple_goals_and_modifications
bf01ffa
@adomani
unindent
f34cce8
@adomani
import early and shake
080b0c0
@adomani
Merge remote-tracking branch 'origin/master' into adomani/lint_multip…
75a0e92 
…le_goals
@adomani
unlint two files
ce9a338
@adomani
more mathlib fixes
1b55583
@adomani
one more cdot
cfe902d
@adomani
silence Archive
1b9d82e
@adomani
silence tests!
1a25287
@adomani
chore: more cdots
f16f928
@adomani
Merge branch 'adomani/use_cdot_7' into adomani/lint_multiple_goals
17ba5da
@adomani
Merge remote-tracking branch 'origin/master' into adomani/lint_multip…
06b9532 
…le_goals
@ghost 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 May 15, 2024
callesonne pushed a commit that referenced this pull request May 16, 2024
@adomani @grunweg @callesonne
chore: adapt to multiple goal linter 6 (#12834)
e316632 
Another halfway split of #12381 on the way to #12352.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
grunweg added a commit that referenced this pull request May 17, 2024
@adomani @grunweg
chore: adapt to multiple goal linter 6 (#12834)
66a5986 
Another halfway split of #12381 on the way to #12352.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
@ghost 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 May 24, 2024
@ghost 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 Jun 6, 2024
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jul 23, 2024

Let me close this PR as obsolete: #14939 addressed the recent adaptations; otherwise, the linter passes on mathlib.
I'll review the multi-goal linter in its own PR.

@grunweg grunweg closed this Jul 23, 2024
@YaelDillies YaelDillies deleted the adomani/multiple_goals_and_modifications branch August 15, 2025 16:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@adomani @grunweg