Getting the HetMet Extensions
The HetMet extensions are distributed as a git “remote branch” of the official GHC repository; the gitweb is here. To obtain and build it:
git clone http://git.megacz.com/ghc-hetmet.git
git clone -b coq-extraction-baked-in \
git submodule init
git submodule update
git submodule foreach 'git branch -D master || :'
git submodule foreach 'git checkout -b master || :'
cp mk/build.mk.sample mk/build.mk
echo 'GhcStage1HcOpts += -O0' >> mk/build.mk
echo 'GhcStage2HcOpts += -O0' >> mk/build.mk
make BuildFlavour=quickest inplace/bin/ghc-stage2
The echo lines are optional; they speed up compilation.
The second git clone above fetches a special branch of the repository in which the Haskell extraction of the Coq code has already been performed; this lets you build the HetMet extensions without having Coq installed.
If you want to extract the Haskell code yourself, just omit that line. However, note that you must have exactly the right version of Coq installed (the Makefile will check this), and you must have patched the extraction code to keep GHC from trying to optimize Coq's use of unsafeCoerce (see this).