From 67fea0e3bea686e59148d13765e20103f9373d24 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 2 Feb 2006 15:41:50 +0000 Subject: [PATCH] release work snapshot ... --- helm/Makefile | 4 ++++ helm/Makefile.defs.in | 2 ++ helm/libs | 1 + helm/matita/Makefile | 26 ++++++++++++++++++++++++++ helm/matita/buildTimeConf.ml.in | 1 - helm/matita/matitaInit.ml | 16 +++++++++++++--- helm/ocaml/Makefile | 4 ++++ helm/ocaml/Makefile.common | 2 ++ helm/ocaml/registry/.ocamlinit | 2 +- helm/ocaml/registry/tests/sample.xml | 2 +- 10 files changed, 54 insertions(+), 6 deletions(-) create mode 120000 helm/libs diff --git a/helm/Makefile b/helm/Makefile index 21012fe0e..de2a403c1 100644 --- 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 b36ba3126..d466f70cb 100644 --- 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 index 000000000..5074bc27f --- /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 3f65ab538..40a4b2014 100644 --- 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 debafe003..8ea2c7b86 100644 --- 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 fec223b00..8223416e4 100644 --- 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 0d1867293..4558a011c 100644 --- 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 1a8b029f9..9feae4f86 100644 --- 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 9aee6008e..b08e0ebfc 100644 --- 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 b0f91f30b..b0edbdae0 100644 --- a/helm/ocaml/registry/tests/sample.xml +++ b/helm/ocaml/registry/tests/sample.xml @@ -12,7 +12,7 @@ yes
- +
yes -- 2.39.2