Makefile revision 5bb7eeaca10ea76595229375f907a5a388b7c882
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# Author: (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2005
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# This Makefile will compile the new hets system and provides also
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# targets for test programs during implementation phases.
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# !!! Note: This makefile is written for GNU make !!!
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# (gmake on solaris)
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen####################################################################
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen## Some varibles, which control the compilation
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenCOMMONLIB_PATH = Common/Lib Common/ATerm fgl/Data/Graph \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen fgl/Data/Graph/Inductive fgl/Data/Graph/Inductive/Internal \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen fgl/Data/Graph/Inductive/Monad fgl/Data/Graph/Inductive/Query
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenCLEAN_PATH = . utils/DrIFT-src utils/GenerateRules utils/InlineAxioms Common \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Logic CASL CASL/CCC Syntax Static GUI HasCASL Haskell Modal CoCASL COL \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen CspCASL ATC ToHaskell Proofs Comorphisms Isabelle Driver $(INCLUDE_PATH) \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Haskell/Hatchet Hatchet Taxonomy CASL_DL SPASS $(PFE_PATHS)
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# the 'replacing spaces' example was taken from the (GNU) Make info manual
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen## set ghc imports properly for your system
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen DERIVEPATH=.:ghc:$(GHC_IMPORTS):$(subst $(space),:,$(PFE_PATHS))
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# override on commandline for other architectures
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen /home/www/agbkb/forschung/formal_methods/CoFI/hets/`utils/sysname.sh`
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps) Common/Utils.hs
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenINLINEAXIOMS_deps = utils/InlineAxioms/InlineAxioms.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Common/Lib/Pretty.hs Common/Keywords.hs Common/Lib/Set.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Common/Lib/Map.hs Common/Lib/Rel.hs Common/Lib/State.hs Common/Id.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Common/AS_Annotation.hs CASL/AS_Basic_CASL.hs CASL/ShowMixfix.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen CASL/Utils.hs Common/Lexer.hs Common/Token.hs Common/Anno_Parser.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Common/GlobalAnnotations.hs Common/PrettyPrint.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Common/Print_AS_Annotation.hs Common/PPUtils.hs CASL/LiteralFuns.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen CASL/Print_AS_Basic.hs Common/AnnoState.hs CASL/Formula.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen CASL/OpItem.hs CASL/SortItem.hs CASL/Inject.hs Common/Result.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Common/ConvertLiteral.hs Common/Earley.hs CASL/MixfixParser.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen CASL/Parse_AS_Basic.hs CASL/Sign.hs CASL/Overload.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen CASL/StaticAna.hs Modal/AS_Modal.hs Modal/Parse_AS.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Modal/ModalSign.hs Modal/Print_AS.hs Modal/StatAna.hs
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenHC_FLAGS = $(HC_WARN) -fglasgow-exts -fno-monomorphism-restriction \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen -fallow-overlapping-instances -fallow-undecidable-instances
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# -ddump-minimal-imports
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# flags also come in via ../uni/uni-package.conf
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# but added it here in case of compilation without uni
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainenlogics = CASL HasCASL Modal CoCASL COL CspCASL Hatchet CASL_DL
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenUNI_PACKAGE_CONF = $(wildcard ../uni/uni-package.conf)
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenHC_PACKAGE = -package-conf $(UNI_PACKAGE_CONF) -package uni-davinci \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# some modules from uni for haddock
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen# if uni/server is included also HaXml sources are needed
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainenuni_dirs = ../uni/davinci ../uni/graphs ../uni/events \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainenuni_sources = $(wildcard $(addsuffix /haddock/*.hs, $(uni_dirs))) \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen### list of directories to run checks in
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenTESTDIRS += Common CASL HasCASL Haskell/Hatchet/examples
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenPFE_TOOLDIR = $(wildcard ../programatica/tools)
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen base/parse2/LexerGen base/parse2/LexerSpec base/tests/HbcLibraries \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen base/transforms base/transforms/Deriving property \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen property/syntax property/AST property/transforms \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen property/TI property/defs property/parse2 property/parse2/Parser
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenPFE_PATHS = $(addprefix $(PFE_TOOLDIR)/, $(PFE_DIRS))
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainenpfe_sources = $(wildcard $(addsuffix /*hs, $(PFE_PATHS)))
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenPFE_FLAGS = -package data -package text $(PFE_PATH) -DPROGRAMATICA
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainenhappy_files += $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen$(LEX_DIR)Gen/HsLexerGen: $(LEX_DIR)Gen/*.hs $(LEX_DIR)Spec/*.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen -i$(LEX_DIR) -i$(LEX_DIR)Gen -i$(LEX_DIR)Spec \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainenderived_sources += Haskell/PreludeString.hs $(LEX_DIR)/HsLex.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenAPPENDPRELUDESTRING = utils/appendHaskellPreludeString \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen## rule for appendHaskellPreludeString
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenHaskell/PreludeString.hs: Haskell/PreludeString.append.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenAst_Haskell_files = HsDeclStruct HsExpStruct HsFieldsStruct \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen HsGuardsStruct HsKindStruct HsPatStruct HsTypeStruct HsAssocStruct \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenOther_PFE_files = property/AST/HsPropStruct base/defs/PNT \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen base/defs/UniqueNames base/Modules/TypedIds base/TI/TiKinds \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen base/parse2/SourceNames base/syntax/SyntaxRec \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen $(addprefix $(PFE_TOOLDIR)/base/AST/, $(Ast_Haskell_files)) \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen $(addprefix $(PFE_TOOLDIR)/, $(Other_PFE_files)))
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen## rule for ATC generation
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenHaskell/ATC_Haskell.der.hs: $(Haskell_files) utils/genRules
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen utils/genRules -r $(rule) -o Haskell -h ATC/Haskell.header.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen### Profiling (only for debugging)
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen### Attention every module must be compiled with profiling or the linker
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen### cannot link the various .o files properly. So after switching on
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen### Profiling, do an 'gmake real_clean; gmake'
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen### and comment out HC_PACKAGE variable definition above.
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen### Comment in the following line for switching on profiling.
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen#HC_PROF = -prof -auto-all
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenHCI_OPTS = $(HC_FLAGS) $(HC_INCLUDE) $(HC_PACKAGE) $(PFE_FLAGS)
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenHC_OPTS = $(HCI_OPTS) $(HC_PROF) -DHATCHET -DCASLEXTENSIONS
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen####################################################################
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen## sources for hets
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainennon_sources = Common/LaTeX_maps.svmono.hs CspCASL/Main.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Static/LogicStructured.hs Common/CaslLanguage.hs ./Test.hs
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainensources = hets.hs $(filter-out $(non_sources), \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen $(wildcard $(addsuffix /[A-Z]*hs, $(SOURCE_PATHS))))
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainendrifted_files = Syntax/AS_Architecture.hs Syntax/AS_Library.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Common/AS_Annotation.hs CASL/AS_Basic_CASL.hs Syntax/AS_Structured.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Modal/AS_Modal.hs CoCASL/AS_CoCASL.hs COL/AS_COL.hs CASL_DL/AS_CASL_DL.hs\
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainengenrule_header_files = $(wildcard ATC/*.header.hs)
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Syntax/AS_Structured.der.hs Syntax/AS_Architecture.der.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Common/GlobalAnnotations.hs Syntax/AS_Library.der.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Static/DevGraph.hs Proofs/Proofs.hs Isabelle/IsaSign.hs
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainenatc_der_files = $(foreach file, $(atc_files), \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen ATC/$(basename $(basename $(notdir $(file)))).der.hs)
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenCASL_files = CASL/Sublogic.hs CASL/Morphism.hs CASL/Sign.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenHasCASL_files = HasCASL/As.hs HasCASL/Le.hs HasCASL/Morphism.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenModal_files = Modal/AS_Modal.hs Modal/ModalSign.hs
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenCoCASL_files = CoCASL/AS_CoCASL.hs CoCASL/CoCASLSign.hs
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenCspCASL_files = CspCASL/AS_CSP_CASL.hs CspCASL/SignCSP.hs
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenHatchet_files = Haskell/Hatchet/AnnotatedHsSyn.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Haskell/Hatchet/MultiModuleBasics.hs Haskell/Hatchet/HsSyn.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Haskell/Hatchet/Representation.hs Haskell/Hatchet/Class.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainen Haskell/Hatchet/KindInference.hs Haskell/Hatchet/Env.hs \
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo SirainenCASL_DL_files = CASL_DL/AS_CASL_DL.hs CASL_DL/Sign.hs
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainenatc_logic_files = $(foreach logic, $(logics), $(logic)/ATC_$(logic).der.hs)
1537d20b852cbbf0d6971790b84e0cce5ca61307Timo Sirainengenerated_rule_files = $(atc_der_files) $(atc_logic_files)
$(wildcard utils/GenerateRules/*.hs) \
$(wildcard utils/InlineAxioms/*.hs) \
$(RM) $@
$(HC_FLAGS) -O
# "HetCATS/hetcats.TAGS"
(cd utils/GenerateRules; \
GenerateRules.hs -o ../genRules && strip ../genRules)
-i../.. -o $(INLINEAXIOMS)
if [ -d ../programatica ] ; then \
./clean.sh; \
gen_atc_files = \
### also delete *.d.bak (dependency file backups)
ghci:
### ATerm.Lib test system
## two hardcoded dependencies for a correct generation of Version.hs
.SUFFIXES:
%: %.hs
$(HAPPY) $<
%.hs: %.y
$(HAPPY) -o $@ $<
$(INLINEAXIOMS) $< > $@
%.d : %.hs
%.d : %.lhs
## rule for Modal/ModalSystems.hs needed for ModalLogic Translation