let baseuri_of_inv = Hashtbl.create 13 in
let dot_file = ref "" in
(* helpers *)
- let include_paths =
- Helm_registry.get_list Helm_registry.string "matita.includes"
- in
+ let include_paths = ref [] in
let baseuri_of_script s =
try Hashtbl.find baseuri_of s
with Not_found ->
- let _,b,_,_ = Librarian.baseuri_of_script ~include_paths s in
+ let _,b,_,_ =
+ Librarian.baseuri_of_script ~include_paths:!include_paths s
+ in
Hashtbl.add baseuri_of s b;
Hashtbl.add baseuri_of_inv b s;
b
in
- let script_of_baseuri b =
- try Hashtbl.find baseuri_of_inv b
+ let script_of_baseuri ma b =
+ try Some (Hashtbl.find baseuri_of_inv b)
with Not_found ->
- assert false
- (* should be called only after baseuri_of_script is
- * called on every file *)
+ HLog.error ("Skipping dependency of '"^ma^"' over '"^b^"'");
+ HLog.error ("Plase include the file defining such baseuri, or fix");
+ HLog.error ("possibly incorrect verbatim URIs in the .ma file.");
+ None
in
let buri alias = U.buri_of_uri (U.uri_of_string alias) in
let resolve alias current_buri =
"<file> Save dependency graph in dot format to the given file";];
MatitaInit.parse_cmdline_and_configuration_file ();
MatitaInit.initialize_environment ();
- let args = Helm_registry.get_list Helm_registry.string "matita.args" in
let args =
- if args = [] then
let roots = Librarian.find_roots_in_dir (Sys.getcwd ()) in
match roots with
| [] ->
exit 1
| [x] ->
Sys.chdir (Filename.dirname x);
+ let opts = Librarian.load_root_file "root" in
+ include_paths :=
+ (try Str.split (Str.regexp " ") (List.assoc "include_paths" opts)
+ with Not_found -> []) @
+ (Helm_registry.get_list Helm_registry.string "matita.includes");
HExtlib.find ~test:(fun x -> Filename.check_suffix x ".ma") "."
| _ ->
- prerr_endline ("Too many roots: " ^ String.concat ", " roots);
- prerr_endline ("Enter one of these directories and retry");
+ let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in
+ prerr_endline ("Too many roots found:\n\t" ^ String.concat "\n\t" roots);
+ prerr_endline ("\nEnter one of these directories and retry");
exit 1
- else
- args
in
let ma_files = args in
(* here we go *)
let dep = resolve uri ma_baseuri in
(match dep with
| None -> ()
- | Some u -> Hashtbl.add include_deps ma_file (script_of_baseuri u))
+ | Some u ->
+ match script_of_baseuri ma_file u with
+ | Some d -> Hashtbl.add include_deps ma_file d
+ | None -> ())
| DependenciesParser.IncludeDep path ->
+ ignore (baseuri_of_script path);
Hashtbl.add include_deps ma_file path)
dependencies)
ma_files;
close_out oc
end;
(* generate regular depend output *)
- let oc = open_out "depends" in
- List.iter
- (fun ma_file ->
+ let fix_name f =
+ let f =
+ if Pcre.pmatch ~pat:"^\\./" f then
+ String.sub f 2 (String.length f - 2)
+ else
+ f
+ in
+ HExtlib.normalize_path f
+ in
+ let deps =
+ List.fold_left
+ (fun acc ma_file ->
let deps = Hashtbl.find_all include_deps ma_file in
let deps = List.fast_sort Pervasives.compare deps in
let deps = HExtlib.list_uniq deps in
- let deps = ma_file :: deps in
- let deps =
- List.map (fun f ->
- let f =
- if Pcre.pmatch ~pat:"^\\./" f then
- String.sub f 2 (String.length f - 2)
- else
- f
- in HExtlib.normalize_path f) deps
- in
- output_string oc (String.concat " " deps ^ "\n"))
- ma_files;
- close_out oc;
- HLog.message ("Generated " ^ Sys.getcwd () ^ "/depends")
+ let deps = List.map fix_name deps in
+ (fix_name ma_file, deps) :: acc)
+ [] ma_files
+ in
+ let extern =
+ List.fold_left
+ (fun acc (_,d) ->
+ List.fold_left
+ (fun a x ->
+ if List.exists (fun (t,_) -> x=t) deps then a
+ else x::a)
+ acc d)
+ [] deps
+ in
+ Librarian.write_deps_file (Sys.getcwd())
+ (deps@HExtlib.list_uniq (List.sort Pervasives.compare (List.map (fun x ->
+ x,[]) extern)))
+;;