tests are now handled with a standard Makefile that does not use do_tests.sh

diff --git a/components/getter/http_getter.ml b/components/getter/http_getter.ml
index d2993575a439f3770ffb35c4caab5745dd3c5dea..574f6b3c281b8f1113bbbd7ff9a2c274e8370935 100644 (file)
--- a/components/getter/http_getter.ml
+++ b/components/getter/http_getter.ml
@@ -151,13 +151,21 @@ let exists uri =
    let uri = deref_index_theory uri in
     Http_getter_storage.exists (uri ^ xml_suffix)
        
+let is_an_obj s = 
+  try 
+    s <> UriManager.buri_of_uri (UriManager.uri_of_string s)
+  with UriManager.IllFormedUri _ -> false
+    
 let resolve ~writable uri =
   if remote () then
     resolve_remote ~writable uri
   else
    let uri = deref_index_theory uri in
     try
-      Http_getter_storage.resolve ~writable (uri ^ xml_suffix)
+      if is_an_obj uri then
+        Http_getter_storage.resolve ~writable (uri ^ xml_suffix)
+      else
+        Http_getter_storage.resolve ~writable uri
     with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
 
 let filename ~writable uri =

diff --git a/components/getter/http_getter_storage.ml b/components/getter/http_getter_storage.ml
index 3650d79b95f0bc9b492271a4ea35db4d64e150eb..b1a05d9963f0b24673a56892af8ede8695fdc125 100644 (file)
--- a/components/getter/http_getter_storage.ml
+++ b/components/getter/http_getter_storage.ml
@@ -295,7 +295,10 @@ let exists s =
   with Resource_not_found _ -> false
 
 let resolve ?(must_exists=true) ~writable =
-  dispatch_single 
+  (if must_exists then
+    dispatch_multi
+  else
+    dispatch_single)
     { write = writable;
       name="resolve"; 
       exists = must_exists;

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 59e3d5cf9e69ef8831014a186895b11411e31ea0..c6139e0e574da702d0c95a3a20a41a70e5cfabdc 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -565,8 +565,10 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
      GrafiteTypes.add_moo_content [cmd] status,[]
   | GrafiteAst.Include (loc, baseuri) ->
      let moopath_rw, moopath_r = 
-       LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true,
-       LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:false
+       LibraryMisc.obj_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:true,
+       LibraryMisc.obj_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:false
      in
      let moopath = 
        if Sys.file_exists moopath_r then moopath_r else
@@ -596,6 +598,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
           LibraryClean.clean_baseuris [value];
           assert (Http_getter_storage.is_empty value);
         end;
+        HExtlib.mkdir 
+          (Filename.dirname (Http_getter.filename ~writable:true (value ^
+            "/foo.con")));
       end;
       GrafiteTypes.set_option status name value,[]
   | GrafiteAst.Drop loc -> raise Drop

diff --git a/components/lexicon/lexiconEngine.ml b/components/lexicon/lexiconEngine.ml
index 6e3c1b53d2c5aff600c98ea970689c493dc737e1..d3a8954ff7479be5978ad73d62126d51f8238f28 100644 (file)
--- a/components/lexicon/lexiconEngine.ml
+++ b/components/lexicon/lexiconEngine.ml
@@ -111,8 +111,10 @@ let rec eval_command status cmd =
   match cmd with
   | LexiconAst.Include (loc, baseuri) ->
      let lexiconpath_rw, lexiconpath_r = 
-       LibraryMisc.lexicon_file_of_baseuri ~writable:true ~baseuri,
-       LibraryMisc.lexicon_file_of_baseuri ~writable:false ~baseuri
+       LibraryMisc.lexicon_file_of_baseuri 
+         ~must_exist:false ~writable:true ~baseuri,
+       LibraryMisc.lexicon_file_of_baseuri 
+         ~must_exist:false ~writable:false ~baseuri
      in
      let lexiconpath = 
        if Sys.file_exists lexiconpath_rw then lexiconpath_rw else
@@ -123,8 +125,10 @@ let rec eval_command status cmd =
      let status = List.fold_left eval_command status lexicon in
       if Helm_registry.get_bool "db.nodb" then
        let metadatapath_rw, metadatapath_r = 
-         LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true,
-         LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:false
+         LibraryMisc.metadata_file_of_baseuri 
+           ~must_exist:false ~baseuri ~writable:true,
+         LibraryMisc.metadata_file_of_baseuri 
+           ~must_exist:false ~baseuri ~writable:false
        in
        let metadatapath =
         if Sys.file_exists metadatapath_rw then metadatapath_rw else

diff --git a/components/library/libraryClean.ml b/components/library/libraryClean.ml
index 04333fc9a66724230fea843153a4d36d22d42e3b..2ac65c5c8b9d2f3435a17fdf10a99a82415d6353 100644 (file)
--- a/components/library/libraryClean.ml
+++ b/components/library/libraryClean.ml
@@ -213,11 +213,14 @@ let clean_baseuris ?(verbose=true) buris =
    (fun baseuri ->
      try 
        HExtlib.safe_remove 
-         (LibraryMisc.obj_file_of_baseuri ~writable:true ~baseuri);
+         (LibraryMisc.obj_file_of_baseuri 
+           ~must_exist:false ~writable:true ~baseuri);
        HExtlib.safe_remove 
-         (LibraryMisc.metadata_file_of_baseuri ~writable:true ~baseuri);
+         (LibraryMisc.metadata_file_of_baseuri 
+           ~must_exist:false ~writable:true ~baseuri);
        HExtlib.safe_remove 
-         (LibraryMisc.lexicon_file_of_baseuri ~writable:true ~baseuri)
+         (LibraryMisc.lexicon_file_of_baseuri 
+           ~must_exist:false ~writable:true ~baseuri)
      with Http_getter_types.Key_not_found _ -> ())
    (HExtlib.list_uniq (List.fast_sort Pervasives.compare
      (List.map (UriManager.buri_of_uri) l)));

diff --git a/components/library/libraryMisc.ml b/components/library/libraryMisc.ml
index 148b5f8bc905b077691a6c06c61100b648e8db36..e971c52d4b09cfe489ac27facb5e0c43729de748 100644 (file)
--- a/components/library/libraryMisc.ml
+++ b/components/library/libraryMisc.ml
@@ -25,12 +25,16 @@
 
 (* $Id$ *)
 
-let resolve ~writable baseuri = Http_getter.filename ~writable baseuri
+let resolve ~must_exist ~writable baseuri = 
+  if must_exist then 
+    Http_getter.resolve ~writable baseuri
+  else 
+    Http_getter.filename ~writable baseuri
 
-let obj_file_of_baseuri ~writable ~baseuri = 
-  resolve ~writable baseuri ^ ".moo"
-let lexicon_file_of_baseuri ~writable ~baseuri = 
-  resolve ~writable baseuri ^ ".lexicon"
-let metadata_file_of_baseuri~writable  ~baseuri = 
-  resolve ~writable baseuri ^ ".metadata"
+let obj_file_of_baseuri ~must_exist ~writable ~baseuri = 
+  resolve ~must_exist ~writable baseuri ^ ".moo"
+let lexicon_file_of_baseuri ~must_exist ~writable ~baseuri = 
+  resolve ~must_exist ~writable baseuri ^ ".lexicon"
+let metadata_file_of_baseuri~must_exist ~writable  ~baseuri = 
+  resolve ~must_exist ~writable baseuri ^ ".metadata"
 

diff --git a/components/library/libraryMisc.mli b/components/library/libraryMisc.mli
index 08ac4638d3ff2b4f94be8fa610098bb7895c6f8f..d834dbd1ad1b55280f876a47cdc6ae4a84c1ce17 100644 (file)
--- a/components/library/libraryMisc.mli
+++ b/components/library/libraryMisc.mli
@@ -23,6 +23,9 @@
  * http://helm.cs.unibo.it/
  *)
 
-val obj_file_of_baseuri: writable:bool -> baseuri:string -> string
-val lexicon_file_of_baseuri: writable:bool -> baseuri:string -> string
-val metadata_file_of_baseuri: writable:bool -> baseuri:string -> string
+val obj_file_of_baseuri: 
+  must_exist:bool -> writable:bool -> baseuri:string -> string
+val lexicon_file_of_baseuri: 
+  must_exist:bool -> writable:bool -> baseuri:string -> string
+val metadata_file_of_baseuri: 
+  must_exist:bool -> writable:bool -> baseuri:string -> string

diff --git a/matita/buildTimeConf.ml.in b/matita/buildTimeConf.ml.in
index 5a448cde22fb5b531c140c104a0057912d1d4150..ec01152c44e878cdd97fe5b3f5c8ada08b981d87 100644 (file)
--- a/matita/buildTimeConf.ml.in
+++ b/matita/buildTimeConf.ml.in
@@ -51,6 +51,8 @@ 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"
+let matitamake_makefile_template_devel = 
+  runtime_base_dir ^ "/template_makefile_devel.in"
 let stdlib_dir_devel = runtime_base_dir ^ "/library"
 let stdlib_dir_installed = runtime_base_dir ^ "/ma/standard-library"
 let help_dir = runtime_base_dir ^ "/help"

diff --git a/matita/buildTimeConf.mli b/matita/buildTimeConf.mli
index 5477c6c20afcd1af3acbadabf6746299d3c88b5c..78d0df0e8cbc5a6ef2f9fd65f25b73e1c9a735c4 100644 (file)
--- a/matita/buildTimeConf.mli
+++ b/matita/buildTimeConf.mli
@@ -25,28 +25,29 @@
 
 (* $Id$ *)
 
-val base_uri                      : string
-val blank_uri                     : string
-val browser_history_size          : int
-val closed_xml                    : string
-val console_history_size          : int
-val core_notation_script          : string
-val current_proof_uri             : string
-val debug                         : bool
-val default_font_size             : int
-val gtkmathview_conf              : string
-val gtkrc_file                    : string
-val help_dir                      : string
-val images_dir                    : string
-val lang_file                     : string
-val matita_conf                   : string
-val matitamake_makefile_template  : string
-val phrase_sep                    : string
-val runtime_base_dir              : string
-val script_font                   : string
-val script_template               : string
-val stdlib_dir_devel              : string
-val stdlib_dir_installed          : string
-val undo_history_size             : int
-val version                       : string
+val base_uri                              : string
+val blank_uri                             : string
+val browser_history_size                  : int
+val closed_xml                            : string
+val console_history_size                  : int
+val core_notation_script                  : string
+val current_proof_uri                     : string
+val debug                                 : bool
+val default_font_size                     : int
+val gtkmathview_conf                      : string
+val gtkrc_file                            : string
+val help_dir                              : string
+val images_dir                            : string
+val lang_file                             : string
+val matita_conf                           : string
+val matitamake_makefile_template          : string
+val matitamake_makefile_template_devel    : string
+val phrase_sep                            : string
+val runtime_base_dir                      : string
+val script_font                           : string
+val script_template                       : string
+val stdlib_dir_devel                      : string
+val stdlib_dir_installed                  : string
+val undo_history_size                     : int
+val version                               : string
 

diff --git a/matita/contribs/LAMBDA-TYPES/Makefile b/matita/contribs/LAMBDA-TYPES/Makefile
deleted file mode 100644 (file)
index 5b2b2fa..0000000
--- a/matita/contribs/LAMBDA-TYPES/Makefile
+++ /dev/null
@@ -1,57 +0,0 @@
-SRC=$(shell find . -name "*.ma" -a -type f)
-
-MATITA_FLAGS = -I ../..
-NODB=false
-ifeq ($(NODB),true)
-       MATITA_FLAGS += -nodb
-endif
-
-MATITAC=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac $(MATITA_FLAGS)" "../../matitaclean $(MATITA_FLAGS)" /dev/null OK
-MATITACOPT=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac.opt $(MATITA_FLAGS)" "../../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
-VERBOSEMATITAC=../../matitac $(MATITA_FLAGS)
-VERBOSEMATITACOPT=../../matitac.opt $(MATITA_FLAGS)
-
-MATITACLEAN=../../matitaclean $(MATITA_FLAGS)
-MATITACLEANOPT=../../matitaclean.opt $(MATITA_FLAGS)
-
-MATITADEP=../../matitadep $(MATITA_FLAGS)
-MATITADEPOPT=../../matitadep.opt $(MATITA_FLAGS)
-
-DEPEND_NAME=.depend
-
-H=@
-
-all: $(SRC:%.ma=%.mo)
-
-opt:
-       $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' all
-
-verbose:
-       $(H)$(MAKE) MATITAC='$(VERBOSEMATITAC)' MATITACLEAN='$(MATITACLEAN)' MATITADEP='$(MATITADEP)' all
-
-%.opt:
-       $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
-
-clean_:
-       $(H)rm -f __*not_for_matita
-
-clean: clean_
-       $(H)$(MATITACLEAN) $(SRC)
-
-cleanall: clean_
-       $(H)rm -f $(SRC:%.ma=%.moo)
-       $(H)$(MATITACLEAN) all
-
-depend:
-       $(H)rm -f $(DEPEND_NAME)
-       $(H)$(MAKE) $(DEPEND_NAME)
-.PHONY: depend
-
-%.moo:
-       $(H)$(MATITAC) $<
-
-$(DEPEND_NAME): $(SRC)
-       $(H)$(MATITADEP) $(SRC) > $@ || rm -f $@
-
-#include $(DEPEND_NAME)
-include .depend

diff --git a/matita/contribs/LAMBDA-TYPES/makefile b/matita/contribs/LAMBDA-TYPES/makefile
new file mode 100644 (file)
index 0000000..9ef6694
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/makefile
@@ -0,0 +1,33 @@
+H=@
+
+RT_BASEDIR=../../
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) 
+
+devel:=$(shell basename `pwd`)
+
+all: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       
+preall:
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+

diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile b/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile
deleted file mode 100644 (file)
index 5b2b2fa..0000000
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile
+++ /dev/null
@@ -1,57 +0,0 @@
-SRC=$(shell find . -name "*.ma" -a -type f)
-
-MATITA_FLAGS = -I ../..
-NODB=false
-ifeq ($(NODB),true)
-       MATITA_FLAGS += -nodb
-endif
-
-MATITAC=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac $(MATITA_FLAGS)" "../../matitaclean $(MATITA_FLAGS)" /dev/null OK
-MATITACOPT=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac.opt $(MATITA_FLAGS)" "../../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
-VERBOSEMATITAC=../../matitac $(MATITA_FLAGS)
-VERBOSEMATITACOPT=../../matitac.opt $(MATITA_FLAGS)
-
-MATITACLEAN=../../matitaclean $(MATITA_FLAGS)
-MATITACLEANOPT=../../matitaclean.opt $(MATITA_FLAGS)
-
-MATITADEP=../../matitadep $(MATITA_FLAGS)
-MATITADEPOPT=../../matitadep.opt $(MATITA_FLAGS)
-
-DEPEND_NAME=.depend
-
-H=@
-
-all: $(SRC:%.ma=%.mo)
-
-opt:
-       $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' all
-
-verbose:
-       $(H)$(MAKE) MATITAC='$(VERBOSEMATITAC)' MATITACLEAN='$(MATITACLEAN)' MATITADEP='$(MATITADEP)' all
-
-%.opt:
-       $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
-
-clean_:
-       $(H)rm -f __*not_for_matita
-
-clean: clean_
-       $(H)$(MATITACLEAN) $(SRC)
-
-cleanall: clean_
-       $(H)rm -f $(SRC:%.ma=%.moo)
-       $(H)$(MATITACLEAN) all
-
-depend:
-       $(H)rm -f $(DEPEND_NAME)
-       $(H)$(MAKE) $(DEPEND_NAME)
-.PHONY: depend
-
-%.moo:
-       $(H)$(MATITAC) $<
-
-$(DEPEND_NAME): $(SRC)
-       $(H)$(MATITADEP) $(SRC) > $@ || rm -f $@
-
-#include $(DEPEND_NAME)
-include .depend

diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/makefile b/matita/contribs/PREDICATIVE-TOPOLOGY/makefile
new file mode 100644 (file)
index 0000000..9ef6694
--- /dev/null
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/makefile
@@ -0,0 +1,33 @@
+H=@
+
+RT_BASEDIR=../../
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) 
+
+devel:=$(shell basename `pwd`)
+
+all: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       
+preall:
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+

diff --git a/matita/library/Makefile b/matita/library/Makefile
deleted file mode 100644 (file)
index fd278eb..0000000
--- a/matita/library/Makefile
+++ /dev/null
@@ -1,57 +0,0 @@
-SRC=$(shell find . -name "*.ma" -a -type f)
-
-MATITA_FLAGS =
-NODB=false
-ifeq ($(NODB),true)
-       MATITA_FLAGS += -nodb
-endif
-
-MATITAC=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac $(MATITA_FLAGS)" "../matitaclean $(MATITA_FLAGS)" /dev/null OK
-MATITACOPT=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac.opt $(MATITA_FLAGS)" "../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
-VERBOSEMATITAC=../matitac $(MATITA_FLAGS)
-VERBOSEMATITACOPT=../matitac.opt $(MATITA_FLAGS)
-
-MATITACLEAN=../matitaclean $(MATITA_FLAGS)
-MATITACLEANOPT=../matitaclean.opt $(MATITA_FLAGS)
-
-MATITADEP=../matitadep $(MATITA_FLAGS)
-MATITADEPOPT=../matitadep.opt $(MATITA_FLAGS)
-
-DEPEND_NAME=.depend
-
-H=@
-
-all: $(SRC:%.ma=%.mo)
-
-opt:
-       $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' all
-
-verbose:
-       $(H)$(MAKE) MATITAC='$(VERBOSEMATITAC)' MATITACLEAN='$(MATITACLEAN)' MATITADEP='$(MATITADEP)' all
-
-%.opt:
-       $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
-
-clean_:
-       $(H)rm -f __*not_for_matita
-
-clean: clean_
-       $(H)$(MATITACLEAN) $(SRC)
-
-cleanall:
-       $(H)rm -f $(SRC:%.ma=%.moo)
-       $(H)$(MATITACLEAN) all
-
-depend:
-       $(H)rm -f $(DEPEND_NAME)
-       $(H)$(MAKE) $(DEPEND_NAME)
-.PHONY: depend
-
-%.moo:
-       $(H)$(MATITAC) $<
-
-$(DEPEND_NAME): $(SRC)
-       $(H)$(MATITADEP) $(SRC) > $@ || rm -f $@
-
-#include $(DEPEND_NAME)
-include .depend

diff --git a/matita/matita.conf.xml.in b/matita/matita.conf.xml.in
index 1c8146435a6375428cd8ad0a16602a11c22d797b..b016367e980f8df9d697a323187ac1b07e91e564 100644 (file)
--- a/matita/matita.conf.xml.in
+++ b/matita/matita.conf.xml.in
@@ -66,7 +66,12 @@
     </key>
     <key name="prefix">
       cic:/
-      file://@RT_BASE_DIR@/legacy-library/coq/
+      file://@RT_BASE_DIR@/xml/legacy-library/coq/
+      legacy
+    </key>
+    <key name="prefix">
+      cic:/
+      file:///projects/helm/library/coq_contribs/
       legacy
     </key>
   </section>

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index e2274c387162f7b4830c104c0764706406058850..7decc583c58ab4b8de1b7a0dab4b49867792bae9 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -71,12 +71,15 @@ let clean_current_baseuri grafite_status =
 
 let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = 
   let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in
-  let moo_fname = LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true in
+  let moo_fname = 
+    LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in
   let save () =
     let metadata_fname =
-     LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true in
+     LibraryMisc.metadata_file_of_baseuri 
+       ~must_exist:false ~baseuri ~writable:true in
     let lexicon_fname =
-     LibraryMisc.lexicon_file_of_baseuri ~baseuri ~writable:true
+     LibraryMisc.lexicon_file_of_baseuri 
+       ~must_exist:false ~baseuri ~writable:true
     in
      GrafiteMarshal.save_moo moo_fname
       grafite_status.GrafiteTypes.moo_content_rev;

diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml
index b34f1dfc5b67ced099ea20aa9aec97599c964b6b..c2677afdbd82ad40f9d8d5b816b4888087e601cb 100644 (file)
--- a/matita/matitaInit.ml
+++ b/matita/matitaInit.ml
@@ -211,8 +211,8 @@ let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
 let parse_cmdline init_status =
   if not (already_configured [CmdLine] init_status) then begin
     let includes = ref [ 
-      BuildTimeConf.stdlib_dir_installed ;
-      BuildTimeConf.stdlib_dir_devel ] 
+      BuildTimeConf.stdlib_dir_devel;
+      BuildTimeConf.stdlib_dir_installed ; ] 
     in
     let args = ref [] in
     let add_l l = fun s -> l := s :: !l in
@@ -269,6 +269,7 @@ let parse_cmdline init_status =
     in
     Arg.parse arg_spec (add_l args) (usage ());
     set_list ~key:"matita.includes" includes;
+    args := List.filter (fun x -> x <> "") !args;
     set_list ~key:"matita.args" args;
     HExtlib.set_profiling_printings 
       (fun () -> Helm_registry.get_bool "matita.profile");

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 923354cbda7058c4a7c4635594b301cc5564ee81..844d4f5d854dd723ba1f3390d6b449674596608f 100644 (file)
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -81,11 +81,17 @@ let run_script is eval_function  =
       raise exn
 
 let fname () =
-  match Helm_registry.get_list Helm_registry.string "matita.args" with
+  let rec aux = function
+  | ""::tl -> aux tl
   | [x] -> x
+  | [] -> MatitaInit.die_usage ()
   | l -> 
-      prerr_endline ("Wrong commands: " ^ String.concat " " l);
+      prerr_endline 
+        ("Wrong commands: " ^ 
+          String.concat " " (List.map (fun x -> "'" ^ x ^ "'") l));
       MatitaInit.die_usage ()
+  in
+  aux (Helm_registry.get_list Helm_registry.string "matita.args")
 
 let pp_ocaml_mode () = 
   HLog.message "";
@@ -187,9 +193,13 @@ let pp_times fname bench_mode rc big_bang =
             assert (fnamelen > rootlen); 
             String.sub fname rootlen (fnamelen - rootlen)           
       in
-      let s = 
-        Printf.sprintf "%s %-35s %-4s %s %s" cc fname rc times extra 
+      let fname = 
+        if fname.[0] = '/' then
+          String.sub fname 1 (String.length fname - 1)
+        else
+          fname
       in
+      let s = Printf.sprintf "%s %-35s %-4s %s %s" cc fname rc times extra in
       print_endline s;
       flush stdout
     end
@@ -268,13 +278,16 @@ let main ~mode =
        let baseuri =
         DependenciesParser.baseuri_of_script ~include_paths fname in
        let moo_fname = 
-         LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true 
+         LibraryMisc.obj_file_of_baseuri 
+           ~must_exist:false ~baseuri ~writable:true 
        in
        let lexicon_fname= 
-         LibraryMisc.lexicon_file_of_baseuri ~baseuri ~writable:true 
+         LibraryMisc.lexicon_file_of_baseuri 
+          ~must_exist:false ~baseuri ~writable:true 
        in
        let metadata_fname =
-        LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true
+        LibraryMisc.metadata_file_of_baseuri 
+          ~must_exist:false ~baseuri ~writable:true
        in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
        LibraryNoDb.save_metadata metadata_fname metadata;

diff --git a/matita/matitadep.ml b/matita/matitadep.ml
index 919a3ec03e76168faff98c174eff5a11cb718ee3..b951571f3fc85155400553604ad8ddf3aa6190ce 100644 (file)
--- a/matita/matitadep.ml
+++ b/matita/matitadep.ml
@@ -27,6 +27,17 @@
 
 module GA = GrafiteAst 
 module U = UriManager
+                
+let obj_file_of_baseuri writable baseuri = 
+  try 
+    LibraryMisc.obj_file_of_baseuri 
+     ~must_exist:true ~baseuri ~writable
+  with 
+  | Http_getter_types.Unresolvable_URI _ 
+  | Http_getter_types.Key_not_found _ ->  
+    LibraryMisc.obj_file_of_baseuri 
+     ~must_exist:false ~baseuri ~writable:true
+;;
 
 let main () =
   (* all are maps from "file" to "something" *)
@@ -45,8 +56,8 @@ let main () =
   List.iter
    (fun ma_file -> 
     let ic = open_in ma_file in
-    let istream = Ulexing.from_utf8_channel ic in
-    let dependencies = DependenciesParser.parse_dependencies istream in
+      let istream = Ulexing.from_utf8_channel ic in
+      let dependencies = DependenciesParser.parse_dependencies istream in
     close_in ic;
     List.iter 
      (function
@@ -62,8 +73,7 @@ let main () =
             let baseuri =
               DependenciesParser.baseuri_of_script ~include_paths path in
             if not (Http_getter_storage.is_legacy baseuri) then
-              let moo_file =
-                LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:false in
+              let moo_file = obj_file_of_baseuri false baseuri in
               Hashtbl.add include_deps ma_file moo_file
           with Sys_error _ -> 
             HLog.warn 
@@ -76,8 +86,7 @@ let main () =
       match dep with 
       | None -> ()
       | Some u -> 
-         Hashtbl.add include_deps file
-          (LibraryMisc.obj_file_of_baseuri ~baseuri:u ~writable:false))
+         Hashtbl.add include_deps file (obj_file_of_baseuri false u))
   uri_deps;
   List.iter
    (fun ma_file -> 
@@ -86,8 +95,9 @@ let main () =
     let deps = HExtlib.list_uniq deps in
     let deps = ma_file :: deps in
     let baseuri = Hashtbl.find baseuri_of ma_file in
-    let moo = LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:false in
-     Printf.printf "%s: %s\n" moo (String.concat " " deps);
-     Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file) moo)
+    let moo = obj_file_of_baseuri true baseuri in
+    Printf.printf "%s: %s\n%s: %s\n%s: %s\n" moo (String.concat " " deps)
+      (Filename.basename (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file)) moo
+      (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file) moo)
    (Helm_registry.get_list Helm_registry.string "matita.args")
 

diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml
index 490e753e86abd853d37b672a424c8d7f21e581b9..ec9a40b814b8cca206fef14af5a49af30c8f3f88 100644 (file)
--- a/matita/matitamakeLib.ml
+++ b/matita/matitamakeLib.ml
@@ -137,26 +137,29 @@ let rebuild_makefile development =
   let template = Pcre.replace ~pat:"@CLEAN@" ~templ:rm template in
   HExtlib.output_file ~filename:makefilepath ~text:template
   
+let rebuild_makefile_devel development = 
+  let path = development.root ^ "/makefile" in
+  if not (Sys.file_exists path) then
+    begin
+      let template = 
+        HExtlib.input_file BuildTimeConf.matitamake_makefile_template_devel
+      in
+      let template = 
+        Pcre.replace ~pat:"@MATITA_RT_BASE_DIR@"
+          ~templ:BuildTimeConf.runtime_base_dir template
+      in
+      HExtlib.output_file ~filename:path ~text:template
+    end
+  
 (* creates a new development if possible *)
 let initialize_development name dir =
   let name = Pcre.replace ~pat:" " ~templ:"_" name in 
   let dev = {name = name ; root = dir} in
-  match development_for_dir dir with
-  | Some dev ->
-      if dir <> dev.root then begin
-        logger `Error 
-          (sprintf ("Dir \"%s\" is already handled by development \"%s\"\n"
-            ^^ "Development \"%s\" is rooted in \"%s\"\n"
-            ^^ "Dir \"%s\" is a sub-dir of \"%s\"")
-          dir dev.name dev.name dev.root dir dev.root);
-        None
-      end else (* requirement development alreay exists, do nothing *)
-        Some dev
-  | None -> 
-      dump_development dev;
-      rebuild_makefile dev;
-      developments := dev :: !developments;
-      Some dev
+  dump_development dev;
+  rebuild_makefile dev;
+  rebuild_makefile_devel dev;
+  developments := dev :: !developments;
+  Some dev
 
 let make chdir args = 
   let old = Unix.getcwd () in
@@ -197,6 +200,7 @@ let call_make ?matita_flags development target make =
   let args = 
     ["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] @ flags 
   in
+(*     prerr_endline (String.concat " " args);   *)
   make development.root args
       
 let build_development ?matita_flags ?(target="all") development =
@@ -239,6 +243,7 @@ let mk_maker refresh_cb =
     let pid = ref ~-1 in
     ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
     try
+(*       prerr_endline (String.concat " " args); *)
       let argv = Array.of_list ("make"::args) in
       pid := Unix.create_process "make" argv Unix.stdin out_w err_w;
       Unix.close out_w;

diff --git a/matita/template_makefile.in b/matita/template_makefile.in
index d24c75b0ff36858fa85c02248929546a73af01bd..6a66e269ac133b74aca98d09c28bd7d619ef26a0 100644 (file)
--- a/matita/template_makefile.in
+++ b/matita/template_makefile.in
@@ -19,7 +19,11 @@ clean:
        rm -f $(TODO)
 
 %.moo:
-       $(MATITAC) $(MATITA_FLAGS) -q -I @ROOT@ $<
+       if [ -z "$<" ]; then \
+               echo "missing dependencies for $@"; \
+       else \
+               $(MATITAC) $(MATITA_FLAGS) -q -I @ROOT@ $<; \
+       fi
 
 @DEPFILE@ : $(SRC)
        $(MATITADEP) $(MATITA_FLAGS) -I '@ROOT@' $^ 1> @DEPFILE@ 

diff --git a/matita/template_makefile_devel.in b/matita/template_makefile_devel.in
new file mode 100644 (file)
index 0000000..e0307bb
--- /dev/null
+++ b/matita/template_makefile_devel.in
@@ -0,0 +1,33 @@
+H=@
+
+RT_BASEDIR=@MATITA_RT_BASE_DIR@/
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) 
+
+devel:=$(shell basename `pwd`)
+
+all: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       
+preall:
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+

diff --git a/matita/tests/Makefile b/matita/tests/Makefile
deleted file mode 100644 (file)
index 34d4d12..0000000
--- a/matita/tests/Makefile
+++ /dev/null
@@ -1,57 +0,0 @@
-SRC=$(wildcard *.ma)
-
-MATITA_FLAGS = -I ..
-NODB=false
-ifeq ($(NODB),true)
-       MATITA_FLAGS += -nodb
-endif
-
-MATITAC=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac $(MATITA_FLAGS)" "../matitaclean $(MATITA_FLAGS)" /dev/null OK
-MATITACOPT=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac.opt $(MATITA_FLAGS)" "../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
-VERBOSEMATITAC=../matitac $(MATITA_FLAGS)
-VERBOSEMATITACOPT=../matitac.opt $(MATITA_FLAGS)
-
-MATITACLEAN=../matitaclean $(MATITA_FLAGS)
-MATITACLEANOPT=../matitaclean.opt $(MATITA_FLAGS)
-
-MATITADEP=../matitadep $(MATITA_FLAGS)
-MATITADEPOPT=../matitadep.opt $(MATITA_FLAGS)
-
-DEPEND_NAME=.depend
-
-H=@
-
-all: $(SRC:%.ma=%.mo)
-
-opt:
-       $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' all
-
-verbose:
-       $(H)$(MAKE) MATITAC='$(VERBOSEMATITAC)' MATITACLEAN='$(MATITACLEAN)' MATITADEP='$(MATITADEP)' all
-
-%.opt:
-       $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
-
-clean_:
-       $(H)rm -f __*not_for_matita
-
-clean: clean_
-       $(H)$(MATITACLEAN) $(SRC)
-
-cleanall: clean_
-       $(H)rm -f $(SRC:%.ma=%.moo)
-       $(H)$(MATITACLEAN) all
-
-depend:
-       $(H)rm -f $(DEPEND_NAME)
-       $(H)$(MAKE) $(DEPEND_NAME)
-.PHONY: depend
-
-%.moo:
-       $(H)$(MATITAC) $<
-
-$(DEPEND_NAME): $(SRC)
-       $(H)$(MATITADEP) $(SRC) > $@ || rm -f $@
-
-#include $(DEPEND_NAME)
-include .depend

diff --git a/matita/tests/makefile b/matita/tests/makefile
new file mode 100644 (file)
index 0000000..39d64a9
--- /dev/null
+++ b/matita/tests/makefile
@@ -0,0 +1,33 @@
+H=@
+
+RT_BASEDIR=../
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) 
+
+devel:=$(shell basename `pwd`)
+
+all: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       
+preall:
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+