Write a list of ACL2 objects to a file, when ttags are needed to write.
;; Writes the OBJECTS to FILENAME, each on a separate line, overwriting the ;; previous contents of FILENAME. Returns (mv erp state). The ttag is needed ;; because this calls open-output-channel!, but that makes this version usable ;; during make-event expansion, clause-processors, etc. (defund write-objects-to-file! (objects filename ctx state) (declare (xargs :stobjs state :guard (and (true-listp objects) (stringp filename) ;; required by print-object$ (why?): (member (get-serialize-character state) '(nil #\Y #\Z))))) (mv-let (channel state) (open-output-channel! filename :object state) (if (not channel) (prog2$ (er hard? ctx "Unable to open file ~s0 for :object output." filename) (mv t state)) (pprogn (write-objects-to-channel objects channel state) (close-output-channel channel state) (mv nil state)))))