rules revision 37a9d042e9f85a1d6e229eb80b48f93df810f155
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder# Author: (c) Klaus Luettich, Christian Maeder, Uni Bremen 2002-2009
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder# This Makefile will compile the hets system and provides also
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder# targets for test programs during implementation phases.
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder# !!! Note: This makefile is written for GNU make !!!
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder# (gmake on solaris)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder# the 'replacing spaces' example was taken from the (GNU) Make info manual
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederspace = $(empty) $(empty)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederDRIFT_ENV = DERIVEPATH=$(subst $(space),:,$(PFE_PATHS))
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederGENERATERULES_deps = utils/GenerateRules/*hs $(DRIFT_deps)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederGENITCORRECTIONS_deps = utils/itcor/GenItCorrections.hs
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederINLINEAXIOMS_deps = utils/InlineAxioms/InlineAxioms.hs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder Common/Doc.hs CASL/ToDoc.hs Modal/AS_Modal.hs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder Modal/Parse_AS.hs Modal/ModalSign.hs Modal/Print_AS.hs Modal/StatAna.hs
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederHAPPY = happy -sga
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederGENRULECALL = $(GENRULES) -r Typeable -r ShATermConvertible \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederGENRULECALL2 = $(GENRULES) -r Typeable -r ShATermLG \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder -i Data.Typeable -i ATerm.Lib -i ATC.Grothendieck
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederHADDOCK = haddock
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederARCH = $(subst $(space),,$(shell uname -m))
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederSETUPPREFIX = --prefix=$(HOME)/.ghc/$(ARCH)-$(OSBYUNAME)-hets-packages
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederSETUPPACKAGE = ../$(SETUP) clean; \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder ../$(SETUP) configure -O -p $(SETUPPREFIX) --user; \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder ../$(SETUP) build; ../$(SETUP) haddock; ../$(SETUP) install
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder# list glade files
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederGTK_GLADE_FILES = $(wildcard GUI/Glade/*.glade)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederGTK_GLADE_HSFILES = $(subst .glade,.hs,$(GTK_GLADE_FILES))
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederderived_sources += $(GTK_GLADE_HSFILES)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder# the list of logics that need ShATermConvertible instances
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederlogics = CASL HasCASL Isabelle Modal Temporal CoCASL COL CspCASL CASL_DL \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder SoftFOL ConstraintCASL Propositional RelationalScheme VSE OMDoc DFOL \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder LF Framework Maude ExtModal CommonLogic CSL QBF Adl HolLight Fpl THF \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederTESTTARGETFILES += Scratch.hs CASL/fromKif.hs CASL/capa.hs HasCASL/hacapa.hs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder Haskell/wrap.hs Isabelle/isa.hs Syntax/hetpa.hs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder ATC/ATCTest.hs ATC/ATCTest2.hs Common/ATerm/ATermLibTest.hs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder Common/ATerm/ATermDiffMain.hs Common/annos.hs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder SoftFOL/tests/PrintTPTPTests.hs Comorphisms/test/showKP.hs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder Comorphisms/test/sublogicGraph.hs PGIP/ParseProofScript.hs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder Common/testxupdate.hs Common/testxpath.hs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder SoftFOL/dfg.hs Adl/adl.hs GUI/displayDependencyGraph.hs
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder### list of directories to run checks in
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederTESTDIRS += Common CASL Fpl/test HasCASL test HolLight ExtModal/Tries \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederhs_clean_files = Haskell/TiATC.hs Haskell/TiDecorateATC.hs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder Haskell/TiPropATC.hs Haskell/ATC_Haskell.der.hs
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederPFE_TOOLDIR = $(wildcard programatica/tools)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederifneq ($(strip $(PFE_TOOLDIR)),)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederPFE_DIRS = base/AST base/TI base/parse2 base/parse2/Lexer base/parse2/Parser \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder base/parse2/LexerGen base/parse2/LexerSpec base/tests/HbcLibraries \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder base/pretty base/syntax base/lib base/lib/Monads base/Modules base/defs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder base/transforms base/transforms/Deriving property \
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder property/syntax property/AST property/transforms \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder property/TI property/defs property/parse2 property/parse2/Parser
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederPFE_PATHS = $(addprefix $(PFE_TOOLDIR)/, $(PFE_DIRS))
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederpfe_sources = $(wildcard $(addsuffix /*hs, $(PFE_PATHS)))
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederPFE_PATH = $(addprefix -i, $(PFE_PATHS))
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederhappy_files += $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von SchroederLEX_DIR = $(PFE_TOOLDIR)/base/parse2/Lexer
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroederprogramatica_pkg: $(PFE_TOOLDIR)/property/parse2/Parser/PropParser.hs \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder $(LEX_DIR)/HsLex.hs $(SETUP)
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder @if $(HCPKG) field programatica version; then \
00e7b6ae7da2801da668cfc8246c9a2e5023fb5bJonathan von Schroeder echo "of programatica package found"; else \
-i `pwd`/Haskell/Programatica.patch || exit 0); \
cp -f utils/programatica.cabal $(PFE_TOOLDIR); \
cp -f LICENSE.txt $(PFE_TOOLDIR); \
$(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 \
derived_sources += Haskell/PreludeString.hs
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)
# unset this variable from var.mk because the programatica sources
# uncomment HC_PROF for profiling (and comment out packages in var.mk)
drifted_files = Common/AS_Annotation.hs \
ATC/$(basename $(basename $(notdir $(file)))).der.hs)
# the rules to create ATC .der.hs file for DriFT
$(GENRULECALL) -i ATC.Id -o $@ $<
$(GENRULECALL) -x Common.Consistency.ConservativityChecker -o $@ $<
$(GENRULECALL) -i Common.ATerm.ConvInstances -o $@ $<
$(GENRULECALL2) -i ATC.AS_Structured -o $@ $<
$(GENRULECALL) -x Logic.Prover.ProverTemplate \
Isabelle_files = Isabelle/IsaSign.hs
ConstraintCASL_files = ConstraintCASL/AS_ConstraintCASL.hs
SoftFOL_files = SoftFOL/Sign.hs
VSE_files = VSE/As.hs
OMDoc_files = OMDoc/OMDocInterface.hs
Framework_files = Framework/AS.hs
FreeCAD_files = FreeCAD/As.hs
CASL/ATC_CASL.der.hs: $(CASL_files) $(GENRULES)
$(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(CASL_files)
RelationalScheme/ATC_RelationalScheme.der.hs: $(RS_files) $(GENRULES)
$(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(RS_files)
Propositional/ATC_Propositional.der.hs: $(Propositional_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(Propositional_files)
QBF/ATC_QBF.der.hs: $(QBF_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(QBF_files)
HolLight/ATC_HolLight.der.hs: $(HolLight_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(HolLight_files)
HasCASL/ATC_HasCASL.der.hs: $(HasCASL_files) $(GENRULES)
$(GENRULECALL) -i ATC.GlobalAnnotations -o $@ $(HasCASL_files)
Isabelle/ATC_Isabelle.der.hs: $(Isabelle_files) $(GENRULES)
Modal/ATC_Modal.der.hs: $(Modal_files) $(GENRULES)
$(GENRULECALL) -i CASL.ATC_CASL -o $@ $(Modal_files)
Temporal/ATC_Temporal.der.hs: $(Temporal_files) $(GENRULES)
$(GENRULECALL) -i CASL.ATC_CASL -o $@ $(Temporal_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)
SoftFOL/ATC_SoftFOL.der.hs: $(SoftFOL_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(SoftFOL_files)
VSE/ATC_VSE.der.hs: $(VSE_files) $(GENRULES)
OMDoc/ATC_OMDoc.der.hs: $(OMDoc_files) $(GENRULES)
$(GENRULECALL) -i OMDoc.ATerm -o $@ $(OMDoc_files)
DFOL/ATC_DFOL.der.hs: $(DFOL_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(DFOL_files)
LF/ATC_LF.der.hs: $(LF_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(LF_files)
Framework/ATC_Framework.der.hs: $(Framework_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(Framework_files)
Maude/ATC_Maude.der.hs: $(Maude_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(Maude_files)
ExtModal/ATC_ExtModal.der.hs: $(ExtModal_files) $(GENRULES)
$(GENRULECALL) -i CASL.ATC_CASL -o $@ $(ExtModal_files)
CSL/ATC_CSL.der.hs: $(CSL_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(CSL_files)
CommonLogic/ATC_CommonLogic.der.hs: $(CommonLogic_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(CommonLogic_files)
Adl/ATC_Adl.der.hs: $(Adl_files) $(GENRULES)
$(GENRULECALL) -i ATC.AS_Annotation -o $@ $(Adl_files)
Fpl/ATC_Fpl.der.hs: $(Fpl_files) $(GENRULES)
$(GENRULECALL) -i CASL.ATC_CASL -o $@ $(Fpl_files)
THF/ATC_THF.der.hs: $(THF_files) $(GENRULES)
FreeCAD/ATC_FreeCAD.der.hs: $(FreeCAD_files) $(GENRULES)
$(GENRULECALL) -i Common.ATerm.ConvInstances -o $@ $(FreeCAD_files)
OWL2/ATC_OWL2.der.hs: $(OWL2_files) $(GENRULES)
$(GENRULECALL) -i ATC.Result -o $@ $(OWL2_files)
# all ATC .der.hs files for all logics
atc_logic_files = $(foreach logic, $(logics), $(logic)/ATC_$(logic).der.hs)
# a rule to create all .der.hs files
gendrifted_files = $(patsubst %.der.hs, %.hs, $(generated_rule_files))
derived_sources += $(drifted_files) Driver/Version.hs $(happy_files) \
$(inline_axiom_files) Modal/ModalSystems.hs $(hs_der_files)
$(SETUP): utils/Setup.hs
$(HC) --make -O -o hets hets.hs $(HC_OPTS)
$(MAKE) hets.cgi
ghc --make GUI/hets_cgi.hs -o $@ $(HC_OPTS) -O
doc: docs/index.html
-i http://hackage.haskell.org/packages/archive/$(basename $(notdir $(file)))/latest/doc/html,$(file))
-p Hets-Haddock-Prologue.txt $(HADDOCK_OPTS) \
(cd utils/GenerateRules; \
GenerateRules.hs -o ../genRules)
$(HC) $(PARSEC_FLAG) --make utils/InlineAxioms/InlineAxioms.hs \
svn co https://svn-agbkb.informatik.uni-bremen.de/Hets/$(REV) Hets
cp Makefile Makefile.orig; \
./clean.sh; \
$(RM) clean.*; utils/replaceAllHeaders.sh)
$(TAR) cvf Hets.tar Hets
# 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)
-o -name \*.exe -o -name \*.exe.manifest | xargs $(RM)
$(RM) hets.cgi
$(RM) pretty/*.c.* pretty/*.h.* pretty/gen_it_* \
$(RM) ToHaskell/test/*.{out,output}
$(RM) */test/temp*
$(RM) doc/UserGuide.{log,aux,bbl,blg,out,pdf}
$(RM) OWL2/*.jar OWL2/java/lib/*.jar
build: hets.hs packages
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)
%.hs: %.glade utils/appendHaskellPreludeString \
cat GUI/Glade/Template.append.hs | sed "s/\%s/$$b/" | \
utils/appendHaskellPreludeString $< > $@
## rule for Modal/ModalSystems.hs needed for ModalLogic Translation
# uses intransparently utils/outlineAxioms
utils/genTransMFormFunc.pl $(INLINEAXIOMS)
$(PERL) utils/genTransMFormFunc.pl $< $@
sed "s/^\(HETS_VERSION =\).*/\1$(HETS_VERSION)/" Makefile.installer \