rules revision c59d1c38ef94b4fb1c8d9fda9573bc1e1d2801e7
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# Author: (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2005
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# This Makefile will compile the new hets system and provides also
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# targets for test programs during implementation phases.
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# !!! Note: This makefile is written for GNU make !!!
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# (gmake on solaris)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster####################################################################
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster## Some varibles, which control the compilation
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterINCLUDE_PATH =
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterHAIFA_PATHS = Network Network/Server Org Org/W3 Org/W3/N2001 \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Org/Xmlsoap Org/Xmlsoap/Schemas Org/Xmlsoap/Schemas/Soap \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Text Text/XML Text/XML/HXT Text/XML/Schema Text/XML/Schema/TypeMapper \
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterSOURCE_PATHS = . utils/itcor \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster utils utils/DrIFT-src utils/GenerateRules utils/InlineAxioms Common \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Common/Lib Common/ATerm Logic CASL CASL/CCC CASL/CompositionTable \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Syntax Static GUI HasCASL Haskell Modal CoCASL COL ConstraintCASL \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster CspCASL ATC Proofs Comorphisms Isabelle Driver \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Taxonomy CASL_DL SPASS OWL_DL OMDoc PGIP Propositional
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# the 'replacing spaces' example was taken from the (GNU) Make info manual
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterspace = $(empty) $(empty)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster## set ghc imports properly for your system
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterGHC_IMPORTS = `$(HC) --print-libdir`/imports
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# import directories for ghc-5.04.2
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterGHC5 = $(GHC_IMPORTS)/base:$(GHC_IMPORTS)/haskell98
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterDRIFT_ENV = \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster DERIVEPATH=.:$(GHC_IMPORTS):$(GHC5):$(subst $(space),:,$(PFE_PATHS))
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# override on commandline for other architectures
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterINSTALLDIR = \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster /home/www/agbkb/forschung/formal_methods/CoFI/hets/`utils/sysname.sh`
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterDRIFT_deps = utils/DrIFT-src/*hs
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterGENITCORRECTIONS_deps = utils/itcor/GenItCorrections.hs
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterINLINEAXIOMS_deps = utils/InlineAxioms/InlineAxioms.hs \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Common/Doc.hs CASL/ToDoc.hs Modal/AS_Modal.hs \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Modal/Parse_AS.hs Modal/ModalSign.hs Modal/Print_AS.hs Modal/StatAna.hs
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterHCPKG = ghc-pkg
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterHAPPY = happy -sga
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterGENRULECALL = $(GENRULES) -r Typeable -r ShATermConvertible \
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterHADDOCK = haddock
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterOSBYUNAME = $(shell uname)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterifneq ($(findstring SunOS, $(OSBYUNAME)),)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterARCH = $(subst $(space),,$(shell uname -m))
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterSETUPPREFIX = --prefix=$(HOME)/.ghc/$(ARCH)-$(OSBYUNAME)-hets-packages
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterSETUPPACKAGE = ../$(SETUP) clean; \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ../$(SETUP) configure -p $(SETUPPREFIX); \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ../$(SETUP) build; ../$(SETUP) haddock; ../$(SETUP) install --user
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterHAXMLVERSION = $(shell $(HCPKG) field HaXml version)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterifneq ($(findstring 1.13.2, $(HAXMLVERSION)),)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterHAXML_PACKAGE = -package HaXml -DHAXML_PACKAGE
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# remove -fno-warn-orphans for older ghcs and add -ifgl
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterHC_WARN = -Wall -fno-warn-orphans
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterHC_FLAGS = $(HAXML_PACKAGE) \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster $(HC_WARN) -fglasgow-exts -fallow-overlapping-instances
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterHC_OPTS_MAC := $(if $(findstring Darwin,$(shell uname -s)), \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -optl-F$(HOME)/Library/Frameworks -optl-framework -optlGNUreadline,)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# -ddump-minimal-imports
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# flags also come in via ../uni/uni-package.conf
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# but added it here in case of compilation without uni
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterHC_INCLUDE = $(addprefix -i, $(INCLUDE_PATH))
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterlogics = CASL HasCASL Isabelle Modal CoCASL COL CspCASL CASL_DL SPASS \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster OWL_DL ConstraintCASL Propositional
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterTESTTARGETFILES += CASL/fromKif.hs CASL/capa.hs HasCASL/hacapa.hs \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Haskell/wrap.hs Isabelle/isa.hs Syntax/hetpa.hs \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ATC/ATCTest.hs ATC/ATCTest2.hs Common/ATerm/ATermLibTest.hs \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Common/ATerm/ATermDiffMain.hs Common/annos.hs Common/test_parser.hs \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster SPASS/tests/PrintTPTPTests.hs Comorphisms/test/showKP.hs \
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterUNI_PACKAGE_CONF = $(wildcard ../uni/uni-package.conf)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterifneq ($(strip $(UNI_PACKAGE_CONF)),)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterHC_PACKAGE = -package-conf $(UNI_PACKAGE_CONF) -package uni-davinci \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -package uni-server -DUNI_PACKAGE
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# some modules from uni for haddock
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster# if uni/server is included also HaXml sources are needed
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosteruni_dirs = ../uni/davinci ../uni/graphs ../uni/events \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosteruni_sources = $(wildcard $(addsuffix /haddock/*.hs, $(uni_dirs))) \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster $(wildcard ../uni/htk/haddock/*/*.hs)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterTESTTARGETFILES += OWL_DL/ToHaskellAS.hs Taxonomy/taxonomyTool.hs \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster### list of directories to run checks in
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterTESTDIRS += Common CASL HasCASL test
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterhs_clean_files = Haskell/TiATC.hs Haskell/TiDecorateATC.hs \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Haskell/TiPropATC.hs Haskell/ATC_Haskell.der.hs
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterPFE_TOOLDIR = $(wildcard ../programatica/tools)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterifneq ($(strip $(PFE_TOOLDIR)),)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster base/parse2/LexerGen base/parse2/LexerSpec base/tests/HbcLibraries \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster base/transforms base/transforms/Deriving property \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster property/syntax property/AST property/transforms \
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster property/TI property/defs property/parse2 property/parse2/Parser
happy_files += $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs
LEX_DIR = $(PFE_TOOLDIR)/base/parse2/Lexer
programatica_pkg: $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs \
$(LEX_DIR)/HsLex.hs $(SETUP)
-i `pwd`/Haskell/Programatica.patch || exit 0); \
cp -f $(SETUP) ../programatica/tools; \
(cd ../programatica/tools; \
$(LEX_DIR)Gen/HsLexerGen: $(LEX_DIR)Gen/*.hs $(LEX_DIR)Spec/*.hs \
$(LEX_DIR)/HsTokens.hs
-i$(PFE_TOOLDIR)/base/tests/HbcLibraries \
-i$(PFE_TOOLDIR)/base/lib \
$(LEX_DIR)Gen/HsLexerGen
APPENDPRELUDESTRING = utils/appendHaskellPreludeString \
#files in base/TI/
$(addprefix $(PFE_TOOLDIR)/base/AST/, $(Ast_Haskell_files)) \
Haskell/ATC_Haskell.der.hs: $(Haskell_files) $(GENRULES)
$(GENRULECALL) -i Haskell.BaseATC -o $@ $(Haskell_files)
TESTDIRS += ToHaskell Haskell/test
TESTTARGETS = Test.o $(subst .hs,,$(TESTTARGETFILES))
sources = hets.hs $(filter-out $(non_sources), \
ATC/$(basename $(basename $(notdir $(file)))).der.hs)
$(GENRULECALL) -i ATC.AS_Structured -o $@ $<
$(GENRULECALL) -i ATC.AS_Architecture -o $@ $<
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $<
$(GENRULECALL) -x Logic.Prover.ProverTemplate \
-i ATC.AS_Annotation -o $@ $<
Isabelle_files = Isabelle/IsaSign.hs
ConstraintCASL_files = ConstraintCASL/AS_ConstraintCASL.hs
SPASS_files = SPASS/Sign.hs
OWL_DL_files = OWL_DL/Sign.hs
atc_logic_files = $(foreach logic, $(logics), $(logic)/ATC_$(logic).der.hs)
gendrifted_files = $(patsubst %.der.hs, %.hs, $(generated_rule_files))
inline_axiom_files = Comorphisms/CASL2PCFOL.hs \
gen_inline_axiom_files = $(patsubst %.hs,%.inline.hs, $(inline_axiom_files))
derived_sources += $(drifted_files) Driver/Version.hs $(happy_files) \
$(inline_axiom_files) Modal/ModalSystems.hs $(hs_der_files) \
genrule_header_files = $(wildcard ATC/*.header.hs)
nondoc_sources = $(wildcard utils/DrIFT-src/*.hs) \
$(wildcard utils/DrIFT-src/*.lhs) \
$(wildcard utils/GenerateRules/*.hs) \
$(wildcard utils/InlineAxioms/*.hs) \
$(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hspp \
$(patsubst %.hs, %.der.hs, $(drifted_files))
$(SETUP): utils/Setup.hs
http_pkg: utils/http.tgz $(SETUP)
$(TAR) zxf utils/http.tgz; \
shellac_pkg: utils/shellac.tgz $(SETUP)
$(TAR) zxf utils/shellac.tgz; \
shread_pkg: utils/shread.tgz $(SETUP) shellac_pkg
$(TAR) zxf utils/shread.tgz; \
$(TAR) zxf utils/hxt.tgz; \
$(HC) --make -O -o hets hets.hs $(HC_OPTS)
$(MAKE) hets.cgi
ghc --make GUI/hets_cgi.hs -o $@ $(HC_OPTS) -O
strip hets.cgi
hets_maintainers.txt: $(sources)
doc: docs/index.html
# the interface treatment is stolen from uni/mk/suffix.mk
docs/index.html: $(doc_sources)
HINTERFACES0=`find -L docs/www -name '*.haddock' \
-p Hets-Haddock-Prologue.txt $(doc_sources)
$(MAKE) hets.cgi
$(PERL) utils/post_process_docs.pl a-docs \
$(PERL) utils/post_process_docs.pl a-docs \
utils/DrIFT: $(DRIFT_deps)
utils/genRules: $(GENERATERULES_deps)
(cd utils/GenerateRules; \
GenerateRules.hs -o ../genRules && strip ../genRules)
$(HC) --make utils/InlineAxioms/InlineAxioms.hs $(HC_WARN) $(HC_PROF) \
cp Makefile Makefile.orig; \
./clean.sh; \
$(TAR) cvf Hets.tar Hets
cp -p hets $(INSTALLDIR)/versions/hets-`cat version_nr`
ln -s versions/hets-`cat version_nr` hets; $(RM) version_nr)
### Common/LaTeX_maps.hs generation
utils/genItCorrections: $(GENITCORRECTIONS_deps)
@echo -n "Generating pretty/LaTeX_maps.hs ... "
gen_it_characters gen_it_words >> LaTeX_maps.hs)
CASL/ATC_CASL.der.hs: $(CASL_files) $(GENRULES)
$(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(CASL_files)
Propositional/ATC_Propositional.der.hs: $(Propositional_files) \
$(GENRULECALL) -i ATC.GlobalAnnotations -o $@ \
HasCASL/ATC_HasCASL.der.hs: $(HasCASL_files) $(GENRULES)
$(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(HasCASL_files)
Isabelle/ATC_Isabelle.der.hs: $(Isabelle_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(Isabelle_files)
Modal/ATC_Modal.der.hs: $(Modal_files) $(GENRULES)
$(GENRULECALL) -i CASL.ATC_CASL -o $@ $(Modal_files)
ConstraintCASL/ATC_ConstraintCASL.der.hs: $(ConstraintCASL_files) $(GENRULES)
$(GENRULECALL) -i CASL.ATC_CASL -o $@ $(ConstraintCASL_files)
CASL_DL/ATC_CASL_DL.der.hs: $(CASL_DL_files) $(GENRULES)
$(GENRULECALL) -i CASL.ATC_CASL -o $@ $(CASL_DL_files)
CoCASL/ATC_CoCASL.der.hs: $(CoCASL_files) $(GENRULES)
$(GENRULECALL) -i CASL.ATC_CASL -o $@ $(CoCASL_files)
COL/ATC_COL.der.hs: $(COL_files) $(GENRULES)
$(GENRULECALL) -i CASL.ATC_CASL -o $@ $(COL_files)
CspCASL/ATC_CspCASL.der.hs: $(CspCASL_files) $(GENRULES)
$(GENRULECALL) -i CASL.ATC_CASL -o $@ $(CspCASL_files)
SPASS/ATC_SPASS.der.hs: $(SPASS_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(SPASS_files)
OWL_DL/ATC_OWL_DL.der.hs: $(OWL_DL_files) $(GENRULES)
$(RM) hets.cgi
$(RM) pretty/*.c.* pretty/*.h.* pretty/gen_it_* \
fromKif: CASL/fromKif
annos: Common/annos
capa: CASL/capa
hacapa: HasCASL/hacapa
hana: Haskell/hana
h2hf: Haskell/h2hf
Common/Lib/*.hs Comorphisms/*.hs
h2h: Haskell/h2h
showKP: Comorphisms/test/showKP
LANG=C $(PERL) utils/build_version.pl version_nr \
< Driver/Version.in > $@
## two hardcoded dependencies for a correct generation of Version.hs
%.hs: %.der.hs $(DRIFT)
%.hs: %.inline.hs $(INLINEAXIOMS)
## rule for Modal/ModalSystems.hs needed for ModalLogic Translation
# uses intransparently utils/outlineAxioms
utils/genTransMFormFunc.pl $(INLINEAXIOMS)
$(PERL) utils/genTransMFormFunc.pl $< $@
sed "s/^\(SPASS_DIR_MAC=\).*/\1`ls utils/SPASS-ppc-mac/ | grep SPASS`/" Makefile.inst > Makefile.inst2 ;\
rm Makefile.inst ;\
mv Makefile.inst2 $(INSTALLER_DIR)/Makefile