/usr/share/acl2-7.2dfsg/books/make-event/stobj-test.lisp is in acl2-books-source 7.2dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; This book tests the interaction of make-event with stobjs. Up through ACL2
; 3.0.1 this book failed to certify, as explained in the "Technical remark"
; below.
(in-package "ACL2")
(defstobj st fld)
(make-event
(let ((st (update-fld 23 st)))
(pprogn (princ$ "EXECUTING FIRST MAKE-EVENT." *standard-co* state)
(newline *standard-co* state)
(mv-let (erp val state)
(defun bar (x) x)
(declare (ignore erp val))
(mv nil '(value-triple 100) state st))))
:check-expansion t)
; Technical remark (for implementors rather than users): The following
; value-triple fails if the make-event expansion just above causes reverting to
; the beginning of the book, as explained in a comment in the call of
; find-longest-common-retraction in the definition set-w! in the ACL2 sources.
(value-triple (or (equal (fld st) 23)
(er hard 'top "OUCH")))
(make-event
(let ((st (update-fld 17 st)))
(pprogn (princ$ "EXECUTING SECOND MAKE-EVENT." *standard-co* state)
(newline *standard-co* state)
(mv-let (erp val state)
(defun bar (x) x)
(declare (ignore erp val))
(mv nil '(value-triple 100) state st)))))
; The following succeeds during certification (well, at least when writing the
; .acl2x file) and is ignored during include-book.
(value-triple (or (not (f-get-global 'write-acl2x state))
(prog2$ (cw "CHECKING LAST VALUE-TRIPLE~%")
(or (equal (fld st) 17)
(er hard 'top "OUCH")))))
|