##
## Makefile for Proof General.
## 
## Author:  David Aspinall <David.Aspinall@ed.ac.uk>
##
##  make		- do "compile" and "scripts" targets
##  make compile	- make .elc's in a single session
##  make scripts	- edit paths to bash/perl/PGHOME in scripts
##  make install	- install into system directories
##  make clean		- return to clean source
##
## Makefile,v 8.9 2006/09/22 19:26:01 da Exp
## 
###########################################################################

# Set this to "emacs" or "xemacs" according to your version of Emacs.
# NB: this is also used to set default install path names below.
EMACS=${EMACS_NAME}

# We default to /usr rather than /usr/local because installs of
# desktop and doc files under /usr/local are unlikely to work with
# rest of the system.  If that's no good for you, edit the paths
# individually before the install section.
# NB: DEST_PREFIX is used for final destination prefix, in case we're
# packaging into a build prefix rather than live root (e.g. in rpmbuild).
DEST_PREFIX=${PREFIX}

PWD=$(shell pwd)

PROVERS=acl2 ccc coq demoisa hol98 isa isar lclam lego pgshell phox plastic twelf
OTHER_ELISP=generic lib mmm
ELISP_DIRS=${PROVERS} ${OTHER_ELISP}
ELISP_EXTRAS=isar/interface isar/isartags
EXTRA_DIRS = images x-symbol

DOC_FILES=AUTHORS BUGS CHANGES COPYING INSTALL README.* REGISTER doc/*.pdf
DOC_EXAMPLES=acl2/*.acl2 hol98/*.sml isa/*.ML isa/*.thy isar/*.thy lclam/*.lcm lego/*.l pgshell/*.pgsh phox/*.phx plastic/*.lf twelf/*.elf
DOC_SUBDIRS=${DOC_EXAMPLES} */README.* */CHANGES */BUGS 

BATCHEMACS=${EMACS} -batch -q -no-site-file

# Scripts to edit paths to shells
BASH_SCRIPTS = isar/interface bin/proofgeneral
PERL_SCRIPTS = lego/legotags coq/coqtags isar/isartags
# Scripts to edit path to PG
PG_SCRIPTS = bin/proofgeneral

# Scripts to install to bin directory
BIN_SCRIPTS = bin/proofgeneral lego/legotags coq/coqtags isar/isartags

# FIXME: would rather set load path in Elisp,
# but seems tricky to do only during compilation.
# Another idea: put a function in proof-site to
# output the compile-time load path and
# ELISP_DIRS so these are set just in that one
# place.
BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (concat "${PWD}/" (symbol-name d))) (quote (${ELISP_DIRS}))) load-path))' -f batch-byte-compile
EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done)
ELC=$(EL:.el=.elc)

# Some parts of code were not compile safe, because of macros
# being expanded too early (e.g. proof-defshortcut, easy-menu-define)
# This should be fixed for 3.5, although careful testing is required.
BROKENELC=

.SUFFIXES:	.el .elc

default: all

FORCE:

## 
## compile : byte compile files in working directory:
##           Clearout old .elc's and re-compile in a
##           single Emacs process.  This is faster than "make elc",
##	     but can have artefacts because of context between
##	     compiles.
##
compile: .byte-compile
	lastemacs=`cat .byte-compile`; if [ "$$lastemacs" != "$(EMACS_NAME)" ]; then rm -f .byte-compile; $(MAKE) .byte-compile; fi


.byte-compile: $(EL) x-symbol/lisp/*.el
	@echo "*************************************************"
	@echo " Byte compiling..."
	@echo "*************************************************"
	rm -f $(ELC) 
## ignore errors for now: some files still have probs [x-symbol induced]
	-$(BYTECOMP) $(EL)
	rm -f $(BROKENELC)
	@echo " Byte compiling X-Symbol..."
	(cd x-symbol/lisp; rm -f *.elc; $(MAKE) EMACS="$(EMACS) -q -no-site-file")
	echo $(EMACS) > $(@)
	@echo "*************************************************"
	@echo " Finished."
	@echo "*************************************************"


##
## Make .elc's individually.  For testing only: it's a nuisance to
## set compiling context properly in each .el file.
##

.el.elc:
	$(BYTECOMP) $*.el
	rm -f $(BROKENELC)

elc:	$(ELC)


##
## Default targets
##

default: compile scripts

all:	compile scripts


##
## Remove generated targets
##
clean:	cleanpgscripts
	rm -f $(ELC) *~ */*~ .\#* */.\#* .byte-compile
	(cd doc; $(MAKE) clean)
	(cd x-symbol/lisp; $(MAKE) distclean)

distclean: clean

##
## Install files 
##
DESKTOP_PREFIX=${PREFIX}

# Set Elisp directories according to paths used in Red Hat RPMs
# (which may or may not be official Emacs policy).  We generate
# a pg-init.el file which loads the appropriate proof-site.el.
ELISPP=${EMACS_SITE_LISPDIR}/proofgeneral
ELISP_START=${PREFIX}/${EMACS_SITE_LISPDIR}/site-start.d

ELISP=${PREFIX}/${ELISPP}
DEST_ELISP=${DEST_PREFIX}/${ELISPP}

BINDIR=${PREFIX}/bin
DESKTOP=${PREFIX}/share
DOCDIR=${DOCSDIR}
MANDIR=${PREFIX}/man/man1
INFODIR=${PREFIX}/info

install: install-desktop install-elisp install-bin install-init ${INSTALLDOC}

install-desktop:
	if [ -d ${DESKTOP}/icons/hicolor ]; then \
	  ${BSD_INSTALL_DATA} etc/desktop/icons/16x16/proofgeneral.png ${DESKTOP}/icons/hicolor/16x16; \
	  ${BSD_INSTALL_DATA} etc/desktop/icons/32x32/proofgeneral.png ${DESKTOP}/icons/hicolor/32x32; \
	  ${BSD_INSTALL_DATA} etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/icons/hicolor/48x48; \
	fi

	if [ -d ${DESKTOP} ]; then \
	  ${BSD_INSTALL_DATA} etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/pixmaps; \
	  ${BSD_INSTALL_DATA} etc/desktop/proofgeneral.desktop ${DESKTOP}/applications; \
	  ${BSD_INSTALL_DATA} etc/desktop/mime-info/proofgeneral.mime ${DESKTOP}/mime-info; \
	  ${BSD_INSTALL_DATA} etc/desktop/mime-info/proofgeneral.keys ${DESKTOP}/mime-info; \
	fi

# backwards compatibility with old linuxes
	mkdir -p ${DESKTOP}/application-registry
	cp etc/desktop/application-registry/proofgeneral.applications ${DESKTOP}/application-registry

# NB: .el files are not strictly necessary, but we package/install them
# for the time being to help with debugging, or for users to recompile.
install-elisp: install-el install-elc

# NB: "elisp" directory actually includes the extra subdirs in EXTRA_DIRS,
# i.e. images, x-symbol.  FIXME: we could put these elsewhere, but
# then we would need to adjust paths in proof-site.el.
# FIXME 2: should deal with x-symbol properly and avoid duplication
# with images, and also to avoid including .elc and .el files in
# x-symbol subdirectory.
install-el:
	mkdir -p ${ELISP}
	for f in ${ELISP_DIRS} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done
	for f in ${ELISP_DIRS}; do ${BSD_INSTALL_DATA} $$f/*.el ${ELISP}/$$f; done
	for f in ${ELISP_EXTRAS}; do ${BSD_INSTALL_DATA} $$f ${ELISP}/$$f; done
	for f in ${EXTRA_DIRS}; \
		do for g in `find -d $$f -type d`; \
		   do mkdir -p ${ELISP}/$$g; \
		      files=`find $$g -depth 1 -type f \\! -perm +u+x`; \
		      if [ "$$files" != "" ]; then ${BSD_INSTALL_DATA} $$files ${ELISP}/$$g; fi; \
		      scripts=`find $$g -depth 1 -type f -perm +u+x`; \
		      if [ "$$scripts" != "" ]; then ${BSD_INSTALL_SCRIPT} $$scripts ${ELISP}/$$g; fi; \
		   done; \
	    done

install-elc: compile
	mkdir -p ${ELISP}
	for f in ${ELISP_DIRS} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done
	for f in ${ELISP_DIRS}; do ${BSD_INSTALL_DATA} $$f/*.elc ${ELISP}/$$f; done
	for f in ${ELISP_EXTRAS}; do ${BSD_INSTALL_DATA} $$f ${ELISP}/$$f; done

install-init:
	mkdir -p ${ELISP_START}
	echo ';;; pg-init.el --- setup for Proof General' > ${ELISP_START}/pg-init.el
	echo "(setq load-path (append load-path '(\"${DEST_ELISP}/generic\")))" >> ${ELISP_START}/pg-init.el
	echo "(require 'proof-site)" >> ${ELISP_START}/pg-init.el

install-bin: scripts
	mkdir -p ${BINDIR}
	${BSD_INSTALL_SCRIPT} ${BIN_SCRIPTS} ${BINDIR}

install-doc: doc.info doc.pdf doc.html
	mkdir -p ${MANDIR}
	${BSD_INSTALL_MAN} doc/proofgeneral.1 ${MANDIR}
	${BSD_INSTALL_MAN} doc/PG-adapting.info ${INFODIR}
	${BSD_INSTALL_MAN} doc/ProofGeneral.info ${INFODIR}
	mkdir -p ${DOCDIR}
	for f in ${DOC_FILES}; do ${BSD_INSTALL_MAN} $$f ${DOCDIR}; done
	for f in ${DOC_EXAMPLES}; do mkdir -p ${DOCDIR}/`dirname $$f`; \
		${BSD_INSTALL_MAN} $$f ${DOCDIR}/$$f; done
	mkdir -p ${DOCDIR}/ProofGeneral
	for f in doc/ProofGeneral/*.html; do \
		${BSD_INSTALL_MAN} $$f ${DOCDIR}/ProofGeneral/`basename $$f`; done
	mkdir -p ${DOCDIR}/PG-adapting
	for f in doc/PG-adapting/*.html; do \
		${BSD_INSTALL_MAN} $$f ${DOCDIR}/PG-adapting/`basename $$f`; done
	for f in ProofGeneral.pdf PG-adapting.pdf; do \
		${BSD_INSTALL_MAN} doc/$$f ${DOCDIR}/$$f; done

doc: FORCE
	(cd doc; $(MAKE) $*)

doc.%: FORCE
	(cd doc; $(MAKE) $*)

##
## scripts: try to patch bash and perl scripts with correct paths
##
scripts: bashscripts perlscripts pgscripts

bashscripts:
	@(bash="`which bash`"; \
	 if [ -z "$$bash" ]; then \
	   echo "Could not find bash - bash paths not checked" >&2; \
	   exit 0; \
	 fi; \
	 for i in $(BASH_SCRIPTS); do \
	   sed "s|^#.*!.*/bin/bash.*$$|#!$$bash|" < $$i > .tmp \
	   && cat .tmp > $$i; \
	 done; \
	 rm -f .tmp)

perlscripts:
	@(perl="`which perl`"; \
	 if [ -z "$$perl" ]; then \
	   echo "Could not find perl - perl paths not checked" >&2; \
	   exit 0; \
	 fi; \
	 for i in $(PERL_SCRIPTS); do \
	   sed "s|^#.*!.*/bin/perl.*$$|#!$$perl|" < $$i > .tmp \
	   && cat .tmp > $$i; \
	 done; \
	 rm -f .tmp)

# FIXME: this next edit is really for install case, shouldn't be made
# just when user types 'make'
pgscripts:
	@(for i in $(PG_SCRIPTS); do \
	   sed "s|PGHOMEDEFAULT=.*$$|PGHOMEDEFAULT=${DEST_ELISP}|" < $$i > .tmp \
	   && cat .tmp > $$i; \
	 done; \
	 rm -f .tmp)

# Set PGHOME path in scripts back to default location.
cleanpgscripts:
	@(for i in $(PG_SCRIPTS); do \
	   sed "s|PGHOMEDEFAULT=.*$$|PGHOMEDEFAULT=\$$HOME/ProofGeneral|" < $$i > .tmp \
	   && cat .tmp > $$i; \
	 done; \
	 rm -f .tmp)

##
## Include developer's makefile if it exists here.
##

-include Makefile.devel