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

Ltac2: importing a mutable definition does not undo its mutations #18713

Merged
merged 3 commits into from Apr 2, 2024
Merged

Ltac2: importing a mutable definition does not undo its mutations #18713

merged 3 commits into from Apr 2, 2024

Conversation

SkySkimmer
Copy link
Contributor

cf #10556

The previous behaviour can be gotten by doing eg

(* auxiliary definition to avoid repeating it, if it's a simple expression it can also be inlined *)
Ltac2 original_def := ...

Ltac2 mutable the_def := original_def.

Ltac2 Set the_def := original_def.

instead of Ltac2 mutable the_def := ....

Also add test for Ltac2 mutable definitions vs Import/Export.

This exposes some complex behaviour around repeated imports when using Set as.

@SkySkimmer SkySkimmer added the part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. label Feb 23, 2024
@SkySkimmer SkySkimmer requested a review from a team as a code owner February 23, 2024 13:50
@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 Feb 23, 2024
@SkySkimmer SkySkimmer requested a review from a team as a code owner February 23, 2024 13:59
@SkySkimmer
Copy link
Contributor 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 Feb 23, 2024
@SkySkimmer SkySkimmer mentioned this pull request Feb 23, 2024
Open
@ppedrot ppedrot self-assigned this Feb 25, 2024
@rlepigre
Copy link
Contributor

Are we sure this is the right semantics? It seems to me that seeing toplevel commands like Ltac2 Set as things running only at "module initialization" (by analogy to OCaml's module initialization for example) would be more intuitive. In other words, maybe the effect should take place as soon as one Imports a module that performs the effect directly, or a module that Exports the module doing the effect (and so on), and also, ensure that the effect can only be run once, on the first Import that should trigger it, and subsequent Imports are no-ops. CC @Janno.

@SkySkimmer
Copy link
Contributor Author

Ocaml module initialization would be Require time not Import.

@rlepigre
Copy link
Contributor

Ocaml module initialization would be Require time not Import.

That's why I put it in quotes, I agree the analogy is not perfect.

@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 Feb 27, 2024
@SkySkimmer
Copy link
Contributor 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 Feb 27, 2024
@proux01 proux01 mentioned this pull request Feb 28, 2024
Merged
ppedrot
ppedrot reviewed Mar 4, 2024
View reviewed changes
test-suite/ltac2/rebind.v

Import Change1 Change1.

(* Import doesn't deduplicate / assume idempotence (may change in the future?) *)
Copy link
Member

Choose a reason for hiding this comment

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

Non-idempotence of import looks fine to me, both in general and for this particular command. The one thing we care about is idempotence of require.

@ppedrot
Copy link
Member

ppedrot commented Mar 14, 2024

@SkySkimmer refman not happy

@SkySkimmer SkySkimmer force-pushed the ltac2-original-redef-no-import branch from 471d430 to 5b53b64 Compare March 14, 2024 11:41
@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 Mar 14, 2024
@SkySkimmer
Ltac2: importing a mutable definition does not undo its mutations
2e0aced 
cf coq#10556

The previous behaviour can be gotten by doing eg

~~~coq
(* auxiliary definition to avoid repeating it, if it's a simple expression it can also be inlined *)
Ltac2 original_def := ...

Ltac2 mutable the_def := original_def.

Ltac2 Set the_def := original_def.
~~~

instead of `Ltac2 mutable the_def := ...`.
@SkySkimmer
Add test for Ltac2 mutable definitions vs Import/Export
dce238d 
This exposes some complex behaviour around repeated imports when using
`Set as`.
@SkySkimmer
Document locality of Ltac2 Set
5dea992
@SkySkimmer SkySkimmer force-pushed the ltac2-original-redef-no-import branch from 5b53b64 to 5dea992 Compare March 18, 2024 10:27
@ppedrot
Copy link
Member

ppedrot commented Mar 23, 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 Mar 23, 2024
@ppedrot
Copy link
Member

ppedrot commented Mar 28, 2024

I have no strong opinion about the expected semantics of Ltac2 late binding w.r.t. require / import. The new behaviour is more expressive than the previous one, and it's reasonable to me. @rlepigre @Janno are you fine with the current semantics?

@rlepigre
Copy link
Contributor

I have no strong opinion about the expected semantics of Ltac2 late binding w.r.t. require / import. The new behaviour is more expressive than the previous one, and it's reasonable to me. @rlepigre @Janno are you fine with the current semantics?

I don't have a very strong opinion either. What would be most intuitive to me would be to perform the update at Require time, to make this similar to what you'd get in OCaml. But is that even be an option?

@SkySkimmer
Copy link
Contributor Author

That's what ltac1 does.

@ppedrot ppedrot added this to the 8.20+rc1 milestone Apr 2, 2024
@ppedrot
Copy link
Member

ppedrot commented Apr 2, 2024

Let's merge then @coqbot merge now

@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Apr 2, 2024

@ppedrot: You cannot merge this PR because:

  • There is no kind: label.

@ppedrot ppedrot added the kind: fix This fixes a bug or incorrect documentation. label Apr 2, 2024
@ppedrot
Copy link
Member

ppedrot commented Apr 2, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 1247653 into coq:master Apr 2, 2024
6 checks passed
@SkySkimmer SkySkimmer deleted the ltac2-original-redef-no-import branch April 2, 2024 10:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jfehrle jfehrle jfehrle left review comments

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: fix This fixes a bug or incorrect documentation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@SkySkimmer @rlepigre @ppedrot @jfehrle