Compilation experience report

[LasseBlaauwbroek]

I did an installation of the platform on a fresh Windows 10 install that came stock with a notebook. Most things went fine, but I did have a few issues (some of them are just things that might be useful to document in the readme):

• I had to set git config --global core.autocrlf false before cloning the git repo. Otherwise, the bash scripts won't execute, because they contain carriage returns
• I had to disable some scanners. In particular 'HP Sure Sense' (whatever that is) and 'Windows real-time protection'
• I had to change this line

  platform/shell_scripts/install_opam.sh

  Line 50 in 4c14268

  bash opam$BITSIZE/install.sh --prefix "/usr/$(uname -m)-w64-mingw32/sys-root/mingw"

  to bash opam64/install.sh --prefix /usr/sys-root/mingw

Otherwise, everything was pretty smooth! Much better than the previous installer for windows.

[Zimmi48]

What do you mean by this?

Much better than the previous installer for windows.

[LasseBlaauwbroek]

I mean that customizing coq platform is much easier than the way one could generate a windows custom installer previously (using the code that is in the main Coq repo). And by customizing I mean adding/removing packages.

[MSoegtropIMC]

@LasseBlaauwbroek : can you give some more details on the Virus scanner settings you used? E.g. a screen shot of the default and after settings would be nice. Also example error messages when the scanners are enabled would be helpful.

I will add notes about the git config settings (what you have should be the default for Cygwin git, but not for "GIT for Windows".

[LasseBlaauwbroek]

Attached are some images. The virues scanners seem to be unhappy about the downloading of the opam binary. To turn of HP Sure Sense, go to the HP Sure Sense App -> Settings -> Advanced Settings -> Edit and turn of Threat Protection.

[LasseBlaauwbroek]

Note that I just turned everything I could find off, because I don't really care about the security of this machine. There may be more subtle methods.

[MSoegtropIMC]

Thanks! Since it seems to be about a specific file it might also make sense to report a false positive. With GData I have more the issue that it crawls folders which in windows has the effect that deleting the folder is denied - so the effects I see are random failures on a rm or mv.

[LasseBlaauwbroek]

Ah, I never use scanners normally, so I have no idea how such reporting would work...

[MSoegtropIMC]

I took the feedback comments into account in PR #160. Thanks!