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: use 0 argument externals when possible #17534

Merged
merged 2 commits into from Dec 4, 2023
Merged

Ltac2: use 0 argument externals when possible #17534

merged 2 commits into from Dec 4, 2023

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Apr 26, 2023 •
edited

@SkySkimmer SkySkimmer added needs: discussion Further discussion is needed. needs: overlay This is breaking external developments we track in CI. labels Apr 26, 2023
@SkySkimmer SkySkimmer requested a review from a team as a code owner April 26, 2023 16:12
@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 Apr 26, 2023
@SkySkimmer SkySkimmer mentioned this pull request Apr 26, 2023
Merged
@ppedrot ppedrot added the needs: merge of dependency This PR depends on another PR being merged first. label Apr 26, 2023
@SkySkimmer SkySkimmer force-pushed the ltac2-0arg-empty branch 4 times, most recently from 4e9d81a to e3e2dd0 Compare May 2, 2023 11:04
@SkySkimmer SkySkimmer removed the needs: merge of dependency This PR depends on another PR being merged first. label May 2, 2023
@SkySkimmer SkySkimmer force-pushed the ltac2-0arg-empty branch 2 times, most recently from 1159554 to 8cefaca Compare May 5, 2023 13:05
@ppedrot ppedrot self-assigned this May 22, 2023
@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 Sep 25, 2023
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 25, 2023
@ppedrot
Copy link
Member

ppedrot commented Nov 6, 2023

@SkySkimmer I think this should go in to 8.19 with the other API-breaking changes so that we concentrate the breakage in one version. Could you rebase and write the missing overlays?

@ppedrot ppedrot added this to the 8.19+rc1 milestone Nov 6, 2023
@ppedrot ppedrot removed the needs: discussion Further discussion is needed. label Nov 6, 2023
@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 Nov 6, 2023
@SkySkimmer SkySkimmer added kind: cleanup Code removal, deprecation, refactorings, etc. needs: changelog entry This should be documented in doc/changelog. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. labels Nov 6, 2023
@SkySkimmer
Copy link
Contributor Author

Not sure what's a nice way to make an overlay for coqutil. [| |] is only since 8.18.

cc @JasonGross

@SkySkimmer SkySkimmer requested a review from a team as a code owner November 8, 2023 13:48
@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 Nov 8, 2023
SkySkimmer added a commit to SkySkimmer/coqutil that referenced this pull request Nov 22, 2023
@SkySkimmer
Use Ltac2.Array.make 0 instead of Array.empty for compat (coq/coq…
676f556 
…#17534)
@SkySkimmer
Copy link
Contributor Author

Ended up doing mit-plv/coqutil#107, now waiting for merge and submodule bumps

@SkySkimmer SkySkimmer removed the needs: changelog entry This should be documented in doc/changelog. label Nov 22, 2023
samuelgruetter pushed a commit to mit-plv/coqutil that referenced this pull request Nov 22, 2023
@SkySkimmer
Use Ltac2.Array.make 0 instead of Array.empty for compat (coq/coq…
c1f3e55 
…#17534) (#107)
@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 Nov 22, 2023
@SkySkimmer SkySkimmer removed the needs: overlay This is breaking external developments we track in CI. label Nov 22, 2023
@ppedrot
Copy link
Member

ppedrot commented Dec 4, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit aba4c65 into coq:master Dec 4, 2023
6 checks passed
@SkySkimmer SkySkimmer deleted the ltac2-0arg-empty branch December 4, 2023 14:46
ejgallego
ejgallego reviewed Dec 4, 2023
View reviewed changes
theories/Compat/Coq818.v
Export Ltac2.Array.
Ltac2 empty () := empty.
End Array.
End Ltac2.
Copy link
Member

Choose a reason for hiding this comment

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

@SkySkimmer @ppedrot this seems wrong, as it makes the stdlib depend on Ltac2 .

It doesn't fail in CI because we implicitly put Ltac2 in scope, but that could change in the future.

I'm not sure we should do anything about this, but at least I feel I had to signal it to you.

Copy link
Member

Choose a reason for hiding this comment

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

Shouldn't we have Compat as a separate theory depending on everything from Coq?

Copy link
Member

Choose a reason for hiding this comment

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

I don't know, several options are possible; I guess it'd make more sense to have the stdlib depend on Ltac2?

Copy link
Member

Choose a reason for hiding this comment

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

As of today we handle Ltac2 and Coq as the same package, in both cases we pass -boot -Q $path_to_ltac2 Ltac2 -R $path_to_theories Coq, so there is no separation.

I detected this issue on some private setups I have where I enforce more separation.

For example if you wish, we could compile Ltac2 without -R theories Coq and with -noinit, similarly for the stdlib.

@ejgallego ejgallego mentioned this pull request Dec 7, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

@ejgallego ejgallego ejgallego left review comments

Assignees

@ppedrot ppedrot

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@SkySkimmer @ppedrot @ejgallego