# 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.
#
# If the following environment variables are set, their values get passed to
# the corresponding tool as is: GHC_PKG_FLAGS (ghc-pkg), GHC_FLAGS (ghc).
# 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.
# Upgrade haskell-stack
# Create the build environment
-e '/^hetsVersionNumeric =/ { s/.*"\([^"]*\)".*/\1/; p; q; }' \
# 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
# the list of logics that need ShATermConvertible instances
### list of directories to run checks in
## rule for appendHaskellPreludeString
$(APPENDPRELUDESTRING) < $< > $@
#Ti_Haskell_files = TiTypes TiKinds TiDecorate TiInstanceDB
#Ti_Prop_files = property/TI/TiPropDecorate property/syntax/PropSyntaxRec
## rule for ATC generation
-o $@ $(Haskell_files)
hs_der_files += $(hs_clean_files)
else
# end of programatica stuff (PFE_FLAGS)
# 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' @
# 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; \
-o ../genRules GenerateRules.hs
# Common/LaTeX_maps.hs generation
### clean up
### removes all *.o, *.hi and *.p_o files in all subdirectories except for
### .stack-work, where the compiled dependencies reside
### remove binaries
$(TESTTARGETS)
# do not delete on exported archive, because latexmk might not be available
CommonLogic/TestData/*.{pp.het,th} Common/testxmldiff \
debian/{root,files,hets-*,tmp} \
"
### additionally removes generated files not in the repository tree
$(DTD2HS) \
### interactive
ghci: $(derived_sources)
### 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:
## two dependencies to avoid circular prerequisites
## suffix rules
.SUFFIXES:
## rule for GHC
## rule for DrIFT
## 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:
@if [ -z $(PROGRAMATICA_SRC_FILE) -o ! -e $(PROGRAMATICA_SRC_FILE) ] && \
printf 'Unable to get programatica (%s %s)\n' \
'neither PROGRAMATICA_SRC_FILE nor PROGRAMATICA_SRC_FILE' \
exit 1 ; \
fi
@if [ -e $(PFE_BASE) ]; then \
exit 2 ; \
fi
cd $(PFE_BASE) || exit 3 ; \
if [ -n $(PROGRAMATICA_SRC_FILE) -a -e $(PROGRAMATICA_SRC_FILE) ]; then \
printf 'Extracting $(PROGRAMATICA_SRC_FILE) ...\n' ; \
fi ; \
fi ; \
printf 'Fetching $(PROGRAMATICA_SRC_URL) ...\n' ; \
fi ; \
fi ; \
fi
@if [ -e $(PFE_SETUP_FILE) ]; then \
printf 'Programatica support available.\nYou probably need to %s\n\n' \
'"make distclean" and make the desired target again.' ; \
else \
fi
# remove trailing .txz or .tar.xz
archive: $(USER_GUIDE)
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 := \
# 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 ./README
# 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)
# "dpkg-genchanges -b -m'...' >../${fullPkgName}.changes"
# vim: ts=4 sw=4 filetype=make