This will take awhile and you will probably need to install lots of software. Please email firstname.lastname@example.org if you have any problems.
You will need a reasonable Unix environment (bash, make, perl, ...), and also some less common software:
Required: Clozure Common Lisp
Required: ACL2 with Hons
The latest version of the sources may be obtained via Subversion.
You can get either:
svn checkout svn://uvanimor-3.cs.utexas.edu:34567/Milawa/trunk/Sources <target>
svn checkout svn://uvanimor-3.cs.utexas.edu:34567/Milawa/trunk <target>
(Alternate option: Replace trunk with tags/dissertation for the version as of my dissertation, which diverges in some ways and has different requirements; see the archive version if you want to do this.)
Estimated time: a couple of hours.
If you have some kind of cluster, look at Sources/ACL2/Makefile and see if you can write a startjob command that will work.
This takes a LOT of CPU time.
Successful bootstrapping leaves you with:
Milawa/Sources/ACL2/bootstrap/utilities/symmetryYou can use these programs to carry out your own proofs in Milawa. The symmetry executable in the user directory has our highest-level proof checker already verified and loaded.
Please see the separate instructions for building a core proof checker using your choice of lisps, and using it to check the proofs.