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: make argument order of fold combinators same as OCaml #18197

Merged
merged 1 commit into from Nov 16, 2023
Merged

Ltac2: make argument order of fold combinators same as OCaml #18197

merged 1 commit into from Nov 16, 2023

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Oct 23, 2023 •
edited

@SkySkimmer SkySkimmer added needs: changelog entry This should be documented in doc/changelog. request: full CI Use this label when you want your next push to trigger a full CI. labels Oct 23, 2023
@SkySkimmer SkySkimmer requested a review from a team as a code owner October 23, 2023 13:12
@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 Oct 23, 2023
@SkySkimmer SkySkimmer added needs: overlay This is breaking external developments we track in CI. needs: test-suite update Test case should be added to / updated in the test-suite. labels Oct 24, 2023
SkySkimmer added a commit to SkySkimmer/coqutil that referenced this pull request Oct 26, 2023
@SkySkimmer
Adapt to coq/coq#18197 (List and Array fold argument order change)
dc7dc82 
Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)
SkySkimmer added a commit to SkySkimmer/rewriter that referenced this pull request Oct 26, 2023
@SkySkimmer
Adapt to coq/coq#18197 (List and Array fold argument order change)
afce8ed 
Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)
SkySkimmer added a commit to SkySkimmer/neural-net-coq-interp that referenced this pull request Oct 26, 2023
@SkySkimmer
Adapt to coq/coq#18197 (List and Array fold argument order change)
c319b7c 
Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)
@SkySkimmer SkySkimmer added needs: overlay This is breaking external developments we track in CI. and removed needs: overlay This is breaking external developments we track in CI. needs: test-suite update Test case should be added to / updated in the test-suite. labels Oct 26, 2023
SkySkimmer added a commit to SkySkimmer/neural-net-coq-interp that referenced this pull request Oct 26, 2023
@SkySkimmer
Adapt to coq/coq#18197 (List and Array fold argument order change)
7cfac3f 
Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)
@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 Oct 26, 2023
@samuelgruetter
Copy link
Contributor

In this commit, @JasonGross wrote

We generally favor Coq argument ordering when there is a conflict between Coq and OCaml.

Currently, Ltac2 fold_left/right have the same argument order as the Gallina fold_left/right in Coq.Lists.List, but disagree with OCaml's argument order. This PR makes Ltac2 agree with with OCaml, but disagree with Gallina, so the number of inconsistencies remains constant 😉
But I personally prefer the OCaml argument order, so overall, this PR slightly improves usability for me.
And maybe the plan is to change the Gallina argument order in the future as well?

@JasonGross
Copy link
Member

I'm happy to have Ltac2 swap to preferring the OCaml ordering, especially if there's a plan to update gallina as well (though this seems hard to do in a way that allows projects to build with multiple versions of Coq)

JasonGross pushed a commit to SkySkimmer/neural-net-coq-interp that referenced this pull request Oct 30, 2023
@SkySkimmer @JasonGross
Adapt to coq/coq#18197 (List and Array fold argument order change)
0c4350a 
Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)
JasonGross pushed a commit to SkySkimmer/neural-net-coq-interp that referenced this pull request Nov 2, 2023
@SkySkimmer @JasonGross
Adapt to coq/coq#18197 (List and Array fold argument order change)
3e4d66a 
Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)
JasonGross pushed a commit to mit-plv/rewriter that referenced this pull request Nov 2, 2023
@SkySkimmer
Adapt to coq/coq#18197 (List and Array fold argument order change) (#120
5b13cd7 
)

Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)
JasonGross pushed a commit to mit-plv/coqutil that referenced this pull request Nov 2, 2023
@SkySkimmer
Adapt to coq/coq#18197 (List and Array fold argument order change) (#100
7eb2160 
)

Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)
JasonGross pushed a commit to SkySkimmer/neural-net-coq-interp that referenced this pull request Nov 6, 2023
@SkySkimmer @JasonGross
Adapt to coq/coq#18197 (List and Array fold argument order change)
765977e 
Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)
JasonGross pushed a commit to SkySkimmer/neural-net-coq-interp that referenced this pull request Nov 6, 2023
@SkySkimmer @JasonGross
Adapt to coq/coq#18197 (List and Array fold argument order change)
b9c698b 
Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)
JasonGross pushed a commit to JasonGross/neural-net-coq-interp that referenced this pull request Nov 6, 2023
@SkySkimmer
Adapt to coq/coq#18197 (List and Array fold argument order change) (#6)
ac253f4 
Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)
@SkySkimmer
Copy link
Contributor Author

@coqbot run full ci

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

@coqbot run full ci
(pipeline is currently pending, remerge master to be compatible with just now merged overlays)

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 15, 2023
@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 Nov 15, 2023
MSoegtropIMC
MSoegtropIMC approved these changes Nov 15, 2023
View reviewed changes
Copy link
Contributor

@MSoegtropIMC MSoegtropIMC left a comment

Choose a reason for hiding this comment

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

I double checked the 4 functions against the OCaml header docs at

https://v2.ocaml.org/api/List.html
https://v2.ocaml.org/api/Array.html

Thanks for cleaning up the mess I created!

@MSoegtropIMC
Copy link
Contributor

@samuelgruetter : there was some voting last month at the bottom of issue: #16485.

The Ltac2 libraries I wrote were intended to follow OCaml - I just messed it up somehow.

@ppedrot ppedrot self-assigned this Nov 15, 2023
@ppedrot
Copy link
Member

ppedrot commented Nov 15, 2023

@coqbot run full ci

@MSoegtropIMC
Copy link
Contributor

@SkySkimmer @ppedrot : Can I help with fixing CI? I looked at the failures but they all seem to be timeouts / disk size issues.

@ppedrot
Copy link
Member

ppedrot commented Nov 16, 2023

All these failures should be spurious, I ran a CI just in case.

@ppedrot
Copy link
Member

ppedrot commented Nov 16, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit edd3bad into coq:master Nov 16, 2023
12 of 14 checks passed
@SkySkimmer SkySkimmer deleted the ltac2-fold-order branch November 17, 2023 13:30
SkySkimmer added a commit to SkySkimmer/coq that referenced this pull request Feb 22, 2024
@SkySkimmer
Ltac2.List.fold_(left/right)2: fix argument order to be same as OCaml
e2d0761 
Missed in coq#18197
@SkySkimmer SkySkimmer mentioned this pull request Feb 22, 2024
Merged
SkySkimmer added a commit to SkySkimmer/coq that referenced this pull request Feb 22, 2024
@SkySkimmer
Ltac2.List.fold_(left/right)2: fix argument order to be same as OCaml
964e2f3 
Missed in coq#18197
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

@MSoegtropIMC MSoegtropIMC MSoegtropIMC approved these changes

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.

Ltac2 library: list and array fold functions don't match OCaml
5 participants
@SkySkimmer @samuelgruetter @JasonGross @MSoegtropIMC @ppedrot