Makefile revision 39ec02ed6f8f24492deffc7324e2cd6f83605534
dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews# Author: (c) Klaus Luettich, Christian Maeder, Uni Bremen 2002-2009
ec5347e2c775f027573ce5648b910361aa926c01Automatic Updater# This Makefile will compile the hets system and provides also
483a5a91ada151e7edba90b98ce376b06b0013e3Mark Andrews# targets for test programs during implementation phases.
40f53fa8d9c6a4fc38c0014495e7a42b08f52481David Lawrence# !!! Note: This makefile is written for GNU make !!!
dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews# (gmake on solaris)
dafcb997e390efa4423883dafd100c975c4095d6Mark Andrews# the 'replacing spaces' example was taken from the (GNU) Make info manual
9c3531d72aeaad6c5f01efe6a1c82023e1379e4dDavid LawrenceDRIFT_ENV = DERIVEPATH=$(subst $(space),:,$(PFE_PATHS))
ed94876a19354c03545152abbc8826a95bcadbdcDavid LawrenceGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps)
29747dfe5e073a299b3681e01f5c55540f8bfed7Mark AndrewsGENITCORRECTIONS_deps = utils/itcor/GenItCorrections.hs
ab023a65562e62b85a824509d829b6fad87e00b1Rob AusteinINLINEAXIOMS_deps = utils/InlineAxioms/InlineAxioms.hs \
49a83dbc7e0a0c209789d389d6ac95d437d782c1Mark Andrews Common/Doc.hs CASL/ToDoc.hs Modal/AS_Modal.hs \
358628c8f4804a2db52be0f6d03a66137fab4884David Lawrence Modal/Parse_AS.hs Modal/ModalSign.hs Modal/Print_AS.hs Modal/StatAna.hs
d468b1b7b2ccfdf132df15f600be48dccf447eb1Evan HuntGENRULECALL = $(GENRULES) -r Typeable -r ShATermConvertible \
d468b1b7b2ccfdf132df15f600be48dccf447eb1Evan HuntGENRULECALL2 = $(GENRULES) -r Typeable -r ShATermLG \
358628c8f4804a2db52be0f6d03a66137fab4884David LawrenceSETUPPREFIX = --prefix=$(HOME)/.ghc/$(ARCH)-$(OSBYUNAME)-hets-packages
358628c8f4804a2db52be0f6d03a66137fab4884David Lawrence ../$(SETUP) configure -O -p $(SETUPPREFIX) --user; \
358628c8f4804a2db52be0f6d03a66137fab4884David Lawrence ../$(SETUP) build; ../$(SETUP) haddock; ../$(SETUP) install
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# list glade files
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterGTK_GLADE_FILES = $(wildcard GUI/Glade/*.glade)
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterGTK_GLADE_HSFILES = $(subst .glade,.hs,$(GTK_GLADE_FILES))
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# the list of logics that need ShATermConvertible instances
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyterlogics = CASL HasCASL Isabelle Modal Temporal CoCASL COL CspCASL CASL_DL \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter SoftFOL ConstraintCASL Propositional OWL RelationalScheme VSE OMDoc DFOL \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter LF Framework Maude ExtModal CommonLogic CSL QBF
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterTESTTARGETFILES += CASL/fromKif.hs CASL/capa.hs HasCASL/hacapa.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter Haskell/wrap.hs Isabelle/isa.hs Syntax/hetpa.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter ATC/ATCTest.hs ATC/ATCTest2.hs Common/ATerm/ATermLibTest.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter Common/ATerm/ATermDiffMain.hs Common/annos.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter SoftFOL/tests/PrintTPTPTests.hs Comorphisms/test/showKP.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter Comorphisms/test/sublogicGraph.hs PGIP/ParseProofScript.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter### list of directories to run checks in
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyterhs_clean_files = Haskell/TiATC.hs Haskell/TiDecorateATC.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter Haskell/TiPropATC.hs Haskell/ATC_Haskell.der.hs
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter base/parse2/LexerGen base/parse2/LexerSpec base/tests/HbcLibraries \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter base/transforms base/transforms/Deriving property \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter property/syntax property/AST property/transforms \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter property/TI property/defs property/parse2 property/parse2/Parser
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterPFE_PATHS = $(addprefix $(PFE_TOOLDIR)/, $(PFE_DIRS))
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyterpfe_sources = $(wildcard $(addsuffix /*hs, $(PFE_PATHS)))
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyterhappy_files += $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyterprogramatica_pkg: $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter @if $(HCPKG) field programatica version; then \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter echo "of programatica package found"; else \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter -i `pwd`/Haskell/Programatica.patch || exit 0); \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter cp -f utils/programatica.cabal ../programatica/tools; \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter echo "{-# OPTIONS -w #-}" > $@
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter$(LEX_DIR)Gen/HsLexerGen: $(LEX_DIR)Gen/*.hs $(LEX_DIR)Spec/*.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter $(HC) --make -fno-monomorphism-restriction -O \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter -i$(LEX_DIR) -i$(LEX_DIR)Gen -i$(LEX_DIR)Spec \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterAPPENDPRELUDESTRING = utils/appendHaskellPreludeString \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter## rule for appendHaskellPreludeString
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterHaskell/PreludeString.hs: Haskell/PreludeString.append.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterAst_Haskell_files = HsDeclStruct HsExpStruct HsFieldsStruct \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter HsGuardsStruct HsKindStruct HsPatStruct HsTypeStruct HsAssocStruct \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter#Ti_Haskell_files = TiTypes TiKinds TiDecorate TiInstanceDB
6f4375f230743997c80fbb13e6b9bbb168bde586Mark Andrews#Ti_Prop_files = property/TI/TiPropDecorate property/syntax/PropSyntaxRec
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterOther_PFE_files = property/AST/HsPropStruct base/defs/PNT \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter base/defs/UniqueNames base/Modules/TypedIds base/Modules/Ents \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter base/parse2/SourceNames base/syntax/SyntaxRec \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter $(addprefix $(PFE_TOOLDIR)/base/AST/, $(Ast_Haskell_files)) \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter $(addprefix $(PFE_TOOLDIR)/, $(Other_PFE_files)))
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter## rule for ATC generation
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterHaskell/ATC_Haskell.der.hs: $(Haskell_files) $(GENRULES)
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter $(GENRULECALL) -i Haskell.BaseATC -o $@ $(Haskell_files)
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterTESTTARGETFILES += Haskell/hana.hs Haskell/h2h.hs Haskell/h2hf.hs
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# unset this variable from var.mk because the programatica sources
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# are needed to created our sources!
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# end of programatica stuff
49a83dbc7e0a0c209789d389d6ac95d437d782c1Mark AndrewsTESTTARGETS = Test.o $(subst .hs,,$(TESTTARGETFILES))
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterHC_WARN = -Wall -fno-warn-orphans $(NO_BIND_WARNING)
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# uncomment HC_PROF for profiling (and comment out packages in var.mk)
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# call resulting binary with a final +RTS -p to get a file <binary>.prof
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# HC_PROF = -prof -auto-all -osuf p_o +RTS -K100m -RTS
baf62093eb60684ad8514d56ac300a8030d8e501Jakob SchlyterHC_OPTS += $(HC_WARN) $(HC_INCLUDE) $(HC_PROF)
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# -ddump-minimal-imports
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# uncomment the above line to generate .imports files for displayDependencyGraph
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# files generated by DriFT
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter Syntax/AS_Structured.hs Syntax/AS_Architecture.hs Syntax/AS_Library.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter CspCASL/AS_CspCASL_Process.hs CspCASL/AS_CspCASL.hs \
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyter# files to extract data types from to generate ShATermConvertible instances
baf62093eb60684ad8514d56ac300a8030d8e501Jakob Schlyteratc_files = Common/AS_Annotation.der.hs Common/DefaultMorphism.hs \
358628c8f4804a2db52be0f6d03a66137fab4884David Lawrence Syntax/AS_Structured.der.hs Syntax/AS_Architecture.der.hs \
483a5a91ada151e7edba90b98ce376b06b0013e3Mark Andrews Common/GlobalAnnotations.hs Syntax/AS_Library.der.hs \
40f53fa8d9c6a4fc38c0014495e7a42b08f52481David Lawrence Logic/Prover.hs Common/LibName.hs Common/ExtSign.hs \
ed94876a19354c03545152abbc8826a95bcadbdcDavid Lawrence Common/Consistency.hs Common/ProofTree.hs Static/DevGraph.hs \
b8870486533975eaecda7827532560b3f13ff534David Lawrence Common/Id.hs Common/Result.hs Common/OrderedMap.hs \
483a5a91ada151e7edba90b98ce376b06b0013e3Mark Andrews# files generated by genRules as input for DriFT
21f1794606dce19928cf455029e173321f166380Mark Andrews ATC/$(basename $(basename $(notdir $(file)))).der.hs)
21f1794606dce19928cf455029e173321f166380Mark Andrews# the rules to create ATC .der.hs file for DriFT
935000aa6e2b9d08f363b2e698a258a458a5a7cfMark AndrewsATC/OrderedMap.der.hs: Common/OrderedMap.hs $(GENRULES)
935000aa6e2b9d08f363b2e698a258a458a5a7cfMark AndrewsATC/Graph.der.hs: Common/Lib/Graph.hs $(GENRULES)
935000aa6e2b9d08f363b2e698a258a458a5a7cfMark AndrewsATC/ProofTree.der.hs: Common/ProofTree.hs $(GENRULES)
935000aa6e2b9d08f363b2e698a258a458a5a7cfMark AndrewsATC/AS_Annotation.der.hs: Common/AS_Annotation.der.hs $(GENRULES)
483a5a91ada151e7edba90b98ce376b06b0013e3Mark Andrews $(GENRULECALL) -i ATC.Id -i Common.ATerm.ConvInstances -o $@ $<
ed94876a19354c03545152abbc8826a95bcadbdcDavid LawrenceATC/Consistency.der.hs: Common/Consistency.hs $(GENRULES)
$(GENRULECALL) -o $@ $<
$(GENRULECALL2) -o $@ $<
# all ATC .der.hs files for all logics
# a rule to create all .der.hs files
# files to be processed by utils/InlineAxioms
cgi:
(cd utils/GenerateRules; \
GenerateRules.hs -o ../genRules)
-i../.. -o $(INLINEAXIOMS)
./clean.sh; \
# Common/LaTeX_maps.hs generation
@echo -n "Generating pretty/LaTeX_maps.hs ... "
@(cd pretty >/dev/null; ../utils/genItCorrections \
$(RM) $@
## two hardcoded dependencies for a correct generation of Version.hs
.SUFFIXES:
%.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) $@
@echo Please do