</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="figures/developments.png" />
- </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 on 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>
projects / helm.git / blobdiff