release work snapshot ...

diff --git a/helm/Makefile b/helm/Makefile
index 21012fe0eecf55436a46698d32d6f8c4e0808646..de2a403c12d124d0cfc160bcea8b78f0da343f95 100644 (file)
--- a/helm/Makefile
+++ b/helm/Makefile
@@ -16,6 +16,10 @@ clean.%:
        $(MAKE) -C $* clean
 distclean.%:
        $(MAKE) -C $* distclean
+install.%:
+       $(MAKE) -C $* install
+uninstall.%:
+       $(MAKE) -C $* uninstall
 
 BASENAME = matita
 NULL =

diff --git a/helm/Makefile.defs.in b/helm/Makefile.defs.in
index b36ba3126c9473d4fdb0f32cac411162c5489ae1..d466f70cbe34c64b3d02994c5771eaa01e73f6f8 100644 (file)
--- a/helm/Makefile.defs.in
+++ b/helm/Makefile.defs.in
@@ -7,3 +7,5 @@ MATITA_REQUIRES = @FINDLIB_REQUIRES@
 MATITA_CREQUIRES = @FINDLIB_CREQUIRES@
 
 MATITA_VERSION = @MATITA_VERSION@
+
+RT_BASE_DIR = @RT_BASE_DIR@

diff --git a/helm/libs b/helm/libs
new file mode 120000 (symlink)
index 0000000..5074bc2
--- /dev/null
+++ b/helm/libs
@@ -0,0 +1 @@
+ocaml/
\ No newline at end of file

diff --git a/helm/matita/Makefile b/helm/matita/Makefile
index 3f65ab53860377761d05c75c21b19c2bafd806e6..40a4b2014b97dbfb09ace795ac569d362fb3c1ea 100644 (file)
--- a/helm/matita/Makefile
+++ b/helm/matita/Makefile
@@ -190,6 +190,32 @@ cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt)
 
 # {{{ Distribution stuff
 
+stdlib:
+       $(MAKE) MATITA_FLAGS="-system" -C library/
+
+DEST = @RT_BASE_DIR@
+INSTALL_STUFF =                        \
+       icons/                          \
+       matita.gtkrc                    \
+       matita.lang                     \
+       matita.ma.templ                 \
+       core_notation.moo               \
+       matita.conf.xml                 \
+       closed.xml                      \
+       gtkmathview.matita.conf.xml     \
+       template_makefile.in            \
+       library/                        \
+       $(PROGRAMS_BYTE)                \
+       $(NULL)
+ifeq ($(HAVE_OCAMLOPT),yes)
+INSTALL_STUFF += $(PROGRAMS_OPT)
+endif
+
+install:
+       install -d $(DEST)
+       cp -a $(INSTALL_STUFF) $(DEST)
+uninstall:
+
 STATIC_LINK = dist/static_link/static_link
 # for matita
 STATIC_LIBS =  \

diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in
index debafe00397bbb39e8751ccc66cf1dfb8e11bb05..8ea2c7b869cf03a70d7b9004fb2f279e3cbb1b3f 100644 (file)
--- a/helm/matita/buildTimeConf.ml.in
+++ b/helm/matita/buildTimeConf.ml.in
@@ -47,7 +47,6 @@ let gtkrc_file = runtime_base_dir ^ "/matita.gtkrc"
 let lang_file  = runtime_base_dir ^ "/matita.lang"
 let script_template  = runtime_base_dir ^ "/matita.ma.templ"
 let core_notation_script = runtime_base_dir ^ "/core_notation.moo"
-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"

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index fec223b006c2f7fc99b8cda7adb4b4f0689ae53f..8223416e4dd7d632846e7963927bef57e700948e 100644 (file)
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -56,6 +56,10 @@ let load_configuration init_status =
         Helm_registry.set "user.name" login
       end;
       tilde_expand_key "matita.basedir";
+      if Helm_registry.get_bool "matita.system" then begin
+        prerr_endline "SISTEMA";
+        Helm_registry.set "user.home" BuildTimeConf.runtime_base_dir;
+      end;
       tilde_expand_key "user.home";
       ConfigurationFile::init_status 
     end
@@ -66,7 +70,8 @@ let initialize_db init_status =
   wants [ ConfigurationFile; CmdLine ] init_status;
   if not (already_configured [ Db ] init_status) then
     begin
-      MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+      if not (Helm_registry.get_bool "matita.system") then
+        MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
       LibraryDb.create_owner_environment ();
       Db::init_status
     end
@@ -143,6 +148,7 @@ let usage () =
 let registry_defaults =
   [
     "db.nodb",                  "false";
+    "matita.system",            "false";
     "matita.debug",             "false";
     "matita.external_editor",   "gvim -f -c 'go %p' %f";
     "matita.preserve",          "false";
@@ -169,8 +175,12 @@ let parse_cmdline init_status =
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
           "Turns off automatic baseuri cleaning";
         "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true),
-              ("Avoid using external database connection "
-               ^ "(WARNING: disable many features)");
+            ("Avoid using external database connection "
+             ^ "(WARNING: disable many features)");
+        "-system", Arg.Unit (fun () ->
+              Helm_registry.set_bool "matita.system" true),
+            ("Act on the system library instead of the user one"
+             ^ "(WARNING: not for the casual user)");
         "-noprofile", 
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
           "Turns off profiling printings";

diff --git a/helm/ocaml/Makefile b/helm/ocaml/Makefile
index 0d1867293bdb3b1687a60a8d6844d1199ac916b1..4558a011cb2b22fb99740be45c612492d3ef2683 100644 (file)
--- a/helm/ocaml/Makefile
+++ b/helm/ocaml/Makefile
@@ -76,6 +76,10 @@ distclean: clean clean_metas
        $(MAKE) -C $* depend 
 %.stats:
        @$(MAKE) -C $* .stats
+%.install:
+       $(MAKE) -C $* install 
+%.uninstall:
+       $(MAKE) -C $* uninstall 
 
 METAS/META.helm-%: METAS/meta.helm-%.src
        cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@

diff --git a/helm/ocaml/Makefile.common b/helm/ocaml/Makefile.common
index 1a8b029f97a626e0dbd0632f091b28ffa13be444..9feae4f8685cfbf825955da7bee37e8bb06f13b9 100644 (file)
--- a/helm/ocaml/Makefile.common
+++ b/helm/ocaml/Makefile.common
@@ -67,6 +67,8 @@ test: test.ml $(ARCHIVE)
        $(OCAMLC) $(ARCHIVE) -linkpkg -o $@ $<
 test.opt: test.ml $(ARCHIVE_OPT)
        $(OCAMLOPT) $(ARCHIVE_OPT) -linkpkg -o $@ $<
+install:
+uninstall:
 
 depend: $(DEPEND_FILES)
        $(OCAMLDEP) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend

diff --git a/helm/ocaml/registry/.ocamlinit b/helm/ocaml/registry/.ocamlinit
index 9aee6008e6a2c0dada86588e8510073725d69377..b08e0ebfc1d4d161661ee542545d8301e752d993 100644 (file)
--- a/helm/ocaml/registry/.ocamlinit
+++ b/helm/ocaml/registry/.ocamlinit
@@ -1,4 +1,4 @@
 #use "topfind";;
 #require "helm-registry";;
 open Helm_registry;;
-load_from "sample.xml";;
+load_from "tests/sample.xml";;

diff --git a/helm/ocaml/registry/tests/sample.xml b/helm/ocaml/registry/tests/sample.xml
index b0f91f30b4e48d4190b3fbd93cd1988a334f2825..b0edbdae0d292ba85403ba466481594daac0d590 100644 (file)
--- a/helm/ocaml/registry/tests/sample.xml
+++ b/helm/ocaml/registry/tests/sample.xml
@@ -12,7 +12,7 @@
     <key name="merge1">yes</key>
   </section>
   <section name="triciclo">
-    <include href="sample_include.xml" />
+    <include href="tests/sample_include.xml" />
   </section>
   <section name="triciclo">
     <key name="merge2">yes</key>