Stream: Dune devs & users

Topic: Error when moving from 0.7 to 0.8


view this post on Zulip Yannick Zakowski (Oct 06 2023 at 18:34):

Hey folks,
I just tried to move to coq 0.8 in one of my projects, and I now get an error that I don't understand: I suppose I am missing something that changed, but I'm not sure what.
Here is a minimal example reproducing it: https://gitlab.inria.fr/cash/dune-compilation-0.8
Basically, with a library installed globally on my opam switch, things compile normally with coq 0.7 but fails the import with coq 0.8. Anybody knows what has changed/what I should do?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 18:39):

Hi @Yannick Zakowski , indeed in (lang coq 0.8) you are now required to declare library deps, even if these are globally installed.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 18:39):

Otherwise the setup was not stable by vendoring / installation.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 18:40):

The support is missing an important feature for some, transitive deps, so YMMV.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 18:41):

The reason we deprecated 0.7 was that the old model is unsound: as Dune was obvilivious about the user-contrib stuff, you could update your opam install, and Dune won't rebuild your project.

view this post on Zulip Karl Palmskog (Oct 06 2023 at 18:41):

@Yannick Zakowski see my overview here of why I think the current lack of transitive dep handling makes Dune 0.8 unfeasible in many projects, except for in CI: https://github.com/coq-community/manifesto/issues/87#issuecomment-1619803762

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 18:41):

Surprinsignly we forgot to add a changelog it seems https://dune.readthedocs.io/en/stable/coq.html#coq-language-version

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 18:41):

cc: @Ali Caglayan

view this post on Zulip Karl Palmskog (Oct 06 2023 at 18:43):

that is not to say Dune 0.8 can't work fine in projects with few deps (and transitive dep stuff may be addressed in the future)

view this post on Zulip Yannick Zakowski (Oct 06 2023 at 18:43):

Emilio Jesús Gallego Arias said:

Surprinsignly we forgot to add a changelog it seems https://dune.readthedocs.io/en/stable/coq.html#coq-language-version

Yes the changelog was the first place I looked into but it's indeed bare :) Thanks for the explanation Emilio, I'll read the locating theories section and fix that then, perfect!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 18:47):

Thanks @Yannick Zakowski and sorry for the problem with the docs, I've just opened an issue.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 18:49):

I couldn't see your repos, but beware of what Karl said, for now we don't install in user-contrib the right metadata to compute transitive deps, so depending on your setup you can be fine, or annoyed.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 18:55):

https://github.com/ocaml/dune/issues/8871

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 18:55):

Issue for the missing changelog!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 18:56):

Oh, actually the changelog is there, just that the formatting is pretty unintuitive!


Last updated: May 25 2024 at 21:01 UTC