"towards a distribution of matita" changes:

- @USER_HOME@, @USER_NAME@ no longer hard coded at configure time
- added support for tilde expansion in configuration file
- added support for runtime overriding of RT_BASE_DIR
- better configure.ac, can now configure RT_BASE_DIR, debugging, and distribution defaults

diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in
index 85418121f93a8785699b982adfce99a676bc27fb..abb1aff4e172da754281dedbe0ff03589595f066 100644 (file)
--- a/helm/matita/buildTimeConf.ml.in
+++ b/helm/matita/buildTimeConf.ml.in
@@ -24,7 +24,7 @@
  *)
 
 let debug = @DEBUG@;;
-let version = "0.0.1";;
+let version = "@MATITA_VERSION";;
 let undo_history_size = 10;;
 let console_history_size = 100;;
 let browser_history_size = 100;;
@@ -34,7 +34,13 @@ let blank_uri = "about:blank";;
 let current_proof_uri = "about:current_proof";;
 let default_font_size = 10;;
 let script_font = "Monospace";;
-let runtime_base_dir = "@RT_BASE_DIR@";;
+
+  (** may be overridden with MATITA_RT_BASE_DIR environment variable, useful for
+   * binary distribution installed in user home directories *)
+let runtime_base_dir =
+  try
+    Sys.getenv "MATITA_RT_BASE_DIR"
+  with Not_found -> "@RT_BASE_DIR@";;
 
 let images_dir = runtime_base_dir ^ "/icons"
 let gtkrc_file = runtime_base_dir ^ "/matita.gtkrc"
@@ -45,6 +51,5 @@ let coq_notation_script = runtime_base_dir ^ "/coq.moo"
 let matita_conf  = runtime_base_dir ^ "/matita.conf.xml"
 let closed_xml = runtime_base_dir ^ "/closed.xml"
 let gtkmathview_conf = runtime_base_dir ^ "/gtkmathview.matita.conf.xml"
-
 let matitamake_makefile_template = runtime_base_dir ^ "/template_makefile.in"
 

diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac
index 4f8c991d1082d380e1fd4fe6bdcd089360e5d87e..d20bf2192224b1bd79463cfb5ce12c69c9bdf8fa 100644 (file)
--- a/helm/matita/configure.ac
+++ b/helm/matita/configure.ac
@@ -1,5 +1,11 @@
 AC_INIT(matitaTypes.ml)
 
+# Distribution settings (i.e. settings to be manipulated before a release)
+DEBUG_DEFAULT="true"
+RT_BASE_DIR_DEFAULT="`pwd`"
+MATITA_VERSION="0.0.1"
+# End of distribution settings
+
 AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no)
 if test $HAVE_OCAMLC = "no"; then
   AC_MSG_ERROR(could not find ocamlc)
@@ -87,21 +93,31 @@ OCAMLFIND_COMMANDS=""
 if test "$OCAMLFIND_COMMANDS" != ""; then
   OCAMLFIND="OCAMLFIND_COMMANDS='$OCAMLFIND_COMMANDS' $OCAMLFIND"
 fi
+
+AC_MSG_CHECKING(--enable-debug argument)
 AC_ARG_ENABLE(debug,
-  [  --enable-debug    Turn on debugging],
-  [case "${enableval}" in
+  [  --enable-debug    Turn on debugging],
+  [GIVEN="yes";
+   case "${enableval}" in
    yes) DEBUG=true ;;
    no)  DEBUG=false ;;
    *) AC_MSG_ERROR(bad value ${enableval} for --enable-debug) ;;
   esac],
-  [DEBUG=true])
+  [GIVEN="no"; DEBUG="$DEBUG_DEFAULT"])
+MSG=$GIVEN
 if test "$DEBUG" = "true"; then
-  echo "debugging enabled"
+  MSG="$MSG, debugging enabled."
+else
+  MSG="$MSG, debugging disabled."
 fi
+AC_MSG_RESULT($MSG)
 
-RT_BASE_DIR=`pwd`
-USER_HOME=`pwd` #should be `echo $HOME`
-USER_NAME=`echo $USER`
+AC_MSG_CHECKING(--with-runtime-dir argument)
+AC_ARG_WITH(runtime-dir,
+  [ --with-runtime-dir Runtime directory (current working directory if not given)],
+  [ RT_BASE_DIR="${withval}" ],
+  [ RT_BASE_DIR="$RT_BASE_DIR_DEFAULT" ])
+AC_MSG_RESULT($RT_BASE_DIR)
 
 AC_SUBST(CAMLP4O)
 AC_SUBST(DEBUG)
@@ -115,8 +131,7 @@ AC_SUBST(HAVE_OCAMLOPT)
 AC_SUBST(LABLGLADECC)
 AC_SUBST(OCAMLFIND)
 AC_SUBST(RT_BASE_DIR)
-AC_SUBST(USER_HOME)
-AC_SUBST(USER_NAME)
+AC_SUBST(MATITA_VERSION)
 
 AC_OUTPUT([
   matita.conf.xml.sample

diff --git a/helm/matita/matita.conf.xml.sample.in b/helm/matita/matita.conf.xml.sample.in
index 0087d604fcc289a79fd23f75e7789835179581e9..b932b7ca9c54f8c61852d991952cf1aea27584a5 100644 (file)
--- a/helm/matita/matita.conf.xml.sample.in
+++ b/helm/matita/matita.conf.xml.sample.in
@@ -1,11 +1,16 @@
 <?xml version="1.0" encoding="utf-8"?>
 <helm_registry>
+  <section name="user">
+    <key name="home">~</key>
+<!-- If not specified here, name of the user executing matita will be used -->
+<!--     <key name="name">foo</key> -->
+  </section>
   <section name="matita">
     <key name="auto_disambiguation">true</key>
     <key name="environment_trust">true</key>
     <key name="baseuri">cic:/matita/</key>
-    <key name="basedir">@USER_HOME@/.matita</key>
-    <key name="owner">@USER_NAME@</key>
+    <key name="basedir">$(user.home)/.matita</key>
+    <key name="owner">$(user.name)</key>
 <!--     <key name="font_size">10</key> -->
     <key name="tactics_bar">false</key>
   </section>
@@ -16,7 +21,7 @@
     <key name="database">matita</key>
   </section>
   <section name="getter">
-    <key name="cache_dir">@USER_HOME@/.matita/getter/cache</key>
+    <key name="cache_dir">$(user.home)/.matita/getter/cache</key>
     <key name="dtd_dir">/projects/helm/xml/dtd</key>
     <key name="prefix">
       cic:/
@@ -24,7 +29,7 @@
     </key>
     <key name="prefix">
       cic:/matita/
-      file://@USER_HOME@/.matita/xml/matita/
+      file://$(user.home)/.matita/xml/matita/
     </key>
   </section>
 </helm_registry>

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index dd8d6d83dad6a115d6e13540a44fc128ca8c0cb7..da09fb27dbea99945d407ad9003bdf7e64efccd3 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -121,10 +121,6 @@ let _ =
     addDebugItem "print selections" (fun () ->
       let cicMathView = MatitaMathView.cicMathView_instance () in
       List.iter MatitaLog.debug (cicMathView#string_of_selections));
-    addDebugItem "dump getter settings" (fun _ ->
-      prerr_endline (Http_getter_env.env_to_string ()));
-    addDebugItem "getter: getalluris" (fun _ ->
-      List.iter prerr_endline (Http_getter.getalluris ()));
     addDebugItem "dump script status" script#dump;
     addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
       Helm_registry.save_to "./foo.conf.xml");
@@ -168,6 +164,9 @@ let _ =
       (fun _ ->
          let nb = gui#main#hintNotebook in
          nb#goto_page ((nb#current_page + 1) mod 3));
+    addDebugItem "print runtime dir"
+      (fun _ ->
+        prerr_endline BuildTimeConf.runtime_base_dir);
   end
   (** Debugging }}} *)
 

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index 9ea9e07d2670d89729b3b9fe5eafbbc9487a928f..1e9ebe2dd2b2eb539ea7096816fd3a131ba1578b 100644 (file)
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -40,10 +40,21 @@ let wants s l =
 let already_configured s l =
   List.for_all (fun item -> List.exists (fun x -> x = item) l) s
   
+let tilde_expand_key k =
+  try
+    Helm_registry.set k (HExtlib.tilde_expand (Helm_registry.get k))
+  with Helm_registry.Key_not_found _ -> ()
+
 let load_configuration init_status =
   if not (already_configured [ConfigurationFile] init_status) then
     begin
       Helm_registry.load_from BuildTimeConf.matita_conf;
+      if not (Helm_registry.has "user.name") then begin
+        let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in
+        Helm_registry.set "user.name" login
+      end;
+      tilde_expand_key "matita.basedir";
+      tilde_expand_key "user.home";
       ConfigurationFile::init_status 
     end
   else

diff --git a/helm/matita/matitamake.ml b/helm/matita/matitamake.ml
index 46b194bda7126bb207cd58f66a88565919e4a879..96fdbfb28ef0727451dc5dd51d2f3617121cbf95 100644 (file)
--- a/helm/matita/matitamake.ml
+++ b/helm/matita/matitamake.ml
@@ -26,7 +26,7 @@
 module MK = MatitamakeLib ;;
 
 let main () =
-  Helm_registry.load_from BuildTimeConf.matita_conf;
+  MatitaInit.load_configuration_file ();
   MK.initialize ();
   let usage = ref (fun () -> ()) in
   let dev_of_name name =