I’m trying to download the zip file from https://github.com/coq/platform/blob/2021.02.1/README_Windows.mdvv so that I can use it with unimath but my antivirus is blocking the file download. Should I just disable it and keep going? Is there another way of me using unimath on windows? Is there another library that has category theory constructs that would be easier to download?
TIA
You should report this as false positive to your virus checker provider. This is definitely nonsense. I am using Gdata and have around one false positive with open source software per month and they fix it within a day.
If you cannot download the ZIP, you can use git to get the sources.
Please note that currently a release is ongoing and the links in the readme point already to a new tag, which doesn’t exist as yet. You should get the code links directly from the github code page.
Also note that UniMath is included in the binary installers provided in the release section - for a start this would be much faster - unimath takes a long while to compile from sources on Windows.
I did download the 8.15.0 yesterday, but it t still doesn’t give me access to any of the unimath libraries.
I also tried cloning the GitHub directory but then the unimath/sub subdirectory is empty for whatever reason and I don’t have access to the coq binaries within. I’m just super confused right now xD
Not sure what you are doing. I tried the following:
-
download Coq-Platform-release-2022.09.1-version.8.15.2022.09-Windows-x86_64.exe from the release page of Coq Platform.
-
Install it
-
Download the matching smoke test kit Smoke-test-kit-2022.09.1-version.8.15.2022.09-Windows-x86_64.zip
-
Extract the smoke test kit ZIP
-
Start CoqIDE (I started it from the installation target bin folder since I have many installed)
-
Load the test file for UniMath “smoke-test-kit/coq-unimath/Test.v” into CoqIDE and execute it. It runs fine and loads the UniMath files.
If something doesn’t work for you, you need to be more specific what exectly you do and expect.
Two notes:
-
unless there is a very good reason for using 8.15, I would use the latest Windows installer
-
when you use the Coq Platform ZIP / GIT you need to build Coq Platform from sources (which takes hours for UniMath) - the Coq Platform scripts / GIT as such don’t contain any Coq stuff at all, just scripts to build it from sources. I hope that this is sufficiently well documented in platform/doc/README_Windows.md at main · coq/platform · GitHub
@dodos: does it work now, or do you still have issues?