matita/help/C/sec_gettingstarted.xml

   1
   2 <!-- ============= Getting started ============================== -->
   3
   4 <chapter id="sec_gettingstarted">
   5   <title>Getting started</title>
   6   <para> If you are already familiar with the Calculus of (Co)Inductive
   7   Constructions (CIC) and with interactive theorem provers with procedural
   8   proof languages (expecially Coq), getting started with Matita is relatively
   9   easy. You just need to learn how to type Unicode symbols, how to browse
  10   and search the library and how to author a proof script.</para>
  11
  12   <sect1 id="unicode">
  13    <title>How to type Unicode symbols</title>
  14    <para>Unicode characters can be typed in several ways:</para>
  15     <itemizedlist>
  16       <listitem><para>Using the &quot;Ctrl+Shift+Unicode code&quot; standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates &quot;Ω&quot;.</para>
  17      </listitem>
  18      <listitem><para>Typing the ligature &quot;\name&quot; where &quot;name&quot;
  19       is a standard Unicode or LaTeX name for the character. Pressing
  20       &quot;Alt+L&quot; just after the last character of the name converts
  21       the ligature to the Unicode symbol. This operation is
  22       not required since Matita understands also the &quot;\name&quot;
  23       sequences. E.g. &quot;\Omega&quot; followed by Alt+L generates
  24       &quot;Ω&quot;.</para>
  25      </listitem>
  26      <listitem><para>Typing one of the following ligatures (and optionally
  27          converting the ligature to the Unicode character has described before):
  28          &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for
  29          &quot;→&quot;); &quot;=>&quot; (which stands for &quot;⇒&quot;).</para>
  30      </listitem>
  31     </itemizedlist>
  32   </sect1>
  33   <sect1 id="cicbrowser">
  34    <title>Browsing and searching</title>
  35    <para>The CIC browser is used to browse and search the library.
  36     You can open a new CIC browser selecting &quot;New Cic Browser&quot;
  37     from the &quot;View&quot; menu of Matita, or by pressing &quot;F3&quot;.
  38     The CIC browser is similar to a traditional Web browser.</para>
  39    <sect2 id="browsinglib">
  40     <title>Browsing the library</title>
  41     <para>To browse the library, type in the location bar the absolute URI of
  42     the theorem, definition or library fragment you are interested in.
  43     &quot;cic:/&quot; is the root of the library. Contributions developed
  44     in Matita are under &quot;cic:/matita&quot;; all the others are
  45     part of the library of Coq.</para>
  46     <para>Following the hyperlinks it is possible to navigate in the Web
  47     of mathematical notions. Proof are rendered in pseudo-natural language
  48     and mathematical notation is used for formulae. For now, mathematical
  49     notation must be included in the current script to be activated, but we
  50     plan to remove this limitation.</para>
  51    </sect2>
  52    <sect2 id="aboutproof">
  53     <title>Looking at a proof under development</title>
  54     <para>A proof under development is not yet part of the library.
  55      The special URI &quot;about:proof&quot; can be used to browse the
  56      proof currently under development, if there is one.
  57      The &quot;home&quot; button of the CIC browser sets the location bar to
  58      &quot;about:proof&quot;.
  59     </para>
  60    </sect2>
  61    <sect2 id="whelp">
  62     <title>Searching the library</title>
  63     <para>The query bar of the CIC browser can be used to search the library
  64      of Matita for theorems or definitions that match certain criteria.
  65      The criteria is given by typing a term in the query bar and selecting
  66      an action in the drop down menu right of it.</para>
  67     <sect3 id="locate">
  68      <title>Searching by name</title>
  69      <para>     &TODO;</para>
  70    </sect3>
  71     <sect3 id="hint">
  72      <title>List of lemmas that can be applied</title>
  73      <para>     &TODO;</para>
  74    </sect3>
  75     <sect3 id="match">
  76      <title>Searching by exact match</title>
  77      <para>     &TODO;</para>
  78    </sect3>
  79     <sect3 id="elim">
  80      <title>List of elimination principles for a given type</title>
  81      <para>     &TODO;</para>
  82    </sect3>
  83     <sect3 id="instance">
  84      <title>Searching by instantiation</title>
  85      <para>     &TODO;</para>
  86    </sect3>
  87    </sect2>
  88   </sect1>
  89   <sect1 id="authoring">
  90    <title>Authoring</title>
  91    <sect2 id="developments">
  92    <title>How to use developments</title>
  93    <para>
  94      A development is a set of scripts files that are strictly related (i.e.
  95      they depend on each other).  &appname; is able to automatically manage
  96      dependencies among the scripts in a development, compiling them in the
  97      correct order.
  98    </para>
  99    <para>
 100      The include statement can be performed by &appname; only if the mentioned
 101      script is compiled. If both scripts (the one that includes and the included)
 102      are part of the same development, the included script (and recursively all
 103      its dependencies) can be compiled automatically. Dependencies among scripts
 104      belonging to different developments is not implemented yet.
 105    </para>
 106    <para>
 107      The &quot;Developments...&quot; item the File menu (or pressing
 108      Ctrl+D) opens the Developments window.
 109    </para>
 110    <figure><title>The Developments window</title>
 111      <mediaobject>
 112        <imageobject>
 113          <imagedata fileref="figures/developments.png" />
 114        </imageobject>
 115        <textobject><phrase>Screenshot of the Developments window.</phrase></textobject>
 116      </mediaobject>
 117    </figure>
 118    <para>
 119     <variablelist><title>Developments window buttons</title>
 120       <varlistentry><term><filename>New</filename></term>
 121         <listitem>
 122           <para>
 123             To create a new Development the user needs to specify a name<footnote>
 124               <para>
 125                 The name of the Development should be the name of the directory in
 126                 which it lives. This is not a requirement, but the makefile
 127                 automatically generated by matita in the root directory of the
 128                 development will eventually generate a new Development with a name
 129                 that follows this convention. Having more than one development for
 130                 the same set of files is not an issue.
 131               </para>
 132             </footnote>
 133             and the root directory in which all scripts will be placed,
 134             eventually organized in subdirectories. The Development should be
 135             named as the directory in which it lives. A &quot;makefile&quot;
 136             file is placed in the specified root directory. That makefile
 137             supports the following targets:
 138             <variablelist>
 139               <varlistentry><term><filename>all</filename></term>
 140                 <listitem>
 141                   <para>
 142                     Build the whole development.
 143                   </para>
 144                 </listitem>
 145               </varlistentry>
 146               <varlistentry><term><filename>clean</filename></term>
 147                 <listitem>
 148                   <para>
 149                     Cleans the whole development.
 150                   </para>
 151                 </listitem>
 152               </varlistentry>
 153               <varlistentry><term><filename>cleanall</filename></term>
 154                 <listitem>
 155                   <para>
 156                     Resets the user environment (i.e. deleting all the results
 157                     of compilation of every development, including the contents
 158                     of the database). This target should be used only in case
 159                     something goes wrong and &appname; behaves incorrectly.
 160                   </para>
 161                 </listitem>
 162               </varlistentry>
 163               <varlistentry><term><filename>scriptname.mo</filename></term>
 164                 <listitem>
 165                   <para>
 166                     Compiles &quot;scriptname.ma&quot;
 167                   </para>
 168                 </listitem>
 169               </varlistentry>
 170             </variablelist>
 171           </para>
 172         </listitem>
 173       </varlistentry>
 174       <varlistentry><term><filename>Delete</filename></term>
 175         <listitem>
 176           <para>
 177             Decompiles the whole development and removes it.
 178           </para>
 179         </listitem>
 180       </varlistentry>
 181       <varlistentry><term><filename>Build</filename></term>
 182         <listitem>
 183           <para>
 184             Compiles all the scripts in the development.
 185           </para>
 186         </listitem>
 187       </varlistentry>
 188       <varlistentry><term><filename>Clean</filename></term>
 189         <listitem>
 190           <para>
 191             Decompiles the whole development.
 192           </para>
 193         </listitem>
 194       </varlistentry>
 195       <varlistentry><term><filename>Publish</filename></term>
 196         <listitem>
 197           <para>
 198             All the user developments live in the &quot;user&quot; space. That is, the
 199             result of the compilation of scripts is placed in his home directory
 200             and the tuples are placed in personal tables inside the database.
 201             Publishing a development means putting it in the &quot;library&quot; space. This
 202             means putting the result of compilation in the same place where the
 203             standard library lives. This feature will be improved in the future
 204             to support publishing the development in the &quot;distributed
 205             library&quot; space (making your development public).
 206           </para>
 207         </listitem>
 208       </varlistentry>
 209       <varlistentry><term><filename>Close</filename></term>
 210         <listitem>
 211           <para>
 212             Closes the Developments window
 213           </para>
 214         </listitem>
 215       </varlistentry>
 216     </variablelist>
 217     </para>
 218  </sect2>
 219    <sect2 id="authoringinterface">
 220     <title>The authoring interface</title>
 221     <para>&TODO;</para>
 222    </sect2>
 223  </sect1>
 224 </chapter>
 225
 226