# -*- Fundamental -*- # ACL2 Version 1.9 -- A Computational Logic for Applicative Common Lisp # Copyright (C) 1997 Computational Logic, Inc. # This program is free software; you can redistribute it and/or modify # it under the terms of the GNU General Public License as published by # the Free Software Foundation; either version 2 of the License, or # (at your option) any later version. # This program is distributed in the hope that it will be useful, # but WITHOUT ANY WARRANTY; without even the implied warranty of # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # GNU General Public License for more details. # You should have received a copy of the GNU General Public License # along with this program; if not, write to the Free Software # Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. # Written by: Matt Kaufmann and J Strother Moore # email: Matt_Kaufmann@email.mot.com and Moore@cs.utexas.edu # Computational Logic, Inc. # 1717 West Sixth Street, Suite 290 # Austin, TX 78703-4776 U.S.A. # At CLI the various Lisp images located using meta-x info and going to the # node Lisp Implementations Available at CLI. # Example invocations for users: # make ; Build saved_acl2 from scratch. Same as make small. # make small ; Build saved_acl2 from scratch. # make large ; Build large-saved_acl2 from scratch. # make both ; Build both large and small images from scratch. # make LISP=cl PREFIX=allegro- # make LISP=lisp PREFIX=lucid- # make LISP="lispworks -init -" PREFIX=lispworks- # ; Same as make, except that image is named # ; allegro-saved_acl2 and the image is built on top of # ; a Common Lisp executable called cl (similarly for the # ; other two examples). # ; Note from Rich Cohen: # ; The "-init -" tell Lispworks not to load the user's # ; initialisation file. By default Lispworks will load # ; ~/.lispworks at start-up, regardless of the current # ; working directory. Further, when you attempt to save a # ; core image, Lispworks notes that you previously loaded # ; your personal initialisation file, and requires # ; confirmation before saving the core image. # make TAGS ; Create tags table, handy for viewing sources with emacs. # make certify-books # ; Certify all the example books using current acl2 command # ; (Implementors might wish to use certify-books-test # ; below). # make certify-books PREFIX=xxx- EXT=wfasl # ; Same as make certify-books, but use xxx-saved_acl2, # ; where the Lisp underlying xxx-saved_acl2 uses the # ; extension .wfasl for compiled files. (The default value # ; of EXT is .o, which is correct for GCL and AKCL. If # ; PREFIX is unspecified, then saved_acl2 is used.) NOTE: # ; PREFIX may only be used to specify a pathname relative # ; to the directory of this makefile. # make clean-books ; Remove certificate files, object files, log files, # ; debris, ..., created by `make certify-books'. ############################################################################### # NOTE: Users need not read below this line. Neither should installers of # ACL2 at sites other than CLI. We have no reason to believe that the make # commands illustrated below will work at sites other than CLI. Indeed, we # have reasons to believe they will not! A typical problem is that we refer # to a file or directory that exists at CLI but that is not created when our # installation instructions are followed at other sites. # Example invocations for CLI implementors: # WARNING: Implementors should NOT use `make large'. Let's call all our # images saved_acl2, except perhaps for prefixes indicating for example the # underlying Lisp used in building the image. # NOTE: make small and make large both completely recompile, initialize and # save. Consider some of the "fast" and "very-fast" options below if only # part of the system needs to be rebuilt. # make big-test # ; Build the large image from scratch, make the DOC files in # ; EMACS (TexInfo), HTML, and TEX, build the small image, # ; certify all the books, prove through axioms.lisp. # ; Typical invocations: # make big-test >& make-big-test.log& # make big-test LISP=cl PREFIX=cl- >& make-cl-big-test.log& # make test # ; Build the system from scratch, certify all books, and # ; prove through axioms.lisp. Consider "make test DOC" if # ; running late at night (so that you don't smash someone's # ; documentation). # make very-fast init # ; Build the system, recompiling as little as possible # ; (perhaps don't even recompile TMP1.lisp). # make distribution # ; Build the system for distribution via ftp. # make fast init ; Compile as needed, initialize, build full-size saved_acl2 # make fast-small init-small # ; Compile as needed, initialize, build small saved_acl2. # make very-fast-small init-small # ; As above, only compiling files with out of date objects. # make full ; A complete recompilation whether needed or not. # make full init ; Completely recompile, initialize and save. # make full-meter init ; Completely recompile with meters, init and save. # make init ; Just build full-size saved_acl2. # make small ; Completely recompile and then build small saved_acl2 image. # make check-sum ; Call only after ACL2 is completely compiled. # make full LISP=lucid PREFIX=lucid- ; makes acl2 in Lucid # make full LISP=cl PREFIX=allegro- ; makes acl2 in allegro # ; Note: Allegro is not always named cl at CLI. See # ; ~moore/allegro/runcl for some clues. # make full LISP=lispworks PREFIX=lispworks- ; makes acl2 in lispworks # make copy DIR=targetdir ; copies all of acl2 to targetdir. Don't use ~ notation. # make DOC ; Build html and emacs info files # make clean-doc ; Remove debris created by make DOC # make red ; Just build full-size saved_acl2, but do so without pass 2 # make proofs ; Assuming sources are compiled, initialize without skipping # ; proofs during pass 2. Does not save an image. Uses same # ; flags used to build full-size image. # make certify-books-test # ; Certify all the example books using # ; `pwd`/${PREFIX}saved_acl2, e.g., # ; /slocal/src/acl2/v1-9/saved_acl2. This is different # ; from certify-books because that command uses whatever # ; acl2 is invoked by the shell command acl2. # Metering: If the currently compiled version is unmetered and you wish # it metered, the fastest thing to do is to (push :acl2-metering *features*) # and then yank in and recompile just those definitions that mention # acl2-metering. However, if you would like to install metering as part # of a system-wide recompilation, you must use the full-meter option below, # rather than the fast-meter option. If, while running a fully metered # system you wish to do what would otherwise be a make fast but you want # to preserve the metering, use the fast-meter option. If you want to # get rid of the metering in the compiled code, do make full. LISP = gcl DIR = /tmp PREFIX = "" sources = axioms.lisp basis.lisp type-set-a.lisp type-set-b.lisp\ translate.lisp rewrite.lisp simplify.lisp bdd.lisp\ other-processes.lisp induct.lisp prove.lisp\ proof-checker-a.lisp history-management.lisp defuns.lisp defthm.lisp\ other-events.lisp ld.lisp proof-checker-b.lisp interface-raw.lisp\ defpkgs.lisp small: full-small init-small-pass1 init-small fast: check date rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::quick-compile-acl2 nil nil)' >> workxxx ${LISP} < workxxx rm -f workxxx fast-small: check date rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::quick-compile-acl2 nil t)' >> workxxx ${LISP} < workxxx rm -f workxxx check: date rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::check-suitability-for-acl2)' >> workxxx ${LISP} < workxxx rm -f workxxx compile-ok: date rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::note-compile-ok)' >> workxxx ${LISP} < workxxx rm -f workxxx very-fast: check date rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::quick-compile-acl2 t nil)' >> workxxx ${LISP} < workxxx rm -f workxxx very-fast-small: check date rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::quick-compile-acl2 t t)' >> workxxx ${LISP} < workxxx rm -f workxxx fast-meter: check date rm -f workxxx echo '(load "init.lsp") (push :acl2-metering *features*)' > workxxx echo '(acl2::quick-compile-acl2 nil nil)' >> workxxx ${LISP} < workxxx rm -f workxxx check-sum: date rm -f workxxx echo '(load "init.lsp") (acl2)' > workxxx echo '(acl2::make-check-sum-file)' >> workxxx ${LISP} < workxxx rm -f workxxx full: TAGS check rm -f workxxx rm -f acl2-fns.o acl2-fns.lbin acl2-fns.sbin acl2-fns.fasl acl2-fns.wfasl echo '(load "init.lsp")' > workxxx echo '(acl2::compile-acl2 nil)' >> workxxx ${LISP} < workxxx rm -f workxxx full-small: TAGS check rm -f workxxx rm -f acl2-fns.o acl2-fns.lbin acl2-fns.sbin acl2-fns.fasl acl2-fns.wfasl echo '(load "init.lsp")' > workxxx echo '(acl2::compile-acl2 t)' >> workxxx ${LISP} < workxxx rm -f workxxx full-meter: check date rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::make-tags)' >> workxxx echo '(push :acl2-metering *features*)' >> workxxx echo '(acl2::compile-acl2 nil)' >> workxxx ${LISP} < workxxx rm -f workxxx copy: rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::copy-acl2 "${DIR}")' >> workxxx ${LISP} < workxxx rm -f workxxx TAGS: acl2.lisp acl2-check.lisp acl2-fns.lisp acl2-init.lisp ${sources} rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::make-tags)' >> workxxx ${LISP} < workxxx rm -f workxxx init: # Note: If you believe that compilation is up-to-date, do # make compile-ok init # rather than # make init. rm -f workxxx echo -n "" >> ${PREFIX}osaved_acl2 rm -f ${PREFIX}osaved_acl2 echo '(load "init.lsp")' > workxxx echo '(acl2::save-acl2' "'(acl2::initialize-acl2 (quote acl2::include-book) acl2::*acl2-pass-2-files* nil))" >> workxxx ${LISP} < workxxx echo -n "" >> ${PREFIX}saved_acl2 mv -f ${PREFIX}saved_acl2 ${PREFIX}osaved_acl2 mv -f nsaved_acl2 ${PREFIX}saved_acl2 rm -f workxxx rm -fr saved mkdir saved cp *.lisp saved rm -f workxxx proofs: compile-ok rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::load-acl2 nil)' >> workxxx # Don't bother building TMP1.* files. echo '(setq acl2::*compiled-*1*-fns* t)' >> workxxx echo '(acl2::initialize-acl2 nil acl2::*acl2-pass-2-files* nil)' >> workxxx ${LISP} < workxxx rm -f workxxx DOC: rm -f workxxx PREFIX=$(PREFIX) ; export PREFIX ; doc/create-acl2-html PREFIX=$(PREFIX) ; export PREFIX ; doc/create-acl2-texinfo rm -f workxxx TEXINFO: rm -f workxxx PREFIX=$(PREFIX) ; export PREFIX ; doc/create-acl2-texinfo rm -f workxxx HTML: rm -f workxxx PREFIX=$(PREFIX) ; export PREFIX ; doc/create-acl2-html rm -f workxxx clean: # Does not remove TAGS rm -f *.o *#* *.c *.h *.data gazonk.* workxxx \ *.lbin *.sbin *.fasl *.wfasl *.fn acl2-status.txt *.log TMP* saved/* rm -f *~ */*~ */*/*~ */*/*/*~ red: compile-ok rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::save-acl2' "'(acl2::initialize-acl2 nil nil nil))" >> workxxx ${LISP} < workxxx echo -n "" >> red-${PREFIX}saved_acl2 mv -f red-${PREFIX}saved_acl2 red-${PREFIX}osaved_acl2 mv -f nsaved_acl2 red-${PREFIX}saved_acl2 rm -f workxxx rm -fr saved mkdir saved cp *.lisp saved init-small: rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::save-acl2' "'(acl2::initialize-acl2 (quote acl2::include-book) acl2::*acl2-pass-2-files* t))" >> workxxx ${LISP} < workxxx echo -n "" >> ${PREFIX}saved_acl2 mv -f ${PREFIX}saved_acl2 ${PREFIX}osaved_acl2 mv -f nsaved_acl2 ${PREFIX}saved_acl2 rm -f workxxx rm -fr saved mkdir saved cp *.lisp saved rm -f workxxx init-small-pass1: rm -f workxxx echo '(load "init.lsp")' > workxxx echo '(acl2::load-acl2 t)' >> workxxx echo '(acl2::initialize-acl2 (quote acl2::include-book) acl2::*acl2-pass-2-files* t t)' >> workxxx ${LISP} < workxxx rm -f workxxx # CAREFUL! Do not use large unless you want the image renamed to large-.... large: full init move-large move-large: mv ${PREFIX}saved_acl2 large-${PREFIX}saved_acl2 # It's important to make the large image first, in order to trust the small one. both: large small certify-books: ACL2=acl2 ; cd books ; rm -f public/*.cert ; rm -f data-structures/*.cert ; make ACL2=$$ACL2 certify-books-test: ACL2=`pwd`/${PREFIX}saved_acl2 ; \ cd books ; \ touch placeholder.log ; \ mv *.log ../saved ; \ rm -f public/*.cert ; \ rm -f data-structures/*.cert ; \ make ACL2=$$ACL2 # The next two targets can be used with certify-books-test to run the # test with infix syntax output. Just do # make infix-init certify-books-test infix-fin >& make.log & # If you want to do the certification twice, first with infix and then # without, use # make infix-init certify-books-test infix-fin certify-books-test >& make.log & # To get the books certified while using infix printing we arrange for the # connected directory to contain an init.lsp file which is not normally there. # The init.lsp file we put there is just a symbolic link to our # infix-patch.lisp which loads all the infix stuff. If we do not want infix # printing during the book certification, we must make sure to remove those # init.lsp files, as done by infix-fin. That also moves the .log and .out # files to the v1-9/infix-logs/ subdirectory, where they overwrite the old # files there, if any. infix-init: cd /slocal/src/acl2/v1-9/books ; \ rm -f */init.lsp ; \ rm -f *.log ; \ rm -f public/*.cert ; \ rm -f data-structures/*.cert ; \ ln -s /slocal/src/acl2/v1-9/infix-patch.lisp arithmetic/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch.lisp bdd/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch.lisp cowles/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch.lisp meta/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch.lisp nqthm/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch.lisp public/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch.lisp data-structures/init.lsp infix-init10: cd /slocal/src/acl2/v1-9/books ; \ rm -f */init.lsp ; \ rm -f *.log ; \ rm -f public/*.cert ; \ rm -f data-structures/*.cert ; \ ln -s /slocal/src/acl2/v1-9/infix-patch-10.lisp arithmetic/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch-10.lisp bdd/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch-10.lisp cowles/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch-10.lisp meta/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch-10.lisp nqthm/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch-10.lisp public/init.lsp ; \ ln -s /slocal/src/acl2/v1-9/infix-patch-10.lisp data-structures/init.lsp infix-fin: rm -f /slocal/src/acl2/v1-9/infix-logs/*.* ; \ cd /slocal/src/acl2/v1-9/books ; \ cp *.log /slocal/src/acl2/v1-9/infix-logs/ ; \ cp public/*.out /slocal/src/acl2/v1-9/infix-logs/ ; \ cp data-structures/*.out /slocal/src/acl2/v1-9/infix-logs/ ; \ rm -f */init.lsp clean-doc: cd doc ; rm -f *.o *~* *#* TAGS *.c *.h *.data gazonk.* workxxx \ *.lbin *.sbin *.fasl *.wfasl *.fn *.cert rm -f doc/EMACS/acl2-doc-emacs.texinfo rm -f doc/EMACS/saved/* rm -f doc/LEMACS/acl2-doc-lemacs.texinfo rm -f doc/LEMACS/saved/* rm -f doc/HTML/saved/* rm -f doc/TEX/saved/* cd doc/TEX ; rm -f acl2-book.aux acl2-book.cp acl2-book.cps \ acl2-book.fn acl2-book.ky acl2-book.log acl2-book.pg acl2-book.tex \ acl2-book.toc acl2-book.tp acl2-book.vr cd doc/TEX ; gzip acl2-book.ps cd doc/TEX ; gzip acl2-book.dvi clean-books: cd books ; rm -f *.log *~ */*.cert */*.out */*.date */*.o */*~ \ */*.lbin */*.sbin */*.fasl */*.wfasl */*.fn */*.log # Note that we have hardwired in the directory name below. We don't expect # anyone other than CLI implementors to use this target. Be sure to edit # the pathname for future versions after v1-9. distribution: rm -f workxxx rm -f workyyy echo '(load "init.lsp")' > workxxx echo '(acl2::copy-distribution "workyyy" "/slocal/src/acl2/v1-9")' >> workxxx ${LISP} < workxxx # The following command causes an error (which is good) if check-distribution # fails. chmod 777 workyyy echo "Making distribution directory." workyyy echo "Done. Now creating tar file." cd ../acl2-sources ; make tar # This following should be executed inside the acl2-sources directory. # You probably need to be the owner of all files in order for the chmod # commands to work, but perhaps not. tar: rm -f acl2.tar.Z acl2.tar.gz acl2.tar rm -f SUM # We want the extracted tar files to have permission for everyone to write, # so that when they use -p with tar they get that permission. # But we don't want the tar file itself to have that permission. We may as # well protect all the other files too from writing by CLI people other than # those in the acl2 group, even though these files aren't the ones transferred # to the ftp server. Those come from the tar file, and we will extract them # without the -p option so that the ftp files will not be world-writable. cd .. ; chmod -R g+w acl2-sources ; chmod -R o+w acl2-sources ; tar cvf /tmp/acl2.tar acl2-sources ; chmod -R o-w acl2-sources mv /tmp/acl2.tar . gzip acl2.tar sum acl2.tar.gz > acl2.tar.gz.SUM rm -f workxxx rm -f workyyy # Consider "make test DOC" if running late at night. test: full init certify-books-test proofs big-test: full init DOC move-large small certify-books-test proofs