Paolo Giarrusso (Jan 29 2022 at 20:01): Paolo Giarrusso (Jan 29 2022 at 20:01):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?
Paolo Giarrusso (Jan 29 2022 at 20:02):as --switch=k might hint, I did interrupt and resume installation (with Ctrl-C).
Kartik Singhal (Jan 29 2022 at 20:12):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.
Enrico Tassi (Jan 29 2022 at 20:45):@Michael Soegtrop
Paolo Giarrusso (Jan 29 2022 at 21:03):to be sure it's not a big deal _for me_ but I know many colleagues haven't had time to learn opam switches.
Paolo Giarrusso (Jan 29 2022 at 21:10):[ ... 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 ]
Michael Soegtrop (Jan 30 2022 at 12:39):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.
Paolo Giarrusso (Jan 30 2022 at 21:38):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: Apr 19 2024 at 20:01 UTC