raise
(Failure "find_in")
;;
-
+
+let is_prefix_of_aux d1 d2 =
+ let len1 = String.length d1 in
+ let len2 = String.length d2 in
+ if len2 < len1 then
+ false, len1, len2
+ else
+ let pref = String.sub d2 0 len1 in
+ pref = d1 && (len1 = len2 || d1.[len1-1] = '/' || d2.[len1] = '/'), len1, len2
+
let is_prefix_of d1 d2 =
- let len1 = String.length d1 in
- let len2 = String.length d2 in
- if len2 < len1 then
- false
- else
- let pref = String.sub d2 0 len1 in
- pref = d1 && (len1 = len2 || d2.[len1] = '/')
+ let b,_,_ = is_prefix_of_aux d1 d2 in b
+;;
+
+let chop_prefix prefix s =
+ let b,lp,ls = is_prefix_of_aux prefix s in
+ if b then
+ String.sub s lp (ls - lp)
+ else
+ s
;;
let touch s =
(* size in KB (SLOW) *)
val estimate_size: 'a -> int
-(* is_prefix_of [prefix] [string] *)
+(* is_prefix_of [prefix] [string], in terms of dirs:
+ * foo/bar/ is prefix of foo/bar/baz
+ * foo/bar is prefix of foo/bar/baz
+ * foo/b isn't of foo/bar/baz
+ * foo/bar is prefix of foo/bar
+ *)
val is_prefix_of: string -> string -> bool
+val chop_prefix: string -> string -> string
val touch: string -> unit
--- /dev/null
+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
+++ /dev/null
-H=@
-
-RT_BASEDIR=../
-OPTIONS=-bench
-MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
-CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS)
-MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
-CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS)
-
-devel:=$(shell basename `pwd`)
-
-ifneq "$(SRC)" ""
- XXX="SRC=$(SRC)"
-endif
-
-all: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
-clean: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
-cleanall: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
-
-all.opt opt: preall.opt
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
-clean.opt: preall.opt
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
-cleanall.opt: preall.opt
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
-
-%.mo: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
-%.mo.opt: preall.opt
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
-
-preall:
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
-
-preall.opt:
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel)
--- /dev/null
+baseuri=cic:/matita
"matita.paste_unicode_as_tex", "false";
"matita.noinnertypes", "false";
"matita.do_heavy_checks", "true";
+ "matita.moo", "true";
]
let set_registry_values =
print lines;
out_line_comment och "This file was automatically generated: do not edit"
-(* from matitacLib *)
-
let pp_ast_statement st =
GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
~map_unicode_to_tex:(Helm_registry.get_bool
MatitaInit.initialize_all ();
(* targets and deps *)
let targets = Helm_registry.get_list Helm_registry.string "matita.args" in
- let deps =
+ let deps, target =
match targets with
| [] ->
(match Librarian.find_roots_in_dir (Sys.getcwd ()) with
| [x] ->
- Make.load_deps_file (Filename.dirname x ^ "/depends")
+ Make.load_deps_file (Filename.dirname x ^ "/depends"), []
| [] ->
HLog.error "No targets and no root found"; exit 1
| roots ->
HLog.error ("Too many roots found, move into one and retry: "^
String.concat ", " roots);exit 1);
- | hd::_ ->
- let root, _, _ = Librarian.baseuri_of_script hd in
- Make.load_deps_file (root ^ "/depends")
+ | [hd] ->
+ let root, buri, file = Librarian.baseuri_of_script hd in
+ Make.load_deps_file (root ^ "/depends"),
+ let target = HExtlib.chop_prefix (root^"/") file in
+ HLog.debug ("Compiling target '" ^ target ^ "' with base uri '"^buri^"'");
+ [target]
+ | _ -> HLog.error "Only one target (or none) can be specified.";exit 1
in
(* must be called after init since args are set by cmdline parsing *)
let system_mode = Helm_registry.get_bool "matita.system" in
if system_mode then HLog.message "Compiling in system space";
if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
(* here we go *)
- let module F =
- struct
- type source_object = string
- type target_object = string
- let string_of_source_object s = s;;
- let string_of_target_object s = s;;
-
- let target_of mafile =
- let _,baseuri,_ = Librarian.baseuri_of_script mafile in
- LibraryMisc.obj_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true
- ;;
-
- let mtime_of_source_object s =
- try Some (Unix.stat s).Unix.st_mtime
- with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s ->
- raise (Failure ("Unable to stat a source file: " ^ s))
- ;;
-
- let mtime_of_target_object s =
- try Some (Unix.stat s).Unix.st_mtime
- with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
- ;;
-
- let build = MatitacLib.compile;;
- end
- in
- let module Make = Make.Make(F) in
- Make.make deps targets
+ MatitacLib.Make.make deps target
;;
let main () =
- Helm_registry.set_bool "matita.moo" true;
- match Filename.basename Sys.argv.(0) with
- |"matitadep" |"matitadep.opt" |"matitadep.opt.static" ->Matitadep.main()
- |"matitaclean"|"matitaclean.opt"|"matitaclean.opt.static"->Matitaclean.main()
- |"matitaprover"|"matitaprover.opt"|"matitaprover.opt.static"->Matitaprover.main()
- |"matitawiki"|"matitawiki.opt" ->MatitaWiki.main()
- | _ ->
+ let bin = Filename.basename Sys.argv.(0) in
+ if Pcre.pmatch ~pat:"^matitadep" bin then Matitadep.main ()
+ else if Pcre.pmatch ~pat:"^matitaclean" bin then Matitaclean.main ()
+ else if Pcre.pmatch ~pat:"^matitaprover" bin then Matitaprover.main ()
+ else if Pcre.pmatch ~pat:"^matitawiki" bin then MatitaWiki.main ()
+ else
let dump_msg = "<filename> Dump with expanded macros to <filename>" in
MatitaInit.add_cmdline_spec ["-dump", Arg.String dump, dump_msg];
main_compiler ()
+;;
let _ = main ()
let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
let r = Unix.gettimeofday () -. big_bang in
let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
- let rc = if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
+ let rc,rcascii =
+ if rc then "\e[0;32mOK\e[0m","Ok" else "\e[0;31mFAIL\e[0m","Fail" in
let times =
let fmt t =
let seconds = int_of_float t in
in
let s = Printf.sprintf "%-4s %s %s" rc times extra in
print_endline s;
- flush stdout
+ flush stdout;
+ HLog.message ("Compilation of "^Filename.basename fname^": "^rc)
;;
let cut prefix s =
clean_exit baseuri false
;;
+module F =
+ struct
+ type source_object = string
+ type target_object = string
+ let string_of_source_object s = s;;
+ let string_of_target_object s = s;;
+
+ let target_of mafile =
+ let _,baseuri,_ = Librarian.baseuri_of_script mafile in
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true
+ ;;
+
+ let mtime_of_source_object s =
+ try Some (Unix.stat s).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s ->
+ raise (Failure ("Unable to stat a source file: " ^ s))
+ ;;
+
+ let mtime_of_target_object s =
+ try Some (Unix.stat s).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
+ ;;
+
+ let build = compile;;
+ end
+
+module Make = Make.Make(F)
+
* http://helm.cs.unibo.it/
*)
-val compile: string -> bool
-
(* this callback is called on the expansion of every inline macro *)
val set_callback: (string -> unit) -> unit
+
+module Make : sig
+ val make: (string * string list) list -> string list -> unit
+end
+
projects / helm.git / commitdiff