]> matita.cs.unibo.it Git - helm.git/commitdiff
better doc and root/depends file parsing
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 7 Jan 2008 09:32:21 +0000 (09:32 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 7 Jan 2008 09:32:21 +0000 (09:32 +0000)
components/library/librarian.ml
matita/help/C/sec_gettingstarted.xml

index 9a16e814d56527354b66d4e8d5d5bdc6477795a3..f2268488f2afbc3ce975578c072a172af1ec72ac 100644 (file)
@@ -38,10 +38,11 @@ let remove_trailing_slash s =
 let load_root_file rootpath =
   let data = HExtlib.input_file rootpath in
   let lines = Str.split (Str.regexp "\n") data in
+  let clean s = Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s) in
   List.map 
     (fun l -> 
       match Str.split (Str.regexp "=") l with
-      | [k;v] -> Pcre.replace ~pat:"^ *" k, Pcre.replace ~pat:" *$" v
+      | [k;v] -> clean k, Http_getter_misc.strip_trailing_slash (clean v)
       | _ -> raise (Failure ("Malformed root file: " ^ rootpath)))
     lines
 ;;
index 3b9af3e30c59ff7a525ce0c4ba01a90b163f775b..c6a0daaf5dc65b51ea9c8c271f56cfa5e6772b93 100644 (file)
    <title>How to compile a script</title>
    <para>
        Scripts are compiled to base URIs. Base URIs are of the form
-       &quot;cic:/matita/path&quot; and are give once for all for a given set of 
-       scripts using the &quot;root&quot; file. For example, imagine a directory
-       &quot;dir1&quot; containing a script file &quot;file1.ma&quot; and a
-       subdirectory &quot;dir2&quot; containing &quot;file2.ma&quot;. A 
-       regular text file called &quot;root&quot; has to be placed in &quot;dir1&quot;
-       ad must contain a line like &quot;baseuri=cic:/matita/example&quot;.
-       Then, running &quot;matitac&quot; from &quot;dir1&quot; will compile
-       both script files, placing objects defined in &quot;file1.ma&quot; in 
-       &quot;cic:/matita/example/file1&quot; while objects defined in &quot;file2.ma&quot;
-       are placed in &quot;cic:/matita/example/dir2/file2&quot;.
-       Before you can compile the scripts you have to generate a &quot;depend&quot; file
-       running &quot;matitadep&quot; 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 &quot;include_paths=../other_root1 ../foo/bar&quot; and &quot;matitac&quot;
-       will enter these patsh to eventually compile needed files.
+       &quot;cic:/matita/path&quot; and are given once for all for a set
+       of scripts using the &quot;root&quot; file. 
    </para>
+   <para>
+       A &quot;root&quot; 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 &quot;list&quot; separated from files
+       in &quot;sort&quot; (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 &quot;list&quot;
+       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 
+       &quot;list.ma&quot; have to be placed in 
+       &quot;cic:/matita/mydatastructures/list&quot; while 
+       objects generated by 
+       &quot;swap.ma&quot; have to be placed in 
+       &quot;cic:/matita/mydatastructures/utils/swap&quot;.
+  </para>
+  <para>
+       Once you created the root file, you must generate a depend file.
+       Enter the &quot;list&quot; directory (the root of yuor file set)
+       and type &quot;matitadep&quot;. 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 &quot;matitac&quot;.
+  </para>
+  <para>
+         To compile the &quot;sort&quot; directory, create a root file
+         in &quot;sort/&quot; like the following one and then run 
+         &quot;matitadep&quot;.
+<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 &quot;/&quot; from the end of base URIs or paths.
+  </para>
  </sect2>
    <sect2 id="authoringinterface">
     <title>The authoring interface</title>