Stream: Coq devs & plugin devs

Topic: in-repo coqide.dev vs opam archive


view this post on Zulip 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:

Can someone from core give advice on how we can resolve these discrepancies?

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 01 2022 at 15:50):

(but the .opam files do not match generation output today, at best this avoids adding differences)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 18:11):

As far as I know modulo the adawaita icon

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 18:11):

the right coqide package was done in coq-opam

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 18:11):

it should not call configure

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 22:56):

for CoqIDE I mean

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 22:56):

for Coq we have reduced a lot

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 22:56):

that's IMO a good thing

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2022 at 22:56):

but configure is starting to look very lean


Last updated: Feb 05 2023 at 19:29 UTC