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 http://coq.inria.fr/distrib/V8.3pl2/files/coq-8.3pl2.tar.gz | tar -xvzf -
cd coq-8.3pl2
curl http://www.cs.berkeley.edu/~megacz/garrows/coq-8.3pl2-tracer-patch | patch -p1 
./configure -prefix /usr/local/coq/
make
sudo make install



rendered from WIX