Build
Instructions for obtaining and building Milawa.
Milawa has a close relationship with ACL2. All of its tactics can
be thought of as both ACL2 and Milawa functions. The full bootstrapping proof
is first "sketched" in ACL2, and then "re-discovered" or "formalized"
with Milawa.
This documentation describes how to build the ACL2-related portion of
Milawa. But these instructions do not cover Magnus Myreen's work on
jitawa, and the HOL4 verification of Milawa's kernel.
The Milawa source code is now included in the ACL2 Community Books project.
However, Milawa is not built during the "make" of the ordinary ACL2 Community
Books, because building it:
- takes several hours
- requires a lot of memory and hard disk space, and
- requires Clozure Common Lisp (CCL).
Instead, to build Milawa, you should:
- Build CCL and ACL2 according to the instructions in
books/centaur/README.html.
- Then run these commands:
$ cd acl2/books/projects/milawa/ACL2
$ make -j <n> # n is how many jobs to run in parallel
Where <n> is appropriate for your computer, e.g.:
- As large as possible, but
- No more than your number of CPU cores, to avoid excessive
task switching overhead.
- No more than (Physical_Memory / 4 GB), to avoid death by swapping.
A successful build should result in:
- Several new ACL2 images in acl2/books/projects/milawa/ACL2/acl2-images/
including one called user-symmetry
- ACL2 certificates (.cert) or "ACL2 Milawa Provisional
Certificates" (.mpcert) for files throughout the milawa/ACL2 directory
- Thousands of proof files throughout the milawa/Proofs directory.
These proof files are the "boostrapping proofs" that can now be checked by
the Milawa kernel. There are many options here: Milawa has two kernels:
- The original kernel, a Common Lisp program that has historically been run
successfully on at least CCL, SBCL, CMUCL, and (for the very patient) CLISP, on
certain platforms. In this case, the proof files can be processed
directly.
- The new kernel, either a Common Lisp or Jitawa Lisp program, that can be
run on at least CCL, SBCL, and Jitawa (a verified Lisp by Magnus Myreen). In
this case, the proof files first need to be further collected and
compressed.
See final-checks for information about how to build the Milawa
kernel on your choice of Lisps, and how to use it to check these proofs.
