Until 8.13, ./configure -local would give me a local installation of coq, for which I had a /bin/ folder that I could include in my $PATH for local use (without the need for an opam switch).
Now the -local flag is gone. I can provide a custom folder to ./configure -prefix, but then it seems that I must provide -coqlib whenever I invoke coqc.
Is there a way to have my bin/coqc automatically lookup the library that was built with it?
Thanks
configure -profile devel
binaries are in _build_vo/bin instead of bin/ IIRC
Thanks! But how could I guess from the documentation?
-profile <profile> Sets a bunch of flags. Supported profiles:
devel = -annot -bin-annot -warn-error yes
says nothing about the library path and its resolution by coqc.
What @SkySkimmer answered is tailored to developers, not to users, so it’s documented in the developer documentation (and BTW, the explanation that you quote should probably have been updated).
Basically, your use case (producing a local installation) is not supported anymore. But I’m a bit surprised that the alternative solution that you tried (providing a custom folder to ./configure -prefix) did not work because of this -coqlib issue that you mention. Maybe that’s something worth digging into and possibly writing a bug report about…
Basically, your use case (producing a local installation) is not supported anymore.
It is though, you just have to use devel
We could put -local back easily, not sure why it was removed
What I meant is that devel is targeting developers and that we could remove it at any time, since it is not meant for users…
cc @ejgallego regarding the reasons of the removal of -local.
-local was removed because used a different layout which was a PITA to use.
We do support local installation for now, in addition to -profile devel, a clean build make -f Makefile.dune world will also produce a usable layout in _build/install [as of today]
Tho, if you are not developing Coq itself, I think it is a better idea to use stow or local opam swichtes.