module Controller_itp:sig
..end
Controller to run provers and transformations asynchronously on goals of a session
type
proof_attempt_status =
| |
Undone |
(* | prover was never called | *) |
| |
Scheduled |
(* | external proof attempt is scheduled | *) |
| |
Running |
(* | external proof attempt is in progress | *) |
| |
Done of |
(* | external proof done | *) |
| |
Interrupted |
(* | external proof has never completed | *) |
| |
Detached |
(* | parent goal has no task, is detached | *) |
| |
InternalFailure of |
(* | external proof aborted by internal error | *) |
| |
Uninstalled of |
(* | prover is uninstalled | *) |
| |
UpgradeProver of |
(* | prover is upgraded | *) |
| |
Removed of |
(* | prover has been removed or upgraded | *) |
val print_status : Stdlib.Format.formatter -> proof_attempt_status -> unit
type
transformation_status =
| |
TSscheduled |
| |
TSdone of |
| |
TSfailed of |
| |
TSfatal of |
val print_trans_status : Stdlib.Format.formatter -> transformation_status -> unit
type
strategy_status =
| |
STSgoto of |
| |
STShalt |
| |
STSfatal of |
val print_strategy_status : Stdlib.Format.formatter -> strategy_status -> unit
val default_delay_ms : int
Default delay for the scheduler timeout
module type Scheduler =sig
..end
type
controller = private {
|
mutable controller_session : |
|
mutable controller_config : |
|
mutable controller_env : |
|
controller_provers : |
|
controller_strategies : |
|
controller_running_proof_attempts : |
}
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)
module Make: