Bas Spitters (Aug 11 2020 at 08:39): Bas Spitters (Aug 11 2020 at 08:39):What is the current preferred install method on Windows? Still the windows installer? Or has it been replaced by Coq platform?
https://github.com/coq/coq/wiki/Installation-of-Coq-on-Windows
Michael Soegtrop (Aug 11 2020 at 09:01):Bas Spitters said:
What is the current preferred install method on Windows? Still the windows installer? Or has it been replaced by Coq platform?
https://github.com/coq/coq/wiki/Installation-of-Coq-on-Windows
the Coq platform is still in alpha stage, but I would say it is usable and it has the advantage to set up a reasonable Coq development system, which easily allows to install additional Coq modules via opam. But I must admit I currently test only the 64 bit builds - I am not sure if the 32 bit builds work (there might be some minor issues). In the future the Windows installer will be build using the Coq platform.
E.g. it should be easy to take the Coq platform script and add CoRN to it (I will do so soon, but it is not yet there).
Bas Spitters (Aug 11 2020 at 09:30):I'll need to recommend something to my students. I'm teaching a Coq course soon using SF, Equations and Quickchick.
Most of them will use linux or Mac, but some will use windows. I hear you are staying stay with the windows installer for now.
Michael Soegtrop (Aug 11 2020 at 09:49):Well the coq-platform has the advantage that it works on all platforms (Windows, Mac, Linux) in the same way and you could easily install additional stuff, say SF. Also with the Coq platform you get a working make on Windows. The goal of the Coq platform is to provide a consistent environment independent of platform. The downside is that currently it installs from sources so it takes one hour (much less if you remove mathcomp, VST and CompCert).
Michael Soegtrop (Aug 11 2020 at 09:51):I would say technically the alpha3 is good enough for your needs. The only issues I am aware of is a sandbox issue with remake, but from what you said you don't need remake based packages (Flocq, Coqueilcot, ...). So I would recommend to make a fork of Coq-platform and taylor the package installations at the end to your specific needs. You definitely have my support in case you need it.
Théo Zimmermann (Aug 11 2020 at 13:02):Just be aware that if you start recommending the platform to your students, you will effectively make them all alpha testers (and you should be ready to report all the issues that they face).
Michael Soegtrop (Aug 11 2020 at 14:30):@Bas Spitters : one question: which IDE do you recommend to your students? VSCoq, CoqIDE or ProofGeneral?
Bas Spitters (Aug 11 2020 at 14:31):I'll go with vscode and PG.
Michael Soegtrop (Aug 11 2020 at 14:36):I guess on Windows VSCode only or do your students install Emacs for Windows?
Bas Spitters (Aug 11 2020 at 14:51):I gather students will choose vscode on windows.
Michael Soegtrop (Aug 11 2020 at 15:00):OK, this should work fine (emacs is a bit tricky on Windows - either one uses emacs for Windows which more or less comes with its own posix OS abstraction or you use cygwin emacs, which has path restrictions).
So as I said, if you want to give the platform a try, I make sure I am available around the time your students install it.
Clément Pit-Claudel (Aug 14 2020 at 19:06):Is there anything wrong with installing Emacs on Windows? I did that as an undergrad, it worked fine
Karl Palmskog (Aug 14 2020 at 19:10):I did it early this year, worked fine for me as well (emacs for Windows, not the Cygwin one)
Clément Pit-Claudel (Aug 14 2020 at 19:54):I would hope so, given that the maintainer of Emacs develops on Windows ^^
Michael Soegtrop (Aug 15 2020 at 13:23):Clément Pit-Claudel said:
Is there anything wrong with installing Emacs on Windows? I did that as an undergrad, it worked fine
What I don't like about it is the size of it. It duplicates so much infrastructure one anyway needs an has.
Last updated: Jun 03 2023 at 04:30 UTC