I'm still pasting code around like a barbarian, but to do this properly, I'd follow these instructions, then cargo-cult their opam file and maybe understand it:
gitlab.mpi-sws.org/FP/iris-exampl
Coq-iris doesn't seem to depend on autosubst, but that code does, through a separate opam repo.
Conversation
Ahh yes, seems to be on their repository: gitlab.mpi-sws.org/FP/opam-dev/tr
1
2
We were confused is because it requires you to mutate your opam environment:
opam repo add coq-released coq.inria.fr/opam/released
opam repo add iris-dev gitlab.mpi-sws.org/FP/opam-dev.git
find opam abit ick from a 'repoducable environment' perspective, but maybe I just don't understand...
2
2
Honestly... I have had some not great experiences with it. I think 2.0 is coming out soon though and that is supposed to resolve some pervasive issues.
2
2
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.
2
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?
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
Show replies