whyconf.ml 8.43 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
19 20

open Format
21
open Util
22
open Rc
23

24 25
(* lib and shared dirs *)

MARCHE Claude's avatar
MARCHE Claude committed
26
let compilation_libdir = default_option Config.libdir Config.localdir
27

MARCHE Claude's avatar
MARCHE Claude committed
28 29
let compilation_datadir = 
  option_apply Config.datadir
30 31
    (fun d -> Filename.concat d "share") Config.localdir

MARCHE Claude's avatar
MARCHE Claude committed
32 33 34
let compilation_loadpath = 
  Filename.concat compilation_datadir "theories"

35
let default_conf_file =
36 37 38
  match Config.localdir with
    | None -> Filename.concat (Rc.get_home_dir ()) ".why.conf"
    | Some d -> Filename.concat d "why.conf"
39

40 41 42
(* Configuration file *)

type config_prover = {
43 44 45
  name    : string;   (* "Alt-Ergo v2.95 (special)" *)
  command : string;   (* "exec why-limit %t %m alt-ergo %f" *)
  driver  : string;   (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
46 47 48 49 50
  version : string;   (* "v2.95" *)
  editor  : string;
}

type main = {
51 52 53 54 55
  private_libdir   : string;      (* "/usr/local/lib/why/" *)
  private_datadir  : string;      (* "/usr/local/share/why/" *)
  loadpath  : string list;  (* "/usr/local/lib/why/theories" *)
  timelimit : int;   (* default prover time limit in seconds
                               (0 unlimited) *)
56
  memlimit  : int;
57
  (* default prover memory limit in megabytes (0 unlimited)*)
58
  running_provers_max : int;
59
  (* max number of running prover processes *)
François Bobot's avatar
François Bobot committed
60 61 62
  plugins : string list;
  (* plugins to load, without extension, relative to 
     [private_libdir]/plugins *)
63 64
}

MARCHE Claude's avatar
MARCHE Claude committed
65 66 67 68 69 70 71
let libdir m =
  try
    Sys.getenv "WHY3LIB"
  with Not_found -> m.private_libdir

let datadir m =
  try
72 73 74 75 76
    let d = Sys.getenv "WHY3DATA" in
(*
    eprintf "[Info] datadir set using WHY3DATA='%s'@." d;
*)
    d
MARCHE Claude's avatar
MARCHE Claude committed
77 78
  with Not_found -> m.private_datadir

79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
let loadpath m = 
  try
    let d = Sys.getenv "WHY3LOADPATH" in
(*
    eprintf "[Info] loadpath set using WHY3LOADPATH='%s'@." d;
*)
    [d]
  with Not_found -> m.loadpath

let timelimit m = m.timelimit
let memlimit m = m.memlimit
let running_provers_max m = m.running_provers_max

let set_limits m time mem running =
  { m with timelimit = time; memlimit = mem; running_provers_max = running }

François Bobot's avatar
François Bobot committed
95 96 97 98 99 100 101 102 103 104 105 106 107 108
let plugins m = m.plugins
let set_plugins m pl =
  (* TODO : sanitize? *)
  { m with plugins = pl}
let add_plugin m p =
  if List.mem p m.plugins
  then m
  else { m with plugins = List.rev (p::(List.rev m.plugins))}

let pluginsdir m = Filename.concat m.private_libdir "plugins"
let load_plugins m =
  let dirs = [pluginsdir m] in
  let load x =
    try Plugin.load ~dirs x
109 110 111
    with exn ->
      Format.eprintf "%s can't be loaded : %a@." x
        Exn_printer.exn_printer exn in
François Bobot's avatar
François Bobot committed
112 113
  List.iter load m.plugins

114 115
type config = {
  conf_file : string;       (* "/home/innocent_user/.why.conf" *)
116
  config    : Rc.t  ;
117 118
  main      : main;
  provers   : config_prover Mstr.t;
119 120
}

121 122
let default_main =
  {
MARCHE Claude's avatar
MARCHE Claude committed
123 124 125
    private_libdir = compilation_libdir;
    private_datadir = compilation_datadir;
    loadpath = [compilation_loadpath];
126 127 128
    timelimit = 10;
    memlimit = 0;
    running_provers_max = 2;
François Bobot's avatar
François Bobot committed
129
    plugins = [];
130
  }
131

132
let set_main rc main =
133
  let section = empty_section in
MARCHE Claude's avatar
MARCHE Claude committed
134 135
  let section = set_string section "libdir"    main.private_libdir in
  let section = set_string section "datadir"    main.private_datadir in
136 137 138 139 140
  let section = set_stringl section "loadpath" main.loadpath in
  let section = set_int section "timelimit" main.timelimit in
  let section = set_int section "memlimit" main.memlimit in
  let section =
    set_int section "running_provers_max" main.running_provers_max in
François Bobot's avatar
François Bobot committed
141
  let section = set_stringl section "plugin" main.plugins in
142
  set_section rc "main" section
143 144 145 146 147 148 149 150 151 152

let set_prover id prover family =
  let section = empty_section in
  let section = set_string section "name" prover.name in
  let section = set_string section "command" prover.command in
  let section = set_string section "driver" prover.driver in
  let section = set_string section "version" prover.version in
  let section = set_string section "editor" prover.editor in
  (id,section)::family

153
let set_provers rc provers =
154
  let family = Mstr.fold set_prover provers [] in
155
  set_family rc "prover" family
156

157 158 159 160 161 162
let absolute_filename dirname f =
  if Filename.is_relative f then
    Filename.concat dirname f
  else
    f

163 164 165 166 167 168 169 170 171 172 173
let load_prover dirname provers (id,section) =
  Mstr.add id
    { name    = get_string section "name";
      command = get_string section "command";
      (* TODO command : absolute_filename dirname ? *)
      driver  = absolute_filename dirname (get_string section "driver");
      version = get_string ~default:"" section "version";
      editor  = get_string ~default:"" section "editor";
    } provers

let load_main dirname section =
174 175 176 177
  { private_libdir    = get_string ~default:default_main.private_libdir
      section "libdir";
    private_datadir   = get_string ~default:default_main.private_datadir
      section "datadir";
178
    loadpath  = List.map (absolute_filename dirname)
179 180 181 182 183 184
      (get_stringl ~default:default_main.loadpath section "loadpath");
    timelimit = get_int ~default:default_main.timelimit section "timelimit";
    memlimit  = get_int ~default:default_main.memlimit section "memlimit";
    running_provers_max =
      get_int ~default:default_main.running_provers_max section
        "running_provers_max";
François Bobot's avatar
François Bobot committed
185
    plugins = get_stringl ~default:[] section "plugin";
186 187
  }

188

189
let read_config_rc conf_file =
190 191 192 193 194
  let filename = match conf_file with
    | Some filename -> filename
    | None -> begin try Sys.getenv "WHY_CONFIG" with Not_found ->
          if Sys.file_exists "why.conf" then "why.conf" else
          if Sys.file_exists ".why.conf" then ".why.conf" else
195 196
          if Sys.file_exists default_conf_file then default_conf_file
          else raise Exit
197 198
        end
  in
199 200 201 202 203 204 205 206 207 208 209
  filename,Rc.from_file filename

let get_config (filename,rc) =
  let dirname = Filename.dirname filename in
  let rc, main =
    match get_section rc "main" with
      | None -> set_main rc default_main,default_main
      | Some main ->
        rc, load_main dirname main in
  let provers = get_family rc "prover" in
  let provers = List.fold_left (load_prover dirname) Mstr.empty provers in
210
  { conf_file = filename;
211 212 213
    config    = rc;
    main      = main;
    provers   = provers;
214
  }
215

216 217 218
let default_config conf_file = get_config (conf_file,Rc.empty)


219
let read_config conf_file =
220
  let filenamerc = try read_config_rc conf_file
221
    with Exit -> (default_conf_file,Rc.empty) in
222
  get_config filenamerc
MARCHE Claude's avatar
MARCHE Claude committed
223

224

225
let save_config config = to_file config.conf_file config.config
226

227 228
let get_main config = config.main
let get_provers config = config.provers
229

230 231 232 233
let set_main config main =
  {config with
    config = set_main config.config main;
    main = main;
234 235
  }

236 237 238 239 240
let set_provers config provers =
  {config with
    config = set_provers config.config provers;
    provers = provers;
  }
241

242
let set_conf_file config conf_file = {config with conf_file = conf_file}
243
let get_conf_file config           =  config.conf_file
244

245 246
let get_section config name = assert (name <> "main");
  get_section config.config name
247

248 249
let get_family config name = assert (name <> "prover");
  get_family config.config name
250 251


252 253
let set_section config name section = assert (name <> "main");
  {config with config = set_section config.config name section}
254

255 256
let set_family config name section = assert (name <> "prover");
  {config with config = set_family config.config name section}