autodetection.ml 6.61 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 19 20 21 22 23 24
(*    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

25
let debug = Debug.register_flag "autodetect"
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 73

(* 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 =
74 75
  let filename = Filename.concat (Whyconf.datadir main)
    "provers-detection-data.conf" in
76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
  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

101 102 103 104 105 106 107 108 109 110 111
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

112
let detect_prover main acc0 data =
113 114
  let keys = Queue.create () in
  let acc = List.fold_left
115 116 117
    (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
118
	let c = sprintf "(%s) > %s 2>&1" cmd out in
119
        Debug.dprintf debug "Run : %s@." c;
120 121 122
	let ret = Sys.command c in
	if ret <> 0 then
	  begin
123
	    Debug.dprintf debug "command '%s' failed@." cmd;
124 125 126 127 128 129
	    acc
	  end
	else
	  let s =
            try
              let ch = open_in out in
MARCHE Claude's avatar
MARCHE Claude committed
130 131 132 133
              let c = Sysutil.channel_contents ch in
              close_in ch;
	      Sys.remove out;
              c
134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155
            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
156 157 158
            let key = sanitize_exec com in
            Queue.add key keys;
            Mstr.add key
159 160 161
              {name = data.prover_name;
               version = ver;
               command = c;
MARCHE Claude's avatar
MARCHE Claude committed
162
               driver  = Filename.concat (datadir main) data.prover_driver;
163 164 165 166 167 168 169 170 171 172
               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)
173
    acc0
174
    data.execs
175
  in
176 177 178 179 180 181 182 183 184 185 186
  let acc = 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 in
  (** If the accumulator has not been touched we warn
      that we don't find the prover *)
  if acc == acc0 then eprintf "Prover %s not found.@." data.prover_name;
  acc
187 188 189 190 191

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
François Bobot's avatar
François Bobot committed
192
  let length = Mstr.cardinal detect in
193 194
  eprintf "%d provers detected.@." length;
  set_provers config detect