Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - chore: fix outdated ext porting notes #17810

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: fix outdated ext porting notes #17810

wants to merge 1 commit into from

Conversation

Vierkantor
Copy link
Contributor

I went through all porting notes mentioning ext and fixed / removed those that no longer apply.

Open in Gitpod

@Vierkantor Vierkantor added porting-notes Mathlib3 to Mathlib4 porting notes. tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip labels Oct 16, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Oct 16, 2024 •
edited
Loading

PR summary dd52b4e769

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@Vierkantor Vierkantor mentioned this pull request Oct 16, 2024
Closed
YaelDillies
YaelDillies approved these changes Oct 16, 2024
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

🎉

Mathlib/CategoryTheory/EpiMono.lean
@@ -38,7 +38,6 @@ such that `f ≫ retraction f = 𝟙 X`.
Every split monomorphism is a monomorphism.
-/
/- Porting note(#5171): removed @[nolint has_nonempty_instance] -/
/- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule -/
@[ext, aesop apply safe (rule_sets := [CategoryTheory])]
structure SplitMono {X Y : C} (f : X ⟶ Y) where
Copy link
Collaborator

Choose a reason for hiding this comment

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

Should the aesop tag be removed accordingly? What does it even do, when applied to a structure?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

So I went as far as checking the aesop source code and as far as I can tell, no idea what it's supposed to mean 🤷. Looks like removing the attribute doesn't break anything either.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Thanks for the digging! @JLimperg, maybe there should be a check in aesop that one is not tagging a structure?

Copy link
Collaborator

Choose a reason for hiding this comment

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

The rule takes the structure and register it as a rule with conclusion Type _, naturally. 🙂 But yes, Aesop should warn about this. leanprover-community/aesop#172

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 16, 2024
grunweg
grunweg approved these changes Oct 16, 2024
View reviewed changes
Copy link
Collaborator

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

Thanks, this is great. Feel free to maintainer merge on my behalf once Yael's question about aesop has been resolved.

mathlib-bors bot pushed a commit that referenced this pull request Oct 16, 2024
@Vierkantor
chore: classify porting notes about ext (#17809)
0b07d2a 
I checked all porting notes mentioning `ext` and either fixed them (see #17810), or classified them as
 * #5229 if it's a new `@[ext]` lemma
 * #11041 if it's a regression in `ext`
 * #11182 if `@[ext]` had to be removed

This PR should contain only modifications to comments.
@Vierkantor
chore: fix outdated ext porting notes
dd52b4e 
I went through all porting notes mentioning `ext` and fixed / removed those that no longer apply.
@Vierkantor Vierkantor force-pushed the outdated-ext-porting-notes branch from 2e1ebb3 to dd52b4e Compare October 17, 2024 09:01
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 17, 2024
@bryangingechen
Copy link
Contributor

Thanks!
bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 17, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 17, 2024
@Vierkantor
chore: fix outdated ext porting notes (#17810)
bdecdcb 
I went through all porting notes mentioning `ext` and fixed / removed those that no longer apply.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Oct 17, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: fix outdated ext porting notes [Merged by Bors] - chore: fix outdated ext porting notes Oct 17, 2024
@mathlib-bors mathlib-bors bot closed this Oct 17, 2024
@mathlib-bors mathlib-bors bot deleted the outdated-ext-porting-notes branch October 17, 2024 20:34
@JLimperg JLimperg mentioned this pull request Oct 28, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JLimperg JLimperg JLimperg left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

@grunweg grunweg grunweg approved these changes

Assignees
No one assigned
Labels
porting-notes Mathlib3 to Mathlib4 porting notes. ready-to-merge This PR has been sent to bors. tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@Vierkantor @bryangingechen @JLimperg @grunweg @YaelDillies @leanprover-community-bot-assistant