WARNING: ARCHIVE VERSION

Milawa has changed since my dissertation. The current version can be found here. This page is a "snapshot" of how the original web site looked, mostly. (I screwed up the file listing slightly by svn updating to revision 507, but otherwise things are unchanged.)

Milawa

Building Milawa

This will take awhile and you will probably need to install lots of software.

Recommended hardware:

1. Install Prerequisite Software

Required: Clozure Common Lisp

  1. Follow their directions to get the most recent SVN snapshot.
  2. Add a symlink to the ccl executable, named ccl, to your $PATH.

Required: ACL2 3.4 with Hons

  1. Download acl2.tar.gz from their web site
  2. Build ACL2h with CCL, e.g., make LISP=ccl ACL2_HONS=h
  3. Add a symlink to the saved_acl2h executable, named acl2, to your $PATH.
  4. Build the ACL2 system books, e.g., make ACL2=acl2 regression -j N, where N is the number of cores your machine has available.

Required: OMake 0.9.8.5

Recommended (if using multiple computers): addjob

2. Obtaining Milawa Sources

The latest version of the sources may be obtained via Subversion.

You can get either:

(Alternate option: Replace tags/dissertation with trunk for the most recent version, which may diverge in some ways from the dissertation.)

If the server does not respond:

3. Build ACL2 Books for Milawa

Estimated time: up to 2 hours.

  1. (If using addjob): start the addjob-server on your "main machine"
  2. cd Milawa/Sources/ACL2/interface
  3. omake -j N, where N is the sum of all available CPU cores.

4. Bootstrapping

This takes a LOT of CPU time.

  1. (If using addjob): start the addjob-server on your "main machine"
  2. cd Milawa/Sources/ACL2/bootstrap
  3. omake -j N, where N is the sum of all available CPU cores.

I typically use eight, 8-core 2.15 GHz Opterons, with omake -j 64. It keeps them all fairly busy for maybe an hour, then drops off to a few cores for another few hours.

Successful bootstrapping leaves you with:

5. Final Proof Checking

Please see the separate instructions for building a core proof checker using your choice of lisps, and using it to check the proofs.