Not sure, it might be part of iris-dev I guess (that's the only other one listed).
"coq-iris" { (= "dev.2018-07-13.2.af5611c8") | (= "dev") }
Conversation
I can't even see coq-iris on opam... opam.ocaml.org/packages/
1
I think it's part of the "devel" repository... or something. I wish I understood opam better so I could tell you what that means.
1
Ohh, huh, interesting. Yeah, it confuses me too. Would be interesting to see how one could find it. Cant find any way to see a list of the devel packages online... 🤔 cc.
2
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.
1
2
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
I think the multiple versions thing is because they mutate the global opam environment whenever you work on something. Unlike something like cargo which doesn't mutate any global state (other than caching stuff).
I mean, it would be fine except that it can take a really long time to rebuild the Coq dependencies. And every once in a while it fails (I forget if I figured out why) and you get to try to manually fix it up or revert the whole thing and reinstall an old version you don't want.