Note: the uncompressed proofs take 8 GB of disk space.
Before you can check the proofs, you will need to either
Generate them, following the instructions for a full build, or
Download them, in any of the following formats:
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.
You will need to install a Lisp environment to run the proof checker.
Here are some options:
Instructions:
Instructions:
Instructions:
Instructions:
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.
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.
(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.
(load "milawa.lisp")
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.
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.
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 2.6.24.6+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 2.6.24.6+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.