module Whyconf:sig
..end
Managing the configuration of Why3
type
config
A configuration linked to an rc file. Whyconf gives access to
every sections of the rc file (Whyconf.get_section
,
Whyconf.set_section
, Whyconf.get_family
,
Whyconf.set_family
) but the section main and the family prover
which are dealt by it (Whyconf.get_main
, Whyconf.set_main
,
Whyconf.get_provers
, Whyconf.set_provers
exception ConfigFailure of string * string
exception DuplicateShortcut of string
val read_config : string option -> config
read_config conf_file
:
val init_config : ?extra_config:string list -> string option -> config
init_config ?extra_config conf_file
Add the automatically generated part of the configuration, and load plugins
val read_config_rc : string option -> string * Rc.t
read_config_rc conf_file
same rule than Whyconf.init_config
but just returned
the parsed Rc file
val add_extra_config : config -> string -> config
add_extra_config config filename
merge the content of filename
into config
val empty_rc : Rc.t
val save_config : config -> unit
save_config config
save the configuration
val default_config : string -> config
default_config filename
create a default configuration which is going
to be saved in filename
val get_conf_file : config -> string
get_conf_file config
get the rc file corresponding to this
configuration
val rc_of_config : config -> Rc.t
type
main
val get_main : config -> main
get_main config
get the main section stored in the Rc file
val set_main : config -> main -> config
set_main config main
replace the main section by the given one
val set_stdlib : bool -> config -> config
Set if the standard library should be added to loadpath
val set_load_default_plugins : bool -> config -> config
Set if the plugins in the default path should be loaded
val libdir : main -> string
val datadir : main -> string
val loadpath : main -> string list
val set_loadpath : main -> string list -> main
val timelimit : main -> int
val memlimit : main -> int
val running_provers_max : main -> int
val set_limits : main -> int -> int -> int -> main
val default_editor : main -> string
editor name used when no specific editor known for a prover
val set_default_editor : main -> string -> main
val plugins : main -> string list
val pluginsdir : main -> string
val set_plugins : main -> string list -> main
val add_plugin : main -> string -> main
val load_plugins : main -> unit
type
prover = {
|
prover_name : |
|
prover_version : |
|
prover_altern : |
record of necessary data for a given external prover
val print_prover : Stdlib.Format.formatter -> prover -> unit
val print_prover_parseable_format : Stdlib.Format.formatter -> prover -> unit
val prover_parseable_format : prover -> string
module Prover:OrderedHashedType
with type t = prover
Printer for prover
module Mprover:Extmap.S
with type key = prover
module Sprover:Extset.S
with module M = Mprover
module Hprover:Exthtbl.S
with type key = prover
type
config_prover = {
|
prover : |
|
command : |
|
command_steps : |
|
driver : |
|
in_place : |
|
editor : |
|
interactive : |
|
extra_options : |
|
extra_drivers : |
val get_complete_command : config_prover -> with_steps:bool -> string
add the extra_options to the command
val get_provers : config -> config_prover Mprover.t
get_provers config
get the prover family stored in the Rc file. The
keys are the unique ids of the prover (argument of the family)
val get_prover_config : config -> prover -> config_prover
get_prover_config config prover
get the prover config as stored in
the config. Raise Not_found if the prover does not exists in the config.
val set_provers : config ->
?shortcuts:prover Wstdlib.Mstr.t ->
config_prover Mprover.t -> config
set_provers config provers
replace all the family prover by the
one given
val is_prover_known : config -> prover -> bool
test if a prover is detected
val get_prover_shortcuts : config -> prover Wstdlib.Mstr.t
return the prover shortcuts
val set_prover_shortcuts : config -> prover Wstdlib.Mstr.t -> config
set the prover shortcuts
type
config_editor = {
|
editor_name : |
|
editor_command : |
|
editor_options : |
module Meditor:Extmap.S
with type key = string
val set_editors : config -> config_editor Meditor.t -> config
replace the set of editors
val get_editors : config -> config_editor Meditor.t
returns the set of editors
val editor_by_id : config -> string -> config_editor
return the configuration of the editor if found, otherwise return Not_found
prover upgrade policy
type
prover_upgrade_policy =
| |
CPU_keep |
| |
CPU_upgrade of |
| |
CPU_duplicate of |
| |
CPU_remove |
val print_prover_upgrade_policy : Stdlib.Format.formatter -> prover_upgrade_policy -> unit
val set_prover_upgrade_policy : config ->
prover -> prover_upgrade_policy -> config
set_prover_upgrade c p cpu
sets or updates the policy to follow if the
prover p
is absent from the system
val get_prover_upgrade_policy : config -> prover -> prover_upgrade_policy
get_prover_upgrade config
returns a map providing the policy to
follow for each absent prover (if it has already been decided
by the user and thus stored in the config)
val get_policies : config -> prover_upgrade_policy Mprover.t
val set_policies : config ->
prover_upgrade_policy Mprover.t -> config
strategies
type
config_strategy = {
|
strategy_name : |
|
strategy_desc : |
|
strategy_code : |
|
strategy_shortcut : |
val get_strategies : config -> config_strategy Wstdlib.Mstr.t
val add_strategy : config -> config_strategy -> config
type
filter_prover
filter prover
val mk_filter_prover : ?version:string -> ?altern:string -> string -> filter_prover
val print_filter_prover : Stdlib.Format.formatter -> filter_prover -> unit
val parse_filter_prover : string -> filter_prover
parse the string representing a filter_prover:
regexp must start with ^. Partial match will be used.
val filter_prover_with_shortcut : config -> filter_prover -> filter_prover
resolve prover shortcut in filter
val filter_prover : filter_prover -> prover -> bool
test if the prover match the filter prover
val filter_provers : config ->
filter_prover -> config_prover Mprover.t
Get all the provers that match this filter
exception ProverNotFound of config * filter_prover
exception ProverAmbiguity of config * filter_prover
* config_prover Mprover.t
exception ParseFilterProver of string
val filter_one_prover : config -> filter_prover -> config_prover
find the uniq prover that verify the filter. If it doesn't exists raise ProverNotFound or raise ProverAmbiguity
val why3_regexp_of_string : string -> Re.Str.regexp
module User:sig
..end
Common command line options
module Args:sig
..end
Loading drivers with relative names
val load_driver_raw : main -> Env.env -> string -> string list -> Driver.driver
load_driver_raw main env file extras
loads the driver in file
file
and with additional drivers in list extras
, in the context
of the configuration main
and environment env
. This function
is a wrapper to the lower level function
Driver.load_driver_absolute
val load_driver : main -> Env.env -> config_prover -> Driver.driver
load_driver main env p
loads the driver for prover p
,
in the context of the configuration main
and environment env
.
This function is a wrapper to the lower level function
load_driver_raw
val unknown_to_known_provers : config_prover Mprover.t ->
prover ->
prover list * prover list * prover list
return others, same name, same version
*/
Internal, recursive functionality with Autodetection
val provers_from_detected_provers : (save_to:string -> Rc.t -> config) Stdlib.ref
*/