Getting the HetMet ExtensionsThe 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). |