On the contrary, theorem and definitions declared in a file can be
immediately used without including it.</para>
<para>The file <command>s</command> is automatically compiled
- if it is not compiled yet and if it is handled by a
- <link linkend="developments">development</link>.
+ if it is not compiled yet.
</para>
</listitem>
</varlistentry>
</variablelist>
</para>
</sect1>
- <sect1 id="command_set">
- <title>set</title>
- <para><userinput>set "baseuri" "s"</userinput></para>
- <para>
- <variablelist>
- <varlistentry>
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">set</emphasis> &qstring; &qstring;</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>Sets to <command>s</command> the baseuri of all the
- theorems and definitions stated in the current file.
- The baseuri should be <command>a/b/c/foo</command>
- if the file is named <command>foo</command> and it is in
- the subtree <command>a/b/c</command> of the current
- <link linkend="developments">development</link>.
- This requirement is not enforced, but it could be in the future.
- </para>
- <para>Currently, <command>baseuri</command> is the only
- property that can be set even if the parser accepts
- arbitrary property names.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
<sect1 id="command_whelp">
<title>whelp</title>
<para><userinput>whelp locate "s"</userinput></para>
</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>
-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
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";
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;
]
wants [Registry] init_status;
let includes = ref [] in
let default_includes = [
- ".";
BuildTimeConf.stdlib_dir_devel;
BuildTimeConf.stdlib_dir_installed ; ]
in
"-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"
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
(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);
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
projects / helm.git / commitdiff
