		Search-engine friendly clone of the ACL2 documentation.

Open-output-channel!

When trust tags are needed to open output channels

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 during make-event expansion and clause-processor hints. If this functionality doesn't quite seem like what you need, take a look at the definition of open-output-channel! in axioms.lisp, specifically the binding of state global variable writes-okp. The following example, taken from (no longer available) community book books/hons-archive/hons-archive.lisp, illustrates 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))

(in-package "ACL2")

(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)