README
1==========================================================================
2These files were written by and are maintained by Matt Kaufmann and
3Mike Gordon. This README file is an abbreviated version (created by
4MJCG) of Matt's longer original file.
5==========================================================================
6
7Contents:
8
9.cert and .o files: Generated by (certify-book "...").
10
11Makefile To re-certify ACL2 books in this directory
12README This file
13a2ml.lisp ACL2 book to translate internal form ACL2 file to ML file
14a2ml.csh Shell wrapper for a2ml.lisp
15axioms-essence.csh Shell wrapper for a2ml.lisp, customized to handle
16 ACL2 source file axioms.lisp
17 (called in tests/round-trip/doit)
18book-essence.lisp Utility mapping an ACL2 input file to input for a2ml.csh
19book-essence.csh Shell wrapper for book-essence.lisp
20check-file.lisp Utility for checking round-trip output
21untranslate-file.lisp Utility for generating file of pretty DEFP forms from
22 a file of DEFUN forms
23
24obsolete/ Superseded files, to keep around for awhile
25
26==========================================================================
27
28Usage:
29
30First do this, after suitably editing ../.acl2holrc.bash:
31
32 source ../.acl2holrc.bash
33
34To update tools after updating their sources:
35
36 ./make
37
38To map ACL2 source file axioms.lisp to input for a2ml.csh:
39
40 ./axioms-essence.csh outfile
41
42To map other than ACL2 source file axioms.lisp to input for a2ml.csh:
43
44 ./book-essence.csh infile outfile
45
46To convert a file of ACL defun, mutual-recursion, defaxiom, defthm
47events into a file that can be read into HOL:
48
49 ./a2ml.csh infile outfile
50
51The outfile created will contain
52
53 val _ = current_package := <package-name>
54
55 val _ = sexp.acl2_list_ref := [<mlsexp1>, ... ,<mlsexpn>]
56
57where <package-name> evaluates to an ML string (e.g. "ACL2") and
58<mlsexp1>, ... ,<mlsexpn> are ML expressions of type mlsexp that
59represent the corresponding ACL2 s-expressions in infile (the
60apparently redundant "val _ = " is boilerplate needed if the file is
61to be compiled).
62
63==========================================================================
64
65