sig
  type driver
  val load_driver_absolute :
    Env.env -> string -> string list -> Driver.driver
  val file_of_task : Driver.driver -> string -> string -> Task.task -> string
  val file_of_theory : Driver.driver -> string -> Theory.theory -> string
  val print_task :
    ?old:Pervasives.in_channel ->
    Driver.driver -> Format.formatter -> Task.task -> unit
  val print_theory :
    ?old:Pervasives.in_channel ->
    Driver.driver -> Format.formatter -> Theory.theory -> unit
  val prove_task :
    command:string ->
    limit:Call_provers.resource_limit ->
    ?old:string ->
    ?inplace:bool ->
    ?interactive:bool ->
    Driver.driver -> Task.task -> Call_provers.prover_call
  val prepare_task : Driver.driver -> Task.task -> Task.task
  val print_task_prepared :
    ?old:Pervasives.in_channel ->
    Driver.driver -> Format.formatter -> Task.task -> Printer.printer_mapping
  val prove_task_prepared :
    command:string ->
    limit:Call_provers.resource_limit ->
    ?old:string ->
    ?inplace:bool ->
    ?interactive:bool ->
    Driver.driver -> Task.task -> Call_provers.prover_call
  val syntax_map : Driver.driver -> Printer.syntax_map
end