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

fix(coq): pass correct flags to coqdep when building boot libs #7942

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Jun 12, 2023

fix #7909

I've tested the reproduction in #7909 and it works. I will not add a test for this.

  • changelog

@Alizter Alizter requested a review from ejgallego June 12, 2023 10:07
@Alizter Alizter added the coq label Jun 12, 2023
@Alizter Alizter mentioned this pull request Jun 12, 2023
7 tasks
@Alizter Alizter force-pushed the ps/branch/fix_coq___pass_correct_flags_to_coqdep_when_building_boot_libs branch from 8ba3a37 to 3c4192d Compare June 12, 2023 10:22
@ejgallego ejgallego self-assigned this Jun 13, 2023
@ejgallego
Copy link
Collaborator

ejgallego commented Jun 13, 2023

Thanks a lot @Alizter , will review (and hopefully merge) ASAP.

@ejgallego
Copy link
Collaborator

I will not add a test for this.

Why not?

Patch seems broken? Didn't look closely at the test cases but maybe this is due to the logic being a bit more subtle now.

Even in earlier versions of the build language, we do detect the boot library that is in $coqlib, thus the condition needs to be refined for langs < 0.8 as to be "we have a boot library, and its path is in the workspace"

Does it make sense?

@Alizter
Copy link
Collaborator Author

Alizter commented Jun 14, 2023

@ejgallego feel free to takeover. It seemed to work for me.

@ejgallego
Copy link
Collaborator

@ejgallego feel free to takeover. It seemed to work for me.

I see CI / Coq test suite is broken, isn't it?

@Alizter
Copy link
Collaborator Author

Alizter commented Jun 14, 2023

@ejgallego only updating thr new flags.

@Alizter
Copy link
Collaborator Author

Alizter commented Jun 25, 2023

If this is the right fix, please resurrect.

@Alizter Alizter closed this Jun 25, 2023
@ejgallego
Copy link
Collaborator

@ejgallego only updating the new flags.

I see a truly broken test-case and a few suspicious things, don't you?

It seems that combining -boot (>= 0.8) and theories that doesn't ( < 0.8) could turn out the be quite tricky, see for example the discussion at https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users/topic/Adding.20transitive.20deps.20into.20theories

ejgallego added a commit to ejgallego/dune that referenced this pull request Dec 1, 2023
Indeed the logic is a bit more complex than what we had. Current setup
should work well now.

Fixes ocaml#7909 , replaces ocaml#7942

This also reverts most of d92cb2e

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ejgallego added a commit to ejgallego/dune that referenced this pull request Dec 1, 2023
Indeed the logic is a bit more complex than what we had. Current setup
should work well now.

Fixes ocaml#7909 , replaces ocaml#7942

This also reverts most of d92cb2e

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ejgallego added a commit to ejgallego/dune that referenced this pull request Dec 1, 2023
Indeed the logic is a bit more complex than what we had. Current setup
should work well now.

Fixes ocaml#7909 , replaces ocaml#7942

This also reverts most of d92cb2e

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ejgallego added a commit to ejgallego/dune that referenced this pull request Dec 1, 2023
Indeed the logic is a bit more complex than what we had. Current setup
should work well now.

Fixes ocaml#7909 , replaces ocaml#7942

This also reverts most of d92cb2e

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ejgallego added a commit to ejgallego/dune that referenced this pull request Dec 1, 2023
Indeed the logic is a bit more complex than what we had. Current setup
should work well now.

Fixes ocaml#7909 , replaces ocaml#7942

This also reverts most of d92cb2e

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

[coq] Composition with (boot) theories is not working in Dune 3.8
2 participants