/usr/share/acl2-6.5/books/misc/with-waterfall-parallelism.lisp is in acl2-books-source 6.5-2.
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 | ; Defines a macro that temporarily disables waterfall parallelism and then
; restores it to its previous value. Perhaps the calls of
; set-waterfall-parallelism need not be local, but be careful about removing
; the LOCALs: perhaps that would cause problems for how
; set-waterfall-parallelism changes the memoization status of functions, in the
; case of locally defined functions. Another reason to keep the LOCALs is that
; the user of this macro will be unhappy if it messes with
; waterfall-parallelism settings when including a book.
(in-package "ACL2")
(defun with-waterfall-parallelism-fn (events state)
; (declare (xargs :guard (state-p state) :stobjs state))
(declare (xargs :mode :program :stobjs state))
(let ((curr-waterfall-parallelism-val
(f-get-global 'waterfall-parallelism state)))
`(progn (local (make-event
(er-progn (set-waterfall-parallelism t)
(value '(value-triple nil)))
:check-expansion t))
,@events
(local (make-event
(er-progn (set-waterfall-parallelism
',curr-waterfall-parallelism-val)
(value '(value-triple t)))
:check-expansion t)))))
(defmacro with-waterfall-parallelism (&rest events)
`(make-event (with-waterfall-parallelism-fn ',events state)))
|