Makefile revision bd54a9917cd87169b8e40bcc5616c537fed85815
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# Author: (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2005
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# This Makefile will compile the new hets system and provides also
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# targets for test programs during implementation phases.
e20788e1216ed720aefa84f3295f7899d9f28c22Mark Andrews# !!! Note: This makefile is written for GNU make !!!
e20788e1216ed720aefa84f3295f7899d9f28c22Mark Andrews# (gmake on solaris)
e20788e1216ed720aefa84f3295f7899d9f28c22Mark Andrews####################################################################
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt## Some varibles, which control the compilation
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntHXT_PATHS = Data Data/Tree Data/Tree/NTree Data/Digest Text Text/XML \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Text/XML/HXT Text/XML/HXT/IO Text/XML/HXT/DOM Text/XML/HXT/Arrow \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Text/XML/HXT/XPath Text/XML/HXT/Validator Text/XML/HXT/Parser \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Text/XML/HXT/RelaxNG Text/XML/HXT/ProtocolHandler Codec Codec/ASN1 \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Codec/Binary Codec/Encryption Codec/Encryption/RSA System Control \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt utils utils/DrIFT-src utils/GenerateRules utils/InlineAxioms Common \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Common/Lib Common/ATerm Logic CASL CASL/CCC CASL/CompositionTable \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Syntax Static GUI HasCASL Haskell Modal CoCASL COL ConstraintCASL \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Taxonomy CASL_DL SPASS OWL_DL OMDoc $(PFE_PATHS) \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# the 'replacing spaces' example was taken from the (GNU) Make info manual
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt## set ghc imports properly for your system
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# import directories for ghc-5.04.2
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntGHC5 = $(GHC_IMPORTS)/base:$(GHC_IMPORTS)/haskell98
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt DERIVEPATH=.:$(GHC_IMPORTS):$(GHC5):$(subst $(space),:,$(PFE_PATHS))
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# override on commandline for other architectures
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt /home/www/agbkb/forschung/formal_methods/CoFI/hets/`utils/sysname.sh`
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps) Common/Utils.hs
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntINLINEAXIOMS_deps = utils/InlineAxioms/InlineAxioms.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Common/Lib/Pretty.hs Common/Keywords.hs Common/Lib/Set.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Common/Lib/Map.hs Common/Lib/Rel.hs Common/Lib/State.hs Common/Id.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Common/AS_Annotation.hs CASL/AS_Basic_CASL.hs CASL/ShowMixfix.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt CASL/Utils.hs Common/Lexer.hs Common/Token.hs Common/Anno_Parser.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Common/GlobalAnnotations.hs Common/PrettyPrint.hs Common/Partial.hs \
75e5062bc524bbd1067cd42d5725e8bbe9f2134aMark Andrews Common/Print_AS_Annotation.hs Common/PPUtils.hs CASL/LiteralFuns.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt CASL/Print_AS_Basic.hs Common/AnnoState.hs CASL/Formula.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt CASL/OpItem.hs CASL/SortItem.hs CASL/Inject.hs Common/Result.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Common/ConvertLiteral.hs Common/Earley.hs CASL/MixfixParser.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt CASL/Parse_AS_Basic.hs CASL/Sign.hs CASL/Overload.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt CASL/StaticAna.hs Modal/AS_Modal.hs Modal/Parse_AS.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Modal/ModalSign.hs Modal/Print_AS.hs Modal/StatAna.hs
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntGENRULECALL = $(GENRULES) -r Typeable -r ShATermConvertible \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# remove -fno-warn-orphans for older ghcs and add -ifgl
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt $(HC_WARN) -fglasgow-exts -fno-monomorphism-restriction \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt -fallow-overlapping-instances -fallow-undecidable-instances
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# -ddump-minimal-imports
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# flags also come in via ../uni/uni-package.conf
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# but added it here in case of compilation without uni
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Huntlogics = CASL HasCASL Isabelle Modal CoCASL COL CspCASL CASL_DL SPASS OWL_DL ConstraintCASL
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntTESTTARGETS += test_parser hetpa hetana Test.o wrap isa fromKif \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntUNI_PACKAGE_CONF = $(wildcard ../uni/uni-package.conf)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntHC_PACKAGE = -package-conf $(UNI_PACKAGE_CONF) -package uni-davinci \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# some modules from uni for haddock
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt# if uni/server is included also HaXml sources are needed
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Huntuni_dirs = ../uni/davinci ../uni/graphs ../uni/events \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Huntuni_sources = $(wildcard $(addsuffix /haddock/*.hs, $(uni_dirs))) \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt### list of directories to run checks in
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt base/parse2/LexerGen base/parse2/LexerSpec base/tests/HbcLibraries \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt base/transforms base/transforms/Deriving property \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt property/syntax property/AST property/transforms \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt property/TI property/defs property/parse2 property/parse2/Parser
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntPFE_PATHS = $(addprefix $(PFE_TOOLDIR)/, $(PFE_DIRS))
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Huntpfe_sources = $(wildcard $(addsuffix /*hs, $(PFE_PATHS)))
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntPFE_FLAGS = -package data -package text $(PFE_PATH) -DPROGRAMATICA
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunthappy_files += $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt echo "{-# OPTIONS -w #-}" > $@
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt$(LEX_DIR)Gen/HsLexerGen: $(LEX_DIR)Gen/*.hs $(LEX_DIR)Spec/*.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Huntderived_sources += Haskell/PreludeString.hs $(LEX_DIR)/HsLex.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntAPPENDPRELUDESTRING = utils/appendHaskellPreludeString \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt## rule for appendHaskellPreludeString
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntHaskell/PreludeString.hs: Haskell/PreludeString.append.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntAst_Haskell_files = HsDeclStruct HsExpStruct HsFieldsStruct \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt HsGuardsStruct HsKindStruct HsPatStruct HsTypeStruct HsAssocStruct \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt#Ti_Haskell_files = TiTypes TiKinds TiDecorate TiInstanceDB
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt#Ti_Prop_files = property/TI/TiPropDecorate property/syntax/PropSyntaxRec
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntOther_PFE_files = property/AST/HsPropStruct base/defs/PNT \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt base/defs/UniqueNames base/Modules/TypedIds base/Modules/Ents \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt $(addprefix $(PFE_TOOLDIR)/base/AST/, $(Ast_Haskell_files)) \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt## rule for ATC generation
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntHaskell/ATC_Haskell.der.hs: $(Haskell_files) $(GENRULES)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt $(GENRULECALL) -i Haskell.BaseATC -o $@ $(Haskell_files)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunths_der_files += Haskell/TiATC.hs Haskell/TiDecorateATC.hs Haskell/TiPropATC.hs
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt### Profiling (only for debugging)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt### Attention every module must be compiled with profiling or the linker
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt### cannot link the various .o files properly. So after switching on
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt### Profiling, do an 'gmake real_clean; gmake'
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt### Comment in the following line for switching on profiling.
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt#HC_PROF = -prof -auto-all -fignore-asserts
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntHC_OPTS = $(HC_FLAGS) $(HC_INCLUDE) $(HC_PACKAGE) $(PFE_FLAGS) $(HC_PROF) \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt####################################################################
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt## sources for hets
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Huntnon_sources = Common/LaTeX_maps.svmono.hs CspCASL/Main.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Common/CaslLanguage.hs ./Test.hs Static/LogicStructured.hs
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt $(wildcard $(addsuffix /[A-Z]*hs, $(SOURCE_PATHS))))
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Huntdrifted_files = Syntax/AS_Architecture.hs Syntax/AS_Library.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Common/AS_Annotation.hs CASL/AS_Basic_CASL.hs Syntax/AS_Structured.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Modal/AS_Modal.hs CoCASL/AS_CoCASL.hs COL/AS_COL.hs CASL_DL/AS_CASL_DL.hs\
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Huntatc_files = Common/AS_Annotation.der.hs Common/DefaultMorphism.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Syntax/AS_Structured.der.hs Syntax/AS_Architecture.der.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Common/GlobalAnnotations.hs Syntax/AS_Library.der.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt Logic/Prover.hs #Common/Id.hs Common/Result.hs OWL_DL/AS.hs
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt ATC/$(basename $(basename $(notdir $(file)))).der.hs)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntATC/AS_Annotation.der.hs: Common/AS_Annotation.der.hs $(GENRULES)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntATC/DefaultMorphism.der.hs: Common/DefaultMorphism.hs $(GENRULES)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntATC/AS_Structured.der.hs: Syntax/AS_Structured.der.hs $(GENRULES)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt $(GENRULECALL) -i ATC.AS_Annotation -i ATC.Grothendieck -o $@ $<
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntATC/AS_Architecture.der.hs: Syntax/AS_Architecture.der.hs $(GENRULES)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntATC/AS_Library.der.hs: Syntax/AS_Library.der.hs $(GENRULES)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntATC/GlobalAnnotations.der.hs: Common/GlobalAnnotations.hs $(GENRULES)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Hunt $(GENRULECALL) -x ProverTemplate -i ATC.AS_Annotation -o $@ $<
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntCASL_files = CASL/Sublogic.hs CASL/Morphism.hs CASL/Sign.hs \
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntHasCASL_files = Common/Prec.hs HasCASL/As.hs HasCASL/Le.hs HasCASL/Sublogic.hs
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntConstraintCASL_files = ConstraintCASL/AS_ConstraintCASL.hs
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntCoCASL_files = CoCASL/AS_CoCASL.hs CoCASL/CoCASLSign.hs CoCASL/Sublogic.hs
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntCspCASL_files = CspCASL/AS_CSP_CASL.hs CspCASL/SignCSP.hs
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan HuntCASL_DL_files = CASL_DL/AS_CASL_DL.hs CASL_DL/Sign.hs
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Huntatc_logic_files = $(foreach logic, $(logics), $(logic)/ATC_$(logic).der.hs)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Huntgenerated_rule_files = $(atc_der_files) $(atc_logic_files)
ba751492fcc4f161a18b983d4f018a1a52938cb9Evan Huntgendrifted_files = $(patsubst %.der.hs, %.hs, $(generated_rule_files))
$(wildcard utils/GenerateRules/*.hs) \
$(wildcard utils/InlineAxioms/*.hs) \
$(RM) $@
cgi:
# "HetCATS/hetcats.TAGS"
@$(PERL) -e \
$(sources) >> $@
(cd utils/GenerateRules; \
GenerateRules.hs -o ../genRules && strip ../genRules)
if [ -d ../programatica ] ; then \
./clean.sh; \
-o $@ $(OWL_DL_files)
### ATerm.Lib test system
$(RM) $@
## two hardcoded dependencies for a correct generation of Version.hs
.SUFFIXES:
%: %.hs
%.hs: %.y
$(RM) $@
$(RM) $@
$(INLINEAXIOMS) $< > $@
%.d : %.hs
%.d : %.lhs
$(RM) $@
$(RM) $@
$(PERL) $+ > $@
## rule for Modal/ModalSystems.hs needed for ModalLogic Translation
# uses intransparently utils/outlineAxioms
$(RM) $@