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 \
     http://git.megacz.com/coq-hetmet.git \
     ghc-hetmet/compiler/hetmet/

cd ghc-hetmet
git submodule init
git submodule update
git submodule foreach 'git branch   -D master || :'
git submodule foreach 'git checkout -b master || :'

perl boot
./configure
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

cd compiler/hetmet/examples
make

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).