X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=ghc.mk;h=738b5ca11fbf3ea209a55f0d314676480331e3d9;hp=160b2277d7af1dc6cfaa2becfbf07f17f4ac604c;hb=e10a75279987aa31492f5ead289a6646d69b3a23;hpb=295016c3c0aa1f407436136e39ababf2dc8b50c6

diff --git a/ghc.mk b/ghc.mk
index 160b227..738b5ca 100644
--- a/ghc.mk
+++ b/ghc.mk
@@ -1,3 +1,4 @@
+
 # -----------------------------------------------------------------------------
 #
 # (c) 2009 The University of Glasgow
@@ -135,9 +136,14 @@ $(error $$(GhcLibWays) is empty, it must contain at least one way)
 endif
 endif
 
+ifeq "$(phase)" ""
+phase = final
+endif
+
 # -----------------------------------------------------------------------------
 # Utility definitions
 
+include rules/prof.mk
 include rules/trace.mk
 include rules/make-command.mk
 
@@ -306,7 +312,7 @@ TH_PACKAGES := $(DPH_PACKAGES)
 #
 # We assume that the stage0 compiler has a suitable bytestring package,
 # so we don't have to include it below.
-STAGE0_PACKAGES = Cabal hpc extensible-exceptions binary bin-package-db
+STAGE0_PACKAGES = Cabal hpc extensible-exceptions binary bin-package-db hoopl
 
 # These packages are installed, but are installed hidden
 # Why install them at all?  Because the 'ghc' package depends on them
@@ -389,6 +395,7 @@ $(eval $(call addPackage,template-haskell))
 $(eval $(call addPackage,Cabal))
 $(eval $(call addPackage,binary))
 $(eval $(call addPackage,bin-package-db))
+$(eval $(call addPackage,hoopl))
 $(eval $(call addPackage,mtl))
 $(eval $(call addPackage,utf8-string))
 $(eval $(call addPackage,xhtml))
@@ -504,7 +511,7 @@ endif
 # ----------------------------------------------
 # Checking packages with 'cabal check'
 
-ifeq "$(phase)" ""
+ifeq "$(phase)" "final"
 ifeq "$(CHECK_PACKAGES)" "YES"
 all: check_packages
 endif
@@ -641,7 +648,7 @@ $(foreach p,$(STAGE0_PACKAGES),$(eval libraries/$p_dist-boot_DO_HADDOCK = NO))
 ifeq "$(HADDOCK_DOCS)" "YES"
 libraries/index.html: inplace/bin/haddock$(exeext) $(ALL_HADDOCK_FILES)
 	cd libraries && sh gen_contents_index --inplace
-ifeq "$(phase)" ""
+ifeq "$(phase)" "final"
 $(eval $(call all-target,library_doc_index,libraries/index.html))
 endif
 INSTALL_LIBRARY_DOCS += libraries/*.html libraries/*.gif libraries/*.css libraries/*.js
@@ -673,6 +680,7 @@ $(eval $(call build-package,libraries/extensible-exceptions,dist-boot,0))
 $(eval $(call build-package,libraries/Cabal,dist-boot,0))
 $(eval $(call build-package,libraries/binary,dist-boot,0))
 $(eval $(call build-package,libraries/bin-package-db,dist-boot,0))
+$(eval $(call build-package,libraries/hoopl,dist-boot,0))
 
 # register the boot packages in strict sequence, because running
 # multiple ghc-pkgs in parallel doesn't work (registrations may get
@@ -1204,3 +1212,15 @@ phase_0_builds: $(utils/genprimopcode_dist_depfile_c_asm)
 .PHONY: phase_1_builds
 phase_1_builds: $(PACKAGE_DATA_MKS)
 
+# -----------------------------------------------------------------------------
+# Support for writing GHC passes in Coq
+
+compiler/hetmet/Makefile:
+	git submodule update --init compiler/hetmet
+	cd compiler/hetmet/; git checkout master
+compiler/hetmet/build/CoqPass.hs: compiler/hetmet/Makefile $(wildcard compiler/hetmet/src/*.v) $(wildcard compiler/hetmet/src/*.hs)
+	cd compiler/hetmet; make
+compiler/stage1/build/CoqPass.hs: compiler/hetmet/build/CoqPass.hs
+	cp compiler/hetmet/build/CoqPass.hs $@
+compiler/stage2/build/CoqPass.hs: compiler/hetmet/build/CoqPass.hs
+	cp compiler/hetmet/build/CoqPass.hs $@