From: Stefano Zacchiroli Date: Fri, 3 Feb 2006 15:13:40 +0000 (+0000) Subject: release snapshot X-Git-Tag: make_still_working~7653 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f28480139ee72d092a9405619c3bdf6d4ff155ee;p=helm.git release snapshot - split of multiple matita conffiles (users vs developers) - removed no longer needed keys in conffiles - commented conffiles entries - made matitaInit.ml more like other matita tools (still a lot to do ...) - save .xml debugging files only if debug is enabled - ... --- diff --git a/helm/matita/Makefile b/helm/matita/Makefile index 415d4a1a5..75d878780 100644 --- a/helm/matita/Makefile +++ b/helm/matita/Makefile @@ -59,32 +59,26 @@ PROGRAMS = $(PROGRAMS_BYTE) matitatop PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) .PHONY: all -all: matita.conf.xml $(PROGRAMS) coq.moo - -matita.conf.xml: matita.conf.xml.sample - @if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\ - touch matita.conf.xml;\ - else\ - echo;\ - echo "matita.conf.xml.sample is newer than matita.conf.xml";\ - echo;\ - echo "PLEASE update your configuration file!";\ - echo "(copying matita.conf.xml.sample should work)";\ - echo;\ - false;\ - fi - -matita.conf.xml.sample: matita.conf.xml.sample.in - autoconf - ./configure - @echo - @echo "WARNING: The configuration sample file has changed!" - @echo - -coq.moo: library/legacy/coq.ma matitac - ./matitac $(MATITA_FLAGS) $< -coq.moo.opt: library/legacy/coq.ma matitac.opt - ./matitac.opt $(MATITA_FLAGS) $< +all: $(PROGRAMS) +# all: matita.conf.xml $(PROGRAMS) coq.moo + +# matita.conf.xml: matita.conf.xml.sample +# @if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\ +# touch matita.conf.xml;\ +# else\ +# echo;\ +# echo "matita.conf.xml.sample is newer than matita.conf.xml";\ +# echo;\ +# echo "PLEASE update your configuration file!";\ +# echo "(copying matita.conf.xml.sample should work)";\ +# echo;\ +# false;\ +# fi + +# coq.moo: library/legacy/coq.ma matitac +# ./matitac $(MATITA_FLAGS) $< +# coq.moo.opt: library/legacy/coq.ma matitac.opt +# ./matitac.opt $(MATITA_FLAGS) $< ifeq ($(HAVE_OCAMLOPT),yes) @@ -190,7 +184,7 @@ cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt) # {{{ Distribution stuff -ifeq ($(HAVE_OCAMLOPT),yes) +ifeq ($(wildcard matitac.opt),matitac.opt) BEST=opt else BEST=all @@ -198,7 +192,11 @@ endif stdlib: MATITA_RT_BASE_DIR=`pwd` \ - $(MAKE) MATITA_FLAGS="-system" -C library/ $(BEST) + MATITA_FLAGS="-system -conffile `pwd`/matita.conf.xml.build" \ + ./matitamake -init build_stdlib + +# MATITA_RT_BASE_DIR=`pwd` \ + $(MAKE) MATITA_FLAGS="-system -conffile `pwd`/matita.conf.xml.build" -C library/ $(BEST) DEST = @RT_BASE_DIR@ INSTALL_STUFF = \ @@ -287,10 +285,9 @@ cicbrowser.opt.static.upx: matita.opt.static.upx distclean: clean $(MAKE) -C dist/ clean rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli - rm -f config.log config.status Makefile buildTimeConf.ml + rm -f buildTimeConf.ml rm -f matita.glade.bak matita.gladep.bak - rm -rf autom4te.cache/ - rm -f configure matita.conf.xml.sample + rm -f matita.conf.xml.sample %.upx: % cp $< $@ diff --git a/helm/matita/matita.conf.xml b/helm/matita/matita.conf.xml new file mode 120000 index 000000000..7f7b7b8e1 --- /dev/null +++ b/helm/matita/matita.conf.xml @@ -0,0 +1 @@ +matita.conf.xml.devel \ No newline at end of file diff --git a/helm/matita/matita.conf.xml.build.in b/helm/matita/matita.conf.xml.build.in new file mode 100644 index 000000000..0ee624540 --- /dev/null +++ b/helm/matita/matita.conf.xml.build.in @@ -0,0 +1,27 @@ + + +
+ $(HOME) +
+
+ .matita + nobody +
+
+ @DBHOST@ + helm + matita +
+
+ .matita/getter/cache + + cic:/matita/ + file://.matita/xml/matita/ + + + cic:/ + file:///does_not_exists/ + legacy + +
+ diff --git a/helm/matita/matita.conf.xml.devel.in b/helm/matita/matita.conf.xml.devel.in new file mode 100644 index 000000000..3a4e7bb70 --- /dev/null +++ b/helm/matita/matita.conf.xml.devel.in @@ -0,0 +1,68 @@ + + +
+ + $(HOME) + + +
+
+ + + + + $(user.home)/.matita + + $(user.name) + + +
+
+ + @DBHOST@ + helm + matita +
+
+ + $(user.home)/.matita/getter/cache + + + cic:/matita/ + file://$(user.home)/.matita/xml/matita/ + + + cic:/ + file:///projects/helm/library/coq_contribs/ + legacy + +
+ diff --git a/helm/matita/matita.conf.xml.sample.in b/helm/matita/matita.conf.xml.sample.in deleted file mode 100644 index ee9aae13b..000000000 --- a/helm/matita/matita.conf.xml.sample.in +++ /dev/null @@ -1,36 +0,0 @@ - - -
- ~ - - -
-
- true - true - cic:/matita/ - $(user.home)/.matita - $(user.name) - - false -
-
- - mowgli.cs.unibo.it - helm - matita -
-
- $(user.home)/.matita/getter/cache - /projects/helm/xml/dtd - - cic:/ - file:///projects/helm/library/coq_contribs/ - legacy - - - cic:/matita/ - file://$(user.home)/.matita/xml/matita/ - -
- diff --git a/helm/matita/matita.conf.xml.user.in b/helm/matita/matita.conf.xml.user.in new file mode 100644 index 000000000..ff4be401e --- /dev/null +++ b/helm/matita/matita.conf.xml.user.in @@ -0,0 +1,73 @@ + + +
+ + $(HOME) + + +
+
+ + + + + $(user.home)/.matita + + $(user.name) + + +
+
+ + @DBHOST@ + helm + matita +
+
+ + $(user.home)/.matita/getter/cache + + + cic:/matita/ + file://@RT_BASE_DIR@/library/ + ro + + + cic:/matita/$(user.name)/ + file://$(user.home)/.matita/xml/matita/ + + + cic:/ + file://@RT_BASE_DIR@/legacy/coq/ + legacy + +
+ diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml index 34b64284f..53ff6b9d6 100644 --- a/helm/matita/matitaInit.ml +++ b/helm/matita/matitaInit.ml @@ -28,7 +28,7 @@ open Printf type thingsToInitilaize = - ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine + ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry exception FailedToInitialize of thingsToInitilaize @@ -42,10 +42,34 @@ let wants s l = let already_configured s l = List.for_all (fun item -> List.exists (fun x -> x = item) l) s +let conffile = ref BuildTimeConf.matita_conf + +let registry_defaults = + [ + "db.nodb", "false"; + "matita.system", "false"; + "matita.debug", "false"; + "matita.external_editor", "gvim -f -c 'go %p' %f"; + "matita.preserve", "false"; + "matita.quiet", "false"; + "matita.profile", "true"; + ] + +let set_registry_values = + List.iter (fun key, value -> Helm_registry.set ~key ~value) + +let fill_registry init_status = + if not (already_configured [ Registry ] init_status) then begin + set_registry_values registry_defaults; + Registry :: init_status + end else + init_status + let load_configuration init_status = + wants [ Registry ] init_status; if not (already_configured [ConfigurationFile] init_status) then begin - Helm_registry.load_from BuildTimeConf.matita_conf; + Helm_registry.load_from !conffile; 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 @@ -85,7 +109,9 @@ let initialize_environment init_status = begin Http_getter.init (); CicEnvironment.set_trust (* environment trust *) - (let trust = Helm_registry.get_bool "matita.environment_trust" in + (let trust = + Helm_registry.get_opt_default Helm_registry.get_bool + ~default:true "matita.environment_trust" in fun _ -> trust); Getter::Environment::init_status end @@ -136,20 +162,6 @@ let usage () = in try Hashtbl.find usages usage_key with Not_found -> default_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"; - "matita.quiet", "false"; - "matita.profile", "true"; - ] - -let set_registry_values = - List.iter (fun key, value -> Helm_registry.set ~key ~value) - let parse_cmdline init_status = if not (already_configured [CmdLine] init_status) then begin let includes = ref [ BuildTimeConf.stdlib_dir ] in @@ -160,6 +172,9 @@ let parse_cmdline init_status = "-I", Arg.String (add_l includes), (" Adds path to the list of searched paths for the " ^ "include command"); + "-conffile", Arg.Set_string conffile, + (Printf.sprintf " Read configuration from filename (default: %s)" + BuildTimeConf.matita_conf); "-q", Arg.Unit (fun () -> Helm_registry.set_bool "matita.quiet" true), "Turn off verbose compilation"; "-preserve", @@ -190,7 +205,6 @@ let parse_cmdline init_status = let set_list ~key l = Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l) in - set_registry_values registry_defaults; Arg.parse arg_spec (add_l args) (usage ()); set_list ~key:"matita.includes" includes; set_list ~key:"matita.args" args; @@ -207,7 +221,8 @@ let die_usage () = let initialize_all () = status := List.fold_left (fun s f -> f s) !status - [ parse_cmdline; load_configuration; initialize_makelib; + [ fill_registry; + parse_cmdline; load_configuration; initialize_makelib; initialize_db; initialize_environment ] (* initialize_notation (initialize_environment @@ -222,3 +237,6 @@ let load_configuration_file () = let parse_cmdline () = status := parse_cmdline !status +let fill_registry () = + status := fill_registry !status + diff --git a/helm/matita/matitaInit.mli b/helm/matita/matitaInit.mli index 9d8671299..63b84b448 100644 --- a/helm/matita/matitaInit.mli +++ b/helm/matita/matitaInit.mli @@ -27,6 +27,7 @@ val initialize_all: unit -> unit (** {2 per-components initialization} *) +val fill_registry: unit -> unit (** fill registry with default values *) val parse_cmdline: unit -> unit (** parse cmdline setting registry keys *) val load_configuration_file: unit -> unit diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 3c4997aec..e2eb22d5b 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -490,9 +490,11 @@ object (self) (Some (Some unsh_sequent, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Hashtbl.create 1, None)); - let name = "sequent_viewer.xml" in - HLog.debug ("load_sequent: dumping MathML to ./" ^ name); - ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()); + if BuildTimeConf.debug then begin + let name = "sequent_viewer.xml" in + HLog.debug ("load_sequent: dumping MathML to ./" ^ name); + ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()) + end; self#load_root ~root:mathml#get_documentElement method load_object obj = @@ -510,9 +512,11 @@ object (self) XmlDiff.update_dom ~from:current_mathml mathml; self#thaw | _ -> - let name = "cic_browser.xml" in - HLog.debug ("cic_browser: dumping MathML to ./" ^ name); - ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()); + if BuildTimeConf.debug then begin + let name = "cic_browser.xml" in + HLog.debug ("cic_browser: dumping MathML to ./" ^ name); + ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()) + end; self#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); end diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 3567c33f0..ee09258e0 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -141,7 +141,9 @@ let go () = MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); LibraryDb.create_owner_environment (); CicEnvironment.set_trust (* environment trust *) - (let trust = Helm_registry.get_bool "matita.environment_trust" in + (let trust = + Helm_registry.get_opt_default Helm_registry.get_bool + ~default:true "matita.environment_trust" in fun _ -> trust); let include_paths = Helm_registry.get_list Helm_registry.string "matita.includes" in diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 48011c0b5..c1ada6aea 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -37,8 +37,9 @@ let main () = let resolve alias current_buri = let buri = buri alias in if buri <> current_buri then Some buri else None in - MatitaInit.load_configuration_file (); + MatitaInit.fill_registry (); MatitaInit.parse_cmdline (); + MatitaInit.load_configuration_file (); let include_paths = Helm_registry.get_list Helm_registry.string "matita.includes" in let basedir = Helm_registry.get "matita.basedir" in diff --git a/helm/matita/matitamake.ml b/helm/matita/matitamake.ml index 9eab0f6d8..f0e17eb8b 100644 --- a/helm/matita/matitamake.ml +++ b/helm/matita/matitamake.ml @@ -28,6 +28,7 @@ module MK = MatitamakeLib ;; let main () = + MatitaInit.fill_registry (); MatitaInit.load_configuration_file (); MK.initialize (); let usage = ref (fun () -> ()) in diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml index 8eba26fb0..fba66e0d6 100644 --- a/helm/matita/matitamakeLib.ml +++ b/helm/matita/matitamakeLib.ml @@ -25,6 +25,8 @@ (* $Id$ *) +open Printf + let logger = fun mark -> match mark with | `Error -> HLog.error @@ -176,7 +178,12 @@ let call_make development target make = let nodb = Helm_registry.get_opt_default Helm_registry.bool ~default:false "db.nodb" in - let flags = if nodb then ["NODB=true"] else [] in + let flags = [] in + let flags = flags @ if nodb then ["NODB=true"] else [] in + let flags = + try + flags @ [ sprintf "MATITA_FLAGS=\"%s\"" (Sys.getenv "MATITA_FLAGS") ] + with Not_found -> flags in make development.root (["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] @ flags) diff --git a/helm/matita/template_makefile.in b/helm/matita/template_makefile.in index 8cbef1fd1..57f1301d5 100644 --- a/helm/matita/template_makefile.in +++ b/helm/matita/template_makefile.in @@ -1,7 +1,8 @@ SRC=$(shell find @ROOT@ -name "*.ma" -a -type f) TODO=$(SRC:%.ma=%.mo) -MATITA_FLAGS=-noprofile +MATITA_FLAGS= +MATITA_FLAGS+=-noprofile NODB=false ifeq ($(NODB),true) MATITA_FLAGS += -nodb