Makefile revision 7165a916d2fa1bf87c4741ec63b253413eebbf69
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering# Author: (c) Klaus Luettich, Christian Maeder, Uni Bremen 2002-2009
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering# This Makefile will compile the hets system and provides also
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering# targets for test programs during implementation phases.
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering# !!! Note: This makefile is written for GNU make !!!
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering# (gmake on solaris)
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering# the 'replacing spaces' example was taken from the (GNU) Make info manual
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart PoetteringDRIFT_ENV = DERIVEPATH=$(subst $(space),:,$(PFE_PATHS))
d122948d6fbaac4505cf14a08f1237daa89efdd0Lennart PoetteringGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps)
d122948d6fbaac4505cf14a08f1237daa89efdd0Lennart PoetteringGENITCORRECTIONS_deps = utils/itcor/GenItCorrections.hs
d122948d6fbaac4505cf14a08f1237daa89efdd0Lennart PoetteringINLINEAXIOMS_deps = utils/InlineAxioms/InlineAxioms.hs \
d1ab0ca07372649dad70a0348d75e394f254e1b6Lennart Poettering Common/Doc.hs CASL/ToDoc.hs Modal/AS_Modal.hs \
8c6db8336536916d0476ff8233e0abf40a2f6aabLennart Poettering Modal/Parse_AS.hs Modal/ModalSign.hs Modal/Print_AS.hs Modal/StatAna.hs
8c4a3079a7f358c179430d1aec59de8b670b5f6eLennart PoetteringGENRULECALL = $(GENRULES) -r Typeable -r ShATermConvertible \
af2d49f70bcff20efaf2d69aecaf4b3e898ff1faLennart PoetteringGENRULECALL2 = $(GENRULES) -r Typeable -r ShATermLG \
34c8deaae1fcfa9e7c9db49b5f3a33973e103218Lennart Poettering -i Data.Typeable -i ATerm.Lib -i ATC.Grothendieck
487393e9f11e4a06d91df03232914bd8c4b3368eLennart PoetteringARCH = $(subst $(space),,$(shell uname -m))
70fcff314feff469a8e61dbe5017ed74f5e0a09dLennart PoetteringSETUPPREFIX = --prefix=$(HOME)/.ghc/$(ARCH)-$(OSBYUNAME)-hets-packages
af2d49f70bcff20efaf2d69aecaf4b3e898ff1faLennart Poettering ../$(SETUP) configure -O -p $(SETUPPREFIX) --user; \
af2d49f70bcff20efaf2d69aecaf4b3e898ff1faLennart Poettering ../$(SETUP) build; ../$(SETUP) haddock; ../$(SETUP) install --user
91901329245f070b621a24577393fb8f4ce9bffcLennart Poettering# list glade files
f401faf540ee31740b4cd0a8b3d4038ea8c33092Lennart PoetteringGTK_GLADE_FILES = $(wildcard GUI/Glade/*.glade)
b1b2a107d15a370d40b200172837bdd82ff3c3b2Fabiano FidêncioGTK_GLADE_HSFILES = $(subst .glade,.hs,$(GTK_GLADE_FILES))
bb29785e0df6a7cf07db0259a60bc1f3b4814cb4Lennart Poettering# the list of logics that need ShATermConvertible instances
ca2cab5dcd3d29f45992a439f54e48faad764c6eLennart Poetteringlogics = CASL HasCASL Isabelle Modal Temporal CoCASL COL CspCASL CASL_DL \
e23a0ce8badd09aefa961a3a576bfe85f6ebbad7Lennart Poettering SoftFOL ConstraintCASL Propositional OWL RelationalScheme VSE OMDoc DFOL \
83cc030fadf71d63d488cf9015275f9e5a02e2ccLennart PoetteringTESTTARGETFILES += CASL/fromKif.hs CASL/capa.hs HasCASL/hacapa.hs \
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering Haskell/wrap.hs Isabelle/isa.hs Syntax/hetpa.hs \
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering ATC/ATCTest.hs ATC/ATCTest2.hs Common/ATerm/ATermLibTest.hs \
9841e8e3d305e6f4173c9aedbe8d57adfe10d145Gustavo Sverzut Barbieri Common/ATerm/ATermDiffMain.hs Common/annos.hs \
9841e8e3d305e6f4173c9aedbe8d57adfe10d145Gustavo Sverzut Barbieri SoftFOL/tests/PrintTPTPTests.hs Comorphisms/test/showKP.hs \
9841e8e3d305e6f4173c9aedbe8d57adfe10d145Gustavo Sverzut Barbieri Comorphisms/test/sublogicGraph.hs PGIP/ParseProofScript.hs \
9841e8e3d305e6f4173c9aedbe8d57adfe10d145Gustavo Sverzut Barbieri SoftFOL/dfg.hs GUI/displayDependencyGraph.hs
9841e8e3d305e6f4173c9aedbe8d57adfe10d145Gustavo Sverzut Barbieri### list of directories to run checks in
c226fa4196aacf44a2aa9ebbd222161f79c2f070Lucas De Marchihs_clean_files = Haskell/TiATC.hs Haskell/TiDecorateATC.hs \
c226fa4196aacf44a2aa9ebbd222161f79c2f070Lucas De Marchi Haskell/TiPropATC.hs Haskell/ATC_Haskell.der.hs
c226fa4196aacf44a2aa9ebbd222161f79c2f070Lucas De MarchiPFE_TOOLDIR = $(wildcard ../programatica/tools)
f5c88ec1330b61787441156de7d764a140774bd2Miklos VajnaPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
f5c88ec1330b61787441156de7d764a140774bd2Miklos Vajna base/parse2/LexerGen base/parse2/LexerSpec base/tests/HbcLibraries \
f5c88ec1330b61787441156de7d764a140774bd2Miklos Vajna base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
f5c88ec1330b61787441156de7d764a140774bd2Miklos Vajna base/transforms base/transforms/Deriving property \
f5c88ec1330b61787441156de7d764a140774bd2Miklos Vajna property/syntax property/AST property/transforms \
1de4d79bf554946f486adf56ed765c5335816f15Andrey Borzenkov property/TI property/defs property/parse2 property/parse2/Parser
1de4d79bf554946f486adf56ed765c5335816f15Andrey BorzenkovPFE_PATHS = $(addprefix $(PFE_TOOLDIR)/, $(PFE_DIRS))
1de4d79bf554946f486adf56ed765c5335816f15Andrey Borzenkovpfe_sources = $(wildcard $(addsuffix /*hs, $(PFE_PATHS)))
1de4d79bf554946f486adf56ed765c5335816f15Andrey Borzenkovhappy_files += $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs
9841e8e3d305e6f4173c9aedbe8d57adfe10d145Gustavo Sverzut BarbieriLEX_DIR = $(PFE_TOOLDIR)/base/parse2/Lexer
9841e8e3d305e6f4173c9aedbe8d57adfe10d145Gustavo Sverzut Barbieriprogramatica_pkg: $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs \
c226fa4196aacf44a2aa9ebbd222161f79c2f070Lucas De Marchi @if $(HCPKG) field programatica version; then \
f5c88ec1330b61787441156de7d764a140774bd2Miklos Vajna echo "of programatica package found"; else \
9841e8e3d305e6f4173c9aedbe8d57adfe10d145Gustavo Sverzut Barbieri -i `pwd`/Haskell/Programatica.patch || exit 0); \
8c4a3079a7f358c179430d1aec59de8b670b5f6eLennart Poettering cp -f utils/programatica.cabal ../programatica/tools; \
ec863ba65a41e58680a3ab15841243088284e808Lennart Poettering ./Setup build; ./Setup install --user) fi
a5f9be457957731f6bd21bf60dd182fb2a6278cfLennart Poettering$(LEX_DIR)/HsLex.hs: $(LEX_DIR)Gen/HsLexerGen
d7ccca2e3f86feb81a48e243d8bad78814659a74Lennart Poettering echo "{-# OPTIONS -w #-}" > $@
a8f11321c209830a35edd0357e8def5d4437d854Lennart Poettering$(LEX_DIR)Gen/HsLexerGen: $(LEX_DIR)Gen/*.hs $(LEX_DIR)Spec/*.hs \
88213476187cafc86bea2276199891873000588dLennart Poettering -i$(PFE_TOOLDIR)/base/tests/HbcLibraries \
490aed584944b684026a3fd01f8d81f2881e38d6Lennart Poetteringderived_sources += Haskell/PreludeString.hs
a9b5b03212f9c854938483b8901e433c2ba6619bMichael TremerAPPENDPRELUDESTRING = utils/appendHaskellPreludeString \
8e27452380193a5f81bfd08a59aab8b07008ba0bLennart Poettering## rule for appendHaskellPreludeString
0b7964b804e093d31c9adc34ba1917017c7f4d60Lennart PoetteringHaskell/PreludeString.hs: Haskell/PreludeString.append.hs \
449ddb2d23a63ca4c8cd70d13a070fba87c1fb30Lennart PoetteringAst_Haskell_files = HsDeclStruct HsExpStruct HsFieldsStruct \
addab137cd8d318e4f543ca56018ee23d51aaca9Lennart Poettering HsGuardsStruct HsKindStruct HsPatStruct HsTypeStruct HsAssocStruct \
22be093ffb403a1c474037939ca9b88b1ee39f77Lennart Poettering#Ti_Haskell_files = TiTypes TiKinds TiDecorate TiInstanceDB
3d20ed6d51e38968cd646e2b3b24f36673408024Lennart Poettering#Ti_Prop_files = property/TI/TiPropDecorate property/syntax/PropSyntaxRec
e23a0ce8badd09aefa961a3a576bfe85f6ebbad7Lennart PoetteringOther_PFE_files = property/AST/HsPropStruct base/defs/PNT \
06cdd2484c5d0b7792168a7c2d99311e35b0fb8eLennart Poettering base/defs/UniqueNames base/Modules/TypedIds base/Modules/Ents \
8e1bd70d4ce6d3881c1df6a6482643a2b3a69bb1Lennart Poettering base/parse2/SourceNames base/syntax/SyntaxRec \
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering $(addprefix $(PFE_TOOLDIR)/base/AST/, $(Ast_Haskell_files)) \
2a796654b9a1f84962e5dafbcf171dcc22742c99Lennart Poettering $(addprefix $(PFE_TOOLDIR)/, $(Other_PFE_files)))
2a796654b9a1f84962e5dafbcf171dcc22742c99Lennart Poettering## rule for ATC generation
7f4e08056de0184b205a20632e62db73d299937eLennart PoetteringHaskell/ATC_Haskell.der.hs: $(Haskell_files) $(GENRULES)
7f4e08056de0184b205a20632e62db73d299937eLennart Poettering $(GENRULECALL) -i Haskell.BaseATC -o $@ $(Haskell_files)
7f4e08056de0184b205a20632e62db73d299937eLennart PoetteringTESTTARGETFILES += Haskell/hana.hs Haskell/h2h.hs Haskell/h2hf.hs
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering# unset this variable from var.mk because the programatica sources
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering# are needed to created our sources!
8c47c7325fa1ab72febf807f8831ff24c75fbf45Lennart Poettering# end of programatica stuff
8c6db8336536916d0476ff8233e0abf40a2f6aabLennart PoetteringTESTTARGETS = Test.o $(subst .hs,,$(TESTTARGETFILES))
f90cf44c02ac09469279126e2863a1e71358ee11Lennart PoetteringGHCVERSION = $(shell ghc --numeric-version)
8c6db8336536916d0476ff8233e0abf40a2f6aabLennart PoetteringNO_BIND_WARNING = -fno-warn-unused-do-bind
8c6db8336536916d0476ff8233e0abf40a2f6aabLennart PoetteringHC_WARN = -Wall -fno-warn-orphans $(NO_BIND_WARNING)
487393e9f11e4a06d91df03232914bd8c4b3368eLennart PoetteringHC_INCLUDE = $(addprefix -i, $(INCLUDE_PATH))
487393e9f11e4a06d91df03232914bd8c4b3368eLennart Poettering# uncomment HC_PROF for profiling (and comment out packages in var.mk)
d1ab0ca07372649dad70a0348d75e394f254e1b6Lennart Poettering# call resulting binary with a final +RTS -p to get a file <binary>.prof
dfac97b21e00cd3617ba817227db7b621841b5ccLennart Poettering# HC_PROF = -prof -auto-all -osuf p_o +RTS -K100m -RTS
d122948d6fbaac4505cf14a08f1237daa89efdd0Lennart PoetteringHC_OPTS += $(HC_WARN) $(HC_INCLUDE) $(HC_PROF)
d122948d6fbaac4505cf14a08f1237daa89efdd0Lennart Poettering# -ddump-minimal-imports
d122948d6fbaac4505cf14a08f1237daa89efdd0Lennart Poettering# uncomment the above line to generate .imports files for displayDependencyGraph
dfac97b21e00cd3617ba817227db7b621841b5ccLennart Poettering# files generated by DriFT
d122948d6fbaac4505cf14a08f1237daa89efdd0Lennart Poettering CASL/AS_Basic_CASL.hs Modal/AS_Modal.hs \
4288f619215e3dda0b75113d78e4fb7ba219ed58Lennart Poettering Syntax/AS_Structured.hs Syntax/AS_Architecture.hs Syntax/AS_Library.hs \
4288f619215e3dda0b75113d78e4fb7ba219ed58Lennart Poettering Propositional/AS_BASIC_Propositional.hs \
4288f619215e3dda0b75113d78e4fb7ba219ed58Lennart Poettering CspCASL/AS_CspCASL_Process.hs CspCASL/AS_CspCASL.hs \
871d7de47c13ee6cd78b8eefdf9128be3c740ac0Lennart Poettering RelationalScheme/AS.hs ATC/Grothendieck.hs \
4288f619215e3dda0b75113d78e4fb7ba219ed58Lennart Poettering# files to extract data types from to generate ShATermConvertible instances
4288f619215e3dda0b75113d78e4fb7ba219ed58Lennart Poetteringatc_files = Common/AS_Annotation.der.hs Common/DefaultMorphism.hs \
4288f619215e3dda0b75113d78e4fb7ba219ed58Lennart Poettering Syntax/AS_Structured.der.hs Syntax/AS_Architecture.der.hs \
01f78473b104d28db0fa813414092bc6358ae521Lennart Poettering Common/GlobalAnnotations.hs Syntax/AS_Library.der.hs \
01f78473b104d28db0fa813414092bc6358ae521Lennart Poettering Logic/Prover.hs Common/LibName.hs Common/ExtSign.hs \
4288f619215e3dda0b75113d78e4fb7ba219ed58Lennart Poettering Common/Consistency.hs Common/ProofTree.hs Static/DevGraph.hs \
42bb3074fe9632d7aa0fee825ad30d2083c3c629Ran Benita Common/Id.hs Common/Result.hs Common/OrderedMap.hs \
34c8deaae1fcfa9e7c9db49b5f3a33973e103218Lennart Poettering# files generated by genRules as input for DriFT
34c8deaae1fcfa9e7c9db49b5f3a33973e103218Lennart Poetteringatc_der_files = $(foreach file, $(atc_files), \
34c8deaae1fcfa9e7c9db49b5f3a33973e103218Lennart Poettering ATC/$(basename $(basename $(notdir $(file)))).der.hs)
cca4aeeead1985f503d175eb1fcad9ed66f2e25dLennart Poettering# the rules to create ATC .der.hs file for DriFT
cca4aeeead1985f503d175eb1fcad9ed66f2e25dLennart PoetteringATC/Result.der.hs: Common/Result.hs $(GENRULES)
db25d1d7655b1de4554942e49bc80a9b176ef8dfLennart PoetteringATC/OrderedMap.der.hs: Common/OrderedMap.hs $(GENRULES)
de47ca9b50e8c05c9fc116ff37794e526bddf92eLennart PoetteringATC/Graph.der.hs: Common/Lib/Graph.hs $(GENRULES)
5e6afdd3d359fc42de7ac432243e98673577e81fLennart PoetteringATC/ProofTree.der.hs: Common/ProofTree.hs $(GENRULES)
2f8cd170aeb0d748f5af3cefb387d14f67fc286eLennart PoetteringATC/AS_Annotation.der.hs: Common/AS_Annotation.der.hs $(GENRULES)
70449379def39da2a3efbd7c7da27a4745702b08Lennart Poettering $(GENRULECALL) -i ATC.Id -i Common.ATerm.ConvInstances -o $@ $<
683f468c54a81fd4084a2ba1082025959cd3c7d1Lennart PoetteringATC/Consistency.der.hs: Common/Consistency.hs $(GENRULES)
a2ff477f6775dcff74e32f7d0221b1b11376e84cLennart Poettering $(GENRULECALL) -x Common.Consistency.ConservativityChecker -o $@ $<
5e6afdd3d359fc42de7ac432243e98673577e81fLennart PoetteringATC/LibName.der.hs: Common/LibName.hs $(GENRULES)
5e6afdd3d359fc42de7ac432243e98673577e81fLennart Poettering $(GENRULECALL) -i ATC.Id -i Common.ATerm.ConvInstances -o $@ $<
70449379def39da2a3efbd7c7da27a4745702b08Lennart PoetteringATC/ExtSign.der.hs: Common/ExtSign.hs $(GENRULES)
70449379def39da2a3efbd7c7da27a4745702b08Lennart Poettering $(GENRULECALL) -i Common.ATerm.ConvInstances -o $@ $<
4e67ddd6b39c2847cc399ab0874427baa7ea8935Lennart PoetteringATC/DefaultMorphism.der.hs: Common/DefaultMorphism.hs $(GENRULES)
70449379def39da2a3efbd7c7da27a4745702b08Lennart PoetteringATC/AS_Structured.der.hs: Syntax/AS_Structured.der.hs $(GENRULES)
f61448083198dc0e4e0d19a916bcd478336cc85dLennart PoetteringATC/AS_Architecture.der.hs: Syntax/AS_Architecture.der.hs $(GENRULES)
52f319b29398d36ed8d1a70f68a170c0a85f401dLennart Poettering $(GENRULECALL2) -i ATC.AS_Structured -o $@ $<
670802d4b1d16c3785a695bea6e13b8bf8c8a822Lennart PoetteringATC/AS_Library.der.hs: Syntax/AS_Library.der.hs $(GENRULES)
670802d4b1d16c3785a695bea6e13b8bf8c8a822Lennart Poettering $(GENRULECALL2) -i ATC.AS_Architecture -i ATC.LibName -o $@ $<
670802d4b1d16c3785a695bea6e13b8bf8c8a822Lennart PoetteringATC/GlobalAnnotations.der.hs: Common/GlobalAnnotations.hs $(GENRULES)
670802d4b1d16c3785a695bea6e13b8bf8c8a822Lennart Poettering $(GENRULECALL) -i ATC.AS_Annotation -i ATC.Result -o $@ $<
670802d4b1d16c3785a695bea6e13b8bf8c8a822Lennart PoetteringATC/Prover.der.hs: Logic/Prover.hs $(GENRULES)
6d526de26737a0f1e8d1cf422da364d29489022eLennart Poettering $(GENRULECALL) -x Logic.Prover.ProverTemplate \
da78e1b444924a7e10bdde6eeba8e6c818169a86Lennart Poettering -i ATC.AS_Annotation -i ATC.OrderedMap -o $@ $<
5481ab2b385855b9489debe901918b2d9b27faffLennart PoetteringATC/DevGraph.der.hs: Static/DevGraph.hs $(GENRULES)
f556ea46f61bc883d5a7a01b8b55b37b5b9efffbLennart Poettering $(GENRULECALL2) -i ATC.LibName -i ATC.Consistency \
88dfa2938af09e511e4911e6984360ded0e2cd8dLennart Poettering# ATC files for every logic
ceda54d93c9c16f24737412cfbc719e01c474ef6Lennart PoetteringCASL_files = CASL/Sublogic.hs CASL/Morphism.hs CASL/Sign.hs \
a9e1f5ec36049dca715f83b2c6fc44a019e2da53Lennart PoetteringHasCASL_files = Common/Prec.hs HasCASL/As.hs HasCASL/Le.hs HasCASL/Sublogic.hs
6699c857a20378e1fd2a33e3e306a96404e7f83dLennart PoetteringPropositional_files = Propositional/Sign.hs Propositional/Morphism.hs \
6699c857a20378e1fd2a33e3e306a96404e7f83dLennart Poettering Propositional/AS_BASIC_Propositional.hs Propositional/Symbol.hs \
5b754353282e3ba3cf9c4ffc50579aff4b7d72dbKay SieversRS_files = RelationalScheme/AS.hs RelationalScheme/Sign.hs
5b754353282e3ba3cf9c4ffc50579aff4b7d72dbKay SieversModal_files = Modal/AS_Modal.hs Modal/ModalSign.hs
5b754353282e3ba3cf9c4ffc50579aff4b7d72dbKay SieversTemporal_files = Temporal/AS_BASIC_Temporal.hs Temporal/Sign.hs \
5e6afdd3d359fc42de7ac432243e98673577e81fLennart PoetteringConstraintCASL_files = ConstraintCASL/AS_ConstraintCASL.hs
93a45c562a1989dfbb2dd08c65f8a21b02959934Lennart PoetteringCoCASL_files = CoCASL/AS_CoCASL.hs CoCASL/CoCASLSign.hs
dfac97b21e00cd3617ba817227db7b621841b5ccLennart PoetteringCspCASL_files = CspCASL/AS_CspCASL.hs CspCASL/AS_CspCASL_Process.hs \
addab137cd8d318e4f543ca56018ee23d51aaca9Lennart PoetteringCASL_DL_files = CASL_DL/AS_CASL_DL.hs CASL_DL/Sign.hs CASL_DL/Sublogics.hs
97c4a07df982ee967705022feaba9be33947abf0Lennart PoetteringOWL_files = OWL/Sign.hs OWL/Sublogic.hs OWL/Morphism.hs
cd6d0a456bc9c45fa79316fc5896e4a3ae75a30bLennart PoetteringDFOL_files = DFOL/AS_DFOL.hs DFOL/Sign.hs DFOL/Morphism.hs DFOL/Symbol.hs
4bb2357f77c875976de5e238a5783e4e136b37b5Lennart PoetteringMaude_files = Maude/Sign.hs Maude/Morphism.hs Maude/Sentence.hs \
3b63d2d31d0850bd7a81ab9b468218d2c4c461e8Lennart PoetteringExtModal_files = ExtModal/AS_ExtModal.hs ExtModal/ExtModalSign.hs \
306a7fd82e790b3c00ba5cf806ccd6c0108061b5Lennart PoetteringCommonLogic_files = CommonLogic/AS_CommonLogic.hs CommonLogic/Sign.hs
8e1bd70d4ce6d3881c1df6a6482643a2b3a69bb1Lennart Poettering# ATC DrIFT-rule generation for logics
151b190e79e64824552e01849352ca8f6ac7dedbLennart PoetteringCASL/ATC_CASL.der.hs: $(CASL_files) $(GENRULES)
46574a5b4afeac0c3f69f15ce47c460309cb9becLennart Poettering $(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(CASL_files)
46574a5b4afeac0c3f69f15ce47c460309cb9becLennart PoetteringRelationalScheme/ATC_RelationalScheme.der.hs: $(RS_files) $(GENRULES)
a9e1f5ec36049dca715f83b2c6fc44a019e2da53Lennart Poettering $(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(RS_files)
335aa753fa60ba0bb3c9fe679c761d5f1f3b1588Lennart PoetteringPropositional/ATC_Propositional.der.hs: $(Propositional_files) $(GENRULES)
de47ca9b50e8c05c9fc116ff37794e526bddf92eLennart Poettering $(GENRULECALL) -i ATC.AS_Annotation -o $@ $(Propositional_files)
d1ab0ca07372649dad70a0348d75e394f254e1b6Lennart PoetteringHasCASL/ATC_HasCASL.der.hs: $(HasCASL_files) $(GENRULES)
af2d49f70bcff20efaf2d69aecaf4b3e898ff1faLennart Poettering $(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(HasCASL_files)
af2d49f70bcff20efaf2d69aecaf4b3e898ff1faLennart PoetteringIsabelle/ATC_Isabelle.der.hs: $(Isabelle_files) $(GENRULES)
af2d49f70bcff20efaf2d69aecaf4b3e898ff1faLennart PoetteringModal/ATC_Modal.der.hs: $(Modal_files) $(GENRULES)
af2d49f70bcff20efaf2d69aecaf4b3e898ff1faLennart Poettering $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(Modal_files)
e24067c3ec0e16e94e9620d4f7a06ccc4b637eb4Lennart PoetteringTemporal/ATC_Temporal.der.hs: $(Temporal_files) $(GENRULES)
5e6afdd3d359fc42de7ac432243e98673577e81fLennart Poettering $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(Temporal_files)
5b754353282e3ba3cf9c4ffc50579aff4b7d72dbKay SieversConstraintCASL/ATC_ConstraintCASL.der.hs: $(ConstraintCASL_files) $(GENRULES)
705dbf3aa3e95a4e591dcbc79774708d71b0e2e8Lennart Poettering $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(ConstraintCASL_files)
70fcff314feff469a8e61dbe5017ed74f5e0a09dLennart PoetteringCASL_DL/ATC_CASL_DL.der.hs: $(CASL_DL_files) $(GENRULES)
70fcff314feff469a8e61dbe5017ed74f5e0a09dLennart Poettering $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(CASL_DL_files)
addab137cd8d318e4f543ca56018ee23d51aaca9Lennart PoetteringCoCASL/ATC_CoCASL.der.hs: $(CoCASL_files) $(GENRULES)
b2423f1f436f847d9fc96a63679be2b5552b6bafLennart Poettering $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(CoCASL_files)
449ddb2d23a63ca4c8cd70d13a070fba87c1fb30Lennart PoetteringCOL/ATC_COL.der.hs: $(COL_files) $(GENRULES)
cd6d0a456bc9c45fa79316fc5896e4a3ae75a30bLennart Poettering $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(COL_files)
ca2cab5dcd3d29f45992a439f54e48faad764c6eLennart PoetteringCspCASL/ATC_CspCASL.der.hs: $(CspCASL_files) $(GENRULES)
ca2cab5dcd3d29f45992a439f54e48faad764c6eLennart Poettering $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(CspCASL_files)
4bb2357f77c875976de5e238a5783e4e136b37b5Lennart PoetteringSoftFOL/ATC_SoftFOL.der.hs: $(SoftFOL_files) $(GENRULES)
c7b508592b28ee1e62350f0d249856811371f631Lennart Poettering $(GENRULECALL) -i ATC.AS_Annotation -o $@ $(SoftFOL_files)
3b63d2d31d0850bd7a81ab9b468218d2c4c461e8Lennart PoetteringOWL/ATC_OWL.der.hs: $(OWL_files) $(GENRULES)
447be1550523114f96c7f9eacb9d6a1ff6ca4197Lennart Poettering $(GENRULECALL) -i OWL.ReadWrite -o $@ $(OWL_files)
8cf3a8a982661c0bb9b04ff27f6d486b38b1b35eLennart PoetteringVSE/ATC_VSE.der.hs: $(VSE_files) $(GENRULES)
8e1bd70d4ce6d3881c1df6a6482643a2b3a69bb1Lennart Poettering $(GENRULECALL) -x VSE.As.FoldRec -i CASL.ATC_CASL -o $@ $(VSE_files)
46574a5b4afeac0c3f69f15ce47c460309cb9becLennart PoetteringOMDoc/ATC_OMDoc.der.hs: $(OMDoc_files) $(GENRULES)
46574a5b4afeac0c3f69f15ce47c460309cb9becLennart Poettering $(GENRULECALL) -i OMDoc.ATerm -o $@ $(OMDoc_files)
85ed27f699939f75b8422ae67e016bdf9f439da9Lennart PoetteringDFOL/ATC_DFOL.der.hs: $(DFOL_files) $(GENRULES)
af2d49f70bcff20efaf2d69aecaf4b3e898ff1faLennart Poettering $(GENRULECALL) -i ATC.AS_Annotation -o $@ $(DFOL_files)
335aa753fa60ba0bb3c9fe679c761d5f1f3b1588Lennart Poettering $(GENRULECALL) -i ATC.AS_Annotation -o $@ $(LF_files)
25705583af79130d2692de297ac971f3cf165619Lennart PoetteringMaude/ATC_Maude.der.hs: $(Maude_files) $(GENRULES)
3eb4d9a214a09883e50ce557b36c7903406d7ef8Kay Sievers $(GENRULECALL) -i ATC.AS_Annotation -o $@ $(Maude_files)
5e6afdd3d359fc42de7ac432243e98673577e81fLennart PoetteringExtModal/ATC_ExtModal.der.hs: $(ExtModal_files) $(GENRULES)
5e6afdd3d359fc42de7ac432243e98673577e81fLennart Poettering $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(ExtModal_files)
5e6afdd3d359fc42de7ac432243e98673577e81fLennart PoetteringCommonLogic/ATC_CommonLogic.der.hs: $(CommonLogic_files) $(GENRULES)
cd3f8b7ddb052ab5e4eab420968bae689db3899aJeff Mahoney $(GENRULECALL) -i ATC.AS_Annotation -o $@ $(CommonLogic_files)
cd3f8b7ddb052ab5e4eab420968bae689db3899aJeff Mahoney# all ATC .der.hs files for all logics
1de4d79bf554946f486adf56ed765c5335816f15Andrey Borzenkovatc_logic_files = $(foreach logic, $(logics), $(logic)/ATC_$(logic).der.hs)
1de4d79bf554946f486adf56ed765c5335816f15Andrey Borzenkovgenerated_rule_files = $(atc_der_files) $(atc_logic_files)
1de4d79bf554946f486adf56ed765c5335816f15Andrey Borzenkov# a rule to create all .der.hs files
196e3fa74a88a04b0ecec7d3af648287dd088f8aMiklos Vajna# the final ATC target files created by DriFT
196e3fa74a88a04b0ecec7d3af648287dd088f8aMiklos Vajnagendrifted_files = $(patsubst %.der.hs, %.hs, $(generated_rule_files))
196e3fa74a88a04b0ecec7d3af648287dd088f8aMiklos Vajna# files to be processed by utils/InlineAxioms
196e3fa74a88a04b0ecec7d3af648287dd088f8aMiklos Vajnainline_axiom_files = Comorphisms/Modal2CASL.hs CASL_DL/PredefinedSign.hs
cd3f8b7ddb052ab5e4eab420968bae689db3899aJeff Mahoneygen_inline_axiom_files = $(patsubst %.hs,%.inline.hs, $(inline_axiom_files))
cd3f8b7ddb052ab5e4eab420968bae689db3899aJeff Mahoney# all sources that need to be created before ghc can be called
cd3f8b7ddb052ab5e4eab420968bae689db3899aJeff Mahoneyderived_sources += $(drifted_files) Driver/Version.hs $(happy_files) \
aa2e2115873e102b8f6701f4211ddf7bec4c5e10Lennart Poettering $(inline_axiom_files) Modal/ModalSystems.hs $(hs_der_files)
cd3f8b7ddb052ab5e4eab420968bae689db3899aJeff Mahoney####################################################################
aa2e2115873e102b8f6701f4211ddf7bec4c5e10Lennart Poettering.PHONY : all hets-opt hets-optimized clean o_clean clean_pretty \
aa2e2115873e102b8f6701f4211ddf7bec4c5e10Lennart Poettering real_clean bin_clean package_clean distclean packages \
aa2e2115873e102b8f6701f4211ddf7bec4c5e10Lennart Poettering programatica_pkg aterm_pkg maintainer-clean annos \
aa2e2115873e102b8f6701f4211ddf7bec4c5e10Lennart Poettering check capa hacapa h2h h2hf showKP clean_genRules genRules \
aa2e2115873e102b8f6701f4211ddf7bec4c5e10Lennart Poettering count doc fromKif derivedSources release cgi ghci build
aa2e2115873e102b8f6701f4211ddf7bec4c5e10Lennart Poettering.SECONDARY : %.hs %.d $(generated_rule_files) $(gen_inline_axiom_files)
d0b4880988c5900c0f951aa6fe700686411cd03eLennart Poetteringaterm_sources = $(wildcard atermlib/src/ATerm/*.hs)
8c6db8336536916d0476ff8233e0abf40a2f6aabLennart Poettering echo "of aterm package found"; else \
4927fcae48de061393b3ce9c12d49f80d73fbf1dLennart Poettering ghc --make GUI/hets_cgi.hs -o $@ $(HC_OPTS) -O
4927fcae48de061393b3ce9c12d49f80d73fbf1dLennart Poettering @echo 'File : Maintainer' > $@
d3f09cf39637de2441288b5e4c93eecbd1fb872dKay Sievers# count lines of code
d3f09cf39637de2441288b5e4c93eecbd1fb872dKay Sievers# Documentation via haddock
d3f09cf39637de2441288b5e4c93eecbd1fb872dKay SieversHADDOCK_OPTS = $(addprefix --optghc=, $(HC_OPTS))
01f78473b104d28db0fa813414092bc6358ae521Lennart Poettering -t 'Hets - the Heterogeneous Tool Set' \
d3f09cf39637de2441288b5e4c93eecbd1fb872dKay Sievers Syntax/ADoc.hs $(filter-out Test.hs, $(wildcard *.hs)) \
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering (cd utils/DrIFT-src; $(HC) --make DrIFT.hs -o ../DrIFT)
871d7de47c13ee6cd78b8eefdf9128be3c740ac0Lennart Poettering$(GENRULES): $(DRIFT) $(GENERATERULES_deps)
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering $(HC) --make -i../DrIFT-src -i../.. $(HC_WARN) \
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering# "-package hssource" for ghc-5.04.2
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering $(HC) --make utils/InlineAxioms/InlineAxioms.hs $(HC_WARN) $(HC_PROF) \
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poetteringutils/appendHaskellPreludeString: utils/appendHaskellPreludeString.hs
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering# release management
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering svn co https://svn-agbkb.informatik.uni-bremen.de/Hets/$(REV) Hets
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering if [ -d ../uni ] ; then ln -s ../uni uni ; fi
8c6db8336536916d0476ff8233e0abf40a2f6aabLennart Poettering if [ -d ../programatica ] ; then \
52661efd21608dc7e0ac26b714a9254ed6180ddbLennart Poettering ln -s ../../programatica/tools programatica/tools ; fi
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering (cd Hets; $(MAKE) derivedSources; $(MAKE) clean; \
4927fcae48de061393b3ce9c12d49f80d73fbf1dLennart Poettering find . -name .svn -o -name \*.o -o -name \*.hi | xargs $(RM) -r; \
4927fcae48de061393b3ce9c12d49f80d73fbf1dLennart Poettering $(RM) clean.*; utils/replaceAllHeaders.sh)
139be57d9441b5c890e1e4ee69e15aad03276fdeLennart Poetteringutils/genItCorrections: $(GENITCORRECTIONS_deps)
139be57d9441b5c890e1e4ee69e15aad03276fdeLennart Poetteringpretty/LaTeX_maps.hs: utils/words.pl utils/genItCorrections \
139be57d9441b5c890e1e4ee69e15aad03276fdeLennart Poettering pretty/words.input pretty/fonts.input pretty/width-table.tex.templ
7a58bfa4aef88c9ddead6668d83640f762938e72Daniel J Walsh @echo -n "Generating pretty/LaTeX_maps.hs ... "
4927fcae48de061393b3ce9c12d49f80d73fbf1dLennart Poettering @(cd pretty >/dev/null; $(PERL) ../utils/words.pl > words.pl.log)
139be57d9441b5c890e1e4ee69e15aad03276fdeLennart Poettering @(cd pretty >/dev/null; ../utils/genItCorrections \
2f6a1ab18e8372ea9e77df4f1f9fdaac78396b10Michael Biebl gen_it_characters gen_it_words >> LaTeX_maps.hs)
2f6a1ab18e8372ea9e77df4f1f9fdaac78396b10Michael Biebl @echo "ready"
2f6a1ab18e8372ea9e77df4f1f9fdaac78396b10Michael Biebl @echo "please copy the file manually to Common"
9a1ac7b9ae2fb218170d1bd106d5351a76d03a95Lennart Poettering $(RM) $(generated_rule_files) $(gendrifted_files) $(hspp_sources) \
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering### removes all *.o, *.hi and *.p_o files in all subdirectories
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering find . -name \*.o -o -name \*.hi -o -name \*.p_o \
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering -o -name \*.exe -o -name \*.exe.manifest | xargs $(RM)
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering### remove binaries
cd6d0a456bc9c45fa79316fc5896e4a3ae75a30bLennart Poettering $(RM) pretty/*.c.* pretty/*.h.* pretty/gen_it_* \
26e190cf872226b46c2806c8120a394ad97b62faKay Sievers### additionally removes the library files
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering### clean user packages
160cd5c9aa2301892e13950015de7968c764340dLennart Poettering $(HCPKG) unregister programatica --user || exit 0
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering $(HCPKG) unregister aterm --user || exit 0
fa776d8e962da9d90459e2f3e86a2a0c6366ee12Lennart Poettering### additionally removes generated files not in the CVS tree
c5abba08873903d80a2dcdd46aace959fcae1b0fLennart Poettering $(RM) Modal/GeneratePatterns.inline.hs utils/appendHaskellPreludeString
f9378423b9758861850748aeb49ae0d3300e56e6Lennart Poettering $(RM) utils/DrIFT utils/genRules $(INLINEAXIOMS)
6624768c9c39ab409edebe07cb06ecd93cc6f3edLennart Poettering $(RM) utils/genItCorrections pretty/LaTeX_maps.hs pretty/words.pl.log
f9378423b9758861850748aeb49ae0d3300e56e6Lennart Poettering $(RM) -r $(HOME)/.ghc/$(ARCH)-$(OSBYUNAME)-hets-packages
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering### interactive
e0cabd4bb536bce3a9636a12b8dbc512c28c2395Lennart Poettering### build only, don't link
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering### Annos parser
359957ee23e8dad97f6c75969d7ecfe4d3c4369fLennart Poettering### CASL parser
160cd5c9aa2301892e13950015de7968c764340dLennart Poettering### HasCASL parser
6a7e63eff2a03be705342f6c33d2aada01a9f544Lennart Poettering### Haskell analysis
ee48647271132188e9ecc3507e62b6c7c7a6c9ebLennart Poettering### Haskell to Isabelle-HOLCF translation
151b190e79e64824552e01849352ca8f6ac7dedbLennart PoetteringHaskell/h2hf: Haskell/h2hf.hs Haskell/*.hs Isabelle/*.hs Common/*.hs \
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering### HasCASL to Haskell translation
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering### test program to check the known provers
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering### run tests in other directories
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering for i in $(TESTDIRS); do $(MAKE) -C $$i check; done
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering## Preparing the version of Hets
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart PoetteringDriver/Version.hs: Driver/Version.in version_nr
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering LANG=C $(PERL) utils/build_version.pl version_nr \
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering## two hardcoded dependencies for a correct generation of Version.hs
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart PoetteringDriver/Options.hs Driver/WriteFn.hs Driver/ReadFn.hs: Driver/Version.hs
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering## two dependencies to avoid circular prerequisites
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart PoetteringCASL_DEPENDENT_BINARIES = hets CASL/capa CASL/fromKif \
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering Common/annos Common/test_parser Comorphisms/test/showKP \
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering CspCASL/print_csp HasCASL/hacapa Haskell/h2h Haskell/h2hf \
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering Haskell/hana Haskell/wrap Isabelle/isa Syntax/hetpa
9f2c5942e1e10099027f0da438aafdd9f40440baLennart Poettering$(CASL_DEPENDENT_BINARIES): $(derived_sources)
d1ab0ca07372649dad70a0348d75e394f254e1b6Lennart Poettering## suffix rules
d1ab0ca07372649dad70a0348d75e394f254e1b6Lennart Poettering## rule for GHC
6f6083dc73c4bdd48678456fa6b969d6f1152373Lennart Poettering## rule for HAPPY
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering echo "{-# OPTIONS -w #-}" > $@
10e87ee7f66b59a504c0ed2025463ba5faa69923Lennart Poettering## rule for DrIFT
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering ($(DRIFT_ENV); export DERIVEPATH; $(DRIFT) $< > $@)
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering## rule for inlineAxioms
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering## rule for cpp and haddock
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering -DUNI_PACKAGE -DCASLEXTENSIONS -DPROGRAMATICA -optP -P $<
47be870bd83fb3719dffc3ee9348a409ab762a14Lennart Poettering## compiling rules for object and interface files
15ae422b7471cf6f41ccf450243d8afd8ea0a054Lennart Poettering## compiling rules for dependencies
e99e38bbdcca3fe5956823bdb3d38544ccf93221Lennart Poettering $(HC) -M $< $(HC_OPTS) -optdep-f -optdep$@
139be57d9441b5c890e1e4ee69e15aad03276fdeLennart Poettering $(HC) -M $< $(HC_OPTS) -optdep-f -optdep$@
139be57d9441b5c890e1e4ee69e15aad03276fdeLennart Poettering## Rule to generate hs files from glade files. Needed for GTK
e59077036bcf5a041e336f04cb0d2f7d18d489a1Lennart Poettering%.hs: %.glade utils/appendHaskellPreludeString \
e59077036bcf5a041e336f04cb0d2f7d18d489a1Lennart Poettering cat GUI/Glade/Template.append.hs | sed "s/\%s/$$b/" | \
e59077036bcf5a041e336f04cb0d2f7d18d489a1Lennart Poettering## generate the inline file for the predefined CASL_DL sign
2f6a1ab18e8372ea9e77df4f1f9fdaac78396b10Michael Biebl CASL_DL/PredefinedSign.inline.hs.in utils/appendHaskellPreludeString \
2f6a1ab18e8372ea9e77df4f1f9fdaac78396b10Michael Biebl utils/appendHaskellPreludeString CASL_DL/PredDatatypes.het \
139be57d9441b5c890e1e4ee69e15aad03276fdeLennart Poettering echo " )" >> $@
8c6db8336536916d0476ff8233e0abf40a2f6aabLennart Poettering# Warning: Don't change the order of the depencies!!
8c6db8336536916d0476ff8233e0abf40a2f6aabLennart PoetteringCASL_DL/PredDatatypes.het: utils/transformLibAsBasicSpec.pl \
8c6db8336536916d0476ff8233e0abf40a2f6aabLennart Poettering## rule for Modal/ModalSystems.hs needed for ModalLogic Translation
c24eb49e6aecd6de2ad450083e826d4c9d9c75b6Lennart Poettering# uses intransparently utils/outlineAxioms
c24eb49e6aecd6de2ad450083e826d4c9d9c75b6Lennart PoetteringModal/ModalSystems.hs: Modal/GeneratePatterns.inline.hs.in \
c24eb49e6aecd6de2ad450083e826d4c9d9c75b6Lennart Poettering utils/genTransMFormFunc.pl $(INLINEAXIOMS)
c24eb49e6aecd6de2ad450083e826d4c9d9c75b6Lennart Poettering# directory for installers
f90cf44c02ac09469279126e2863a1e71358ee11Lennart Poettering# or `date +%F`
f90cf44c02ac09469279126e2863a1e71358ee11Lennart Poettering# prepare installer creation
f90cf44c02ac09469279126e2863a1e71358ee11Lennart Poettering sed "s/^\(HETS_VERSION =\).*/\1$(HETS_VERSION)/" Makefile.installer \
0213c3f8102bdc934c629d11a44ca0b408762287Lennart Poettering @echo " -> make"
2f6a1ab18e8372ea9e77df4f1f9fdaac78396b10Michael Biebl# check out java parts for OWL