Open MSoegtropIMC opened 2 months ago
Doesn't seem to work
The issue is that there are some coq opam packages which do require dune >= 3.14. Also in Coq Platform I had to upgrade to dune 3.15.3 cause of issues.
IMHO it should be discussed with the dune team if the way the CI is setup will permanently be incompatible with dune - in this case the only way is to change the CI setup - or if dune will be made compatible in the near future.
For a few months I can use patched opam files in Coq Platform for the coq packages, but not forever.
cc @rgrinberg
FYI @rgrinberg, the issue at stake would be: https://github.com/ocaml/dune/pull/9895#issuecomment-2090421992
Not sure I really understand the issue, but you might be able to fix if you disable substitution altogether with (subst disabled) in the dune-project file. To help out more, I will need a ticket with a more complete description of the problem.
Unfortunately, Dune >= 3.14 (which includes 3.15.3) is incompatible with the way our continuous integration is setup, as you can see from the failures. (My hypothesis is that
dune subst
does not support the fact that the home directory contains anopam
component.)Polluting the
opam
files ofcoq-core
with the upper bound ondune
is certainly crude, but it gets the continuous integration running. It would be better to somehow enforce the upper bound inscripts/opam-coq-setup-root
, for instance. But nobody investigated how to do that properly.