How set up ACL2 and ACL2s (with SBCL) on Unix-like Systems?

Cloning Repositories

Make a directory where you want everything to recide (the base directory). Go into it and clone sbcl and acl2 repositories from github:

git clone git@github.com:sbcl/sbcl.git
git clone git@github.com:acl2/acl2.git

Building SBCL

Now we need to actually build SBCL and then install it. Go into the SBCL directory and issue to following commands:

sh make.sh --without-immobile-space --without-immobile-code --without-compact-instance-header --fancy --dynamic-space-size=4Gb
sh install.sh

Building ACL2

Now we do some cleaning and then build ACL2 (do this is the acl2 repo):

make clean-all
make clean-books
make LISP=<path to the ACL2 repo>

Certifying ACL2s books

Use cert.pl to certify all the books in books/acl2s with the following command:

cert.pl *.lisp

(note: make sure you have openssl otherwise quicklisp books may not be certified)

Making an ACL2s executable

Then, start acl2 in a directory in which you want to create the ACL2s executable and issue these commands:

(make-event `(add-include-book-dir :acl2s-modes ,(concatenate 'string (@ system-books-dir) "acl2s/")))
(ld "acl2s-mode.lsp" :dir :acl2s-modes)
(acl2s-defaults :set verbosity-level 1)
(set-inhibit-warnings! "Invariant-risk" "theory")
(reset-prehistory t)
(in-package "ACL2S")
:q
(defun print-ttag-note (val active-book-name include-bookp deferred-p state)
  (declare (xargs :stobjs state)
           (ignore val active-book-name include-bookp deferred-p))
  state)
(defun print-deferred-ttag-notes-summary (state)
  state)
(defun notify-on-defttag (val active-book-name include-bookp state)
    state)
  
(save-exec "acl2s-latest" "ACL2s Mode")

The code above generated an executable: acl2s-latest.

Setup on Emacs

acl2s-latest executable should be opened in a shell buffer within emacs to drive the theorem prover.

You might wanna load the following files in you emacs config for a smoother acl2 experience:

I have the following code in my .emacs.d/init.el file to load these (make sure emacs knows about the directory using (add-to-list 'load-path "<path to folder>"):

;; stop the shell from popping up every time I start emacs
(defvar acl2-skip-shell nil)
(setq acl2-skip-shell t)


;; the main acl2 emacs support
(load "emacs-acl2.el")

;; pete's send-form binding
(load "send-form.lisp")