- clean_exit baseuri false
- | Sys.Break when not matita_debug ->
- HLog.error "user break!";
- pp_times fname false big_bang big_bang_u big_bang_s;
- clean_exit baseuri false
- | exn when not matita_debug ->
- HLog.error
- ("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn));
- pp_times fname false big_bang big_bang_u big_bang_s;
- clean_exit baseuri false
-
-module F =
- struct
- type source_object = string
- type target_object = string
- let string_of_source_object s = s;;
- let string_of_target_object s = s;;
-
- let is_readonly_buri_of opts file =
- let buri = List.assoc "baseuri" opts in
- Http_getter_storage.is_read_only (Librarian.mk_baseuri buri file)
- ;;
-
- let root_and_target_of opts mafile =
- try
- let include_paths = get_include_paths opts in
- let root,baseuri,_,relpath =
- Librarian.baseuri_of_script ~include_paths mafile
- in
- let obj_writeable, obj_read_only =
- if Filename.check_suffix mafile ".mma" then
- Filename.chop_suffix mafile ".mma" ^ ".ma",
- Filename.chop_suffix mafile ".mma" ^ ".ma"
- else
- LibraryMisc.obj_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true,
- LibraryMisc.obj_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:false
- in
- Some root, relpath, obj_writeable, obj_read_only
- with Librarian.NoRootFor x -> None, "", "", ""
- ;;
-
- 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 -> None
- ;;
-
- 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
- ;;
-
-(* FG: a problem was noticed in relising memory between subsequent *)
-(* invocations of the compiler. The following might help *)
- let compact r = Gc.compact (); r
-
- let build options fname =
- let matita_debug = Helm_registry.get_bool "matita.debug" in
- let compile opts fname =
- try
- (* MATITA 1.0: c'erano le push/pop per il parser; ma per
- * l'environment nuovo? *)
- compile opts fname
- with
- | Sys.Break -> false
- | exn when not matita_debug ->
- HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
- assert false
- in
- compact (compile options fname)
- ;;
-
- let load_deps_file = Librarian.load_deps_file;;
-
- end
-
-module Make = Librarian.Make(F)
-
-(* FINE EX MATITACLIB *)
-
-
-
-(* this function calls the parser in a way that it does not perform inclusions,
- * so that we can ensure the inclusion is performed after the included file
- * is compiled (if needed). matitac does not need that, since it compiles files
- * in the good order, here files may be compiled on demand. *)
-let wrap_with_make include_paths f x =
- match f x with
- (GrafiteAst.Executable
- (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
- ->
- let root, buri, _, tgt =
- try Librarian.baseuri_of_script ~include_paths mafilename
- with Librarian.NoRootFor _ ->
- HLog.error ("The included file '"^mafilename^"' has no root file,");
- HLog.error "please create it.";
- raise (Failure ("No root file for "^mafilename))
+ clean_exit baseuri exn
+
+(* BIG BUG: if a file recursively includes itself, anything can happen,
+ * from divergence to inclusion of an old copy of itself *)
+and assert_ng ~compiling ~include_paths ~root mapath =
+ let root',baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
+ assert (root=root');
+ let baseuri = NUri.uri_of_string baseuri in
+ let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
+ let ngtime =
+ try
+ Some (Unix.stat ngpath).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
+ let matime =
+ try (Unix.stat fullmapath).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
+ in
+ let to_be_compiled =
+ match ngtime with
+ Some ngtime ->
+ let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
+ let children_bad =
+ List.exists (assert_ng ~compiling ~include_paths ~root) preamble