package why3find

  1. Overview
  2. Docs

Module Why3find.ConfigSource

Configurations and Environments

Sourcetype config = {
  1. fast : float;
  2. time : float;
  3. depth : int;
  4. packages : string list;
  5. provers : string list;
  6. tactics : string list;
  7. drivers : string list;
  8. warnoff : string list;
  9. preprocess : string option;
  10. profile : Why3findUtils.Json.t option;
}

The project configuration type

Sourceval default : config

Default configuration

Sourceval conf_file : string

The name of the configuration file

Sourceval load_raw_config : string -> Why3findUtils.Json.t

Load configuration as a Json object from the given configuration file

Sourceval config_of_json : Why3findUtils.Json.t -> config

Convert the raw configuration Json object to a config value

Sourceval config_to_json : config -> Why3findUtils.Json.t

Convert the given config to a raw configuration Json object

Sourceval load_config : string -> config

Read the configuration from the given configuration file

Sourceval save_config : string -> config -> unit

Save the given configuration as a configuration file in the given directory

Sourcetype wenv = private {
  1. config : Why3.Whyconf.config;
  2. env : Why3.Env.env;
}
module WenvWhtbl : Why3.Weakhtbl.S with type key = wenv
Sourceval create_wenv : ?loadpath:string list -> Why3.Whyconf.config -> wenv

Create a why3 environment from the given why3 config. If present, the parameter loadpath is added to the loadpath defined by the config.

Sourcetype env = private {
  1. config : config;
  2. wenv : wenv;
  3. pkgs : Meta.pkg list;
}

The environment type

Sourceval create_env : ?root:string -> config:config -> unit -> env

Create an environment with configuration config for the project located in root (which default to ".")

OCaml

Innovation. Community. Security.