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

Adding a modifier "clear simpl" to Arguments to reset "simpl" behavior to its default #19216

Merged
merged 3 commits into from
Jul 15, 2024
Merged

Adding a modifier "clear simpl" to Arguments to reset "simpl" behavior to its default #19216

merged 3 commits into from
Jul 15, 2024

Conversation

herbelin
Copy link
Member

@herbelin herbelin commented Jun 17, 2024 •
edited by proux01
Loading

This is proposal for supporting resetting the effect of simpl never, simpl nomatch, and /.

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.

Overlay (to be merged in sync with the current PR)

@herbelin herbelin added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: reduction strategies The Strategy command for defining reduction straegies. labels Jun 17, 2024
@herbelin herbelin added this to the 8.21+rc1 milestone Jun 17, 2024
@herbelin herbelin requested review from a team as code owners June 17, 2024 13:04
@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 Jun 17, 2024
@SkySkimmer
Copy link
Contributor

Is this useful?

@SkySkimmer SkySkimmer added the needs: documentation Documentation was not added or updated. label Jun 17, 2024
@herbelin
Copy link
Member Author

I don't know how to reset the behavior table otherwise, but maybe I missed something. For instance, how do you revert the effect of e.g. Arguments Nat.add : simpl never.?

@SkySkimmer
Copy link
Contributor

Is it useful to reset the table?

@herbelin
Copy link
Member Author

herbelin commented Jun 17, 2024 •
edited
Loading

The motivation is that I was working on the overlays for #18591. The two failing developments were setting simpl never for some constants (namely List.app and Nat.add). I wanted to test what it would change to deactivate simpl never but I found no way to do it.

proux01
proux01 approved these changes Jun 20, 2024
View reviewed changes
Copy link
Contributor

@proux01 proux01 left a comment

Choose a reason for hiding this comment

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

LGTM, just requires update of doc and a changelog entry.

@rlepigre
Copy link
Contributor

Is this useful?

@SkySkimmer I know that we missed having the possibility to reset the behaviour several times. The typical situation is when an external library messes with the simpl behaviour on some shared definitions (e.g., from the standard library), but you want a different behaviour in parts of your development.

@proux01 proux01 self-assigned this Jun 20, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 20, 2024
herbelin added a commit to herbelin/github-coq that referenced this pull request Jun 20, 2024
@herbelin
Change log for coq#19216
3452b89
@herbelin herbelin force-pushed the master+clear-simpl branch from 52c19fa to 3452b89 Compare June 20, 2024 18:33
@herbelin herbelin requested a review from a team as a code owner June 20, 2024 18:33
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Jun 20, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 20, 2024
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 20, 2024
proux01
proux01 reviewed Jun 21, 2024
View reviewed changes
@herbelin herbelin removed the needs: documentation Documentation was not added or updated. label Jul 2, 2024
herbelin added a commit to herbelin/github-coq that referenced this pull request Jul 2, 2024
@herbelin
Change log for coq#19216
622f756
@herbelin herbelin force-pushed the master+clear-simpl branch from d1874d6 to e09a02f Compare July 2, 2024 13:13
@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 Jul 2, 2024
@herbelin
Copy link
Member Author

herbelin commented Jul 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 Jul 2, 2024
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 3, 2024
@proux01 proux01 force-pushed the master+clear-simpl branch from e09a02f to adfd773 Compare July 3, 2024 12:55
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 3, 2024
@proux01 proux01 force-pushed the master+clear-simpl branch 2 times, most recently from 7adfce7 to 65959a7 Compare July 3, 2024 16:26
@coqbot-app coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. request: full CI Use this label when you want your next push to trigger a full CI. labels Jul 3, 2024
proux01 added a commit to proux01/coq-elpi that referenced this pull request Jul 15, 2024
@proux01
Adapt to coq/coq#19216
da34ca3
@proux01 proux01 mentioned this pull request Jul 15, 2024
Merged
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 15, 2024
@proux01 proux01 force-pushed the master+clear-simpl branch from 65959a7 to 38aec86 Compare July 15, 2024 09:21
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 15, 2024
proux01 added a commit to proux01/coq-elpi that referenced this pull request Jul 15, 2024
@proux01
Adapt to coq/coq#19216
e32901f
@proux01
Copy link
Contributor

proux01 commented Jul 15, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 3f08009 into coq:master Jul 15, 2024
6 checks passed
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Jul 15, 2024

@proux01: Please take care of the following overlays:

  • 19216-herbelin-clear-simpl.sh

gares added a commit to LPCIC/coq-elpi that referenced this pull request Jul 15, 2024
@gares
Merge pull request #665 from proux01/coq_19216
48c3020 
Adapt to coq/coq#19216
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@proux01 proux01 proux01 approved these changes

Assignees

@proux01 proux01

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: reduction strategies The Strategy command for defining reduction straegies.
Projects
None yet
Milestone
9.0+rc1
Development

Successfully merging this pull request may close these issues.
4 participants
@herbelin @SkySkimmer @rlepigre @proux01