helm/www/matita/docs/manual-0.5.9/matita.conf.xml.html

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Configuring Matita</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets V1.78.1" /><link rel="home" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="up" href="sec_install.html" title="Chapter 2. Installation" /><link rel="prev" href="inst_from_src.html" title="Installing from sources" /><link rel="next" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Configuring Matita</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="inst_from_src.html">Prev</a> </td><th width="60%" align="center">Chapter 2. Installation</th><td width="20%" align="right"> <a accesskey="n" href="sec_gettingstarted.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="matita.conf.xml"></a>Configuring Matita</h2></div></div></div><p>
   3             The configuration file is divided in four sections. The user and
   4             matita ones are self explicative and does not need user
   5             intervention. Here we report a sample snippet for these two
   6             sections. The remaining db and getter sections will be explained in
   7             details later.
   8            </p><pre class="programlisting">
   9
  10   &lt;section name="user"&gt;
  11     &lt;key name="home"&gt;$(HOME)&lt;/key&gt;
  12     &lt;key name="name"&gt;$(USER)&lt;/key&gt;
  13   &lt;/section&gt;
  14   &lt;section name="matita"&gt;
  15     &lt;key name="basedir"&gt;$(user.home)/.matita&lt;/key&gt;
  16     &lt;key name="rt_base_dir"&gt;/usr/share/matita/&lt;/key&gt;
  17     &lt;key name="owner"&gt;$(user.name)&lt;/key&gt;
  18   &lt;/section&gt;
  19 </pre><p>
  20     </p><p>
  21            Matita needs to store/fetch data and metadata. Data is essentially
  22            composed of XML files, metadata is a set of tuples for a relational
  23            model. Data and metadata can produced by the user or be already
  24            available. Both kind of data/metadata can be local and/or remote.
  25    </p><p>
  26            The db section tells Matita where to store and retrieve metadata,
  27            while the getter section describes where XML files have to be
  28            found. The following picture describes the suggested configuration.
  29            Dashed arrows are determined by the configuration file.
  30    </p><div class="figure"><a id="idp68778624"></a><p class="title"><strong>Figure 2.9. Configuring the Databases</strong></p><div class="figure-contents"><div class="mediaobject"><img src="figures/database.png" alt="How to configure the databases." /></div></div></div><br class="figure-break" /><p>The getter</p><p>
  31            Consider the following snippet and the URI
  32            <strong class="userinput"><code>cic:/matita/foo/bar.con</code></strong>. If Matita
  33            is asked to read that object it will resolve the object trough
  34            the getter. Since the first two entries are equally specific
  35            (longest match rule applies) first the path
  36            <strong class="userinput"><code>file://$(matita.rt_base_dir)/xml/standard-library/foo/bar.con</code></strong>
  37            and then <strong class="userinput"><code>file://$(user.home)/.matita/xml/matita/foo/bar.con</code></strong>
  38            are inspected.
  39            </p><pre class="programlisting">
  40
  41   &lt;section name="getter"&gt;
  42     &lt;key name="cache_dir"&gt;$(user.home)/.matita/getter/cache&lt;/key&gt;
  43     &lt;key name="prefix"&gt;
  44       cic:/matita/
  45       file://$(matita.rt_base_dir)/xml/standard-library/
  46       ro
  47     &lt;/key&gt;
  48     &lt;key name="prefix"&gt;
  49       cic:/matita/
  50       file://$(user.home)/.matita/xml/matita/
  51     &lt;/key&gt;
  52     &lt;key name="prefix"&gt;
  53       cic:/Coq/
  54       http://mowgli.cs.unibo.it/xml/
  55       legacy
  56     &lt;/key&gt;
  57   &lt;/section&gt;
  58
  59         </pre><p>
  60         if the same URI has to be written, the former prefix is skipped
  61         since it is marked as readonly (<strong class="userinput"><code>ro</code></strong>).
  62         Objects resolved using the third prefix are readonly too, and are
  63         retrieved using the network. There is no limit to the number of
  64         prefixes the user can define. The distinction between prefixes marked
  65         as readonly and legacy is that, legacy ones are really read only, while
  66         the ones marked with <strong class="userinput"><code>ro</code></strong> are considered for
  67         writing when Matita is started in system mode (used to publish user
  68         developments in the library space).
  69    </p><p>The db</p><p>
  70            The database subsystem has three fron ends: library, user and
  71            legacy.  The latter is the only optional one. Every query is done on
  72            every frontend, making the duplicate free union of the results.
  73            The user front end kepps metadata produced by the user, and is thus
  74            heavily accessed in read/write mode, while the library and legacy
  75            fron ends are read only. Every front end can be connected to
  76            backend, the storage actually.
  77            Consider the following snippet.
  78            </p><pre class="programlisting">
  79
  80   &lt;section name="db"&gt;
  81     &lt;key name="metadata"&gt;mysql://mowgli.cs.unibo.it matita helm none legacy&lt;/key&gt;
  82     &lt;key name="metadata"&gt;file://$(matita.rt_base_dir) metadata.db helm helm library&lt;/key&gt;
  83     &lt;key name="metadata"&gt;file://$(matita.basedir) user.db helm helm user&lt;/key&gt;
  84   &lt;/section&gt;
  85
  86         </pre><p>
  87         Here the usr database is a file (thus locally accessed trough the
  88         Sqlite library) placed in the user's home directory. The library one is
  89         placed in the Matita runtime directory. The legacy fron end is
  90         connected to a remote <span class="application"> <a class="ulink" href="http://www.mysql.com" target="_top">MySQL</a> </span> based storage. Every metadata key
  91         takes a path to the storage, the name of the database, the user name,
  92         a password (or <strong class="userinput"><code>none</code></strong>) and the name of the front
  93         end to which it is attached.
  94    </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="inst_from_src.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_install.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_gettingstarted.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Installing from sources </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 3. Getting started</td></tr></table></div></body></html>