Notes for 11/18/2014 ACL2 seminar
A "toothbrush" utility
Matt Kaufmann

Table of contents:

I.   Abstract
II.  Introduction
III. Demo: how to build a "toothbrush" application
IV . Implementation remarks

============================================================
I.   Abstract
============================================================

This talk will present a "toothbrush" utility for creating ACL2
applications that depend on only a small(-ish) fraction of the ACL2
source code.  Warren Hunt wanted this utility in order to create ACL2
applications with a smaller memory footprint than they would have
simply by starting ACL2, loading the application, and then using
save-exec to save an executable.  The "toothbrush" name was bandied
around in the early 1990s at Computational Logic, Inc., the idea being
that you don't want to load all of ACL2 merely to run a toothbrush.

I'll start by going briefly through community book
books/system/toothbrush/README. The remainder of the talk will consist
of two parts:

- A demo will show how to use this utility.

- We'll walk through the "toothbrush" source code, which I think could
  be useful to those who want to do ACL2 programming.

============================================================
II.  Introduction
============================================================

We'll go briefly through books/system/toothbrush/README.

============================================================
III. Demo: how to build a "toothbrush" application
============================================================

To run the demo using "make", do the following.  It assumes that the
value shown for ACL2 is a full pathname of an ACL2 (or ACL2(h), etc.)
executable and that the value shown for LISP is a Lisp executable,
preferably CCL or SBCL.  The ACL2 executable needs to be a reasonably
recent, namely after about November 3, 2014.

Change to suitable directory, for example:

cd /projects/acl2/devel/books/system/toothbrush/

To clean:

make ACL2=/projects/acl2/devel/ccl-saved_acl2h clean

To build in this directory and under tests/:

time nice make -j 4 ACL2=/projects/acl2/devel/ccl-saved_acl2h LISP=ccl

Here is how to do everything manually, without "make":

------------------------------------------------------------

Step 1: Build infrastructure

First make "clean" again, as above:

cd /projects/acl2/devel/books/system/toothbrush/
make ACL2=/projects/acl2/devel/ccl-saved_acl2h clean

------------------------------

(1a) Build defined-syms.lsp, a file that defines a useful function,
CL-DEFINED-P, which returns true when called on a function symbol
defined by the ACL2 system toothbrush.

ccl
(defparameter COMMON-LISP-USER::*acl2-dir* "/projects/acl2/devel/")
(load "make-defined-syms.lsp")
(acl2::exit-lisp)

------------------------------

(1b) Certify the book make-toothbrush.lisp, which defines the main
macro, MAKE-TOOTHBRUSH, to create a "toothbrush" application (.lisp)
file.  Note that function CL-DEFINED-P, defined in this book, is
intended to be overridden by the raw Lisp definition of CL-DEFINED-P
in generated file defined-syms.lsp.

/projects/acl2/devel/ccl-saved_acl2h
(certify-book "make-toothbrush" ? t :ttags (:make-toothbrush))
(quit)

------------------------------------------------------------

Step 2: Build a particular toothbrush

First change to a suitable directory, for example:

cd tests/test1

------------------------------

(2a) Generate toothbrush file.

# Optionally certify application:

/projects/acl2/devel/ccl-saved_acl2h
(certify-book "test1")
(quit)

# Load application and extract toothbrush:

/projects/acl2/devel/ccl-saved_acl2h
(include-book "test1") ; might instead use LD or whatever to load application
(include-book "../../make-toothbrush")
(value :q) ; or :q
(load "../../defined-syms.lsp") ; redefine CL-DEFINED-P
(lp)
; Create output "toothbrush" file to support indicated functions:
(make-toothbrush "test1-toothbrush.lsp" top)
(quit)

# Optionally, compile the toothbrush:

ccl
(defparameter COMMON-LISP-USER::*acl2-dir* "/projects/acl2/devel/")
(load "../../load-toothbrush.lsp")
(acl2::with-suppression (load "test1-toothbrush.lsp"))
(compile-file "test1-toothbrush.lsp")
(acl2::exit-lisp)

# Optionally, run a test:

ccl
(defparameter COMMON-LISP-USER::*acl2-dir* "/projects/acl2/devel/")
(load "../../load-toothbrush.lsp")
(acl2::with-suppression (load "test1-toothbrush"))
(load "tb-test.lsp") ; This particular test should print "SUCCESS"
(acl2::exit-lisp)

============================================================
IV . Implementation remarks
============================================================

We'll go through the how the implementation supports the steps above,
as time permits, and as guided by questions from the group.

If there is interest, I could discuss how Makefiles implement the
steps shown in Section III above.

============================================================