/usr/share/acl2-7.1/books/tools/time-dollar-with-gc.lisp is in acl2-books-source 7.1-1.
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 | ; This book provides macro time-with-gc$, which times a form and also reports
; information related to garbage collection. Anyone should feel free to add to
; the information that this macro reports.
; Original author: David Rager <ragerdl@cs.utexas.edu>
(in-package "ACL2")
(defttag :profiling)
; example form to certify this book:
; (certify-book "time-dollar-with-gc" 0 t :ttags :all)
(progn!
(set-raw-mode t)
(load (concatenate 'string (cbd) "time-dollar-with-gc-raw.lsp")))
(defmacro-last time$-with-gc1)
(defmacro time$-with-gc (form)
`(return-last 'time$-with-gc1-raw 'doesntseemtomatter ,form))
|