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.

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

Rename Relation.Binary.Construct.(Flip/Converse) #1979

Merged
merged 7 commits into from
Jun 20, 2023

Conversation

Saransh-cpp
Copy link
Contributor

@Saransh-cpp Saransh-cpp commented Jun 13, 2023

Fixes #1757

Renamed -

  • Relation.Binary.Construct.Flip -> Relation.Binary.Construct.Flip.Ord
  • Relation.Binary.Construct.Converse -> Relation.Binary.Construct.Flip.EqAndOrd

A few questions -

  • Should I keep the original modules and mark them for deprecation, instead of removing them suddenly?
  • Should the CHANGELOG entry go in the Non-backwards compatible changes section?

Thanks!

@MatthewDaggitt
Copy link
Contributor

Thanks, looks great! Good questions as well 👍

Should I keep the original modules and mark them for deprecation, instead of removing them suddenly?

Yes, please!

Should the CHANGELOG entry go in the Non-backwards compatible changes section?

If the old modules are kept then it should go under the "Deprecated modules" section

@MatthewDaggitt
Copy link
Contributor

@Saransh-cpp the tests are showing there's still a reference to the old names left in.

@jamesmckinna
Copy link
Contributor

GenerateEverything should fix this once the old modules have been marked as DEPRECATED. At the moment, it looks though the generated EverythingSafe is picking up the old modules.

@Saransh-cpp
Copy link
Contributor Author

Hmm yes, there are no direct imports of Relation.Binary.Construct.Converse in the code at the moment. I traced back the chain of dependencies to check if the modules are being imported anywhere and found nothing.

I think the tests started failing once I removed the contents of Relation.Binary.Construct.Converse and Relation.Binary.Construct.Flip. Running the tests locally to confirm this.

Relation.Binary.Construct.Flip -> Relation.Binary.Construct.Flip.Ord
Relation.Binary.Construct.Converse -> Relation.Binary.Construct.Flip.EqAndOrd
@Saransh-cpp Saransh-cpp force-pushed the rename-flip-converse branch from 7746386 to 5fb8983 Compare June 19, 2023 15:22
@Saransh-cpp
Copy link
Contributor Author

Ah, I had to literally use "DEPRECATED" in the file. This works now. Thanks @jamesmckinna @MatthewDaggitt!

@MatthewDaggitt MatthewDaggitt merged commit 3b0f908 into agda:master Jun 20, 2023
@Saransh-cpp Saransh-cpp deleted the rename-flip-converse branch June 20, 2023 02:32
andreasabel added a commit that referenced this pull request Jun 20, 2023
@andreasabel
Copy link
Member

andreasabel commented Jun 20, 2023

This PR has a filename spelling mistake src/Relation/Binary/Construct/Flip.Agda (the uppercase .Agda extension).

As a consequence, I cannot update my working copy to master anymore:

agda-stdlib[master]$ git pull
Updating df8bdd4ab..8c70a9bfa
error: The following untracked working tree files would be overwritten by merge:
	src/Relation/Binary/Construct/Flip.Agda
Please move or remove them before you merge.
Aborting

Fixed by 3041cea

@MatthewDaggitt
Copy link
Contributor

Eek nice spot. Thank you @andreasabel

@Saransh-cpp
Copy link
Contributor Author

Woops, missed that, thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Rename Relation.Binary.Construct.(Flip/Converse)
4 participants