install works more or less. make bench still fails on programs

Makefile.in

@@ -36,7 +36,7 @@ datarootdir = @datarootdir@
 
 BINDIR  = $(DESTDIR)@bindir@
 LIBDIR  = $(DESTDIR)@libdir@
-DATADIR = $(DESTDIR)@datadir@
+DATADIR = $(DESTDIR)@datarootdir@
 MANDIR  = $(DESTDIR)@mandir@
 
 # OS specific stuff
@@ -212,6 +212,21 @@ clean::
 	rm -f src/why.cm[iox] src/why.[ao] src/why.cma src/why.cmxa
 	rm -f .depend.lib
 
+###############
+# installation
+###############
+
+install::
+	mkdir -p $(BINDIR)
+	mkdir -p $(LIBDIR)/why3
+	mkdir -p $(DATADIR)/why3/images
+	mkdir -p $(DATADIR)/why3/lang
+	cp -f --parents theories/*.why theories/*/*.why $(DATADIR)/why3/
+	cp -f --parents drivers/*.drv $(DATADIR)/why3/
+	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
+	cp -f share/images/*.png $(DATADIR)/why3/images
+	cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang
+
 ##################
 # Why binary
 ##################
@@ -236,7 +251,6 @@ clean::
 	rm -f bin/why.byte bin/why.opt
 
 install::
-	mkdir -p $(BINDIR)
 	cp -f bin/why.@OCAMLBEST@ $(BINDIR)/why3
 
 ########
@@ -295,8 +309,7 @@ clean::
 	bin/whyml.byte -P alt-ergo $*.mlw
 
 install::
-	mkdir -p $(BINDIR)
-	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/whyml3
+	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/why3ml
 
 ###############
 # IDE
@@ -350,6 +363,9 @@ clean::
 	rm -f bin/whyide.byte bin/whyide.opt
 	rm -f .depend.ide
 
+install::
+	cp -f bin/whyide.@OCAMLBEST@ $(BINDIR)/why3ide
+
 ##############
 # Coq plugin
 ##############
@@ -476,7 +492,6 @@ clean::
 	rm -f bin/why3-cpulimit src/tools/*~
 
 install::
-	mkdir -p $(BINDIR)
 	cp -f bin/why3-cpulimit $(BINDIR)
 
 ########
@@ -533,15 +548,6 @@ testl: bin/whyml.byte
 testl-type: bin/whyml.byte
 	ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
 
-###############
-# installation
-###############
-
-install::
-	mkdir -p $(LIBDIR)/why3
-	cp -f --parents theories/*.why theories/*/*.why $(LIBDIR)/why3/
-	cp -f --parents drivers/*.drv $(LIBDIR)/why3/
-	cp -f why.conf $(LIBDIR)/why3/
 
 ## install: install-binary install-lib install-man
 ##
@@ -846,7 +852,7 @@ src/config.sh: src/config.sh.in config.status
 	./config.status chmod --file $@
 
 src/config.ml: src/config.sh
-	LIBDIR=$(LIBDIR) src/config.sh
+	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
 
 doc/version.tex: doc/version.tex.in config.status
 	./config.status chmod --file $@

src/config.sh.in

@@ -2,10 +2,11 @@
 
 F=src/config.ml
 
-echo "let why_version   = \"@VERSION@\"" > $F
-echo "let why_builddate = \"@BUILDDATE@\"" >> $F
-echo "let why_plugins   = (\"@enable_plugins@\" = \"yes\")" >> $F
-echo "let why_libdir    = \"$LIBDIR/why3\"" >> $F
+echo "let version   = \"@VERSION@\"" > $F
+echo "let builddate = \"@BUILDDATE@\"" >> $F
+echo "let plugins   = (\"@enable_plugins@\" = \"yes\")" >> $F
+echo "let libdir    = \"$LIBDIR/why3\"" >> $F
+echo "let datadir   = \"$DATADIR/why3\"" >> $F
 
 echo "
 module Dynlink_ = struct

src/driver/driver.ml

@@ -50,7 +50,7 @@ type driver = {
 exception NoPlugins
 
 let load_plugin dir (byte,nat) =
-  if not Config.why_plugins then raise NoPlugins;
+  if not Config.plugins then raise NoPlugins;
   let file = if Config.Dynlink.is_native then nat else byte in
   let file = Filename.concat dir file in
   Config.Dynlink.loadfile_private file

src/driver/whyconf.ml

@@ -40,6 +40,23 @@ let error ?loc e = match loc with
   | None -> raise e
   | Some loc -> raise (Loc.Located (loc, e))
 
+(* lib and shared dirs *)
+
+let libdir =
+  try
+    Sys.getenv "WHY3LIB"
+  with Not_found -> Config.libdir
+
+let datadir =
+  try
+    Sys.getenv "WHY3DATA"
+  with Not_found -> Config.datadir
+
+
+
+
+(* conf files *)
+
 let print_rc_value fmt = function
   | Rc.RCint i -> fprintf fmt "%d" i
   | Rc.RCbool b -> fprintf fmt "%B" b
@@ -90,7 +107,9 @@ type config_prover = {
 
 type config = {
   conf_file : string;       (* "/home/innocent_user/.why.conf" *)
+(*
   loadpath  : string list;  (* "/usr/local/share/why/theories" *)
+*)
   timelimit : int option;   (* default prover time limit in seconds *)
   memlimit  : int option;   (* default prover memory limit in megabytes *)
   running_provers_max : int option; (* max number of running prover processes *)
@@ -140,7 +159,10 @@ let load_prover dirname al =
     | "command"     -> set_string key cmd value
     | "driver"      -> set_string key drv value; 
 	               drv := option_map (absolute_filename dirname) !drv
-    | _             -> error (UnknownField key)
+    | _             -> ()
+        (*
+          error (UnknownField key)
+        *)
   in
   List.iter load al;
   { name    = get_field "name" !nam;
@@ -158,11 +180,16 @@ let load_main dirname main al =
     | "timelimit" -> set_int key tl value
     | "memlimit"  -> set_int key ml value
     | "running_provers_max" -> set_int key rp value
-    | _           -> error (UnknownField key)
+    | _           -> ()
+        (*
+          error (UnknownField key)
+        *)
   in
   List.iter load al;
   { main with
+(*
     loadpath  = List.rev !lp;
+*)
     timelimit = !tl;
     memlimit  = !ml;
     running_provers_max = !rp;
@@ -176,7 +203,7 @@ let read_config conf_file =
           if Sys.file_exists ".why.conf" then ".why.conf" else
           let f = Filename.concat (Rc.get_home_dir ()) ".why.conf" in
 	  if Sys.file_exists f then f else
-	  Filename.concat Config.why_libdir "why.conf"
+	  Filename.concat Config.libdir "why.conf"
         end
   in
   let dirname = Filename.dirname filename in
@@ -185,7 +212,9 @@ let read_config conf_file =
   in
   let main = ref {
     conf_file = filename;
+(*
     loadpath  = [];
+*)
     timelimit = None;
     memlimit  = None;
     running_provers_max = None;
@@ -213,7 +242,9 @@ let save_config config =
   let ch = open_out config.conf_file in
   let fmt = Format.formatter_of_out_channel ch in
   fprintf fmt "[main]@\n";
+(*
   List.iter (fprintf fmt "library = \"%s\"@\n") config.loadpath;
+*)
   Util.option_iter (fprintf fmt "timelimit = %d@\n") config.timelimit;
   Util.option_iter (fprintf fmt "memlimit = %d@\n") config.memlimit;
   Util.option_iter (fprintf fmt "running_provers_max = %d@\n") config.running_provers_max;

src/driver/whyconf.mli

@@ -21,6 +21,9 @@
 
 open Util
 
+val libdir : string
+val datadir : string
+
 type config_prover = {
   name    : string;   (* "Alt-Ergo v2.95 (special)" *)
   command : string;   (* "exec why-limit %t %m alt-ergo %f" *)
@@ -29,7 +32,9 @@ type config_prover = {
 
 type config = {
   conf_file : string;       (* "/home/innocent_user/.why.conf" *)
+(*
   loadpath  : string list;  (* "/usr/local/share/why/theories" *)
+*)
   timelimit : int option;   (* default prover time limit in seconds *)
   memlimit  : int option;   (* default prover memory limit in megabytes *)
   running_provers_max : int option; (* max number of running prover processes *)

src/ide/gconfig.ml

@@ -79,8 +79,9 @@ let load_main c (key, value) =
 
 
 let get_prover_data env id name ver c d e = 
+  let f = Filename.concat Whyconf.datadir d in
   try
-    let dr = Driver.load_driver env d in
+    let dr = Driver.load_driver env f in
     { prover_id = id ;
       prover_name = name;
       prover_version = ver;
@@ -89,10 +90,18 @@ let get_prover_data env id name ver c d e =
       driver = dr; 
       editor = e;
     }
-  with _e ->
-    eprintf "Failed to load driver %s for prover %s. prover disabled@."
-      d name;
-    raise Not_found
+  with 
+    | Loc.Located(p,e) ->
+        eprintf "Syntax error %a in driver %s for prover %s (%s).@\nprover disabled@."
+          Loc.report_position p f name (Printexc.to_string e);
+        Printexc.print_backtrace stdout;
+        raise Not_found
+
+    | e ->
+        eprintf "Failed to load driver %s for prover %s (%s).@\nprover disabled@."
+          f name (Printexc.to_string e);
+        Printexc.print_backtrace stdout;
+        raise Not_found
 
 let load_prover env id l =
   let name = ref "?" in
@@ -145,7 +154,7 @@ let read_config env =
 *)
 
 let image ?size f =
-  let n = Filename.concat "" (* todo: libdir *) (Filename.concat "images" (f^".png"))
+  let n = Filename.concat Whyconf.datadir (Filename.concat "images" (f^".png"))
   in
   match size with
     | None ->

src/ide/gmain.ml

@@ -54,17 +54,17 @@ let fname = match !file with
       f
 
 let lang =
-  let load_path = 
-    List.fold_right Filename.concat 
-      [Filename.dirname Sys.argv.(0); ".."; "share"] "lang" 
-  in
+  let load_path = Filename.concat Whyconf.datadir "lang" in
   let languages_manager = 
     GSourceView2.source_language_manager ~default:true 
   in
   languages_manager#set_search_path 
     (load_path :: languages_manager#search_path);
   match languages_manager#language "why" with
-    | None -> Format.eprintf "pas trouv@;"; None
+    | None -> 
+        Format.eprintf "language file for 'why' not found in directory %s@." 
+          load_path; 
+        exit 1
     | Some _ as l -> l
 
 let source_text = 
@@ -75,7 +75,7 @@ let source_text =
   close_in ic;
   buf
 
-let env = Why.Env.create_env (Why.Lexer.retrieve ["theories"])
+let env = Why.Env.create_env (Why.Lexer.retrieve [Filename.concat Whyconf.datadir "theories"])
 
 (********************************)
 (* loading WhyIDE configuration *)

src/main.ml

@@ -89,7 +89,7 @@ let add_opt_meta meta =
 let opt_config = ref None
 let opt_parser = ref None
 let opt_prover = ref None
-let opt_loadpath = ref []
+let opt_loadpath = ref [Filename.concat Whyconf.datadir "theories"]
 let opt_driver = ref None
 let opt_output = ref None
 let opt_timelimit = ref None
@@ -289,14 +289,18 @@ let () =
       (eprintf "No config file found (required by '-P %s').@.") !opt_prover;
     if !opt_config <> None || !opt_prover <> None then exit 1;
     { conf_file = "";
+(*
       loadpath  = [];
+*)
       timelimit = None;
       memlimit  = None;
       running_provers_max = None;
       provers   = Mstr.empty }
   in
 
+(*
   opt_loadpath := List.rev_append !opt_loadpath config.loadpath;
+*)
   if !opt_timelimit = None then opt_timelimit := config.timelimit;
   if !opt_memlimit  = None then opt_memlimit  := config.memlimit;
   begin match !opt_prover with