helm/www/matita/docs/manual/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">
   3 <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" href="docbook.css" type="text/css" /><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0&#10; User Manual (rev. 1α)" /><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="../../images/matita-tiny.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" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="authoring"></a>Authoring</h2></div></div></div><div class="sect2" lang="en" xml:lang="en"><div class="titlepage"><div><div><h3 class="title"><a id="developments"></a>How to use developments</h3></div></div></div><p>
   4      A development is a set of scripts files that are strictly related (i.e.
   5      they depend on each other).  Matita is able to automatically manage
   6      dependencies among the scripts in a development, compiling them in the
   7      correct order.
   8    </p><p>
   9      The include statement can be performed by Matita only if the mentioned
  10      script is compiled. If both scripts (the one that includes and the included)
  11      are part of the same development, the included script (and recursively all
  12      its dependencies) can be compiled automatically. Dependencies among scripts
  13      belonging to different developments is not implemented yet.
  14    </p><p>
  15      The "Developments..." item the File menu (or pressing
  16      Ctrl+D) opens the Developments window.
  17    </p><div class="figure"><a id="id2521185"></a><p class="title"><b>Figure 3.1. The Developments window</b></p><div class="mediaobject" align="center"><img src="developments.png" align="middle" alt="Screenshot of the Developments window." /></div></div><p>
  18     </p><div class="variablelist"><p class="title"><b>Developments window buttons</b></p><dl><dt><span class="term"><code class="filename">New</code></span></dt><dd><p>
  19             To create a new Development the user needs to specify a name<sup>[<a id="id2521230" href="#ftn.id2521230">1</a>]</sup>
  20             and the root directory in which all scripts will be placed,
  21             eventually organized in subdirectories. The Development should be
  22             named as the directory in which it lives. A "makefile"
  23             file is placed in the specified root directory. That makefile
  24             supports the following targets:
  25             </p><div class="variablelist"><dl><dt><span class="term"><code class="filename">all</code></span></dt><dd><p>
  26                     Build the whole development.
  27                   </p></dd><dt><span class="term"><code class="filename">clean</code></span></dt><dd><p>
  28                     Cleans the whole development.
  29                   </p></dd><dt><span class="term"><code class="filename">cleanall</code></span></dt><dd><p>
  30                     Resets the user environment (i.e. deleting all the results
  31                     of compilation of every development, including the contents
  32                     of the database). This target should be used only in case
  33                     something goes wrong and Matita behaves incorrectly.
  34                   </p></dd><dt><span class="term"><code class="filename">scriptname.mo</code></span></dt><dd><p>
  35                     Compiles "scriptname.ma"
  36                   </p></dd></dl></div><p>
  37           </p></dd><dt><span class="term"><code class="filename">Delete</code></span></dt><dd><p>
  38             Decompiles the whole development and removes it.
  39           </p></dd><dt><span class="term"><code class="filename">Build</code></span></dt><dd><p>
  40             Compiles all the scripts in the development.
  41           </p></dd><dt><span class="term"><code class="filename">Clean</code></span></dt><dd><p>
  42             Decompiles the whole development.
  43           </p></dd><dt><span class="term"><code class="filename">Publish</code></span></dt><dd><p>
  44             All the user developments live in the "user" space. That is, the
  45             result of the compilation of scripts is placed in his home directory
  46             and the tuples are placed in personal tables inside the database.
  47             Publishing a development means putting it in the "library" space. This
  48             means putting the result of compilation in the same place where the
  49             standard library lives. This feature will be improved in the future
  50             to support publishing the development in the "distributed
  51             library" space (making your development public).
  52           </p></dd><dt><span class="term"><code class="filename">Close</code></span></dt><dd><p>
  53             Closes the Developments window
  54           </p></dd></dl></div><p>
  55     </p></div><div class="footnotes"><br /><hr width="100" align="left" /><div class="footnote"><p><sup>[<a id="ftn.id2521230" href="#id2521230">1</a>] </sup>
  56                 The name of the Development should be the name of the directory in
  57                 which it lives. This is not a requirement, but the makefile
  58                 automatically generated by matita in the root directory of the
  59                 development will eventually generate a new Development with a name
  60                 that follows this convention. Having more than one development for
  61                 the same set of files is not an issue.
  62               </p></div></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>