Write-objects-to-file!
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)))))
