Write-objects-to-file
Write a list of ACL2 objects to a file.
;; Writes the OBJECTS to FILENAME, each on a separate line, overwriting the
;; previous contents of FILENAME. Returns (mv erp state).
(defund write-objects-to-file (objects filename ctx state)
(declare (xargs :guard (and (true-listp objects)
(stringp filename)
;; required by print-object$ (why?):
(member (get-serialize-character state)
'(nil #\Y #\Z)))
:stobjs state))
(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)
;; no error:
(mv nil state)))))
