ACL2 Version 8.3 release

GNUmakefile

@@ -1,5 +1,5 @@
-# ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-# Copyright (C) 2019, Regents of the University of Texas
+# ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+# Copyright (C) 2020, Regents of the University of Texas
 
 # This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 # (C) 1997 Computational Logic, Inc.  See the documentation topic NOTES-2-0.

LICENSE

@@ -8,7 +8,7 @@
 When a file in the ACL2 Community Books refers to this LICENSE, that file's
 specified copyright supersedes the copyright shown immediately below.]
 
-Copyright (c) 2019, Regents of the University of Texas
+Copyright (c) 2020, Regents of the University of Texas
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without

acl2-check.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

acl2-fns.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

acl2-init.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.
@@ -928,28 +928,28 @@ implementations.")
 ;       for release instructions.
 
 ; Temporarily, for a release:
-; ""
+""
 
 ; Normally:
 
-  (format
-   nil
-   "
- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
- + WARNING: This is NOT an ACL2 release; it is a development snapshot. +
-~a
- + On rare occasions development snapshots may be incomplete, fragile, +
- + or unable to pass the usual regression tests.                       +
- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-"
-   (acl2-snapshot-info))
+;  (format
+;   nil
+;   "
+; +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+; + WARNING: This is NOT an ACL2 release; it is a development snapshot. +
+;~a
+; + On rare occasions development snapshots may be incomplete, fragile, +
+; + or unable to pass the usual regression tests.                       +
+; +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+;"
+;   (acl2-snapshot-info))
   )
 
 (defvar *saved-string*
   (concatenate
    'string
    "~% ~a built ~a.~
-    ~% Copyright (C) 2019, Regents of the University of Texas"
+    ~% Copyright (C) 2020, Regents of the University of Texas"
    "~% ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you~
     ~% are welcome to redistribute it under certain conditions.  For details,~
     ~% see the LICENSE file distributed with ACL2.~%"

acl2.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.
@@ -1063,7 +1063,7 @@ ACL2 from scratch.")
    (setq acl2::*copy-of-acl2-version*
 ;  Keep this in sync with the value of acl2-version in *initial-global-table*.
          (concatenate 'string
-                      "ACL2 Version 8.2"
+                      "ACL2 Version 8.3"
                       #+non-standard-analysis
                       "(r)"
                       #+(and mcl (not ccl))

akcl-acl2-trace.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

allegro-acl2-trace.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

apply-constraints.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

apply-prim.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

apply-raw.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.
@@ -3140,7 +3140,7 @@
 ;                                  symbol with the original measure
 ;                                  term used in its admission
 
-; *MAX-LEX-LENGTH*                length of the longest LLIST justifying a 
+; *MAX-LEX-LENGTH*                length of the longest LLIST justifying a
 ;                                  user-defined G2 function
 
 ; *BIG-0*                         a list of *MAX-LEX-LENGTH* zeros to fill the

apply.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.
@@ -1022,7 +1022,7 @@
         (cond ((ffnnamep fn (cadr term))
 
 ; We don't even allow fns admitted with :LOOP$-RECURSION T because we don't
-; think the user will ever explicitly type a call of EV$! 
+; think the user will ever explicitly type a call of EV$!
 
                (mv (msg "~x0 cannot be warranted because an :EXPR slot ~
                          in its body is occupied by a quoted term, ~x1, that ~

axioms.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.
@@ -14050,7 +14050,7 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
 ; The reason MCL needs special treatment is that (char-code #\Newline) = 13 in
 ; MCL, not 10.  See also :DOC version.
 
-; ACL2 Version 8.2
+; ACL2 Version 8.3
 
 ; We put the version number on the line above just to remind ourselves to bump
 ; the value of state global 'acl2-version, which gets printed in .cert files.
@@ -14075,7 +14075,7 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
 ; reformatting :DOC comments.
 
                   ,(concatenate 'string
-                                "ACL2 Version 8.2"
+                                "ACL2 Version 8.3"
                                 #+non-standard-analysis
                                 "(r)"
                                 #+(and mcl (not ccl))

basis-a.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

basis-b.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

bdd.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

books/Makefile-generic

@@ -1,5 +1,5 @@
 #; Support for ACL2 Community Books
-#; Copyright (C) 2019, Regents of the University of Texas
+#; Copyright (C) 2020, Regents of the University of Texas
 #; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
 
 #; Written by:  Matt Kaufmann               and J Strother Moore

books/Makefile-psubdirs

@@ -1,5 +1,5 @@
 #; Support for ACL2 Community Books
-#; Copyright (C) 2019, Regents of the University of Texas
+#; Copyright (C) 2020, Regents of the University of Texas
 #; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
 
 #; Written by:  Matt Kaufmann               and J Strother Moore

books/Makefile-subdirs

@@ -1,5 +1,5 @@
 #; Support for ACL2 Community Books
-#; Copyright (C) 2019, Regents of the University of Texas
+#; Copyright (C) 2020, Regents of the University of Texas
 #; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
 
 #; Written by:  Matt Kaufmann               and J Strother Moore

books/build/universal-dependency.certdep

@@ -2,5 +2,4 @@
 ; books.  Suggestion: leave a short note saying why recertification was
 ; required.
 
-Recertification of many books may be required because of new changes to the
-raw Lisp support for defstobj array-resizing functions.
+Version 8.3 release

books/misc/check-acl2-exports.lisp

@@ -200,8 +200,6 @@
 
 ; Symbols below should probably be added to *acl2-exports*.
 
-    SET-SAVED-OUTPUT
-
   ))
 
 (defconst *special-ops*

books/system/doc/acl2-doc-wrap.lisp

@@ -69,7 +69,7 @@
 ; who are looking at an older version of ACL2 will see the corresponding
 ; ACL2+Books Manual at this link.
 
-  "http://www.cs.utexas.edu/users/moore/acl2/v8-2/")
+  "http://www.cs.utexas.edu/users/moore/acl2/v8-3/")
 
 (defconst *installation-url*
 

books/system/doc/acl2-doc.lisp

@@ -2,8 +2,8 @@
 ;
 ; acl2-doc.lisp - Documentation for the ACL2 Theorem Prover
 ;
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 ;
 ; This documentation was derived from the ACL2 system in October 2013, which
 ; was a descendant of ACL2 Version 1.9, Copyright (C) 1997 Computational Logic,
@@ -170,7 +170,7 @@
 ; who are looking at an older version of ACL2 will see the corresponding
 ; ACL2+Books Manual at this link.
 
-  "http://www.cs.utexas.edu/users/moore/acl2/v8-2/")
+  "http://www.cs.utexas.edu/users/moore/acl2/v8-3/")
 
 (defconst *installation-url*
 
@@ -745,7 +745,7 @@
 (defxdoc about-acl2
   :parents (acl2)
   :short "General information About ACL2"
-  :long "<p>This is @(`(:raw (@ acl2-version))`), @(see copyright) (C) 2019,
+  :long "<p>This is @(`(:raw (@ acl2-version))`), @(see copyright) (C) 2020,
  Regents of the University of Texas, authored by Matt Kaufmann and J Strother
  Moore.</p>
 
@@ -17083,7 +17083,7 @@ subtree of X with T, without duplication.</p>
  <p>@(`(:raw (@ acl2-version))`) &mdash; A Computational Logic for Applicative
  Common Lisp</p>
 
- <p>Copyright (C) 2019, Regents of the University of Texas</p>
+ <p>Copyright (C) 2020, Regents of the University of Texas</p>
 
  <p>This version of ACL2 is a descendant of ACL2 Version 1.9, Copyright (C)
  1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.</p>

books/system/doc/render-doc.lisp

@@ -79,8 +79,8 @@
 ; The contents of this file are derived from ACL2 Community Book
 ; books/system/doc/acl2-doc.lisp.
 
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

boot-strap-pass-2-a.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

boot-strap-pass-2-b.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

defpkgs.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.
@@ -539,7 +539,7 @@
         SET-REGISTER-INVARIANT-RISK SET-REWRITE-STACK-LIMIT
         SET-RULER-EXTENDERS
         SET-RW-CACHE-STATE SET-RW-CACHE-STATE!
-        SET-SAVED-OUTPUT SET-SERIALIZE-CHARACTER SET-SERIALIZE-CHARACTER-SYSTEM
+        SET-SERIALIZE-CHARACTER SET-SERIALIZE-CHARACTER-SYSTEM
         SET-SKIP-META-TERMP-CHECKS SET-SKIP-META-TERMP-CHECKS!
         SET-SLOW-ALIST-ACTION SET-SPLITTER-OUTPUT SET-STATE-OK
         SET-TAU-AUTO-MODE

defthm.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.
@@ -11650,7 +11650,7 @@
 
 (defconst *defequiv-package-values* '(:current :equiv :legacy))
 
-(defun defequiv-form (equiv package current-pkg event-name 
+(defun defequiv-form (equiv package current-pkg event-name
                             rule-classes instructions hints otf-flg)
   (declare (xargs :guard
                   (and (symbolp equiv)

defuns.lisp

@@ -1,5 +1,5 @@
-; ACL2 Version 8.2 -- A Computational Logic for Applicative Common Lisp
-; Copyright (C) 2019, Regents of the University of Texas
+; ACL2 Version 8.3 -- A Computational Logic for Applicative Common Lisp
+; Copyright (C) 2020, Regents of the University of Texas
 
 ; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
 ; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.