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
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.
Isn't it still needed for coq-native?
Why would it? I don't even think that
-native-compiler is one of the options that has an interactive equivalent.
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
by interactive I mean the way it asks for install paths if you don't use -prefix
Ok, my bad, thanks for the explanation.
Indeed it is not so important IMHO, feel free to push atop of #14189 to remove it if you feel like it.
Tho, I hope that work ongoing there will make having the interactive part not complex at all.
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]
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