#!/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