/usr/share/acl2-7.2dfsg/books/misc/check-state.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 45 46 47 48 49 50 51 52 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann, Feb., 2013
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
; See comment below for check-hons-enabled.
(defmacro check-state (form error-msg &key ctx check-expansion)
`(with-output :stack :push
:off (error summary)
(make-event (if ,form
(value '(value-triple :CHECK-STATE-PASSED))
(with-output
:stack :pop
(er soft ,(or ctx 'check-state)
"~@0"
,error-msg)))
:check-expansion ,check-expansion)))
(defmacro check-hons-enabled (ctx &optional check-expansion)
; Typical usage is at the top of a book that requires ACL2(h) (say, because it
; includes GL and takes too long to certify in ACL2):
; (check-hons-enabled (:book "my-book.lisp"))
; Notice that the string is just the book name. In the error message, ACL2
; will automatically prepend the directory path.
; Use check-expansion = t if you want this check executed at include-book time,
; not just certify-book time, as this uses :check-expansion t for the
; underlying make-event form. Otherwise, you might want to make both your
; include-book and check-hons-enabled forms local, e.g.:
; (local (include-book "misc/check-state" :dir :system))
; (local (check-hons-enabled (:book "my-book.lisp")))
(declare (xargs :guard (booleanp check-expansion)))
`(check-state (hons-enabledp state)
"The current context requires the use of ACL2(h).~%See ~
:DOC hons-and-memoization."
:ctx ,(cond ((and (consp ctx)
(consp (cdr ctx))
(eq (car ctx) :book)
(stringp (cadr ctx)))
`(msg "processing book~%~s0~s1"
(@ connected-book-directory)
,(cadr ctx)))
(ctx)
(t ''check-hons-enabled))
:check-expansion ,check-expansion))
|