rules revision 4d5652abf9ed9c5714723ff7fdb80a54f7350fb2
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee# Author: (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2004
bf56214c0556fa6864189c826d39dbe156bb22a0stevel# Year: 2004
bf56214c0556fa6864189c826d39dbe156bb22a0stevel# This Makefile will compile the new hetcats system and provides also
bf56214c0556fa6864189c826d39dbe156bb22a0stevel# targets for test programs during implementation phases.
bf56214c0556fa6864189c826d39dbe156bb22a0stevel# !!! Note: This makefile is written for GNU make !!!
bf56214c0556fa6864189c826d39dbe156bb22a0stevel# (gmake on solaris ; make on linux)
bf56214c0556fa6864189c826d39dbe156bb22a0stevel####################################################################
bf56214c0556fa6864189c826d39dbe156bb22a0stevel## Some varibles, which control the compilation
bf56214c0556fa6864189c826d39dbe156bb22a0stevelINCLUDE_PATH = ghc:hetcats:fgl
bf56214c0556fa6864189c826d39dbe156bb22a0stevelCOMMONLIB_PATH = Common/Lib:Common/ATerm:fgl/Data/Graph:fgl/Data/Graph/Inductive:fgl/Data/Graph/Inductive/Aux:fgl/Data/Graph/Inductive/Monad:fgl/Data/Graph/Inductive/Query
bf56214c0556fa6864189c826d39dbe156bb22a0stevelCLEAN_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:Taxonomy:$(PFE_PATHS)
bf56214c0556fa6864189c826d39dbe156bb22a0stevel## set ghc imports properly for your system
bf56214c0556fa6864189c826d39dbe156bb22a0stevelLINUX_IMPORTS = $(wildcard /home/linux-bkb/ghc/ghc-latest/lib/ghc-*/imports)
bf56214c0556fa6864189c826d39dbe156bb22a0stevelDRIFT_ENV = DERIVEPATH='.:ghc:hetcats:${LINUX_IMPORTS}:${GHC_IMPORTS}'
bf56214c0556fa6864189c826d39dbe156bb22a0stevel# the 'replacing spaces' example was taken from the (GNU) Make info manual
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleespace:= $(empty) $(empty)
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee# override on commandline for other architectures
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeINSTALLDIR = /home/www/agbkb/forschung/formal_methods/CoFI/hets/`utils/sysname.sh`
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeDRIFT_deps = utils/DrIFT-src/*hs
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps)
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeINLINEAXIOMS_deps = utils/InlineAxioms/*hs $(drifted_files)
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeHAPPY = happy
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeDRIFT = $(DRIFT_ENV) utils/DrIFT
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeHADDOCK = haddock
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeHC_FLAGS = -Wall -fglasgow-exts -fno-monomorphism-restriction \
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee -fallow-overlapping-instances -fallow-undecidable-instances
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee# -ddump-minimal-imports
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997frits# flags also come in via ../uni/uni-package.conf
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997frits# but added it here in case of compilation without uni
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeHC_INCLUDE = -i$(INCLUDE_PATH)
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeUNI_PACKAGE_CONF := $(wildcard ../uni/uni-package.conf)
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeifneq ($(strip $(UNI_PACKAGE_CONF)),)
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeHC_PACKAGE = -package-conf $(UNI_PACKAGE_CONF) -package uni-davinci \
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee -package uni-server -DUNI_PACKAGE
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee# some modules from uni for haddock
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee# if uni/server is included also HaXml sources are needed
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeuni_sources = $(wildcard ../uni/davinci/haddock/*.hs) \
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee $(wildcard ../uni/graphs/haddock/*.hs) \
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee $(wildcard ../uni/htk/haddock/*/*.hs) \
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee $(wildcard ../uni/events/haddock/*.hs) \
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee $(wildcard ../uni/reactor/haddock/*.hs) \
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee $(wildcard ../uni/util/haddock/*.hs) \
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee $(wildcard ../uni/posixutil/haddock/*.hs)
bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jgPFE_TOOLDIR := $(wildcard ../programatica/tools)
bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jgifneq ($(strip $(PFE_TOOLDIR)),)
bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jgPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg base/transforms base/transforms/Deriving hs2html pfe property base \
bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg property/pfe property/syntax property/AST property/transforms \
bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg property/TI property/defs property/parse2 property/parse2/Parser \
bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jgPFE_PATH = $(addprefix -i$(PFE_TOOLDIR)/, $(PFE_DIRS))
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee# add PFE_PATHS to DERIVEPATH if needed
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee# but name clashes currently prevent ATC generation in a single file
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleePFE_PATHS = $(subst $(space),:,$(addprefix $(PFE_TOOLDIR)/, $(PFE_DIRS)))
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleepfe_sources = $(wildcard $(subst :,/*hs , $(PFE_PATHS)))
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleePFE_FLAGS = -package data -package text $(PFE_PATH) -DPROGRAMATICA
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee#-fallow-undecidable-instances -fno-monomorphism-restriction
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee### Profiling (only for debugging)
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997frits### Attention every module must be compiled with profiling or the linker
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee### cannot link the various .o files properly. So after switching on
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee### Profiling, do an 'gmake real_clean; gmake'
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997frits### and comment out HC_PACKAGE variable definition above.
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee### Comment in the following line for switching on profiling.
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee#HC_PROF = -prof -auto-all
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeHCI_OPTS = $(HC_FLAGS) $(HC_INCLUDE) $(HC_PACKAGE) $(PFE_FLAGS)
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeHC_OPTS = $(HCI_OPTS) $(HC_PROF)
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeDRIFT_OPTS = +RTS -K10m -RTS
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee### list of directories to run checks in
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlcleeTESTDIRS = Common CASL HasCASL
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee####################################################################
3ccda6479cf240cd732ac4b7a8a82fcc1716496dlclee## sources for hetcats (semi - manually produced with a perl script)
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997fritsGHCMAKE_OUTPUT = $(wildcard hetcats-make)
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997fritsifneq ($(strip $(GHCMAKE_OUTPUT)),)
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997fritsSOURCE_PATHS = $(COMMON_LIB_PATH):$(CLEAN_PATH)
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997fritssources = $(wildcard $(subst :,/*hs , $(SOURCE_PATHS))/*hs)
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997fritsobjects = $(patsubst %.lhs,%.o,$(sources:%.hs=%.o))
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997fritsdrifted_files = Syntax/AS_Architecture.hs Syntax/AS_Library.hs \
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997frits Common/AS_Annotation.hs CASL/AS_Basic_CASL.hs Syntax/AS_Structured.hs \
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997frits $(gendrifted_files)
4ebb14b236958cfe1ef4ff3b7a50216d9e51f997fritsgenrule_header_files = $(wildcard ATC/*.header.hs)
ATC/$(basename $(basename $(notdir $(file)))).der.hs)
atc_logic_files = $(foreach logic, $(logics), $(logic)/ATC_$(logic).der.hs)
gendrifted_files = $(patsubst %.der.hs, %.hs, $(generated_rule_files))
gen_inline_axiom_files = $(patsubst %.hs,%.inline.hs,$(inline_axiom_files))
derived_sources = $(drifted_files) hetcats/Version.hs \
$(inline_axiom_files) Modal/ModalSystems.hs
cpp_sources = ./Isabelle/Logic_Isabelle.hs \
taxonomy hets.cgi count doc apache_doc post_doc4apache \
#.PRECIOUS: sources_hetcats.mk
$(HC) --make -o $@ hets.hs $(HC_OPTS) 2>&1 | tee hetcats-make
$(HC) --make -O -o hets hets.hs $(HC_OPTS) -w 2>&1 | tee hetcats-make
ghc --make -package-conf /home/luettich/ghc-pkg/package.conf \
taxonomy: Taxonomy/taxonomyTool.hs $(tax_sources)
$(HC) --make -o Taxonomy/taxonomyTool $< -ifgl $(HC_OPTS)
hetcats.TAGS: $(sources)
$(sources); mv TAGS $@; mv tags hetcats.tags
doc: docs/index.html
docs/index.html: $(doc_sources)
$(MAKE) hets.cgi
$(PERL) utils/post_process_docs.pl docs \
utils/DrIFT: $(DRIFT_deps)
utils/genRules: $(GENERATERULES_deps)
(cd utils/GenerateRules; \
GenerateRules.hs -o ../genRules && strip ../genRules)
$(HC) --make utils/InlineAxioms/InlineAxioms.hs \
(cd HetCATS; $(MAKE) derivedSources; ./clean.sh; \
$(RM) clean.*; mv Makefile Makefile.orig; \
tar cvf HetCATS.tar HetCATS
cp -p hets $(INSTALLDIR)/versions/hets-`cat version_nr`
ln -s versions/hets-`cat version_nr` hets; $(RM) version_nr)
$(atc_der_files): $(atc_files) $(genrule_header_files) utils/genRules
utils/genRules -r $(rule) -o CASL $(CASL_files)
utils/genRules -r $(rule) -o HasCASL $(HasCASL_files)
utils/genRules -r $(rule) -o Modal $(Modal_files)
utils/genRules -r $(rule) -o CoCASL $(CoCASL_files)
utils/genRules -r $(rule) -o COL $(COL_files)
utils/genRules -r $(rule) -o CspCASL $(CspCASL_files)
if [ -f ATC/$(basename $(basename $(notdir $(file)))).header.hs ]; \
then utils/genRules -r $(rule) -o ATC -h \
ATC/$(basename $(basename $(notdir $(file)))).header.hs $(file); \
else utils/genRules -r $(rule) -o ATC $(file); fi ;
LEX_DIR := $(PFE_TOOLDIR)/base/parse2/Lexer
$(LEX_DIR)Gen/HsLexerGen: $(LEX_DIR)Gen/*.hs $(LEX_DIR)Spec/*.hs \
$(LEX_DIR)/HsTokens.hs
-i$(PFE_TOOLDIR)/base/tests/HbcLibraries \
-i$(PFE_TOOLDIR)/base/lib \
$(RM) CASL/capa
$(RM) HasCASL/hacapa
$(RM) Haskell/hapa
$(RM) Haskell/hana
$(RM) Haskell/wrap
$(RM) Syntax/hetpa
$(RM) Static/hetana
$(RM) GUI/hetdg
$(RM) Common/annos
$(RM) Haskell/Hatchet/hatch
$(RM) ToHaskell/translateAna
$(RM) Taxonomy/taxonomyTool
### also delete *.d.bak (dependency file backups)
(cd $$p ; $(RM) *.d *.d.bak) ; done
$(RM) hetcats-make sources_hetcats.mk
$(RM) hetcats/Version.hs
test_parser: Common/test_parser
capa: CASL/capa
hacapa: HasCASL/hacapa
hana: Haskell/hana
hetpa: Syntax/hetpa.hs Syntax/*.hs
hetana: Static/hetana.hs Static/*.hs
atctest: ATC/ATCTest.hs ATC/*.hs
### ATerm.Lib test system
hetdg: GUI/hetdg.hs $(drifted_files) *.hs
## two hardcoded dependencies for a correct generation of Version.hs
%.hs: %.inline.hs $(INLINEAXIOMS)
## rule for Modal/ModalSystems.hs needed for ModalLogic Translation
utils/genTransMFormFunc.pl $(INLINEAXIOMS)
$(PERL) utils/genTransMFormFunc.pl $< $@