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