From c780c9756b67d116b1d5b5149ae758fa613c5fe6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 5 Jan 2008 16:55:25 +0000 Subject: [PATCH] some work on making the compiler command line cleaner, moved the .ma instantiation of the Make module in matitacLib. still not working: ./matitac library/nat/plus/ma while should work: ../matitac nat/plus.ma --- components/extlib/hExtlib.ml | 27 +++++++---- components/extlib/hExtlib.mli | 8 +++- matita/library/depends | 89 +++++++++++++++++++++++++++++++++++ matita/library/makefile | 39 --------------- matita/library/root | 1 + matita/matitaInit.ml | 1 + matita/matitac.ml | 60 +++++++---------------- matita/matitacLib.ml | 35 +++++++++++++- matita/matitacLib.mli | 7 ++- 9 files changed, 172 insertions(+), 95 deletions(-) create mode 100644 matita/library/depends delete mode 100644 matita/library/makefile create mode 100644 matita/library/root diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml index c32ed0bed..53d8c74e8 100644 --- a/components/extlib/hExtlib.ml +++ b/components/extlib/hExtlib.ml @@ -452,15 +452,26 @@ let find_in paths path = 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 = diff --git a/components/extlib/hExtlib.mli b/components/extlib/hExtlib.mli index 0d8d0aeff..73450ae11 100644 --- a/components/extlib/hExtlib.mli +++ b/components/extlib/hExtlib.mli @@ -120,6 +120,12 @@ val raise_localized_exception: offset:int -> Stdpp.location -> exn -> 'a (* 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 diff --git a/matita/library/depends b/matita/library/depends new file mode 100644 index 000000000..199b1e9a7 --- /dev/null +++ b/matita/library/depends @@ -0,0 +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 diff --git a/matita/library/makefile b/matita/library/makefile deleted file mode 100644 index ec9f8cb26..000000000 --- a/matita/library/makefile +++ /dev/null @@ -1,39 +0,0 @@ -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) diff --git a/matita/library/root b/matita/library/root new file mode 100644 index 000000000..e6f78ade0 --- /dev/null +++ b/matita/library/root @@ -0,0 +1 @@ +baseuri=cic:/matita diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index 7bdf36a1a..789573c06 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -52,6 +52,7 @@ let registry_defaults = [ "matita.paste_unicode_as_tex", "false"; "matita.noinnertypes", "false"; "matita.do_heavy_checks", "true"; + "matita.moo", "true"; ] let set_registry_values = diff --git a/matita/matitac.ml b/matita/matitac.ml index 8f8a19b2d..968bdf505 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -50,8 +50,6 @@ let out_preamble och (path, lines) = 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 @@ -91,68 +89,44 @@ let main_compiler () = 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 = " Dump with expanded macros to " in MatitaInit.add_cmdline_spec ["-dump", Arg.String dump, dump_msg]; main_compiler () +;; let _ = main () diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index ee7a2eae5..7bc3a1b7e 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -69,7 +69,8 @@ let pp_times fname rc big_bang = 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 "OK" else "FAIL" in + let rc,rcascii = + if rc then "OK","Ok" else "FAIL","Fail" in let times = let fmt t = let seconds = int_of_float t in @@ -82,7 +83,8 @@ let pp_times fname rc big_bang = 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 = @@ -220,3 +222,32 @@ let rec compile fname = 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) + diff --git a/matita/matitacLib.mli b/matita/matitacLib.mli index 1fd12cbdb..b126df3a1 100644 --- a/matita/matitacLib.mli +++ b/matita/matitacLib.mli @@ -23,7 +23,10 @@ * 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 + -- 2.39.2