sig val run : includes:string list -> files:string list -> session:string -> bool Task.task val prove : ?callback:(Wpo.t -> VCS.prover -> VCS.result -> unit) -> iter:((Wpo.t -> unit) -> unit) -> unit Task.task end