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

Rename homo to ∙-homo in Algebra.Morphism.Structures #2464

Open
wants to merge 18 commits into
base: master
Choose a base branch
from
Open

Rename homo to ∙-homo in Algebra.Morphism.Structures #2464

wants to merge 18 commits into from

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Aug 29, 2024 •
edited
Loading

Fixes #2458

NB: the warning-on-usage does not seem to be correctly triggering when reference to homo is made in renaming directives, nor in actual usage? UPDATED: A known, but not-yet-fixed, Agda bug. Grrrr.

UPDATED: TODO

  • fix CHANGELOG only after the v2.x milestone/release cycle converges

JacquesCarette
JacquesCarette approved these changes Aug 29, 2024
View reviewed changes
Copy link
Contributor

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

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

Looks good to me - but isn't this a breaking change?

@jamesmckinna jamesmckinna added this to the v2.2 milestone Aug 29, 2024
@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Aug 29, 2024 •
edited
Loading

Looks good to me - but isn't this a breaking change?

I forget (or: have never properly understood?!) whether changing (field) names via deprecation is breaking or not?
UPDATED: Oh, I suppose it must be!?

@jamesmckinna jamesmckinna modified the milestones: v2.2, v3.0 Aug 29, 2024
This was referenced Aug 29, 2024
Open
Closed
@MatthewDaggitt
Copy link
Contributor

Yes, unfortunately it is an unavoidable breaking change.

@jamesmckinna
Copy link
Contributor Author

Thanks @gallais but I'd been waiting to merge until we had a clean CHANGELOG for v3.0, but perhaps others things had got into conflict? I can't see that now on GH...

MatthewDaggitt
MatthewDaggitt approved these changes Feb 11, 2025
View reviewed changes
Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

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

Otherwise looks good.

CHANGELOG.md
* In `Algebra.Morphism.Structures`:
```agda
homo ↦ ∙-homo
```
Copy link
Contributor

Choose a reason for hiding this comment

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

This unfortunately is in the wrong section of the CHANGELOG, as it's not a deprecated name. Instead it's a breaking change to the name.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes, that's a good catch. Sorry not to have revisited this recently... will fix.

Copy link
Contributor Author

@jamesmckinna jamesmckinna Feb 11, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

Now done... but there is still a WARNING_ON_USE deprecation warning in Algebra.Morphism.Structures.IsMagmaHomomorphism associated with the copy of the old name. Does that not also merit an entry in the Deprecated names section? If not, will remove! Please advise

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JacquesCarette JacquesCarette JacquesCarette approved these changes

@MatthewDaggitt MatthewDaggitt MatthewDaggitt approved these changes

Assignees
No one assigned
Labels
breaking cosmetic deprecation naming refactoring
Projects
None yet
Milestone
v3.0
Development

Successfully merging this pull request may close these issues.

Get rid of inconsistent homo name in algebra hierarchy?
4 participants
@jamesmckinna @MatthewDaggitt @JacquesCarette @gallais