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

Make equality hints export and hidden inside a Hints module. #16157

Closed
wants to merge 1 commit into from

Conversation

Alizter
Copy link
Contributor

@Alizter Alizter commented Jun 8, 2022

This was a particularly annoying patch to do. I wonder if there is a way to mark Hints as "just there for the signature" so we don't have to include it everywhere.

@ppedrot any ideas?

Regarding this, I have no idea if we want to go this way, but it would be interesting to see how many people are even relying on this behaviour.

Fixes / closes coq/stdlib#18

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
  • Opened overlay pull requests.

cc @JasonGross

Sorry, something went wrong.

@Alizter Alizter added the kind: cleanup Code removal, deprecation, refactorings, etc. label Jun 8, 2022
@Alizter Alizter added this to the 8.17+rc1 milestone Jun 8, 2022
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jun 8, 2022

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

Comment on lines +57 to 66
Module Hints.
(** In order to avoid polluting the global hint database, we put these
equality hints into a Module. When implementing IsEqOrig, you will have to
include an empty [Module Hints. End Hints.]. *)
#[export] Hint Immediate eq_sym : core.
#[export] Hint Resolve eq_refl : core. #[export] Hint Resolve eq_trans :
core.
End Hints.
End IsEqOrig.

Copy link
Member

Choose a reason for hiding this comment

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

Ew, I forgot that this would require empty Hints modules in all downstream clients. What about just doing

Suggested change
Module Hints.
(** In order to avoid polluting the global hint database, we put these
equality hints into a Module. When implementing IsEqOrig, you will have to
include an empty [Module Hints. End Hints.]. *)
#[export] Hint Immediate eq_sym : core.
#[export] Hint Resolve eq_refl : core. #[export] Hint Resolve eq_trans :
core.
End Hints.
End IsEqOrig.
#[global]
Hint Immediate eq_refl eq_sym : core.
#[export]
Hint Resolve eq_trans : core.
End IsEqOrig.

and then just replace all of the Import FOO.Hints that you added with #[local] Hint Resolve FOO.eq_trans : core.?

@Zimmi48 Zimmi48 modified the milestones: 8.17+rc1, 8.18+rc1 Nov 21, 2022
@Alizter
Copy link
Contributor Author

Alizter commented Jan 9, 2023

Don't care to continue this any longer.

@Alizter Alizter closed this Jan 9, 2023
@coqbot-app coqbot-app bot removed this from the 8.18+rc1 milestone Jan 9, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: cleanup Code removal, deprecation, refactorings, etc.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

The Standard Library should not be adding transitivity and symmetry hints to core
3 participants