Makefile revision e220b2051a2342a9291721e6c7f408860bed01b7
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# Author: (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2005
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# This Makefile will compile the new hets system and provides also
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# targets for test programs during implementation phases.
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# !!! Note: This makefile is written for GNU make !!!
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# (gmake on solaris)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes####################################################################
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes## Some varibles, which control the compilation
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesCOMMONLIB_PATH = Common/Lib Common/ATerm fgl/Data/Graph \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes fgl/Data/Graph/Inductive fgl/Data/Graph/Inductive/Internal \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes fgl/Data/Graph/Inductive/Monad fgl/Data/Graph/Inductive/Query
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesCLEAN_PATH = . utils/DrIFT-src utils/GenerateRules utils/InlineAxioms Common \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Logic CASL CASL/CCC Syntax Static GUI HasCASL Haskell Modal CoCASL COL \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes CspCASL ATC ToHaskell Proofs Comorphisms Isabelle Driver $(INCLUDE_PATH) \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# the 'replacing spaces' example was taken from the (GNU) Make info manual
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes## set ghc imports properly for your system
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# import directories for ghc-5.04.2
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesGHC5 = $(GHC_IMPORTS)/base:$(GHC_IMPORTS)/haskell98
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes DERIVEPATH=.:ghc:$(GHC_IMPORTS):$(GHC5):$(subst $(space),:,$(PFE_PATHS))
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# override on commandline for other architectures
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes /home/www/agbkb/forschung/formal_methods/CoFI/hets/`utils/sysname.sh`
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps) Common/Utils.hs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesINLINEAXIOMS_deps = utils/InlineAxioms/InlineAxioms.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Common/Lib/Pretty.hs Common/Keywords.hs Common/Lib/Set.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Common/Lib/Map.hs Common/Lib/Rel.hs Common/Lib/State.hs Common/Id.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Common/AS_Annotation.hs CASL/AS_Basic_CASL.hs CASL/ShowMixfix.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes CASL/Utils.hs Common/Lexer.hs Common/Token.hs Common/Anno_Parser.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Common/GlobalAnnotations.hs Common/PrettyPrint.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Common/Print_AS_Annotation.hs Common/PPUtils.hs CASL/LiteralFuns.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes CASL/Print_AS_Basic.hs Common/AnnoState.hs CASL/Formula.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes CASL/OpItem.hs CASL/SortItem.hs CASL/Inject.hs Common/Result.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Common/ConvertLiteral.hs Common/Earley.hs CASL/MixfixParser.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes CASL/Parse_AS_Basic.hs CASL/Sign.hs CASL/Overload.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes CASL/StaticAna.hs Modal/AS_Modal.hs Modal/Parse_AS.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Modal/ModalSign.hs Modal/Print_AS.hs Modal/StatAna.hs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesGENRULECALL = $(GENRULES) -r ShATermConvertible -i Common.ATerm.Lib
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# remove -fno-warn-orphans for older ghcs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesHC_FLAGS = $(HC_WARN) -fglasgow-exts -fno-monomorphism-restriction \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes -fallow-overlapping-instances -fallow-undecidable-instances
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# -ddump-minimal-imports
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# flags also come in via ../uni/uni-package.conf
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# but added it here in case of compilation without uni
bb2b38cd44b032118359afbc743efbea12f48e61bnicholeslogics = CASL HasCASL Isabelle Modal CoCASL COL CspCASL CASL_DL SPASS
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesUNI_PACKAGE_CONF = $(wildcard ../uni/uni-package.conf)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesHC_PACKAGE = -package-conf $(UNI_PACKAGE_CONF) -package uni-davinci \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# some modules from uni for haddock
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# if uni/server is included also HaXml sources are needed
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesuni_dirs = ../uni/davinci ../uni/graphs ../uni/events \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesuni_sources = $(wildcard $(addsuffix /haddock/*.hs, $(uni_dirs))) \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes### list of directories to run checks in
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes base/parse2/LexerGen base/parse2/LexerSpec base/tests/HbcLibraries \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes base/transforms base/transforms/Deriving property \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes property/syntax property/AST property/transforms \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes property/TI property/defs property/parse2 property/parse2/Parser
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesPFE_PATHS = $(addprefix $(PFE_TOOLDIR)/, $(PFE_DIRS))
bb2b38cd44b032118359afbc743efbea12f48e61bnicholespfe_sources = $(wildcard $(addsuffix /*hs, $(PFE_PATHS)))
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesPFE_FLAGS = -package data -package text $(PFE_PATH) -DPROGRAMATICA
bb2b38cd44b032118359afbc743efbea12f48e61bnicholeshappy_files += $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes patch -sNlp0 -d $(PFE_TOOLDIR) -i `pwd`/$< || exit 0
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes echo "{-# OPTIONS -w #-}" > $@
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes$(LEX_DIR)Gen/HsLexerGen: $(LEX_DIR)Gen/*.hs $(LEX_DIR)Spec/*.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesderived_sources += Haskell/PreludeString.hs $(LEX_DIR)/HsLex.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesAPPENDPRELUDESTRING = utils/appendHaskellPreludeString \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes## rule for appendHaskellPreludeString
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesHaskell/PreludeString.hs: Haskell/PreludeString.append.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesAst_Haskell_files = HsDeclStruct HsExpStruct HsFieldsStruct \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes HsGuardsStruct HsKindStruct HsPatStruct HsTypeStruct HsAssocStruct \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesOther_PFE_files = property/AST/HsPropStruct base/defs/PNT \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes base/defs/UniqueNames base/Modules/TypedIds base/Modules/Ents \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes $(addprefix $(PFE_TOOLDIR)/base/AST/, $(Ast_Haskell_files)) \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes## rule for ATC generation
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesHaskell/ATC_Haskell.der.hs: $(Haskell_files) $(GENRULES)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes $(GENRULECALL) -i Haskell.BaseATC -o $@ $(Haskell_files)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes### Profiling (only for debugging)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes### Attention every module must be compiled with profiling or the linker
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes### cannot link the various .o files properly. So after switching on
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes### Profiling, do an 'gmake real_clean; gmake'
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes### and comment out HC_PACKAGE variable definition above.
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes### Comment in the following line for switching on profiling.
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes#HC_PROF = -prof -auto-all
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesHCI_OPTS = $(HC_FLAGS) $(HC_INCLUDE) $(HC_PACKAGE) $(PFE_FLAGS)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes####################################################################
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes## sources for hets
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesnon_sources = Common/LaTeX_maps.svmono.hs CspCASL/Main.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Static/LogicStructured.hs Common/CaslLanguage.hs ./Test.hs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes $(wildcard $(addsuffix /[A-Z]*hs, $(SOURCE_PATHS))))
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesdrifted_files = Syntax/AS_Architecture.hs Syntax/AS_Library.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Common/AS_Annotation.hs CASL/AS_Basic_CASL.hs Syntax/AS_Structured.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Modal/AS_Modal.hs CoCASL/AS_CoCASL.hs COL/AS_COL.hs CASL_DL/AS_CASL_DL.hs\
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Syntax/AS_Structured.der.hs Syntax/AS_Architecture.der.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Common/GlobalAnnotations.hs Syntax/AS_Library.der.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Static/DevGraph.hs Logic/Prover.hs Proofs/Proofs.hs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes ATC/$(basename $(basename $(notdir $(file)))).der.hs)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesATC/AS_Annotation.der.hs: Common/AS_Annotation.der.hs $(GENRULES)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesATC/AS_Structured.der.hs: Syntax/AS_Structured.der.hs $(GENRULES)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes $(GENRULECALL) -i ATC.AS_Annotation -i ATC.Grothendieck -o $@ $<
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesATC/AS_Architecture.der.hs: Syntax/AS_Architecture.der.hs $(GENRULES)
e961abd49ab1b184b356f63591d37083a5651451bnicholesATC/AS_Library.der.hs: Syntax/AS_Library.der.hs $(GENRULES)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesATC/GlobalAnnotations.der.hs: Common/GlobalAnnotations.hs $(GENRULES)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesATC/DevGraph.der.hs: Static/DevGraph.hs $(GENRULES)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes $(GENRULECALL) -i ATC.AS_Library -i ATC.BasicProof -o $@ $<
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes $(GENRULECALL) -x ProverTemplate -i ATC.AS_Annotation -o $@ $<
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes $(GENRULECALL) -x BasicProof -i ATC.DevGraph -i ATC.GlobalAnnotations \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesCASL_files = CASL/Sublogic.hs CASL/Morphism.hs CASL/Sign.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesHasCASL_files = HasCASL/As.hs HasCASL/Le.hs HasCASL/Morphism.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesCoCASL_files = CoCASL/AS_CoCASL.hs CoCASL/CoCASLSign.hs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesCspCASL_files = CspCASL/AS_CSP_CASL.hs CspCASL/SignCSP.hs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesCASL_DL_files = CASL_DL/AS_CASL_DL.hs CASL_DL/Sign.hs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesatc_logic_files = $(foreach logic, $(logics), $(logic)/ATC_$(logic).der.hs)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesgenerated_rule_files = $(atc_der_files) $(atc_logic_files)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesgendrifted_files = $(patsubst %.der.hs, %.hs, $(generated_rule_files))
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesinline_axiom_files = Comorphisms/CASL2PCFOL.hs Comorphisms/PCFOL2FOL.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Comorphisms/Modal2CASL.hs Comorphisms/CASL2TopSort.hs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesgen_inline_axiom_files = $(patsubst %.hs,%.inline.hs, $(inline_axiom_files))
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesderived_sources += $(drifted_files) Driver/Version.hs $(happy_files) \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# sources that have {-# OPTIONS -cpp #-}
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Isabelle/Logic_Isabelle.hs Isabelle/CreateTheories.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Comorphisms/LogicList.hs Comorphisms/LogicGraph.hs $(happy_files)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# unused, remove when header files are gone
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesnondoc_sources = $(wildcard utils/DrIFT-src/*.hs) \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes $(cpp_sources) $(pfe_sources) $(gen_inline_axiom_files) \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Haskell/PreludeString.append.hs Haskell/ProgramaticaPrelude.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes hxt/HXT.hs hxt/Net.hs $(patsubst %.hs, %.der.hs, $(drifted_files))
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# this variable holds the modules that should be documented
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesdoc_sources = $(filter-out $(nondoc_sources), $(sources)) \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes $(patsubst %.hs, %.hspp, $(cpp_sources)) $(uni_sources)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholestax_sources = Taxonomy/AbstractGraphView.hs Taxonomy/MMiSSOntology.hs \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes Taxonomy/MMiSSOntologyGraph.hs Taxonomy/OntoParser.hs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholestax_objects = $(patsubst %.hs, %.o, $(tax_sources))
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes####################################################################
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes.PHONY : all hets-opt hets-optimized clean d_clean real_clean bin_clean \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes lib_clean distclean check capa hacapa h2h clean_genRules genRules \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes.SECONDARY : %.hs %.d $(generated_rule_files) $(gen_inline_axiom_files)
2e3a086879b1ac9681ea9ccf458096236f500dccbnicholes ghc --make -package-conf $(HOME)/wash-pkg/package.conf \
0f7cc4b1d3c42262bcdced99f682778963e83ea7bnicholes -package WASH GUI/hets_cgi.hs -o $@ $(HC_INCLUDE) \
78039ad02fa79fb9131c0ed1dad29421fcc9b528bnicholes $(HC) --make -o Taxonomy/taxonomyTool $< -ifgl $(HC_OPTS)
0f7cc4b1d3c42262bcdced99f682778963e83ea7bnicholes###############################
0f7cc4b1d3c42262bcdced99f682778963e83ea7bnicholes### TAGS files for (x)emacs
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# load them with "M-x" "visit-tags-table" from
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# use "M-." to search for a tag
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# !!Beware this is somewhat instable, because it uses an absolute path!!
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes /home/ger/linux/ghc-5.04.2/bin/i386-unknown-linux/hasktags \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes @echo 'File : Maintainer' > $@
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes 'foreach my $$f (@ARGV) { open I, "<$$f"; \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes print "$$f :"; while (<I>) \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes { if(m,^\s*Maintainer\s*:\s*(.*)$$,o) { \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes print " $$1" ; last} }; print "\n"; close I; }' \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes @echo " done"
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes###############################
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes### count lines of code
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes###############################
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes### Documentation via haddock
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# generate haddock documentation with links to sources
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes -i docs/base.haddock -i docs/parsec.haddock -s ../ \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes -t 'Hets - the Heterogeneous Tool Set' \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# sources are not copied here
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes###############################
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes### release management
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes (cd utils/DrIFT-src; $(HC) --make DrIFT.hs -o ../DrIFT && \
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes GenerateRules.hs -o ../genRules && strip ../genRules)
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes# "hssource" for ghc-5.04.2
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes $(HC) --make utils/InlineAxioms/InlineAxioms.hs $(HC_WARN) $(HC_PROF) \
if [ -d ../programatica ] ; then \
./clean.sh; \
### 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) $@