matita/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 or an
  20                      ASCII art resembling the shape of the character. Pressing
  21       &quot;Alt+L&quot; or Space or Enter just after the last character
  22       of the name converts
  23       the ligature to the Unicode symbol.
  24       E.g. &quot;\Delta&quot; followed by Alt+L generates
  25       &quot;Δ&quot;, while pressing Alt-L after &quot;=>&quot; generates
  26       &quot;⇒&quot;</para>
  27      </listitem>
  28      <listitem>
  29              <para>Typing a symbol and rotating trough its equivalence class
  30                    with Alt-L. E.g. pressing Alt-L after an  &quot;l&quot;
  31                    generates a &quot;λ&quot;, while pressing Alt-L after an
  32                    &quot;→&quot; once generates &quot;⇉&quot; and pressing
  33                    Alt-L again generates &quot;⇒&quot;.
  34          </para>
  35      </listitem>
  36     </itemizedlist>
  37     <para>
  38     The comprehensive list of symbols names or shortcuts and their equivalence
  39     classes is available clicking on the &quot;TeX/UTF-8 table&quot; item
  40     of the &quot;View&quot; menu.
  41     </para>
  42     <para>
  43             There is a memory mechanism related to equivalence classes that
  44             remembers your last choice, making it the default one. For example,
  45             if you use &quot;_&quot; to generate &quot;⎻&quot;
  46             (that is the third choice, after &quot;⎽&quot; and &quot;⎼&quot;),
  47             the next time you type Alt-L
  48             after &quot;_&quot; you immediately get &quot;⎻&quot;.
  49     </para>
  50   </sect1>
  51   <sect1 id="cicbrowser">
  52    <title>Browsing and searching</title>
  53    <para>The CIC browser is used to browse and search the library.
  54     You can open a new CIC browser selecting &quot;New Cic Browser&quot;
  55     from the &quot;View&quot; menu of Matita, or by pressing &quot;F3&quot;.
  56     The CIC browser is similar to a traditional Web browser.</para>
  57    <sect2 id="browsinglib">
  58     <title>Browsing the library</title>
  59     <para>To browse the library, type in the location bar the absolute URI of
  60     the theorem, definition or library fragment you are interested in.
  61     &quot;cic:/&quot; is the root of the library. Contributions developed
  62     in Matita are under &quot;cic:/matita&quot;; all the others are
  63     part of the library of Coq.</para>
  64     <para>Following the hyperlinks it is possible to navigate in the Web
  65     of mathematical notions. Proof are rendered in pseudo-natural language
  66     and mathematical notation is used for formulae. For now, mathematical
  67     notation must be included in the current script to be activated, but we
  68     plan to remove this limitation.</para>
  69    </sect2>
  70    <sect2 id="aboutproof">
  71     <title>Looking at a proof under development</title>
  72     <para>A proof under development is not yet part of the library.
  73      The special URI &quot;about:proof&quot; can be used to browse the
  74      proof currently under development, if there is one.
  75      The &quot;home&quot; button of the CIC browser sets the location bar to
  76      &quot;about:proof&quot;.
  77     </para>
  78    </sect2>
  79    <!--
  80    <sect2 id="whelp">
  81     <title>Searching the library</title>
  82     <para>The query bar of the CIC browser can be used to search the library
  83      of Matita for theorems or definitions that match certain criteria.
  84      The criteria is given by typing a term in the query bar and selecting
  85      an action in the drop down menu right of it.</para>
  86     <sect3 id="locate">
  87      <title>Searching by name</title>
  88      <para>     &TODO;</para>
  89    </sect3>
  90     <sect3 id="hint">
  91      <title>List of lemmas that can be applied</title>
  92      <para>     &TODO;</para>
  93    </sect3>
  94     <sect3 id="match">
  95      <title>Searching by exact match</title>
  96      <para>     &TODO;</para>
  97    </sect3>
  98     <sect3 id="elim">
  99      <title>List of elimination principles for a given type</title>
 100      <para>     &TODO;</para>
 101    </sect3>
 102     <sect3 id="instance">
 103      <title>Searching by instantiation</title>
 104      <para>     &TODO;</para>
 105    </sect3>
 106    </sect2>-->
 107   </sect1>
 108   <sect1 id="authoring">
 109    <title>Authoring</title>
 110    <sect2 id="compilation">
 111    <title>How to compile a script</title>
 112    <para>
 113         Scripts are compiled to base URIs. Base URIs are of the form
 114         &quot;cic:/matita/path&quot; and are given once for all for a set
 115         of scripts using the &quot;root&quot; file.
 116    </para>
 117    <para>
 118         A &quot;root&quot; file has to be placed in the root of a script set,
 119         for example, consider the following files and directories, and
 120         assume you keep files in &quot;list&quot; separated from files
 121         in &quot;sort&quot; (for example the former directory may contain
 122         functions and proofs about lists, while latter sorting algorithms
 123         for lists):
 124 <programlisting><![CDATA[
 125   list/
 126     list.ma (* depending just on the standard library *)
 127     utils/
 128       swap.ma (* including list.ma *)
 129   sort/
 130     qsort.ma (* including utils/swap.ma *)
 131 ]]></programlisting>
 132         To be able to compile properly the contents of &quot;list&quot;
 133         a file called root has to be placed in it. The file should be like
 134         the following snippet.
 135 <programlisting><![CDATA[
 136   baseuri=cic:/matita/mydatastructures
 137 ]]></programlisting>
 138         This file tells &appname; that objects generated by
 139         &quot;list.ma&quot; have to be placed in
 140         &quot;cic:/matita/mydatastructures/list&quot; while
 141         objects generated by
 142         &quot;swap.ma&quot; have to be placed in
 143         &quot;cic:/matita/mydatastructures/utils/swap&quot;.
 144   </para>
 145   <para>
 146         Once you created the root file, you must generate a depend file.
 147         Enter the &quot;list&quot; directory (the root of yuor file set)
 148         and type &quot;matitadep&quot;. Remember to regenerate the depend file
 149         every time you alter the dependencies of your files (for example
 150         including other scripts).
 151         You can now compile you files typing &quot;matitac&quot;.
 152   </para>
 153   <para>
 154           To compile the &quot;sort&quot; directory, create a root file
 155           in &quot;sort/&quot; like the following one and then run
 156           &quot;matitadep&quot;.
 157 <programlisting><![CDATA[
 158   baseuri=cic:/matita/myalgorithms
 159   include_paths=../list
 160 ]]></programlisting>
 161         The include_paths field can declare a list of paths separated by space.
 162         Please omit any &quot;/&quot; from the end of base URIs or paths.
 163   </para>
 164  </sect2>
 165    <sect2 id="authoringinterface">
 166     <title>The authoring interface</title>
 167     <para>&TODO;</para>
 168    </sect2>
 169  </sect1>
 170 </chapter>
 171
 172