1. the .moo files are now kept in the logical structure (i.e. in .matita/xml/*)
2. matitaclean is now able to correctly remove all the .moo files
3. the compilation target in library and tests is now foo.mo (it used to be
foo.moo) and it is PHONY
matitaDb.cmx: matitaMisc.cmx matitaDb.cmi
matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi
matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi
-matitaEngine.cmo: matitaTypes.cmi matitaSync.cmi matitaMisc.cmi matitaLog.cmi \
- matitaDisambiguator.cmi matitaDb.cmi matitaEngine.cmi
-matitaEngine.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \
- matitaDisambiguator.cmx matitaDb.cmx matitaEngine.cmi
+matitaEngine.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \
+ matitaMisc.cmi matitaLog.cmi matitaDisambiguator.cmi matitaDb.cmi \
+ matitaEngine.cmi
+matitaEngine.cmx: matitacleanLib.cmx matitaTypes.cmx matitaSync.cmx \
+ matitaMisc.cmx matitaLog.cmx matitaDisambiguator.cmx matitaDb.cmx \
+ matitaEngine.cmi
matitaExcPp.cmo: matitaTypes.cmi matitaExcPp.cmi
matitaExcPp.cmx: matitaTypes.cmx matitaExcPp.cmi
matitaGeneratedGui.cmo: matitaGeneratedGui.cmi
matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
matitaGui.cmx matitaGtkMisc.cmx matitaExcPp.cmx buildTimeConf.cmx \
matitaMathView.cmi
-matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi
-matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi
+matitaMisc.cmo: matitaTypes.cmi matitaLog.cmi matitaExcPp.cmi \
+ buildTimeConf.cmo matitaMisc.cmi
+matitaMisc.cmx: matitaTypes.cmx matitaLog.cmx matitaExcPp.cmx \
+ buildTimeConf.cmx matitaMisc.cmi
matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \
matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaEngine.cmi \
matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo matitaScript.cmi
buildTimeConf.cmo
matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
buildTimeConf.cmx
-matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi \
- matitaExcPp.cmi matitaDb.cmi matitacleanLib.cmi
-matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx \
- matitaExcPp.cmx matitaDb.cmx matitacleanLib.cmi
+matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
+ matitacleanLib.cmi
+matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
+ matitacleanLib.cmi
matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi buildTimeConf.cmo
matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx buildTimeConf.cmx
matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo
H=@
-all: $(SRC:%.ma=%.moo)
+all: $(SRC:%.ma=%.mo)
opt:
$(H)make MATITAC="$(MATITACOPT)" MATITACLEAN="$(MATITACLEANOPT)" MATITADEP="$(MATITADEPOPT)" all
make $(DEPEND_NAME)
.PHONY: depend
-%.moo:%.ma
+%.moo:
$(H)$(MATITAC) $<
$(DEPEND_NAME): $(SRC)
else
value
in
- if not (MatitacleanLib.is_empty value) then
+ if not (MatitaMisc.is_empty value) then
begin
MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
if opts.clean_baseuri then
open Printf
open MatitaTypes
+let strip_trailing_slash =
+ let rex = Pcre.regexp "/$" in
+ fun s -> Pcre.replace ~rex s
+
+let baseuri_of_baseuri_decl st =
+ match st with
+ | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) ->
+ Some buri
+ | _ -> None
+
+let baseuri_of_file file =
+ let uri = ref None in
+ let ic = open_in file in
+ let istream = Stream.of_channel ic in
+ (try
+ while true do
+ try
+ let stm = GrafiteParser.parse_statement istream in
+ match baseuri_of_baseuri_decl stm with
+ | Some buri ->
+ let u = 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(Http_getter.resolve u)
+ with
+ | Http_getter_types.Unresolvable_URI _ ->
+ MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
+ | Http_getter_types.Key_not_found _ -> ());
+ uri := Some u;
+ raise End_of_file
+ | None -> ()
+ with
+ CicNotationParser.Parse_error _ as exn ->
+ prerr_endline ("Unable to parse: " ^ file);
+ prerr_endline (MatitaExcPp.to_string exn);
+ ()
+ done
+ with End_of_file -> close_in ic);
+ match !uri with
+ | Some uri -> uri
+ | None -> failwith ("No baseuri defined in " ^ file)
+
+let is_empty buri =
+ List.for_all
+ (function
+ Http_getter_types.Ls_section _ -> true
+ | Http_getter_types.Ls_object _ -> false)
+ (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/"))
+
let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
let is_dir fname =
let rex = Pcre.regexp "\\s*$" in
fun s -> Pcre.replace ~rex s
-let strip_trailing_slash =
- let rex = Pcre.regexp "/$" in
- fun s -> Pcre.replace ~rex s
-
let empty_mathml () =
DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
~qualifiedName:(Gdome.domString "math") ~doctype:None
let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n
let end_ma_RE = Pcre.regexp "\\.ma$"
-let obj_file_of_script f = Pcre.replace ~rex:end_ma_RE ~templ:".moo" f
+
+let obj_file_of_baseuri baseuri =
+ let path =
+ Helm_registry.get "matita.basedir" ^ "/xml" ^
+ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri
+ in
+ path ^ ".moo"
+
+let obj_file_of_script f =
+ let baseuri = baseuri_of_file f in
+ obj_file_of_baseuri baseuri
let rec list_uniq = function
| [] -> []
* http://helm.cs.unibo.it/
*)
+val baseuri_of_file : string -> string
+
+val baseuri_of_baseuri_decl : ('a, 'b, 'c) GrafiteAst.statement -> string option
+
+ (** check whether no objects are defined below a given baseuri *)
+val is_empty: string -> bool
+
(** removes a file if it exists *)
val safe_remove: string -> unit
(** given the base name of an image, returns its full path *)
val image_path: string -> string
+val obj_file_of_baseuri: string -> string
val obj_file_of_script: string -> string
(** invoke a given function and return its value; in addition il will print
with
MatitaEngine.UnableToInclude what as exc ->
let compile_needed_and_go_on d =
- let root = MatitamakeLib.root_for_development d in
- let target = root ^ "/" ^ what in
+ let target = what in
let refresh_cb () =
while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
in
match ex with
| TA.Command (loc, _) | TA.Tactical (loc, _) ->
(try
- (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
+ (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
| None -> ()
| Some u ->
- if not (ML.is_empty u) then
+ if not (MatitaMisc.is_empty u) then
match
guistuff.ask_confirmation
~title:"Baseuri redefinition"
with
UM.IllFormedUri _ ->
files_to_remove := suri :: !files_to_remove;
- let u = MatitacleanLib.baseuri_of_file suri in
+ let u = MatitaMisc.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);
module UM = UriManager;;
module TA = GrafiteAst;;
-let baseuri_of_baseuri_decl st =
- match st with
- | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
- Some buri
- | _ -> None
-
let cache_of_processed_baseuri = Hashtbl.create 1024
let one_step_depend suri =
in
uri_to_remove, depend
-let baseuri_of_file file =
- let uri = ref None in
- let ic = open_in file in
- let istream = Stream.of_channel ic in
- (try
- while true do
- try
- let stm = GrafiteParser.parse_statement istream in
- match baseuri_of_baseuri_decl stm with
- | 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 := Some u;
- raise End_of_file
- | None -> ()
- with
- CicNotationParser.Parse_error _ as exn ->
- prerr_endline ("Unable to parse: " ^ file);
- prerr_endline (MatitaExcPp.to_string exn);
- ()
- done
- with End_of_file -> close_in ic);
- match !uri with
- | Some uri -> uri
- | None -> failwith ("No baseuri defined in " ^ file)
-
-let rec fix uris next =
+let rec close uris next =
match next with
| [] -> uris
- | l -> let uris, next = close_uri_list l in fix uris next @ uris
+ | l -> let uris, next = close_uri_list l in close uris next @ uris
let cleaned_no = ref 0;;
debug_prerr "clean_baseuris called on:";
if debug then
List.iter debug_prerr buris;
- let l = fix [] buris in
+ let l = close [] buris in
let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in
let l = List.map UriManager.uri_of_string l in
debug_prerr "clean_baseuri will remove:";
if debug then
List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
List.iter (MatitaSync.remove ~verbose) l;
+ Hashtbl.iter
+ (fun buri _ ->
+ MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri)
+ ) cache_of_processed_baseuri;
cleaned_no := !cleaned_no + List.length l;
if !cleaned_no > 30 then
List.iter
[MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
MetadataTypes.count_tbl()]
-
-let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = []
-
*)
val clean_baseuris : ?verbose:bool -> string list -> unit
-val baseuri_of_file : string -> string
-
-val baseuri_of_baseuri_decl : ('a, 'b, 'c) GrafiteAst.statement -> string option
-
- (** check whether no objects are defined below a given baseuri *)
-val is_empty: string -> bool
-
module U = UriManager
let deps = Hashtbl.create (Array.length Sys.argv)
-let baseuri = ref []
+let baseuris = ref []
let aliases = Hashtbl.create (Array.length Sys.argv)
(*
U.buri_of_uri (U.uri_of_string alias)
let resolve alias =
- try
- Some (snd(List.find (fun (u, f) -> u = (buri alias)) !baseuri))
- with
- | Not_found -> None
+ let buri = buri alias in
+ if List.exists (fun u -> u = buri) !baseuris then Some buri else None
(*** TODO MANCANO LE URI VERBATIM DENTRO GLI AST DEI TERMINI ****)
CicNotation.load_notation BuildTimeConf.core_notation_script;
let files = ref [] in
Arg.parse arg_spec (add_l files) usage;
- List.iter (fun file ->
+ List.iter
+ (fun file ->
let ic = open_in file in
let istream = Stream.of_channel ic in
(try
match GrafiteParser.parse_statement istream with
| TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) ->
let uri = MatitaMisc.strip_trailing_slash uri in
- baseuri := (uri, file) :: !baseuri
+ baseuris := uri :: !baseuris
| TA.Executable (_, TA.Command
(_, TA.Alias (_, TA.Ident_alias(_, uri)))) ->
Hashtbl.add aliases file uri
| TA.Executable (_, TA.Command (_, TA.Include (_, path))) ->
- Hashtbl.add deps file (find path)
+ Hashtbl.add deps file (MatitaMisc.obj_file_of_script (find path))
| _ -> ()
with
CicNotationParser.Parse_error _ as exn ->
let dep = resolve alias in
match dep with
| None -> ()
- | Some d -> Hashtbl.add deps file d)
- aliases)
- !files;
- List.iter (fun file ->
+ | Some u -> Hashtbl.add deps file (MatitaMisc.obj_file_of_baseuri u))
+ 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
- let deps =
- List.map (fun x -> Pcre.replace ~pat:"ma$" ~templ:"moo" x) deps
- in
let deps = file :: deps in
- Printf.printf "%s: %s\n" (MatitaMisc.obj_file_of_script file)
- (String.concat " " deps))
- !files
+ let moo = MatitaMisc.obj_file_of_script file in
+ Printf.printf "%s: %s\n" moo (String.concat " " deps);
+ Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo
+ ) !files
;;
let _ =
main ()
-
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
try
let argv = Array.of_list ("make"::args) in
pid := Unix.create_process "make" argv Unix.stdin out_w err_w;
+let ch = open_out "/tmp/pippo" in output_string ch (String.concat " " ("make"::(Array.to_list argv)) ^ "\n"); flush ch; close_out ch;
Unix.close out_w;
Unix.close err_w;
let buf = String.create 1024 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);
developments :=
List.filter (fun d -> d.name <> development.name) !developments
$(MATITACLEAN) $(SRC)
rm -f $(TODO)
-%.moo:%.ma
- [ ! -e $@ ] || ($(MATITACLEAN) $< 1>/dev/null 2>/dev/null ; rm -f $@)
- ($(MATITAC) -preserve -q -I @ROOT@ $< | (grep -v "^make" || true)) || \
- ($(MATITACLEAN) $< ; exit 1)
+%.moo:
+ ($(MATITAC) -q -I @ROOT@ $< | (grep -v "^make" || true))
-@DEPFILE@ @DEPFILESHORT@: $(SRC)
+@DEPFILE@ : $(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@
H=@
-all: $(SRC:%.ma=%.moo)
+all: $(SRC:%.ma=%.mo)
opt:
$(H)make MATITAC="$(MATITACOPT)" MATITACLEAN="$(MATITACLEANOPT)" MATITADEP="$(MATITADEPOPT)" all
make $(DEPEND_NAME)
.PHONY: depend
-%.moo:%.ma
+%.moo:
$(H)$(MATITAC) $<
$(DEPEND_NAME): $(SRC)
projects / helm.git / commitdiff