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
You will need to install a Lisp environment to run the proof checker. Many options may work.
Performance note: at the top of
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 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.
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.
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.
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.
The original (Common Lisp, not jitawa-Lisp) version of the Milawa kernel is located at:
When you load this into your Lisp, it will create a new executable. The
proper way to do this is to go to the
(defconstant image-extension "<name>") (load "milawa.lsp")
This should produce a new file named
At this point, to make sure everything is working you should run
For instance, if you decided to use CCL, and your
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 the benchmarks in my dissertation for a better idea.)
Now that everything is set up, you can use the
The usage is:
cd acl2/books/projects/milawa sh final-checks.sh <lispname> <name>
sh final-checks.sh ccl ccl-darwin
This will result in a lot of output, and I generally
If everything is successful, the file