Makefile revision a5e5b8c3e5c11177e5034ef2423813a5d28979ed
# Makefile
# $Header$
# Author: (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2005
# Year: 2004
# This Makefile will compile the new hets system and provides also
# targets for test programs during implementation phases.
# !!! Note: This makefile is written for GNU make !!!
# (gmake on solaris)
####################################################################
## Some varibles, which control the compilation
# the 'replacing spaces' example was taken from the (GNU) Make info manual
empty =
## set ghc imports properly for your system
# import directories for ghc-5.04.2
DRIFT_ENV = \
# override on commandline for other architectures
INSTALLDIR = \
else
# remove -fno-warn-orphans for older ghcs and add -ifgl
HC_FLAGS = $(HAXML_PACKAGE) \
# -ddump-minimal-imports
# flags also come in via ../uni/uni-package.conf
# but added it here in case of compilation without uni
UNI_PACKAGE_CONF = $(wildcard ../uni/uni-package.conf)
# some modules from uni for haddock
### list of directories to run checks in
PFE_TOOLDIR = $(wildcard ../programatica/tools)
echo "of programatica package found"; else \
(cd ../programatica/tools; \
echo "{-# OPTIONS -w #-}" > $@
$< >> $@
$@.hs -o $@
strip $@
## rule for appendHaskellPreludeString
$(RM) $@
$(APPENDPRELUDESTRING) < $< > $@
chmod 444 $@
#Ti_Haskell_files = TiTypes TiKinds TiDecorate TiInstanceDB
#Ti_Prop_files = property/TI/TiPropDecorate property/syntax/PropSyntaxRec
Haskell_files = $(addsuffix .hs, \
## rule for ATC generation
hs_der_files += $(hs_clean_files)
### Profiling (only for debugging)
### Attention every module must be compiled with profiling or the linker
### cannot link the various .o files properly. So after switching on
### Profiling, do an 'gmake real_clean; gmake'
### Comment in the following line for switching on profiling.
#HC_PROF = -prof -auto-all -fignore-asserts
####################################################################
## sources for hets
SOURCE_PATHS = $(CLEAN_PATH)
#endif
$(GENRULECALL) -o $@ $<
$(GENRULECALL) -o $@ $<
$(GENRULECALL) -o $@ $<
$(GENRULECALL) -o $@ $<
-i ATC.AS_Annotation -o $@ $<
# sources that have {-# OPTIONS -cpp #-}
cpp_sources = \
# unused, remove when header files are gone
nondoc_sources = $(wildcard utils/DrIFT-src/*.hs) \
$(wildcard utils/GenerateRules/*.hs) \
$(wildcard utils/InlineAxioms/*.hs) \
# this variable holds the modules that should be documented
####################################################################
### targets
echo "of HTTP package found"; else \
echo "of syb-generics package found"; else \
echo "of shellac package found"; else \
echo "of shellac-readline package found"; else \
echo "of hxt package found"; else \
echo "of HAIFA package found"; else \
$(RM) $@
cgi:
$(MAKE) real_clean
@echo 'File : Maintainer' > $@
@echo -n Generating $@ " "
@$(PERL) -e \
'foreach my $$f (@ARGV) { open I, "<$$f"; \
print "$$f :"; while (<I>) \
{ if(m,^\s*Maintainer\s*:\s*(.*)$$,o) { \
print " $$1" ; last} }; print "\n"; close I; }' \
$(sources) >> $@
@echo " done"
###############################
### count lines of code
###############################
### Documentation via haddock
# generate haddock documentation with links to sources
HINTERFACES=`echo $$HINTERFACES0 | \
-t 'Hets - the Heterogeneous Tool Set' \
# sources are not copied here
###############################
### release management
(cd utils/GenerateRules; \
GenerateRules.hs -o ../genRules && strip ../genRules)
# "-package hssource" for ghc-5.04.2
$(INLINEAXIOMS): $(INLINEAXIOMS_deps)
-i../.. -o $(INLINEAXIOMS)
# set this variable from the command line to i,e. RELEASETAG='-r release-0-60'
$(RM) -r programatica
if [ -d ../programatica ] ; then \
./clean.sh; \
## TODO: add more dependencies and use hets-opt
# compile $< -b . -k web -o $@
###################################
### Common/LaTeX_maps.hs generation
strip $@
@echo -n "Generating pretty/LaTeX_maps.hs ... "
@(cd pretty >/dev/null; ../utils/genItCorrections \
@echo "ready"
@echo "please copy the file manually to Common"
#############################
### ATC DrIFT-rule generation
$(GENRULES)
$(GENRULECALL) -i ATC.GlobalAnnotations -o $@ \
-o $@ $(OWL_DL_files)
###############
### clean up
### removes *.hi and *.o in all include directories
for p in $(CLEAN_PATH) ; do \
### remove binaries
$(RM) $(TESTTARGETS)
### additionally removes the library files
### clean user packages
### additionally removes generated files not in the CVS tree
$(RM) $(derived_sources)
####################################################################
### test targets
####################################################################
### interactive
ghci: $(derived_sources)
### christian's target
### CASL parser
### CASL parser
### HasCASL parser
### Haskell analysis
### Haskell to Isabelle-HOLCF translation
### HasCASL to Haskell translation
### test program to check the known provers
### run tests in other directories
check: $(TESTTARGETS)
####################################################################
## Preparing the version of HetCATS
$(RM) $@
chmod 444 $@
## two hardcoded dependencies for a correct generation of Version.hs
## two dependencies for avoidence of circular prerequisites
####################################################################
## rules for DrIFT
.SUFFIXES:
%.hs: %.y
echo "{-# OPTIONS -w #-}" > $@
$(RM) $@
chmod 444 $@
## rules for inlineAxioms
$(RM) $@
$(INLINEAXIOMS) $< > $@
chmod 444 $@
## rule for cpp and haddock
## compiling rules for object and interface files
## compiling rules for dependencies
%.d : %.hs
%.d : %.lhs
## generate the inline file for the predefined CASL_DL sign
# Warning: Don't change the order of the depencies!!
$(RM) $@
echo " )" >> $@
chmod 444 $@
$(RM) $@
$(PERL) $+ > $@
chmod 444 $@
## rule for Modal/ModalSystems.hs needed for ModalLogic Translation
# uses intransparently utils/outlineAxioms
$(RM) $@
chmod 444 $@
@if [ -d $(INSTALLER_DIR) ] ; then \
else \
mkdir -p $(INSTALLER_DIR) ; \
fi
@echo =========================================================================
@echo "then please first login:"
@echo " cvs -d :pserver:anoncvs@cvs.haskell.org:/cvs login"
@echo " the password is cvn "
@echo " cvs -d :pserver:cvsread@cvs-agbkb.informatik.uni-bremen.de:/repository login "
@echo " the password is "
@echo =========================================================================
@echo Please do
@echo " -> make"