[Iris-Club] std++ and Iris master on opam (and: opam.pins is dead)

Ralf Jung jung at mpi-sws.org
Tue Sep 19 15:04:53 CEST 2017


Hi all,

for some time now, we have used the "opam.pins" hack to declare with
version of std++ is required to build Iris, and to declare which version
of Iris is used by e.g. lambdaRust.  We used this hack because opam
cannot handle directly depending on a git SHA.  Unfortunately, this
meant that you could not just "opam install coq-iris" for a development
version of Iris, because the Iris -> std++ dependency would have broken
all the time.

Well, we fixed that!  We now have a magic opam repository at
<https://gitlab.mpi-sws.org/FP/opam-dev> that will automatically contain
opam versions for every single thing we push to Iris or std++ (master
branches only).  After doing

  opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git

you can obtain today's Iris via

  opam install coq-iris.dev.2017-09-19.0

Or maybe you want yesterday's std++?

  opam install coq-stdpp.dev.2017-09-18.0

This is now the preferred way to install Iris if you want to work *with*
Iris, i.e., if you import Iris in your own proofs.  For working *on*
Iris, we still have `make build-dep` (which has a new hilarious set of
hacks replacing opam.pins, but that's a story for another day).

If you work on Iris, this means that in the future, if you want to
update the build-dependency on std++, you do this by editing the opam
file rather than opam.pins.   You do not have to care about updating the
new opam repository; that will be done automagically by our CI.

If you work on a project depending on Iris (e.g. lambdaRust), the
project has to be converted away from opam.pins to depend on versions of
Iris newer than yesterday's.

Please play around with this and let me know what you think!

Kind regards,
Ralf



More information about the Iris-Club mailing list