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

[coqdep] Be more deterministic w.r.t. the plugin loading mode #16658

Merged
merged 1 commit into from
Oct 17, 2022
Merged

[coqdep] Be more deterministic w.r.t. the plugin loading mode #16658

merged 1 commit into from
Oct 17, 2022

Conversation

ejgallego
Copy link
Member

If the legacy mode is set, we don't even attempt to use findlib to resolve anything, we also won't emit a META dependency, even if this dependency is in scope.

This is morally the right thing to do, should reduce non-determinism, and helps a bit to isolate the legacy code more.

This should help with problems such as
ocaml/dune#5833

@ejgallego
[coqdep] Be more deterministic w.r.t. the plugin loading mode
ce9b6dd 
If the legacy mode is set, we don't even attempt to use findlib to
resolve anything, we also won't emit a META dependency, even if this
dependency is in scope.

This is morally the right thing to do, should reduce non-determinism,
and helps a bit to isolate the legacy code more.

This should help with problems such as
ocaml/dune#5833
@ejgallego ejgallego requested a review from a team as a code owner October 13, 2022 16:25
@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 13, 2022
@ejgallego ejgallego added this to the 8.16.1 milestone Oct 13, 2022
@ejgallego ejgallego added the part: coqdep The coqdep binary for resolving dependencies amongst coq .v files. label Oct 13, 2022
@ejgallego ejgallego mentioned this pull request Oct 13, 2022
Open
@Alizter Alizter added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 13, 2022
@rlepigre
Copy link
Contributor

@ejgallego I wanted to try out this change, but for my setup I can (for now) only use the v8.16 branch extended with a few patches. Unfortunately, since there were quite a few changes to coqdep since then, I can't just cherry-pick your commit. I had a look to see if I could redo your changes in v8.16 to try them out, but it is non-trivial (names changed) and I don't want to mess things up. If this gets merged in 8.16.1, does that mean all the coqdep changes will also get in?

@Alizter
Copy link
Contributor

Alizter commented Oct 14, 2022 •
edited
Loading

@rlepigre That's a good point, I think this patch will need to be backported separately. AFAIK most of the coqdep changes were refactorings rather than behavioral changes.

@rlepigre
Copy link
Contributor

rlepigre commented Oct 14, 2022 •
edited
Loading

@rlepigre That's a good point, I think this patch will need to be backported separately. AFAIK most of the coqdep changes were refactorings rather than behavioral changes.

After giving it another look, it is indeed not too hard to backport. I'll check if that solves my problem. Thanks!

@ejgallego
Copy link
Member Author

@coqbot run full ci

@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Oct 14, 2022
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 14, 2022
@ejgallego
Backport of coq#16658 for v8.16.
d187b93 
[coqdep] Be more deterministic w.r.t. the plugin loading mode

If the legacy mode is set, we don't even attempt to use findlib to
resolve anything, we also won't emit a META dependency, even if this
dependency is in scope.

This is morally the right thing to do, should reduce non-determinism,
and helps a bit to isolate the legacy code more.

This should help with problems such as
ocaml/dune#5833

Co-authored-by: Emilio Jesús Gallego Arias <[email protected]>
@rlepigre rlepigre mentioned this pull request Oct 14, 2022
Merged
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 14, 2022
@ejgallego
Backport of coq#16658 for v8.16.
5f57359 
[coqdep] Be more deterministic w.r.t. the plugin loading mode

If the legacy mode is set, we don't even attempt to use findlib to
resolve anything, we also won't emit a META dependency, even if this
dependency is in scope.

This is morally the right thing to do, should reduce non-determinism,
and helps a bit to isolate the legacy code more.

This should help with problems such as
ocaml/dune#5833

Co-authored-by: Emilio Jesús Gallego Arias <[email protected]>
@ejgallego
Copy link
Member Author

@coqbot run full ci

@ejgallego
Copy link
Member Author

CI looks good, color failure due to native compiler problem, vst got killed.

@Alizter Alizter self-assigned this Oct 17, 2022
@ejgallego ejgallego mentioned this pull request Oct 17, 2022
Closed
@Alizter
Copy link
Contributor

Alizter commented Oct 17, 2022

@coqbot merge now

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Oct 17, 2022

@Alizter: You cannot merge this PR because:

  • There is no kind: label.

@Alizter Alizter added the kind: infrastructure CI, build tools, development tools. label Oct 17, 2022
@Alizter
Copy link
Contributor

Alizter commented Oct 17, 2022

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 1f37b23 into coq:master Oct 17, 2022
@ejgallego ejgallego deleted the coqdep+dont_meta_on_legacy branch October 18, 2022 08:47
@ppedrot ppedrot modified the milestones: 8.16.1, 8.17+rc1 Nov 17, 2022
ppedrot added a commit that referenced this pull request Nov 17, 2022
@ppedrot
Merge PR #16664: [coqdep] backport of #16658 for Coq 8.16.
bd05166 
Reviewed-by: ppedrot
@ejgallego ejgallego mentioned this pull request Sep 20, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Alizter Alizter Alizter approved these changes

Assignees

@Alizter Alizter

Labels
kind: infrastructure CI, build tools, development tools. part: coqdep The coqdep binary for resolving dependencies amongst coq .v files.
Projects
None yet
Milestone
8.17+rc1
Development

Successfully merging this pull request may close these issues.
4 participants
@ejgallego @rlepigre @Alizter @ppedrot