localdir in configure, datadir used for theories and drivers,\n symbolic link...

localdir in configure, datadir used for theories and drivers,\n symbolic link in build directory before instead of moving directory

configure.in

@@ -59,6 +59,13 @@ AC_ARG_ENABLE(verbose-make,
     [  --enable-verbose-make   verbose makefile commands],,
     enable_verbose_make=no)
 
+# LOCAL_CONF
+
+AC_ARG_ENABLE(local,
+    [  --enable-local            use only WHY3 in the build directory],,
+    ENABLE_LOCAL=no)
+
+
 # IDE
 
 AC_ARG_ENABLE(ide,
@@ -291,6 +298,13 @@ if test "$enable_hypothesis_selection" = yes; then
   AC_CHECK_FILE($OCAMLLIB/ocamlgraph/,enable_hypothesis_selection=yes,enable_hypothesis_selection=no)
 fi
 
+if test "$ENABLE_LOCAL" = no; then
+   LOCALDIR=None
+else
+   LOCALDIR='Some \"$PWD\"'
+   ENABLE_LOCAL=yes
+fi
+
 #Viewer for ps and pdf
 dnl AC_CHECK_PROGS(PSVIEWER,gv evince)
 dnl AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince)
@@ -342,6 +356,8 @@ AC_SUBST(enable_menhirlib)
 
 AC_SUBST(enable_hypothesis_selection)
 
+AC_SUBST(LOCALDIR)
+
 dnl AC_SUBST(PSVIEWER)
 dnl AC_SUBST(PDFVIEWER)
 
@@ -374,4 +390,4 @@ echo "TPTP parser             : $enable_whytptp"
 echo "Menhir library          : $enable_menhirlib"
 echo "hypothesis selection    : $enable_hypothesis_selection"
 echo "profiling               : $ENABLE_PROFILING"
-
+echo "localdir                : $ENABLE_LOCAL"

share/drivers

+../drivers
\ No newline at end of file

share/theories

+../theories
\ No newline at end of file

src/config.sh.in

@@ -7,6 +7,7 @@ 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 "let localdir = @LOCALDIR@" >> $F
 
 echo "
 module Dynlink_ = struct

src/config/whyconfig.ml

@@ -66,4 +66,5 @@ let () =
     if !auto
     then Autodetection.run_auto_detection config
     else config in
+  printf "Save config to %s@." (get_conf_file config);
   save_config config

src/driver/autodetection.ml

@@ -144,7 +144,7 @@ let detect_prover main acc data =
               {name = data.prover_name;
                version = ver;
                command = c;
-               driver  = Filename.concat main.libdir data.prover_driver;
+               driver  = Filename.concat main.datadir data.prover_driver;
                editor = data.prover_editor} acc
 	  with Not_found ->
 	    begin

src/driver/whyconf.ml

@@ -26,12 +26,18 @@ open Rc
 let libdir =
   try
     Sys.getenv "WHY3LIB"
-  with Not_found -> Config.libdir
+  with Not_found -> default_option Config.libdir Config.localdir
 
 let datadir =
   try
     Sys.getenv "WHY3DATA"
-  with Not_found -> Config.datadir
+  with Not_found -> option_apply Config.datadir
+    (fun d -> Filename.concat d "share") Config.localdir
+
+let default_conf_file =
+  Filename.concat  (match Config.localdir with
+    | None -> Rc.get_home_dir ()
+    | Some d -> d) ".why.conf"
 
 (* Configuration file *)
 
@@ -63,7 +69,7 @@ let default_main =
   {
     libdir = libdir;
     datadir = datadir;
-    loadpath = [Filename.concat libdir "theories"];
+    loadpath = [Filename.concat datadir "theories"];
     timelimit = 10;
     memlimit = 0;
     running_provers_max = 2;
@@ -128,8 +134,8 @@ let read_config_rc conf_file =
     | None -> begin try Sys.getenv "WHY_CONFIG" with Not_found ->
           if Sys.file_exists "why.conf" then "why.conf" else
           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 raise Exit
+          if Sys.file_exists default_conf_file then default_conf_file
+          else raise Exit
         end
   in
   filename,Rc.from_file filename
@@ -154,8 +160,7 @@ let default_config conf_file = get_config (conf_file,Rc.empty)
 
 let read_config conf_file =
   let filenamerc = try read_config_rc conf_file
-    with Exit ->
-      (Filename.concat (Rc.get_home_dir ()) ".why.conf",Rc.empty) in
+    with Exit -> (default_conf_file,Rc.empty) in
   get_config filenamerc
 
 
@@ -177,6 +182,7 @@ let set_provers config provers =
   }
 
 let set_conf_file config conf_file = {config with conf_file = conf_file}
+let get_conf_file config           =  config.conf_file
 
 let get_section config name = assert (name <> "main");
   get_section config.config name

src/driver/whyconf.mli

@@ -60,6 +60,7 @@ val set_main    : config -> main                 -> config
 val set_provers : config -> config_prover Mstr.t -> config
 
 val set_conf_file : config -> string -> config
+val get_conf_file : config -> string
 
 val get_section : config -> string -> Rc.section option
 val get_family  : config -> string -> Rc.family