~/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$