[Iris-Club] Installing Iris Coq mode on Windows

[Jan Menz]

Hello,

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.

> 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.


Thanks for all the help I got here, it pointed me in the right direction.


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?

Yours Jan.

Am 09.03.2018 um 13:50 schrieb 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
> 

-- 
Legal Notice: I hereby specifically prohibit the use and storage of this
message by the BND, NSA, GCHQ or any other intelligence agency and
withdraw any permission I might or might not have given to any of these
institutions to use or store any of my data.

Should my data be stored or used in any way anyway I reserve the right
to take legal action.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20180323/1285c722/attachment.sig>