sig   val prove :     Wpo.t ->     ?mode:VCS.mode ->     ?start:(Wpo.t -> unit) ->     ?callin:(Wpo.t -> VCS.prover -> unit) ->     ?callback:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->     VCS.prover -> bool Task.task   val spawn :     Wpo.t ->     ?start:(Wpo.t -> unit) ->     ?callin:(Wpo.t -> VCS.prover -> unit) ->     ?callback:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->     ?success:(Wpo.t -> VCS.prover option -> unit) ->     (VCS.mode * VCS.prover) list -> unit end