From: Enrico Tassi Date: Sun, 6 Jan 2008 21:43:28 +0000 (+0000) Subject: better documentation both with -h and with F1 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=54e4c7dc896732bafcd907b0380d59efa0a181b7;p=helm.git better documentation both with -h and with F1 --- diff --git a/matita/help/C/figures/developments.png b/matita/help/C/figures/developments.png deleted file mode 100644 index f72458940..000000000 Binary files a/matita/help/C/figures/developments.png and /dev/null differ diff --git a/matita/help/C/sec_commands.xml b/matita/help/C/sec_commands.xml index 5e55de999..4fe77d7b7 100644 --- a/matita/help/C/sec_commands.xml +++ b/matita/help/C/sec_commands.xml @@ -254,8 +254,7 @@ On the contrary, theorem and definitions declared in a file can be immediately used without including it. The file s is automatically compiled - if it is not compiled yet and if it is handled by a - development. + if it is not compiled yet. @@ -282,36 +281,6 @@ - - set - set "baseuri" "s" - - - - Synopsis: - - set &qstring; &qstring; - - - - Action: - - Sets to s the baseuri of all the - theorems and definitions stated in the current file. - The baseuri should be a/b/c/foo - if the file is named foo and it is in - the subtree a/b/c of the current - development. - This requirement is not enforced, but it could be in the future. - - Currently, baseuri is the only - property that can be set even if the parser accepts - arbitrary property names. - - - - - whelp whelp locate "s" diff --git a/matita/help/C/sec_gettingstarted.xml b/matita/help/C/sec_gettingstarted.xml index 0066449b0..3b9af3e30 100644 --- a/matita/help/C/sec_gettingstarted.xml +++ b/matita/help/C/sec_gettingstarted.xml @@ -88,133 +88,27 @@ Authoring - - How to use developments + + How to compile a script - 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. - - 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. - - - The "Developments..." item the File menu (or pressing - Ctrl+D) opens the Developments window. - -
The Developments window - - - - - Screenshot of the Developments window. - -
- - Developments window buttons - New - - - To create a new Development the user needs to specify a name - - 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. - - - 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: - - all - - - Build the whole development. - - - - clean - - - Cleans the whole development. - - - - cleanall - - - 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. - - - - scriptname.mo - - - Compiles "scriptname.ma" - - - - - - - - Delete - - - Decompiles the whole development and removes it. - - - - Build - - - Compiles all the scripts in the development. - - - - Clean - - - Decompiles the whole development. - - - - Publish - - - 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). - - - - Close - - - Closes the Developments window - - - - - The authoring interface diff --git a/matita/library/depends b/matita/library/depends index 199b1e9a7..40cddf02f 100644 --- a/matita/library/depends +++ b/matita/library/depends @@ -1,89 +1,89 @@ -higher_order_defs/ordering.ma logic/equality.ma -higher_order_defs/functions.ma logic/equality.ma -higher_order_defs/relations.ma logic/connectives.ma -decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma -decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma -decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma -decidable_kit/fgraph.ma decidable_kit/fintype.ma -decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma -decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma -Fsub/part1a_inversion.ma Fsub/defn.ma -Fsub/defn.ma Fsub/util.ma -Fsub/util.ma list/list.ma logic/equality.ma nat/compare.ma -Fsub/part1a.ma Fsub/defn.ma -technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma -Q/q.ma Z/compare.ma Z/plus.ma -Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma -nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma -nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma -nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma -nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma -nat/plus.ma nat/nat.ma -nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma -nat/orders.ma logic/connectives.ma higher_order_defs/ordering.ma nat/nat.ma -nat/map_iter_p.ma nat/count.ma nat/permutation.ma -nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma -nat/nat.ma higher_order_defs/functions.ma -nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma -nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma -nat/factorization.ma nat/ord.ma -nat/lt_arith.ma nat/div_and_mod.ma -nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma -nat/gcd_properties1.ma nat/gcd.ma -nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma -nat/div_and_mod_diseq.ma nat/lt_arith.ma -nat/times.ma nat/plus.ma -nat/le_arith.ma nat/orders.ma nat/times.ma -nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma -nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma -nat/chebyshev_thm.ma nat/neper.ma -nat/gcd.ma nat/lt_arith.ma nat/primes.ma -nat/minimization.ma nat/minus.ma -nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma -nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma -nat/binomial.ma nat/factorial2.ma nat/iteration2.ma -nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma -nat/factorial.ma nat/le_arith.ma -nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma -nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma -nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma -nat/minus.ma nat/compare.ma nat/le_arith.ma -nat/congruence.ma nat/primes.ma nat/relevant_equations.ma -nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma -nat/factorial2.ma nat/exp.ma nat/factorial.ma -nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma -nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma -logic/connectives2.ma higher_order_defs/relations.ma -logic/coimplication.ma logic/connectives.ma -logic/connectives.ma -logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma -list/list.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma -list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma -demo/power_derivative.ma nat/nat.ma nat/compare.ma nat/orders.ma nat/plus.ma -demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma -algebra/CoRN/SetoidFun.ma algebra/CoRN/Setoids.ma higher_order_defs/relations.ma -algebra/CoRN/Setoids.ma Z/plus.ma datatypes/constructors.ma higher_order_defs/relations.ma logic/equality.ma nat/nat.ma -algebra/CoRN/SemiGroups.ma algebra/CoRN/SetoidInc.ma -algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma -algebra/monoids.ma algebra/semigroups.ma -algebra/semigroups.ma higher_order_defs/functions.ma -algebra/finite_groups.ma nat/relevant_equations.ma algebra/groups.ma -algebra/groups.ma logic/connectives.ma algebra/monoids.ma datatypes/bool.ma nat/compare.ma nat/le_arith.ma -datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma -datatypes/compare.ma -datatypes/constructors.ma logic/equality.ma -assembly/extra.ma list/list.ma nat/div_and_mod.ma nat/primes.ma -assembly/exadecimal.ma assembly/extra.ma -assembly/vm.ma assembly/byte.ma -assembly/byte.ma assembly/exadecimal.ma -assembly/test.ma assembly/vm.ma -Z/z.ma datatypes/bool.ma nat/nat.ma -Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma -Z/compare.ma Z/orders.ma nat/compare.ma -Z/plus.ma Z/z.ma nat/minus.ma -Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma -Z/orders.ma logic/connectives.ma Z/z.ma nat/orders.ma -Z/times.ma Z/plus.ma nat/lt_arith.ma -Z/moebius.ma Z/sigma_p.ma nat/factorization.ma -Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma library_notation.ma Q/q.ma Z/compare.ma Z/orders.ma Z/plus.ma Z/times.ma Z/z.ma algebra/finite_groups.ma algebra/groups.ma algebra/monoids.ma algebra/semigroups.ma datatypes/bool.ma datatypes/compare.ma datatypes/constructors.ma higher_order_defs/functions.ma higher_order_defs/ordering.ma higher_order_defs/relations.ma list/list.ma list/sort.ma logic/connectives.ma logic/equality.ma nat/chinese_reminder.ma nat/compare.ma nat/congruence.ma nat/count.ma nat/div_and_mod.ma nat/exp.ma nat/factorial.ma nat/factorization.ma nat/fermat_little_theorem.ma nat/gcd.ma nat/le_arith.ma nat/lt_arith.ma nat/minimization.ma nat/minus.ma nat/nat.ma nat/nth_prime.ma nat/ord.ma nat/orders.ma nat/permutation.ma nat/plus.ma nat/primes.ma nat/relevant_equations.ma nat/sigma_and_pi.ma nat/times.ma nat/totient.ma +Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma +Z/moebius.ma Z/sigma_p.ma nat/factorization.ma +Z/times.ma Z/plus.ma nat/lt_arith.ma +Z/orders.ma logic/connectives.ma Z/z.ma nat/orders.ma +Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma +Z/plus.ma Z/z.ma nat/minus.ma +Z/compare.ma Z/orders.ma nat/compare.ma +Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma +Z/z.ma datatypes/bool.ma nat/nat.ma +assembly/test.ma assembly/vm.ma +assembly/byte.ma assembly/exadecimal.ma +assembly/vm.ma assembly/byte.ma +assembly/exadecimal.ma assembly/extra.ma +assembly/extra.ma list/list.ma nat/div_and_mod.ma nat/primes.ma +datatypes/constructors.ma logic/equality.ma +datatypes/compare.ma +datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma +algebra/groups.ma logic/connectives.ma algebra/monoids.ma datatypes/bool.ma nat/compare.ma nat/le_arith.ma +algebra/finite_groups.ma nat/relevant_equations.ma algebra/groups.ma +algebra/semigroups.ma higher_order_defs/functions.ma +algebra/monoids.ma algebra/semigroups.ma +algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma +algebra/CoRN/SemiGroups.ma algebra/CoRN/SetoidInc.ma +algebra/CoRN/Setoids.ma Z/plus.ma datatypes/constructors.ma higher_order_defs/relations.ma logic/equality.ma nat/nat.ma +algebra/CoRN/SetoidFun.ma algebra/CoRN/Setoids.ma higher_order_defs/relations.ma +demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma +demo/power_derivative.ma nat/nat.ma nat/compare.ma nat/orders.ma nat/plus.ma +list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma +list/list.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma +logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma +logic/connectives.ma +logic/coimplication.ma logic/connectives.ma +logic/connectives2.ma higher_order_defs/relations.ma +nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma +nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma +nat/factorial2.ma nat/exp.ma nat/factorial.ma +nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma +nat/congruence.ma nat/primes.ma nat/relevant_equations.ma +nat/minus.ma nat/compare.ma nat/le_arith.ma +nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma +nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma +nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma +nat/factorial.ma nat/le_arith.ma +nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma +nat/binomial.ma nat/factorial2.ma nat/iteration2.ma +nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma +nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma +nat/minimization.ma nat/minus.ma +nat/gcd.ma nat/lt_arith.ma nat/primes.ma +nat/chebyshev_thm.ma nat/neper.ma +nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma +nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma +nat/le_arith.ma nat/orders.ma nat/times.ma +nat/times.ma nat/plus.ma +nat/div_and_mod_diseq.ma nat/lt_arith.ma +nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma +nat/gcd_properties1.ma nat/gcd.ma +nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma +nat/lt_arith.ma nat/div_and_mod.ma +nat/factorization.ma nat/ord.ma +nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma +nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma +nat/nat.ma higher_order_defs/functions.ma +nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma +nat/map_iter_p.ma nat/count.ma nat/permutation.ma +nat/orders.ma logic/connectives.ma higher_order_defs/ordering.ma nat/nat.ma +nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma +nat/plus.ma nat/nat.ma +nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma +nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma +nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma +nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma +Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma +Q/q.ma Z/compare.ma Z/plus.ma +technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma +Fsub/part1a.ma Fsub/defn.ma +Fsub/util.ma list/list.ma logic/equality.ma nat/compare.ma +Fsub/defn.ma Fsub/util.ma +Fsub/part1a_inversion.ma Fsub/defn.ma +decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma +decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma +decidable_kit/fgraph.ma decidable_kit/fintype.ma +decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma +decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma +decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma +higher_order_defs/relations.ma logic/connectives.ma +higher_order_defs/functions.ma logic/equality.ma +higher_order_defs/ordering.ma logic/equality.ma diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index 789573c06..03de96b5f 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -45,7 +45,6 @@ let conffile = ref BuildTimeConf.matita_conf let registry_defaults = [ "matita.debug", "false"; "matita.external_editor", "gvim -f -c 'go %p' %f"; - "matita.preserve", "false"; (* FIXME, inutile pure lei *) "matita.profile", "true"; "matita.system", "false"; "matita.verbose", "false"; @@ -127,76 +126,29 @@ let _ = List.iter (fun (name, s) -> Hashtbl.replace usages name s) [ "matitac", - Printf.sprintf "MatitaC v%s + Printf.sprintf "Matita batch compiler v%s Usage: matitac [ OPTION ... ] FILE Options:" BuildTimeConf.version; - "gragrep", - Printf.sprintf "Grafite Grep v%s -Usage: gragrep [ -r ] PATH -Options:" - BuildTimeConf.version; - "matitaprover", - Printf.sprintf "Matita's prover v%s + "matitaprover", + Printf.sprintf "Matita (TPTP) prover v%s Usage: matitaprover [ -tptppath ] FILE.p Options:" BuildTimeConf.version; "matita", - Printf.sprintf "Matita v%s -Usage: matita [ OPTION ... ] [ FILE ... ] -Options:" - BuildTimeConf.version; - "cicbrowser", - Printf.sprintf - "CIC Browser v%s -Usage: cicbrowser [ URL | WHELP QUERY ] + Printf.sprintf "Matita interactive theorem prover v%s +Usage: matita [ OPTION ... ] [ FILE ] Options:" BuildTimeConf.version; "matitadep", - Printf.sprintf "MatitaDep v%s -Usage: matitadep [ OPTION ... ] FILE ... + Printf.sprintf "Matita depency file generator v%s +Usage: matitadep [ OPTION ... ] Options:" BuildTimeConf.version; "matitaclean", Printf.sprintf "MatitaClean v%s Usage: matitaclean all - matitaclean [ (FILE | URI) ... ] -Options:" - BuildTimeConf.version; - "matitamake", - Printf.sprintf "MatitaMake v%s -Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build) - init - Parameters: name (the name of the development, required) - root (the directory in which the delopment is rooted, - optional, default is current working directory) - Description: tells matitamake that a new development radicated - in the current working directory should be handled. - clean - Parameters: name (the name of the development to destroy, optional) - If omitted the development that holds the current working - directory is used (if any). - Description: clean the develpoment. - list - Parameters: - Description: lists the known developments and their roots. - destroy - Parameters: name (the name of the development to destroy, required) - Description: deletes a development (only from matitamake metadat, no - .ma files will be deleted). - build - Parameters: name (the name of the development to build, required) - Description: completely builds the develpoment. - publish - Parameters: name (the name of the development to publish, required) - Description: cleans the development in the user space, rebuilds it - in the system space ('ro' repositories, that for this operation - becames writable). -Notes: - If target is omitted an 'all' will be used as the default. - With -build you can build a development wherever it is. - If you specify a target it implicitly refers to the development that - holds the current working directory (if any). + matitaclean ( FILE | URI ) Options:" BuildTimeConf.version; ] @@ -219,7 +171,6 @@ let parse_cmdline init_status = wants [Registry] init_status; let includes = ref [] in let default_includes = [ - "."; BuildTimeConf.stdlib_dir_devel; BuildTimeConf.stdlib_dir_installed ; ] in @@ -259,9 +210,6 @@ let parse_cmdline init_status = "-profile-only", Arg.String (fun rex -> Helm_registry.set "matita.profile_only" rex), "Activates only profiler with label matching the provided regex"; - "-preserve", - Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true), - "Turns off automatic baseuri cleaning"; "-system", Arg.Unit (fun () -> Helm_registry.set_bool "matita.system" true), ("Act on the system library instead of the user one" diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 3c3d421a5..a17845331 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -110,7 +110,6 @@ let get_include_paths options = let rec compile options fname = (* initialization, MOVE OUTSIDE *) let matita_debug = Helm_registry.get_bool "matita.debug" in - let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in (* sanity checks *) let include_paths = get_include_paths options in let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in @@ -125,7 +124,7 @@ let rec compile options fname = (Printf.sprintf "uri %s belongs to a read-only repository" baseuri); (* cleanup of previously compiled objects *) if (not (Http_getter_storage.is_empty ~local:true baseuri) || - LibraryClean.db_uris_of_baseuri baseuri <> []) && clean_baseuri + LibraryClean.db_uris_of_baseuri baseuri <> []) then begin HLog.message ("baseuri " ^ baseuri ^ " is not empty"); HLog.message ("cleaning baseuri " ^ baseuri); diff --git a/matita/matitadep.ml b/matita/matitadep.ml index 42034c1a8..cf1519eae 100644 --- a/matita/matitadep.ml +++ b/matita/matitadep.ml @@ -76,8 +76,9 @@ let main () = Sys.chdir (Filename.dirname x); HExtlib.find ~test:(fun x -> Filename.check_suffix x ".ma") "." | _ -> - prerr_endline ("Too many roots: " ^ String.concat ", " roots); - prerr_endline ("Enter one of these directories and retry"); + let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in + prerr_endline ("Too many roots found:\n\t" ^ String.concat "\n\t" roots); + prerr_endline ("\nEnter one of these directories and retry"); exit 1 in let ma_files = args in