autodetection.ml 6.36 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

open Format
open Util
open Whyconf
open Rc


(* auto-detection of provers *)

type prover_kind = ATP | ITP
type prover_autodetection_data =
    { kind : prover_kind;
      prover_id : string;
      prover_name : string;
      execs : string list;
      version_switch : string;
      version_regexp : string;
      versions_ok : string list;
      versions_old : string list;
      prover_command : string;
      prover_driver : string;
      prover_editor : string;
    }

let prover_keys =
  let add acc k = Sstr.add k acc in
  List.fold_left add Sstr.empty
    ["name";"exec";"version_switch";"version_regexp";
     "version_ok";"version_old";"command";
     "editor";"driver"]

let load_prover kind (id,section) =
  check_exhaustive section prover_keys;
  { kind = kind;
    prover_id = id;
    prover_name = get_string section "name";
    execs = get_stringl section "exec";
    version_switch = get_string section ~default:"" "version_switch";
    version_regexp = get_string section ~default:"" "version_regexp";
    versions_ok = get_stringl section ~default:[] "version_ok";
    versions_old = get_stringl section ~default:[] "version_old";
    prover_command = get_string section "command";
    prover_driver = get_string section "driver";
    prover_editor = get_string section ~default:"" "editor";
  }

let load rc =
  let atps = get_family rc "ATP" in
  let atps = List.map (load_prover ATP) atps in
  let itps = get_family rc "ITP" in
  let tps = List.fold_left (cons (load_prover ITP)) atps itps in
  tps

let read_auto_detection_data main =
73 74
  let filename = Filename.concat (Whyconf.datadir main)
    "provers-detection-data.conf" in
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
  try
    let rc = Rc.from_file filename in
    load rc
  with
    | Failure "lexing" ->
        eprintf "Syntax error in provers-detection-data.conf@.";
        exit 2
    | Not_found ->
        eprintf "provers-detection-data.conf not found at %s@." filename;
        exit 2


let provers_found = ref 0

let prover_tips_info = ref false


let make_command exec com =
  let cmd_regexp = Str.regexp "%\\(.\\)" in
  let replace s = match Str.matched_group 1 s with
    | "e" -> exec
    | c -> "%"^c
  in
  Str.global_substitute cmd_regexp replace com

100 101 102 103 104 105 106 107 108 109 110
let sanitize_exec =
  let first c = match c with
    | '_' | ' ' -> "_"
    | _ -> Ident.char_to_alpha c
  in
  let rest c = match c with
    | '+' | '-' | '.' -> String.make 1 c
    | _ -> Ident.char_to_alnumus c
  in
  Ident.sanitizer first rest

111
let detect_prover main acc data =
112 113
  let keys = Queue.create () in
  let acc = List.fold_left
114 115 116
    (fun acc com ->
	let out = Filename.temp_file "out" "" in
        let cmd = sprintf "%s %s" com data.version_switch in
MARCHE Claude's avatar
MARCHE Claude committed
117
	let c = sprintf "(%s) > %s 2>&1" cmd out in
118
        eprintf "Run : %s@." c;
119 120 121 122 123 124 125 126 127 128
	let ret = Sys.command c in
	if ret <> 0 then
	  begin
	    eprintf "command '%s' failed@." cmd;
	    acc
	  end
	else
	  let s =
            try
              let ch = open_in out in
MARCHE Claude's avatar
MARCHE Claude committed
129 130 131 132
              let c = Sysutil.channel_contents ch in
              close_in ch;
	      Sys.remove out;
              c
133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
            with Not_found | End_of_file  -> ""
          in
	  let re = Str.regexp data.version_regexp in
	  try
            ignore (Str.search_forward re s 0);
	    let nam = data.prover_name in
	    let ver = Str.matched_group 1 s in
            if List.mem ver data.versions_ok then
	      eprintf "Found prover %s version %s, OK.@." nam ver
            else
              begin
                prover_tips_info := true;
                if List.mem ver data.versions_old then
                  eprintf "Warning: prover %s version %s is quite old, please \
                           consider upgrading to a newer version.@."
                    nam ver
                else
                  eprintf "Warning: prover %s version %s is not known to be \
                           supported, use it at your own risk!@." nam ver
              end;
            incr provers_found;
            let c = make_command com data.prover_command in
155 156 157
            let key = sanitize_exec com in
            Queue.add key keys;
            Mstr.add key
158 159 160
              {name = data.prover_name;
               version = ver;
               command = c;
MARCHE Claude's avatar
MARCHE Claude committed
161
               driver  = Filename.concat (datadir main) data.prover_driver;
162 163 164 165 166 167 168 169 170 171 172 173
               editor = data.prover_editor} acc
	  with Not_found ->
	    begin
              prover_tips_info := true;
	      eprintf "Warning: found prover %s but name/version not \
                       recognized by regexp `%s'@."
                data.prover_name data.version_regexp;
	      eprintf "Answer was `%s'@." s;
	      acc
	    end)
    acc
    data.execs
174 175 176 177 178 179 180 181
  in
  if Queue.length keys = 1 then
    let key = Queue.take keys in
    let prv = Mstr.find key acc in
    let acc = Mstr.remove key acc in
    Mstr.add data.prover_id prv acc
  else
    acc
182 183 184 185 186 187 188 189

let run_auto_detection config =
  let main = get_main config in
  let l = read_auto_detection_data main in
  let detect = List.fold_left (detect_prover main) Mstr.empty l in
  let length = Mstr.fold (fun _ _ i -> i+1) detect 0 in
  eprintf "%d provers detected.@." length;
  set_provers config detect