</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 give once for all for a given set of
+ scripts using the "root" file. For example, imagine a directory
+ "dir1" containing a script file "file1.ma" and a
+ subdirectory "dir2" containing "file2.ma". A
+ regular text file called "root" has to be placed in "dir1"
+ ad must contain a line like "baseuri=cic:/matita/example".
+ Then, running "matitac" from "dir1" will compile
+ both script files, placing objects defined in "file1.ma" in
+ "cic:/matita/example/file1" while objects defined in "file2.ma"
+ are placed in "cic:/matita/example/dir2/file2".
+ Before you can compile the scripts you have to generate a "depend" file
+ running "matitadep" from the root directory.
+ You can divide you work in many roots, just place a proper root file in each of them.
+ If a root depends on files living under another one, you can add an extra line in the root
+ file like "include_paths=../other_root1 ../foo/bar" and "matitac"
+ will enter these patsh to eventually compile needed files.
</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>
</sect2>
<sect2 id="authoringinterface">
<title>The authoring interface</title>
projects / helm.git / blobdiff