|
|
|---|
|
|
|
|---|
Citation conventions for doc operational-semantics
In the documentation topic operational-semantics and its
supporting subtopics, references to published books and papers appear as
ordinary documentation topics, except all the labels are in the "BIB"
package, e.g., bib::mccarthy62 or bib::kmm00a. When finding
them with the
In operational-semantics and its supporting subtopics we also make
frequent reference to Nqthm and ACL2 directories and proof scripts, such as
By the way, the active development of Nqthm ended in 1992, three years after ACL2 development began. For about 10 years Nqthm and ACL2 were both in use. Since then Nqthm has been maintained by Boyer and most of its proof scripts are not only still available but can still be processed.
Documentation for Nqthm may be found in bib::bm97.
The Nqthm source code and proof scripts are available in two places,
ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-1992/
and
https://drive.google.com/drive/folders/18z-uwg8E_3NxIijLoxYE-_NS-klqYI7R
While it is possible to download individual files from these sites, we
recommend that you download the entire
ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-2nd-edition.tar.gz
to a directory where you want the Nqthm source code and regression suite, connect to that directory, and extract the files as follows.
tar xfz nqthm-2nd-edition.tar.gz
That will create the directory
You do not have to build the Nqthm image or do a regression if all you
want to do is inspect either the Nqthm source code (which consists of the
files
The ACL2 system, as it stood in 2000, is documented in two textbooks; see pubs::pubs-books. These books are a good place for a beginner to start, even though some of the material is out-of-date. Up-to-date user-level documentation of ACL2 is available online as described in the User's Manuals link on the homepage (below), and a wealth of information is available there. Some of it is organized for the experienced user trying to get information about a particular feature, but there is a documentation topic, start-here, that provides many starting points for the beginning ACL2 user.
Source code, input files, installation instructions, extensive online documentation and other material is available from the ACL2 homepage:
https://www.cs.utexas.edu/~moore/acl2/
That page provides instructions for obtaining the latest ACL2 numbered release. However, many ACL2 users obtain an up-to-date snapshot of ACL2 from GitHub:
https://github.com/acl2/acl2
As with Nqthm, to explore ACL2 source files or prover input files we
recommend that you see installation and follow the instructions there.
That includes placing a copy of the latest sources and input scripts (but not
prover output) in a directory on your computer. The filenames suffixed with