Jason Gross (Sep 16 2021 at 16:16): Jason Gross (Sep 16 2021 at 16:16):My launchpad packages broke because ./configure no longer accepts -vmbyteflags "-dllib,-lcoqrun". Is there a replacement? Has this been a no-op that was recently removed? Was this option mistakenly removed?
Ali Caglayan (Sep 17 2021 at 06:43):I suspect it is https://github.com/coq/coq/pull/14189
Ali Caglayan (Sep 17 2021 at 06:44):Now, to the developers it seemed like these were no longer being used (thought I'm not sure about it being a noop). What can be done in the future to make sure we aren't breaking the configure script randomly for others? Is it possible to test launchpad packages?
@Théo Zimmermann Perhaps you have an idea?
cc @Emilio Jesús Gallego Arias
Théo Zimmermann (Sep 17 2021 at 08:46):According to the changelog entry in this PR, this option probably did not control what was actually used when compiling with Dune (since 8.14) and this can be tweaked by patching topbin/dune instead.
Emilio Jesús Gallego Arias (Sep 17 2021 at 11:35):That option is not needed since a long time, likely carried over from the times of OCaml 3.x
Emilio Jesús Gallego Arias (Sep 17 2021 at 11:35):Also many packages where setting stuff wrong, for example opam packages where setting coqdoc to $prefix/doc instead of $prefix/doc/coq etc...
Emilio Jesús Gallego Arias (Sep 17 2021 at 11:36):I think we lack the resources to test too many 3rd party packages, I think our best bet is to make our setup as standard as possible
Emilio Jesús Gallego Arias (Sep 17 2021 at 11:36):so Coq is not different from any other OCaml package
Emilio Jesús Gallego Arias (Sep 17 2021 at 11:37):at some point all the configure options should just be enable / disable the several Coq options, packages should control the rest configuring Dune for their package system
Last updated: Apr 19 2024 at 02:02 UTC