Gaëtan Gilbert (Aug 18 2021 at 09:55): 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
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.
Pierre Roux (Aug 19 2021 at 08:43):Isn't it still needed for coq-native?
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.
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
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
Pierre Roux (Aug 19 2021 at 11:17):Ok, my bad, thanks for the explanation.
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.
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.
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]
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: Dec 07 2023 at 06:38 UTC