The configuration file is divided in four sections. The user and matita ones are self explicative and does not need user intervention. Here we report a sample snippet for these two sections. The remaining db and getter sections will be explained in details later.

  <section name="user">
    <key name="home">$(HOME)</key>
    <key name="name">$(USER)</key>
  </section>
  <section name="matita">
    <key name="basedir">$(user.home)/.matita</key>
    <key name="rt_base_dir">/usr/share/matita/</key>
    <key name="owner">$(user.name)</key>
  </section>

Matita 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 Matita 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.

Figure 2.9. Configuring the Databases

The getter

Consider the following snippet and the URI cic:/matita/foo/bar.con. If Matita 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.

  <section name="getter">
    <key name="cache_dir">$(user.home)/.matita/getter/cache</key>
    <key name="prefix">
      cic:/matita/
      file://$(matita.rt_base_dir)/xml/standard-library/
      ro
    </key>
    <key name="prefix">
      cic:/matita/
      file://$(user.home)/.matita/xml/matita/
    </key>
    <key name="prefix">
      cic:/Coq/
      http://mowgli.cs.unibo.it/xml/
      legacy
    </key>
  </section>
	
	

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 Matita 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.

  <section name="db">
    <key name="metadata">mysql://mowgli.cs.unibo.it matita helm none legacy</key>
    <key name="metadata">file://$(matita.rt_base_dir) metadata.db helm helm library</key>
    <key name="metadata">file://$(matita.basedir) user.db helm helm user</key>
  </section>
	
	

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 Matita 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.