[Iris-Club] Installing Iris Coq mode on Windows

[Ralf Jung]

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