From: Enrico Tassi Date: Fri, 17 Mar 2006 09:36:38 +0000 (+0000) Subject: tests are now handled with a standard Makefile that does not use do_tests.sh X-Git-Tag: make_still_working~7499 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4e238c92f66aedf21c2d3a33aa5215cdf0a7189f;p=helm.git tests are now handled with a standard Makefile that does not use do_tests.sh --- diff --git a/helm/software/components/getter/http_getter.ml b/helm/software/components/getter/http_getter.ml index d2993575a..574f6b3c2 100644 --- a/helm/software/components/getter/http_getter.ml +++ b/helm/software/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/helm/software/components/getter/http_getter_storage.ml b/helm/software/components/getter/http_getter_storage.ml index 3650d79b9..b1a05d996 100644 --- a/helm/software/components/getter/http_getter_storage.ml +++ b/helm/software/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/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 59e3d5cf9..c6139e0e5 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/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/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index 6e3c1b53d..d3a8954ff 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/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/helm/software/components/library/libraryClean.ml b/helm/software/components/library/libraryClean.ml index 04333fc9a..2ac65c5c8 100644 --- a/helm/software/components/library/libraryClean.ml +++ b/helm/software/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/helm/software/components/library/libraryMisc.ml b/helm/software/components/library/libraryMisc.ml index 148b5f8bc..e971c52d4 100644 --- a/helm/software/components/library/libraryMisc.ml +++ b/helm/software/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/helm/software/components/library/libraryMisc.mli b/helm/software/components/library/libraryMisc.mli index 08ac4638d..d834dbd1a 100644 --- a/helm/software/components/library/libraryMisc.mli +++ b/helm/software/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/helm/software/matita/buildTimeConf.ml.in b/helm/software/matita/buildTimeConf.ml.in index 5a448cde2..ec01152c4 100644 --- a/helm/software/matita/buildTimeConf.ml.in +++ b/helm/software/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/helm/software/matita/buildTimeConf.mli b/helm/software/matita/buildTimeConf.mli index 5477c6c20..78d0df0e8 100644 --- a/helm/software/matita/buildTimeConf.mli +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile deleted file mode 100644 index 5b2b2fa40..000000000 --- a/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/makefile b/helm/software/matita/contribs/LAMBDA-TYPES/makefile new file mode 100644 index 000000000..9ef6694ee --- /dev/null +++ b/helm/software/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/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile deleted file mode 100644 index 5b2b2fa40..000000000 --- a/helm/software/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/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/makefile b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/makefile new file mode 100644 index 000000000..9ef6694ee --- /dev/null +++ b/helm/software/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/helm/software/matita/library/Makefile b/helm/software/matita/library/Makefile deleted file mode 100644 index fd278eb40..000000000 --- a/helm/software/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/helm/software/matita/matita.conf.xml.in b/helm/software/matita/matita.conf.xml.in index 1c8146435..b016367e9 100644 --- a/helm/software/matita/matita.conf.xml.in +++ b/helm/software/matita/matita.conf.xml.in @@ -66,7 +66,12 @@ cic:/ - file://@RT_BASE_DIR@/legacy-library/coq/ + file://@RT_BASE_DIR@/xml/legacy-library/coq/ + legacy + + + cic:/ + file:///projects/helm/library/coq_contribs/ legacy diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index e2274c387..7decc583c 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/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/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index b34f1dfc5..c2677afdb 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/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/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 923354cbd..844d4f5d8 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/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/helm/software/matita/matitadep.ml b/helm/software/matita/matitadep.ml index 919a3ec03..b951571f3 100644 --- a/helm/software/matita/matitadep.ml +++ b/helm/software/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/helm/software/matita/matitamakeLib.ml b/helm/software/matita/matitamakeLib.ml index 490e753e8..ec9a40b81 100644 --- a/helm/software/matita/matitamakeLib.ml +++ b/helm/software/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/helm/software/matita/template_makefile.in b/helm/software/matita/template_makefile.in index d24c75b0f..6a66e269a 100644 --- a/helm/software/matita/template_makefile.in +++ b/helm/software/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/helm/software/matita/template_makefile_devel.in b/helm/software/matita/template_makefile_devel.in new file mode 100644 index 000000000..e0307bbf7 --- /dev/null +++ b/helm/software/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/helm/software/matita/tests/Makefile b/helm/software/matita/tests/Makefile deleted file mode 100644 index 34d4d120c..000000000 --- a/helm/software/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/helm/software/matita/tests/makefile b/helm/software/matita/tests/makefile new file mode 100644 index 000000000..39d64a952 --- /dev/null +++ b/helm/software/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) +