Just installed the platform with
./coq_platform_make.sh -extent=f -pick=8.15~beta1 -parallel=p -jobs=16 -vst=n -compcert=n -switch=k; the new switch got made into the default, despite the output suggesting otherwise. I might have seen that earlier as well. Does this happen to anybody else?
--switch=k might hint, I did interrupt and resume installation (with Ctrl-C).
I think it's been happening for a while (at least a few weeks) while I have been testing from the main/master branch on coq platform. I did not mind it and perhaps didn't read the output to notice until you mentioned.
to be sure it's not a big deal _for me_ but I know many colleagues haven't had time to learn opam switches.
[ ... I also wonder how many will be stuck trying to get Spacemacs to pick up the new switch (since it defaults to caching the PATH until it's refreshed explicitly)... but clearly I'm overthinking it ]
I did changhe something there, so that one can run several builds for different picks / switches in parallel, but it should more have the effect that it does not switch. The relevant line is (https://github.com/coq/platform/blob/46b73278b52a3aaaa555bc146acb34a1676be9c5/shell_scripts/install_opam.sh#L192) - I would appreciate if you could play around with it and tell me what works best for you. E.g. one could remove --set-switch.
But as far as I can tell it was always like this, because before the scripts did just call
opam switch <switch> - and this should be global.
Might have happened before, I'm a recent user :-). I'll take the documented behavior as the intended one.
E.g. one could remove --set-switch.
No, that just adds
OPAMSWITCH to the environment inside the script.
opam switch is also global.
But you need
opam switch create --no-switch. https://github.com/coq/platform/pull/209 is still untested, it just has what I spotted.
Last updated: Jun 03 2023 at 04:30 UTC