whyconf.ml 8.44 KB
Newer Older
1
2
3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
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
(* lib and shared dirs *)

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

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

32
let compilation_loadpath =
33
34
  [ Filename.concat compilation_datadir "theories";
    Filename.concat compilation_datadir "modules"; ]
MARCHE Claude's avatar
MARCHE Claude committed
35

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

41
42
43
(* Configuration file *)

type config_prover = {
44
45
46
  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" *)
47
48
49
50
51
  version : string;   (* "v2.95" *)
  editor  : string;
}

type main = {
52
53
54
55
56
  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) *)
57
  memlimit  : int;
58
  (* default prover memory limit in megabytes (0 unlimited)*)
59
  running_provers_max : int;
60
  (* max number of running prover processes *)
François Bobot's avatar
François Bobot committed
61
  plugins : string list;
62
  (* plugins to load, without extension, relative to
François Bobot's avatar
François Bobot committed
63
     [private_libdir]/plugins *)
64
65
}

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

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

80
let loadpath m =
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
  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
96
97
98
99
100
101
102
103
104
105
106
107
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 load x =
108
    try Plugin.load 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
    private_libdir = compilation_libdir;
    private_datadir = compilation_datadir;
125
    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}