Top-level README for IACL2 (Infix ACL2)

April 1, 1997. Michael K. Smith

Copyright (C) 1996-97 Computational Logic, Inc. (CLI). All rights reserved.
This software is subject to the same license agreement as ACL2
See your ACL2 distribution.


CONTENTS

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



Comments, bugs, suggestions: Send email to Michael K. Smith at mksmith@cli.com


USE

IACL2 provides two capabilities, both directed at presentation.

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

A conventional infix inteface to ACL2 is provided. IACL2 also includes some preloaded libraries that support list, alist, and record types and reasoning about them.

For example:

 type ilist = integer *;

 function foo (x : integer, y : cons) : ilist { cons(x,y) };
The "type" ilist recognizes lists of integers. Because ":>" is an infix version of cons, foo could be stated:
 function foo (x : integer, y : cons) : ilist { x :> y };
The type and function above are equivalent to the prefix syntax:
 (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.

You can translate a file to a simple infix ascii text file, to an HTML file suitable for browsing, or to an input file for the Latex or Scribe document formatting programs. This infix printing is extensible, so that you can specify arbitrarily elaborate formatting for user functions.

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
The simplest calls are then
   (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

The simplest approach is to use the "doinfix" shell script.

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

You can also run the formatter from within 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

To obtain IACL2 by ftp using Unix or a Unix variant,
  1. connect to ftp.cs.utexas.edu by anonymous login.
  2. `cd' to /pub/moore/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 you are running Unix with versions of sed and the following GNU tools - Bison, Flex, GCC & GCL. C compilers other than GCC are possible but we haven't tried them. We use GCL for our Common Lisp and have not experimented with other Lisp implementations. Note that ACL2 has been extensively tested on multiple lisps, but we have not had the resources to do so with this interface.

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


BUILDING THE SYSTEM

A. Editing Makefile.settings, etc.

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 any of the above hold, you may need to edit Makefile.settings before starting. If you DO maintain multiple versions, but the directory that the tar file resides in includes the version as part of its pathname you don't need to modify VERSION.

B. Building iacl2 and doinfix.

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

 make
which will
  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'.
This does not put iacl2 into any sort of local bin directory, that's your job.


TESTING THE SYSTEM

Once that is complete, you can run some parser and printer tests by executing:
 make tests
This checks that the parser and the ascii version of the printer are in synch. At the end of this test you should see:
- benchmarks versions 1.x and 2.x differ
- embedding versions 1.x and 2.x differ
These files, while literally different, are semanticly equivalent. If anything else shows up, something is wrong. Please notify mksmith@cli.com.