Karl Palmskog (Oct 01 2022 at 12:05): Karl Palmskog (Oct 01 2022 at 12:05):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:
"ocamlfind" {build}"conf-findutils" {build}"conf-adwaita-icon-theme"[ "./configure" ... ] clause before dune is actually used to build.Can someone from core give advice on how we can resolve these discrepancies?
Théo Zimmermann (Oct 01 2022 at 12:11):Most likely these things are there for a good reason and a PR could be made to add them to the in-repo coqide.opam file.
Karl Palmskog (Oct 01 2022 at 12:20):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 ocamlfind anymore?)
Théo Zimmermann (Oct 01 2022 at 12:24):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.
Théo Zimmermann (Oct 01 2022 at 12:25):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).
Paolo Giarrusso (Oct 01 2022 at 15:47):FWIW, coqide depends on conf-adwaita-icon-theme because it needs the icons, and on conf-findutils because upstream OPAM CI breaks otherwise
Paolo Giarrusso (Oct 01 2022 at 15:49):@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
Paolo Giarrusso (Oct 01 2022 at 15:50):(but the .opam files do not match generation output today, at best this avoids adding differences)
Paolo Giarrusso (Oct 01 2022 at 15:52):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
Emilio Jesús Gallego Arias (Oct 01 2022 at 18:10):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
Emilio Jesús Gallego Arias (Oct 01 2022 at 18:10):So all that what we need is someone to do the job, at some point there was a PR open
Emilio Jesús Gallego Arias (Oct 01 2022 at 18:11):As far as I know modulo the adawaita icon
Emilio Jesús Gallego Arias (Oct 01 2022 at 18:11):the right coqide package was done in coq-opam
Emilio Jesús Gallego Arias (Oct 01 2022 at 18:11):it should not call configure
Emilio Jesús Gallego Arias (Oct 01 2022 at 18:12):only thing coqide uses configure is to detect the platform, that is done automatically and indeed moved to its own configure for 8.17
Paolo Giarrusso (Oct 01 2022 at 18:26):@Emilio Jesús Gallego Arias can dune generate the call to configure, or can you make configure unnecessary?
Paolo Giarrusso (Oct 01 2022 at 18:27):there might have been other differences last I tested auto-generation, but that's the big one I remember
Emilio Jesús Gallego Arias (Oct 01 2022 at 22:55):dune will call the config program, there are no options to pass from the user
Emilio Jesús Gallego Arias (Oct 01 2022 at 22:56):for CoqIDE I mean
Emilio Jesús Gallego Arias (Oct 01 2022 at 22:56):for Coq we have reduced a lot
Emilio Jesús Gallego Arias (Oct 01 2022 at 22:56):that's IMO a good thing
Emilio Jesús Gallego Arias (Oct 01 2022 at 22:56):but configure is starting to look very lean
Last updated: Nov 29 2023 at 18:01 UTC