From b11d278a26840884692cdfb89e168081134d293f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 13 Jul 2005 08:38:00 +0000 Subject: [PATCH] matitamake stuff: - added matitamake - matita.basedir has no /xml (added in save_object_to_disk) - matitadep and matitac take -I to add that path to where includes are searched --- helm/matita/.depend | 11 +- helm/matita/Makefile.in | 13 +- helm/matita/buildTimeConf.ml.in | 3 + helm/matita/matita.conf.xml.sample.in | 2 +- helm/matita/matitaEngine.ml | 51 +++-- helm/matita/matitaEngine.mli | 5 + helm/matita/matitaLog.ml | 1 + helm/matita/matitaLog.mli | 1 + helm/matita/matitaMisc.ml | 5 + helm/matita/matitaMisc.mli | 1 + helm/matita/matitaSync.ml | 2 +- helm/matita/matitacLib.ml | 55 +++-- helm/matita/matitaclean.ml | 15 +- helm/matita/matitacleanLib.ml | 46 ++-- helm/matita/matitadep.ml | 73 +++++- helm/matita/matitamake.ml | 170 ++++++++++++++ helm/matita/matitamakeLib.ml | 207 ++++++++++++++++++ helm/matita/matitamakeLib.mli | 46 ++++ helm/matita/template_makefile.in | 33 +++ helm/matita/tests/interactive/drop.ma | 2 +- helm/matita/tests/interactive/grafite.ma | 10 +- helm/matita/tests/interactive/test5.ma | 2 + helm/matita/tests/interactive/test6.ma | 2 + helm/matita/tests/interactive/test7.ma | 2 + .../matita/tests/interactive/test_instance.ma | 2 + 25 files changed, 688 insertions(+), 72 deletions(-) create mode 100644 helm/matita/matitamake.ml create mode 100644 helm/matita/matitamakeLib.ml create mode 100644 helm/matita/matitamakeLib.mli create mode 100644 helm/matita/template_makefile.in diff --git a/helm/matita/.depend b/helm/matita/.depend index 2f863d6dc..1232842f0 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -54,14 +54,20 @@ matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \ matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \ matitaLog.cmx matitaExcPp.cmx matitaEngine.cmx matitaDb.cmx \ buildTimeConf.cmx matitacLib.cmi -matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaDb.cmi -matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaDb.cmx +matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaDb.cmi \ + buildTimeConf.cmo +matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaDb.cmx \ + buildTimeConf.cmx matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi \ matitacleanLib.cmi matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx \ matitacleanLib.cmi matitadep.cmo: matitaMisc.cmi matitaExcPp.cmi matitadep.cmx: matitaMisc.cmx matitaExcPp.cmx +matitamake.cmo: buildTimeConf.cmo +matitamake.cmx: buildTimeConf.cmx +matitamakeLib.cmo: matitaMisc.cmi buildTimeConf.cmo matitamakeLib.cmi +matitamakeLib.cmx: matitaMisc.cmx buildTimeConf.cmx matitamakeLib.cmi matitaDisambiguator.cmi: matitaTypes.cmi matitaEngine.cmi: matitaTypes.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmi @@ -70,3 +76,4 @@ matitaMathView.cmi: matitaTypes.cmi matitaMisc.cmi: matitaTypes.cmi matitaScript.cmi: matitaTypes.cmi matitaSync.cmi: matitaTypes.cmi +matitamakeLib.cmi: matitaLog.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 4c3d9f305..c0b49433e 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -52,9 +52,10 @@ CCMOS = \ matitacleanLib.cmo \ matitacLib.cmo CLEANCMOS = $(CCMOS) +MAKECMOS = $(CCMOS) matitamakeLib.cmo -all: matita.conf.xml matita matitac matitatop cicbrowser matitadep matitaclean +all: matita.conf.xml matita matitac matitatop cicbrowser matitadep matitaclean matitamake matita.conf.xml: matita.conf.xml.sample @echo @@ -76,6 +77,7 @@ ifeq ($(HAVE_OCAMLOPT),yes) CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) CLEANCMXS = $(patsubst %.cmo,%.cmx,$(CLEANCMOS)) +MAKECMXS = $(patsubst %.cmo,%.cmx,$(MAKECMOS)) LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES)) LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES)) CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(CREQUIRES)) @@ -84,7 +86,9 @@ DEPLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format DEPLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(DEPREQUIRES)) CLEANLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(CLEANREQUIRES)) CLEANLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(CLEANREQUIRES)) -opt: matita.opt matitac.opt cicbrowser.opt matitadep.opt matitaclean.opt +MAKELIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MAKEREQUIRES)) +MAKELIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MAKEREQUIRES)) +opt: matita.opt matitac.opt cicbrowser.opt matitadep.opt matitaclean.opt matitamake.opt else opt: @echo "Native code compilation is disabled" @@ -113,6 +117,11 @@ matitaclean: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMOS) matitaclean.opt: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS) $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< +matitamake: matitamake.ml $(MAKECMOS) + $(OCAMLC) $(PKGS) -linkpkg -o $@ $(MAKECMOS) $< +matitamake.opt: matitamake.ml $(MAKECMXS) + $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(MAKECMXS) $< + cicbrowser: matita @test -f $@ || ln -s $< $@ cicbrowser.opt: matita.opt diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index e8eb4b427..94847494d 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -41,3 +41,6 @@ let gtkrc_file = runtime_base_dir ^ "/matita.gtkrc" let lang_file = runtime_base_dir ^ "/matita.lang" let script_template = runtime_base_dir ^ "/matita.ma.templ" let matita_conf = runtime_base_dir ^ "/matita.conf.xml" + +let matitamake_makefile_template = runtime_base_dir ^ "/template_makefile.in" + diff --git a/helm/matita/matita.conf.xml.sample.in b/helm/matita/matita.conf.xml.sample.in index b353a8791..0087d604f 100644 --- a/helm/matita/matita.conf.xml.sample.in +++ b/helm/matita/matita.conf.xml.sample.in @@ -4,7 +4,7 @@ true true cic:/matita/ - @USER_HOME@/.matita/xml + @USER_HOME@/.matita @USER_NAME@ false diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 53772ccf2..94efb904f 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -7,6 +7,8 @@ exception Drop;; let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; +type options = { do_heavy_checks: bool ; include_paths: string list } + (** create a ProofEngineTypes.mk_fresh_name_type function which uses given * names as long as they are available, then it fallbacks to name generation * using FreshNamesGenerator module *) @@ -443,7 +445,23 @@ let disambiguate_command status = function let status,obj = disambiguate_obj status obj in status, TacticAst.Obj (loc,obj) -let eval_command do_heavy_checks status cmd = +let try_open_in paths path = + let rec aux = function + | [] -> open_in path + | p :: tl -> + try + open_in (p ^ "/" ^ path) + with Sys_error _ -> aux tl + in + try + aux paths + with Sys_error _ as exc -> + MatitaLog.error ("Unable to read " ^ path); + MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); + raise exc +;; + +let eval_command opts status cmd = let status,cmd = disambiguate_command status cmd in match cmd with | TacticAst.Default (loc, what, uris) as cmd -> @@ -452,7 +470,7 @@ let eval_command do_heavy_checks status cmd = (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev} | TacticAst.Include (loc, path) -> let path = MatitaMisc.obj_file_of_script path in - let stream = Stream.of_channel (open_in path) in + let stream = Stream.of_channel (try_open_in opts.include_paths path) in let status = ref status in !eval_from_stream_ref status stream (fun _ _ -> ()); !status @@ -525,7 +543,7 @@ let eval_command do_heavy_checks status cmd = let name = UriManager.name_of_uri uri in if not(CicPp.check name ty) then MatitaLog.warn ("Bad name: " ^ name); - if do_heavy_checks then + if opts.do_heavy_checks then begin let dbd = MatitaDb.instance () in let similar = MetadataQuery.match_term ~dbd ty in @@ -575,45 +593,50 @@ let eval_command do_heavy_checks status cmd = | Cic.CurrentProof _ | Cic.Variable _ -> assert false -let eval_executable do_heavy_checks status ex = +let eval_executable opts status ex = match ex with | TacticAst.Tactical (_, tac) -> eval_tactical status tac - | TacticAst.Command (_, cmd) -> eval_command do_heavy_checks status cmd + | TacticAst.Command (_, cmd) -> eval_command opts status cmd | TacticAst.Macro (_, mac) -> command_error (sprintf "The macro %s can't be in a script" (TacticAstPp.pp_macro_ast mac)) let eval_comment status c = status -let eval_ast ?(do_heavy_checks=false) status st = + +let eval_ast ?(do_heavy_checks=false) ?(include_paths=[]) status st = + let opts = + {do_heavy_checks = do_heavy_checks ; include_paths = include_paths} + in match st with - | TacticAst.Executable (_,ex) -> eval_executable do_heavy_checks status ex + | TacticAst.Executable (_,ex) -> eval_executable opts status ex | TacticAst.Comment (_,c) -> eval_comment status c -let eval_from_stream ?do_heavy_checks status str cb = +let eval_from_stream ?do_heavy_checks ?include_paths status str cb = let stl = CicTextualParser2.parse_statements str in List.iter (fun ast -> - cb !status ast;status := eval_ast ?do_heavy_checks !status ast) + cb !status ast; + status := eval_ast ?do_heavy_checks ?include_paths !status ast) stl ;; (* to avoid a long list of recursive functions *) eval_from_stream_ref := eval_from_stream;; -let eval_from_stream_greedy ?do_heavy_checks status str cb = +let eval_from_stream_greedy ?do_heavy_checks ?include_paths status str cb = while true do print_string "matita> "; flush stdout; let ast = CicTextualParser2.parse_statement str in cb !status ast; - status := eval_ast ?do_heavy_checks !status ast + status := eval_ast ?do_heavy_checks ?include_paths !status ast done ;; -let eval_string ?do_heavy_checks status str = +let eval_string ?do_heavy_checks ?include_paths status str = eval_from_stream - ?do_heavy_checks status (Stream.of_string str) (fun _ _ -> ()) + ?do_heavy_checks ?include_paths status (Stream.of_string str) (fun _ _ ->()) let default_options () = (* @@ -626,7 +649,7 @@ let default_options () = *) let options = StringMap.add "basedir" - (String (Helm_registry.get "matita.basedir" )) + (String (Helm_registry.get "matita.basedir")) no_options in options diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 05092770b..f9699fbb5 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -29,10 +29,12 @@ exception Drop * infos like if the theorem is a duplicate *) val eval_string: ?do_heavy_checks:bool -> + ?include_paths:string list -> MatitaTypes.status ref -> string -> unit val eval_from_stream: ?do_heavy_checks:bool -> + ?include_paths:string list -> MatitaTypes.status ref -> char Stream.t -> (MatitaTypes.status -> (CicAst.term,TacticAst.obj,string) TacticAst.statement -> unit) -> @@ -40,6 +42,7 @@ val eval_from_stream: val eval_from_stream_greedy: ?do_heavy_checks:bool -> + ?include_paths:string list -> MatitaTypes.status ref-> char Stream.t -> (MatitaTypes.status -> (CicAst.term,TacticAst.obj,string) TacticAst.statement -> unit) -> @@ -47,8 +50,10 @@ val eval_from_stream_greedy: val eval_ast: ?do_heavy_checks:bool -> + ?include_paths:string list -> MatitaTypes.status -> (CicAst.term,TacticAst.obj,string) TacticAst.statement -> MatitaTypes.status val initial_status: MatitaTypes.status lazy_t + diff --git a/helm/matita/matitaLog.ml b/helm/matita/matitaLog.ml index 8c2e9a7a5..6ac82da58 100644 --- a/helm/matita/matitaLog.ml +++ b/helm/matita/matitaLog.ml @@ -53,6 +53,7 @@ let default_callback tag s = let callback = ref default_callback let set_log_callback f = callback := f +let get_log_callback () = !callback let message s = !callback `Message s let warn s = !callback `Warning s diff --git a/helm/matita/matitaLog.mli b/helm/matita/matitaLog.mli index 8e789a700..6847ce32d 100644 --- a/helm/matita/matitaLog.mli +++ b/helm/matita/matitaLog.mli @@ -27,6 +27,7 @@ type log_tag = [ `Debug | `Error | `Message | `Warning ] type log_callback = log_tag -> string -> unit val set_log_callback: log_callback -> unit +val get_log_callback: unit -> log_callback val message : string -> unit val warn : string -> unit diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 81f185ae8..53d7bd317 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -46,6 +46,11 @@ let input_file fname = close_in ic; Buffer.contents buf +let output_file data file = + let oc = open_out file in + output_string oc data; + close_out oc + let is_proof_script fname = true (** TODO Zack *) let is_proof_object fname = true (** TODO Zack *) diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index c5ff2ace6..5ea5c4394 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -30,6 +30,7 @@ val is_dir: string -> bool (** @return true if file is a directory *) val is_regular: string -> bool (** @return true if file is a regular file *) val input_file: string -> string (** read all the contents of file to string *) +val output_file: string -> string -> unit (** write string to file *) (** @return true if file is a (textual) proof script *) val is_proof_script: string -> bool diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index f42dad769..b54c67790 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -92,7 +92,7 @@ let add_aliases_for_object status suri = | Cic.CurrentProof _ -> assert false let paths_and_uris_of_obj uri status = - let basedir = get_string_option status "basedir" in + let basedir = get_string_option status "basedir" ^ "/xml" in let innertypesuri = UriManager.innertypesuri_of_uri uri in let bodyuri = UriManager.bodyuri_of_uri uri in let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 27147e6d4..37bb571ef 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -29,8 +29,16 @@ open MatitaTypes (** {2 Initialization} *) +let paths_to_search_in = ref [];; +let quiet_compilation = ref false;; + +let add_l l = fun s -> l := s :: !l ;; +let set_b b = fun () -> b := true;; + let arg_spec = [ -(* "-opt", Arg...., "set bla bla bla"; *) + "-I", Arg.String (add_l paths_to_search_in), + " Adds path to the list of searched paths for the include command"; + "-q", Arg.Unit (set_b quiet_compilation), "Turn off verbose compilation" ] let usage = sprintf "MatitaC v%s\nUsage: matitac [option ...] file\nOptions:" @@ -45,17 +53,21 @@ let run_script is eval_function = | Some s -> s in let slash_n_RE = Pcre.regexp "\\n" in - let cb status stm = - (* dump_status status; *) - let stm = TacticAstPp.pp_statement stm in - let stm = Pcre.replace ~rex:slash_n_RE stm in - let stm = - if String.length stm > 50 then - String.sub stm 0 50 ^ " ..." - else - stm - in - MatitaLog.debug ("Executing: ``" ^ stm ^ "''") + let cb = + if !quiet_compilation then + fun _ _ -> () + else + fun status stm -> + (* dump_status status; *) + let stm = TacticAstPp.pp_statement stm in + let stm = Pcre.replace ~rex:slash_n_RE stm in + let stm = + if String.length stm > 50 then + String.sub stm 0 50 ^ " ..." + else + stm + in + MatitaLog.debug ("Executing: ``" ^ stm ^ "''") in try eval_function status is cb @@ -101,7 +113,8 @@ let clean_exit n = let rec interactive_loop () = let str = Stream.of_channel stdin in try - run_script str MatitaEngine.eval_from_stream_greedy + run_script str + (MatitaEngine.eval_from_stream_greedy ~include_paths:!paths_to_search_in) with | MatitaEngine.Drop -> pp_ocaml_mode () | Sys.Break -> MatitaLog.error "user break!"; interactive_loop () @@ -141,17 +154,29 @@ let main ~mode = MatitaDb.create_owner_environment (); status := Some (ref (Lazy.force MatitaEngine.initial_status)); Sys.catch_break true; + let origcb = MatitaLog.get_log_callback () in + let newcb tag s = + match tag with + | `Debug | `Message -> () + | `Warning | `Error -> origcb tag s + in let fname = fname () in + if !quiet_compilation then + MatitaLog.set_log_callback newcb; try let time = Unix.time () in - MatitaLog.message (sprintf "execution of %s started:" fname); + if !quiet_compilation then + origcb `Message ("compiling " ^ Filename.basename fname ^ "...") + else + MatitaLog.message (sprintf "execution of %s started:" fname); let is = Stream.of_channel (match fname with | "stdin" -> stdin | fname -> open_in fname) in - run_script is MatitaEngine.eval_from_stream; + run_script is + (MatitaEngine.eval_from_stream ~include_paths:!paths_to_search_in); let elapsed = Unix.time () -. time in let tm = Unix.gmtime elapsed in let sec = diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index 69af9bf05..df6fdfecb 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -37,7 +37,14 @@ let _ = with UM.IllFormedUri _ -> files_to_remove := suri :: !files_to_remove; - MatitacleanLib.baseuri_of_file suri + let u = MatitacleanLib.baseuri_of_file suri in + if String.length u < 5 || String.sub u 0 5 <> "cic:/" then + begin + MatitaLog.error ("File " ^ suri ^ " defines a bad baseuri: "^u); + exit 1 + end + else + u in uris_to_remove := uri :: !uris_to_remove done @@ -45,5 +52,7 @@ let _ = Invalid_argument _ -> usage ()); main !uris_to_remove; let moos = List.map MatitaMisc.obj_file_of_script !files_to_remove in - List.iter - (fun s -> try Unix.unlink s with Unix.Unix_error _ -> ()) moos + List.iter + (fun s -> try Unix.unlink s with Unix.Unix_error _ -> ()) + moos + diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index 4218492f4..06c6835ca 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -98,21 +98,25 @@ let close_uri_list uri_to_remove = in (* now calculate the list of objects that belong to these baseuris *) let uri_to_remove = - List.fold_left - (fun acc buri -> - let inhabitants = HG.ls (buri ^ "/") in - let inhabitants = List.filter - (function HGT.Ls_object _ -> true | _ -> false) - inhabitants - in - let inhabitants = List.map - (function - | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri - | _ -> assert false) - inhabitants - in - inhabitants @ acc) - [] buri_to_remove + try + List.fold_left + (fun acc buri -> + let inhabitants = HG.ls (buri ^ "/") in + let inhabitants = List.filter + (function HGT.Ls_object _ -> true | _ -> false) + inhabitants + in + let inhabitants = List.map + (function + | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri + | _ -> assert false) + inhabitants + in + inhabitants @ acc) + [] buri_to_remove + with HGT.Invalid_URI u -> + MatitaLog.error ("We were listing an invalid buri: " ^ u); + exit 1 in (* now we want the list of all uri that depend on them *) let depend = @@ -133,7 +137,17 @@ let baseuri_of_file file = List.iter (fun stm -> match baseuri_of_baseuri_decl stm with - | Some buri -> uri := MatitaMisc.strip_trailing_slash buri + | Some buri -> + let u = MatitaMisc.strip_trailing_slash buri in + if String.length u < 5 || String.sub u 0 5 <> "cic:/" then + MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri); + (try + ignore(HG.resolve u) + with + | HGT.Unresolvable_URI _ -> + MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri) + | HGT.Key_not_found _ -> ()); + uri := u | None -> ()) stms; !uri diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 966b02b09..bd05558f3 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -1,3 +1,40 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let paths_to_search_in = ref [];; + +let add_l l = fun s -> l := s :: !l ;; + +let arg_spec = [ + "-I", Arg.String (add_l paths_to_search_in), + " Adds path to the list of searched paths for the include command"; +] +let usage = + Printf.sprintf "MatitaDep v%s\nUsage: matitadep [options] file...\nOptions:" + BuildTimeConf.version + module TA = TacticAst module U = UriManager @@ -23,9 +60,27 @@ let resolve alias = (*** TODO MANCANO LE URI VERBATIM DENTRO GLI AST DEI TERMINI ****) +let find path = + let rec aux = function + | [] -> close_in (open_in path); path + | p :: tl -> + try + close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path + with Sys_error _ -> aux tl + in + let paths = !paths_to_search_in in + try + aux paths + with Sys_error _ as exc -> + MatitaLog.error ("Unable to read " ^ path); + MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); + raise exc +;; + let main () = - for i = 1 to Array.length Sys.argv - 1 do - let file = Sys.argv.(i) in + let files = ref [] in + Arg.parse arg_spec (add_l files) usage; + List.iter (fun file -> let ic = open_in file in let stms = try @@ -46,7 +101,7 @@ let main () = (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> Hashtbl.add aliases file uri | TA.Executable (_, TA.Command (_, TA.Include (_, path))) -> - Hashtbl.add deps file path + Hashtbl.add deps file (find path) | _ -> ()) stms; Hashtbl.iter @@ -55,10 +110,9 @@ let main () = match dep with | None -> () | Some d -> Hashtbl.add deps file d) - aliases; - done; - for i = 1 to Array.length Sys.argv - 1 do - let file = Sys.argv.(i) in + aliases;) + !files; + List.iter (fun file -> let deps = Hashtbl.find_all deps file in let deps = List.fast_sort Pervasives.compare deps in let deps = MatitaMisc.list_uniq deps in @@ -67,8 +121,9 @@ let main () = in let deps = file :: deps in Printf.printf "%s: %s\n" (MatitaMisc.obj_file_of_script file) - (String.concat " " deps) - done + (String.concat " " deps)) + !files +;; let _ = main () diff --git a/helm/matita/matitamake.ml b/helm/matita/matitamake.ml new file mode 100644 index 000000000..e9efc3822 --- /dev/null +++ b/helm/matita/matitamake.ml @@ -0,0 +1,170 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +module MK = MatitamakeLib ;; + +let _ = + Helm_registry.load_from BuildTimeConf.matita_conf; + MK.initialize () +;; + +let usage = ref (fun () -> ()) + +let dev_of_name name = + match MK.development_for_name name with + | None -> + prerr_endline ("Unable to find a development called " ^ name); + exit 1 + | Some d -> d +;; + +let dev_for_dir dir = + match MK.development_for_dir dir with + | None -> + prerr_endline ("Unable to find a development holding directory: " ^ dir); + exit 1 + | Some d -> d +;; + +let init_dev_doc = " +\tParameters: name (the name of the development, required) +\tDescription: tells matitamake that a new development radicated +\t\tin the current working directory should be handled." +;; + +let init_dev args = + if List.length args <> 1 then !usage (); + match MK.initialize_development (List.hd args) (Unix.getcwd ()) with + | None -> exit 2 + | Some _ -> exit 0 +;; + +let list_dev_doc = " +\tParameters: +\tDescription: lists the known developments and their roots." +;; + +let list_dev args = + if List.length args <> 0 then !usage (); + match MK.list_known_developments () with + | [] -> print_string "No developments found.\n"; exit 0 + | l -> + List.iter + (fun (name, root) -> + print_string (Printf.sprintf "%-10s\trooted in %s\n" name root)) + l; + exit 0 +;; + +let destroy_dev_doc = " +\tParameters: name (the name of the development to destroy, required) +\tDescription: deletes a development (only from matitamake metadat, no +\t\t.ma files will be deleted)." + +let destroy_dev args = + if List.length args <> 1 then !usage (); + let name = (List.hd args) in + let dev = dev_of_name name in + MK.destroy_development dev; + exit 0 +;; + +let clean_dev_doc = " +\tParameters: name (the name of the development to destroy, optional) +\t\tIf omitted the development that holds the current working +\t\tdirectory is used (if any). +\tDescription: clean the develpoment." + +let clean_dev args = + let dev = + match args with + | [] -> dev_for_dir (Unix.getcwd ()) + | [name] -> dev_of_name name + | _ -> !usage (); exit 1 + in + match MK.clean_development dev with + | true -> exit 0 + | false -> exit 1 +;; + +let build_dev_doc = " +\tParameters: name (the name of the development to build, required) +\tDescription: completely builds the develpoment." + +let build_dev args = + if List.length args <> 1 then !usage (); + let name = (List.hd args) in + let dev = dev_of_name name in + match MK.build_development dev with + | true -> exit 0 + | false -> exit 1 +;; + +let target args = + if List.length args < 1 then !usage (); + let dev = dev_for_dir (Unix.getcwd ()) in + List.iter + (fun t -> + ignore(MK.build_development ~target:t dev)) + args +;; + +let params = [ + "-init", init_dev, init_dev_doc; + "-clean", clean_dev, clean_dev_doc; + "-list", list_dev, list_dev_doc; + "-destroy", destroy_dev, destroy_dev_doc; + "-build", build_dev, build_dev_doc; + "-h", (fun _ -> !usage()), "print this help screen"; + "-help", (fun _ -> !usage()), "print this help screen"; +] +;; + +usage := fun () -> + let p = prerr_endline in + p "\nusage:"; + p "\tmatitamake(.opt) [command [options]]\n"; + p "\tmatitamake(.opt) [target]\n"; + p "commands:"; + List.iter (fun (n,_,d) -> p (Printf.sprintf " %-10s%s" n d)) params; + p "\nIf target is omitted a 'all' will be used as the default."; + p "With -build you can build a development wherever it is."; + p "If you specify a target it implicitly refers to the development that"; + p "holds the current working directory (if any).\n"; + exit 1 +;; + +let parse args = + match args with + | [] -> target ["all"] + | s::tl -> + try + let _,f,_ = List.find (fun (n,_,_) -> n = s) params in + f tl + with Not_found -> if s.[0] = '-' then !usage () else target args + +let _ = + parse (List.tl (Array.to_list Sys.argv)) + diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml new file mode 100644 index 000000000..2facdda09 --- /dev/null +++ b/helm/matita/matitamakeLib.ml @@ -0,0 +1,207 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let logger = fun mark -> + match mark with + | `Error -> MatitaLog.error + | `Warning -> MatitaLog.warn + | `Debug -> MatitaLog.debug + | `Message -> MatitaLog.message +;; + +type development = + { root: string ; name: string } + +let developments = ref [] + +let pool () = Helm_registry.get "matita.basedir" ^ "/matitamake/" ;; +let rootfile = "/root" ;; + +let ls_dir dir = + try + let d = Unix.opendir dir in + let content = ref [] in + try + while true do + let name = Unix.readdir d in + if name <> "." && name <> ".." then + content := name :: !content + done; + Some [] + with End_of_file -> Unix.closedir d; Some !content + with Unix.Unix_error _ -> None + +let initialize () = + (* create a base env if none *) + MatitaMisc.mkdir (pool ()); + (* load developments *) + match ls_dir (pool ()) with + | None -> logger `Error ("Unable to list directory " ^ pool ()) + | Some l -> + List.iter + (fun name -> + let root = + try + Some (MatitaMisc.input_file (pool () ^ name ^ rootfile)) + with Unix.Unix_error _ -> + logger `Warning ("Malformed development " ^ name); + None + in + match root with + | None -> () + | Some root -> + developments := {root = root ; name = name} :: !developments) + l + +(* finds the makefile path for development devel *) +let makefile_for_development devel = + let develdir = pool () ^ devel.name in + develdir ^ "/makefile" +;; + +(* given a dir finds a development that is radicated in it or below *) +let development_for_dir dir = + 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 + in + (* it must be unique *) + try + Some (List.find (fun d -> is_prefix_of d.root dir) !developments) + with Not_found -> None +;; + +let development_for_name name = + try + Some (List.find (fun d -> d.name = name) !developments) + with Not_found -> None + +(* dumps the deveopment to disk *) +let dump_development devel = + let devel_dir = pool () ^ devel.name in + MatitaMisc.mkdir devel_dir; + MatitaMisc.output_file devel.root (devel_dir ^ rootfile); +;; + +let list_known_developments () = + List.map (fun r -> r.name,r.root) !developments + +let am_i_opt () = + if Pcre.pmatch ~pat:"\\.opt$" Sys.argv.(0) then ".opt" else "" + +let rebuild_makefile development = + let makefilepath = makefile_for_development development in + let template = + MatitaMisc.input_file BuildTimeConf.matitamake_makefile_template + in + let cc = BuildTimeConf.runtime_base_dir ^ "/matitac" ^ am_i_opt () in + let rm = BuildTimeConf.runtime_base_dir ^ "/matitaclean" ^ am_i_opt () in + let mm = BuildTimeConf.runtime_base_dir ^ "/matitadep" ^ am_i_opt () in + let df = pool () ^ development.name ^ "/depend" in + let dfs = pool () ^ development.name ^ "/depend.short" in + let template = Pcre.replace ~pat:"@ROOT@" ~templ:development.root template in + let template = Pcre.replace ~pat:"@CC@" ~templ:cc template in + let template = Pcre.replace ~pat:"@DEP@" ~templ:mm template in + let template = Pcre.replace ~pat:"@DEPFILE@" ~templ:df template in + let template = Pcre.replace ~pat:"@DEPFILESHORT@" ~templ:dfs template in + let template = Pcre.replace ~pat:"@CLEAN@" ~templ:rm template in + MatitaMisc.output_file template makefilepath + +(* creates a new development if possible *) +let initialize_development name dir = + let dev = {name = name ; root = dir} in + match development_for_dir dir with + | Some d -> + logger `Error + ("Directory " ^ dir ^ " is already handled by development " ^ d.name); + logger `Error + ("Development " ^ d.name ^ " is rooted in " ^ d.root); + logger `Error + (dir ^ " is a subdir of " ^ d.root); + None + | None -> + dump_development dev; + rebuild_makefile dev; + Some dev + +let make chdir args = + let old = Unix.getcwd () in + Unix.chdir chdir; +(* prerr_endline (String.concat " " ("make"::args));*) + let rc = Unix.system (String.concat " " ("make"::args)) in + Unix.chdir old; + match rc with + | Unix.WEXITED 0 -> true + | Unix.WEXITED i -> logger `Error ("make returned " ^ string_of_int i);false + | _ -> logger `Error "make STOPPED or SIGNALED!";false + +let call_make development target = + rebuild_makefile development; + let makefile = makefile_for_development development in + make development.root + ["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] + +let build_development ?(target="all") development = + call_make development target + +let clean_development development = + call_make development "clean" + +let destroy_development development = + let delete_development development = + let unlink file = + try + Unix.unlink file + with Unix.Unix_error _ -> logger `Debug ("Unable to delete " ^ file) + in + let rmdir dir = + try + Unix.rmdir dir + with Unix.Unix_error _ -> + logger `Warning ("Unable to remove dir " ^ dir); + match ls_dir dir with + | None -> logger `Error ("Unable to list directory " ^ dir) + | Some [] -> () + | Some l -> logger `Error ("The directory is not empty") + in + unlink (makefile_for_development development); + unlink (pool () ^ development.name ^ rootfile); + unlink (pool () ^ development.name ^ "/depend"); + unlink (pool () ^ development.name ^ "/depend.short"); + rmdir (pool () ^ development.name) + in + if not(clean_development development) then + begin + logger `Warning "Unable to clean the development problerly."; + logger `Warning "This may cause garbage." + end; + delete_development development + + diff --git a/helm/matita/matitamakeLib.mli b/helm/matita/matitamakeLib.mli new file mode 100644 index 000000000..707122668 --- /dev/null +++ b/helm/matita/matitamakeLib.mli @@ -0,0 +1,46 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +type development + +(* initialize_development [name] [dir] + * ask matitamake to recorder [dir] as the root for thedevelopment [name] *) +val initialize_development: string -> string -> development option +(* make target [default all] *) +val build_development: ?target:string -> development -> bool +(* make clean *) +val clean_development: development -> bool +(* return the development that handles dir *) +val development_for_dir: string -> development option +(* return the development *) +val development_for_name: string -> development option +(* return the known list of name, development_root *) +val list_known_developments: unit -> (string * string ) list +(* cleans the development, forgetting about it *) +val destroy_development: development -> unit +(* initiale internal data structures *) +val initialize : unit -> unit + + diff --git a/helm/matita/template_makefile.in b/helm/matita/template_makefile.in new file mode 100644 index 000000000..83fc7a3c7 --- /dev/null +++ b/helm/matita/template_makefile.in @@ -0,0 +1,33 @@ +SRC=$(shell find @ROOT@ -name "*.ma" -a -type f) +TODO=$(SRC:%.ma=%.moo) + +MATITAC=@CC@ +MATITACLEAN=@CLEAN@ +MATITADEP=@DEP@ + +all: $(TODO) + +clean: + $(MATITACLEAN) $(SRC) + rm -f $(TODO) + +%.moo:%.ma + [ ! -e $@ ] || ($(MATITACLEAN) $< 1>/dev/null 2>/dev/null ; rm -f $@) + ($(MATITAC) -q -I @ROOT@ $< | (grep -v "^make" || true)) || \ + ($(MATITACLEAN) $< ; exit 1) + +@DEPFILE@ @DEPFILESHORT@: $(SRC) + @DEP@ -I @ROOT@ $^ > @DEPFILE@ + >@DEPFILESHORT@ + for X in `cat @DEPFILE@ | cut -f 1 -d :`; do\ + TMP=`basename $$X | sed s/\.moo$$//`;\ + echo "$$TMP: $$X" >> @DEPFILESHORT@;\ + done + +# this is the depend for full targets like: +# dir/dir/name.moo: dir/dir/name.ma dir/dep.moo +-include @DEPFILE@ + +# this is for short name targets like: +# name: dir/dir/name.moo +-include @DEPFILESHORT@ diff --git a/helm/matita/tests/interactive/drop.ma b/helm/matita/tests/interactive/drop.ma index 1a6e2cac1..b8718cdb8 100644 --- a/helm/matita/tests/interactive/drop.ma +++ b/helm/matita/tests/interactive/drop.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/". +set "baseuri" "cic:/matita/tests/drop". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias num (instance 0) = "natural number". diff --git a/helm/matita/tests/interactive/grafite.ma b/helm/matita/tests/interactive/grafite.ma index 9791adecf..aaf570091 100644 --- a/helm/matita/tests/interactive/grafite.ma +++ b/helm/matita/tests/interactive/grafite.ma @@ -1,10 +1,7 @@ -%% test per matita.lang +set "baseuri" "cic:/matita/tests/grafite/". -set "baseuri" "cic:/matita/tests/". - -%% commento (* commento *) -(** hint. **) +(** hint. *) inductive pippo : Type \def | a : Type \to pippo @@ -35,6 +32,3 @@ record w : Type \def { whelp locate pippo. print "coercions". - - - diff --git a/helm/matita/tests/interactive/test5.ma b/helm/matita/tests/interactive/test5.ma index 537df88b6..e48cc827e 100644 --- a/helm/matita/tests/interactive/test5.ma +++ b/helm/matita/tests/interactive/test5.ma @@ -1,3 +1,5 @@ +set "baseuri" "cic:/matita/tests/interactive/test5/". + whelp instance \lambda A:Set. \lambda f: A \to A \to A. diff --git a/helm/matita/tests/interactive/test6.ma b/helm/matita/tests/interactive/test6.ma index 0ee55473e..4afdd3741 100644 --- a/helm/matita/tests/interactive/test6.ma +++ b/helm/matita/tests/interactive/test6.ma @@ -1,3 +1,5 @@ +set "baseuri" "cic:/matita/tests/interactive/test6/". + whelp instance \lambda A:Set. \lambda f:A \to A \to A. diff --git a/helm/matita/tests/interactive/test7.ma b/helm/matita/tests/interactive/test7.ma index 88e971bf7..d7347ed9f 100644 --- a/helm/matita/tests/interactive/test7.ma +++ b/helm/matita/tests/interactive/test7.ma @@ -1,3 +1,5 @@ +set "baseuri" "cic:/matita/tests/interactive/test7/". + whelp instance \lambda A:Set. \lambda r:A \to A \to Prop. diff --git a/helm/matita/tests/interactive/test_instance.ma b/helm/matita/tests/interactive/test_instance.ma index 4f868039a..7e02c0fff 100644 --- a/helm/matita/tests/interactive/test_instance.ma +++ b/helm/matita/tests/interactive/test_instance.ma @@ -1,3 +1,5 @@ +set "baseuri" "cic:/matita/tests/interactive/instance/". + whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x:A. P x x. whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y:A. P x y \to P y x. whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y,z:A. P x y \to P y z \to P y z. -- 2.39.2