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

add 8.19.dev core-dev packages #2853

Merged
merged 1 commit into from
Dec 7, 2023
Merged

Conversation

palmskog
Copy link
Collaborator

@palmskog palmskog commented Dec 7, 2023

ci-skip: coq-core.8.19.dev coq-stdlib.8.19.dev coqide-server.8.19.dev

@palmskog
Copy link
Collaborator Author

palmskog commented Dec 7, 2023

@SkySkimmer do all 8.19 packages really depend on odoc, or is this just Dune-generated boilerplate?

@SkySkimmer
Copy link
Contributor

They do, with-doc does build @doc which is odoc

@SkySkimmer
Copy link
Contributor

(I think)
cc @ejgallego

@palmskog
Copy link
Collaborator Author

palmskog commented Dec 7, 2023

But the 8.18 packages also had build @doc, but no dependency on odoc. So I guess the question for @ejgallego is if something changed under the hood for 8.19 w.r.t. Dune+documentation.

@ejgallego
Copy link
Member

I guess that was a bug in the 8.18 packages?

The doc target requires odoc.

@palmskog
Copy link
Collaborator Author

palmskog commented Dec 7, 2023

@ejgallego @SkySkimmer the coq package's build @runtest did not work properly without adding ounit2 as a dependency. Is this something I should report or fix upstream?

@palmskog palmskog merged commit 45f142c into coq:master Dec 7, 2023
3 checks passed
@palmskog palmskog deleted the add-8.19.dev branch December 7, 2023 23:48
@ejgallego
Copy link
Member

Is this something I should report or fix upstream?

@palmskog , I would have assumed that ounit2 would have been pulled transitively from the coq-core dep, but I'm unsure what the opam semantics are. What opam version did you test this with?

@palmskog
Copy link
Collaborator Author

palmskog commented Dec 8, 2023

@ejgallego it may be easiest if you take a look at one failing pipeline/job: https://gitlab.com/coq/opam/-/jobs/5707150494

All I know is that when I added the ounit2 dep, CI passed. It may have to do with transitive with-test deps not being installed.

@ejgallego
Copy link
Member

Indeed, the problem is that the transitive deps are not installed. As of now we run the test-suite in the coq package, but at some point we could refine it and attach tests to particular packages.

I guess indeed opam expects the deps to be complete, so I suggest we add the missing dep to Coq's for now.

@SkySkimmer
Copy link
Contributor

The ounit dep should be on coq not coq-core yes

@SkySkimmer
Copy link
Contributor

coq/coq#18389

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants