So right now we have some possibly-significant discrepancies between the in-repo
coqide.dev package and the
coqide.devpackage in the opam archive.
Specifically the opam archive package has these "extra" dependencies:
[ "./configure" ... ]clause before
duneis actually used to build.
Can someone from core give advice on how we can resolve these discrepancies?
Most likely these things are there for a good reason and a PR could be made to add them to the in-repo
OK, I can just do a best effort Coq PR to add what I think is missing. Unless @Emilio Jesús Gallego Arias has some other idea (e.g., does the CoqIDE build even use
Well, unless Dune has now a replacement mechanism (and that would depend on the version of Dune I guess), then yes of course, ocamlfind is need to locate its dependencies.
And I guess this is a case where if you don't put it, you won't see any consequence because that's a transitive dependency already (and thus it is in scope).
FWIW, coqide depends on
conf-adwaita-icon-theme because it needs the icons, and on
conf-findutils because upstream OPAM CI breaks otherwise
@Karl Palmskog _maybe_ you'd want to add the deps in
dune-project as well — you can uncomment
; (generate_opam_files true) in
dune-project to check that worked
.opam files do not match generation output today, at best this avoids adding differences)
Maybe it makes sense to give up on
generate_opam_files and maintaining the duplication by hand — I don't know if those dependencies are used for anything. At least the comment next to
generate_opam_files seems outdated
We are not using
generate_opam_files because of a bug, but I think that is already solved in the minimum Dune version we support
So all that what we need is someone to do the job, at some point there was a PR open
As far as I know modulo the adawaita icon
the right coqide package was done in coq-opam
it should not call configure
only thing coqide uses configure is to detect the platform, that is done automatically and indeed moved to its own configure for 8.17
@Emilio Jesús Gallego Arias can dune generate the call to
configure, or can you make
there might have been other differences last I tested auto-generation, but that's the big one I remember
dune will call the config program, there are no options to pass from the user
for CoqIDE I mean
for Coq we have reduced a lot
that's IMO a good thing
but configure is starting to look very lean
Last updated: Nov 29 2023 at 18:01 UTC