I want to be able to import the category theory module from unimath. I already have the coqide and vscode with the coq extensions, I also have wsl. I tried downloading the library from git and used "make", which didnt work. Now I'm trying to follow https://github.com/UniMath/UniMath/blob/master/INSTALL_WIN.md but the first step, Install Coq through Cygwin, fails because I can't run coq_platform_make_windows.bat because my antivirus thinks it's a Trojan. Should I disable it and try running it? Is there an easier way of achieving this goal? TIA
4
-
$\begingroup$ Do you think the authors of unimath library are trying to install a Trojan on your computer? Depending on the answer, the next step is clear. $\endgroup$– Andrej BauerCommented Jan 21 at 19:02
-
1$\begingroup$ I seriously doubt you need to install Coq via Cygwin if you already have a working Coq installed. You should be able to just skip that step. $\endgroup$– Andrej BauerCommented Jan 21 at 19:02
-
1$\begingroup$ If you have troubles with installation, I would suggest to give a look at the Coq platform, a set of scripts designed to make it easy to install Coq and a bunch of libraries (including Unimath) in a relatively automated way. $\endgroup$– Meven Lennon-Bertrand ♦Commented Jan 22 at 9:35
-
$\begingroup$ you can install coq and unimath into whatever Linux system your WSL is running, and use your native (Windows) vscode to communicate with it. In such a setup Cygwin is irrelevant. $\endgroup$– Dima PasechnikCommented Mar 18 at 10:32
Add a comment
|