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

Typeclasses default mode #19473

Merged
merged 1 commit into from
Sep 5, 2024
Merged

Typeclasses default mode #19473

merged 1 commit into from
Sep 5, 2024

Conversation

mattam82
Copy link
Member

@mattam82 mattam82 commented Aug 26, 2024 •
edited by gares
Loading

  • Allow to set globally a default mode for all parameters of a class
  • Add an attribute that overrides this on a class by class basis
  • Add a settable warning for using the default mode
  • The default is still "-", meaning no mode filtering and full compatibility.
  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • Documented any new / changed user messages.

@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 26, 2024
@TheoWinterhalter TheoWinterhalter mentioned this pull request Aug 26, 2024
Closed
2 tasks
@mattam82 mattam82 force-pushed the typeclasses-default-mode branch 2 times, most recently from 33a834c to 9718d58 Compare August 28, 2024 09:44
@mattam82
Copy link
Member Author

mattam82 commented Aug 28, 2024 •
edited
Loading

@coqbot run full ci

@Alizter
Copy link
Contributor

Alizter commented Aug 28, 2024

One thing that is missing in the Hint Mode documentation is an example of what those settings mean in practice. This should probably be improved in a later PR with some examples in the documentaiton.

What does the change of default hint mode mean here in practice for typeclasses?

@mattam82 mattam82 marked this pull request as ready for review August 28, 2024 21:33
@mattam82 mattam82 requested review from a team as code owners August 28, 2024 21:33
@mattam82
Copy link
Member Author

I backtracked on changing the default, too much incompatibilities arise. If one changes it from "-" to "!" or "+" it will generally incur more failed typeclass searches (or speedups in successful searches). I can add more doc, that's really necessary.

jfehrle
jfehrle reviewed Aug 29, 2024
View reviewed changes
Copy link
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

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

wording suggestions

@TheoWinterhalter
Copy link
Contributor

Instead of changing the global default for everyone, my suggestion would be to do it for new user-created stuff, like proposed in #19117.

@ppedrot
Copy link
Member

ppedrot commented Aug 29, 2024

Indeed, the change of default hint locality is a somewhat successful prior of this technique. We could first warn when modes are missing, turn this at some point in an error for one version and then switch the default.

@mattam82
Copy link
Member Author

Agreed @TheoWinterhalter, that was the original motivation of this PR to be able to set the default mode to "!" in GoodDefaults :)

@mattam82
Copy link
Member Author

@coqbot run full ci

@coqbot-app coqbot-app bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Aug 29, 2024
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Aug 29, 2024

🔴 CI failures at commit 9718d58 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 9ed5a0f succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-aac_tactics, ci-coinduction, ci-cross_crypto, ci-iris, ci-itree, ci-math_classes, ci-perennial
  • You can also pass me a specific list of targets to minimize as arguments.

@mattam82 mattam82 force-pushed the typeclasses-default-mode branch from 58e5fe3 to 2bb3c20 Compare August 29, 2024 12:08
@mattam82
Copy link
Member Author

I backtracked on trying to change the default or any mode declaration in the stdlib to ensure compatibility for now.

@mattam82
Copy link
Member Author

@coqbot run full ci

@coqbot-app coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 29, 2024
@mattam82
Copy link
Member Author

mattam82 commented Sep 2, 2024

@coqbot run full ci

@coqbot-app coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 2, 2024
@mattam82
Copy link
Member Author

mattam82 commented Sep 3, 2024

It just needs a changelog and review now.

@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 4, 2024
@mattam82
Copy link
Member Author

mattam82 commented Sep 4, 2024

@gares could you assign and merge?

SkySkimmer
SkySkimmer reviewed Sep 4, 2024
View reviewed changes
SkySkimmer
SkySkimmer reviewed Sep 4, 2024
View reviewed changes
pretyping/typeclasses.ml
Comment on lines -266 to +273
let evi = Evd.find_undefined evd ev in
let ev_class = class_of_constr env evd (Evd.evar_concl evi) in
if Option.is_empty ev_class then accu
else (* focus on one instance if only one was searched for *)
if Option.has_some accu then raise MultipleFound
else (Some ev)
match Evd.find_undefined evd ev with
| exception Not_found -> None
| evi ->
let ev_class = class_of_constr env evd (Evd.evar_concl evi) in
if Option.is_empty ev_class then accu
else (* focus on one instance if only one was searched for *)
if Option.has_some accu then raise MultipleFound
else (Some ev)
Copy link
Contributor

Choose a reason for hiding this comment

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

why this change?

Copy link
Member Author

Choose a reason for hiding this comment

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

This is a bugfix

Copy link
Member Author

Choose a reason for hiding this comment

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

It would otherwise result in an uncaught exception

Copy link
Contributor

Choose a reason for hiding this comment

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

Why though? What's the test case?

Copy link
Member

Choose a reason for hiding this comment

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

I guess the evar in question could be solved by a previous TC resolution. Does this make sense?

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes, it could be solved from another resolution in principle.

@gares gares self-assigned this Sep 4, 2024
@gares gares added this to the 8.21+rc1 milestone Sep 4, 2024
gares
gares reviewed Sep 4, 2024
View reviewed changes
@gares
Copy link
Member

gares commented Sep 4, 2024

@coqbot run full ci

@coqbot-app coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 4, 2024
jfehrle
jfehrle reviewed Sep 4, 2024
View reviewed changes
Copy link
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

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

Further suggestions

@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 5, 2024
gares
gares reviewed Sep 5, 2024
View reviewed changes
vernac/record.ml Outdated
Comment on lines 43 to 48
let { Goptions.get = typeclasses_default_mode } =
let interp = function
| Hints.ModeInput -> "+"
| Hints.ModeOutput -> "-"
| Hints.ModeNoHeadEvar -> "!"
in
Copy link
Member

Choose a reason for hiding this comment

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

I would prefer to have this code next to the one for parsing modes.

@gares
Copy link
Member

gares commented Sep 5, 2024

@mattam82 I think we can merge, but I also think you could rebase and squash.
If you want to apply my last nit while doing so fine, otherwise it is not the end of the world.

Just tell me if you do any other change, cause CI was already green and I'd rather not run it again if not needed.

@mattam82
[typeclasses] Typeclasses Default Mode option and mode attribute
a6362e5 
Overlay for elpi

Add tests for the mode attribute of Class

Add changelog

Move parse_mode(s) to hints.ml

Slightly simplify code

Fixed parsing rule for mode attribute, refering to Hint Mode syntax definition (as is done for the warning attribute for example)

Expose string of mode and factorize code
@mattam82 mattam82 force-pushed the typeclasses-default-mode branch from 966f593 to a6362e5 Compare September 5, 2024 07:53
@mattam82
Copy link
Member Author

mattam82 commented Sep 5, 2024

I just did your nitpick and squashed, factorizing with code in hints.ml (string_of_mode). A light pipeline should be enough here.

@gares
Copy link
Member

gares commented Sep 5, 2024

@coqbot merge now

@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 5, 2024

@gares: You cannot merge this PR because:

  • There is still a needs: full CI label.
  • There is no kind: label.

@gares gares added kind: feature New user-facing feature request or implementation. and removed needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Sep 5, 2024
@gares
Copy link
Member

gares commented Sep 5, 2024

sudo @coqbot merge now

@coqbot-app coqbot-app bot merged commit 7d5ef7c into coq:master Sep 5, 2024
6 checks passed
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 5, 2024

@gares: Please take care of the following overlays:

  • 19473-mattam82-typeclasses-default-mode.sh

@mattam82 mattam82 deleted the typeclasses-default-mode branch September 5, 2024 17:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@gares gares gares approved these changes

@jfehrle jfehrle jfehrle left review comments

@SkySkimmer SkySkimmer SkySkimmer left review comments

Assignees

@gares gares

Labels
kind: feature New user-facing feature request or implementation.
Projects
None yet
Milestone
9.0+rc1
Development

Successfully merging this pull request may close these issues.
7 participants
@mattam82 @Alizter @TheoWinterhalter @ppedrot @gares @jfehrle @SkySkimmer