From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 8 Jun 2006 12:00:35 +0000 (+0000)
Subject: developments added
X-Git-Tag: 0.4.95@7852~1357
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=357d03db09f8b136b1c049d2c982902112d1cc49;p=helm.git

developments added
---

diff --git a/matita/help/C/sec_gettingstarted.xml b/matita/help/C/sec_gettingstarted.xml
index 5f9dda35a..be9a5f22c 100644
--- a/matita/help/C/sec_gettingstarted.xml
+++ b/matita/help/C/sec_gettingstarted.xml
@@ -90,8 +90,133 @@
    <title>Authoring</title>
    <sect2 id="developments">
    <title>How to use developments</title>
-   <para>   &TODO;</para>
+   <para>
+     A development is a set of scripts files that are strictly related (i.e.
+     they depend on each other).  &appname; is able to automatically manage
+     dependencies among the scripts in a development, compiling them in the
+     correct order. 
+   </para>
+   <para>
+     The include statement can be performed by &appname; 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.
+   </para>
+   <para>
+     The &quot;Developments...&quot; item the File menu (or pressing
+     Ctrl+D) opens the Developments window.
+   </para>
+   <figure><title>The Developments window</title>
+     <mediaobject>
+       <imageobject>
+         <imagedata fileref="developments.png" align="center"/> 
+       </imageobject>
+       <textobject><phrase>Screenshot of the Developments window.</phrase></textobject>
+     </mediaobject>
+   </figure>
+   <para> 
+    <variablelist><title>Developments window buttons</title>
+      <varlistentry><term><filename>New</filename></term>
+        <listitem>
+          <para>
+            To create a new Development the user needs to specify a name<footnote>
+              <para>
+                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.
+              </para>
+            </footnote>
+            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 &quot;makefile&quot;
+            file is placed in the specified root directory. That makefile
+            supports the following targets:
+            <variablelist>
+              <varlistentry><term><filename>all</filename></term>
+                <listitem>
+                  <para>
+                    Build the whole development.
+                  </para>
+                </listitem>
+              </varlistentry>
+              <varlistentry><term><filename>clean</filename></term>
+                <listitem>
+                  <para>
+                    Cleans the whole development.
+                  </para>
+                </listitem>
+              </varlistentry>
+              <varlistentry><term><filename>cleanall</filename></term>
+                <listitem>
+                  <para>
+                    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 &appname; behaves incorrectly.
+                  </para>
+                </listitem>
+              </varlistentry>
+              <varlistentry><term><filename>scriptname.mo</filename></term>
+                <listitem>
+                  <para>
+                    Compiles &quot;scriptname.ma&quot;
+                  </para>
+                </listitem>
+              </varlistentry>
+            </variablelist>
+          </para>
+        </listitem>
+      </varlistentry>
+      <varlistentry><term><filename>Delete</filename></term>
+        <listitem>
+          <para>
+            Decompiles the whole development and removes it.
+          </para>
+        </listitem>
+      </varlistentry>
+      <varlistentry><term><filename>Build</filename></term>
+        <listitem>
+          <para>
+            Compiles all the scripts in the development.
+          </para>
+        </listitem>
+      </varlistentry>
+      <varlistentry><term><filename>Clean</filename></term>
+        <listitem>
+          <para>
+            Decompiles the whole development.
+          </para>
+        </listitem>
+      </varlistentry>
+      <varlistentry><term><filename>Publish</filename></term>
+        <listitem>
+          <para>
+            All the user developments live in the &quot;user&quot; 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 &quot;library&quot; 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 &quot;distributed
+            library&quot; space (making your development public).
+          </para>
+        </listitem>
+      </varlistentry>
+      <varlistentry><term><filename>Close</filename></term>
+        <listitem>
+          <para>
+            Closes the Developments window
+          </para>
+        </listitem>
+      </varlistentry>
+    </variablelist>
+    </para>
  </sect2>
  </sect1>
 </chapter>
 
+