I've had some really bad issues... e.g. the default solver taking 50 GB of RAM and hanging because there were a lot of minor versions published for the iris development package. Also, it can't seem to handle multiple versions of a package on the same machine at the same time...
Conversation
You too might be interested in opam switch then, it's a bit like virtualenv! That even lets you install multiple coq versions! ssr.msr-inria.inria.fr/~gares/www/des
It's not perfect but after old Cabal I'll conform to anything.
1
1
1
Yeah, I really should use it... I think I mostly haven't because our build scripts don't, and I'm not sure why that is (IIRC it's hard to automate or something? Or was?).
2
To automate this, I fear you'll need a `prepare-profiles.sh` and a build script relying on those envs. Plus pain when prepare-profiles.sh changes, unless you can detect which build profiles exist (which you probably can?)...
I'd prefer this to what you describe but YMMV!
2
1
I am now scared and want to run away to Lean again... but yes, I want to run this stuff on CI and this would be neccessary. And I hate dev config being in READMEs 🤦♂️
1
yikes wait, does ``eval `opam config env` `` mutate your shell state?
1
Probably... not sure why else eval would be used here.
1
Yeah, guess I'm just used to the cargo/npm/yarn/bundler approach of working off the current directory and config files. Just seems quite easy to forget that you've altered your environment in a long running shell.
1
It just sets environment vars (PATH etc.) — use `opam config env` to see what it'll do. New shells get that automatically (once you add that command to the init sequence) — but opam switch *sets* the default profile, so you're scared of the wrong thing IMHO? :-D
1
1
Ah, right, gotcha. Can you pin stuff scoped to a specific directory?
2
like, scoped to an opam project?