|
|
|---|
|
|
|
|---|
Running ACL2 without building an executable image
The most convenient way to use ACL2 is first to install an executable image; see creating-executable. However, in some cases this is not possible, for example, perhaps if you are using a trial version of a Common Lisp implementation. In that case you should follow the steps below each time you want to start up ACL2.
We assume you have obtained ACL2 and placed it in your current directory. Start up your Common Lisp in that directory, and compile by executing the following forms. This sequence of steps needs to be performed only once.
(load "init.lisp") (in-package "ACL2") (compile-acl2)
Now each time you want to use ACL2, execute the following forms after starting up Common Lisp in that same directory. This may take a minute or two.
(load "init.lisp") (in-package "ACL2") (load-acl2) (initialize-acl2) (lp) ; enter the ACL2 read-eval-print loop
Now see using-ACL2.