Stream: Coq devs & plugin devs

Topic: ./configure -local no longer exists, what to use now?

Robbert Krebbers (Jan 25 2022 at 20:50):

Until recently (at least Coq 8.13), I used to build Coq as follows:

cd folder_with_coq_sources
./configure -local
make

And then a Coq binary would appear in the folder_with_coq_sources/bin directory. Since Coq 8.15 the -local option of configure no longer seems to exist. What is the alternative way to make a simple local build?

Thanks!

Gaëtan Gilbert (Jan 25 2022 at 20:56):

-profile devel

Ali Caglayan (Jan 25 2022 at 20:56):

See the doc also https://github.com/coq/coq/blob/master/dev/doc/INSTALL.make.md

Karl Palmskog (Jan 25 2022 at 20:57):

this is clearly a Coq dev question, so moving to that stream

Notification Bot (Jan 25 2022 at 20:57):

This topic was moved here from #Coq users > ./configure -local no longer exists, what to use now? by Karl Palmskog

Théo Zimmermann (Jan 26 2022 at 09:45):

Karl Palmskog said:

this is clearly a Coq dev question, so moving to that stream

Well, the point of the question is precisely that users used to rely on this (even though from the point of view of developers, this was a developer option).

Théo Zimmermann (Jan 26 2022 at 09:46):

This exact same question was also asked here BTW: https://coq.discourse.group/t/how-to-use-a-local-installation-of-coq/1507

Last updated: Sep 15 2024 at 13:02 UTC