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?
as --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.
@Michael Soegtrop
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: Oct 13 2024 at 01:02 UTC