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: Take some small APIs from rewriter (fst/snd) #18370

Merged
merged 1 commit into from Jan 30, 2024
Merged

Ltac2: Take some small APIs from rewriter (fst/snd) #18370

merged 1 commit into from Jan 30, 2024

Conversation

SkySkimmer
Copy link
Contributor

No description provided.

@SkySkimmer SkySkimmer requested a review from a team as a code owner December 5, 2023 14:58
@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 Dec 5, 2023
ppedrot
ppedrot reviewed Dec 5, 2023
View reviewed changes
user-contrib/Ltac2/Char.v Outdated
@@ -16,3 +16,13 @@ Ltac2 @external to_int : char -> int := "coq-core.plugins.ltac2" "char_to_int".

Ltac2 equal (x : char) (y : char) : bool := Int.equal (to_int x) (to_int y).
Ltac2 compare (x : char) (y : char) : int := Int.compare (to_int x) (to_int y).

(** Special characters *)
Ltac2 null () : char := Char.of_int 0.
Copy link
Member

Choose a reason for hiding this comment

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

Having these as thunks is a bad idea, we should probably have char literals, or some hand-defined externals.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

ok let's keep just fst/snd

@SkySkimmer SkySkimmer changed the title Ltac2: Take some small APIs from rewriter (fst/snd, Special chars) Ltac2: Take some small APIs from rewriter (fst/snd) Jan 22, 2024
@ppedrot ppedrot self-assigned this Jan 22, 2024
@ppedrot ppedrot added this to the 8.20+rc1 milestone Jan 22, 2024
@ppedrot
Copy link
Member

ppedrot commented Jan 22, 2024

Maybe a changelog is in order?

@ppedrot
Copy link
Member

ppedrot commented Jan 22, 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 Jan 22, 2024
@ppedrot ppedrot added needs: changelog entry This should be documented in doc/changelog. kind: feature New user-facing feature request or implementation. labels Jan 24, 2024
@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 Jan 24, 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 Jan 24, 2024
@SkySkimmer SkySkimmer removed the needs: changelog entry This should be documented in doc/changelog. label Jan 24, 2024
@ppedrot ppedrot added the needs: fixing The proposed code change is broken. label Jan 28, 2024
@ppedrot
Copy link
Member

ppedrot commented Jan 28, 2024

@SkySkimmer Test-suite is broken it seems.

@SkySkimmer SkySkimmer added needs: test-suite update Test case should be added to / updated in the test-suite. and removed needs: fixing The proposed code change is broken. labels Jan 28, 2024
@JasonGross
Copy link
Member

The output file needs updating

logs/output/ltac2_printabout.v.log
==========> TESTING output/ltac2_printabout.v <==========
--- output/ltac2_printabout.out	2024-01-24 19:09:24.139999973 +0000
+++ output/ltac2_printabout.out.real	2024-01-24 19:25:33.176666633 +0000
@@ -1,3 +1,5 @@
+fst : 'a * 'b -> 'a
+snd : 'b * 'a -> 'a
 type : constr -> constr
 Ltac2 type : constr -> constr
       type := @external "coq-core.plugins.ltac2" "constr_type"
0m0.000000s 0m0.000000s
0m0.080000s 0m0.080000s
==========> FAILURE <==========
    output/ltac2_printabout.v...Error! (unexpected output)

FAILURES
    output/ltac2_printabout.v...Error! (unexpected output)
make[1]: *** [Makefile:288: report] Error 1

@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: test-suite update Test case should be added to / updated in the test-suite. labels Jan 29, 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 Jan 29, 2024
@ppedrot
Copy link
Member

ppedrot commented Jan 30, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 18b537d into coq:master Jan 30, 2024
5 of 7 checks passed
@SkySkimmer SkySkimmer deleted the ltac2-apis branch January 31, 2024 13:28
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

Assignees

@ppedrot ppedrot

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

Successfully merging this pull request may close these issues.

None yet
3 participants
@SkySkimmer @ppedrot @JasonGross