X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatitadep.ml;h=473445fffc60c5c6fff5825631558b467277296f;hb=892992b24f5476c2b4eed13f64e04854ef919020;hp=f62a6067fa405765294d8251aa2622007767eaac;hpb=19618ce16bb4a5fd2f7e88bfe9b5002511197faf;p=helm.git

diff --git a/helm/software/matita/matitadep.ml b/helm/software/matita/matitadep.ml
index f62a6067f..473445fff 100644
--- a/helm/software/matita/matitadep.ml
+++ b/helm/software/matita/matitadep.ml
@@ -25,18 +25,20 @@
 
 (* $Id$ *)
 
+open Printf
+
 module GA = GrafiteAst 
 module U = UriManager
                 
 let obj_file_of_baseuri writable baseuri = 
   try 
     LibraryMisc.obj_file_of_baseuri 
-     ~must_exist:true ~baseuri ~writable
+     ~must_exist:true ~baseuri ~writable 
   with 
   | Http_getter_types.Unresolvable_URI _ 
   | Http_getter_types.Key_not_found _ ->  
     LibraryMisc.obj_file_of_baseuri 
-     ~must_exist:false ~baseuri ~writable:true
+     ~must_exist:false ~baseuri ~writable:true 
 ;;
 
 let main () =
@@ -46,17 +48,22 @@ let main () =
   let baseuri_of = Hashtbl.create (Array.length Sys.argv) in
   let baseuri_of_inv = Hashtbl.create (Array.length Sys.argv) in
   let uri_deps = Hashtbl.create (Array.length Sys.argv) in
+  let ma_topo = Hashtbl.create (Array.length Sys.argv) in
+  let ma_topo_keys = ref [] in
   let buri alias = U.buri_of_uri (U.uri_of_string alias) in
   let resolve alias current_buri =
     let buri = buri alias in
     if buri <> current_buri then Some buri else None in
-  MatitaInit.fill_registry ();
   let dot_file = ref "" in
+  let order_only = ref false in
   MatitaInit.add_cmdline_spec 
     ["-dot", Arg.Set_string dot_file,
-      "<file> Save dependency graph in dot format to the given file"];
-  MatitaInit.parse_cmdline ();
-  MatitaInit.load_configuration_file ();
+      "<file> Save dependency graph in dot format to the given file";
+     "-order", Arg.Set order_only,
+      "Only print (one of the possibles) build order(s) for the given *.ma"];
+  MatitaInit.parse_cmdline_and_configuration_file ();
+  MatitaInit.initialize_environment ();
+  MatitamakeLib.initialize ();
   let include_paths =
    Helm_registry.get_list Helm_registry.string "matita.includes" in
   let args = Helm_registry.get_list Helm_registry.string "matita.args" in
@@ -79,27 +86,54 @@ let main () =
       let istream = Ulexing.from_utf8_channel ic in
       let dependencies = DependenciesParser.parse_dependencies istream in
     close_in ic;
-    List.iter 
-     (function
-       | DependenciesParser.UriDep uri -> 
-          let uri = UriManager.string_of_uri uri in
-          if not (Http_getter_storage.is_legacy uri) then
-            Hashtbl.add uri_deps ma_file uri
-       | DependenciesParser.BaseuriDep uri -> 
-          let uri = Http_getter_misc.strip_trailing_slash uri in
-          Hashtbl.add baseuri_of ma_file uri;
-          Hashtbl.add baseuri_of_inv uri ma_file
-       | DependenciesParser.IncludeDep path -> 
-          try 
-            let baseuri = baseuri_of_script path in
-            if not (Http_getter_storage.is_legacy baseuri) then
-              (let moo_file = obj_file_of_baseuri false baseuri in
-              Hashtbl.add include_deps ma_file moo_file;
-              Hashtbl.add include_deps_dot ma_file baseuri)
-          with Sys_error _ -> 
-            HLog.warn 
-              ("Unable to find " ^ path ^ " that is included in " ^ ma_file))
-     dependencies)
+    if !order_only then begin
+      let relative_ma_file =
+        (* change a path leading to a .ma file into a path relative to its
+         * development root dir *)
+        let absolute_ma_file =
+          if Filename.is_relative ma_file then
+            Filename.concat (Sys.getcwd ()) ma_file
+          else
+            ma_file in
+        let ma_dir = Filename.dirname absolute_ma_file in
+        match MatitamakeLib.development_for_dir ma_dir with
+        | None ->
+            eprintf "no development setup for dir '%s'\n%!" ma_dir;
+            assert false
+        | Some devel ->
+            Pcre.replace
+              ~pat:(Pcre.quote(MatitamakeLib.root_for_development devel) ^ "/?")
+              ~templ:"" absolute_ma_file
+      in
+      ma_topo_keys := relative_ma_file :: !ma_topo_keys;
+      List.iter
+        (function
+          | DependenciesParser.IncludeDep path ->
+              Hashtbl.add ma_topo relative_ma_file path
+          | _ -> ())
+        dependencies
+    end else
+      List.iter 
+       (function
+         | DependenciesParser.UriDep uri -> 
+            let uri = UriManager.string_of_uri uri in
+            if not (Http_getter_storage.is_legacy uri) then
+              Hashtbl.add uri_deps ma_file uri
+         | DependenciesParser.BaseuriDep uri -> 
+            let uri = Http_getter_misc.strip_trailing_slash uri in
+            Hashtbl.add baseuri_of ma_file uri;
+            Hashtbl.add baseuri_of_inv uri ma_file
+         | DependenciesParser.IncludeDep path -> 
+            try 
+              let baseuri = baseuri_of_script path in
+              if not (Http_getter_storage.is_legacy baseuri) then
+                (let moo_file = obj_file_of_baseuri false baseuri in
+                Hashtbl.add include_deps ma_file moo_file;
+                Hashtbl.add include_deps_dot ma_file baseuri)
+            with Sys_error _ -> 
+              HLog.warn 
+                ("Unable to find " ^ path ^ " that is included in " ^ ma_file))
+       dependencies)
    ma_files;
   Hashtbl.iter 
     (fun file alias -> 
@@ -112,7 +146,7 @@ let main () =
       with Not_found -> 
         prerr_endline ("File "^ file^" has no baseuri. Use set baseuri");
         exit 1)
-  uri_deps;
+    uri_deps;
       let gcp x y = 
       (* explode and implode from the OCaml Expert FAQ. *)
         let explode s =
@@ -159,22 +193,35 @@ let main () =
       GraphvizPp.Dot.trailer fmt;
       close_out oc
     end;
-  List.iter (* (always) generate regular .depend output *)
-   (fun ma_file -> 
-     try
-      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 baseuri = Hashtbl.find baseuri_of ma_file in
-      let moo = obj_file_of_baseuri true baseuri in
-      Printf.printf "%s: %s\n%s: %s\n%s: %s\n%s: %s\n" 
-        moo (String.concat " " deps)
-        (Filename.basename(Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file)) moo
-        (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file) moo
-        (Pcre.replace ~pat:"ma$" ~templ:"mo" (short ma_file)) moo
-     with Not_found -> 
-       prerr_endline ("File "^ma_file^" has no baseuri. Use set baseuri");
-       exit 1)
-    ma_files
+  if !order_only then begin
+    let module OrdererString =
+      struct
+        type t = string
+        let compare = Pervasives.compare
+      end
+    in
+    let module Topo = HTopoSort.Make (OrdererString) in
+    let sorted_ma =
+      Topo.topological_sort !ma_topo_keys (Hashtbl.find_all ma_topo) in
+    List.iter print_endline sorted_ma
+    (*Hashtbl.iter (fun k v -> printf "%s: %s\n" k v) ma_topo*)
+  end else
+    List.iter (* generate regular .depend output *)
+     (fun ma_file -> 
+       try
+        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 baseuri = Hashtbl.find baseuri_of ma_file in
+        let moo = obj_file_of_baseuri true baseuri in
+        printf "%s: %s\n%s: %s\n%s: %s\n%s: %s\n" 
+          moo (String.concat " " deps)
+          (Filename.basename(Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file)) moo
+          (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file) moo
+          (Pcre.replace ~pat:"ma$" ~templ:"mo" (short ma_file)) moo
+       with Not_found -> 
+         prerr_endline ("File "^ma_file^" has no baseuri. Use set baseuri");
+         exit 1)
+      ma_files