--- /dev/null
+
+<!-- ============= Getting started ============================== -->
+
+<chapter id="sec_gettingstarted">
+ <title>Getting started</title>
+ <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
+ and search the library and how to author a proof script.</para>
+
+ <sect1 id="unicode">
+ <title>How to type Unicode symbols</title>
+ <para>Unicode characters can be typed in several ways:</para>
+ <itemizedlist>
+ <listitem><para>Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω".</para>
+ </listitem>
+ <listitem><para>Typing the ligature "\name" where "name"
+ is a standard Unicode or LaTeX name for the character. Pressing
+ "Alt+L" 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 "\name"
+ sequences. E.g. "\Omega" followed by Alt+L generates
+ "Ω".</para>
+ </listitem>
+ <listitem><para>Typing one of the following ligatures (and optionally
+ converting the ligature to the Unicode character has described before):
+ ":=" (which stands for ≝); "->" (which stands for
+ "→"); "=>" (which stands for "⇒").</para>
+ </listitem>
+ </itemizedlist>
+ </sect1>
+ <sect1 id="cicbrowser">
+ <title>Browsing and searching</title>
+ <para>The CIC browser is used to browse and search the library.
+ You can open a new CIC browser selecting "New Cic Browser"
+ from the "View" menu of Matita, or by pressing "F3".
+ The CIC browser is similar to a traditional Web browser.</para>
+ <sect2 id="browsinglib">
+ <title>Browsing the library</title>
+ <para>To browse the library, type in the location bar the absolute URI of
+ the theorem, definition or library fragment you are interested in.
+ "cic:/" is the root of the library. Contributions developed
+ in Matita are under "cic:/matita"; all the others are
+ part of the library of Coq.</para>
+ <para>Following the hyperlinks it is possible to navigate in the Web
+ of mathematical notions. Proof are rendered in pseudo-natural language
+ and mathematical notation is used for formulae. For now, mathematical
+ notation must be included in the current script to be activated, but we
+ plan to remove this limitation.</para>
+ </sect2>
+ <sect2 id="aboutproof">
+ <title>Looking at a proof under development</title>
+ <para>A proof under development is not yet part of the library.
+ The special URI "about:proof" can be used to browse the
+ proof currently under development, if there is one.
+ The "home" button of the CIC browser sets the location bar to
+ "about:proof".
+ </para>
+ </sect2>
+ <sect2 id="whelp">
+ <title>Searching the library</title>
+ <para>The query bar of the CIC browser can be used to search the library
+ of Matita for theorems or definitions that match certain criteria.
+ The criteria is given by typing a term in the query bar and selecting
+ an action in the drop down menu right of it.</para>
+ <sect3 id="locate">
+ <title>Searching by name</title>
+ <para> &TODO;</para>
+ </sect3>
+ <sect3 id="hint">
+ <title>List of lemmas that can be applied</title>
+ <para> &TODO;</para>
+ </sect3>
+ <sect3 id="match">
+ <title>Searching by exact match</title>
+ <para> &TODO;</para>
+ </sect3>
+ <sect3 id="elim">
+ <title>List of elimination principles for a given type</title>
+ <para> &TODO;</para>
+ </sect3>
+ <sect3 id="instance">
+ <title>Searching by instantiation</title>
+ <para> &TODO;</para>
+ </sect3>
+ </sect2>
+ </sect1>
+ <sect1 id="authoring">
+ <title>Authoring</title>
+ <sect2 id="compilation">
+ <title>How to compile a script</title>
+ <para>
+ Scripts are compiled to base URIs. Base URIs are of the form
+ "cic:/matita/path" and are given once for all for a set
+ of scripts using the "root" file.
+ </para>
+ <para>
+ A "root" 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 "list" separated from files
+ in "sort" (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 "list"
+ 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
+ "list.ma" have to be placed in
+ "cic:/matita/mydatastructures/list" while
+ objects generated by
+ "swap.ma" have to be placed in
+ "cic:/matita/mydatastructures/utils/swap".
+ </para>
+ <para>
+ Once you created the root file, you must generate a depend file.
+ Enter the "list" directory (the root of yuor file set)
+ and type "matitadep". 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 "matitac".
+ </para>
+ <para>
+ To compile the "sort" directory, create a root file
+ in "sort/" like the following one and then run
+ "matitadep".
+<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 "/" from the end of base URIs or paths.
+ </para>
+ </sect2>
+ <sect2 id="authoringinterface">
+ <title>The authoring interface</title>
+ <para>&TODO;</para>
+ </sect2>
+ </sect1>
+</chapter>
+
+
projects / helm.git / blobdiff