gconfig.ml 14.2 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
(*    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 21

open Format
open Why
22
open Util
23
open Rc
24 25
open Whyconf

MARCHE Claude's avatar
MARCHE Claude committed
26

27 28
type prover_data = Session.prover_data
(*
MARCHE Claude's avatar
MARCHE Claude committed
29 30 31 32
    { prover_id : string;
      prover_name : string;
      prover_version : string;
      command : string;
33 34
      driver_name : string;
      driver : Driver.driver;
35
      mutable editor : string;
MARCHE Claude's avatar
MARCHE Claude committed
36
    }
37
*)
MARCHE Claude's avatar
MARCHE Claude committed
38

39
type t =
MARCHE Claude's avatar
MARCHE Claude committed
40 41 42
    { mutable window_width : int;
      mutable window_height : int;
      mutable tree_width : int;
43
      mutable task_height : int;
44
      mutable time_limit : int;
45
      mutable mem_limit : int;
MARCHE Claude's avatar
MARCHE Claude committed
46
      mutable verbose : int;
47
      mutable max_running_processes : int;
48
      mutable provers : prover_data Util.Mstr.t;
49
      mutable default_editor : string;
MARCHE Claude's avatar
MARCHE Claude committed
50
      mutable show_labels : bool;
MARCHE Claude's avatar
MARCHE Claude committed
51
      mutable env : Env.env;
52
      mutable config : Whyconf.config;
MARCHE Claude's avatar
MARCHE Claude committed
53 54
    }

MARCHE Claude's avatar
MARCHE Claude committed
55

56 57 58 59 60 61 62 63
type ide = {
  ide_window_width : int;
  ide_window_height : int;
  ide_tree_width : int;
  ide_task_height : int;
  ide_verbose : int;
  ide_default_editor : string;
}
MARCHE Claude's avatar
MARCHE Claude committed
64

65 66 67 68 69 70
let default_ide =
  { ide_window_width = 1024;
    ide_window_height = 768;
    ide_tree_width = 512;
    ide_task_height = 384;
    ide_verbose = 0;
71
    ide_default_editor = try Sys.getenv "EDITOR" with Not_found -> "editor";
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
  }

let load_ide section =
  { ide_window_width =
      get_int section ~default:default_ide.ide_window_width "window_width";
    ide_window_height =
      get_int section ~default:default_ide.ide_window_height "window_height";
    ide_tree_width =
      get_int section ~default:default_ide.ide_tree_width "tree_width";
    ide_task_height =
      get_int section ~default:default_ide.ide_task_height "task_height";
    ide_verbose =
      get_int section ~default:default_ide.ide_verbose "verbose";
    ide_default_editor =
      get_string section ~default:default_ide.ide_default_editor
        "default_editor";
  }
MARCHE Claude's avatar
MARCHE Claude committed
89

90
let load_config config =
91
  let main = get_main config in
92
  let ide  = match get_section config "ide" with
93 94
    | None -> default_ide
    | Some s -> load_ide s in
MARCHE Claude's avatar
MARCHE Claude committed
95
(*
96
  let provers = get_provers config in
MARCHE Claude's avatar
MARCHE Claude committed
97 98
*)
(*
99
  let env = Lexer.create_env main.loadpath in
MARCHE Claude's avatar
MARCHE Claude committed
100 101
*)
  (* temporary sets env to empty *)
102
  let env = Lexer.create_env [] in
MARCHE Claude's avatar
MARCHE Claude committed
103 104 105 106
  { window_height = ide.ide_window_height;
    window_width  = ide.ide_window_width;
    tree_width    = ide.ide_tree_width;
    task_height   = ide.ide_task_height;
107 108
    time_limit    = Whyconf.timelimit main;
    mem_limit     = Whyconf.memlimit main;
MARCHE Claude's avatar
MARCHE Claude committed
109
    verbose       = ide.ide_verbose;
110
    max_running_processes = Whyconf.running_provers_max main;
MARCHE Claude's avatar
MARCHE Claude committed
111
(*
MARCHE Claude's avatar
MARCHE Claude committed
112
    provers = Mstr.fold (get_prover_data env) provers [];
MARCHE Claude's avatar
MARCHE Claude committed
113
*)
114
    provers = Mstr.empty;
MARCHE Claude's avatar
MARCHE Claude committed
115
    default_editor = ide.ide_default_editor;
MARCHE Claude's avatar
MARCHE Claude committed
116
    show_labels = false;
MARCHE Claude's avatar
MARCHE Claude committed
117 118 119
    config         = config;
    env            = env
  }
MARCHE Claude's avatar
MARCHE Claude committed
120

121
let read_config () =
122
  try
123 124
    let config = Whyconf.read_config None in
    load_config config
125 126 127
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "@.%a@." Exn_printer.exn_printer e;
    exit 1
128 129

let save_config t =
130
  let save_prover _ pr acc =
131
    Mstr.add pr.Session.prover_id
132
      {
133 134 135 136 137
        Whyconf.name    = pr.Session.prover_name;
        command = pr.Session.command;
        driver  = pr.Session.driver_name;
        version = pr.Session.prover_version;
        editor  = pr.Session.editor;
138 139
      } acc in
  let config = t.config in
140
  let config = set_main config
141 142 143
    (set_limits (get_main config)
       t.time_limit t.mem_limit t.max_running_processes)
  in
144 145 146 147 148 149 150
  let ide = empty_section in
  let ide = set_int ide "window_height" t.window_height in
  let ide = set_int ide "window_width" t.window_width in
  let ide = set_int ide "tree_width" t.tree_width in
  let ide = set_int ide "task_height" t.task_height in
  let ide = set_int ide "verbose" t.verbose in
  let ide = set_string ide "default_editor" t.default_editor in
151
  let config = set_section config "ide" ide in
152
  let config = set_provers config
153
    (Mstr.fold save_prover t.provers Mstr.empty) in
154
  save_config config
MARCHE Claude's avatar
MARCHE Claude committed
155

156
let config =
MARCHE Claude's avatar
MARCHE Claude committed
157
  eprintf "reading IDE config file...@?";
158
  let c = read_config () in
MARCHE Claude's avatar
MARCHE Claude committed
159 160
  eprintf " done.@.";
  c
161 162 163 164 165 166

let save_config () = save_config config

let get_main () = (get_main config.config)


MARCHE Claude's avatar
MARCHE Claude committed
167 168 169 170 171 172 173
(*

  boomy icons

*)

let image ?size f =
174
  let main = get_main () in
MARCHE Claude's avatar
MARCHE Claude committed
175
  let n = Filename.concat (datadir main) (Filename.concat "images" (f^".png"))
MARCHE Claude's avatar
MARCHE Claude committed
176 177 178 179 180 181 182
  in
  match size with
    | None ->
        GdkPixbuf.from_file n
    | Some s ->
        GdkPixbuf.from_file_at_size ~width:s ~height:s n

MARCHE Claude's avatar
MARCHE Claude committed
183 184
let iconname_default = "undone32"
let iconname_undone = "undone32"
185
let iconname_scheduled = "pausehalf32"
MARCHE Claude's avatar
MARCHE Claude committed
186 187 188 189 190 191
let iconname_running = "play32"
let iconname_valid = "accept32"
let iconname_unknown = "help32"
let iconname_invalid = "delete32"
let iconname_timeout = "clock32"
let iconname_failure = "bug32"
192 193 194 195 196
let iconname_valid_obs = "obsaccept32"
let iconname_unknown_obs = "obshelp32"
let iconname_invalid_obs = "obsdelete32"
let iconname_timeout_obs = "obsclock32"
let iconname_failure_obs = "obsbug32"
MARCHE Claude's avatar
MARCHE Claude committed
197 198 199 200 201
let iconname_yes = "accept32"
let iconname_no = "delete32"
let iconname_directory = "folder32"
let iconname_file = "file32"
let iconname_prover = "wizard32"
202
let iconname_transf = "configure32"
MARCHE Claude's avatar
MARCHE Claude committed
203
let iconname_editor = "edit32"
204
let iconname_replay = "refresh32"
MARCHE Claude's avatar
MARCHE Claude committed
205
let iconname_reload = "movefile32"
MARCHE Claude's avatar
merge  
MARCHE Claude committed
206
let iconname_remove = "deletefile32"
207
let iconname_cleaning = "trashb32"
MARCHE Claude's avatar
MARCHE Claude committed
208 209

let image_default = ref (image ~size:20 iconname_default)
MARCHE Claude's avatar
MARCHE Claude committed
210
let image_undone = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
211 212 213 214 215 216 217
let image_scheduled = ref !image_default
let image_running = ref !image_default
let image_valid = ref !image_default
let image_unknown = ref !image_default
let image_invalid = ref !image_default
let image_timeout = ref !image_default
let image_failure = ref !image_default
218 219 220 221 222
let image_valid_obs = ref !image_default
let image_unknown_obs = ref !image_default
let image_invalid_obs = ref !image_default
let image_timeout_obs = ref !image_default
let image_failure_obs = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
223 224 225 226 227 228
let image_yes = ref !image_default
let image_no = ref !image_default
let image_directory = ref !image_default
let image_file = ref !image_default
let image_prover = ref !image_default
let image_transf = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
229
let image_editor = ref !image_default
230
let image_replay = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
231
let image_reload = ref !image_default
MARCHE Claude's avatar
merge  
MARCHE Claude committed
232
let image_remove = ref !image_default
233
let image_cleaning = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
234 235 236

let resize_images size =
  image_default := image ~size iconname_default;
MARCHE Claude's avatar
MARCHE Claude committed
237
  image_undone := image ~size iconname_undone;
MARCHE Claude's avatar
MARCHE Claude committed
238 239 240 241 242 243 244
  image_scheduled := image ~size iconname_scheduled;
  image_running := image ~size iconname_running;
  image_valid := image ~size iconname_valid;
  image_unknown := image ~size iconname_unknown;
  image_invalid := image ~size iconname_invalid;
  image_timeout := image ~size iconname_timeout;
  image_failure := image ~size iconname_failure;
245 246 247 248 249
  image_valid_obs := image ~size iconname_valid_obs;
  image_unknown_obs := image ~size iconname_unknown_obs;
  image_invalid_obs := image ~size iconname_invalid_obs;
  image_timeout_obs := image ~size iconname_timeout_obs;
  image_failure_obs := image ~size iconname_failure_obs;
MARCHE Claude's avatar
MARCHE Claude committed
250 251 252 253 254 255
  image_yes := image ~size iconname_yes;
  image_no := image ~size iconname_no;
  image_directory := image ~size iconname_directory;
  image_file := image ~size iconname_file;
  image_prover := image ~size iconname_prover;
  image_transf := image ~size iconname_transf;
MARCHE Claude's avatar
MARCHE Claude committed
256
  image_editor := image ~size iconname_editor;
257
  image_replay := image ~size iconname_replay;
MARCHE Claude's avatar
MARCHE Claude committed
258
  image_reload := image ~size iconname_reload;
MARCHE Claude's avatar
merge  
MARCHE Claude committed
259
  image_remove := image ~size iconname_remove;
260
  image_cleaning := image ~size iconname_cleaning;
MARCHE Claude's avatar
MARCHE Claude committed
261 262
  ()

MARCHE Claude's avatar
MARCHE Claude committed
263
let () =
MARCHE Claude's avatar
MARCHE Claude committed
264 265 266
  eprintf "reading icons...@?";
  resize_images 20;
  eprintf " done.@."
MARCHE Claude's avatar
MARCHE Claude committed
267 268

let show_legend_window () =
MARCHE Claude's avatar
MARCHE Claude committed
269
  let dialog = GWindow.dialog ~title:"Why: legend of icons" () in
MARCHE Claude's avatar
MARCHE Claude committed
270
  let vbox = dialog#vbox in
271 272
  let text = GText.view ~packing:vbox#add
    ~editable:false ~cursor_visible:false () in
MARCHE Claude's avatar
MARCHE Claude committed
273
  let b = text#buffer in
274 275
  let tt = b#create_tag [`WEIGHT `BOLD; `JUSTIFICATION `CENTER;
    `PIXELS_ABOVE_LINES 15; `PIXELS_BELOW_LINES 3; ] in
MARCHE Claude's avatar
MARCHE Claude committed
276
  let i s = b#insert ~iter:b#end_iter s in
277
  let it s = b#insert ~iter:b#end_iter ~tags:[tt] s in
MARCHE Claude's avatar
MARCHE Claude committed
278
  let ib i = b#insert_pixbuf ~iter:b#end_iter ~pixbuf:!i in
279
  it "Tree view\n";
MARCHE Claude's avatar
MARCHE Claude committed
280
  ib image_directory;
281
  i "   Theory, containing a set of goals\n";
MARCHE Claude's avatar
MARCHE Claude committed
282
  ib image_file;
283
  i "   Goal\n";
MARCHE Claude's avatar
MARCHE Claude committed
284
  ib image_prover;
285
  i "   External prover\n";
MARCHE Claude's avatar
MARCHE Claude committed
286
  ib image_transf;
MARCHE Claude's avatar
MARCHE Claude committed
287
  i "   Transformation\n";
288
  it "Status column\n";
MARCHE Claude's avatar
MARCHE Claude committed
289
  ib image_scheduled;
290
  i "   Scheduled external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
291
  ib image_running;
292
  i "   Running external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
293
  ib image_valid;
294 295 296 297 298
  i "   Goal is proved / Theory is fully verified\n";
(*
  ib image_invalid;
  i "   External prover disproved the goal\n";
*)
MARCHE Claude's avatar
MARCHE Claude committed
299
  ib image_timeout;
300
  i "   External prover reached the time limit\n";
MARCHE Claude's avatar
MARCHE Claude committed
301
  ib image_unknown;
302
  i "   External prover answer not conclusive\n";
MARCHE Claude's avatar
MARCHE Claude committed
303
  ib image_failure;
304
  i "   External prover call failed\n";
MARCHE Claude's avatar
MARCHE Claude committed
305
  dialog#add_button "Close" `CLOSE ;
306 307
  let t = b#create_tag [`LEFT_MARGIN 10; `RIGHT_MARGIN 10 ] in
  b#apply_tag t ~start:b#start_iter ~stop:b#end_iter;
MARCHE Claude's avatar
MARCHE Claude committed
308 309 310 311 312
  let ( _ : GWindow.Buttons.about) = dialog#run () in
  dialog#destroy ()


let show_about_window () =
MARCHE Claude's avatar
MARCHE Claude committed
313 314
  let about_dialog =
    GWindow.about_dialog
MARCHE Claude's avatar
MARCHE Claude committed
315
      ~name:"Why3"
MARCHE Claude's avatar
MARCHE Claude committed
316 317 318
      ~authors:["François Bobot";
                "Jean-Christophe Filliâtre";
                "Claude Marché";
MARCHE Claude's avatar
MARCHE Claude committed
319 320
                "Andrei Paskevich"
               ]
MARCHE Claude's avatar
MARCHE Claude committed
321
      ~copyright:"Copyright 2010-2011 Univ Paris-Sud, CNRS, INRIA"
322
      ~license:"GNU Lesser General Public License"
MARCHE Claude's avatar
MARCHE Claude committed
323 324 325
      ~website:"https://gforge.inria.fr/projects/why3"
      ~website_label:"Project web site"
      ~version:Config.version
MARCHE Claude's avatar
MARCHE Claude committed
326
      ()
MARCHE Claude's avatar
MARCHE Claude committed
327
  in
MARCHE Claude's avatar
MARCHE Claude committed
328 329
  let ( _ : GWindow.Buttons.about) = about_dialog#run () in
  about_dialog#destroy ()
MARCHE Claude's avatar
MARCHE Claude committed
330

MARCHE Claude's avatar
MARCHE Claude committed
331 332 333 334 335
let set_labels_flag = 
  let fl = Debug.lookup_flag "print_labels" in
  fun b ->
    (if b then Debug.set_flag else Debug.unset_flag) fl

336
let preferences c =
MARCHE Claude's avatar
MARCHE Claude committed
337
  let dialog = GWindow.dialog ~title:"Why: preferences" () in
MARCHE Claude's avatar
MARCHE Claude committed
338 339
  let vbox = dialog#vbox in
  let notebook = GPack.notebook ~packing:vbox#add () in
340
  (** page 1 **)
MARCHE Claude's avatar
MARCHE Claude committed
341
  let label1 = GMisc.label ~text:"General" () in
MARCHE Claude's avatar
MARCHE Claude committed
342 343 344
  let page1 =
    GPack.vbox ~homogeneous:false ~packing:
      (fun w -> ignore(notebook#append_page ~tab_label:label1#coerce w)) ()
MARCHE Claude's avatar
MARCHE Claude committed
345
  in
MARCHE Claude's avatar
MARCHE Claude committed
346 347 348 349 350 351 352 353 354 355
  (* toggle show labels in formulas *)
  let showlabels =
    GButton.check_button ~label:"show labels in formulas" ~packing:page1#add ()
      ~active:(set_labels_flag c.show_labels;c.show_labels)
  in
  let (_ : GtkSignal.id) =
    showlabels#connect#toggled ~callback:
      (fun () -> c.show_labels <- not c.show_labels;
         set_labels_flag c.show_labels)
  in
MARCHE Claude's avatar
MARCHE Claude committed
356 357
  (* editor *)
 let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
358
 let _ = GMisc.label ~text:"Default editor: " ~packing:(hb#pack ~expand:false) () in
MARCHE Claude's avatar
MARCHE Claude committed
359
 let editor_entry = GEdit.entry ~text:c.default_editor ~packing:hb#add () in
MARCHE Claude's avatar
MARCHE Claude committed
360
 let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
361 362 363
    editor_entry#connect#changed ~callback:
      (fun () -> c.default_editor <- editor_entry#text)
  in
364
  (* debug mode ? *)
MARCHE Claude's avatar
MARCHE Claude committed
365
(*
MARCHE Claude's avatar
MARCHE Claude committed
366
  let debugmode =
MARCHE Claude's avatar
MARCHE Claude committed
367
    GButton.check_button ~label:"debug" ~packing:page1#add ()
MARCHE Claude's avatar
MARCHE Claude committed
368 369
      ~active:(c.verbose > 0)
  in
MARCHE Claude's avatar
MARCHE Claude committed
370
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
371 372
    debugmode#connect#toggled ~callback:
      (fun () -> c.verbose <- 1 - c.verbose)
MARCHE Claude's avatar
MARCHE Claude committed
373
  in
MARCHE Claude's avatar
MARCHE Claude committed
374
*)
375 376
  (* timelimit ? *)
  let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
377
  let _ = GMisc.label ~text:"Time limit: " ~packing:(hb#pack ~expand:false) () in
378 379 380
  let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
  timelimit_spin#adjustment#set_bounds ~lower:2. ~upper:300. ~step_incr:1. ();
  timelimit_spin#adjustment#set_value (float_of_int c.time_limit);
MARCHE Claude's avatar
MARCHE Claude committed
381
  let (_ : GtkSignal.id) =
382 383 384 385
    timelimit_spin#connect#value_changed ~callback:
      (fun () -> c.time_limit <- timelimit_spin#value_as_int)
  in
  (* nb of processes ? *)
MARCHE Claude's avatar
MARCHE Claude committed
386
  let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
387
  let _ = GMisc.label ~text:"Nb of processes: " ~packing:(hb#pack ~expand:false) () in
MARCHE Claude's avatar
MARCHE Claude committed
388
  let nb_processes_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
389 390 391 392
  nb_processes_spin#adjustment#set_bounds
    ~lower:1. ~upper:16. ~step_incr:1. ();
  nb_processes_spin#adjustment#set_value
    (float_of_int c.max_running_processes);
MARCHE Claude's avatar
MARCHE Claude committed
393
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
394
    nb_processes_spin#connect#value_changed ~callback:
395
      (fun () -> c.max_running_processes <- nb_processes_spin#value_as_int)
MARCHE Claude's avatar
MARCHE Claude committed
396
  in
397
  (** page 2 **)
MARCHE Claude's avatar
MARCHE Claude committed
398
  let label2 = GMisc.label ~text:"Provers" () in
MARCHE Claude's avatar
MARCHE Claude committed
399 400 401
  let _page2 = GMisc.label ~text:"This page should display detected provers"
    ~packing:(fun w -> ignore(notebook#append_page
                                ~tab_label:label2#coerce w)) ()
MARCHE Claude's avatar
MARCHE Claude committed
402
  in
MARCHE Claude's avatar
MARCHE Claude committed
403 404
  dialog#add_button "Close" `CLOSE ;
  let ( _ : GWindow.Buttons.about) = dialog#run () in
MARCHE Claude's avatar
MARCHE Claude committed
405
  eprintf "saving IDE config file@.";
406
  save_config ();
MARCHE Claude's avatar
MARCHE Claude committed
407
  dialog#destroy ()
408

409
let run_auto_detection gconfig =
410 411 412
  let config = Autodetection.run_auto_detection gconfig.config in
  gconfig.config <- config;
  let provers = get_provers config in
413
  gconfig.provers <- Mstr.fold (Session.get_prover_data gconfig.env) provers Mstr.empty
MARCHE Claude's avatar
MARCHE Claude committed
414 415 416


let () = eprintf "end of configuration initialization@."
417

MARCHE Claude's avatar
MARCHE Claude committed
418
(*
MARCHE Claude's avatar
MARCHE Claude committed
419
Local Variables:
420
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
MARCHE Claude's avatar
MARCHE Claude committed
421
End:
MARCHE Claude's avatar
MARCHE Claude committed
422
*)