		Search-engine friendly clone of the ACL2 documentation.

Milawa

Final-checks

How to build the Milawa kernel on your choice of Lisps, and use it to check the proofs produced by the bootstrapping process.

After you have done a build, you will have thousands of proof files throughout the milawa/Proofs directory. Here, we explain how to create a standalone Milawa proof checker, and use it to check these proofs with a Common Lisp implementation. The instructions for Jitawa are different; see jitawa-checks.

1. Choose a Lisp Implementation

You will need to install a Lisp environment to run the proof checker. Many options may work.

CCL -- Recommended, free, high performance

Instructions:

After installing ccl, add a symlink named ccl to your $PATH

Performance note: at the top of milawa.lsp, 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.

SBCL -- free, multiplatform, good performance

Instructions:

After installing, add a symlink named sbcl to your $PATH

Performance note: at the top of milawa.lsp, 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.

Other Options

Other Lisps may or may not still work. The instructions below are probably a good starting point, but I have not tried to use these Lisps to check the proofs since my dissertation.

CMUCL -- free, good performance

Instructions:

After installing, add a symlink named lisp to your $PATH

Performance note: at the top of milawa.lsp, 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.

CLISP -- free, VERY SLOW

Instructions:

After installing, add a symlink named clisp to your $PATH

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:

After installing, add a symlink named acl to your $PATH

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

After installing, add a symlink named scl to your $PATH

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.

Other Lisps?

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.

2. Build the Proof Checker

The original (Common Lisp, not jitawa-Lisp) version of the Milawa kernel is located at:

acl2/books/projects/milawa/milawa.lsp

When you load this into your Lisp, it will create a new executable. The proper way to do this is to go to the acl2/books/projects/milawa directory, then start your lisp and run:

(defconstant image-extension "<name>")
(load "milawa.lsp")

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. (It's perfectly fine to check the proofs with multiple Lisps.)

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

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

./milawa-<lispname> base.<name>

For instance, if you decided to use CCL, and your image-extension is ccl-darwin, then you would run:

./milawa-ccl base.ccl-darwin

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.

3. Check the Proofs.

Estimated time: 1-2 days (see the benchmarks in my dissertation for a better idea.)

Now that everything is set up, you can use the final-checks.sh script to check the proofs.

The usage is:

cd acl2/books/projects/milawa
sh final-checks.sh <lispname> <name>

For instance:

sh final-checks.sh ccl ccl-darwin

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> will be produced. This image will have the highest-level proof checker already loaded and ready to go.