matita/matita/help/C/html/authoring.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>Authoring</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets Vsnapshot" /><link rel="home" href="index.html" title="Matita V0.99.5 User Manual (rev. 0.99.5 )" /><link rel="up" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /><link rel="prev" href="cicbrowser.html" title="Browsing and searching" /><link rel="next" href="sec_terms.html" title="Chapter 4. Syntax" /></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">Authoring</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="cicbrowser.html">Prev</a> </td><th width="60%" align="center">Chapter 3. Getting started</th><td width="20%" align="right"> <a accesskey="n" href="sec_terms.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="authoring"></a>Authoring</h2></div></div></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="compilation"></a>How to compile a script</h3></div></div></div><p>
   3         Scripts are compiled to base URIs. Base URIs are of the form
   4         "cic:/matita/path" and are given once for all for a set
   5         of scripts using the "root" file.
   6    </p><p>
   7         A "root" file has to be placed in the root of a script set,
   8         for example, consider the following files and directories, and
   9         assume you keep files in "list" separated from files
  10         in "sort" (for example the former directory may contain
  11         functions and proofs about lists, while latter sorting algorithms
  12         for lists):
  13 </p><pre class="programlisting">
  14   list/
  15     list.ma (* depending just on the standard library *)
  16     utils/
  17       swap.ma (* including list.ma *)
  18   sort/
  19     qsort.ma (* including utils/swap.ma *)
  20 </pre><p>
  21         To be able to compile properly the contents of "list"
  22         a file called root has to be placed in it. The file should be like
  23         the following snippet.
  24 </p><pre class="programlisting">
  25   baseuri=cic:/matita/mydatastructures
  26 </pre><p>
  27         This file tells Matita that objects generated by
  28         "list.ma" have to be placed in
  29         "cic:/matita/mydatastructures/list" while
  30         objects generated by
  31         "swap.ma" have to be placed in
  32         "cic:/matita/mydatastructures/utils/swap".
  33   </p><p>
  34         Once you created the root file, you must generate a depend file.
  35         Enter the "list" directory (the root of yuor file set)
  36         and type "matitadep". Remember to regenerate the depend file
  37         every time you alter the dependencies of your files (for example
  38         including other scripts).
  39         You can now compile you files typing "matitac".
  40   </p><p>
  41           To compile the "sort" directory, create a root file
  42           in "sort/" like the following one and then run
  43           "matitadep".
  44 </p><pre class="programlisting">
  45   baseuri=cic:/matita/myalgorithms
  46   include_paths=../list
  47 </pre><p>
  48         The include_paths field can declare a list of paths separated by space.
  49         Please omit any "/" from the end of base URIs or paths.
  50   </p></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="authoringinterface"></a>The authoring interface</h3></div></div></div><p><span class="emphasis"><em>TODO</em></span></p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="cicbrowser.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_gettingstarted.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_terms.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Browsing and searching </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 4. Syntax</td></tr></table></div></body></html>