Check compatibility of compile-time prover support

Signed-off-by: Claude Marche <Claude.Marche@inria.fr>

configure.in

@@ -444,6 +444,9 @@ fi
 if test "$enable_coq_support" = no; then
    enable_coq_tactic=no
    enable_coq_libs=no
+   COMPILETIMECOQ=
+else
+   COMPILETIMECOQ="\\\"Coq\\\", \\\"$COQVERSION\\\"; "
 fi
 
 if test "$enable_coq_tactic" = yes; then
@@ -519,6 +522,9 @@ fi
 
 if test "$enable_pvs_support" = no; then
    enable_pvs_libs=no
+   COMPILETIMEPVS=
+else
+   COMPILETIMEPVS="\\\"PVS\\\", \\\"$PVSVERSION\\\"; "
 fi
 
 if test "$enable_pvs_libs" = yes; then
@@ -641,10 +647,12 @@ AC_SUBST(COQC)
 AC_SUBST(COQDEP)
 AC_SUBST(COQLIB)
 AC_SUBST(COQVERSION)
+AC_SUBST(COMPILETIMECOQ)
 
 AC_SUBST(enable_pvs_libs)
 AC_SUBST(PVS)
 AC_SUBST(PVSVERSION)
+AC_SUBST(COMPILETIMEPVS)
 
 AC_SUBST(enable_hypothesis_selection)
 

share/provers-detection-data.conf

@@ -398,6 +398,7 @@ driver = "drivers/mathematica.drv"
 
 [ITP coq]
 name = "Coq"
+compile_time_support = true
 exec = "coqtop -batch"
 version_switch = "-v"
 version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
@@ -410,6 +411,7 @@ editor = "coqide"
 
 [ITP coq]
 name = "Coq"
+compile_time_support = true
 exec = "coqtop -batch"
 version_switch = "-v"
 version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
@@ -424,6 +426,7 @@ editor = "coqide"
 
 [ITP pvs]
 name = "PVS"
+compile_time_support = true
 exec = "pvs"
 version_switch = "-version"
 version_regexp = "PVS Version \\([^ \n]+\\)"

src/config.sh.in

@@ -25,4 +25,6 @@ let builddate = \"@BUILDDATE@\"
 let libdir    = $libdir
 let datadir   = $datadir
 let localdir  = $localdir
+
+let compile_time_support = [ @COMPILETIMECOQ@ @COMPILETIMEPVS@ ]
 " > $config

src/driver/autodetection.ml

@@ -57,6 +57,7 @@ type prover_autodetection_data =
       prover_id : string;
       prover_name : string;
       prover_altern : string;
+      compile_time_support : bool;
       execs : string list;
       version_switch : string;
       version_regexp : string;
@@ -74,7 +75,8 @@ type prover_autodetection_data =
 let prover_keys =
   let add acc k = Sstr.add k acc in
   List.fold_left add Sstr.empty
-    ["name";"exec";"version_switch";"version_regexp";
+    ["name";"compile_time_support";
+     "exec";"version_switch";"version_regexp";
      "version_ok";"version_old";"version_bad";"command";
      "editor";"driver";"in_place";"message";"alternative";]
 
@@ -85,6 +87,8 @@ let load_prover kind (id,section) =
     prover_id = id;
     prover_name = get_string section "name";
     prover_altern = get_string section ~default:"" "alternative";
+    compile_time_support = 
+      get_bool section ~default:false "compile_time_support";
     execs = get_stringl section "exec";
     version_switch = get_string section ~default:"" "version_switch";
     version_regexp = get_string section ~default:"" "version_regexp";
@@ -329,7 +333,31 @@ let detect_exec env main data acc exec_name =
   let bad = List.exists (check_version ver) data.versions_bad in
   if bad then (known_version env exec_name; acc)
   else
-
+    (* check if this prover needs compile-time support *)
+    let missing_compile_time_support =
+      if data.compile_time_support then
+        try 
+          let compile_time_ver =
+            List.assoc data.prover_name Config.compile_time_support 
+          in 
+          if compile_time_ver <> ver then begin
+            eprintf 
+              "Found prover %s version %s, but Why3 was compiled with support for version %s@."
+            data.prover_name ver compile_time_ver;
+            true
+          end
+          else
+            false
+        with Not_found ->
+          eprintf 
+            "Found prover %s version %s, but Why3 wasn't compiled with support for it@."
+            data.prover_name ver;
+          true
+      else false
+    in
+    if missing_compile_time_support then
+      (known_version env exec_name; acc)
+    else
     let good = List.exists (check_version ver) data.versions_ok in
     let old  = List.exists (check_version ver) data.versions_old in
     match data.prover_command with