let singleton f =
let instance = lazy (f ()) in
fun () -> Lazy.force instance
-(*
-let mkdir d =
- let errmsg = sprintf "Unable to create directory \"%s\"" d in
- try
- let dir = "mkdir -p " ^ d in
- (match Unix.system dir with
- | Unix.WEXITED 0 -> ()
- | Unix.WEXITED n ->
- MatitaLog.error ("'mkdir -p " ^ dir ^ "' failed with "^string_of_int n);
- failwith errmsg
- | Unix.WSIGNALED s
- | Unix.WSTOPPED s ->
- MatitaLog.error
- ("'mkdir -p " ^ dir ^ "' signaled with " ^ string_of_int s);
- failwith errmsg)
- with Unix.Unix_error _ as exc ->
- MatitaLog.error
- ("Unix error in makigin dir " ^ (MatitaExcPp.to_string exc));
- failwith errmsg
-*)
+
let get_proof_status status =
match status.proof_status with
| Incomplete_proof s -> s