1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
----------------------------------------------------------------------
Book Certification
----------------------------------------------------------------------
We recommend using the latest development version of ACL2 to certify
our proofs.
1. To certify books, execute the following:
make ACL2=<Path to the ACL2 directory>/saved_acl2
If you already set up an environment variable ACL2 on your machine,
just simply run "make" to certify books. Here is how we set up this
variable.
* On Linux, add the following command to .cshrc:
setenv ACL2 <Path to the ACL2 directory>/saved_acl2
* On Mac, add the following command to .bash_profile:
export ACL2=<Path to the ACL2 directory>/saved_acl2
2. To remove certificate files, etc., execute the following:
make clean ACL2=<Path to the ACL2 directory>/saved_acl2
Or just "make clean" if you already set up the ACL2 environment
variable described above.
See Makefile for details.
----------------------------------------------------------------------
Book Organization
----------------------------------------------------------------------
arith-utils.lisp: Arithmetic utilities
rtl-utils.lisp: RTL utilities
|
