Internet connection unnecessary to build books - acl2/acl2 GitHub Wiki

Here's what Matt Kaufmann did on October 30, 2017 to verify that an internet connection is unnecessary to build the books.

My laptop run was successful, confirming that the ACL2 7.4 tarball suffices for building the manual and in fact for doing a successful "everything" regression, without an internet connection. Note that I do have glucose installed; not sure if that was necessary. (There's a current issue about whether it's necessary now.)

For the record, here's what I did.

First, I fetched acl2-7.4.tar.gz from http://www.cs.utexas.edu/users/moore/acl2/v7-4/HTML/installation/installation.html and then moved it to a fresh directory.

Then, after turning off my internet connection -- note that glucose was installed:

tar xfz acl2-7.4.tar.gz cd acl2-7.4 (time nice make LISP=ccl) >& make.log (time nice make -j 8 regression-everything ACL2=pwd/saved_acl2 USE_QUICKLISP=1) >& make-regression-everything-ccl-quicklisp-j-8.log&

Checked that there were no errors:

fgrep -a '**' make-regression-everything-ccl-quicklisp-j-8.log

Opened the manual and navigated it a bit:

open books/doc/manual/index.html