Module Whyconf

module Whyconf: sig .. end

Managing the configuration of Why3

General configuration

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 :

If conf_file is given, then
if it is an empty string, an empty config is loaded,
if the file doesn't exist, Rc.CannotOpen is raised,
otherwise the content of the file is parsed and returned.
If conf_file is None and the WHY3CONFIG environment variable exists, then the above steps are executed with the content of the variable (possibly empty).
If neither conf_file nor WHY3CONFIG are present, the file "$HOME/.why3.conf" (or "$USERPROFILE/.why3.conf" under Windows) is checked for existence:
if present, the content is parsed and returned,
otherwise, we return the built-in default_config with a default configuration filename.

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

Main section

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

Provers

Prover's identifier

type prover = {

	`prover_name : string;`
	`prover_version : string;`
	`prover_altern : string;`

}

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

Prover configuration

type config_prover = {

	`prover : prover;`
	`command : string;`
	`command_steps : string option;`
	`driver : string;`
	`in_place : bool;`
	`editor : string;`
	`interactive : bool;`
	`extra_options : string list;`
	`extra_drivers : string list;`

}

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 : string;`
	`editor_command : string;`
	`editor_options : string list;`

}

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 prover`
`\|`	`CPU_duplicate of prover`
`\|`	`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 : string;`
	`strategy_desc : string;`
	`strategy_code : string;`
	`strategy_shortcut : string;`

}

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:

"name,version,altern"
"name,version" -> "name,version,^.*"
"name,,altern" -> "name,^.*,altern"
"name" -> "name,^.*,^.*"

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

For accesing and modifying the user configuration

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