--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0 Manual (rev. 0)" /><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><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>
+ A development is a set of scripts files that are strictly related (i.e.
+ they depend on each other). Matita is able to automatically manage
+ dependencies among the scripts in a development, compiling them in the
+ correct order.
+ </p><p>
+ The include statement can be performed by Matita only if the mentioned
+ script is compiled. If both scripts (the one that includes and the included)
+ are part of the same development, the included script (and recursively all
+ its dependencies) can be compiled automatically. Dependencies among scripts
+ belonging to different developments is not implemented yet.
+ </p><p>
+ The "Developments..." item the File menu (or pressing
+ Ctrl+D) opens the Developments window.
+ </p><div class="figure"><a id="id2520494"></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>
+ </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>
+ To create a new Development the user needs to specify a name<sup>[<a id="id2520538" href="#ftn.id2520538">1</a>]</sup>
+ and the root directory in which all scripts will be placed,
+ eventually organized in subdirectories. The Development should be
+ named as the directory in which it lives. A "makefile"
+ file is placed in the specified root directory. That makefile
+ supports the following targets:
+ </p><div class="variablelist"><dl><dt><span class="term"><code class="filename">all</code></span></dt><dd><p>
+ Build the whole development.
+ </p></dd><dt><span class="term"><code class="filename">clean</code></span></dt><dd><p>
+ Cleans the whole development.
+ </p></dd><dt><span class="term"><code class="filename">cleanall</code></span></dt><dd><p>
+ Resets the user environment (i.e. deleting all the results
+ of compilation of every development, including the contents
+ of the database). This target should be used only in case
+ something goes wrong and Matita behaves incorrectly.
+ </p></dd><dt><span class="term"><code class="filename">scriptname.mo</code></span></dt><dd><p>
+ Compiles "scriptname.ma"
+ </p></dd></dl></div><p>
+ </p></dd><dt><span class="term"><code class="filename">Delete</code></span></dt><dd><p>
+ Decompiles the whole development and removes it.
+ </p></dd><dt><span class="term"><code class="filename">Build</code></span></dt><dd><p>
+ Compiles all the scripts in the development.
+ </p></dd><dt><span class="term"><code class="filename">Clean</code></span></dt><dd><p>
+ Decompiles the whole development.
+ </p></dd><dt><span class="term"><code class="filename">Publish</code></span></dt><dd><p>
+ All the user developments live in the "user" space. That is, the
+ result of the compilation of scripts is placed in his home directory
+ and the tuples are placed in personal tables inside the database.
+ Publishing a development means putting it in the "library" space. This
+ means putting the result of compilation in the same place where the
+ standard library lives. This feature will be improved in the future
+ to support publishing the development in the "distributed
+ library" space (making your development public).
+ </p></dd><dt><span class="term"><code class="filename">Close</code></span></dt><dd><p>
+ Closes the Developments window
+ </p></dd></dl></div><p>
+ </p></div><div class="footnotes"><br /><hr width="100" align="left" /><div class="footnote"><p><sup>[<a id="ftn.id2520538" href="#id2520538">1</a>] </sup>
+ The name of the Development should be the name of the directory in
+ which it lives. This is not a requirement, but the makefile
+ automatically generated by matita in the root directory of the
+ development will eventually generate a new Development with a name
+ that follows this convention. Having more than one development for
+ the same set of files is not an issue.
+ </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>
projects / helm.git / blobdiff