Module Controller_itp

module Controller_itp: sig .. end

Controller to run provers and transformations asynchronously on goals of a session


State of a proof or transformation in progress

type proof_attempt_status = 
| Undone (*

prover was never called

*)
| Scheduled (*

external proof attempt is scheduled

*)
| Running (*

external proof attempt is in progress

*)
| Done of Call_provers.prover_result (*

external proof done

*)
| Interrupted (*

external proof has never completed

*)
| Detached (*

parent goal has no task, is detached

*)
| InternalFailure of exn (*

external proof aborted by internal error

*)
| Uninstalled of Whyconf.prover (*

prover is uninstalled

*)
| UpgradeProver of Whyconf.prover (*

prover is upgraded

*)
| Removed of Whyconf.prover (*

prover has been removed or upgraded

*)
val print_status : Stdlib.Format.formatter -> 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 -> 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 -> strategy_status -> unit

Signature for asynchronous schedulers

val default_delay_ms : int

Default delay for the scheduler timeout

module type Scheduler = sig .. end

Controllers

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

creates a controller for the given session. The config and env is used to load the drivers for the provers.

val set_session_max_tasks : int -> unit

sets the maximum number of proof tasks that can be running at the same time. Initially set to 1.

val set_session_memlimit : controller -> int -> unit

sets the default memlimit for proof attempts

val set_session_timelimit : controller -> float -> unit

sets the default timelimit for proof attempts

val set_session_prover_upgrade_policy : controller ->
Whyconf.prover -> Whyconf.prover_upgrade_policy -> unit
val print_session : Stdlib.Format.formatter -> 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 -> bool * bool

reload_files c returns a pair (o,d): o true means there are obsolete goals, d means there are missed objects (goals, transformations, theories or files) that are now detached in the session returned.

If parsing or typing errors occurs, a list of errors is raised inside exception Controller_itp.Errors_list.

The detailed process of reloading the files of the given session is as follows.

When the option hard_reload is true (false by default), libraries and drivers are also reloaded.

When the option ignore_shapes is true, the shapes are not taken into account for merging with the old session.

When optional argument reparse_file_fun is an extra function explained in Session_itp.merge_files_gen

val add_file : controller -> ?format:Env.fformat -> string -> unit

add_file cont ?fmt fname parses the source file fname and add the resulting theories to the session of cont. parsing or typing errors are raised inside exception Controller_itp.Errors_list

val remove_subtree : notification:Session_itp.notifier ->
removed:Session_itp.notifier ->
controller -> Session_itp.any -> unit

remove a subtree of the session, taking care of not removing any proof attempt in progress. raise RemoveError if removal is not possible.

val get_undetached_children_no_pa : Session_itp.session -> Session_itp.any -> Session_itp.any list
val set_partial_config : controller -> Whyconf.config -> unit

edit a minimal part of the configuration that should be safe to edit during execution of the server (provers config, editors)

Scheduled jobs

module Make: 
functor (* : sig
end) -> sig .. end