other
(declaim (optimize (store-xref-data 0)))
other
(load "acl2.lisp")
other
(let* ((smallp (getenv$-raw "ACL2_SMALL_FIXNUMS")) (smallp (and smallp (not (equal smallp ""))))) (cond ((and (>= most-positive-fixnum (1- (expt 2 60))) (<= most-negative-fixnum (- (expt 2 60))) (not smallp)) nil) ((and (>= most-positive-fixnum (1- (expt 2 29))) (<= most-negative-fixnum (- (expt 2 29)))) (cond (smallp (pushnew :acl2-small-fixnums *features*)) (t (error "ACL2 generally assumes that all integers that are at least -2^60 but less than 2^60 are Lisp fixnums, but that is not the case for this Lisp implementation. You can defeat this check by setting environment variable ACL2_SMALL_FIXNUMS to a non-empty value when building the ACL2 executable. However, such ACL2 builds are not as fully tested as the usual builds and thus may be less reliable, and they are not guaranteed to work compatibly with ordinary ACL2 builds on the same set of books.")))) (t (error "This Lisp implementation is not a suitable host for ACL2: the values of most-negative-fixnum and most-positive-fixnum are ~s and ~s (respectively), but ACL2 assumes that these have absolute values that are respectively at least (1- (expt 2 29)) and (expt 2 29), which are ~s and ~s, respectively." most-positive-fixnum most-negative-fixnum (1- (expt 2 29)) (expt 2 29)))))
other
(proclaim-optimize)
other
(in-package :sb-c)
other
(when (equal (lisp-implementation-version) "1.0.49") (without-package-locks (defun undefine-fun-name (name) (when name (macrolet ((frob (type &optional val) `(unless (eq (info :function ,TYPE name) ,SB-C::VAL) (setf (info :function ,TYPE name) ,SB-C::VAL)))) (frob :info) (frob :type (specifier-type 'function)) (frob :where-from :assumed) (frob :inlinep) (frob :kind) (frob :macro-function) (frob :inline-expansion-designator) (frob :source-transform) (frob :structure-accessor) (frob :assumed-type))) (values))))
other
(in-package "ACL2")
other
(defconstant *current-acl2-world-key* '*current-acl2-world-key*)
other
(when (not (boundp '*print-pprint-dispatch*)) (exit-with-build-error "ERROR: We do not support building ACL2 in~%~ a host ANSI Common Lisp when variable ~s is~%~ unbound. Please obtain a more recent version of your Lisp~%~ implementation." '*print-pprint-dispatch*))
system-callfunction
(defun system-call (string arguments) (let ((ans (process-exit-code (run-program string arguments :output t :search t)))) (if (integerp ans) ans 1)))
read-file-by-linesfunction
(defun read-file-by-lines (file &optional delete-after-reading) (let ((acc nil) (eof '(nil)) missing-newline-p) (with-open-file (s file :direction :input) (loop (multiple-value-bind (line temp) (read-line s nil eof) (cond ((eq line eof) (return acc)) (t (setq missing-newline-p temp) (setq acc (if acc (concatenate 'string acc (string #\ ) line) line))))))) (when delete-after-reading (delete-file file)) (if missing-newline-p acc (concatenate 'string acc (string #\ )))))
system-call+function
(defun system-call+ (string arguments) (let* (exit-code (output-string (our-ignore-errors (with-output-to-string (s) (setq exit-code (let (temp) (if (progn (setq temp (process-exit-code (run-program string arguments :output s :search t))) 1) temp 1))))))) (values (if (integerp exit-code) exit-code 1) (if (stringp output-string) output-string ""))))
our-probe-filefunction
(defun our-probe-file (filename) (probe-file filename))
copy-distributionfunction
(defun copy-distribution (output-file source-directory target-directory &optional (all-files "all-files.txt") (use-existing-target nil)) (cond ((not (and (stringp source-directory) (not (equal source-directory "")))) (error "The source directory specified for COPY-DISTRIBUTION~%~ must be a non-empty string, but~%~s~%is not." source-directory))) (cond ((not (and (stringp target-directory) (not (equal target-directory "")))) (error "The target directory specified for COPY-DISTRIBUTION~%must ~ be a non-empty string, but~%~s~%is not. (If you invoked ~ "make copy-distribution", perhaps you forgot to set DIR.)" target-directory))) (cond ((eql (char source-directory (1- (length source-directory))) #\/) (setq source-directory (subseq source-directory 0 (1- (length source-directory)))))) (cond ((not (equal (our-truename (format nil "~a/" source-directory) :safe) (our-truename "" "Note: Calling OUR-TRUENAME from COPY-DISTRIBUTION."))) (error "We expected to be in the directory~%~s~%~ but instead are apparently in the directory~%~s .~%~ Either issue, in Unix, the command~%~ cd ~a~%~ or else edit the file (presumably, makefile) from~%~ which the function COPY-DISTRIBUTION was called,~%~ in order to give it the correct second argument." source-directory (our-truename "" t) source-directory))) (cond ((and (not use-existing-target) (our-probe-file target-directory)) (error "Aborting copying of the distribution. The target ~%~ distribution directory~%~s~%~ already exists! You may wish to execute the following~%~ Unix command to remove it and all its contents:~%~ rm -r ~a" target-directory target-directory))) (format t "Checking that distribution files are all present.~%") (let (missing-files) (with-open-file (str (concatenate 'string source-directory "/" all-files) :direction :input) (let (filename (dir nil)) (loop (setq filename (read-line str nil)) (cond ((null filename) (return)) ((or (equal filename "") (equal (char filename 0) #\#))) ((find #\ filename) (error "Found a line with a Tab in it: ~s" filename)) ((find #\ filename) (error "Found a line with a Space in it: ~s" filename)) ((find #\* filename) (format t "Skipping wildcard file name, ~s.~%" filename)) ((eql (char filename (1- (length filename))) #\:) (let* ((new-dir (subseq filename 0 (1- (length filename)))) (absolute-dir (format nil "~a/~a" source-directory new-dir))) (cond ((our-probe-file absolute-dir) (setq dir new-dir)) (t (setq missing-files (cons absolute-dir missing-files)) (error "Failed to find directory ~a ." absolute-dir))))) (t (let ((absolute-filename (if dir (format nil "~a/~a/~a" source-directory dir filename) (format nil "~a/~a" source-directory filename)))) (cond ((not (our-probe-file absolute-filename)) (setq missing-files (cons absolute-filename missing-files)) (format t "Failed to find file ~a.~%" absolute-filename))))))))) (cond (missing-files (error "~%Missing the following files (and/or directories):~%~s" missing-files)) (t (format t "Distribution files are all present.~%")))) (format t "Preparing to copy distribution files from~%~a/~%to~%~a/ .~%" source-directory target-directory) (let (all-dirs) (with-open-file (str (concatenate 'string source-directory "/" all-files) :direction :input) (let (filename) (loop (setq filename (read-line str nil)) (cond ((null filename) (return)) ((or (equal filename "") (equal (char filename 0) #\#))) ((find #\ filename) (error "Found a line with a Tab in it: ~s" filename)) ((find #\ filename) (error "Found a line with a Space in it: ~s" filename)) ((eql (char filename (1- (length filename))) #\:) (setq all-dirs (cons (subseq filename 0 (1- (length filename))) all-dirs))))))) (with-open-file (str (concatenate 'string source-directory "/" all-files) :direction :input) (with-open-file (outstr output-file :direction :output) (let (filename (dir nil)) (if (not use-existing-target) (format outstr "mkdir ~a~%~%" target-directory)) (loop (setq filename (read-line str nil)) (cond ((null filename) (return)) ((or (equal filename "") (equal (char filename 0) #\#))) ((eql (char filename (1- (length filename))) #\:) (setq dir (subseq filename 0 (1- (length filename)))) (format outstr "~%mkdir ~a/~a~%" target-directory dir)) ((null dir) (cond ((not (member filename all-dirs :test 'equal)) (format outstr "cp -p ~a/~a ~a~%" source-directory filename target-directory)))) (t (cond ((not (member (format nil "~a/~a" dir filename) all-dirs :test 'equal)) (format outstr "cp -p ~a/~a/~a ~a/~a~%" source-directory dir filename target-directory dir))))))))) (format t "Finished creating a command file for copying distribution files.")))
make-tagsfunction
(defun make-tags nil (when (not (eql (ignore-errors (system-call "which" '("etags"))) 0)) (format t "SKIPPING etags: No such program is in the path.") (return-from make-tags 1)) (system-call "etags" (let* ((fmt-str "~a.lisp") (lst (append '("acl2.lisp" "acl2-check.lisp" "acl2-fns.lisp" "init.lisp" "acl2-init.lisp" "akcl-acl2-trace.lisp" "allegro-acl2-trace.lisp" "openmcl-acl2-trace.lisp") (let ((result nil)) (dolist (x *acl2-files*) (when (not (equal x "doc.lisp")) (setq result (cons (format nil fmt-str x) result)))) (reverse result))))) (append lst (list "multi-threading-raw.lisp" "futures-raw.lisp" "parallel-raw.lisp")))))
other
(defvar *saved-build-date-lst* nil)
git-commit-hashfunction
(defun git-commit-hash (&optional quiet) (multiple-value-bind (exit-code hash) (ignore-errors (system-call+ "git" '("rev-parse" "HEAD"))) (cond ((and (eql exit-code 0) (stringp hash)) (coerce (remove #\ (coerce hash 'list)) 'string)) (quiet nil) (t (exit-with-build-error "Unable to determine git commit hash.")))))
other
(defvar *acl2-release-p* nil)
acl2-snapshot-infofunction
(defun acl2-snapshot-info nil (let* ((var "ACL2_SNAPSHOT_INFO") (s (getenv$-raw var)) (err-string "Unable to determine git commit hash for use in the startup~%~ banner. Consider setting environment variable ACL2_SNAPSHOT_INFO~%~ to a message to use in its place, or set it to NONE if you simply~%~ want to avoid this error.")) (cond ((and s (string-equal s "NONE")) (format nil "~% +~72t+")) ((and s (not (equal s ""))) (format nil "~% + (Note from the environment when this executable was ~ saved:~72t+~% + ~a)~72t+" s)) (*acl2-release-p* "") (t (let ((h (git-commit-hash t))) (cond (h (format nil "~% + (Git commit hash: ~a)~72t+" h)) (t (exit-with-build-error err-string var))))))))
other
(defvar *saved-string* (concatenate 'string "~% ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++" "~% + ~a~72t+" "~% + built ~a.~72t+" (acl2-snapshot-info) "~% + Copyright (C) 2026, Regents of the University of Texas.~72t+" "~% + ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and~72t+" "~% + you are welcome to redistribute it under certain conditions. For~72t+" "~% + details, see the LICENSE file distributed with ACL2.~72t+" "~% ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++~%"))
maybe-load-acl2-initfunction
(defun maybe-load-acl2-init nil (let* ((home (our-user-homedir-pathname)) (fl (and home (probe-file (merge-pathnames home "acl2-init.lsp"))))) (when fl (format t "; Loading file ~s...~%" fl) (load fl) (format t "; Finished loading file ~s.~%" fl))))
chmod-executablefunction
(defun chmod-executable (sysout-name) (system-call "chmod" (list "+x" sysout-name)))
saved-build-datesfunction
(defun saved-build-dates (separator) (let* ((date-lst (reverse *saved-build-date-lst*)) (result (car date-lst)) (sep (concatenate 'string (string #\ ) (if (eq separator :terminal) (concatenate 'string (make-string (+ 3 (length *copy-of-acl2-version*)) :initial-element #\ ) "then ") separator)))) (dolist (s (cdr date-lst)) (setq result (concatenate 'string result sep s))) result))
our-with-standard-io-syntaxmacro
(defmacro our-with-standard-io-syntax (&rest args) `(with-standard-io-syntax (let ((*print-readably* nil)) ,@ARGS)))
user-args-stringfunction
(defun user-args-string (inert-args &optional (separator '"--")) (cond ((null inert-args) ""$@"") ((eq inert-args t) (concatenate 'string separator " "$@"")) (t (concatenate 'string separator " " inert-args " "$@""))))
write-exec-filemacro
(defmacro write-exec-file (stream prefix string &rest args) `(our-with-standard-io-syntax (format ,STREAM "#!/bin/sh~%~%") (format ,STREAM "# Saved ~a~%~%" (saved-build-dates "# then ")) ,@(AND PREFIX `((FORMAT ,STREAM ,(CAR PREFIX) ,@(CDR PREFIX)))) (format ,STREAM (concatenate 'string "exec " ,STRING) ,@ARGS)))
proclaim-filesfunction
(defun proclaim-files (outfilename) (unless (and *do-proclaims* (not (eq *do-proclaims* :gcl))) (return-from proclaim-files nil)) (when (probe-file outfilename) (delete-file outfilename)) (format t "Writing proclaim forms for ACL2 source files to file ~s.~%" outfilename) (let (str) (or (setq str (safe-open outfilename :direction :output)) (error "Unable to open file ~s for output." outfilename)) (dolist (fl *acl2-files*) (when (not (equal fl "doc.lisp")) (proclaim-file (format nil "~a.lisp" fl) str))) (close str)))
insert-stringfunction
(defun insert-string (s) (cond ((null s) "") (t (concatenate 'string " " s))))
other
(defconstant *thisscriptdir-def*
"absdir=`perl -e 'use Cwd "abs_path";print abs_path(shift)' $0`
THISSCRIPTDIR="$( cd "$( dirname "$absdir" )" && pwd -P )"
")
use-thisscriptdir-pfunction
(defun use-thisscriptdir-p (sysout-name core-name) (and (equal sysout-name core-name) (not (position (symbol-value '*directory-separator*) core-name))))
other
(defvar *acl2-default-restart-complete* nil)
fix-default-pathname-defaultsfunction
(defun fix-default-pathname-defaults nil nil)
other
(defvar *print-startup-banner* t)
other
(defvar *lp-ever-entered-p* nil)
acl2-version+function
(defun acl2-version+ nil (format nil "~a~a" *copy-of-acl2-version* (cond (*acl2-release-p* "") (t (format nil "+ (a development snapshot based on ~a)" *copy-of-acl2-version*)))))
acl2-default-restartfunction
(defun acl2-default-restart (&optional called-by-lp) (if *acl2-default-restart-complete* (return-from acl2-default-restart nil)) (let ((produced-by-save-exec-p *lp-ever-entered-p*)) (proclaim-optimize) (setq *lp-ever-entered-p* nil) (acl2-set-character-encoding) (fix-default-pathname-defaults) (when (not produced-by-save-exec-p) (qfuncall acl2h-init)) (when *print-startup-banner* (format t *saved-string* (acl2-version+) (saved-build-dates :terminal))) (maybe-load-acl2-init) (eval `(in-package ,*STARTUP-PACKAGE-NAME*)) (setq *acl2-default-restart-complete* t) (when (not called-by-lp)) nil))
sbcl-restartfunction
(defun sbcl-restart nil (acl2-default-restart) (eval '(lp)))
other
(defvar *sbcl-dynamic-space-size* 32000)
other
(defvar *sbcl-home-dir* (let* ((sbcl-home-env (getenv$-raw "SBCL_HOME")) (sbcl-home-env (and sbcl-home-env (probe-file sbcl-home-env))) (core-dir (and (boundp '*core-pathname*) (pathname-directory *core-pathname*))) (in-place (and core-dir (equal (car (last core-dir)) "output"))) (installed (and core-dir (not in-place))) (sbcl-home-installed (and installed (make-pathname :directory core-dir))) (sbcl-home-in-place-old (and in-place (make-pathname :directory (append (butlast core-dir 1) '("contrib"))))) (sbcl-home-in-place-new (and in-place (make-pathname :directory (append (butlast core-dir 1) '("obj" "sbcl-home"))))) (sbcl-home-detected (or (and sbcl-home-installed (probe-file sbcl-home-installed)) (and sbcl-home-in-place-new (probe-file sbcl-home-in-place-new)) (and sbcl-home-in-place-old (probe-file sbcl-home-in-place-old))))) (cond ((and sbcl-home-env (not (and in-place core-dir (equal sbcl-home-env (probe-file (make-pathname :directory core-dir)))))) (when (and sbcl-home-detected (not (equal sbcl-home-env sbcl-home-detected))) (warn "SBCL_HOME is currently set to "~a", but our heuristics ~ indicate that it should be set to "~a". The ACL2 image we ~ save may not work correctly.~%" sbcl-home-env sbcl-home-detected)) (namestring sbcl-home-env)) (sbcl-home-detected (namestring sbcl-home-detected)) (t (exit-with-build-error "Could not determine a suitable value for the environment variable ~ SBCL_HOME.~%If it is set, please try unsetting it or correcting ~ it.~%If it is not set, please try setting it to an appropriate ~ value.")))))
save-acl2-in-sbcl-auxfunction
(defun save-acl2-in-sbcl-aux (sysout-name core-name host-lisp-args toplevel-args inert-args) (declare (optimize (inhibit-warnings 3))) (let* ((use-thisscriptdir-p (use-thisscriptdir-p sysout-name core-name)) (eventual-sysout-core (unix-full-pathname core-name "core")) (sysout-core (unix-full-pathname sysout-name "core"))) (if (probe-file sysout-name) (delete-file sysout-name)) (if (probe-file eventual-sysout-core) (delete-file eventual-sysout-core)) (when use-thisscriptdir-p (setq eventual-sysout-core (concatenate 'string "$THISSCRIPTDIR/" core-name ".core"))) (with-open-file (str sysout-name :direction :output) (let ((prog (or (our-truename *runtime-pathname* t) (car *posix-argv*)))) (write-exec-file str ("~a~a~%" (if use-thisscriptdir-p *thisscriptdir-def* "") (format nil "export SBCL_HOME='~a'" *sbcl-home-dir*)) "~s --tls-limit 16384 --dynamic-space-size ~s --control-stack-size ~ 64 --disable-ldb --core ~s~a ${SBCL_USER_ARGS} ~ --end-runtime-options --no-userinit --eval '(acl2::sbcl-restart)'~a ~a~%" prog *sbcl-dynamic-space-size* eventual-sysout-core (insert-string host-lisp-args) (insert-string toplevel-args) (user-args-string inert-args "--end-toplevel-options")))) (chmod-executable sysout-name) (gc) (save-lisp-and-die sysout-core :purify t)))
save-acl2-in-sbclfunction
(defun save-acl2-in-sbcl (sysout-name &optional mode core-name) (declare (ignore mode)) (with-warnings-suppressed (if (probe-file "worklispext") (delete-file "worklispext")) (with-open-file (str "worklispext" :direction :output) (format str "core")) (save-acl2-in-sbcl-aux sysout-name core-name nil nil nil)))
save-exec-rawfunction
(defun save-exec-raw (sysout-name host-lisp-args toplevel-args inert-args) (with-warnings-suppressed (setq *acl2-default-restart-complete* nil) (save-acl2-in-sbcl-aux sysout-name sysout-name host-lisp-args toplevel-args inert-args)))
rc-filenamefunction
(defun rc-filename (dir) (concatenate 'string dir ".acl2rc"))
write-acl2rcfunction
(defun write-acl2rc (dir) (let ((rc-filename (concatenate 'string dir ".acl2rc"))) (if (not (probe-file rc-filename)) (with-open-file (str (rc-filename dir) :direction :output) (format str "; enter ACL2 read-eval-print loop~%~ (ACL2::ACL2-DEFAULT-RESTART)~%~ #+ALLEGRO (EXCL::PRINT-STARTUP-INFO T)~%~ #+ALLEGRO (SETQ EXCL::*PRINT-STARTUP-MESSAGE* NIL)~%~ (ACL2::LP)~%")))))
save-acl2function
(defun save-acl2 (&optional mode other-info do-not-save-gcl) (declare (ignore do-not-save-gcl)) (load-acl2 :load-acl2-proclaims *do-proclaims*) (eval mode) (princ " ****************************************************************************** Initialization complete, beginning the check and save. ****************************************************************************** ") (cond ((or (not (probe-file *acl2-status-file*)) (with-open-file (str *acl2-status-file* :direction :input) (not (eq (read str nil) :initialized)))) (exit-with-build-error "Initialization has failed. Try INITIALIZE-ACL2 again."))) (save-acl2-in-sbcl "nsaved_acl2" mode other-info) (format t "Saving of ACL2 is complete.~%"))
generate-acl2-proclaimsfunction
(defun generate-acl2-proclaims nil (let ((filename "acl2-proclaims.lisp")) (when (probe-file filename) (delete-file filename)) (cond ((eq *do-proclaims* :gcl) (cond ((probe-file "sys-proclaim.lisp") (rename-file "sys-proclaim.lisp" filename)) (t (exit-with-build-error "File sys-proclaim.lisp does not exist!")))) (*do-proclaims* (format t "Beginning load-acl2 and initialize-acl2 on behalf of ~ generate-acl2-proclaims.~%") (load-acl2 :fast t) (qfuncall initialize-acl2 'include-book nil nil 'generating) (proclaim-files filename)) (t (when (probe-file filename) (delete-file filename)) (with-open-file (str filename :direction :output) (format str "(in-package "ACL2")~%~%") (format str "; No proclaims are generated here for this host Lisp.~%"))))) nil)