Stream: Coq devs & plugin devs

Topic: interactive configure?


view this post on Zulip Gaëtan Gilbert (Aug 18 2021 at 09:55):

How important is interactive configure? It seems pretty fiddly to use compared to passing values in the command line, and I think we could enable so cleanups if we remove it.
cc @Emilio Jesús Gallego Arias

view this post on Zulip Ali Caglayan (Aug 18 2021 at 22:35):

I think as long as we document that it can be done by passing arguments in the command line, it is worth getting rid of the interactive element. I agree that it complicates the configure script as it stands. If there really is a user need to have an interactive configure script, we can later implement a better designed one.

view this post on Zulip Pierre Roux (Aug 19 2021 at 08:43):

Isn't it still needed for coq-native?

view this post on Zulip Théo Zimmermann (Aug 19 2021 at 08:46):

Why would it? I don't even think that -native-compiler is one of the options that has an interactive equivalent.

view this post on Zulip Pierre Roux (Aug 19 2021 at 09:12):

I may have misunderstood but last time I asked how to build with native-compute, Emilio told me the only solution was still to explicitly call ./configure -native-compiler yes

view this post on Zulip Gaëtan Gilbert (Aug 19 2021 at 09:17):

by interactive I mean the way it asks for install paths if you don't use -prefix

view this post on Zulip Pierre Roux (Aug 19 2021 at 11:17):

Ok, my bad, thanks for the explanation.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 25 2021 at 11:06):

Indeed it is not so important IMHO, feel free to push atop of #14189 to remove it if you feel like it.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 25 2021 at 11:06):

Tho, I hope that work ongoing there will make having the interactive part not complex at all.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 25 2021 at 11:58):

I had another look at the current logic and it is indeed super weird, tho I think I have fixed the 8.14 problems [I hope]

view this post on Zulip Emilio Jesús Gallego Arias (Aug 25 2021 at 12:23):

Anyways, I finally understood the problems going on with configure code, #14515 should address all the relevant bits for 8.14, so ping me here for further discussion


Last updated: Oct 16 2021 at 02:03 UTC