#!/usr/bin/make -f
# Sample debian/rules that uses debhelper.
# GNU copyright 1997 by Joey Hess.
#
# This version is for a hypothetical package that builds an
# architecture-dependant package, as well as an architecture-independent
# package.

# Uncomment this to turn on verbose mode.
#export DH_VERBOSE=1

# This is the debhelper compatability version to use.
#export DH_COMPAT=4

# This has to be exported to make some magic below work.
export DH_OPTIONS

PN:=acl2
VR:=$(shell awk '{if (i) next;i=1;a=$$2;gsub("[()]","",a);split(a,A,"-");print A[1];}' debian/changelog)
PD:=$(PN)-$(VR)


NO_STRIP:=
# ifeq ($(DEB_BUILD_ARCH),powerpc)
# NO_STRIP:=--exclude=saved_acl2
# endif

# ACL2_HEAP_WORDS_NEEDED_FOR_CERTIFICATION:=500000000
# MAXJOBS:=$(shell gcl -batch -eval \
#    "(print \
#       (multiple-value-bind (a b c d) (si::heap-report) \
# 	(min 8 \
# 	     (ceiling (/ (- d c) (/ a 8)) \
#                       ${ACL2_HEAP_WORDS_NEEDED_FOR_CERTIFICATION}))))")

NUMJOBS:=1
ifneq (,$(filter parallel=%,$(DEB_BUILD_OPTIONS)))
  NUMJOBS:=$(patsubst parallel=%,%,$(filter parallel=%,$(DEB_BUILD_OPTIONS)))
endif
# NUMJOBS:=$(shell if test $(NUMJOBS) -gt ${MAXJOBS}; then echo ${MAXJOBS} ; else echo $(NUMJOBS); fi)

#books/workshops:
#	mkdir $@

#init.lsp.ori:
#	[ -e $@ ] || mv init.lsp $@

DLOPEN_T:=debian/dlopen.lisp #init.lsp.ori

#ifeq ($(DEB_BUILD_ARCH),ia64)
#DLOPEN?=$(DLOPEN_T)
#endif
#ifeq ($(DEB_BUILD_ARCH),alpha)
#DLOPEN?=$(DLOPEN_T)
#endif
#ifeq ($(DEB_BUILD_ARCH),mips)
#DLOPEN?=$(DLOPEN_T)
#endif
#ifeq ($(DEB_BUILD_ARCH),mipsel)
#DLOPEN?=$(DLOPEN_T)
#endif
#ifeq ($(DEB_BUILD_ARCH),hppa)
#DLOPEN?=$(DLOPEN_T)
#endif

debian/elpa-acl2.elpa: debian/acl2-pkg.el
	find books/interface/emacs -name "*.el" >$@
	find emacs -name "*.el" >>$@
	find books/xdoc -name "*.el" >>$@
	find books/system/doc -name "*.el" >>$@
	find books/emacs -name "*.el" >>$@
	echo debian/acl2.el >> debian/elpa-acl2.elpa
	echo debian/acl2-pkg.el >> debian/elpa-acl2.elpa
	echo debian/debian-autoloads.el >> debian/elpa-acl2.elpa


debian/acl2-pkg.el: debian/acl2-pkg.el.in
	cat $< | sed "s,@VR@,$$(echo $(VR) | sed 's,[a-zA-Z]*,,g'),g" > $@

debian/dlopen.lisp: debian/dlopen.lisp.in
	cat $< | sed "s,@VR@,$(VR),g" > $@

# debian/acl2-emacs.emacsen-startup: debian/acl2-emacs.emacsen-startup.in
# 	cat $< | sed "s,@VR@,$(VR),g" > $@

#pgcl:
#	echo "(progn (setq compiler::*split-files* 100000)(si::save-system \"$@\"))" | GCL_ANSI=t gcl

saved_acl2: # pgcl #debian/patches_applied $(DLOPEN_T)
#	gcl -batch -eval "(bye #-native-reloc 1)" || \
#		(gcl -batch -eval '(load "debian/dlopen.lisp")' && $(MAKE) do_saved)
#	gcl -batch -eval "(bye #+native-reloc 1)" || $(MAKE) GCL_ANSI=t LISP=gcl
	$(MAKE) GCL_MEM_MULTIPLE=0.1 GCL_ANSI=t LISP=$(shell command -v gcl) & j=$$! ; tail --retry -f make.log & k=$$! ; wait $$j ; kill $$k
	mv *$@.gcl $@

saved_acl2.c: saved_acl2
	echo "(f-put-global 'old-certification-dir \"$$(pwd)/books\" state)" \
              "(f-put-global 'new-certification-dir \"/usr/share/$(PD)/books\" state)" \
	      ":q #-native-reloc (setq si::*multiply-stacks* 4) :q (in-package :acl2) " \
	      "#+(or sparc sparc64)(progn (si::sgc-on nil) (fmakunbound 'si::sgc-on))" \
              "(save-exec \"$@\" \"Modified to produce final certification files\")" | HOME=$$(pwd) ./$<
	mv $@.gcl $@

debian/mini-proveall.out: saved_acl2
	HOME=$$(pwd) $(MAKE) mini-proveall
	mv $(@F) $@

books/short-test.log: saved_acl2.c
	cp saved_acl2 saved_acl2.ori
	HOME=$$(pwd) $(MAKE) certify-books-short
	cp saved_acl2.ori saved_acl2

#	tail -f --pid=$$j --retry $@ $$(find books -name "*.lisp" | sed 's,\.lisp$$,.out,1') & \

debian/test.log: saved_acl2.c
	mv saved_acl2 saved_acl2.ori
	cp $< saved_acl2
#	These take too much memory when run in parallel
	EXCLUDED_PREFIXES="projects/x86isa/machine/instructions kestrel/x86  kestrel/axe" \
	BUILDDIR="$$(dirname $$(pwd))" \
	FINALDIR="/usr/share/$(PD)" \
	HOME=$$(pwd) \
	GCL_MULTIPROCESS_MEMORY_POOL=t \
	$(MAKE) -j $(NUMJOBS) -l 2.95 regression-fresh 2>&1 | tee $@ & j=$$! ; \
	while sleep 1800; do echo Tick; done & k=$$! ; \
	wait $$j ; kill $$k
#
	BUILDDIR="$$(dirname $$(pwd))" \
	FINALDIR="/usr/share/$(PD)" \
	HOME=$$(pwd) \
	GCL_MULTIPROCESS_MEMORY_POOL=t \
	$(MAKE) -l 2.95 regression 2>&1 | tee -a $@ & j=$$! ; \
	while sleep 1800; do echo Tick; done & k=$$! ; \
	wait $$j ; kill $$k
#	>$@ 2>&1 & j=$$! ; \
#	while sleep 1800; do echo Tick; done & k=$$! ; tail -f debian/test.log & l=$$! ; \
#	wait $$j ; kill $$k $$l
#	[ -f $@ ] && ! fgrep '**' $@ || (echo FULL TEST FAILS ;\
#		for i in $$(find books -name "*.out"); do \
#			if ! [ -e $${i%out}cert ] ; then \
#				echo $$i ; \
#				cat $$i ; \
#			fi ; \
		done)
	mv saved_acl2.ori saved_acl2
	[ -f $@ ] && ( ! fgrep '**' $@ || true )
	  # gcl -batch -eval \
          #   "(bye \
	  # 	  #-native-reloc 0 \
          #         #+native-reloc \
          #           (let ((w (multiple-value-bind (a b c d) (si::heap-report) (/ (- d c) (/ a 8))))) \
	  # 		 (format t \"certification run with ~s heap words~%\" w) \
	  # 		 (if (< w ${ACL2_HEAP_WORDS_NEEDED_FOR_CERTIFICATION}) 0 1)))")

books/interface/infix/Makefile: books/interface/infix/makefile
	sed -e "s,^DIR = .*,DIR = $$(pwd)/books/interface/infix,1" \
	    -e "s,^LISP = .*,LISP = $$(pwd)/saved_acl2,1" $< > $@

infix-stamp: books/interface/infix/Makefile saved_acl2
	cd books/interface/infix && make -f Makefile compile
	cd books/interface/infix && make -f Makefile example
#	cd books/interface/infix && make -f Makefile events
	touch $@

doc/TEX/acl2-book.ps.gz: saved_acl2
	HOME=$$(pwd) $(MAKE) DOC
	rm -f doc/HTML/LICENSE
	find doc -empty -exec rm {} \;

build: build-arch build-indep
build-arch: build-stamp
build-indep: build-stamp
build-stamp: debian/mini-proveall.out debian/test.log infix-stamp # doc/TEX/acl2-book.ps.gz
	dh_testdir

#	$(MAKE)

	touch build-stamp

infix_clean: books/interface/infix/Makefile
	rm -f infix-stamp
	cd books/interface/infix && make -f Makefile clean
	rm -f books/interface/infix/Makefile


debian/dpatches: debian/patches.in
	debian/rules debian/patches_unapplied
	cat $< | sed -e "s,@BDIR@,$$(pwd),1" -e "s,@DDIR@,/usr/share/$(PD),1" >$@

debian/patches_applied: debian/dpatches
	! [ -e debian/patches_unapplied ] || \
		(patch -p1 < $< && rm -f debian/patches_unapplied)
	touch $@

debian/patches_unapplied:
	! [ -e debian/patches_applied ] || ! [ -e debian/dpatches ] ||  \
		(patch -p1 -R < debian/dpatches && rm -f debian/patches_applied)
	touch $@


INSTALLS:=$(addprefix debian/,$(addsuffix .install,acl2 acl2-source acl2-doc acl2-books acl2-books-source acl2-books-certs acl2-infix acl2-infix-source))
LINKS:=$(addprefix debian/,$(addsuffix .links,acl2 acl2-books acl2-infix))
IFILES:=$(INSTALLS) $(shell ls -1 debian/*.examples debian/*.docs)
debian/README.Debian: debian/README.Debian.in $(IFILES)
	awk '/@PLIST@/ {exit 0} {print}' $< >$@
	for i in $(filter %.install,$^); do\
	 awk '/^debian\// {next} {sub(".final$$","",$$1);$$2="/" $$2;print $$0 " " p}' \
		p=$$(basename $${i%.install}) $$i >>$@ ; done
	for i in $(filter %.info,$^); do\
	 awk '/^debian\// {next} {print $$0 " /usr/share/info " p}' p=$$(basename $${i%.info}) $$i >>$@ ; done
	for i in $(filter %.examples,$^); do\
	 awk '/^debian\// {next} {print $$0 " /usr/share/doc/" p "/examples " p}' \
		p=$$(basename $${i%.examples}) $$i >>$@ ; done
	for i in $(filter %.docs,$^); do\
	 awk '/^debian\// {next} {print $$0 " /usr/share/doc/" p " " p}' p=$$(basename $${i%.docs}) $$i >>$@ ; done
	awk '/@PLIST@/ {i=1;next} {if (i) print}' $< >>$@

OVERRIDES:= $(shell find debian/ -name "*.lintian-overrides.in" |sed 's,\.in,,g')

clean: infix_clean #debian/patches_unapplied books/workshops
	dh_testdir
	dh_testroot
	rm -f build-stamp

	$(MAKE) clean-all
	$(MAKE) clean-books
	find books -name "*.final" -exec rm {} \;
	rm -f saved_acl2 init_nsaved1_acl2.lsp worklispext
	rm -f debian/mini-proveall.out books/short-test.log debian/test.log
#	! [ -e init.lsp.ori ] || mv init.lsp.ori init.lsp
	rm -f foo.lsp nsaved_acl2
	for i in data c h ; do \
		for j in $$(find -name "*.$$i") ; do\
			k=$$(echo $$j | sed "s,\.$$i$$,,1") ;\
			! [ -e $$k.lisp ] || rm $$j ; \
		done ; \
	done
	rm -f books/bdd/benchmarks.data acl2r.lisp tmp
	rm -f debian/dpatches $(INSTALLS) $(LINKS) debian/README.Debian saved_acl2*
	rm -f debian/dlopen.lisp debian/acl2-emacs.emacsen-startup
	rm -f debian/acl2.sh pgcl books/Makefile-tmp books/coi/gensym/gensym.out sys-proclaim.lisp
	rm -f books/coi/gensym/Makefile-deps books/coi/gensym/workxxx.gensym books/system/doc/rendered-doc.lsp
	rm -rf doc/HTML-old doc/EMACS-old doc/acl2-wc.txt books/std/io/test.sao
	rm -f books/centaur/bitops/bitsets-opt-raw.o books/centaur/vl/util/gc-raw.o \
		books/centaur/misc/tshell-raw.o books/centaur/vl/Makefile-tmp \
		books/build/Makefile-sources books/build/Makefile-certs
	rm -f books/build/acl2-exports.certdep books/build/acl2-version.certdep \
		books/build/first-order-like-terms-and-out-arities.certdep \
		books/build/ground-zero-theory.certdep gcl_pool
	rm -f $(OVERRIDES)
	rm -f books/centaur/fty/tests/deftagsum-scale.cert.temp books/centaur/fty/tests/deftranssum.cert.temp
	rm -f books/centaur/vl/kit/test.vlzip books/centaur/getopt/demo2 books/centaur/getopt/demo2-test.ok
	rm -f debian/elpa-acl2.elpa debian/acl2-pkg.el
	find books/build/defrec-certdeps -name "*.certdep" -exec rm {} \;
	dh_clean -XTAGS

debian/acl2-infix.install::
	find books/interface/infix -name "*.o" | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/lib/$(PD)/%s\n",$$1,a);}' >>$@
	find books/interface/infix -name "*.sty" | \
		awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/texmf/tex/latex\n",$$1);}' >>$@

debian/acl2-infix-source.install::
	find books/interface/infix -name "*.lisp" | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/lib/$(PD)/%s\n",$$1,a);}' >>$@

# debian/acl2-emacs.install::
# 	find books/interface/emacs -name "*.el" | awk '{printf("%s usr/share/emacs/site-lisp/$(PN)\n",$$1);}' >>$@
# 	find emacs -name "*.el" | awk '{printf("%s usr/share/emacs/site-lisp/$(PN)\n",$$1);}' >>$@

# debian/elpa-acl2.install::
# 	find books/interface/emacs -name "*.el" | awk '{printf("%s usr/share/emacs/site-lisp/$(PN)\n",$$1);}' >>$@
# 	find emacs -name "*.el" | awk '{printf("%s usr/share/emacs/site-lisp/$(PN)\n",$$1);}' >>$@

debian/acl2.install::
	echo debian/acl2.sh usr/bin >>$@
	echo saved_acl2 usr/lib/$(PD) >>$@

debian/acl2-books.install::
	find books -name "*.o" | grep -v interface/ | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/lib/$(PD)/%s\n",$$1,a);}' >>$@

debian/acl2-source.install::
	find * -name "*.lisp" -maxdepth 0 | grep -v TMP1.lisp | awk '{printf("%s usr/share/$(PD)\n",$$1);}' >$@
	find * -name "TAGS" -maxdepth 0 | awk '{printf("%s usr/share/$(PD)\n",$$1);}' >>$@

debian/acl2-books-certs.install::
	find books -name "*.cert" | grep -v fix-cert/moved | grep -v system/pcert | \
		awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@
	find books -name "*.pcert0.final" | \
		awk '{a=$$1;sub(".pcert0.final",".cert",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@

debian/acl2-books-source.install::
	find books -name "*.lisp" | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@
	find books -name "*.acl2" | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@
	find books/bdd -name "bit-vector-reader.lsp" | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/$(PD)/%s\n",$$1,a);}' >>$@

debian/acl2-doc.install::
	echo doc usr/share/doc/acl2-doc >$@
	find books -name "README*" | \
		awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
	find books/textbook -name "*.txt" | \
		awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
	find books/textbook -name "*.html" | \
		awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
	find books/bdd/be/ -type f | awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
	find books/misc -name "simplify-defuns.txt" | \
		awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
	find books/interface/infix -name "README*" | \
		awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
	find books/interface/infix -name "*.ps" | \
		awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
	find books/interface/infix -name "*.dvi" | \
		awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
	find books/interface/emacs -name "README*" | \
		awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@
	find books/arithmetic-2/pass1/arithmetic-axioms.txt | \
		awk '{a=$$1;sub("/[^/]*$$","",a);printf("%s usr/share/doc/$(PN)-doc/%s\n",$$1,a);}' >>$@

debian/acl2.links::
	echo usr/lib/$(PD)/saved_acl2 usr/share/$(PD)/saved_acl2 >$@

debian/acl2-books.links::
	find books -name "*.o" | grep -v interface/ | awk '{printf("usr/lib/$(PD)/%s usr/share/$(PD)/%s\n",$$1,$$1);}' >>$@

debian/acl2-infix.links::
	find books/interface/infix -name "*.o" | awk '{printf("usr/lib/$(PD)/%s usr/share/$(PD)/%s\n",$$1,$$1);}' >>$@

debian/acl2.sh:
	echo "#!/bin/bash" >$@
	echo >>$@
	echo "export ACL2_SYSTEM_BOOKS=/usr/share/$(PD)/books" >>$@
	echo "exec /usr/lib/$(PD)/saved_acl2 -dir /usr/share/$(PD)" >>$@
	chmod 755 $@

%.lintian-overrides: %.lintian-overrides.in
	cat $< | sed "s,@PD@,$(PD),g" > $@

install: DH_OPTIONS=
install: build $(INSTALLS) $(LINKS) debian/acl2.sh debian/README.Debian $(OVERRIDES) #debian/acl2-emacs.emacsen-startup
	dh_testdir
	dh_testroot
	dh_prep -XTAGS
	dh_installdirs

	dh_install

	rm -f debian/acl2-doc/usr/share/doc/acl2-doc/doc/manual/LICENSE
	rm -f debian/acl2-doc/usr/share/doc/acl2-doc/doc/.gitignore

	find debian/acl2-books-source/usr/share/$(PD)/books/quicklisp/bundle/software/ -type f -name release.lisp -exec rm {} \;

	-find debian/acl2-doc/usr/share/doc/acl2-doc// -type f -size 0 -exec rm {} \;

	while ! find debian -type d -empty | awk '{exit 1}' ; do \
		rmdir $$(find debian -type d -empty); \
	done

	for i in $$(find debian -name "*.final"); do mv $$i $${i%.final} ; done
	find debian/acl2-source -name "*.lisp" -type f -exec chmod 444 {} \;
	find debian/acl2-source -name "*.acl2" -type f -exec chmod 444 {} \;
	find debian/acl2-source -name "*.lsp" -type f -exec chmod 444 {} \;
	find debian/acl2-books-source -name "*.lisp" -type f -exec chmod 444 {} \;
	find debian/acl2-books-source -name "*.acl2" -type f -exec chmod 444 {} \;
	find debian/acl2-books-source -name "*.lsp" -type f -exec chmod 444 {} \;

	mv debian/acl2/usr/bin/acl2.sh debian/acl2/usr/bin/acl2

binary-indep: DH_OPTIONS:=-i
binary-indep: build install debian/elpa-acl2.elpa
	dh_testdir
	dh_testroot
	dh_elpa
	dh_installdocs
	dh_installexamples
	dh_installmenu
	dh_installemacsen
	dh_installtex -p acl2-infix
	dh_installcron
	DH_OPTIONS= dh_installinfo -p acl2-doc #$$(find doc/EMACS -name "*.info*")
	dh_installchangelogs
	dh_link
	dh_compress
	dh_lintian
	dh_fixperms
	dh_installdeb
	dh_gencontrol
	dh_md5sums
	dh_builddeb

binary-arch: DH_OPTIONS=-a
binary-arch: build install
	dh_testdir
	dh_testroot
	dh_installdocs
	dh_installexamples
	dh_installmenu
	dh_installemacsen
	dh_installcron
	dh_installman
	dh_installinfo
	dh_installchangelogs
	dh_strip $(NO_STRIP)
	dh_link
	dh_compress
	dh_lintian
	dh_fixperms
	dh_installdeb
	dh_shlibdeps
	dh_gencontrol
	dh_md5sums
	dh_builddeb

binary: binary-indep binary-arch
.PHONY: build build-arch build-indep clean binary-indep binary-arch binary install