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

Extensions to the Ltac2 standard library #18095

Merged
merged 10 commits into from Oct 14, 2023
Merged

Extensions to the Ltac2 standard library #18095

merged 10 commits into from Oct 14, 2023

Conversation

rlepigre
Copy link
Contributor

@rlepigre rlepigre commented Sep 29, 2023 •
edited by SkySkimmer

Fix #10112.

  • Added changelog.

@rlepigre rlepigre requested a review from a team as a code owner September 29, 2023 07:23
@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 29, 2023
@SkySkimmer SkySkimmer requested a review from a team September 29, 2023 13:25
@SkySkimmer SkySkimmer self-assigned this Sep 29, 2023
@rlepigre rlepigre force-pushed the br/ltac2-extensions branch 4 times, most recently from e7adb0f to 7b0d128 Compare October 2, 2023 16:30
@rlepigre rlepigre force-pushed the br/ltac2-extensions branch 3 times, most recently from 1dd33cb to ee593ed Compare October 4, 2023 15:44
JasonGross
JasonGross reviewed Oct 4, 2023
View reviewed changes
plugins/ltac2/tac2core.ml Outdated Show resolved Hide resolved
plugins/ltac2/tac2core.ml Outdated Show resolved Hide resolved
user-contrib/Ltac2/Control.v
@@ -26,6 +26,9 @@ Ltac2 @ external extend : (unit -> unit) list -> (unit -> unit) -> (unit -> unit
Ltac2 @ external enter : (unit -> unit) -> unit := "coq-core.plugins.ltac2" "enter".
Ltac2 @ external case : (unit -> 'a) -> ('a * (exn -> 'a)) result := "coq-core.plugins.ltac2" "case".

Ltac2 once_plus (run : unit -> 'a) (handle : exn -> 'a) : 'a :=
Copy link
Member

Choose a reason for hiding this comment

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

Maybe this should be called first_bt and take a list of handles as its second argument, in analogy to the the first tactical? Or would that make naming less coherent rather than more?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

To us this function is just a short-hand for its definition, as we noticed we were wrapping Control.plus in a Control.once most of the time, so calling it once_plus seemed to be a natural name.

Actually, I'm not sure I understand what first_bt would do. What would its implementation be?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

@JasonGross any more thoughts on that?

user-contrib/Ltac2/Lazy.v Outdated Show resolved Hide resolved
user-contrib/Ltac2/Lazy.v Outdated Show resolved Hide resolved
user-contrib/Ltac2/List.v Show resolved Hide resolved
rlepigre added a commit to rlepigre/coq that referenced this pull request Oct 12, 2023
@rlepigre
Add changelog entry for coq#18095.
abe2f88
@SkySkimmer
Copy link
Contributor

Should Require for the new files be added to Ltac2.v? so that eg

Require Import Ltac2.Ltac2.

Ltac2 foo x := Ref.ref x.

works without an additional Require Ltac2.Ref

@SkySkimmer SkySkimmer removed the needs: changelog entry This should be documented in doc/changelog. label Oct 13, 2023
SkySkimmer
SkySkimmer approved these changes Oct 13, 2023
View reviewed changes
Copy link
Contributor

@SkySkimmer SkySkimmer left a comment

Choose a reason for hiding this comment

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

I think this is ready, let's have a full CI then I expect I'll merge
@coqbot run full ci

@SkySkimmer
Copy link
Contributor

@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 Oct 13, 2023
@SkySkimmer SkySkimmer mentioned this pull request Oct 13, 2023
Closed
@rlepigre
Copy link
Contributor Author

CI failures are spurious, right @SkySkimmer?

@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 49fce3a into coq:master Oct 14, 2023
8 of 10 checks passed
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 16, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#18095: Extensions to the Ltac2 standard library
95b8be4 
Reviewed-by: SkySkimmer
Ack-by: Janno
Ack-by: JasonGross
Ack-by: ppedrot
Ack-by: jfehrle
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 16, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#18095: Extensions to the Ltac2 standard library
1b99d31 
Reviewed-by: SkySkimmer
Ack-by: Janno
Ack-by: JasonGross
Ack-by: ppedrot
Ack-by: jfehrle
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre added a commit to rlepigre/coq that referenced this pull request Oct 16, 2023
@rlepigre
Fixup badly resolved conflict when cherry-picking coq#18095.
bf0ce73
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 25, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#18095: Extensions to the Ltac2 standard library
d4d1bf0 
Reviewed-by: SkySkimmer
Ack-by: Janno
Ack-by: JasonGross
Ack-by: ppedrot
Ack-by: jfehrle
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre added a commit to rlepigre/coq that referenced this pull request Oct 25, 2023
@rlepigre
Fixup badly resolved conflict when cherry-picking coq#18095.
5a15169
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 30, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#18095: Extensions to the Ltac2 standard library
f55c63a 
Reviewed-by: SkySkimmer
Ack-by: Janno
Ack-by: JasonGross
Ack-by: ppedrot
Ack-by: jfehrle
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre added a commit to rlepigre/coq that referenced this pull request Oct 30, 2023
@rlepigre
Fixup badly resolved conflict when cherry-picking coq#18095.
97a98d7
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Janno Janno Janno left review comments

@JasonGross JasonGross JasonGross left review comments

@ppedrot ppedrot ppedrot left review comments

@jfehrle jfehrle jfehrle left review comments

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, 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.

It should be possible to print a backtrace from Control.case / Control.plus
6 participants
@rlepigre @SkySkimmer @Janno @JasonGross @ppedrot @jfehrle