Building Milawa

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

Recommended hardware:

• 64-bit, x86 Linux machines (others kinds might work)
• 8 GB of physical memory (4 might work)
• 30 GB of free hard disk space
• Ideally, many such machines, sharing a file system

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

• You may need to first install ocaml.

Recommended (if using multiple computers): addjob

• Allows the build to be distributed across the network.
• The Milawa build system will try to use addjob if it is installed.
• You may need to first install Ruby.

2. Obtaining Milawa Sources

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

You can get either:

• Source code only, about 20 MB:

     svn checkout svn://nemesis.cs.utexas.edu/u/jared/Subversion/Milawa/trunk/Sources 
     

• Everything (sources, documentation, web pages, ...), about 250 MB:

      svn checkout svn://nemesis.cs.utexas.edu/u/jared/Subversion/Milawa/trunk 
      

If the server does not respond:

• Please email jared@cs.utexas.edu if it is down.
• I have to manually run an SVN server on nemesis, and if the machine gets rebooted I have to restart it.

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:

• Your Milawa/Sources/Proofs directory will contain the resulting proof files.
• You will have several "symmetry" executables, which contain the Milawa user interface at various stages of the bootstrapping process. In particular:
  

  Milawa/Sources/ACL2/bootstrap/utilities/symmetry
  Milawa/Sources/ACL2/bootstrap/logic/symmetry
  Milawa/Sources/ACL2/bootstrap/level2/symmetry
  Milawa/Sources/ACL2/bootstrap/level3/symmetry
  ...
  Milawa/Sources/ACL2/bootstrap/level11/symmetry
  Milawa/Sources/ACL2/bootstrap/user/symmetry
  

  You can use these programs to carry out your own proofs in Milawa. The symmetry executable in the user directory has our highest-level proof checker already verified and loaded.

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.