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 :

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


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


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:

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