Hacker News Reader

Comment by frollo | Hacker News Reader

It was about 4 or 5 years ago, when I was in grad school.

The main problem I had with it is that it kept crashing or failing for misterious reason and it just printed out some obscure French error message (which I was forced to pass through Google Translate, since nobody in the whole class could speak French). This only happened for the most obscure errors, while the more common and easy to spot ones (logical errors, typos...) were well documented in English.

Also a lot of useful parts of the manual (and the community posts around it) were written in French.

I don't think it's really inferior to other tools, but the bad documentation and tendency to crash (which I hope had been fixed by now, TBH) got on my nerves.

View on HN

Lest anyone read this and fear that this is common: In my experience it isn't. Nor was it 4 or 5 years ago. I've never seen Coq crash at all, nor spit out any error message in French, and I was a full-time user for a while.

In my recollection (but I could have read it wrong the first time) it tied to the OS. It had those problem on Linux, but both Mac and Windows users were capable of running it without much hassle (although they did experience the occasional crash). Also, people running Arch had less problems than us running Debian. But I just wanted to pass the course and didn't spend much time debugging it, so it could have been another thing (just a couple of ideas from the top of my head: library versions, conflicts with other running programs, some compiler weirdness...)

Interesting, I've only ever used it on Ubuntu, both with the system Debian packages and with versions built from source (via Opam, the OCaml package manager). Both were rock solid for me. If anything, my understanding is that it's Windows where things are sketchy (for OCaml in general, not Coq specifically). Anyway. I'm sorry to hear you had a bad time. It's probably no consolation that it doesn't seem to be as bad for most others.

> It's probably no consolation that it doesn't seem to be as bad for most others.

I stopped using Coq after that course and moved to other interests, but I'm relatively happy to know that, if I ever need Coq again, the chances for it to be the same PITA I remember are pretty low.

I might not ever need it anymore, but it's a small consolation to know that I don't need to fear that possibility.

Reply on news.ycombinator.com