~/temp/acl2-2020-whats-new$ acl2-8.2 Welcome to Clozure Common Lisp Version 1.12-dev (v1.12-dev.5) DarwinX8664! ACL2 Version 8.2 built May 5, 2019 15:14:49. Copyright (C) 2019, 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. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-8-2 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 8.2. Level 1. Cbd "/Users/kaufmann/temp/acl2-2020-whats-new/". System books directory "/Users/kaufmann/acl2/v8-2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(defstub f (x) t) To verify that the two encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2 !>>(LOGIC) The event ( TABLE ACL2-DEFAULTS-TABLE ...) is redundant. See :DOC redundant-events. :INVISIBLE ACL2 !>>(LOCAL (DEFUN F (X) (DECLARE (IGNORABLE X)) T)) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (EQUAL (F X) T). Summary Form: ( DEFUN F ...) Rules: NIL Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) F End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. Summary Form: ( ENCAPSULATE ((F ...) ...) ...) Rules: NIL Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) T ACL2 !>(defun g (x) (cons x (f x))) Since G is non-recursive, its admission is trivial. We observe that the type of G is described by the theorem (CONSP (G X)). We used primitive type reasoning. Summary Form: ( DEFUN G ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G ACL2 !>(thm (equal (car (append (g 3) x)) 3)) Goal' ([ A key checkpoint: Goal' (EQUAL (CAR (APPEND (HIDE (G 3)) X)) 3) *1 (Goal') is pushed for proof by induction. ]) No induction schemes are suggested by *1. Consequently, the proof attempt has failed. Summary Form: ( THM ...) Rules: ((:DEFINITION HIDE)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 57 --- The key checkpoint goal, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoint at the top level: *** Goal' (EQUAL (CAR (APPEND (HIDE (G 3)) X)) 3) ACL2 Error in ( THM ...): See :DOC failure. ******** FAILED ******** ACL2 !>Bye. ~/temp/acl2-2020-whats-new$ acl2-8.3 Welcome to Clozure Common Lisp Version 1.12-dev (v1.12-dev.5) DarwinX8664! ACL2 Version 8.3 built April 14, 2020 19:52:31. 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. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-8-3 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 8.3. Level 1. Cbd "/Users/kaufmann/temp/acl2-2020-whats-new/". System books directory "/Users/kaufmann/acl2/v8-3/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(defstub f (x) t) To verify that the two encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2 !>>(LOGIC) The event ( TABLE ACL2-DEFAULTS-TABLE ...) is redundant. See :DOC redundant-events. :INVISIBLE ACL2 !>>(LOCAL (DEFUN F (X) (DECLARE (IGNORABLE X)) NIL)) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (EQUAL (F X) NIL). Summary Form: ( DEFUN F ...) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) F End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. Summary Form: ( ENCAPSULATE ((F ...) ...) ...) Rules: NIL Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) T ACL2 !>(defun g (x) (cons x (f x))) Since G is non-recursive, its admission is trivial. We observe that the type of G is described by the theorem (CONSP (G X)). We used primitive type reasoning. Summary Form: ( DEFUN G ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G ACL2 !>(thm (equal (car (append (g 3) x)) 3)) Goal' ([ A key checkpoint: Goal' (EQUAL (CAR (APPEND (HIDE (COMMENT "Called constrained function F" (G 3))) X)) 3) *1 (Goal') is pushed for proof by induction. ]) No induction schemes are suggested by *1. Consequently, the proof attempt has failed. Summary Form: ( THM ...) Rules: ((:DEFINITION HIDE)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 57 --- The key checkpoint goal, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoint at the top level: *** Goal' (EQUAL (CAR (APPEND (HIDE (COMMENT "Called constrained function F" (G 3))) X)) 3) ACL2 Error in ( THM ...): See :DOC failure. ******** FAILED ******** ACL2 !>Bye. ~/temp/acl2-2020-whats-new$ acl2x Welcome to Clozure Common Lisp Version 1.12-dev (v1.12-dev.5) DarwinX8664! ACL2 Version 8.3 built May 28, 2020 20:48:58. 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. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + WARNING: This is NOT an ACL2 release; it is a development snapshot. + + (Git commit hash: 3e812f849d8d5dedeedb75db84041fde00ca6437) + + On rare occasions development snapshots may be incomplete, fragile, + + or unable to pass the usual regression tests. + +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-8-3 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 8.3. Level 1. Cbd "/Users/kaufmann/temp/acl2-2020-whats-new/". System books directory "/Users/kaufmann/acl2/temp/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(defstub f (x) t) To verify that the two encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2 !>>(LOGIC) The event ( TABLE ACL2-DEFAULTS-TABLE ...) is redundant. See :DOC redundant-events. :INVISIBLE ACL2 !>>(LOCAL (DEFUN F (X) (DECLARE (IGNORABLE X)) NIL)) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (EQUAL (F X) NIL). Summary Form: ( DEFUN F ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. Summary Form: ( ENCAPSULATE ((F ...) ...) ...) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) T ACL2 !>(defun g (x) (cons x (f x))) Since G is non-recursive, its admission is trivial. We observe that the type of G is described by the theorem (CONSP (G X)). We used primitive type reasoning. Summary Form: ( DEFUN G ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G ACL2 !>(thm (equal (car (append (g 3) x)) 3)) Q.E.D. Summary Form: ( THM ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION G) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 48 Proof succeeded. ACL2 !>Bye. ~/temp/acl2-2020-whats-new$ acl2x Welcome to Clozure Common Lisp Version 1.12-dev (v1.12-dev.5) DarwinX8664! ACL2 Version 8.3 built May 28, 2020 20:48:58. 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. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + WARNING: This is NOT an ACL2 release; it is a development snapshot. + + (Git commit hash: 3e812f849d8d5dedeedb75db84041fde00ca6437) + + On rare occasions development snapshots may be incomplete, fragile, + + or unable to pass the usual regression tests. + +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-8-3 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 8.3. Level 1. Cbd "/Users/kaufmann/temp/acl2-2020-whats-new/". System books directory "/Users/kaufmann/acl2/temp/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(defstobj st1 fld1) Summary Form: ( DEFSTOBJ ST1 ...) Rules: NIL Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) ST1 ACL2 !>(defstobj st2 fld2 :congruent-to st1) Summary Form: ( DEFSTOBJ ST2 ...) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) ST2 ACL2 !>(defun foo (st1 st2) (declare (xargs :stobjs (st1 st2))) (swap-stobjs st1 st2)) Since FOO is non-recursive, its admission is trivial. We observe that the type of FOO is described by the theorem (AND (CONSP (FOO ST1 ST2)) (TRUE-LISTP (FOO ST1 ST2))). We used primitive type reasoning. (FOO ST1 ST2) => (MV ST1 ST2). Computing the guard conjecture for FOO.... The guard conjecture for FOO is trivial to prove. FOO is compliant with Common Lisp. Summary Form: ( DEFUN FOO ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 !>(update-fld1 1 st1) ACL2 !>(update-fld2 2 st2) ACL2 !>(foo st1 st2) ( ) ACL2 !>(fld1 st1) 2 ACL2 !>(fld2 st2) 1 ACL2 !>Bye. ~/temp/acl2-2020-whats-new$