Building Milawa

This will take awhile and you will probably need to install lots of software. Please email if you have any problems.

Recommended hardware:

1. Install Prerequisite Software

You will need a reasonable Unix environment (bash, make, perl, ...), and also some less common 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 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. Replace the books/ directory with those from the acl2-books project
  5. Build the books, i.e., make ACL2=acl2 regression -j N, where N is the number of cores your machine has available.

2. Obtaining Milawa Sources

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

You can get either:

(Alternate option: Replace trunk with tags/dissertation for the version as of my dissertation, which diverges in some ways and has different requirements; see the archive version if you want to do this.)

3. Building ACL2 Books

Estimated time: a couple of hours.

If you have some kind of cluster, look at Sources/ACL2/Makefile and see if you can write a startjob command that will work.

  1. cd Milawa/Sources/ACL2
  2. make -j N interface/top.cert, where N is the sum of all available CPU cores.

4. Bootstrapping

This takes a LOT of CPU time.

  1. cd Milawa/Sources/ACL2
  2. make -j N, where N is the sum of all available CPU cores.

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.