whyconf.ml 9.25 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18
(*    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
(* magicnumber for the configuration :
  - 0 before the magic number
26
  - 1 when no loadpath meant default loadpath
27 28
  - 2
  - 5 cvc3 native
Andrei Paskevich's avatar
Andrei Paskevich committed
29
  - 6 driver renaming
30
  - 7 yices native (used for release 0.70)
31
  - 8 for release 0.71
32
  - 9 coq realizations
33
  - 10 require %f in editor lines
34

35
If a configuration doesn't contain the actual magic number we don't use it.*)
36

37
let magicnumber = 10
38

39 40
exception WrongMagicNumber

41 42
(* lib and shared dirs *)

43 44 45
let default_loadpath =
  [ Filename.concat Config.datadir "theories";
    Filename.concat Config.datadir "modules"; ]
MARCHE Claude's avatar
MARCHE Claude committed
46

47
let default_conf_file =
48
  match Config.localdir with
49 50
    | None -> Filename.concat (Rc.get_home_dir ()) ".why3.conf"
    | Some d -> Filename.concat d "why3.conf"
51

52 53 54
(* Configuration file *)

type config_prover = {
55 56 57
  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" *)
58 59
  version : string;   (* "v2.95" *)
  editor  : string;
60
  interactive : bool;
61 62 63
}

type main = {
64 65
  libdir   : string;      (* "/usr/local/lib/why/" *)
  datadir  : string;      (* "/usr/local/share/why/" *)
66
  loadpath  : string list;  (* "/usr/local/lib/why/theories" *)
67 68
  timelimit : int;
  (* default prover time limit in seconds (0 unlimited) *)
69
  memlimit  : int;
70
  (* default prover memory limit in megabytes (0 unlimited)*)
71
  running_provers_max : int;
72
  (* max number of running prover processes *)
François Bobot's avatar
François Bobot committed
73
  plugins : string list;
74
  (* plugins to load, without extension, relative to [libdir]/plugins *)
75 76
}

MARCHE Claude's avatar
MARCHE Claude committed
77 78 79
let libdir m =
  try
    Sys.getenv "WHY3LIB"
80
  with Not_found -> m.libdir
MARCHE Claude's avatar
MARCHE Claude committed
81 82 83

let datadir m =
  try
84 85 86 87 88
    let d = Sys.getenv "WHY3DATA" in
(*
    eprintf "[Info] datadir set using WHY3DATA='%s'@." d;
*)
    d
89
  with Not_found -> m.datadir
MARCHE Claude's avatar
MARCHE Claude committed
90

91
let loadpath m =
92 93 94 95 96
  try
    let d = Sys.getenv "WHY3LOADPATH" in
(*
    eprintf "[Info] loadpath set using WHY3LOADPATH='%s'@." d;
*)
97
    Str.split (Str.regexp ":") d
98 99 100 101 102 103 104 105 106
  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
107 108 109 110
let plugins m = m.plugins
let set_plugins m pl =
  (* TODO : sanitize? *)
  { m with plugins = pl}
111

François Bobot's avatar
François Bobot committed
112 113 114 115 116
let add_plugin m p =
  if List.mem p m.plugins
  then m
  else { m with plugins = List.rev (p::(List.rev m.plugins))}

Andrei Paskevich's avatar
Andrei Paskevich committed
117
let pluginsdir m = Filename.concat m.libdir "plugins"
François Bobot's avatar
François Bobot committed
118 119
let load_plugins m =
  let load x =
120
    try Plugin.load x
121 122 123
    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
124 125
  List.iter load m.plugins

126
type config = {
127
  conf_file : string;       (* "/home/innocent_user/.why3.conf" *)
128
  config    : Rc.t;
129 130
  main      : main;
  provers   : config_prover Mstr.t;
131 132
}

133 134
let default_main =
  {
135 136 137
    libdir = Config.libdir;
    datadir = Config.datadir;
    loadpath = default_loadpath;
138 139 140
    timelimit = 10;
    memlimit = 0;
    running_provers_max = 2;
François Bobot's avatar
François Bobot committed
141
    plugins = [];
142
  }
143

144
let set_main rc main =
145
  let section = empty_section in
146
  let section = set_int section "magic" magicnumber in
147 148 149 150 151
  let section = set_string ~default:default_main.libdir
    section "libdir" main.libdir in
  let section = set_string ~default:default_main.datadir
    section "datadir" main.datadir in
  let section = set_stringl section "loadpath" main.loadpath in
152 153 154 155
  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
156
  let section = set_stringl section "plugin" main.plugins in
157
  set_section rc "main" section
158 159 160 161 162 163 164 165

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
166
  let section = set_bool section "interactive" prover.interactive in
167 168
  (id,section)::family

169
let set_provers rc provers =
170
  let family = Mstr.fold set_prover provers [] in
171
  set_family rc "prover" family
172

173
let absolute_filename = Sysutil.absolutize_filename
174

175 176 177 178 179 180 181
let load_prover dirname provers (id,section) =
  Mstr.add id
    { name    = get_string section "name";
      command = get_string section "command";
      driver  = absolute_filename dirname (get_string section "driver");
      version = get_string ~default:"" section "version";
      editor  = get_string ~default:"" section "editor";
182
      interactive = get_bool ~default:false section "interactive";
183 184 185
    } provers

let load_main dirname section =
186 187
  if get_int ~default:0 section "magic" <> magicnumber then
    raise WrongMagicNumber;
188 189
  { libdir    = get_string ~default:default_main.libdir section "libdir";
    datadir   = get_string ~default:default_main.datadir section "datadir";
190
    loadpath  = List.map (absolute_filename dirname)
191
      (get_stringl ~default:[] section "loadpath");
192 193
    timelimit = get_int ~default:default_main.timelimit section "timelimit";
    memlimit  = get_int ~default:default_main.memlimit section "memlimit";
194 195
    running_provers_max = get_int ~default:default_main.running_provers_max
      section "running_provers_max";
François Bobot's avatar
François Bobot committed
196
    plugins = get_stringl ~default:[] section "plugin";
197 198
  }

199
let read_config_rc conf_file =
200 201
  let filename = match conf_file with
    | Some filename -> filename
202
    | None -> begin try Sys.getenv "WHY3CONFIG" with Not_found ->
203 204
          if Sys.file_exists default_conf_file then default_conf_file
          else raise Exit
205 206
        end
  in
207 208 209 210 211
  filename, Rc.from_file filename

exception ConfigFailure of string (* filename *) * string

let () = Exn_printer.register (fun fmt e -> match e with
212
  | ConfigFailure (f, s) ->
213
      Format.fprintf fmt "error in config file %s: %s" f s
214 215
  | WrongMagicNumber ->
      Format.fprintf fmt "outdated config file; rerun why3config"
216
  | _ -> raise e)
217 218 219 220 221

let get_config (filename,rc) =
  let dirname = Filename.dirname filename in
  let rc, main =
    match get_section rc "main" with
222
      | None      -> raise (ConfigFailure (filename, "no main section"))
223
      | Some main -> rc, load_main dirname main
224
  in
225 226
  let provers = get_family rc "prover" in
  let provers = List.fold_left (load_prover dirname) Mstr.empty provers in
227
  { conf_file = filename;
228 229 230
    config    = rc;
    main      = main;
    provers   = provers;
231
  }
232

233
let default_config conf_file =
234
  get_config (conf_file, set_main Rc.empty default_main)
235

236
let read_config conf_file =
237 238
  let filenamerc =
    try
239
      read_config_rc conf_file
240
    with Exit ->
241 242
      default_conf_file, set_main Rc.empty default_main
  in
243
  try
244
    get_config filenamerc
245 246 247 248
  with e when not (Debug.test_flag Debug.stack_trace) ->
    let b = Buffer.create 40 in
    Format.bprintf b "%a" Exn_printer.exn_printer e;
    raise (ConfigFailure (fst filenamerc, Buffer.contents b))
249

250
let save_config config =
251
  let filename = config.conf_file in
252
  Sysutil.backup_file filename;
253
  to_file filename config.config
254

255 256
let get_main config = config.main
let get_provers config = config.provers
257

258 259 260 261
let set_main config main =
  {config with
    config = set_main config.config main;
    main = main;
262 263
  }

264 265 266 267 268
let set_provers config provers =
  {config with
    config = set_provers config.config provers;
    provers = provers;
  }
269

270
let set_conf_file config conf_file = {config with conf_file = conf_file}
271
let get_conf_file config           =  config.conf_file
272

273 274
let get_section config name = assert (name <> "main");
  get_section config.config name
275

276 277
let get_family config name = assert (name <> "prover");
  get_family config.config name
278 279


280 281
let set_section config name section = assert (name <> "main");
  {config with config = set_section config.config name section}
282

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