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 merge_config : config -> string -> config

merge_config config filename merge the content of filename into config

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

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 libdir : main -> string

val datadir : main -> string

val loadpath : main -> string list

val timelimit : main -> int

val memlimit : main -> int

val running_provers_max : main -> int

val cntexample : main -> bool

val set_limits : main -> int -> int -> int -> main

val set_cntexample : main -> bool -> 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 : Format.formatter -> prover -> unit

val print_prover_parseable_format : 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 set_provers : config ->
       ?shortcuts:prover Stdlib.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 Stdlib.Mstr.t

return the prover shortcuts

val set_prover_shortcuts : config -> prover Stdlib.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`

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 Stdlib.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 : 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 -> Str.regexp

For accesing other parts of the configuration

val get_section : config -> string -> Rc.section option

Access to the Rc.t

get_section config name Same as Rc.get_section except name must not be "main"

val get_family : config -> string -> Rc.family

get_family config name Same as Rc.get_family except name must not be prover

val set_section : config -> string -> Rc.section -> config

set_section config name Same as Rc.set_section except name must not be "main"

val set_family : config -> string -> Rc.family -> config

set_family config name Same as Rc.set_family except name must not be prover

Common command line options

module Args: sig .. end

Loading drivers with relative names

val load_driver : main -> Env.env -> string -> string list -> Driver.driver

wrapper for loading a driver from a file that may be relative to the datadir. See Driver.load_driver_absolute