Coq “Tracer” Patch

You must use Coq version 8.3pl2 with the “tracer patch”; this patch wraps every extracted expression in a call to the trace method, which is a {-#NOINLINE#-}'d method which does nothing. This inhibits a (yet-unknown) GHC optimization which causes the resulting binary to segfault.

To summarize,

curl | tar -xvzf -
cd coq-8.3pl2
curl | patch -p1 
./configure -prefix /usr/local/coq/
sudo make install