[Iris-Club] Installing Iris Coq mode on Windows

[Hai Dang]

Hi Jan,

Like Ralf has mentioned, in general there are usually problems with using opam on Windows.

I managed to build Iris on MSYS2 before (I got MSYS2 by installing Git for Windows),
just by compiling everything from source. This includes building Coq (whose make should set PATH
correctly), the dependencies, and then Iris.

Hope this helps,
Hai

> From: Ralf Jung <jung at mpi-sws.org>
> 
> Hi Jan,
> 
> I have very little experience with Windows, and I am not sure if any of us is
> using Windows, so I'm mostly guessing here.  Most of what you say seem to be
> general problems for Coq on Windows though, so maybe the folks on coq-club can
> help you?
> 
> If you use opam, you have to install Coq via opam.  I am not sure what you mean
> by "recognize that Coq is already installed", but opam will not be able to use a
> Coq you installed by some other means.  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.  The main problem with this approach
> is that I failed to compile CoqIDE with opam, so if you want to use that UI
> you're out of luck.  Using ProofGeneral in emacs however should work (but I have
> not tested that); this setup creates native Windows Coq binaries that should
> work outside of the Cygwin environment.  I have not tried the Windows subsystem
> for Linux.
> 
> 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.  If you use the
> latest git master version of Iris, you can also use the COQBIN environment
> variable to configure the path containing the Coq binaries.  If ssreflect
> worked, that indicates that it could somehow find Coq... how exactly did you
> install ssreflect?  And which exact version of Iris did you use?
> 
> Kind regards,
> Ralf
> 
> On 05.03.2018 12:40, Jan Menz wrote:
>> Hello,
>> 
>> I've tried to install the Coq mode for Iris and failed spectacularly.
>> Following the instructions on the Iris page I first tried to install it
>> via opam using the Windows subsystem for Linux. However, for some reason
>> the system does not seem to recognize that the newest Coq version is
>> already installed. It tries to install it again which fails. Apparently
>> there is a problem with camlp5.
>> 
>> Then I tried to install Iris by building it from source. Installing
>> Ssreflect worked fine, but when I tried to install std++ the makefile
>> did not work because when running make coqc is not found. When I try to
>> run make on the windows command environment (which I suspect is not what
>> I should be doing) the command cut cannot be found.
>> 
>> Does anyone have experience with installing Iris on Windows and can tell
>> me how to do it?
>> 
>> Yours,
>> 
>> Jan.
>>