Michael Soegtrop (Nov 29 2020 at 16:18): Michael Soegtrop (Nov 29 2020 at 16:18):I wonder if there are ideas how to handle relocation in instellers (Windows, Mac). The current method on windows is to configure with prefix ./, build, configure with a local install folder, install. This is not easy to do with opam.
How about having a build option for coq to pick up a configuration file in the same folder as the executable, where the installer can write the adjusted paths? Any other suggestions?
Enrico Tassi (Nov 29 2020 at 16:22):I like that, but it is not the only problem. AFAIK ocaml itself is not relocatable (hence an opam root is not either, even on unix). On Linux (in the snap experiment) the hack was to use OPAMROOT=/opt/coq-$version/. I think one can do the same on OSX, just with /Applications/coq-$version. On windows I don't know if the ocamlopt we build is "standard" (hence non relocatable) or not.
Michael Soegtrop (Nov 29 2020 at 17:12):Actually the Windows installer does not contain ocaml. In the pre-dune area it didn't make a lot os sense without a posix shell. This might have changes with dune, though. So now it woul dmake more sense to install OCaml. There is an OCaml installer for Windows - one can see what this does. Afair it relies on environment variables which override the compiled configuration.
Last updated: Jun 03 2023 at 03:01 UTC