Building Milawa

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

Recommended hardware:

• 64-bit, x86 Linux machine(s); 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 in a cluster

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:

• Source code only, about 20 MB:

     svn checkout svn://uvanimor-3.cs.utexas.edu:34567/Milawa/trunk/Sources <target>
     

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

      svn checkout svn://uvanimor-3.cs.utexas.edu:34567/Milawa/trunk <target>
      

(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:

• 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.