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)
# {{{ Distribution stuff
-ifeq ($(HAVE_OCAMLOPT),yes)
+ifeq ($(wildcard matitac.opt),matitac.opt)
BEST=opt
else
BEST=all
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 = \
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 $< $@
--- /dev/null
+matita.conf.xml.devel
\ No newline at end of file
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="user">
+ <key name="home">$(HOME)</key>
+ </section>
+ <section name="matita">
+ <key name="basedir">.matita</key>
+ <key name="owner">nobody</key>
+ </section>
+ <section name="db">
+ <key name="host">@DBHOST@</key>
+ <key name="user">helm</key>
+ <key name="database">matita</key>
+ </section>
+ <section name="getter">
+ <key name="cache_dir">.matita/getter/cache</key>
+ <key name="prefix">
+ cic:/matita/
+ file://.matita/xml/matita/
+ </key>
+ <key name="prefix">
+ cic:/
+ file:///does_not_exists/
+ legacy
+ </key>
+ </section>
+</helm_registry>
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="user">
+ <!-- User home directory. Here a ".matita" directory will be created
+ and used to store the part of the library developed by the user. -->
+ <key name="home">$(HOME)</key>
+ <!-- User name. It is used down in this configuration file. If left
+ unspecified, name of the user executing matita will be used (as per
+ getent) -->
+ <!-- <key name="name">foo</key> -->
+ </section>
+ <section name="matita">
+ <!-- Debug only. Stay away. -->
+ <!-- <key name="auto_disambiguation">true</key> -->
+ <!-- Debug only. Stay away. -->
+ <!-- <key name="environment_trust">true</key> -->
+ <key name="basedir">$(user.home)/.matita</key>
+ <!-- Metadata owner. It will be used to create user-specific tables
+ in the SQL database. -->
+ <key name="owner">$(user.name)</key>
+ <!-- Initial GUI font size. -->
+ <!-- <key name="font_size">10</key> -->
+ </section>
+ <section name="db">
+ <!-- Access parameter to the (MySql) metadata database. They are not
+ needed if Matita is always run with -nodb, but this is _not_
+ recommended since a lot of features wont work.
+ Hint. The simplest way to create a database is:
+ 0) # become an user with database administration privileges
+ 1) mysqladmin create matita
+ 2) echo "grant all privileges on matita.* to helm;" | mysql matita
+ Note that this way the database will be open to anyone, apply
+ stricter permissions if needed.
+ -->
+ <key name="host">@DBHOST@</key>
+ <key name="user">helm</key>
+ <key name="database">matita</key>
+ </section>
+ <section name="getter">
+ <!-- Cache dir for CIC XML documents downloaded from the net.
+ Beware that this dir may become really space-consuming. It wont be
+ used if all prefexises below are local (i.e. "file:///" URI scheme).
+ -->
+ <key name="cache_dir">$(user.home)/.matita/getter/cache</key>
+ <!-- "Prefixes", i.e.: mappings URI -> URL of the global library
+ Each prefix mapps an URI of the cic:/ namespace to an URL where the
+ documents can actually be accessed. URL can be in the "file://" or
+ "http://" scheme. Only "file://" scheme can be used to store
+ documents created by the user.
+ Each prefix may be given a list of attributes. Currently supported
+ attributes are:
+ - "legacy" for parts of the library not generated by Matita (e.g.
+ exported from Coq)
+ - "ro" for parts of the library which are not writable by the user
+ (e.g. the Matita standard library)
+ "legacy" implies "ro"
+ -->
+ <key name="prefix">
+ cic:/matita/
+ file://$(user.home)/.matita/xml/matita/
+ </key>
+ <key name="prefix">
+ cic:/
+ file:///projects/helm/library/coq_contribs/
+ legacy
+ </key>
+ </section>
+</helm_registry>
+++ /dev/null
-<?xml version="1.0" encoding="utf-8"?>
-<helm_registry>
- <section name="user">
- <key name="home">~</key>
-<!-- If not specified here, name of the user executing matita will be used -->
-<!-- <key name="name">foo</key> -->
- </section>
- <section name="matita">
- <key name="auto_disambiguation">true</key>
- <key name="environment_trust">true</key>
- <key name="baseuri">cic:/matita/</key>
- <key name="basedir">$(user.home)/.matita</key>
- <key name="owner">$(user.name)</key>
-<!-- <key name="font_size">10</key> -->
- <key name="tactics_bar">false</key>
- </section>
- <section name="db">
- <!-- <key name="host">localhost</key> -->
- <key name="host">mowgli.cs.unibo.it</key>
- <key name="user">helm</key>
- <key name="database">matita</key>
- </section>
- <section name="getter">
- <key name="cache_dir">$(user.home)/.matita/getter/cache</key>
- <key name="dtd_dir">/projects/helm/xml/dtd</key>
- <key name="prefix">
- cic:/
- file:///projects/helm/library/coq_contribs/
- legacy
- </key>
- <key name="prefix">
- cic:/matita/
- file://$(user.home)/.matita/xml/matita/
- </key>
- </section>
-</helm_registry>
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="user">
+ <!-- User home directory. Here a ".matita" directory will be created
+ and used to store the part of the library developed by the user. -->
+ <key name="home">$(HOME)</key>
+ <!-- User name. It is used down in this configuration file. If left
+ unspecified, name of the user executing matita will be used (as per
+ getent) -->
+ <!-- <key name="name">foo</key> -->
+ </section>
+ <section name="matita">
+ <!-- Debug only. Stay away. -->
+ <!-- <key name="auto_disambiguation">true</key> -->
+ <!-- Debug only. Stay away. -->
+ <!-- <key name="environment_trust">true</key> -->
+ <key name="basedir">$(user.home)/.matita</key>
+ <!-- Metadata owner. It will be used to create user-specific tables
+ in the SQL database. -->
+ <key name="owner">$(user.name)</key>
+ <!-- Initial GUI font size. -->
+ <!-- <key name="font_size">10</key> -->
+ </section>
+ <section name="db">
+ <!-- Access parameter to the (MySql) metadata database. They are not
+ needed if Matita is always run with -nodb, but this is _not_
+ recommended since a lot of features wont work.
+ Hint. The simplest way to create a database is:
+ 0) # become an user with database administration privileges
+ 1) mysqladmin create matita
+ 2) echo "grant all privileges on matita.* to helm;" | mysql matita
+ Note that this way the database will be open to anyone, apply
+ stricter permissions if needed.
+ -->
+ <key name="host">@DBHOST@</key>
+ <key name="user">helm</key>
+ <key name="database">matita</key>
+ </section>
+ <section name="getter">
+ <!-- Cache dir for CIC XML documents downloaded from the net.
+ Beware that this dir may become really space-consuming. It wont be
+ used if all prefexises below are local (i.e. "file:///" URI scheme).
+ -->
+ <key name="cache_dir">$(user.home)/.matita/getter/cache</key>
+ <!-- "Prefixes", i.e.: mappings URI -> URL of the global library
+ Each prefix mapps an URI of the cic:/ namespace to an URL where the
+ documents can actually be accessed. URL can be in the "file://" or
+ "http://" scheme. Only "file://" scheme can be used to store
+ documents created by the user.
+ Each prefix may be given a list of attributes. Currently supported
+ attributes are:
+ - "legacy" for parts of the library not generated by Matita (e.g.
+ exported from Coq)
+ - "ro" for parts of the library which are not writable by the user
+ (e.g. the Matita standard library)
+ "legacy" implies "ro"
+ -->
+ <key name="prefix">
+ cic:/matita/
+ file://@RT_BASE_DIR@/library/
+ ro
+ </key>
+ <key name="prefix">
+ cic:/matita/$(user.name)/
+ file://$(user.home)/.matita/xml/matita/
+ </key>
+ <key name="prefix">
+ cic:/
+ file://@RT_BASE_DIR@/legacy/coq/
+ legacy
+ </key>
+ </section>
+</helm_registry>
open Printf
type thingsToInitilaize =
- ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine
+ ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine | Registry
exception FailedToInitialize of thingsToInitilaize
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
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
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
"-I", Arg.String (add_l includes),
("<path> Adds path to the list of searched paths for the "
^ "include command");
+ "-conffile", Arg.Set_string conffile,
+ (Printf.sprintf "<filename> 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",
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;
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
let parse_cmdline () =
status := parse_cmdline !status
+let fill_registry () =
+ status := fill_registry !status
+
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
(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 =
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
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
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
module MK = MatitamakeLib ;;
let main () =
+ MatitaInit.fill_registry ();
MatitaInit.load_configuration_file ();
MK.initialize ();
let usage = ref (fun () -> ()) in
(* $Id$ *)
+open Printf
+
let logger = fun mark ->
match mark with
| `Error -> HLog.error
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)
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
projects / helm.git / commitdiff