From 92d4c265cd2a6c5f56273ad5938a0da77bde2315 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 2 Nov 2007 13:07:27 +0000 Subject: [PATCH] added doc for db and getter sections --- matita/help/C/sec_install.xml | 96 +++++++++++++++++++++++++++++++++-- 1 file changed, 92 insertions(+), 4 deletions(-) diff --git a/matita/help/C/sec_install.xml b/matita/help/C/sec_install.xml index 9dd240daf..4d50db4e6 100644 --- a/matita/help/C/sec_install.xml +++ b/matita/help/C/sec_install.xml @@ -247,10 +247,11 @@ - Database setup + (optional) &MYSQL; setup - To fully exploit &appname; indexing and search capabilities you - will need a working &MYSQL; database. Detalied instructions on how to do + To fully exploit &appname; indexing and search capabilities + on a huge metadata set you may + need a working &MYSQL; database. Detalied instructions on how to do it can be found in the MySQL documentation. Here you can find a quick howto. @@ -386,11 +387,25 @@ - Configuring Matita + Configuring &appname; The file matita.conf.xml... &TODO; + + The db and the getter sections + + &appname; needs to store/fetch data and metadata. Data is essentially + composed of XML files, metadata is a set of tuples for a relational + model. Data and metadata can produced by the user or be already + available. Both kind of data/metadata can be local and/or remote. + + + The db section tells &appname; where to store and retrieve metadata, + while the getter section describes where XML files have to be + found. The following picture describes the suggested configuration. + Dashed arrows are determined by the configuration file. +
Configuring the Databases @@ -399,6 +414,79 @@ How to configure the databases.
+ + The getter + + Consider the following snippet and the URI + cic:/matita/foo/bar.con. If &appname; + is asked to read that object it will resolve the object trough + the getter. Since the first two entries are equally specific + (longest match rule applies) first the path + file://$(matita.rt_base_dir)/xml/standard-library/foo/bar.con + and then file://$(user.home)/.matita/xml/matita/foo/bar.con + are inspected. + + + $(user.home)/.matita/getter/cache + + cic:/matita/ + file://$(matita.rt_base_dir)/xml/standard-library/ + ro + + + cic:/matita/ + file://$(user.home)/.matita/xml/matita/ + + + cic:/Coq/ + http://mowgli.cs.unibo.it/xml/ + legacy + + +]]> + + if the same URI has to be written, the former prefix is skipped + since it is marked as readonly (ro). + Objects resolved using the third prefix are readonly too, and are + retrieved using the network. There is no limit to the number of + prefixes the user can define. The distinction between prefixes marked + as readonly and legacy is that, legacy ones are really read only, while + the ones marked with ro are considered for + writing when &appname; is started in system mode (used to publish user + developments in the library space). + + + + The db + + The database subsystem has three fron ends: library, user and + legacy. The latter is the only optional one. Every query is done on + every frontend, making the duplicate free union of the results. + The user front end kepps metadata produced by the user, and is thus + heavily accessed in read/write mode, while the library and legacy + fron ends are read only. Every front end can be connected to + backend, the storage actually. + Consider the following snippet. + + + mysql://mowgli.cs.unibo.it matita helm none legacy + file://$(matita.rt_base_dir) metadata.db helm helm library + file://$(matita.basedir) user.db helm helm user + +]]> + + Here the usr database is a file (thus locally accessed trough the + Sqlite library) placed in the user's home directory. The library one is + placed in the &appname; runtime directory. The legacy fron end is + connected to a remote &MYSQL; based storage. Every metadata key + takes a path to the storage, the name of the database, the user name, + a password (or none) and the name of the front + end to which it is attached. + + +
-- 2.39.2