]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/help/C/sec_gettingstarted.xml
New syntax for auto-related tactics and conclude/obtain.
[helm.git] / helm / software / matita / help / C / sec_gettingstarted.xml
index f7d435e70733439a4230046d57cee1ae42fe256f..b0c0a863e55e1a8c9a69602730f360fa48d3bf30 100644 (file)
@@ -3,7 +3,7 @@
 
 <chapter id="sec_gettingstarted">
   <title>Getting started</title>
-  <para> If you are already familiar with the Calculus of (co)Inductive
+  <para> If you are already familiar with the Calculus of (Co)Inductive
   Constructions (CIC) and with interactive theorem provers with procedural
   proof languages (expecially Coq), getting started with Matita is relatively
   easy. You just need to learn how to type Unicode symbols, how to browse
 
   <sect1 id="unicode">
    <title>How to type Unicode symbols</title>
-   Unicode characters can be typed in several ways:
+   <para>Unicode characters can be typed in several ways:</para>
     <itemizedlist>
-     <listitem>Using the &quot;Shift+Ctrl+Unicode code&quot; standard
-      Gnome shortcut. E.g. Shift+Ctrl+3a9 generates &quot;Ω&quot;.
+      <listitem><para>Using the &quot;Ctrl+Shift+Unicode code&quot; standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates &quot;Ω&quot;.</para>
      </listitem>
-     <listitem>Typing the ligature &quot;\name&quot; where &quot;name&quot;
+     <listitem><para>Typing the ligature &quot;\name&quot; where &quot;name&quot;
       is a standard Unicode or LaTeX name for the character. Pressing
       &quot;Alt+L&quot; just after the last character of the name converts
       the ligature to the Unicode symbol. This operation is
       not required since Matita understands also the &quot;\name&quot;
       sequences. E.g. &quot;\Omega&quot; followed by Alt+L generates
-      &quot;Ω&quot;.
+      &quot;Ω&quot;.</para>
      </listitem>
-     <listitem>Typing one of the following ligatures (and opzionally converting
-      the ligature to the Unicode character has described before):
-      &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for &quot;→&quot;);
-      &quot;->&quot; (which stands for &quot;⇒&quot;).
+     <listitem><para>Typing one of the following ligatures (and optionally
+         converting the ligature to the Unicode character has described before):
+         &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for
+         &quot;→&quot;); &quot;=>&quot; (which stands for &quot;⇒&quot;).</para>
      </listitem>
     </itemizedlist>
   </sect1>
      an action in the drop down menu right of it.</para>
     <sect3 id="locate">
      <title>Searching by name</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="hint">
      <title>List of lemmas that can be applied</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="match">
      <title>Searching by exact match</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="elim">
      <title>List of elimination principles for a given type</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="instance">
      <title>Searching by instantiation</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
    </sect2>
   </sect1>
   <sect1 id="authoring">
    <title>Authoring</title>
-   &TODO;
-  </sect1>
+   <sect2 id="compilation">
+   <title>How to compile a script</title>
+   <para>
+       Scripts are compiled to base URIs. Base URIs are of the form
+       &quot;cic:/matita/path&quot; and are given once for all for a set
+       of scripts using the &quot;root&quot; file. 
+   </para>
+   <para>
+       A &quot;root&quot; file has to be placed in the root of a script set,
+       for example, consider the following files and directories, and
+       assume you keep files in &quot;list&quot; separated from files
+       in &quot;sort&quot; (for example the former directory may contain
+       functions and proofs about lists, while latter sorting algorithms
+       for lists):
+<programlisting><![CDATA[
+  list/
+    list.ma (* depending just on the standard library *)
+    utils/
+      swap.ma (* including list.ma *)
+  sort/
+    qsort.ma (* including utils/swap.ma *)
+]]></programlisting>
+       To be able to compile properly the contents of &quot;list&quot;
+       a file called root has to be placed in it. The file should be like
+       the following snippet.
+<programlisting><![CDATA[
+  baseuri=cic:/matita/mydatastructures
+]]></programlisting>
+       This file tells &appname; that objects generated by 
+       &quot;list.ma&quot; have to be placed in 
+       &quot;cic:/matita/mydatastructures/list&quot; while 
+       objects generated by 
+       &quot;swap.ma&quot; have to be placed in 
+       &quot;cic:/matita/mydatastructures/utils/swap&quot;.
+  </para>
+  <para>
+       Once you created the root file, you must generate a depend file.
+       Enter the &quot;list&quot; directory (the root of yuor file set)
+       and type &quot;matitadep&quot;. Remember to regenerate the depend file
+       every time you alter the dependencies of your files (for example 
+       including other scripts).
+       You can now compile you files typing &quot;matitac&quot;.
+  </para>
+  <para>
+         To compile the &quot;sort&quot; directory, create a root file
+         in &quot;sort/&quot; like the following one and then run 
+         &quot;matitadep&quot;.
+<programlisting><![CDATA[
+  baseuri=cic:/matita/myalgorithms
+  include_paths=../list
+]]></programlisting>
+       The include_paths field can declare a list of paths separated by space.
+       Please omit any &quot;/&quot; from the end of base URIs or paths.
+  </para>
+ </sect2>
+   <sect2 id="authoringinterface">
+    <title>The authoring interface</title>
+    <para>&TODO;</para>
+   </sect2>
+ </sect1>
 </chapter>
 
+