Write-bytes-to-file!
Write bytes to a file when not allowed without a trust tag.
;; Writes the BYTES to file FILENAME, overwriting its previous contents.
;; 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.
(defun write-bytes-to-file! (bytes filename ctx state)
(declare (xargs :stobjs state
:guard (and (all-bytep bytes)
(stringp filename))))
(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)
(mv nil state)))))
