1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Authoring</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets V1.78.1" /><link rel="home" href="index.html" title="Matita V0.5.9 User Manual (rev. 0.5.9 )" /><link rel="up" href="sec_gettingstarted.html" title="Chapter 3. Getting started" /><link rel="prev" href="cicbrowser.html" title="Browsing and searching" /><link rel="next" href="sec_terms.html" title="Chapter 4. Syntax" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Authoring</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="cicbrowser.html">Prev</a> </td><th width="60%" align="center">Chapter 3. Getting started</th><td width="20%" align="right"> <a accesskey="n" href="sec_terms.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="authoring"></a>Authoring</h2></div></div></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="compilation"></a>How to compile a script</h3></div></div></div><p>
3 Scripts are compiled to base URIs. Base URIs are of the form
4 "cic:/matita/path" and are given once for all for a set
5 of scripts using the "root" file.
7 A "root" file has to be placed in the root of a script set,
8 for example, consider the following files and directories, and
9 assume you keep files in "list" separated from files
10 in "sort" (for example the former directory may contain
11 functions and proofs about lists, while latter sorting algorithms
13 </p><pre class="programlisting">
15 list.ma (* depending just on the standard library *)
17 swap.ma (* including list.ma *)
19 qsort.ma (* including utils/swap.ma *)
21 To be able to compile properly the contents of "list"
22 a file called root has to be placed in it. The file should be like
23 the following snippet.
24 </p><pre class="programlisting">
25 baseuri=cic:/matita/mydatastructures
27 This file tells Matita that objects generated by
28 "list.ma" have to be placed in
29 "cic:/matita/mydatastructures/list" while
31 "swap.ma" have to be placed in
32 "cic:/matita/mydatastructures/utils/swap".
34 Once you created the root file, you must generate a depend file.
35 Enter the "list" directory (the root of yuor file set)
36 and type "matitadep". Remember to regenerate the depend file
37 every time you alter the dependencies of your files (for example
38 including other scripts).
39 You can now compile you files typing "matitac".
41 To compile the "sort" directory, create a root file
42 in "sort/" like the following one and then run
44 </p><pre class="programlisting">
45 baseuri=cic:/matita/myalgorithms
48 The include_paths field can declare a list of paths separated by space.
49 Please omit any "/" from the end of base URIs or paths.
50 </p></div><div class="sect2"><div class="titlepage"><div><div><h3 class="title"><a id="authoringinterface"></a>The authoring interface</h3></div></div></div><p><span class="emphasis"><em>TODO</em></span></p></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="cicbrowser.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_gettingstarted.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_terms.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Browsing and searching </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 4. Syntax</td></tr></table></div></body></html>