2 <!-- ============= Getting started ============================== -->
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>
13 <title>How to type Unicode symbols</title>
14 <para>Unicode characters can be typed in several ways:</para>
16 <listitem><para>Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω".</para>
18 <listitem><para>Typing the ligature "\name" where "name"
19 is a standard Unicode or LaTeX name for the character. Pressing
20 "Alt+L" 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 "\name"
23 sequences. E.g. "\Omega" followed by Alt+L generates
26 <listitem><para>Typing one of the following ligatures (and optionally
27 converting the ligature to the Unicode character has described before):
28 ":=" (which stands for ≝); "->" (which stands for
29 "→"); "=>" (which stands for "⇒").</para>
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 "New Cic Browser"
37 from the "View" menu of Matita, or by pressing "F3".
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 "cic:/" is the root of the library. Contributions developed
44 in Matita are under "cic:/matita"; 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>
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 "about:proof" can be used to browse the
56 proof currently under development, if there is one.
57 The "home" button of the CIC browser sets the location bar to
58 "about:proof".
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>
68 <title>Searching by name</title>
72 <title>List of lemmas that can be applied</title>
76 <title>Searching by exact match</title>
80 <title>List of elimination principles for a given type</title>
84 <title>Searching by instantiation</title>
89 <sect1 id="authoring">
90 <title>Authoring</title>
91 <sect2 id="developments">
92 <title>How to use developments</title>
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
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.
107 The "Developments..." item the File menu (or pressing
108 Ctrl+D) opens the Developments window.
110 <figure><title>The Developments window</title>
113 <imagedata fileref="figures/developments.png" />
115 <textobject><phrase>Screenshot of the Developments window.</phrase></textobject>
119 <variablelist><title>Developments window buttons</title>
120 <varlistentry><term><filename>New</filename></term>
123 To create a new Development the user needs to specify a name<footnote>
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.
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 "makefile"
136 file is placed in the specified root directory. That makefile
137 supports the following targets:
139 <varlistentry><term><filename>all</filename></term>
142 Build the whole development.
146 <varlistentry><term><filename>clean</filename></term>
149 Cleans the whole development.
153 <varlistentry><term><filename>cleanall</filename></term>
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.
163 <varlistentry><term><filename>scriptname.mo</filename></term>
166 Compiles "scriptname.ma"
174 <varlistentry><term><filename>Delete</filename></term>
177 Decompiles the whole development and removes it.
181 <varlistentry><term><filename>Build</filename></term>
184 Compiles all the scripts in the development.
188 <varlistentry><term><filename>Clean</filename></term>
191 Decompiles the whole development.
195 <varlistentry><term><filename>Publish</filename></term>
198 All the user developments live in the "user" 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 "library" 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 "distributed
205 library" space (making your development public).
209 <varlistentry><term><filename>Close</filename></term>
212 Closes the Developments window
219 <sect2 id="authoringinterface">
220 <title>The authoring interface</title>