Cool, that is good to hear! The CLI is pretty at least, with nice coloured unicode icons and little camels! Even as I recoil in horror as it seems to turn off and on packages globally.
Conversation
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...
3
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?
I don't know and I wouldn't, but it sounds like you're coming at a '90s build tool with expectations from the 2020s.
Right now, to *play* with autosubst, I'm modifying the examples in a checkout. And later I'd "vendor" it (paste it in my tree), it's not fast-moving :-)
1
1
I admire your resolve, but my current *feeling* is that investigating this would be lots of yak-shaving—and in a domain, binding lemmas, which is a YUGE YAK itself!
1
1
Show replies