		Search-engine friendly clone of the ACL2 documentation.

Installation-support

Creating-executable

Creating or obtaining an executable image

This topic may be avoided by reading the installation summary, which is intended to be self-contained.

After obtaining the ACL2 sources, the next step is to produce an executable image. Proceed according to one of the four sections below, and after reading that section, continue by reading the topic, see using-ACL2.

Pre-built images
Building an executable image on a Unix-like system
Building an executable image on other than a Unix-like system
Observations on building an executable image on a Windows system

Pre-built images

This website contains links to ACL2 executables and packages. Each -md5sum file was created using md5sum. We may add additional links from time to time.

Building an executable image on a Unix-like system

We assume you have obtained ACL2, described in obtaining-ACL2, but you have not obtained a pre-built image. Change to the directory containing the ACL2 sources and execute the command

make LISP=<your_lisp>

where <your_lisp> is the command to run your local Common Lisp. By default, if no LISP=<your_lisp> is specified, then LISP=ccl is used, which presumably invokes CCL (see installation-requirements).

This will create executable saved_acl2 in the current directory.

The time taken to carry out this process depends on the host Lisp and the host processor but may well be under a minute. The size of the resulting binary image is dependent on which Lisp was used, but it may be on the order of a couple hundred megabytes or so.

This make command works for the supported host Common Lisp implementations; see installation-requirements, on systems we have tested. If this make command does not work for you, see the instructions below for “Building an executable image on other than a Unix-like system”.

Building an executable image on other than a Unix-like system

It may be best to use this option only if you are using a Common Lisp on which you cannot save an image (e.g., a trial version of a commercial lisp).

Next we describe how to create a binary image containing ACL2 without using the `make' utility. If you cannot save an image, perhaps because you are using a trial version of your Common Lisp, then you may not be able to save an image. In that case, see running-ACL2-without-executable.

Your Common Lisp should be one of those listed in installation-requirements. Stand in the directory where you have downloaded ACL2.

Remove file nsaved_acl2 if it exists.
Start up Common Lisp and submit the following sequence of commands.
```
(load "init.lisp")
(in-package "ACL2")
(compile-acl2) ; essentially a no-op if the Lisp is CCL or SBCL
```
The commands above may, depending on the host Lisp, compile the ACL2 sources and create compiled object files in the current directory. (But they should be run even for Lisps that do not compile the ACL2 sources.) Below, we assume that saved images have extension .core; but this will depend on your host Lisp and operating system.
Now exit your Common Lisp. Make sure you are in the directory where you ran the commands displayed above. Start your Common Lisp and run the following commands to initialize ACL2.
```
(load "init.lisp")
(in-package "ACL2")
(save-acl2 (quote (initialize-acl2)) "saved_acl2")
```
This will load ACL2 source files (possibly compiled) into Lisp and then bootstrap ACL2 by reading and processing the source files, concluding by saving an image. Exit Lisp now. Subsequent steps will put the image in the right place.
Remove osaved_acl2 if it exists.
IF saved_acl2 and saved_acl2.core both exist THEN:
- move saved_acl2.core to osaved_acl2.core
- move saved_acl2 to osaved_acl2 and edit osaved_acl2, changing saved_acl2.core (at end of line) to osaved_acl2.core
ELSE IF saved_acl2 exists THEN:
- move saved_acl2 to osaved_acl2
Move nsaved_acl2 to saved_acl2 .
Move nsaved_acl2.core to saved_acl2.core .
Make sure saved_acl2 is executable. For Windows this involves two mini-steps:
- Remove the "$@" from the saved_acl2 script (because Windows may not understand "$@"). Consequently, any arguments you pass to ACL2 via the command line will be ignored.
- Rename saved_acl2 to saved_acl2.bat, for example by executing the following command.
```
rename saved_acl2 saved_acl2.bat
```

Observations on building an executable image on a Windows system

You may be able to avoid this section by downloading a pre-built binary distribution; see pre-built-binary-distributions, and also see “Pre-built images” above.

Otherwise, see windows-installation for information on installing ACL2 on Windows systems.