rules revision a84a8d508a0778b13a4d097a6dd34b95feae78ac
# Makefile
#
# Authors: (c) Klaus Luettich, Christian Maeder, Uni Bremen 2002-2009
# Jens Elkner, Uni Magdeburg 2016
# This GNU Makefile will compile the hets system and provides also
# targets for test programs during implementation phases.
# We assume ghc 7+
GHCVERSION := $(shell ghc --numeric-version)
# uncomment HC_PROF for profiling (and comment out packages in var.mk)
# call resulting binary with a final +RTS -p to get a file <binary>.prof
#HC_PROF := -prof -auto-all -osuf p_o +RTS -K100m -RTS
# -ddump-minimal-imports
# uncomment the above line to generate .imports files for displayDependencyGraph
.DEFAULT_GOAL := hets
# *.bin variants here to let them survive a 'make clean'
# Documentation (no haddock stuff, i.e. "docs/index.html", since developer can
# generated it on demand by themselves and other users dont't need it). Other
# papers (doc/*.pdf) are already pre-generated.
# indicate, whether working on an exported repo
# the 'replacing spaces' example was taken from the (GNU) Make info manual
empty =
-i ATerm.Lib
-i ATerm.Lib -i ATC.Grothendieck
else
# list glade files
GTK_GLADE_FILES = $(wildcard GUI/Glade/*.glade)
# the list of logics that need ShATermConvertible instances
### list of directories to run checks in
## 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
-o $@ $(Haskell_files)
hs_der_files += $(hs_clean_files)
else
# unset this variable from var.mk because the programatica sources
# are needed to created our sources!
# end of programatica stuff
# files generated by DriFT
# files to extract data types from to generate ShATermConvertible instances
# files generated by genRules as input for DriFT
# the rules to create ATC .der.hs file for DriFT
$(GENRULECALL) -o $@ $<
$(GENRULECALL) -i ATC.Id -o $@ $<
$(GENRULECALL) -i ATC.Id -o $@ $<
$(GENRULECALL) -o $@ $<
$(GENRULECALL) -o $@ $<
$(GENRULECALL) -o $@ $<
$(GENRULECALL) -x Common.Consistency.ConservativityChecker -o $@ $<
$(GENRULECALL) -i Common.ATerm.ConvInstances -o $@ $<
$(GENRULECALL) -o $@ $<
$(GENRULECALL2) -o $@ $<
$(GENRULECALL2) -i ATC.DgUtils -o $@ $<
# ATC files for every logic
# ATC DrIFT-rule generation for logics
$(GENRULECALL) -o $@ $(Isabelle_files)
-o $@ $(QVTR_files)
# all ATC .der.hs files for all logics
# a rule to create all .der.hs files
# the final ATC target files created by DriFT
# all sources that need to be created before ghc can be called
####################################################################
# BUILD related targets
####################################################################
# dummy target to force ghc invocation
# some trickery to trigger a full clean if the main target (hets, hets_server)
# changed since last call
# the variant without GUI
# deprecated target name
if [ -n "$$X" ]; then \
else \
printf '\nMissing "latexmk" - unable to create doc/UserGuide.pdf!\n\n';\
fi
# replace '$Header$' in all *.hs with the filename of the containing file
# call it from time to time
${SED} -i -e 's|\$$Header\$$|@|g' @
GHC_LIBDIR := $(shell ghc --print-libdir)
# scanning the "whole" NFS server isn't so smart, so restrict to wellknown dirs
-i http://hackage.haskell.org/packages/archive/$(basename $(notdir $(file)))/latest/doc/html,$(file))
printf '\nCheck log.haddock for results ...\n'
-t 'Hets - the Heterogeneous Tool Set' \
$(DRIFT): $(DRIFT_deps)
(cd utils/GenerateRules; \
GenerateRules.hs -o ../genRules)
# Common/LaTeX_maps.hs generation
### clean up
### removes all *.o, *.hi and *.p_o files in all subdirectories
### remove binaries
$(TESTTARGETS)
# do not delete on exported archive, because latexmk might not be available
CommonLogic/TestData/*.{pp.het,th} Common/testxmldiff \
debian/{root,changelog*,*.tmp,files,hets-*,tmp} \
"
### additionally removes generated files not in the repository tree
$(DTD2HS) \
### interactive
### build only, don't link. Target was formerly known as 'build'.
### Kif parser
### Annos 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)
test:
## Preparing the version of Hets
$(RM) $@
chmod 444 $@
elif [ ! -e rev.txt ]; then \
exit 1; \
else \
fi
## two dependencies to avoid circular prerequisites
## suffix rules
.SUFFIXES:
## rule for GHC
## rule for DrIFT
$(RM) $@
chmod 444 $@
## compiling rules for object and interface files
## compiling rules for dependencies
%.d : %.hs
%.d : %.lhs
## Rule to generate hs files from glade files. Needed for GTK
utils/appendHaskellPreludeString $< > $@
# just build all required jar files
jars:
$(PFE_SETUP):
printf 'Extracting $(PROGRAMATICA_SRC_FILE) ...\n' ; \
fi ; \
printf 'Fetching $(PROGRAMATICA_SRC_URL) ...\n' ; \
fi ; \
fi ; \
if [ -e $(PFE_SETUP) ]; then \
printf 'Programatica support available. You probably need to %s\n' \
'"make distclean" and make the desired target again.' ; exit 99 ; \
else \
printf 'Warning! No programatica support!\n' ; \
fi
# remove trailing .txz or .tar.xz
if [ ! -e $(PFE_SETUP) ]; then \
printf '\nprogramatica is required.\n' ; \
exit 2 ; \
fi ; \
printf "Exporting source to $${FNAME} ...\n" ; \
if [ -e $(USER_GUIDE) ]; then \
else \
printf '\nWARNING: No $(USER_GUIDE) is unavailable\n!' ; \
fi ; \
printf 'Removing unused/non-distributed files ...\n' ; \
printf 'Done.\n' ; \
cd .. ; \
#############################################################################
# INSTALL targets
#############################################################################
# We use $DEB_BUILD_ARCH to detect, whether this make got triggered via
# dpkg-buildpackage
DEFAULT_DESTDIR := \
SUBDIR_common := \
SUBDIR_hets := \
SUBDIR_hets_server := \
DESTDIR ?= $(DEFAULT_DESTDIR)
# all _relative_ wrt. $(PREFIX) and w/o trailing slashes
# see OWL2/ProveFact.hs - it doesn't use OSGi so we need to extract JNI libs
$(INSTALL) -m 0755 -d \
X=`ls ../lib/uk.ac.manchester.cs.owl.factplusplus*.jar` ; \
@printf 'Sources:\n\t%s\n\t%s\n\t%s\n' \
@printf '\nNOTE:\n\t%s\n\t%s\n' \
'contains JNI libs for Linux and MacOSX only!'
# If one would add haddocs as well, add
# -m 0755 -d $(DESTDIR)$(SUBDIR_common)$(PREFIX)/$(DOC_DIR)/html/
# -m 0644 docs/* $(DESTDIR)$(SUBDIR_common)$(PREFIX)/$(DOC_DIR)/html/
$(INSTALL) -m 0755 -d \
%.bin:
# for now install-{common,hets,hets_server} are supported, only.
$(INSTALL) -m 0755 -d \
############################################################################
# DEBIAN rules
############################################################################
# For PPA source packages we submit a platform specific changelog via
# *.debian.tar.xz, for local packages we generate it on demand.
# See Versioning in ./INSTALL
# NOTE: The dash crap sucks again here! So we assume only the 2nd rev num
# might be padded with a single '0' to avoid more clutter.
if [ -z "${FULL_DEBVERS}" ]; then \
printf "\nUsing '$${FULL_DEBVERS}' as new version.\n\n" ; \
fi ; \
printf "%s (%s) %s; urgency=low\n\n %s\n\n -- %s <%s> %s\n" "$${SRCPKG}" \
"$${FULL_DEBVERS}" "$${REL_NAME}" \
"* Initial release, automatically generated." \
# NOTE: dpkg-gencontrol is not POSIX conform wrt. arg processing!
@[ "$${USERNAME}" != 'root' -o -z "$${FAKEROOTKEY}" ] && \
printf '\nWARNING: The $< target should be called using fakeroot!\n\n'
-l$(CHANGELOG)
@[ "$${USERNAME}" != 'root' -o -z "$${FAKEROOTKEY}" ] && \
printf '\nWARNING: The $< target should be called using fakeroot!\n\n'
$(INSTALL) -m 0755 -d \
-l$(CHANGELOG)
-l$(CHANGELOG)
# vim: ts=4 sw=4 filetype=make