<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>
<sect1 id="authoring">
<title>Authoring</title>
- <sect2 id="developments">
- <title>How to use developments</title>
+ <sect2 id="compilation">
+ <title>How to compile a script</title>
<para>
- A development is a set of scripts files that are strictly related (i.e.
- they depend on each other). &appname; is able to automatically manage
- dependencies among the scripts in a development, compiling them in the
- correct order.
+ 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>
- The include statement can be performed by &appname; only if the mentioned
- script is compiled. If both scripts (the one that includes and the included)
- are part of the same development, the included script (and recursively all
- its dependencies) can be compiled automatically. Dependencies among scripts
- belonging to different developments is not implemented yet.
- </para>
- <para>
- The "Developments..." item the File menu (or pressing
- Ctrl+D) opens the Developments window.
- </para>
- <figure><title>The Developments window</title>
- <mediaobject>
- <imageobject>
- <imagedata fileref="developments.png" align="center"/>
- </imageobject>
- <textobject><phrase>Screenshot of the Developments window.</phrase></textobject>
- </mediaobject>
- </figure>
- <para>
- <variablelist><title>Developments window buttons</title>
- <varlistentry><term><filename>New</filename></term>
- <listitem>
- <para>
- To create a new Development the user needs to specify a name<footnote>
- <para>
- The name of the Development should be the name of the directory in
- which it lives. This is not a requirement, but the makefile
- automatically generated by matita in the root directory of the
- development will eventually generate a new Development with a name
- that follows this convention. Having more than one development for
- the same set of files is not an issue.
- </para>
- </footnote>
- and the root directory in which all scripts will be placed,
- eventually organized in subdirectories. The Development should be
- named as the directory in which it lives. A "makefile"
- file is placed in the specified root directory. That makefile
- supports the following targets:
- <variablelist>
- <varlistentry><term><filename>all</filename></term>
- <listitem>
- <para>
- Build the whole development.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>clean</filename></term>
- <listitem>
- <para>
- Cleans the whole development.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>cleanall</filename></term>
- <listitem>
- <para>
- Resets the user environment (i.e. deleting all the results
- of compilation of every development, including the contents
- of the database). This target should be used only in case
- something goes wrong and &appname; behaves incorrectly.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>scriptname.mo</filename></term>
- <listitem>
- <para>
- Compiles "scriptname.ma"
- </para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>Delete</filename></term>
- <listitem>
- <para>
- Decompiles the whole development and removes it.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>Build</filename></term>
- <listitem>
- <para>
- Compiles all the scripts in the development.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>Clean</filename></term>
- <listitem>
- <para>
- Decompiles the whole development.
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>Publish</filename></term>
- <listitem>
- <para>
- All the user developments live in the "user" space. That is, the
- result of the compilation of scripts is placed in his home directory
- and the tuples are placed in personal tables inside the database.
- Publishing a development means putting it in the "library" space. This
- means putting the result of compilation in the same place where the
- standard library lives. This feature will be improved in the future
- to support publishing the development in the "distributed
- library" space (making your development public).
- </para>
- </listitem>
- </varlistentry>
- <varlistentry><term><filename>Close</filename></term>
- <listitem>
- <para>
- Closes the Developments window
- </para>
- </listitem>
- </varlistentry>
- </variablelist>
- </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