sig
  type 'a process =
      ?valid:bool ->
      ?failed:bool ->
      ?provers:VCS.prover list ->
      ?depth:int ->
      ?width:int ->
      ?backtrack:int ->
      ?auto:Strategy.heuristic list ->
      ?start:(Wpo.t -> unit) ->
      ?progress:(Wpo.t -> string -> unit) ->
      ?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
      ?success:(Wpo.t -> VCS.prover option -> unit) -> Wpo.t -> 'a
  val prove : unit Task.task ProverScript.process
  val spawn : unit ProverScript.process
  val search :
    ?depth:int ->
    ?width:int ->
    ?backtrack:int ->
    ?auto:Strategy.heuristic list ->
    ?provers:VCS.prover list ->
    ?progress:(Wpo.t -> string -> unit) ->
    ?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
    ?success:(Wpo.t -> VCS.prover option -> unit) ->
    ProofEngine.tree -> ProofEngine.node -> unit
  val get : Wpo.t -> [ `None | `Proof | `Saved | `Script ]
  val save : Wpo.t -> unit
end