Write bytes to a file.
;; Writes the BYTES to file FILENAME, overwriting its previous contents. ;; Returns (mv erp state). (defund write-bytes-to-file (bytes filename ctx state) (declare (xargs :guard (and (all-bytep bytes) (stringp filename)) :stobjs state)) (mv-let (channel state) (open-output-channel filename :byte state) (if (not channel) (prog2$ (er hard? ctx "Unable to open file ~s0 for :byte output." filename) (mv t state)) (pprogn (write-bytes-to-channel bytes channel state) (close-output-channel channel state) ;; no error: (mv nil state)))))