autodetect.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(*  Copyright (C) 2022                                                    *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  You can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It 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. See the          *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Base

let null = if Caml.Sys.unix then "/dev/null" else "NUL"

let rec lookup_file dirs filename =
  match dirs with
  | [] -> raise Caml.Not_found
  | dir :: dirs ->
    let file = Caml.Filename.concat dir filename in
    if Caml.Sys.file_exists file then file else lookup_file dirs filename

let autodetection ?(debug = false) () =
  if debug then Debug.set_flag Autodetection.debug;
  let caisar_conf =
    lookup_file Dirs.Sites.config "caisar-detection-data.conf"
  in
  let data = Autodetection.Prover_autodetection_data.from_file caisar_conf in
  let provers = Autodetection.find_provers data in
  let provers =
    List.fold_left ~init:[] provers ~f:(fun acc (path, name, version) ->
      {
        Autodetection.Partial.name;
        path;
        version;
        shortcut = None;
        manual = false;
      }
      :: acc)
  in
  let config = Whyconf.init_config (Some null) in
  let provers = Autodetection.compute_builtin_prover provers config data in
  Whyconf.set_provers config provers