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

Checking the Proofs

1. Get the Proofs

Note: the uncompressed proofs take 8 GB of disk space.

Before you can check the proofs, you will need to either

Either way, you should end up with a directory structure like this:

Sources/Proofs/utilities/,
Sources/Proofs/utilities.events,
Sources/Proofs/logic/,
Sources/Proofs/logic.events,
Sources/Proofs/level2/,
Sources/Proofs/level2.events,
and so on.

2. Choose a Lisp Implementation

You will need to install a Lisp environment to run the proof checker.

Here are some options:

CCL -- Recommended, free, high performance

Instructions:

Performance note: at the top of milawa.lisp, there are some CCL-specific settings which configure the garbage collector to collect after every 512 MB. This seems to be appropriate for a system with up to 4 GB of memory. If your system has considerably more memory than this, increasing this threshold may provide better performance.
CMUCL -- Recommended, free, good performance

Instructions:

Performance note: at the top of milawa.lisp, there are some CMUCL-specific settings which configure the garbage collector to collect after every 512 MB. This seems to be appropriate for a system with up to 4 GB of memory. If your system has considerably more memory than this, increasing this threshold may provide better performance.
SBCL -- Recommended, free, multiplatform, good performance

Instructions:

Performance note: at the top of milawa.lisp, there are some SBCL-specific settings which configure the garbage collector to collect after every 512 MB. This seems to be appropriate for a system with up to 4 GB of memory. If your system has considerably more memory than this, increasing this threshold may provide better performance.
CLISP -- free, but very slow!

Instructions:

Macintosh note: I am unable to use clisp on a macbook because I cannot increase the stack size (e.g., ulimit -s) beyond 16384. In my successful runs Linux machines, I use a ulimit of 65535.
Allegro -- commercial, fast, NOT KNOWN TO WORK

Instructions:

I only have access to a copy of Allegro on 32-bit linux, and it runs out of memory in Level 10 on Nemesis. I have tried to address this by using Allegro's build-lisp-image function to create a copy of Allegro with a larger Lisp heap size, e.g.,

(build-lisp-image "big-acl.dxl"
                  :lisp-heap-start "500M" 
                  :c-heap-start "3000M")

Then, I used acl -I big-acl.dxl when building the base Milawa program, but this is still not successful. It may be that a more recent version of Allegro or more powerful computer will be successful.

Scieneer -- commercial, not known to work

Instructions

I have not been able to get scl to complete the proofs, as it segfaults on me during the proofs in the utilities directory. I have not spent much effort to debug this, and perhaps the problem is specific to my platform (Linux x86-64) or fixed in a more recent version.

It may not be difficult to port Milawa to another Lisp implementation. In my experience, you will probably need to increase various resource limits, e.g., the maximum call-stack size, heap size, and so on, to successfully finish the checks. Also, you'll need to implement the save-and-exit function for the new Lisp, or not use checkpointing.

3. Build the Proof Checker

  1. Download milawa.lisp to your Sources directory.
  2. In the Sources directory, start your lisp and run:
    (defconstant image-extension "name")
    (load "milawa.lisp")
    The name you give determines the file extensions for the Milawa images that will be generated. I typically give names like "ccl-linux64" or "sbcl-win32", and so on, so that I know what kind of platform each image is for.

This should produce a new file named base.name, which is the "base system," with no theorems loaded.

At this point, to make sure everything is working you should run

./milawa-lispname base.name

The script may print a message asking you to configure it, e.g., for SBCL and CMUCL you will need to figure out appropriate memory settings for your host. If all is well, it should print "Milawa Proof Checker," and you can quit by sending EOF.

4. Check the Proofs.

Estimated time: 1-2 days (see benchmarks below for a better idea).

Now that everything is set up, you can download final-checks.sh to your Sources directory.

The usage is:

cd /path/to/Sources/
sh final-checks.sh lispname name

This will result in a lot of output, and I generally tee it into a file. After each directory, a checkpoint is taken so that in the event of a power outage or something, you will only lose the current directory's work (which may still be a few hours).

If everything is successful, the file user.name-image will be produced. This image will have the highest-level proof checker already loaded and ready to go.

Proof-Checking Benchmarks

To get a better idea of how long the checks will take, here are some timings from various systems. Note that no effort was made to ensure these computers were unloaded during the checks, so the figures here should be regarded as merely suggestive.

Nemesis

System information: Dell Precision 390 Workstation running 32-bit Linux 2.6.24.6+desktop7+24.57 #1 SMP, Intel Core 2 6400 @ 2.13 GHz, 2 MB L2 cache, 4 GB memory.

Jordan

System information: Home-built workstation running 64-bit Linux version 2.6.28-15-generic #52 Ubuntu SMP, Intel Core 2 Duo E8400 @ 3.0 GHz, 6 MB L2 cache, 4 GB memory.

Lhug-3

System information: HP Proliant DL585 server running 64-bit Linux 2.6.24.6+desktop7+24.57 #1 SMP, AMD Opteron Processor 850 @ 2.2 GHz, 1 MB cache, 32 GB memory.

Cele

System Information: Macbook laptop running Darwin 9.7.0, Intel Core 2 Duo Processor @ 2.4 Ghz, 4 GB memory.