Stream: Coq Platform devs & users

Topic: Platform changing switch by default

view this post on Zulip Paolo Giarrusso (Jan 29 2022 at 20:01):

Just installed the platform with ./ -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?

view this post on Zulip Paolo Giarrusso (Jan 29 2022 at 20:02):

as --switch=k might hint, I did interrupt and resume installation (with Ctrl-C).

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jan 29 2022 at 20:45):

@Michael Soegtrop

view this post on Zulip 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.

view this post on Zulip 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 ]

view this post on Zulip 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 ( - 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.

view this post on Zulip 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. is still untested, it just has what I spotted.

Last updated: Jan 30 2023 at 12:03 UTC