configure: coq plugin detection; timelimit and memlimit now optional arguments; coq-plugin update

Makefile.in

@@ -338,21 +338,24 @@ clean::
 ##############
 
 ifeq (@enable_coq_support@,yes)
-#byte: src/coq-plugin/whytac.cmo
-#opt:  src/coq-plugin/whytac.cmxs
+byte: src/coq-plugin/whytac.cma
+opt:  src/coq-plugin/whytac.cmxs
 endif
 
 COQTREES = kernel lib interp parsing proofs pretyping tactics library
 
-#src/coq-plugin/whytac.cmo:  INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES))
+src/coq-plugin/whytac.cma:  INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES))
 src/coq-plugin/whytac.cmxs: INCLUDES = $(addprefix -I @COQLIB@/, $(COQTREES))
 
-#src/coq-plugin/whytac.cmo:  BFLAGS+=-rectypes
+src/coq-plugin/whytac.cma:  BFLAGS+=-rectypes
 src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes
 
 src/coq-plugin/whytac.cmxs: src/why.cmxa src/coq-plugin/whytac.ml
 	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
 
+src/coq-plugin/whytac.cma: src/why.cma src/coq-plugin/whytac.ml
+	$(OCAMLC) -a $(BFLAGS) -o $@ $^
+
 #######
 # tools
 #######

configure.in

@@ -225,17 +225,13 @@ else
         enable_coq_support=no
         AC_MSG_WARN(Cannot find coqc.)
     else
-        enable_coq_support=yes
-        AC_CHECK_PROG(COQDEP,coqdep,coqdep,true)
-        if test "$COQDEP" = true ; then
-	   AC_MSG_ERROR(Cannot find coqdep.)
-        fi
         COQLIB=`$COQC -where | sed -e 's|\\\|/|g' -e 's| |\\ |g'`
         AC_MSG_CHECKING(Coq version)
         COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
 
         case $COQVERSION in
           8.*|trunk)
+	        enable_coq_support=yes
                 AC_MSG_RESULT($COQVERSION);;
           *)
                 enable_coq_support=no
@@ -243,6 +239,9 @@ else
         esac
     fi
 fi
+if test "$enable_coq_support" = yes; then
+   AC_CHECK_FILE($COQLIB/kernel/term.cmi,,enable_coq_support=no)
+fi
 
 #Viewer for ps and pdf
 dnl AC_CHECK_PROGS(PSVIEWER,gv evince)

src/coq-plugin/whytac.ml

@@ -14,26 +14,25 @@ open Pp
 
 open Why
 open Call_provers
+open Whyconf
 
 let debug = 
   try let _ = Sys.getenv "WHYDEBUG" in true
   with Not_found -> false
 
-let loadpath = 
-  try Str.split (Str.regexp ":") (Sys.getenv "WHYLOADPATH")
-  with Not_found -> ["theories"]
+let config = Whyconf.read_config None
 
-let env = Env.create_env (Typing.retrieve loadpath)
+let env = Env.create_env (Typing.retrieve config.loadpath)
     
-let timeout = 
-  try int_of_string (Sys.getenv "WHYTIMEOUT")
-  with Not_found -> 2
+let config_prover = 
+  try Util.Mstr.find "alt-ergo" config.provers 
+  with Not_found -> assert false
 
-let drv =
-  let filename = 
-    try Sys.getenv "WHYDRIVER" with Not_found -> "drivers/alt_ergo.drv"
-  in
-  Driver.load_driver env filename
+let drv = Driver.load_driver env config_prover.driver
+let command = config_prover.command
+let timelimit = match config.timelimit with
+  | None -> 3
+  | Some t -> t
 
 (* Coq constants *)
 let logic_dir = ["Coq";"Logic";"Decidable"]
@@ -336,7 +335,9 @@ and tr_global_ts env r =
 	  in
 	  let decl = Array.mapi make_one mib.mind_packets in
 	  let decl = Array.to_list decl in
-	  task := Task.add_ty_decl !task decl;
+	  let decl = Decl.create_ty_decl decl in
+	  Format.printf "decl = %a@." Pretty.print_decl decl;
+	  task := Task.add_decl !task decl;
 	  lookup_global global_ts r
 
 (* assumption: t:T:Set *)
@@ -563,11 +564,8 @@ let whytac gl =
   try
     tr_goal gl;
     if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
-    let tasks = Driver.apply_transforms drv !task in
-    assert (List.length tasks = 1);
-    let task = List.hd tasks in
-    if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) task;
-    let res = Driver.call_prover ~debug ~timeout drv task in
+    if debug then Format.printf "@[%a@]@\n---@." (Prover.print_task drv) !task;
+    let res = Prover.prove_task ~debug ~command ~timelimit drv !task () in
     match res.pr_answer with
       | Valid -> Tactics.admit_as_an_axiom gl
       | Invalid -> error "Invalid"
@@ -575,7 +573,7 @@ let whytac gl =
       | Failure s -> error ("Failure: " ^ s)
       | Timeout -> error "Timeout"
       | HighFailure -> 
-	  error ("Prover failure\n" ^ res.pr_stdout ^ "\n" ^ res.pr_stderr)
+	  error ("Prover failure\n" ^ res.pr_output ^ "\n")
   with NotFO ->
     error "Not a first order goal"
 

src/driver/call_provers.ml

@@ -69,7 +69,7 @@ let call_prover debug command opt_cout buffer =
   if debug then eprintf "Call_provers: prover output:@\n%s@." out;
   ret, out, time
 
-let call_on_buffer ?(debug=false) ~command ~timelimit ~memlimit
+let call_on_buffer ?(debug=false) ~command ?(timelimit=0) ?(memlimit=0)
                                   ~regexps ~exitcodes ~filename buffer () =
   let on_stdin = ref true in
   let on_timelimit = ref false in

src/driver/call_provers.mli

@@ -54,8 +54,8 @@ val print_prover_result : Format.formatter -> prover_result -> unit
 val call_on_buffer :
   ?debug    : bool ->
   command   : string ->
-  timelimit : int ->
-  memlimit  : int ->
+  ?timelimit : int ->
+  ?memlimit  : int ->
   regexps   : (Str.regexp * prover_answer) list ->
   exitcodes : (int * prover_answer) list ->
   filename  : string ->

src/driver/driver.ml

@@ -377,12 +377,12 @@ let get_filename drv input_file theory_name goal_name =
 let file_of_task drv input_file theory_name task =
   get_filename drv input_file theory_name (task_goal task).pr_name.id_short
 
-let call_on_buffer ?debug ~command ~timelimit ~memlimit drv buffer =
+let call_on_buffer ?debug ~command ?timelimit ?memlimit drv buffer =
   let regexps = drv.drv_regexps in
   let exitcodes = drv.drv_exitcodes in
   let filename = get_filename drv "" "" "" in
   Call_provers.call_on_buffer
-    ?debug ~command ~timelimit ~memlimit ~regexps ~exitcodes ~filename buffer
+    ?debug ~command ?timelimit ?memlimit ~regexps ~exitcodes ~filename buffer
 
 (*
 Local Variables:

src/driver/driver.mli

@@ -66,8 +66,8 @@ val file_of_task : driver -> string -> string -> task -> string
 val call_on_buffer :
   ?debug    : bool ->
   command   : string ->
-  timelimit : int ->
-  memlimit  : int ->
+  ?timelimit : int ->
+  ?memlimit  : int ->
   driver -> Buffer.t -> unit -> Call_provers.prover_result
 
 (** {2 syntax arguments} *)

src/driver/prover.ml

@@ -65,9 +65,9 @@ let print_task drv fmt task =
   let printer = printer (driver_query drv task) in
   fprintf fmt "@[%a@]@?" printer task
 
-let prove_task ?debug ~command ~timelimit ~memlimit drv task =
+let prove_task ?debug ~command ?timelimit ?memlimit drv task =
   let buf = Buffer.create 1024 in
   let fmt = formatter_of_buffer buf in
   print_task drv fmt task; pp_print_flush fmt ();
-  call_on_buffer ?debug ~command ~timelimit ~memlimit drv buf
+  call_on_buffer ?debug ~command ?timelimit ?memlimit drv buf
 

src/driver/prover.mli

@@ -24,8 +24,8 @@ val print_task : Driver.driver -> Format.formatter -> Task.task -> unit
 val prove_task :
   ?debug    : bool ->
   command   : string ->
-  timelimit : int ->
-  memlimit  : int ->
+  ?timelimit : int ->
+  ?memlimit  : int ->
   Driver.driver -> Task.task -> unit -> Call_provers.prover_result
 
 (** {2 error reporting} *)