[Iris-Club] Fwd: Re: Installing Iris Coq mode on Windows

[Jan Menz]

Hello Ralf, hello Hai,
thank you for the tips. I spent the last days trying to install Coq on
my raspberry pi as an alternative but that didn't go well either and
probably wouldn't be a great solution anyway.

> 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 did not install Coq via opam but via the Windows installer on the Coq
website. So that might be part of the problem. I was worried that I'd
only be able to use Coq within the shell if I did not use the Windows
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.  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.

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.

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

> And which exact version of Iris did you use?

I used Iris 3.1 following the instructions on the webpage.

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

Thanks, I'll keep that in mind and try it if installing via opam fails.


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?
Yours,
Jan.

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