fact: Definition do_log_reboot (h : do_name) (w : log_files -> option IOStreamWriter.in_channel) : data * list (disk_op log_files) := let d := match channel_to_log w with | Some (es, d) => reboot (apply_log h d es) | None => init_handlers h end in (mk_log_state 0 d, [Delete Log; Write Snapshot (serialize d); Write Count (serialize 0)]).
imports: Verdi(Verdi) Cheerios(Cheerios)