[Iris-Club] Installing Iris Coq mode on Windows

[Ralf Jung]

Hello Jan,

> I finally managed to install Iris on Windows a few days ago and as far
> as I can tell everything seems to work fine. So I wanted to preserve
> what worked for me here for future reference.

Great, and thanks for posting!  Maybe if we can distill this to a step-by-step
list of instructions, we could put it into the Iris README.  Otherwise I guess I
will at least add a link to this opam/cygwin installer.

>> I once managed to install opam on
>> Windows via <https://fdopen.github.io/opam-repository-mingw/installation/>, then
>> compile Coq with it, and then install Iris.
> 
> I tried to do this. Unfortunately the installation of OPAM failed.
> However the installer did install cygwin and I found out that cygwin
> recognized the windows installation of Coq.
> 
> This allowed me to compile stdpp using cygwin.
> 
> I then tried to compile Iris the same way but there was a problem with
> Ssreflect. Apparently the Windows installer for Ssreflect/ the
> mathematical components library installed a version that was compiled
> with Coq 8.7.0 which was incompatible with my Coq version 8.7.2.
> 
> Hence I deleted the mathematical components library and compiled it from
> source using cygwin and Coq 8.7.2.
> 
> Now compiling Iris from source using cygwin worked.

So you did all of this with Cygwin, but manually, i.e. not using opam?

> On a slightly unrelated note: I saw here
> (https://coq.inria.fr/distrib/current/refman/ssreflect.html) that since
> version 8.7 Ssreflect is a native part of Coq. However just compiling
> without additionally installing Ssreflect from the mathematical
> components library did not work. Are there any plans to switch from the
> external Ssreflect library to the one that is part of Coq in the future?

Iris master currently still supports Coq 8.6.1, which is why is still uses the
"external" ssreflect.  But yes, this switch will happen.  In fact it already
happened in the "gen_proofmode" branch that we are currently working on.  We
don't have an ETA for merging that into master, but I hope it happens Soon (TM).

Kind regards,
Ralf