Makefile revision d0279930f87bf39843e0bd2992a4789322662144
77b179cbbe7b820b5d838a675200a7b87eb12dacMark Andrews# Author: (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2005
24f2cc7d06e4bb6625f90323e44b42e0cad63588Mukund Sivaraman# This Makefile will compile the new hets system and provides also
73eacba1f107468b30e8aa7cd6e213bb2d7f3142Evan Hunt# targets for test programs during implementation phases.
73eacba1f107468b30e8aa7cd6e213bb2d7f3142Evan Hunt# !!! Note: This makefile is written for GNU make !!!
73eacba1f107468b30e8aa7cd6e213bb2d7f3142Evan Hunt# (gmake on solaris)
1b05d22789fd9a17aca4f459639bc2b6848c3160Mark Andrews####################################################################
29d52c001ff976561669375cf0c866b815a90c49Mark Andrews## Some varibles, which control the compilation
7ae96d882326357448f8f440c52f47ac1b1fa455Evan HuntHAIFA_PATHS = Network Network/Server Org Org/W3 Org/W3/N2001 \
7ae96d882326357448f8f440c52f47ac1b1fa455Evan Hunt Org/Xmlsoap Org/Xmlsoap/Schemas Org/Xmlsoap/Schemas/Soap \
7ae96d882326357448f8f440c52f47ac1b1fa455Evan Hunt Text Text/XML Text/XML/HXT Text/XML/Schema Text/XML/Schema/TypeMapper \
29d52c001ff976561669375cf0c866b815a90c49Mark Andrews utils utils/DrIFT-src utils/GenerateRules utils/InlineAxioms Common \
a8da00ef95ba37b9d071c2b8db1a0c967e060106Mark Andrews Common/Lib Common/ATerm Logic CASL CASL/CCC CASL/CompositionTable \
a8da00ef95ba37b9d071c2b8db1a0c967e060106Mark Andrews Syntax Static GUI HasCASL Haskell Modal CoCASL COL ConstraintCASL \
48fe77df0c604359c3a406510f4327fc3182e836Evan Hunt CspCASL ATC Proofs Comorphisms Isabelle Driver Modifications \
5f590e93d2ec1372a591b943a375506817787d8aMukund Sivaraman Taxonomy CASL_DL SoftFOL OWL OMDoc PGIP Propositional RelationalScheme \
be9720ae2c2e933da36c5fb209dd4798a0337febMark Andrews# the 'replacing spaces' example was taken from the (GNU) Make info manual
bb5df338d9b119bb2fe18dea9b0e3034c3925f7bMark AndrewsDRIFT_ENV = DERIVEPATH=$(subst $(space),:,$(PFE_PATHS))
f5ea8d2838e0d9279d00afe984aa67f07ad758b1Mark Andrews# override on commandline for other architectures
af669cb4fd7ecfb67ed145b176e5e764b249573bMark Andrews /home/www/agbkb/forschung/formal_methods/CoFI/hets/`utils/sysname.sh`
044008f58f66d7a1b50c1dfc09cf8049e83a8227Evan HuntGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps)
044008f58f66d7a1b50c1dfc09cf8049e83a8227Evan HuntGENITCORRECTIONS_deps = utils/itcor/GenItCorrections.hs
1783676a64b8e390b756d775ae152509f1d76719Mukund SivaramanINLINEAXIOMS_deps = utils/InlineAxioms/InlineAxioms.hs \
84f95ddb2572641022619950a211aff49e331c98Mukund Sivaraman Common/Doc.hs CASL/ToDoc.hs Modal/AS_Modal.hs \
84f95ddb2572641022619950a211aff49e331c98Mukund Sivaraman Modal/Parse_AS.hs Modal/ModalSign.hs Modal/Print_AS.hs Modal/StatAna.hs
db93c0def5c3e1e0ea40c7596482ad3fca4ed03bMukund SivaramanGENRULECALL = $(GENRULES) -r Typeable -r ShATermConvertible \
177e523c48674936078c1422403840de159db5dfEvan HuntSETUPPREFIX = --prefix=$(HOME)/.ghc/$(ARCH)-$(OSBYUNAME)-hets-packages
7acc2f21563b79229d592f09dde17e60d64afc8fEvan Hunt ../$(SETUP) build; ../$(SETUP) haddock; ../$(SETUP) install --user
7acc2f21563b79229d592f09dde17e60d64afc8fEvan HuntHAXMLVERSION = $(shell $(HCPKG) field HaXml version)
e58eb371a047c3a8aee4ce9aaca0f7f3673432a4Mukund Sivaraman# remove -fno-warn-orphans for older ghcs and add -ifgl
e58eb371a047c3a8aee4ce9aaca0f7f3673432a4Mukund SivaramanHC_FLAGS = $(HC_WARN) -fglasgow-exts -fallow-overlapping-instances
2ff2145ff53ec10df0e3c9c51906d63187fd54faMark Andrews# -ddump-minimal-imports
2ff2145ff53ec10df0e3c9c51906d63187fd54faMark Andrews# uncomment to above line to generate .imports files for displayDependencyGraph
f4102ab13ea049d73f5523c1a94fe2b83c408c9eMark Andrewslogics = CASL HasCASL Isabelle Modal CoCASL COL CspCASL CASL_DL SoftFOL \
a98f70acc8d36bf73c000808ffed455ad8f15b02Evan Hunt ConstraintCASL Propositional OWL DL RelationalScheme VSE
8b61aef4dcc53267a500449058c0af705e3a64d1Evan HuntTESTTARGETFILES += CASL/fromKif.hs CASL/capa.hs HasCASL/hacapa.hs \
2616cb69443f6ccd1900901c91e04d86886a7197Evan Hunt ATC/ATCTest.hs ATC/ATCTest2.hs Common/ATerm/ATermLibTest.hs \
e785f9c1c7d838b9a773a757210388130eba5c4aMark Andrews Common/ATerm/ATermDiffMain.hs Common/annos.hs Common/test_parser.hs \
e785f9c1c7d838b9a773a757210388130eba5c4aMark Andrews SoftFOL/tests/PrintTPTPTests.hs Comorphisms/test/showKP.hs \
e785f9c1c7d838b9a773a757210388130eba5c4aMark Andrews SoftFOL/tests/soapTest.hs Comorphisms/test/sublogicGraph.hs \
591389c7d44e5ca20c357627dd179772cfefaaccEvan HuntUNI_PACKAGE_CONF = $(wildcard ../uni/uni-package.conf)
591389c7d44e5ca20c357627dd179772cfefaaccEvan HuntHC_PACKAGE = -package-conf $(UNI_PACKAGE_CONF) -package uni-davinci \
591389c7d44e5ca20c357627dd179772cfefaaccEvan Hunt# some modules from uni for haddock
591389c7d44e5ca20c357627dd179772cfefaaccEvan Hunt# if uni/server is included also HaXml sources are needed
591389c7d44e5ca20c357627dd179772cfefaaccEvan Huntuni_dirs = ../uni/davinci ../uni/graphs ../uni/events \
1059bc2e42e8214f8b73d3b4cd181d8394a94a6aFrancis Dupontuni_sources = $(wildcard $(addsuffix /haddock/*.hs, $(uni_dirs))) \
801fb8b894c75fc1e3fa0284e096ade6dcdc1110Evan Hunt Taxonomy/taxonomyTool.hs SoftFOL/tests/CMDL_tests.hs \
4eefa351cc5549a2cebb45d274f10249e31f6945Mukund Sivaraman### list of directories to run checks in
fe12a8f1077c1556922f1a3be2f592c761917838Mukund Sivaramanhs_clean_files = Haskell/TiATC.hs Haskell/TiDecorateATC.hs \
e77ef50a57091eeb70d0a6d021638c92442c8f0aMark AndrewsPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
4b36b9c1fff56d836feeaa1dc7eb1d4676d9c8bbMark Andrews base/parse2/LexerGen base/parse2/LexerSpec base/tests/HbcLibraries \
4b36b9c1fff56d836feeaa1dc7eb1d4676d9c8bbMark Andrews base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
9175a4ed6325e611d4c95d74f6e447a3f4b50fa0Evan Hunt base/transforms base/transforms/Deriving property \
9175a4ed6325e611d4c95d74f6e447a3f4b50fa0Evan Hunt property/syntax property/AST property/transforms \
9175a4ed6325e611d4c95d74f6e447a3f4b50fa0Evan Hunt property/TI property/defs property/parse2 property/parse2/Parser
84ee90b52d4fb443c796f4e1481f98d5a95b5614Evan HuntPFE_PATHS = $(addprefix $(PFE_TOOLDIR)/, $(PFE_DIRS))
84ee90b52d4fb443c796f4e1481f98d5a95b5614Evan Huntpfe_sources = $(wildcard $(addsuffix /*hs, $(PFE_PATHS)))
875574f1e4e87d8412b682084991954c10c20e35Mark AndrewsPFE_FLAGS = -package programatica -DPROGRAMATICA
875574f1e4e87d8412b682084991954c10c20e35Mark Andrewshappy_files += $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs
17dc146c7c2399e7bd64e776775535b9484ad1d5Mark Andrewsprogramatica_pkg: $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs \
2817aa56ca12139849ba1017ff978833174f6294Evan Hunt echo "of programatica package found"; else \
22e3e00ac95ec1ba89200c5d0e05670ed5ad8fefMark Andrews -i `pwd`/Haskell/Programatica.patch || exit 0); \
22e3e00ac95ec1ba89200c5d0e05670ed5ad8fefMark Andrews cp -f utils/programatica.cabal ../programatica/tools; \
b88b75c2b88618f9c885c61e1ab0bd1cddd4474eEvan Hunt echo "{-# OPTIONS -w #-}" > $@
b88b75c2b88618f9c885c61e1ab0bd1cddd4474eEvan Hunt$(LEX_DIR)Gen/HsLexerGen: $(LEX_DIR)Gen/*.hs $(LEX_DIR)Spec/*.hs \
cc0a48a38173637f7a833e2da52bcfbcecb960b4Mark Andrews -i$(LEX_DIR) -i$(LEX_DIR)Gen -i$(LEX_DIR)Spec \
f8eb4e5bfd1129d7639af5c2c768f53f0895952aMark Andrewsderived_sources += Haskell/PreludeString.hs $(LEX_DIR)/HsLex.hs \
b05a50c852608a40d1a06d6124bafb9b500c10c1Mukund Sivaramanutils/appendHaskellPreludeString: utils/appendHaskellPreludeString.hs
f91c369b4ac84fad07e3106c5c00a15d87250d1eMukund SivaramanAPPENDPRELUDESTRING = utils/appendHaskellPreludeString \
f91c369b4ac84fad07e3106c5c00a15d87250d1eMukund Sivaraman## rule for appendHaskellPreludeString
a6f0e9c985220f0e4509777e6528afb64e0ad576Mukund SivaramanHaskell/PreludeString.hs: Haskell/PreludeString.append.hs \
f4dda9cf28f8be880097ee931b3237e09731a28aMark AndrewsAst_Haskell_files = HsDeclStruct HsExpStruct HsFieldsStruct \
f4dda9cf28f8be880097ee931b3237e09731a28aMark Andrews HsGuardsStruct HsKindStruct HsPatStruct HsTypeStruct HsAssocStruct \
79521569952d5e2475f05e4397dc976f4685056eMark Andrews#Ti_Haskell_files = TiTypes TiKinds TiDecorate TiInstanceDB
d1f1f13c7fc1f1515930053508f1645cfafaa478Mark Andrews#Ti_Prop_files = property/TI/TiPropDecorate property/syntax/PropSyntaxRec
74eb2f5cbc98d9646bcd13ffcb17688f0db5ab8dEvan HuntOther_PFE_files = property/AST/HsPropStruct base/defs/PNT \
74eb2f5cbc98d9646bcd13ffcb17688f0db5ab8dEvan Hunt base/defs/UniqueNames base/Modules/TypedIds base/Modules/Ents \
74eb2f5cbc98d9646bcd13ffcb17688f0db5ab8dEvan Hunt $(addprefix $(PFE_TOOLDIR)/base/AST/, $(Ast_Haskell_files)) \
b0c18fffd3c81d3cb617dbba4d222d49ae266f28Mark Andrews## rule for ATC generation
b0c18fffd3c81d3cb617dbba4d222d49ae266f28Mark AndrewsHaskell/ATC_Haskell.der.hs: $(Haskell_files) $(GENRULES)
b0c18fffd3c81d3cb617dbba4d222d49ae266f28Mark Andrews $(GENRULECALL) -i Haskell.BaseATC -o $@ $(Haskell_files)
44032d3918d4aeb2f0cff3bb90e4a44569016559Mark AndrewsTESTTARGETFILES += Haskell/hana.hs Haskell/h2h.hs Haskell/h2hf.hs
1e0ed0c6f5c359df88767e2c4f0fda24f2da0468Mark AndrewsTESTTARGETS = Test.o $(subst .hs,,$(TESTTARGETFILES))
1e0ed0c6f5c359df88767e2c4f0fda24f2da0468Mark Andrews### Profiling (only for debugging)
1e0ed0c6f5c359df88767e2c4f0fda24f2da0468Mark Andrews### Attention every module must be compiled with profiling or the linker
1e0ed0c6f5c359df88767e2c4f0fda24f2da0468Mark Andrews### cannot link the various .o files properly. So after switching on
1e0ed0c6f5c359df88767e2c4f0fda24f2da0468Mark Andrews### Profiling, do an 'gmake real_clean; gmake'
1e0ed0c6f5c359df88767e2c4f0fda24f2da0468Mark Andrews### Comment in the following line for switching on profiling.
3bdcd91c456adec12ee9f69cfe6b0f79174f78c4Evan Hunt# HC_PROF = -prof -auto-all -osuf p_o +RTS -K100m -RTS
1e0ed0c6f5c359df88767e2c4f0fda24f2da0468Mark AndrewsHC_OPTS = $(HC_FLAGS) $(HC_INCLUDE) $(HC_PROF) $(HAXML_PACKAGE) $(HC_PACKAGE) \
1e0ed0c6f5c359df88767e2c4f0fda24f2da0468Mark Andrews####################################################################
1e0ed0c6f5c359df88767e2c4f0fda24f2da0468Mark Andrews## sources for hets
47d837a49967a6a1b290024f5efb0669276013b1Mukund Sivaramannon_sources = Common/LaTeX_maps.svmono.hs Common/CaslLanguage.hs ./Test.hs \
47d837a49967a6a1b290024f5efb0669276013b1Mukund Sivaramansources = hets.hs $(filter-out $(non_sources), \
47d837a49967a6a1b290024f5efb0669276013b1Mukund Sivaraman $(wildcard $(addsuffix /[A-Z]*hs, $(SOURCE_PATHS))))
03fd9cb81c2a92cf54baab5103db10e8ef9d524aMark Andrews Syntax/AS_Structured.hs Syntax/AS_Architecture.hs Syntax/AS_Library.hs \
dc5e29a7d216b4233c80bec8967015aa9c05962eTinderbox User CspCASL/AS_CspCASL_Process.hs CspCASL/AS_CspCASL.hs \
017aa9aef63aaef6a370c180f6290b8388deda01Mark Andrewsatc_files = Common/AS_Annotation.der.hs Common/DefaultMorphism.hs \
09290020bc9b3cd787f1a19e400413a6ca6827e3Evan Hunt Syntax/AS_Structured.der.hs Syntax/AS_Architecture.der.hs \
2ce24e13faacaf73286298f0068a7e7f0d03fdacMark Andrews Common/GlobalAnnotations.hs Syntax/AS_Library.der.hs \
693d70f96fc2b3c1830580edcc29146afd6a9f61Mark Andrews Logic/Prover.hs Common/ExtSign.hs Static/DevGraph.hs
c5e9423340dff77b2d3b79fcd4908708770a49c3Mukund Sivaramanatc_der_files = $(foreach file, $(atc_files), \
c5e9423340dff77b2d3b79fcd4908708770a49c3Mukund Sivaraman ATC/$(basename $(basename $(notdir $(file)))).der.hs)
6444de08d1aacf7396663b7a82d62eedf534c3d7Mark AndrewsATC/AS_Annotation.der.hs: Common/AS_Annotation.der.hs $(GENRULES)
5c5c6d289db78e41f714007426a387498e15963cFrancis DupontATC/ExtSign.der.hs: Common/ExtSign.hs $(GENRULES)
5c5c6d289db78e41f714007426a387498e15963cFrancis DupontATC/DefaultMorphism.der.hs: Common/DefaultMorphism.hs $(GENRULES)
fc63119c8b7aa8827fad9e3e45e50c69bc2630e8Francis DupontATC/AS_Structured.der.hs: Syntax/AS_Structured.der.hs $(GENRULES)
fc63119c8b7aa8827fad9e3e45e50c69bc2630e8Francis Dupont $(GENRULECALL) -i ATC.AS_Annotation -i ATC.Grothendieck -o $@ $<
d040fa2f1c9c3045420ee25933b699290ab19250Mark AndrewsATC/AS_Architecture.der.hs: Syntax/AS_Architecture.der.hs $(GENRULES)
5c5c6d289db78e41f714007426a387498e15963cFrancis DupontATC/AS_Library.der.hs: Syntax/AS_Library.der.hs $(GENRULES)
5c5c6d289db78e41f714007426a387498e15963cFrancis Dupont $(GENRULECALL) -i ATC.AS_Architecture -o $@ $<
92384667ff3bc059237849b3afd4c715c9164435Evan HuntATC/GlobalAnnotations.der.hs: Common/GlobalAnnotations.hs $(GENRULES)
64d715c22acbed195703bb9b96aac2b938a83de2Mark Andrews $(GENRULECALL) -x Logic.Prover.ProverTemplate \
3230429e175dcaafe9c59967124d44c02ca0ccadEvan HuntATC/DevGraph.der.hs: Static/DevGraph.hs $(GENRULES)
3230429e175dcaafe9c59967124d44c02ca0ccadEvan Hunt $(GENRULECALL) -i ATC.AS_Library -i ATC.Grothendieck -o $@ $<
3230429e175dcaafe9c59967124d44c02ca0ccadEvan HuntCASL_files = CASL/Sublogic.hs CASL/Morphism.hs CASL/Sign.hs \
3230429e175dcaafe9c59967124d44c02ca0ccadEvan HuntHasCASL_files = Common/Prec.hs HasCASL/As.hs HasCASL/Le.hs HasCASL/Sublogic.hs
4ccffa13aa1f87d8d3dbdf7a74cf29b1c323ad52Tinderbox UserPropositional_files = Propositional/Sign.hs Propositional/Morphism.hs \
3230429e175dcaafe9c59967124d44c02ca0ccadEvan Hunt Propositional/AS_BASIC_Propositional.hs Propositional/Symbol.hs \
aee6c351d3b517f3e6a4ddf770606617fd42015bTinderbox UserRS_files = RelationalScheme/AS.hs RelationalScheme/Sign.hs
c4abb197160a74f7cd4ad23ebc63fbe0194010abEvan HuntConstraintCASL_files = ConstraintCASL/AS_ConstraintCASL.hs
c4abb197160a74f7cd4ad23ebc63fbe0194010abEvan HuntCoCASL_files = CoCASL/AS_CoCASL.hs CoCASL/CoCASLSign.hs
a0b4f6d952cc6adde281948cf995868b44f366e8Evan HuntCspCASL_files = CspCASL/AS_CspCASL.hs CspCASL/AS_CspCASL_Process.hs \
a0b4f6d952cc6adde281948cf995868b44f366e8Evan HuntCASL_DL_files = CASL_DL/AS_CASL_DL.hs CASL_DL/Sign.hs CASL_DL/Sublogics.hs
90fc237a1fdf1680ef254f16b497f90ac759f71bEvan Huntatc_logic_files = $(foreach logic, $(logics), $(logic)/ATC_$(logic).der.hs)
a0b4f6d952cc6adde281948cf995868b44f366e8Evan Huntgenerated_rule_files = $(atc_der_files) $(atc_logic_files)
90fc237a1fdf1680ef254f16b497f90ac759f71bEvan Huntgendrifted_files = $(patsubst %.der.hs, %.hs, $(generated_rule_files))
3cc8c7d63040a3eafde2b00e1f60465e7053208aEvan Hunt Comorphisms/Modal2CASL.hs Comorphisms/CASL2TopSort.hs \
3cc8c7d63040a3eafde2b00e1f60465e7053208aEvan Hunt Comorphisms/CASL2SubCFOL.hs CASL_DL/PredefinedSign.hs
ce96d4326c872c8165b5e3a81ac5b49950c782c6Evan Huntgen_inline_axiom_files = $(patsubst %.hs,%.inline.hs, $(inline_axiom_files))
ce96d4326c872c8165b5e3a81ac5b49950c782c6Evan Huntderived_sources += $(drifted_files) Driver/Version.hs $(happy_files) \
ce96d4326c872c8165b5e3a81ac5b49950c782c6Evan Hunt $(inline_axiom_files) Modal/ModalSystems.hs $(hs_der_files)
ce96d4326c872c8165b5e3a81ac5b49950c782c6Evan Hunt# sources that have {-# OPTIONS -cpp #-}
ce96d4326c872c8165b5e3a81ac5b49950c782c6Evan Hunt SoftFOL/Logic_SoftFOL.hs GUI/Utils.hs Driver/WriteFn.hs \
ce96d4326c872c8165b5e3a81ac5b49950c782c6Evan Hunt Comorphisms/LogicList.hs Comorphisms/LogicGraph.hs \
b976c39c07f7672bd1293e878b3306c7decf8afeMark Andrews Comorphisms/KnownProvers.hs hets.hs $(happy_files) \
1feee79e1f8b946af9ebcc9dc31514aafb872438Mark Andrews# unused, remove when header files are gone
1feee79e1f8b946af9ebcc9dc31514aafb872438Mark Andrewsgenrule_header_files = $(wildcard ATC/*.header.hs)
c2f8108123c40f9be5c7d8255300e578ca8a47a6Mark Andrewsnondoc_sources = $(wildcard utils/DrIFT-src/*.hs) \
f0a54842b1a50dac0b020958eb6025ed676f9a34Mark Andrews $(cpp_sources) $(pfe_sources) $(gen_inline_axiom_files) \
f0a54842b1a50dac0b020958eb6025ed676f9a34Mark Andrews $(genrule_header_files) $(generated_rule_files) \
f0a54842b1a50dac0b020958eb6025ed676f9a34Mark Andrews $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hspp \
0f5144163c44a67d9be986383769852a0dae502aMark Andrews Haskell/PreludeString.append.hs Haskell/ProgramaticaPrelude.hs \
f274cbeaed0e4c5fdbde9f5c30833d7f1da37cd3Mark Andrewshspp_sources = $(patsubst %.hs, %.hspp, $(cpp_sources))
00fb0253c9df8a4686115745ae91d501f62c7451Mark Andrews# this variable holds the modules that should be documented
00fb0253c9df8a4686115745ae91d501f62c7451Mark Andrewsdoc_sources = $(filter-out $(nondoc_sources), $(sources) $(hspp_sources))
a5c7cfbac4e401c41741c123347739ab87c80a52Mark Andrewstax_sources = Taxonomy/AbstractGraphView.hs Taxonomy/MMiSSOntology.hs \
a5c7cfbac4e401c41741c123347739ab87c80a52Mark Andrews Taxonomy/MMiSSOntologyGraph.hs Taxonomy/OntoParser.hs
eb5243365c8d5b2dd172f9cbd7c29166716caa3fMark Andrewstax_objects = $(patsubst %.hs, %.o, $(tax_sources))
c6e22bbaefce98c37c1def3f971d214a9a147ad5Evan Hunt####################################################################
d84a4d216d513bec15e83ec6c6e7863a24ff548bMark Andrews.PHONY : all hets-opt hets-optimized clean o_clean clean_pretty \
d84a4d216d513bec15e83ec6c6e7863a24ff548bMark Andrews real_clean bin_clean package_clean distclean packages \
d84a4d216d513bec15e83ec6c6e7863a24ff548bMark Andrews http_pkg syb_pkg shellac_pkg shread_pkg shcompat_pkg \
6932de75eff5f92475027d294264c80478c3c070Tinderbox User hxt_pkg haifa_pkg programatica_pkg maintainer-clean annos \
dd66b77417aff9a7805f52b1e37ac48e647e0102Evan Hunt check capa hacapa h2h h2hf showKP clean_genRules genRules \
40b28f54029a5399fc17d895dd9e8bbcd97d6b70Mark Andrews derivedSources install_hets install release cgi ghci
40b28f54029a5399fc17d895dd9e8bbcd97d6b70Mark Andrews.SECONDARY : %.hs %.d $(generated_rule_files) $(gen_inline_axiom_files)
498b0610312364afc5698b2e4caaa4dcc836133aEvan Huntpackages: base64_pkg http_pkg syb_pkg shellac_pkg shread_pkg shcompat_pkg \
498b0610312364afc5698b2e4caaa4dcc836133aEvan Hunt tagsoup_pkg hxt_pkg hxtfilter_pkg haifa_pkg programatica_pkg
90e0af6bc6c1bcafad126e1779fc478c0aeaeb8fEvan Hunt echo "of dataenc package found"; else \
871f3c8beeb2134b17414ec167b90a57adb8e122Mark Andrews echo "of HTTP package found"; else \
27174d90ccf7d15539b9384744dbbe7beae1723cEvan Hunt echo "of syb-generics package found"; else \
eb6d61d5e02946e1a7a959bac37eae9dbbc2051bEvan Hunt echo "of Shellac package found"; else \
79921aeec24a15883cf3c22a15c77837e69a46beMark Andrewsshread_pkg: utils/shread.tgz $(SETUP) shellac_pkg
188690149b54145e1936898e565eb9eec139bbfeEvan Hunt @if $(HCPKG) field Shellac-readline version; then \
58a1051e92d46638306e2c17806307c04065c2b3Mark Andrews echo "of Shellac-readline package found"; else \
8197ef7cb5619160600bf1c6e5e8374a6c10838fEvan Huntshcompat_pkg: utils/shcompat.tgz $(SETUP) shread_pkg
1831311ac6179951c8fcca75aa29dc2f5c0218b9Francis Dupont @if $(HCPKG) field Shellac-compatline version; then \
c12c746e3abad9e4100c6694118adc1df398f0bcMark Andrews echo "of Shellac-compatline package found"; else \
1c182f1516d3d14de6df81f4103ebfe538a519f6Evan Hunt echo "of tagsoup package found"; else \
6979ebf549b9c0ccd115bbf8c0d905600086f292Mark Andrewshxt_pkg: utils/hxt-8.0.0.tar.gz $(SETUP) http_pkg tagsoup_pkg
b24061719ced97ecdbc7cfcf925c217d0dd80834Mark Andrews echo "of hxt package found"; else \
dda69168ead4bb44f5a23949a04ee2069b7d4ef0Mark Andrewshxtfilter_pkg: utils/hxt-filter-8.0.0.tar.gz $(SETUP) hxt_pkg
dda69168ead4bb44f5a23949a04ee2069b7d4ef0Mark Andrews echo "of hxt-filter package found"; else \
7b04216015f6984fa43fc96f1c741ec287f84917Evan Hunthaifa_pkg: $(SETUP) base64_pkg hxtfilter_pkg syb_pkg
7d891eaf911e5cab1f704615f8f1ef87c8716f46Mark Andrews echo "of HAIFA package found"; else \
a266ab205bfd1c510022e2cd2a8cb62988242593Mark Andrews @echo 'File : Maintainer' > $@
8dba0e7d87d192deef8b2aac197e4f508043a30cEvan Hunt @echo " done"
8dba0e7d87d192deef8b2aac197e4f508043a30cEvan Hunt###############################
947cf282a721b089c1106780f13ae8e6298bddb1Mark Andrews### count lines of code
947cf282a721b089c1106780f13ae8e6298bddb1Mark Andrews###############################
947cf282a721b089c1106780f13ae8e6298bddb1Mark Andrews### Documentation via haddock
52131a835133a76cb62d4a7d8bcf5fe7bf858858Mark Andrews# generate haddock documentation with links to sources
52131a835133a76cb62d4a7d8bcf5fe7bf858858Mark Andrews# the interface treatment is stolen from uni/mk/suffix.mk
523f3d630243211ddfda852f5224f7eff681d3a5Evan Hunt HINTERFACES0=`find -L docs/www -name '*.haddock' \
2fa1fc53324c0fca978c902e883c7cc011210536Mark Andrews $(HADDOCK) -o docs -h -v -s ../%F $$HINTERFACES \
2fa1fc53324c0fca978c902e883c7cc011210536Mark Andrews -t 'Hets - the Heterogeneous Tool Set' \
a8783019814daa36dd57afe3f527462822834c3bEvan Hunt# sources are not copied here
c5379f197647b6e20d5bf48276c8c3b9f676c447Evan Hunt###############################
c5379f197647b6e20d5bf48276c8c3b9f676c447Evan Hunt### release management
d46855caedd5cb101795707f6f467fa363ef1448Evan Hunt (cd utils/DrIFT-src; $(HC) --make DrIFT.hs -o ../DrIFT && \
d46855caedd5cb101795707f6f467fa363ef1448Evan Hunt GenerateRules.hs -o ../genRules && strip ../genRules)
d46855caedd5cb101795707f6f467fa363ef1448Evan Hunt# "-package hssource" for ghc-5.04.2
d46855caedd5cb101795707f6f467fa363ef1448Evan Hunt $(HC) --make utils/InlineAxioms/InlineAxioms.hs $(HC_WARN) $(HC_PROF) \
d46855caedd5cb101795707f6f467fa363ef1448Evan Hunt svn co https://svn-agbkb.informatik.uni-bremen.de/Hets/$(REV) Hets
d46855caedd5cb101795707f6f467fa363ef1448Evan Hunt if [ -d ../programatica ] ; then \
d46855caedd5cb101795707f6f467fa363ef1448Evan Hunt ln -s ../../programatica/tools programatica/tools ; fi
180319f572fb6c1ca7000d22ea79a8dd77ae3f91Evan Hunt (cd Hets; $(MAKE) derivedSources; $(MAKE) clean; \
180319f572fb6c1ca7000d22ea79a8dd77ae3f91Evan Hunt find . -name .svn -o -name \*.o -o -name \*.hi | xargs $(RM) -r; \
0c2313eb367de3b58801d643d52c0fd9bc0e5df7Evan Hunt cp -p hets $(INSTALLDIR)/versions/hets-`cat version_nr`
c3bb8bb228bc8a914abc77a411faace9861632eaMark Andrews ln -s versions/hets-`cat version_nr` hets; $(RM) version_nr)
74745c760c8ac4462aceb2fa6e55bc545621c66dEvan Huntpack/install-%.jar: pack/install-%.xml pack/UserInputSpec-%.xml hets.in hets
905ba39e10a8f483d167b992ec31f4c0bf34326eMark Andrews ## TODO: add more dependencies and use hets-opt
087b3e8d90c482600c20f1bd6958697419c4e77dEvan Hunt# compile $< -b . -k web -o $@
24aaa0440116357eef3ab3796ebe53318b03b1ecEvan Hunt###################################
a0707b6acf359b78e06fd06228ebeec5758e7e1dJeremy C. Reedutils/genItCorrections: $(GENITCORRECTIONS_deps)
251be6e99493754700f868e0021c48b82d1c670cMark Andrewspretty/LaTeX_maps.hs: utils/words.pl utils/genItCorrections \
d4859b0b2a0510d8c4f3c48c606a5568a3b0c1d8Mark Andrews pretty/words.input pretty/fonts.input pretty/width-table.tex.templ
53f91cbd80dc353ecb7e8914dae84a6cd85c67c6Mark Andrews @echo -n "Generating pretty/LaTeX_maps.hs ... "
53f91cbd80dc353ecb7e8914dae84a6cd85c67c6Mark Andrews @(cd pretty >/dev/null; $(PERL) ../utils/words.pl > words.pl.log)
eeb13c7cd2ddde29b8605b9444451ea6e235e06aEvan Hunt @(cd pretty >/dev/null; ../utils/genItCorrections \
48f97c23b7d59c925fc3f4280972e50b8ef67c35Mark Andrews @echo "ready"
eeb13c7cd2ddde29b8605b9444451ea6e235e06aEvan Hunt @echo "please copy the file manually to Common"
c3bb8bb228bc8a914abc77a411faace9861632eaMark Andrews#############################
cef76ee5bd845a80e06da934edce4225bdba22a1Mark Andrews### ATC DrIFT-rule generation
fea81a5e0e9485b24262b6a7271a4643a4d2bad4Tinderbox User $(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(CASL_files)
f5695ad0e1a6cc8e19bfec7b71476e138de6cb6cMark Andrews $(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(DL_files)
f5695ad0e1a6cc8e19bfec7b71476e138de6cb6cMark AndrewsRelationalScheme/ATC_RelationalScheme.der.hs: $(RS_files) $(GENRULES)
f5695ad0e1a6cc8e19bfec7b71476e138de6cb6cMark Andrews $(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(RS_files)
58f1ac8dadf2c1f215343a0b2d1df2df954c4b19Mark AndrewsPropositional/ATC_Propositional.der.hs: $(Propositional_files) $(GENRULES)
58f1ac8dadf2c1f215343a0b2d1df2df954c4b19Mark Andrews $(GENRULECALL) -i ATC.AS_Annotation -o $@ $(Propositional_files)
5244e505adc08719e1387392c6eb85c453729256Mark AndrewsHasCASL/ATC_HasCASL.der.hs: $(HasCASL_files) $(GENRULES)
5244e505adc08719e1387392c6eb85c453729256Mark Andrews $(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(HasCASL_files)
cfe32752a66fe1f050d5ed7ddce75f6d58fe1637Evan HuntIsabelle/ATC_Isabelle.der.hs: $(Isabelle_files) $(GENRULES)
493f3eb297ea90ad2eb349591f1cb88194dce46dMark AndrewsModal/ATC_Modal.der.hs: $(Modal_files) $(GENRULES)
c5734964e6400f9e6d8c3f057fcccab596929deaMark Andrews $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(Modal_files)
d0ffef73fdee75f30e33c628a31d031616ad9433Evan HuntConstraintCASL/ATC_ConstraintCASL.der.hs: $(ConstraintCASL_files) $(GENRULES)
eaa2277753c6e7e642e83b2ccd27671a15336310Evan Hunt $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(ConstraintCASL_files)
eaa2277753c6e7e642e83b2ccd27671a15336310Evan HuntCASL_DL/ATC_CASL_DL.der.hs: $(CASL_DL_files) $(GENRULES)
43b9737b11f4f14b2d378746d0cd5561b1dc24a0Mark Andrews $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(CASL_DL_files)
a338c2d94781f676283f1b110f7802c71e2015bdMukund SivaramanCoCASL/ATC_CoCASL.der.hs: $(CoCASL_files) $(GENRULES)
fffcc1b13582447c9f94e498f4aaf43329c531d2Evan Hunt $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(CoCASL_files)
3e90f6c373d2e6c9c9909b112468975c4c86544eMark Andrews $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(COL_files)
c38341ec435fb78de6d12c1001201f9ac7487b68Mark AndrewsCspCASL/ATC_CspCASL.der.hs: $(CspCASL_files) $(GENRULES)
c38341ec435fb78de6d12c1001201f9ac7487b68Mark Andrews $(GENRULECALL) -i CASL.ATC_CASL -o $@ $(CspCASL_files)
c3bb8bb228bc8a914abc77a411faace9861632eaMark AndrewsSoftFOL/ATC_SoftFOL.der.hs: $(SoftFOL_files) $(GENRULES)
d96f74a3cb6212ac9e4a7a0fa8924f850348eae9Mark Andrews $(GENRULECALL) -i ATC.AS_Annotation -o $@ $(SoftFOL_files)
7712d1660a308ec3de17f1ddbbf801eb0d663f3eEvan Hunt $(GENRULECALL) -i OWL.ReadWrite -o $@ $(OWL_files)
3a55d4352767acb4e0572aabfa917610001f5c9cMark Andrews $(GENRULECALL) -x VSE.As.FoldRec -i CASL.ATC_CASL -o $@ $(VSE_files)
bc5db10d721aa9bf570578e52e17371e67bfcf5cMark Andrews $(RM) $(generated_rule_files) $(gendrifted_files) $(hspp_sources) \
70be3889746884692aa49939833d624ddd432bf0Mark Andrews###############
586db4a3e4664109fe8ce31fdd6a1b9c5bb67cbfMukund Sivaraman### removes all *.o, *.hi and *.p_o files in all subdirectories
275a8affe74d29d5fa51c9ba7172b90e9968199aMark Andrews find . -name \*.o -o -name \*.hi -o -name \*.p_o | xargs $(RM)
275a8affe74d29d5fa51c9ba7172b90e9968199aMark Andrews### remove binaries
89cf81b4625c574f60c21e0dce12b150f3c5583cMark Andrews $(RM) pretty/*.c.* pretty/*.h.* pretty/gen_it_* \
2064e46209f35d2afad526622d975647f9c2098bMark Andrews### additionally removes the library files
71ec6d09406771c0ad546d2d475a7f16c0198844Mark Andrews### clean user packages
71ec6d09406771c0ad546d2d475a7f16c0198844Mark Andrews $(HCPKG) unregister programatica --user || exit 0
a920fb9dc2ff16f32dd73e53469d0febcdcc6c11Mark Andrews $(HCPKG) unregister hxt-filter --user || exit 0
3c13af375900ffe79af4926953799e6123c9d698Mark Andrews $(HCPKG) unregister Shellac-compatline --user || exit 0
3c13af375900ffe79af4926953799e6123c9d698Mark Andrews $(HCPKG) unregister Shellac-readline --user || exit 0
d734818278966c45af997c7242e8cccd7a91a0b3Mark Andrews $(HCPKG) unregister syb-generics --user || exit 0
63e1ac1e0915dd1089493d6d092d39a3da817e59Mark Andrews### additionally removes generated files not in the CVS tree
89119e3cafff373426858f6cec7c09539f53e209Mark Andrews $(RM) Modal/GeneratePatterns.inline.hs utils/appendHaskellPreludeString
89119e3cafff373426858f6cec7c09539f53e209Mark Andrews $(RM) utils/DrIFT utils/genRules $(INLINEAXIOMS)
89119e3cafff373426858f6cec7c09539f53e209Mark Andrews $(RM) utils/genItCorrections pretty/LaTeX_maps.hs pretty/words.pl.log
33399d6a143403bc4a9ccb9307af43ef04ab7633Mark Andrews $(RM) -r $(HOME)/.ghc/$(ARCH)-$(OSBYUNAME)-hets-packages
ef117da20559f2a65f46ed9eb40deab5026cbd66Mark Andrews####################################################################
ef117da20559f2a65f46ed9eb40deab5026cbd66Mark Andrews### test targets
ba5c73b383b08326ab6b5ad2d7ca43e117e212f1Mark Andrews####################################################################
ba5c73b383b08326ab6b5ad2d7ca43e117e212f1Mark Andrews### interactive
cac2181160bdb3ccc89e3560addae5e38d4c05e3Evan Hunt### christian's target
cac2181160bdb3ccc89e3560addae5e38d4c05e3Evan Hunt### CASL parser
b8a9632333a92d73a503afe1aaa7990016c8bee9Evan Hunt### Annos parser
b8a9632333a92d73a503afe1aaa7990016c8bee9Evan Hunt### CASL parser
b8a9632333a92d73a503afe1aaa7990016c8bee9Evan Hunt### HasCASL parser
f5bb5eb7f6640af4a94e666bf1d7f84a6a7f1f23Mark Andrews### Haskell analysis
a0d411c05f12c36b298d811af3b4f2c9f08e86d4Mark Andrews### Haskell to Isabelle-HOLCF translation
42782931073786f98d3d0a617351db40066949a4Mukund SivaramanHaskell/h2hf: Haskell/h2hf.hs Haskell/*.hs Isabelle/*.hs Common/*.hs \
42782931073786f98d3d0a617351db40066949a4Mukund Sivaraman $(HC) -O --make -o $@ $< $(HC_FLAGS) $(PFE_FLAGS)
c1d33c159bf81d6faf9948ac9a6f307ca52284afEvan Hunt### HasCASL to Haskell translation
06e0d6bb126e9986f29036e671b59f48b1d2efbcEvan Hunt### test program to check the known provers
8d8f9f7f86a33a155dd74b9b2c1317afca555d54Evan Hunt### run tests in other directories
8d8f9f7f86a33a155dd74b9b2c1317afca555d54Evan Hunt for i in $(TESTDIRS); do $(MAKE) -C $$i check; done
7c9d11b654028f9901183c076b37a5494635f447Evan Hunt####################################################################
7c9d11b654028f9901183c076b37a5494635f447Evan Hunt## Preparing the version of Hets
20dec973da306d5b0776c9d3b598fdbd3a59a28eMark Andrews LANG=C $(PERL) utils/build_version.pl version_nr \
b16d99bac1d100735224ab3eaa84632537ff21b5Mark Andrews## two hardcoded dependencies for a correct generation of Version.hs
79d27f505a67ee1fb5cf104cbe7b1ead67d252b4Mukund SivaramanDriver/Options.hs Driver/WriteFn.hs Driver/ReadFn.hs: Driver/Version.hs
84dc4b3e7eea3e9c8fafa5f4fd632a51ee8b356fMukund Sivaraman## two dependencies for avoidence of circular prerequisites
84dc4b3e7eea3e9c8fafa5f4fd632a51ee8b356fMukund SivaramanCASL_DEPENDENT_BINARIES= hets CASL/capa CASL/fromKif \
84dc4b3e7eea3e9c8fafa5f4fd632a51ee8b356fMukund Sivaraman Common/annos Common/test_parser Comorphisms/test/showKP \
84dc4b3e7eea3e9c8fafa5f4fd632a51ee8b356fMukund Sivaraman CspCASL/print_csp HasCASL/hacapa Haskell/h2h Haskell/h2hf \
93d4128dcd54c152cf97b2c36caba8f3c8de3280Mark Andrews Haskell/hana Haskell/wrap Isabelle/isa Syntax/hetpa
93d4128dcd54c152cf97b2c36caba8f3c8de3280Mark Andrews$(CASL_DEPENDENT_BINARIES): $(sources) $(derived_sources)
50a745417461a4c007248202bb3a8bf7be426813Mark Andrews####################################################################
50a745417461a4c007248202bb3a8bf7be426813Mark Andrews## rules for DrIFT
0cfb24736841b3e98bb25853229a0efabab88bddEvan Hunt echo "{-# OPTIONS -w #-}" > $@
fa6308bd57f716732ba70bbafc1d09e861e4acc1Mark Andrews ($(DRIFT_ENV); export DERIVEPATH; $(DRIFT) $< > $@)
a4d76e3f0ba6f1fc2ba4b324f318e909b83bc860Evan Hunt## rules for inlineAxioms
800d25b8482c52487b4dab53cb10fa74061f1e94Mark Andrews## rule for cpp and haddock
9b819daddf8f4a5bd42276ee91bf9686d42f3ceeMark Andrews -DUNI_PACKAGE -DCASLEXTENSIONS -DPROGRAMATICA -optP -P $<
586d94eb740587975d5348b22a5fb8440d95925dMark Andrews## compiling rules for object and interface files
a569e1b3213668bc704194367ea12c23456ad1d2Mark Andrews## compiling rules for dependencies
ba586e9568364eb2da871f5fb2b71716f7c31865Mark Andrews## generate the inline file for the predefined CASL_DL sign
a0f91e910bd9af006a65e555ec4082864ca1eb8dMark Andrews CASL_DL/PredefinedSign.inline.hs.in utils/appendHaskellPreludeString \
a0f91e910bd9af006a65e555ec4082864ca1eb8dMark Andrews utils/appendHaskellPreludeString CASL_DL/PredDatatypes.het \
0fe07891819138ad6e1de45f279cff940d170542Mark Andrews echo " )" >> $@
d319beb9d0b08db8b7f9789d916a02a56976b9b9Tinderbox User# Warning: Don't change the order of the depencies!!
ea58c563bccc2a8dc20886c99c7c3334a971b6d3Evan HuntCASL_DL/PredDatatypes.het: utils/transformLibAsBasicSpec.pl \
896f49f8bdee644cd8d10e320ea3084ca3f74e2aEvan Hunt## rule for Modal/ModalSystems.hs needed for ModalLogic Translation
896f49f8bdee644cd8d10e320ea3084ca3f74e2aEvan Hunt# uses intransparently utils/outlineAxioms
896f49f8bdee644cd8d10e320ea3084ca3f74e2aEvan HuntModal/ModalSystems.hs: Modal/GeneratePatterns.inline.hs.in \
ca84a056bdb492e8894c70fd7bf6a885df03039fMark Andrews# or `date +%F`
5a8edcafd13fc63a066e8e42e0f95cdbf9606414Mark Andrews sed "s/^\(HETS_VERSION =\).*/\1$(HETS_VERSION)/" Makefile.installer \
05816676bb82a5657a741ef4d378c7fb83912cfcMark Andrews @echo " -> make"