CONTENTS

1. Use
2. Running IACL2
3. Getting the System
4. SYSTEM REQUIREMENTS
5. BUILDING THE SYSTEM
6. TESTING THE SYSTEM

USE

• an infix interface to ACL2 and
• a formatting capability for ACL2 input files. Formatting options include ASCII, LATEX, HTML, and SCRIBE.

The first is intended to make initial experiments with ACL2 somewhat simpler for those unfamiliar with or opposed to Lisp prefix syntax. It is not an inteface for experts, as some of the more advanced aspects of ACL2 are not supported by the infix parser.

The second aids the user in presenting results in nicely formatted conventional syntax. For example, in LaTex mode comments are formatted as running text, events are indexed and substitutions are made of Tex mathematical symbols for various functions. In HTML mode, cross references are created between function usage and definition.

Other documentation is available:

1. Publishing ACL2 provides the most information on the translation of ACL2 source files to LaTeX, HTML, ascii, and Scribe.
2. printer/README provides an overview of printing.
3. Syntax of IACL2 provides the a fairly extensive description of the infix syntax.

INFIX INTERFACE TO ACL2

For example:

 type ilist = integer *;

 function foo (x : integer, y : cons) : ilist { cons(x,y) };

 function foo (x : integer, y : cons) : ilist { x :> y };

 (deflist ilist (l) (declare (xargs :verify-guards t)) integerp)

 (defun foo (x y)
   (declare (type integer x) (type cons y))
   (cons x y))

 (defthm foo-type
   (imples (and (integerp x) (consp y)) (ilist (foo x y))))

II. INFIX PRINTING OF ACL2 FILES.

There are two approaches.

1. Run the doinfix command (./printer/doinfix). The command with no arguments will provide brief documentation of options.

2. Start up IACL2 (iacl2) and do:

 :q                              ;; to exit the ACL2 loop

   (infix-text   "file.lisp") ;; produces file.x
   (infix-latex  "file.lisp") ;; produces file.tex
   (infix-scribe "file.lisp") ;; produces file.mss
   (infix "file.lisp")        ;; if file-syntax.lisp is present

See printer/README.

Running IACL2

% iacl2

 ;; :out is for output, :in for input, t for both.
 ACL2 !>(assign infixp :out | t | nil)  

 ;; Optionally
 ACL2 !>(assign ld-pre-eval-print t) 
 ;; This prints before evaluation, which can be handy if you are
 ;; in infixp = :out mode, in which case you can enter in
 ;; standare acl2 and see what your input would be like in infix.

Translating to ascii, LaTex, HTML, or Scribe

doinfix [ options ] files

Options :

    -m [ ascii, latex, html, scribe, ... ]  
               Basic mode of output. Default = ascii. Will produce an output
               file with the appropriate suffix (.x, .tex, .html, .mss). 

    -c [ text, verbatim, c, cl]
               Comment formatting. Default depends on mode.
               Comments may be treated in a variety of ways
               The table below lists formats for major comment forms

                     text     verbatim  c        cl
                     ------------------------------------
                 ;   text     verbatim  comment  emphasis
                 ;;  text     verbatim  comment  format
                 ;;; verbatim verbatim  comment  text
                 #|  text     verbatim  comment  text

    -prefix    Overrides infix printing.

    -index     Create index or cross references.
    -calls     Index or cross reference calls.
    -hints     Print hints.

    -nohints   Suppress hints.
    -noguards  Suppress printing of guards (except as types).
    -nokeys    Suppress printing of all keyword args.
    -nolocals  Suppress printing of toplevel locals
    -noverify  Suppress printing verify-guards events.

    -format!   Format ! commands in comments.

Formatting from withing IACL2

% iacl2
  ...
ACL2 !>:q
  ...
;; Then do one of the following.

ACL2>(infix-ascii  "file.lisp") ;; produces file.x
ACL2>(infix-latex  "file.lisp") ;; produces file.tex
ACL2>(infix-hmtl   "file.lisp") ;; produces file.html
ACL2>(infix-scribe "file.lisp") ;; produces file.mss
ACL2>(infix "file.lisp")        ;; if file-syntax.lisp is present

GETTING THE SYSTEM

1. connect to ftp.cs.utexas.edu by anonymous login.
2. `cd' to /pub/moore/acl2/infix
3. Be sure to use binary mode, e.g., execute the ftp command `binary'
4. `get' the file `iacl2.tar'
5. exit ftp

Create a directory in which you wish to build the system and move the tar file there.

Untar the distribution by executing

 tar xpf iacl2.tar

This will create subdirectories named `printer', `parser', and `books', which contains the sources and examples, as well as a top level Makefile, README, and other misc. files.

SYSTEM REQUIREMENTS

We assume the C preprocessor, cpp, is in /usr/ccs/lib/cpp.

BUILDING THE SYSTEM

You should only need to touch this file if:

1. You choose to maintain multiple versions (possibly for multiple hardware platforms),
2. you need to use a C compiler other than GCC or
3. you have your executable Acl2 image somewhere such that the command `acl2' is not sufficient to execute it. Note that this Acl2 needs to be at least version 1.9.

• IF YOU ARE NOT USING GCC, you need to change the parser/Makefile variables, CC and possibly CFLAGS. That makefile also assumes the existence of BISON and FLEX. We have not tried YACC and LEX.

B. Building iacl2 and doinfix.

To build the system, cd to the installation directory and execute

 make

1. edit Makefile.settings (if you have already hand edited it this may turn out to be a no-op) and infix-interface.lisp.
2. create Makefile.csettings.
3. build and install everything
4. make a core image called `iacl2'.

TESTING THE SYSTEM

 make tests

- benchmarks versions 1.x and 2.x differ
- embedding versions 1.x and 2.x differ