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
matitaMisc.cmi: matitaTypes.cmi
matitaScript.cmi: matitaTypes.cmi
matitaSync.cmi: matitaTypes.cmi
+matitamakeLib.cmi: matitaLog.cmi
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
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))
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"
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
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"
+
<key name="auto_disambiguation">true</key>
<key name="environment_trust">true</key>
<key name="baseuri">cic:/matita/</key>
- <key name="basedir">@USER_HOME@/.matita/xml</key>
+ <key name="basedir">@USER_HOME@/.matita</key>
<key name="owner">@USER_NAME@</key>
<!-- <key name="font_size">10</key> -->
<key name="tactics_bar">false</key>
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 *)
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 ->
(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
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
| 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 () =
(*
*)
let options =
StringMap.add "basedir"
- (String (Helm_registry.get "matita.basedir" ))
+ (String (Helm_registry.get "matita.basedir"))
no_options
in
options
* 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) ->
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) ->
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
+
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
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
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 *)
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
| 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:") ""
(** {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),
+ "<path> 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:"
| 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
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 ()
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 =
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
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
+
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 =
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
+(* 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),
+ "<path> 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
(*** 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
(_, 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
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
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 ()
--- /dev/null
+(* 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))
+
--- /dev/null
+(* 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
+
+
--- /dev/null
+(* 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
+
+
--- /dev/null
+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@
-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".
-%% 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
whelp locate pippo.
print "coercions".
-
-
-
+set "baseuri" "cic:/matita/tests/interactive/test5/".
+
whelp instance
\lambda A:Set.
\lambda f: A \to A \to A.
+set "baseuri" "cic:/matita/tests/interactive/test6/".
+
whelp instance
\lambda A:Set.
\lambda f:A \to A \to A.
+set "baseuri" "cic:/matita/tests/interactive/test7/".
+
whelp instance
\lambda A:Set.
\lambda r:A \to A \to Prop.
+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.
projects / helm.git / commitdiff