From df666eb58afe0b312a2c4d41683d7ae4828ee8bd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Jan 2008 09:32:21 +0000 Subject: [PATCH] better doc and root/depends file parsing --- components/library/librarian.ml | 3 +- matita/help/C/sec_gettingstarted.xml | 65 +++++++++++++++++++++------- 2 files changed, 51 insertions(+), 17 deletions(-) diff --git a/components/library/librarian.ml b/components/library/librarian.ml index 9a16e814d..f2268488f 100644 --- a/components/library/librarian.ml +++ b/components/library/librarian.ml @@ -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 ;; diff --git a/matita/help/C/sec_gettingstarted.xml b/matita/help/C/sec_gettingstarted.xml index 3b9af3e30..c6a0daaf5 100644 --- a/matita/help/C/sec_gettingstarted.xml +++ b/matita/help/C/sec_gettingstarted.xml @@ -92,23 +92,56 @@ How to compile a script 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. + "cic:/matita/path" and are given once for all for a set + of scripts using the "root" file. + + 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): + + 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. + + 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". + + + 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". + + + To compile the "sort" directory, create a root file + in "sort/" like the following one and then run + "matitadep". + + The include_paths field can declare a list of paths separated by space. + Please omit any "/" from the end of base URIs or paths. + The authoring interface -- 2.39.2