Makefile revision 824125ad97b34671bd7ea72655967f46caeb0004
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# Author: (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2004
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# Year: 2004
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# This Makefile will compile the new hetcats system and provides also
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# targets for test programs during implementation phases.
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# !!! Note: This makefile is written for GNU make !!!
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# (gmake on solaris ; make on linux)
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync####################################################################
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync## Some varibles, which control the compilation
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncCOMMONLIB_PATH = Common/Lib:Common/Lib/Parsec:Common/ATerm:fgl/Data/Graph:fgl/Data/Graph/Inductive:fgl/Data/Graph/Inductive/Aux:fgl/Data/Graph/Inductive/Monad:fgl/Data/Graph/Inductive/Query
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncCLEAN_PATH = utils/DrIFT-src:utils/GenerateRules:utils/InlineAxioms:Common:Logic:CASL:CASL/CCC:Syntax:Static:GUI:HasCASL:Haskell:Modal:CoCASL:COL:CspCASL:ATC:ToHaskell:Proofs:Comorphisms:Isabelle:$(INCLUDE_PATH):Haskell/Hatchet:$(PFE_PATHS)
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync## set ghc imports properly for your system
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncLINUX_IMPORTS = $(wildcard /home/linux-bkb/ghc/ghc-latest/lib/ghc-*/imports)
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncDRIFT_ENV = DERIVEPATH='.:ghc:hetcats:${LINUX_IMPORTS}:${GHC_IMPORTS}'
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# the 'replacing spaces' example was taken from the (GNU) Make info manual
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# override on commandline for other architectures
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncINSTALLDIR = /home/www/agbkb/forschung/formal_methods/CoFI/hets/`utils/sysname.sh`
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps)
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncINLINEAXIOMS_deps = utils/InlineAxioms/*hs $(drifted_files)
09ac8d4619f93468eb42354e1a1d43822a857fc0vboxsync# -fallow-overlapping-instances -fallow-incoherent-instances
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# -ddump-minimal-imports
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# flags also come in via ../uni/uni-package.conf
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# but added it here in case of compilation without uni
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncUNI_PACKAGE_CONF := $(wildcard ../uni/uni-package.conf)
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncHC_PACKAGE = -package-conf $(UNI_PACKAGE_CONF) -package uni-davinci \
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# some modules from uni for haddock
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# if uni/server is included also HaXml sources are needed
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncuni_sources = $(wildcard ../uni/davinci/haddock/*.hs) \
9446711dd04e377f0de8160e1a191ad33d2032f1vboxsyncPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
a251e09c45654264f660f69396b08b38e813efb9vboxsync base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
a251e09c45654264f660f69396b08b38e813efb9vboxsync property/pfe property/syntax property/AST property/transforms \
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync property/TI property/defs property/parse2 property/parse2/Parser \
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncPFE_PATH = $(addprefix -i$(PFE_TOOLDIR)/, $(PFE_DIRS))
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# add PFE_PATHS to DERIVEPATH if needed
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync# but name clashes currently prevent ATC generation in a single file
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncPFE_PATHS = $(subst $(space),:,$(addprefix $(PFE_TOOLDIR)/, $(PFE_DIRS)))
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncpfe_sources = $(wildcard $(subst :,/*hs , $(PFE_PATHS)))
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsyncPFE_FLAGS = -package data -package text $(PFE_PATH) -DPROGRAMATICA
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync#-fallow-undecidable-instances -fno-monomorphism-restriction
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync### Profiling (only for debugging)
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync### Attention every module must be compiled with profiling or the linker
0a29840869615968f7abf77fb83908f9e660db31vboxsync### cannot link the various .o files properly. So after switching on
0a29840869615968f7abf77fb83908f9e660db31vboxsync### Profiling, do an 'gmake real_clean; gmake'
0a29840869615968f7abf77fb83908f9e660db31vboxsync### and comment out HC_PACKAGE variable definition above.
0a29840869615968f7abf77fb83908f9e660db31vboxsync### Comment in the following line for switching on profiling.
0a29840869615968f7abf77fb83908f9e660db31vboxsync#HC_PROF = -prof -auto-all
0a29840869615968f7abf77fb83908f9e660db31vboxsyncHCI_OPTS = $(HC_FLAGS) $(HC_INCLUDE) $(HC_PACKAGE) $(PFE_FLAGS)
0a29840869615968f7abf77fb83908f9e660db31vboxsync### list of directories to run checks in
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync####################################################################
659ccabad889fa6a1851dd1e34a5acce0daff787vboxsync## sources for hetcats (semi - manually produced with a perl script)
#.PRECIOUS: sources_hetcats.mk
$(RM) $@
$(HC_FLAGS) -O
(cd utils/GenerateRules; \
GenerateRules.hs -o ../genRules && strip ../genRules)
gen_atc_files = \
### also delete *.d.bak (dependency file backups)
$(RM) $@
ghci:
$(RM) $@
$(RM) $@
$(RM) $@
$(happy_files)
$(RM) $@
$(RM) $@
$(RM) $@
$(RM) $@
$(RM) $@
### ATerm.Lib test system
$(RM) $@
$(RM) $@
## two hardcoded dependencies for a correct generation of Version.hs
.SUFFIXES:
$(HAPPY) $<
$(INLINEAXIOMS) $< > $@
%.d : %.hs
%.d : %.lhs
## rule for Modal/ModalSystems.hs needed for ModalLogic Translation