Makefile revision e220b2051a2342a9291721e6c7f408860bed01b7
a34684a59b60a4173c25035d0c627ef17e6dc215rpluem# Author: (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2005
1337c7673efc1f80f634139fbad7cbb98a0dc657ylavic# Year: 2004
1337c7673efc1f80f634139fbad7cbb98a0dc657ylavic# This Makefile will compile the new hets system and provides also
1337c7673efc1f80f634139fbad7cbb98a0dc657ylavic# targets for test programs during implementation phases.
4da61833a1cbbca94094f9653fd970582b97a72etrawick# !!! Note: This makefile is written for GNU make !!!
4da61833a1cbbca94094f9653fd970582b97a72etrawick# (gmake on solaris)
4789804be088bcd86ae637a29cdb7fda25169521jailletc####################################################################
4789804be088bcd86ae637a29cdb7fda25169521jailletc## Some varibles, which control the compilation
e50c3026198fd496f183cda4c32a202925476778covenerCOMMONLIB_PATH = Common/Lib Common/ATerm fgl/Data/Graph \
e50c3026198fd496f183cda4c32a202925476778covener fgl/Data/Graph/Inductive fgl/Data/Graph/Inductive/Internal \
5b88c8507d5ef6d0c4cfbc78230294968175b638minfrin fgl/Data/Graph/Inductive/Monad fgl/Data/Graph/Inductive/Query
5b88c8507d5ef6d0c4cfbc78230294968175b638minfrinCLEAN_PATH = . utils/DrIFT-src utils/GenerateRules utils/InlineAxioms Common \
6c3b9cebb551140fbb25d58bae08b539b3802133ylavic Logic CASL CASL/CCC Syntax Static GUI HasCASL Haskell Modal CoCASL COL \
6c3b9cebb551140fbb25d58bae08b539b3802133ylavic CspCASL ATC ToHaskell Proofs Comorphisms Isabelle Driver $(INCLUDE_PATH) \
4f29b65ab4b547ad5dbe506e2d0ff5d12ead9247ylavic# the 'replacing spaces' example was taken from the (GNU) Make info manual
0a0df13b7f1f4f1a74fe295253d89ca3911b301aylavic## set ghc imports properly for your system
69301145375a889e7e37caf7cc7321ac0f91801erpluem# import directories for ghc-5.04.2
506bfe33206b2fece40ef25f695af39dd4130facjkaluza DERIVEPATH=.:ghc:$(GHC_IMPORTS):$(GHC5):$(subst $(space),:,$(PFE_PATHS))
506bfe33206b2fece40ef25f695af39dd4130facjkaluza# override on commandline for other architectures
d58a848a016d401b965111e50ef829e1641f7834minfrin /home/www/agbkb/forschung/formal_methods/CoFI/hets/`utils/sysname.sh`
2e6f4d654c96c98b761fb012fd25c5d5b1558c44sfGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps) Common/Utils.hs
17e6c95f3b22d18acdf8380fb26a8d0e10c80767ylavic Common/Lib/Pretty.hs Common/Keywords.hs Common/Lib/Set.hs \
17e6c95f3b22d18acdf8380fb26a8d0e10c80767ylavic Common/Lib/Map.hs Common/Lib/Rel.hs Common/Lib/State.hs Common/Id.hs \
17e6c95f3b22d18acdf8380fb26a8d0e10c80767ylavic Common/AS_Annotation.hs CASL/AS_Basic_CASL.hs CASL/ShowMixfix.hs \
17e6c95f3b22d18acdf8380fb26a8d0e10c80767ylavic CASL/Utils.hs Common/Lexer.hs Common/Token.hs Common/Anno_Parser.hs \
e8bd80a4bb88199d2f9a24a50345688e52d9c116ylavic Common/Print_AS_Annotation.hs Common/PPUtils.hs CASL/LiteralFuns.hs \
e8bd80a4bb88199d2f9a24a50345688e52d9c116ylavic CASL/Print_AS_Basic.hs Common/AnnoState.hs CASL/Formula.hs \
e8bd80a4bb88199d2f9a24a50345688e52d9c116ylavic CASL/OpItem.hs CASL/SortItem.hs CASL/Inject.hs Common/Result.hs \
330e16bea8fe9cace4de90c349750c03dfb1fe64ylavic Common/ConvertLiteral.hs Common/Earley.hs CASL/MixfixParser.hs \
330e16bea8fe9cace4de90c349750c03dfb1fe64ylavic CASL/Parse_AS_Basic.hs CASL/Sign.hs CASL/Overload.hs \
330e16bea8fe9cace4de90c349750c03dfb1fe64ylavic CASL/StaticAna.hs Modal/AS_Modal.hs Modal/Parse_AS.hs \
330e16bea8fe9cace4de90c349750c03dfb1fe64ylavic Modal/ModalSign.hs Modal/Print_AS.hs Modal/StatAna.hs
d7205b1a86c51c27b71a2c458dc453fd53a261c1covenerGENRULECALL = $(GENRULES) -r ShATermConvertible -i Common.ATerm.Lib
44ff304057225e944e220e981d434a046d14cf06covener# remove -fno-warn-orphans for older ghcs
5d1ba75b8794925e67591c209085a49279791de9covenerHC_FLAGS = $(HC_WARN) -fglasgow-exts -fno-monomorphism-restriction \
5d1ba75b8794925e67591c209085a49279791de9covener -fallow-overlapping-instances -fallow-undecidable-instances
032982212dbcc7c3cce95bf89c503bb56e185ac7kbrand# -ddump-minimal-imports
032982212dbcc7c3cce95bf89c503bb56e185ac7kbrand# flags also come in via ../uni/uni-package.conf
032982212dbcc7c3cce95bf89c503bb56e185ac7kbrand# but added it here in case of compilation without uni
caad2986f81ab263f7af41467dd622dc9add17f3ylaviclogics = CASL HasCASL Isabelle Modal CoCASL COL CspCASL CASL_DL SPASS
45a10d38e6051fd7bdf9d742aaae633d97ff02abjailletcUNI_PACKAGE_CONF = $(wildcard ../uni/uni-package.conf)
f7317ff316c2b141feea31bddb74d5d3fa1584edjortonHC_PACKAGE = -package-conf $(UNI_PACKAGE_CONF) -package uni-davinci \
a34684a59b60a4173c25035d0c627ef17e6dc215rpluem# some modules from uni for haddock
1e2d421a36999d292042a5539971070d54aa6c63ylavic# if uni/server is included also HaXml sources are needed
1e2d421a36999d292042a5539971070d54aa6c63ylavicuni_dirs = ../uni/davinci ../uni/graphs ../uni/events \
fa7ed98b9dc94c5845cf845aea0a44ecacd290c9humbedoohuni_sources = $(wildcard $(addsuffix /haddock/*.hs, $(uni_dirs))) \
0b67eb8568cd58bb77082703951679b42cf098actrawick### list of directories to run checks in
6502b7b32f980cc2093bb3ebce37e5e4dc68fba4ylavicPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
6502b7b32f980cc2093bb3ebce37e5e4dc68fba4ylavic base/parse2/LexerGen base/parse2/LexerSpec base/tests/HbcLibraries \
3060ce7f798fbda7999cd4ddf89b525d2b294185covener base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
c1a63b8fad09c419c1a64f75993feb8a343a6801ylavic property/TI property/defs property/parse2 property/parse2/Parser
e6b4bd1113567627ab6bb6c6a7105e1e01a7d889jailletcPFE_PATHS = $(addprefix $(PFE_TOOLDIR)/, $(PFE_DIRS))
e466c40e1801982602ee0200c9e8b61cc148742djailletcpfe_sources = $(wildcard $(addsuffix /*hs, $(PFE_PATHS)))
457468b82e59d01eba00dd9d0817309c8f5e414ejimPFE_FLAGS = -package data -package text $(PFE_PATH) -DPROGRAMATICA
457468b82e59d01eba00dd9d0817309c8f5e414ejimhappy_files += $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs
15660979a30d251681463de2e0584853890082accovener patch -sNlp0 -d $(PFE_TOOLDIR) -i `pwd`/$< || exit 0
49dacedb6c387b786b7911082ff35121a45f414bcovener echo "{-# OPTIONS -w #-}" > $@
cfd9415521847b2f9394fad04fb701cfb955f503rjung$(LEX_DIR)Gen/HsLexerGen: $(LEX_DIR)Gen/*.hs $(LEX_DIR)Spec/*.hs \
49dacedb6c387b786b7911082ff35121a45f414bcovenerderived_sources += Haskell/PreludeString.hs $(LEX_DIR)/HsLex.hs \
49dacedb6c387b786b7911082ff35121a45f414bcovenerAPPENDPRELUDESTRING = utils/appendHaskellPreludeString \
3c990331fc6702119e4f5b8ba9eae3021aea5265jim## rule for appendHaskellPreludeString
3c990331fc6702119e4f5b8ba9eae3021aea5265jimHaskell/PreludeString.hs: Haskell/PreludeString.append.hs \
0451df5dc50fa5d8b3e07d92ee6a92e36a1181a5niqAst_Haskell_files = HsDeclStruct HsExpStruct HsFieldsStruct \
0451df5dc50fa5d8b3e07d92ee6a92e36a1181a5niq HsGuardsStruct HsKindStruct HsPatStruct HsTypeStruct HsAssocStruct \
983528026996668ea295be95aedb9c7a346af470ylavicOther_PFE_files = property/AST/HsPropStruct base/defs/PNT \
da0442c0440caef34706e2c2f3af05cb65921cc0jailletc base/defs/UniqueNames base/Modules/TypedIds base/Modules/Ents \
15890c9306ba98f6fc243e15a3c4778ddc7d773erpluem $(addprefix $(PFE_TOOLDIR)/base/AST/, $(Ast_Haskell_files)) \
259878293a997ff49f5ddfc53d3739cbdc25444ecovener## rule for ATC generation
259878293a997ff49f5ddfc53d3739cbdc25444ecovenerHaskell/ATC_Haskell.der.hs: $(Haskell_files) $(GENRULES)
15890c9306ba98f6fc243e15a3c4778ddc7d773erpluem $(GENRULECALL) -i Haskell.BaseATC -o $@ $(Haskell_files)
65967d05f839dbf27cf91d91fa79585eeae19660minfrin### Profiling (only for debugging)
65967d05f839dbf27cf91d91fa79585eeae19660minfrin### Attention every module must be compiled with profiling or the linker
65967d05f839dbf27cf91d91fa79585eeae19660minfrin### cannot link the various .o files properly. So after switching on
8152945ae46857b170cb227e79bb799f4fc7710dminfrin### Profiling, do an 'gmake real_clean; gmake'
8152945ae46857b170cb227e79bb799f4fc7710dminfrin### and comment out HC_PACKAGE variable definition above.
8152945ae46857b170cb227e79bb799f4fc7710dminfrin### Comment in the following line for switching on profiling.
8152945ae46857b170cb227e79bb799f4fc7710dminfrin#HC_PROF = -prof -auto-all
75f5c2db254c0167a0e396254460de09b775d203trawickHCI_OPTS = $(HC_FLAGS) $(HC_INCLUDE) $(HC_PACKAGE) $(PFE_FLAGS)
4f0358189bfa57b8e75bd6b94db264302a8f336amrumph####################################################################
5716f9c6daa92dde5f2f9d11ed63f7c9549c223atrawick## sources for hets
5716f9c6daa92dde5f2f9d11ed63f7c9549c223atrawicknon_sources = Common/LaTeX_maps.svmono.hs CspCASL/Main.hs \
5716f9c6daa92dde5f2f9d11ed63f7c9549c223atrawick Static/LogicStructured.hs Common/CaslLanguage.hs ./Test.hs
54d750a84a175d8e338880514d440773eb986b50covener $(wildcard $(addsuffix /[A-Z]*hs, $(SOURCE_PATHS))))
54d750a84a175d8e338880514d440773eb986b50covenerdrifted_files = Syntax/AS_Architecture.hs Syntax/AS_Library.hs \
83b50288fa7d306324bba68832011ea08f5c7832covener Common/AS_Annotation.hs CASL/AS_Basic_CASL.hs Syntax/AS_Structured.hs \
83b50288fa7d306324bba68832011ea08f5c7832covener Modal/AS_Modal.hs CoCASL/AS_CoCASL.hs COL/AS_COL.hs CASL_DL/AS_CASL_DL.hs\
2e15620d724fb8e3a5be183b917359a2fd6e9468covener Syntax/AS_Structured.der.hs Syntax/AS_Architecture.der.hs \
2e15620d724fb8e3a5be183b917359a2fd6e9468covener Common/GlobalAnnotations.hs Syntax/AS_Library.der.hs \
1b988c41ee505962781d110a3e4c2c90f1ea0aa4covener ATC/$(basename $(basename $(notdir $(file)))).der.hs)
1b988c41ee505962781d110a3e4c2c90f1ea0aa4covenerATC/AS_Annotation.der.hs: Common/AS_Annotation.der.hs $(GENRULES)
b8efdc95bec9cf089aa1be0bfd07d46aa1137a7acovenerATC/AS_Structured.der.hs: Syntax/AS_Structured.der.hs $(GENRULES)
f06e7c4b1bce6b6491e5de0b7998d3f5696b293dchrisd $(GENRULECALL) -i ATC.AS_Annotation -i ATC.Grothendieck -o $@ $<
f06e7c4b1bce6b6491e5de0b7998d3f5696b293dchrisdATC/AS_Architecture.der.hs: Syntax/AS_Architecture.der.hs $(GENRULES)
179565be4043d7e5f9161aa75271fa0a001866d9covenerATC/AS_Library.der.hs: Syntax/AS_Library.der.hs $(GENRULES)
fce4949fb0b309a5744afcd503c6ed2d35621ee2covenerATC/GlobalAnnotations.der.hs: Common/GlobalAnnotations.hs $(GENRULES)
7b7430e701e9a31ce809da7c220bb8dfcf68c86etrawick $(GENRULECALL) -i ATC.AS_Library -i ATC.BasicProof -o $@ $<
ccc20788c1e5fc973f36df634399c89acb70deaejerenkrantz $(GENRULECALL) -x ProverTemplate -i ATC.AS_Annotation -o $@ $<
273e512f20f262e5e2aa8e0e83371d1929fb76adjkaluza $(GENRULECALL) -x BasicProof -i ATC.DevGraph -i ATC.GlobalAnnotations \
fe83f60b41477b14a37edcfcd1f7f5c5a1ebfe44minfrinCASL_files = CASL/Sublogic.hs CASL/Morphism.hs CASL/Sign.hs \
993d1261a278d7322bccef219101220b7b4fb8c5jkaluzaHasCASL_files = HasCASL/As.hs HasCASL/Le.hs HasCASL/Morphism.hs \
ba050a6f942b9fa0e81ed73437588005c569655ccovenerCoCASL_files = CoCASL/AS_CoCASL.hs CoCASL/CoCASLSign.hs
135ddda3a989215d2bedbcf1529bfb269c3eda23niqCspCASL_files = CspCASL/AS_CSP_CASL.hs CspCASL/SignCSP.hs
001a44c352f89c9ec332ffd3e0a6927dcd19432chumbedoohCASL_DL_files = CASL_DL/AS_CASL_DL.hs CASL_DL/Sign.hs
793214f67dede32edfd9ee96c664ead04d175cbbjfclereatc_logic_files = $(foreach logic, $(logics), $(logic)/ATC_$(logic).der.hs)
9b0076ddd1103e5fa9c1f9bafde4b06ce244fbaecovenergenerated_rule_files = $(atc_der_files) $(atc_logic_files)
9b0076ddd1103e5fa9c1f9bafde4b06ce244fbaecovenergendrifted_files = $(patsubst %.der.hs, %.hs, $(generated_rule_files))
249d09d51808cb7981af99762c3b3736ca126cd5jkaluzainline_axiom_files = Comorphisms/CASL2PCFOL.hs Comorphisms/PCFOL2FOL.hs \
249d09d51808cb7981af99762c3b3736ca126cd5jkaluza Comorphisms/Modal2CASL.hs Comorphisms/CASL2TopSort.hs
56589be3d7a3e9343370df240010c6928cc78b39jkaluzagen_inline_axiom_files = $(patsubst %.hs,%.inline.hs, $(inline_axiom_files))
56589be3d7a3e9343370df240010c6928cc78b39jkaluzaderived_sources += $(drifted_files) Driver/Version.hs $(happy_files) \
77ca16c5676da23155311e13cee61e7eaba9fa3ejailletc# sources that have {-# OPTIONS -cpp #-}
f87299dab99bc04b51a6b8cad51b6795db862c0atrawick Isabelle/Logic_Isabelle.hs Isabelle/CreateTheories.hs \
4d12805e6c18253040223ea637acd6b3b3c18f60jorton Comorphisms/LogicList.hs Comorphisms/LogicGraph.hs $(happy_files)
85eacfc96a04547ef25aabbc06440039715084c2jorton# unused, remove when header files are gone
cb666b29f81df1d11d65002250153353568021fccovener $(cpp_sources) $(pfe_sources) $(gen_inline_axiom_files) \
1c2cab00d988fc48cbe59032cf76cc0bab20d6f7covener Haskell/PreludeString.append.hs Haskell/ProgramaticaPrelude.hs \
6a80c3c6f4b8ea7ba5e89402b8b779b09ce020e0covener hxt/HXT.hs hxt/Net.hs $(patsubst %.hs, %.der.hs, $(drifted_files))
75a230a728338d84dcfe81edd375352f34de22d0covener# this variable holds the modules that should be documented
75a230a728338d84dcfe81edd375352f34de22d0covenerdoc_sources = $(filter-out $(nondoc_sources), $(sources)) \
1f50dc34ae069adeed20b2986e5ffdefa5c410e0covener $(patsubst %.hs, %.hspp, $(cpp_sources)) $(uni_sources)
1f50dc34ae069adeed20b2986e5ffdefa5c410e0covenertax_sources = Taxonomy/AbstractGraphView.hs Taxonomy/MMiSSOntology.hs \
63a5ea80bddcc84a462e40f402b4f330e0e05411covener Taxonomy/MMiSSOntologyGraph.hs Taxonomy/OntoParser.hs
65a4e663b82f8bce28ac22ab2edfd7502de36998sf####################################################################
65a4e663b82f8bce28ac22ab2edfd7502de36998sf### targets
65a4e663b82f8bce28ac22ab2edfd7502de36998sf.PHONY : all hets-opt hets-optimized clean d_clean real_clean bin_clean \
c7de1955eb0eaeabf7042902476397692672d549sf lib_clean distclean check capa hacapa h2h clean_genRules genRules \
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin.SECONDARY : %.hs %.d $(generated_rule_files) $(gen_inline_axiom_files)
ef82e8fa164e0a1f8b813f7deb6b7ead96018c94niq ghc --make -package-conf $(HOME)/wash-pkg/package.conf \
c12917da693bae4028a1d5a5e8224bceed8c739dsf $(HC) --make -o Taxonomy/taxonomyTool $< -ifgl $(HC_OPTS)
eafcc0ebf263d0ba69855b6e10958c4c1a2361bdsf###############################
eafcc0ebf263d0ba69855b6e10958c4c1a2361bdsf### TAGS files for (x)emacs
eafcc0ebf263d0ba69855b6e10958c4c1a2361bdsf# load them with "M-x" "visit-tags-table" from
eafcc0ebf263d0ba69855b6e10958c4c1a2361bdsf# use "M-." to search for a tag
d7ffd2da16d58b1a0de212e4d56f7aebb72bef26sf# !!Beware this is somewhat instable, because it uses an absolute path!!
d7ffd2da16d58b1a0de212e4d56f7aebb72bef26sf /home/ger/linux/ghc-5.04.2/bin/i386-unknown-linux/hasktags \
9811aed12bbc71783d2e544ccb5fecd193843eadsf @echo 'File : Maintainer' > $@
88fac54d9d64f85bbdab5d7010816f4377f95bd7rjung 'foreach my $$f (@ARGV) { open I, "<$$f"; \
88fac54d9d64f85bbdab5d7010816f4377f95bd7rjung print "$$f :"; while (<I>) \
bd3f5647b96d378d9c75c954e3f13582af32c643sf { if(m,^\s*Maintainer\s*:\s*(.*)$$,o) { \
bd3f5647b96d378d9c75c954e3f13582af32c643sf print " $$1" ; last} }; print "\n"; close I; }' \
bd3f5647b96d378d9c75c954e3f13582af32c643sf @echo " done"
2a7beea91d46beb41f043a84eaad060047ee04aafabien###############################
2a7beea91d46beb41f043a84eaad060047ee04aafabien### count lines of code
584a85dd4047e38d3ed3a29b6662fcc9d100ae4csf###############################
584a85dd4047e38d3ed3a29b6662fcc9d100ae4csf### Documentation via haddock
f21e9e3d0bfb7a507ecc5bc963f2159d693503d1sf# generate haddock documentation with links to sources
f6b9c755a0b793e8a3a3aebd327ca20a86478117sf -t 'Hets - the Heterogeneous Tool Set' \
132ee6ac1c26d6e8953836316ba50734eefab47bsf# sources are not copied here
79c5787b92ac5f0e1cc82393816c77a006399316trawick###############################
79c5787b92ac5f0e1cc82393816c77a006399316trawick### release management
7b395e4e878c28a4784919cfd2e704ddd14a3390jorton (cd utils/DrIFT-src; $(HC) --make DrIFT.hs -o ../DrIFT && \
3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton GenerateRules.hs -o ../genRules && strip ../genRules)
53e9b27aba029b18be814df40bcf6f0428771d1efuankg# "hssource" for ghc-5.04.2
53e9b27aba029b18be814df40bcf6f0428771d1efuankg $(HC) --make utils/InlineAxioms/InlineAxioms.hs $(HC_WARN) $(HC_PROF) \
6bb524f1895f30265a1431afc460977d391cb36bsf cvs -d :pserver:cvsread@cvs-agbkb.informatik.uni-bremen.de:/repository\
23f1535d6a60817d2846bac0aea230ea475d7dccminfrin if [ -d ../programatica ] ; then \
23f1535d6a60817d2846bac0aea230ea475d7dccminfrin ln -s ../../programatica/tools programatica/tools ; fi
23f1535d6a60817d2846bac0aea230ea475d7dccminfrin (cd HetCATS; $(MAKE) derivedSources; $(MAKE) real_clean; \
ec7520b24cd80d34d82bbcaca153cbb23cc04bc0rjung find . -name CVS -o -name \*.o -o -name \*.hi | xargs $(RM) -r; \
6249dfa569d3b4f1f539665b979a80c6e335d93etrawick cp -p hets $(INSTALLDIR)/versions/hets-`cat version_nr`
ae600ca541efc686b34f8b1f21bd3d0741d37674covener ln -s versions/hets-`cat version_nr` hets; $(RM) version_nr)
cfa64348224b66dd1c9979b809406c4d15b1c137fielding#############################
74499a117b3b2cd9666715a14f90c0e5d1a4ee8ajim### ATC DrIFT-rule generation
cfa64348224b66dd1c9979b809406c4d15b1c137fielding $(GENRULECALL) -i ATC.AS_Annotation -o $@ $(CASL_files)
### also delete *.d.bak (dependency file backups)
ghci:
ToHaskell/h2hf: ToHaskell/h2hf.hs ToHaskell/*.hs Haskell/*.hs HasCASL/*.hs Isabelle/*.hs Common/*.hs
### 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
## rule for Modal/ModalSystems.hs needed for ModalLogic Translation
# uses intransparently utils/outlineAxioms
$(RM) $@