"matita.profile", "true";
"matita.system", "false";
"matita.verbosity", "1";
+ "matita.bench", "false";
(** verbosity level: 1 is the default, 0 is intuitively "quiet", > 1 is
* intuitively verbose *)
]
if not (already_configured [Getter;Environment] init_status) then
begin
Http_getter.init ();
+ if Helm_registry.get_bool "matita.system" then
+ Http_getter_storage.activate_system_mode ();
CicEnvironment.set_trust (* environment trust *)
(let trust =
Helm_registry.get_opt_default Helm_registry.get_bool
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
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.
let parse_cmdline init_status =
if not (already_configured [CmdLine] init_status) then begin
- let includes = ref [ BuildTimeConf.stdlib_dir ] in
+ let includes = ref [
+ BuildTimeConf.stdlib_dir_installed ;
+ BuildTimeConf.stdlib_dir_devel ]
+ in
let args = ref [] in
let add_l l = fun s -> l := s :: !l in
let reduce_verbosity () =
"-noprofile",
Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
"Turns off profiling printings";
+ "-bench",
+ Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true),
+ "Turns on parsable output on stdout, that is timings for matitac...";
"-preserve",
Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true),
"Turns off automatic baseuri cleaning";
let fill_registry () =
status := fill_registry !status
+;;
+Inversion_principle.init ()