sig
  type proof_attempt_status =
      Undone
    | Scheduled
    | Running
    | Done of Call_provers.prover_result
    | Interrupted
    | Detached
    | InternalFailure of exn
    | Uninstalled of Whyconf.prover
    | UpgradeProver of Whyconf.prover
    | Removed of Whyconf.prover
  val print_status :
    Stdlib.Format.formatter -> Controller_itp.proof_attempt_status -> unit
  type transformation_status =
      TSscheduled
    | TSdone of Session_itp.transID
    | TSfailed of (Session_itp.proofNodeID * exn)
    | TSfatal of (Session_itp.proofNodeID * exn)
  val print_trans_status :
    Stdlib.Format.formatter -> Controller_itp.transformation_status -> unit
  type strategy_status =
      STSgoto of Session_itp.proofNodeID * int
    | STShalt
    | STSfatal of string * Session_itp.proofNodeID * exn
  val print_strategy_status :
    Stdlib.Format.formatter -> Controller_itp.strategy_status -> unit
  val default_delay_ms : int
  module type Scheduler =
    sig
      val blocking : bool
      val multiplier : int
      val timeout : ms:int -> (unit -> bool) -> unit
      val idle : prio:int -> (unit -> bool) -> unit
    end
  type controller = private {
    mutable controller_session : Session_itp.session;
    mutable controller_config : Whyconf.config;
    mutable controller_env : Env.env;
    controller_provers :
      (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
    controller_strategies :
      (string * string * string * Strategy.instruction array) Wstdlib.Hstr.t;
    controller_running_proof_attempts : unit Session_itp.Hpan.t;
  }
  val create_controller :
    Whyconf.config ->
    Env.env -> Session_itp.session -> Controller_itp.controller
  val set_session_max_tasks : int -> unit
  val set_session_memlimit : Controller_itp.controller -> int -> unit
  val set_session_timelimit : Controller_itp.controller -> float -> unit
  val set_session_prover_upgrade_policy :
    Controller_itp.controller ->
    Whyconf.prover -> Whyconf.prover_upgrade_policy -> unit
  val print_session :
    Stdlib.Format.formatter -> Controller_itp.controller -> unit
  exception Errors_list of exn list
  val reload_files :
    ?hard_reload:bool ->
    ?reparse_file_fun:(Session_itp.session ->
                       Env.env -> Session_itp.file -> Theory.theory list) ->
    ignore_shapes:bool -> Controller_itp.controller -> bool * bool
  val add_file :
    Controller_itp.controller -> ?format:Env.fformat -> string -> unit
  val remove_subtree :
    notification:Session_itp.notifier ->
    removed:Session_itp.notifier ->
    Controller_itp.controller -> Session_itp.any -> unit
  val get_undetached_children_no_pa :
    Session_itp.session -> Session_itp.any -> Session_itp.any list
  val set_partial_config :
    Controller_itp.controller -> Whyconf.config -> unit
  module Make :
    Scheduler ->
      sig
        val register_observer : (int -> int -> int -> unit) -> unit
        val interrupt : Controller_itp.controller -> unit
        val interrupt_proof_attempts_for_goal :
          Controller_itp.controller -> Session_itp.proofNodeID -> unit
        val schedule_proof_attempt :
          ?proof_script_filename:string ->
          Controller_itp.controller ->
          Session_itp.proofNodeID ->
          Whyconf.prover ->
          limits:Call_provers.resource_limits ->
          callback:(Session_itp.proofAttemptID ->
                    Controller_itp.proof_attempt_status -> unit) ->
          notification:Session_itp.notifier -> unit
        val schedule_edition :
          Controller_itp.controller ->
          Session_itp.proofNodeID ->
          Whyconf.prover ->
          callback:(Session_itp.proofAttemptID ->
                    Controller_itp.proof_attempt_status -> unit) ->
          notification:Session_itp.notifier -> unit
        val prepare_edition :
          Controller_itp.controller ->
          ?file:Sysutil.file_path ->
          Session_itp.proofNodeID ->
          Whyconf.prover ->
          notification:Session_itp.notifier ->
          Session_itp.proofAttemptID * string *
          Call_provers.prover_result option
        exception GoalNodeDetached of Session_itp.proofNodeID
        val schedule_transformation :
          Controller_itp.controller ->
          Session_itp.proofNodeID ->
          string ->
          string list ->
          callback:(Controller_itp.transformation_status -> unit) ->
          notification:Session_itp.notifier -> unit
        val run_strategy_on_goal :
          Controller_itp.controller ->
          Session_itp.proofNodeID ->
          Strategy.t ->
          callback_pa:(Session_itp.proofAttemptID ->
                       Controller_itp.proof_attempt_status -> unit) ->
          callback_tr:(string ->
                       string list ->
                       Controller_itp.transformation_status -> unit) ->
          callback:(Controller_itp.strategy_status -> unit) ->
          notification:Session_itp.notifier ->
          removed:Session_itp.notifier -> unit
        val run_strat_on_goal :
          Controller_itp.controller ->
          Session_itp.proofNodeID ->
          string ->
          Strategy.gen_strat ->
          string list ->
          callback_pa:(Session_itp.proofAttemptID ->
                       Controller_itp.proof_attempt_status -> unit) ->
          callback_tr:(string ->
                       string list ->
                       Controller_itp.transformation_status -> unit) ->
          callback:(Controller_itp.strategy_status -> unit) ->
          notification:Session_itp.notifier -> unit
        val clean :
          Controller_itp.controller ->
          removed:Session_itp.notifier -> Session_itp.any option -> unit
        val reset_proofs :
          Controller_itp.controller ->
          removed:Session_itp.notifier ->
          notification:Session_itp.notifier -> Session_itp.any option -> unit
        val mark_as_obsolete :
          notification:Session_itp.notifier ->
          Controller_itp.controller -> Session_itp.any option -> unit
        exception BadCopyPaste
        val copy_paste :
          notification:Session_itp.notifier ->
          callback_pa:(Session_itp.proofAttemptID ->
                       Controller_itp.proof_attempt_status -> unit) ->
          callback_tr:(string ->
                       string list ->
                       Controller_itp.transformation_status -> unit) ->
          Controller_itp.controller ->
          Session_itp.any -> Session_itp.any -> unit
        type report =
            Result of Call_provers.prover_result * Call_provers.prover_result
          | CallFailed of exn
          | Replay_interrupted
          | Prover_not_installed
          | Edited_file_absent of string
          | No_former_result of Call_provers.prover_result
        val replay_print :
          Stdlib.Format.formatter ->
          (Session_itp.proofNodeID * Whyconf.prover *
           Call_provers.resource_limits * Controller_itp.Make.report)
          list -> unit
        val replay :
          valid_only:bool ->
          obsolete_only:bool ->
          ?use_steps:bool ->
          ?filter:(Session_itp.proof_attempt_node -> bool) ->
          Controller_itp.controller ->
          callback:(Session_itp.proofAttemptID ->
                    Controller_itp.proof_attempt_status -> unit) ->
          notification:Session_itp.notifier ->
          final_callback:(bool ->
                          (Session_itp.proofNodeID * Whyconf.prover *
                           Call_provers.resource_limits *
                           Controller_itp.Make.report)
                          list -> unit) ->
          any:Session_itp.any option -> unit
        exception CannotRunBisectionOn of Session_itp.proofAttemptID
        val bisect_proof_attempt :
          callback_tr:(string ->
                       string list ->
                       Controller_itp.transformation_status -> unit) ->
          callback_pa:(Session_itp.proofAttemptID ->
                       Controller_itp.proof_attempt_status -> unit) ->
          notification:Session_itp.notifier ->
          removed:Session_itp.notifier ->
          Controller_itp.controller -> Session_itp.proofAttemptID -> unit
      end
end