Proof Pad allows you to build native executable files from the ACL2 code you write.
At the top of your file (but below your book imports), add the line:
This allows you to use the special variable
state in your code.
state is required for many types of input and output in ACL2. Programming with
state is challenging, but necessary if you want to really take advantage of ACL2, especially as a non-interactive executable. You can find more information about
state at the ACL2 documentation.
main function that takes one argument,
state. If you don’t need to use
(declare (ignore state)) to ignore it:
(defun main (state) (declare (ignore state)) (...))
In any case, the body of
main should contain the code you want to run when the executable is run. It should be the entry point to your application.
Click “Tools > Build” or the hammer button on the toolbar to build. If you have not saved the file, you will be prompted to do so; otherwise, you will be prompted to save the executable. Building should take a few seconds for small files, but can take much longer for large projects.