NOTE: These instructions are for the old kernel. For the new, verified kernel for Jitawa (and Common Lisp), see the Milawa on Jitawa page.
Before you can check the proofs, you will need to generate them by following the instructions for a full build. (I used to post archives of the proofs for download, but this takes a lot of space and doesn't really seem worth continuing, as the proofs are updated.)
After the proofs are generated, you should have a directory structure like this:
and so on.
You will need to install a Lisp environment to run the proof checker.
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.
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.
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.
(defconstant image-extension "name")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
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.
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:
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.
Note: These figures are outdated, they were collected at the time of my dissertation, modern machines and Lisps may have significantly better performance -- well, one hopes, at least. :)
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.
System information: Dell Precision 390 Workstation running 32-bit Linux 18.104.22.168+desktop7+24.57 #1 SMP, Intel Core 2 6400 @ 2.13 GHz, 2 MB L2 cache, 4 GB memory.
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.
System information: HP Proliant DL585 server running 64-bit Linux 22.214.171.124+desktop7+24.57 #1 SMP, AMD Opteron Processor 850 @ 2.2 GHz, 1 MB cache, 32 GB memory.
System Information: Macbook laptop running Darwin 9.7.0, Intel Core 2 Duo Processor @ 2.4 Ghz, 4 GB memory.