[Iris-Club] Installing Iris Coq mode on Windows

[Ralf Jung]

Hi Jan,

> Thanks. I wanted to use ProofGeneral anyway, so CoqIDE not working
> should not be a problem.
>> When building from source, if it cannot find coqc, that sounds like your
>> environment is not set up properly.  coqc must be in the PATH.
> 
> Coqc is in the path, and works fine from the Windows command prompt but
> not from the Linux subsystem.

Yes, I think that is expected.  The Linux subsystem is separate and can only use
Linux binaries.  So you have to install a Linux Coq first.  (At least, I think
that's how this works.  I've never used it.)  I don't know if opam works in the
Linux subsystem, but some people seem to have gotten it to work:
<https://stackoverflow.com/a/46414810>.

>> If ssreflect
>> worked, that indicates that it could somehow find Coq... how exactly did you
>> install ssreflect? 
> 
> There is a Windows installer for Ssreflect on the mathematical
> components website. I just used that one.

Ah, I see.  I assume this, too, doesn't make anything usable from the Linux
subsystem; instead this just installs ssreflect for your Windows Coq.  Iris'
Makefile requires some basic POSIX tools, so you'll have to install some kind of
POSIX-compatible environment in Windows (MSYS should be enough).

Essentially, "Cygwin-opam" and "Windows+MSYS/MinGW" and "Linux subsystem" each
form their own little independent world, and if you are in one world you cannot
use anything from another world.

> If everything else fails, would it be possible to compile Iris on a
> Linux system and then copy the .vo and .v files over to Windows, or is
> there something else to Iris that could not be transferred in that way?

Besides Iris, you'll also need to do the same for std++.  And it has to be the
exact same version of Coq.  I have not tried this, and I do not know if .vo
files are cross-platform-compatible.

Kind regards,
Ralf