Major Section: IO
Use this function in place of
open-output-channel if you want to open a
channel for output at times this would otherwise be prohibited, for example
make-event expansion and
clause-processor hints. If
this functionality doesn't quite seem like what you need, take a look at the
open-output-channel! in axioms.lisp, specifically the
state global variable
writes-okp. The following
example, taken from
the latter approach.
(defmacro har-zip! (x filename &key sortp) "See :doc hons-archive" `(mv-let (erp val state) (progn! :state-global-bindings ((temp-touchable-vars t set-temp-touchable-vars)) (state-global-let* ((writes-okp t)) (let ((state (har-zip-fn ,x ,filename ,sortp state))) (mv nil nil state)))) (declare (ignore erp val)) state))
The book below illustrates the soundness loophole plugged in ACL2 Version_3.2 related to file writes during book certification.
; The following example is adapted (with only very slight changes) ; from one written by Peter Dillinger. It illustrates the prohibition ; against writing files enforced by with-output-channel during book ; certification (more specifically, during make-event expansion).
; This book certifies in ACL2 Version_3.1 before the fix discussed in the ; paragraph about it being ``possible to write files during book ; certification'' in :DOC NOTE-3-2. The fix was actually made to ACL2 ; function open-output-channel.
; After the fix, in order for certification to succeed one needs to do ; two things. First, in raw lisp: ; (push :after-writes-okp-fix *features*) ; Second, certify with this command: ; (certify-book "writes-okp" 0 nil :ttags (:writes-okp))
(local (defun write-objects-to-channel (obj-lst chan state) (declare (xargs :mode :program :stobjs state :guard (true-listp obj-lst))) (if (consp obj-lst) (pprogn (print-object$ (car obj-lst) chan state) (write-objects-to-channel (cdr obj-lst) chan state) state) state)))
#+after-writes-okp-fix (defttag :writes-okp)
(local (defun write-objects-to-file (obj-lst filename state) (declare (xargs :mode :program :stobjs state :guard (and (stringp filename) (true-listp obj-lst)))) (mv-let (chan state) #-after-writes-okp-fix (open-output-channel filename :object state) #+after-writes-okp-fix (open-output-channel! filename :object state) (if chan (pprogn (write-objects-to-channel obj-lst chan state) (close-output-channel chan state) (value :done)) (er soft 'write-object-to-file "Could not open for writing: ~x0" filename)))))
(local (defconst *nil.lisp* '((in-package "ACL2") (defthm bad nil :rule-classes nil))))
(local (defconst *nil.cert* '((IN-PACKAGE "ACL2") "ACL2 Version 3.1" :BEGIN-PORTCULLIS-CMDS :END-PORTCULLIS-CMDS NIL (("/home/peterd/test/nil.lisp" "nil" "nil" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 134094174)) 62589544 )))
(local (make-event (er-progn (write-objects-to-file *nil.lisp* "nil.lisp" state) (write-objects-to-file *nil.cert* "nil.cert" state) (value '(value-triple :invisible)))))
(local (include-book "nil" :load-compiled-file nil))
(defthm bad nil :rule-classes nil)