The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

On Thu, Jul 3, 2014 at 11:45 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

Officially, we support both, even though we clearly lack usable feedback
from windows users, as well as machines to debug ourselves.

I use Coq primarily on Windows (with Emacs/PG, so I don't know about CoqIDE), and the biggest issues I've had are https://coq.inria.fr/bugs/show_bug.cgi?id=2944 (which I believe is now fixed in trunk), https://coq.inria.fr/bugs/show_bug.cgi?id=3335, and possibly https://coq.inria.fr/bugs/show_bug.cgi?id=3275.  None of these are particularly major (though a lack of [Timeout] is annoying when minimizing scripts in 8.4), and I find that Coq tends to work smoothly, except when I send it into an infinite loop and occasionally spamming ctrl+c isn't enough to break it.  Oh, I guess another issue is that if I do a parallel make and then break the script with ctrl+c, the Coq processes don't die until they finish, and I have to kill them from task manager.

-Jason