/usr/share/acl2-7.2dfsg/books/make-event/defconst-fast.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 | ; 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 macro, defconst-fast, is based on a conversation with Warren Hunt. A
; defconst in a book has the unfortunate property that its form is evaluated
; not only when that book is certified, but also (again) when that book is
; included. Defconst-fast is more efficient because it generates a defconst
; that uses the result of the evaluation. Moreover, defconst does its
; evaluation in a "safe mode" that avoids soundness issues but can cause a
; slowdown of (we have seen) 4X.
; See also defconst-fast-examples.lisp.
; For a more general utility, see ../tools/defconsts.lisp.
(in-package "ACL2")
(defmacro defconst-fast (name form &optional (doc '"" doc-p))
`(make-event
(let ((val ,form))
(list* 'defconst ',name (list 'quote val)
,(and doc-p (list 'list doc))))))
|