rules revision 0898ff703a21cf78e18cc03e8fe5a3c6d1fc25c3
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# Author: (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2004
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# This Makefile will compile the new hetcats system and provides also
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# targets for test programs during implementation phases.
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# !!! Note: This makefile is written for GNU make !!!
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# (gmake on solaris ; make on linux)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith####################################################################
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith## Some varibles, which control the compilation
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithINCLUDE_PATH = ghc:hetcats:fgl
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithCOMMONLIB_PATH = Common/Lib:Common/Lib/Parsec:Common/ATerm:fgl/Data/Graph:fgl/Data/Graph/Inductive:fgl/Data/Graph/Inductive/Aux:fgl/Data/Graph/Inductive/Monad:fgl/Data/Graph/Inductive/Query
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithCLEAN_PATH = utils/DrIFT-src:utils/GenerateRules:utils/InlineAxioms:Common:Logic:CASL:CASL/CCC:Syntax:Static:GUI:HasCASL:Haskell:Modal:CoCASL:COL:CspCASL:ATC:ToHaskell:Proofs:Comorphisms:Isabelle:$(INCLUDE_PATH):Haskell/Hatchet:$(PFE_PATHS)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith## set ghc imports properly for your system
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithLINUX_IMPORTS = $(wildcard /home/linux-bkb/ghc/ghc-latest/lib/ghc-*/imports)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithDRIFT_ENV = DERIVEPATH='.:ghc:hetcats:${LINUX_IMPORTS}:${GHC_IMPORTS}'
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# the 'replacing spaces' example was taken from the (GNU) Make info manual
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmithspace:= $(empty) $(empty)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# override on commandline for other architectures
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithINSTALLDIR = /home/www/agbkb/forschung/formal_methods/CoFI/hets/`utils/sysname.sh`
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithINLINEAXIOMS_deps = utils/InlineAxioms/*hs
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithDRIFT = $(DRIFT_ENV) utils/DrIFT
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithHADDOCK = haddock
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithHC_FLAGS = -Wall -fglasgow-exts -fallow-overlapping-instances -fallow-incoherent-instances
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# -ddump-minimal-imports
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# flags also come in via ../uni/uni-package.conf
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# but added it here in case of compilation without uni
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithHC_INCLUDE = -i$(INCLUDE_PATH)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithUNI_PACKAGE_CONF := $(wildcard ../uni/uni-package.conf)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmithifneq ($(strip $(UNI_PACKAGE_CONF)),)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithHC_PACKAGE = -package-conf $(UNI_PACKAGE_CONF) -package uni-davinci \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith -package uni-server -DUNI_PACKAGE
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# some modules from uni for haddock
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# if uni/server is included also HaXml sources are needed
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmithuni_sources = $(wildcard ../uni/davinci/haddock/*.hs) \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith $(wildcard ../uni/graphs/haddock/*.hs) \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith $(wildcard ../uni/htk/haddock/*/*.hs) \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith $(wildcard ../uni/events/haddock/*.hs) \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith $(wildcard ../uni/reactor/haddock/*.hs) \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith $(wildcard ../uni/util/haddock/*.hs) \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith $(wildcard ../uni/posixutil/haddock/*.hs)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithPFE_TOOLDIR := $(wildcard ../programatica/tools)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmithifneq ($(strip $(PFE_TOOLDIR)),)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith base/transforms base/transforms/Deriving hs2html \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith property/pfe property/syntax property/AST property/transforms \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith property/TI property/defs property/parse2 property/parse2/Parser \
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithPFE_PATH = $(addprefix -i$(PFE_TOOLDIR)/, $(PFE_DIRS))
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# add PFE_PATHS to DERIVEPATH if needed
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith# but name clashes currently prevent ATC generation in a single file
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithPFE_PATHS = $(subst $(space),:,$(addprefix $(PFE_TOOLDIR)/, $(PFE_DIRS)))
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmithpfe_sources = $(wildcard $(subst :,/*hs , $(PFE_PATHS)))
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David GoldsmithPFE_FLAGS = -package data -package text $(PFE_PATH) -DPROGRAMATICA
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith#-fallow-undecidable-instances -fno-monomorphism-restriction
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith### Profiling (only for debugging)
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith### Attention every module must be compiled with profiling or the linker
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith### cannot link the various .o files properly. So after switching on
c1bef59b02d89a84c23d29663cc4e6d46148ebd2David Goldsmith### Profiling, do an 'gmake real_clean; gmake'
include sources_hetcats.mk
genrule_header_files = $(wildcard ATC/*.header.hs)
ATC/$(basename $(basename $(notdir $(file)))).der.hs)
atc_logic_files = $(foreach logic, $(logics), $(logic)/ATC_$(logic).der.hs)
gendrifted_files = $(patsubst %.der.hs, %.hs, $(generated_rule_files))
gen_inline_axiom_files = $(patsubst %.hs,%.inline.hs,$(inline_axiom_files))
derived_sources = $(drifted_files) $(happy_files) hetcats/Version.hs \
$(inline_axiom_files) Modal/ModalSystems.hs
cpp_sources = ./Isabelle/Logic_Isabelle.hs \
taxonomy hets.cgi count doc apache_doc post_doc4apache \
#.PRECIOUS: sources_hetcats.mk
$(HC) --make -o $@ hets.hs $(HC_OPTS) 2>&1 | tee hetcats-make
$(HC) --make -O -o hets hets.hs $(HC_OPTS) -w 2>&1 | tee hetcats-make
ghc --make -package-conf /home/luettich/ghc-pkg/package.conf \
taxonomy: Taxonomy/taxonomyTool.hs $(tax_sources)
$(HC) --make -o Taxonomy/taxonomyTool $< -ifgl $(HC_OPTS)
hetcats.TAGS: $(sources)
$(sources); mv TAGS $@; mv tags hetcats.tags
doc: docs/index.html
docs/index.html: $(doc_sources)
$(MAKE) hets.cgi
$(PERL) utils/post_process_docs.pl docs \
utils/DrIFT: $(DRIFT_deps)
utils/genRules: $(GENERATERULES_deps)
(cd utils/GenerateRules; \
GenerateRules.hs -o ../genRules && strip ../genRules)
$(HC) --make utils/InlineAxioms/InlineAxioms.hs \
(cd HetCATS; $(MAKE) derivedSources; ./clean.sh; \
$(RM) clean.*; mv Makefile Makefile.orig; \
tar cvf HetCATS.tar HetCATS
cp -p hets $(INSTALLDIR)/versions/hets-`cat version_nr`
ln -s versions/hets-`cat version_nr` hets; $(RM) version_nr)
$(atc_der_files): $(atc_files) $(genrule_header_files) utils/genRules
utils/genRules -r $(rule) -o CASL $(CASL_files)
utils/genRules -r $(rule) -o HasCASL $(HasCASL_files)
utils/genRules -r $(rule) -o Modal $(Modal_files)
utils/genRules -r $(rule) -o CoCASL $(CoCASL_files)
utils/genRules -r $(rule) -o COL $(COL_files)
utils/genRules -r $(rule) -o CspCASL $(CspCASL_files)
if [ -f ATC/$(basename $(basename $(notdir $(file)))).header.hs ]; \
then utils/genRules -r $(rule) -o ATC -h \
ATC/$(basename $(basename $(notdir $(file)))).header.hs $(file); \
else utils/genRules -r $(rule) -o ATC $(file); fi ;
$(RM) CASL/capa
$(RM) HasCASL/hacapa
$(RM) Haskell/hapa
$(RM) Haskell/hana
$(RM) Haskell/wrap
$(RM) Syntax/hetpa
$(RM) Static/hetana
$(RM) GUI/hetdg
$(RM) Common/annos
$(RM) Haskell/Hatchet/hatch
$(RM) ToHaskell/translateAna
$(RM) Taxonomy/taxonomyTool
### also delete *.d.bak (dependency file backups)
(cd $$p ; $(RM) *.d *.d.bak) ; done
$(RM) hetcats-make sources_hetcats.mk
$(RM) hetcats/Version.hs
test_parser: Common/test_parser
capa: CASL/capa
hacapa: HasCASL/hacapa
hapa: Haskell/hapa
hana: Haskell/hana
hetpa: Syntax/hetpa.hs Syntax/*.hs
hetana: Static/hetana.hs Static/*.hs
atctest: ATC/ATCTest.hs ATC/*.hs
### ATerm.Lib test system
hetdg: GUI/hetdg.hs $(drifted_files) *.hs
## two hardcoded dependencies for a correct generation of Version.hs
%.hs: %.inline.hs $(INLINEAXIOMS)
## rule for Modal/ModalSystems.hs needed for ModalLogic Translation
utils/genTransMFormFunc.pl $(INLINEAXIOMS)
$(PERL) utils/genTransMFormFunc.pl $< $@