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.

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

Normalize more paths in coqdep to avoid spurious warnings #18165

Merged
merged 1 commit into from Dec 7, 2023

Conversation

rlepigre
Copy link
Contributor

This fixes warnings such as the following:

Warning: ltac_plugin.cmxs already found in [...]/_opam/lib/coq-core/plugins/ltac (discarding [...]/_opam/lib/coq/../coq-core/plugins/ltac/ltac_plugin.cmxs)
         [multiple-matching-files,filesystem,default]

@rlepigre rlepigre requested a review from a team as a code owner October 16, 2023 10:10
@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 16, 2023
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.

Seems fine to me but I'm not a coqdep expert.
@ejgallego @Alizter I think you are more up to date on coqdep, any objections?

@SkySkimmer SkySkimmer self-assigned this Dec 5, 2023
@SkySkimmer SkySkimmer added this to the 8.19+rc1 milestone Dec 5, 2023
@SkySkimmer SkySkimmer added kind: infrastructure CI, build tools, development tools. part: tools Coqdoc, coq_makefile, etc. part: coqdep The coqdep binary for resolving dependencies amongst coq .v files. and removed part: tools Coqdoc, coq_makefile, etc. labels Dec 5, 2023
@Alizter
Copy link
Contributor

Alizter commented Dec 5, 2023

We need to make sure this works correctly on windows. Are we testing Coq platform for windows in the CI?

@ejgallego
Copy link
Member

Thanks @rlepigre , I was actually looking into this the other day; the "right" fix would be to have Coq stopping to set coq/../coq-core as a path. However this change requires a bit of deep surgery on the config code, so I didn't have the cycles to finish it.

[Basically you want to move from the current setup where coqlib is the "root" for a Coq install to a true prefix root, where packages are then located]

Happy to have this in Coq meanwhile.

Regarding testing, I think using ppx_inline_test or use unit tests to check the implementation in all architectures would be the best option.

@ejgallego
Copy link
Member

Seems fine to me but I'm not a coqdep expert. @ejgallego @Alizter I think you are more up to date on coqdep, any objections?

Patch is an improvement over the current situation.

@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 Dec 6, 2023
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 9aa4e1f into coq:master Dec 7, 2023
5 of 7 checks passed
@coqbot-app coqbot-app bot added this to Request 8.19+rc1 inclusion in Coq 8.19 Dec 7, 2023
SkySkimmer added a commit to SkySkimmer/coq that referenced this pull request Dec 7, 2023
@coqbot-app coqbot-app bot moved this from Request 8.19+rc1 inclusion to Shipped in 8.19+rc1 in Coq 8.19 Dec 11, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: infrastructure CI, build tools, development tools. part: coqdep The coqdep binary for resolving dependencies amongst coq .v files.
Projects
Coq 8.19
Shipped in 8.19+rc1
Development

Successfully merging this pull request may close these issues.

None yet

4 participants