X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitamakeLib.ml;h=499d0eaf361938c9bd363d7f72e8d7bbf0118f2f;hb=3a5b9647787e1402f6886d41824f664db290963f;hp=0ab251ddc5d3c5784f2a296550e767f5f4219dc1;hpb=7dda71a95fb8dee4ba3da5f760bdbbe075895e8f;p=helm.git

diff --git a/helm/software/matita/matitamakeLib.ml b/helm/software/matita/matitamakeLib.ml
index 0ab251ddc..499d0eaf3 100644
--- a/helm/software/matita/matitamakeLib.ml
+++ b/helm/software/matita/matitamakeLib.ml
@@ -42,6 +42,21 @@ let developments = ref []
 let pool () = Helm_registry.get "matita.basedir" ^ "/matitamake/" ;;
 let rootfile = "/root" ;;
 
+(* /foo/./bar/..//baz -> /foo/baz *)
+let normalize_path s = 
+  let s = Str.global_replace (Str.regexp "//") "/" s in
+  let l = Str.split (Str.regexp "/") s in
+  let rec aux = function
+    | [] -> []
+    | he::".."::tl -> aux tl
+    | he::"."::tl -> aux (he::tl)
+    | he::tl -> he :: aux tl
+  in
+  (if Str.string_match (Str.regexp "^/") s 0 then "/" else "") ^
+  String.concat "/" (aux l)
+  ^ (if Str.string_match (Str.regexp "/$") s 0 then "/" else "")
+;;
+
 let ls_dir dir = 
   try
     let d = Unix.opendir dir in
@@ -63,25 +78,26 @@ let initialize () =
   match ls_dir (pool ()) with
   | None -> logger `Error ("Unable to list directory " ^ pool ()) 
   | Some l -> 
-      List.iter 
-        (fun name -> 
-          let root = 
-            try 
-              Some (HExtlib.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;
-              let inc = Helm_registry.get_list 
-                Helm_registry.string "matita.includes" in
-              Helm_registry.set_list Helm_registry.of_string 
-                ~key:"matita.includes" ~value:(inc @ [root])
-          ) 
-      l
+      let paths = 
+        List.fold_left 
+          (fun acc name -> 
+            let root = 
+              try 
+                Some (HExtlib.input_file (pool () ^ name ^ rootfile))
+              with Unix.Unix_error _ -> 
+                logger `Warning ("Malformed development " ^ name);
+                None
+            in 
+            match root with 
+            | None -> acc
+            | Some root -> 
+                developments := {root = root ; name = name} :: !developments;
+                root::acc)
+         [] l
+      in
+      let inc = Helm_registry.get_list Helm_registry.string "matita.includes" in
+      Helm_registry.set_list Helm_registry.of_string 
+        ~key:"matita.includes" ~value:(inc @ paths)
 
 (* finds the makefile path for development devel *)
 let makefile_for_development devel =
@@ -94,6 +110,7 @@ let dot_for_development devel =
 
 (* given a dir finds a development that is radicated in it or below *)
 let development_for_dir dir =
+  let dir = normalize_path dir in
   let is_prefix_of d1 d2 =
     let len1 = String.length d1 in
     let len2 = String.length d2 in
@@ -130,9 +147,14 @@ let rebuild_makefile development =
     HExtlib.input_file BuildTimeConf.matitamake_makefile_template 
   in
   let ext = Lazy.force am_i_opt in
-  let cc = BuildTimeConf.runtime_base_dir ^ "/matitac" ^ ext in
-  let rm = BuildTimeConf.runtime_base_dir ^ "/matitaclean" ^ ext in
-  let mm = BuildTimeConf.runtime_base_dir ^ "/matitadep" ^ ext in
+  let binpath = 
+    if HExtlib.is_executable 
+      (BuildTimeConf.runtime_base_dir ^ "/matitac" ^ ext)
+    then BuildTimeConf.runtime_base_dir ^ "/" else ""
+  in
+  let cc = binpath ^ "matitac" ^ ext in
+  let rm = binpath ^ "matitaclean" ^ ext in
+  let mm = binpath ^ "matitadep" ^ ext in
   let df = pool () ^ development.name ^ "/depend" in
   let template = Pcre.replace ~pat:"@ROOT@" ~templ:development.root template in
   let template = Pcre.replace ~pat:"@CC@" ~templ:cc template in
@@ -157,6 +179,7 @@ let rebuild_makefile_devel development =
   
 (* creates a new development if possible *)
 let initialize_development name dir =
+  let dir = normalize_path dir in
   let name = Pcre.replace ~pat:" " ~templ:"_" name in 
   let dev = {name = name ; root = dir} in
   dump_development dev;
@@ -187,8 +210,16 @@ let call_make ?matita_flags development target make =
       | None -> (try Sys.getenv "MATITA_FLAGS" with Not_found -> "")
       | Some s -> s 
     in
-    already_defined ^ 
-      if Helm_registry.get_bool "matita.bench" then "-bench" else ""
+    let bench = 
+      if Helm_registry.get_bool "matita.bench" then " -bench" else ""
+    in
+    let system = 
+      if Helm_registry.get_bool "matita.system" then " -system" else ""
+    in
+    let noinnertypes = 
+      if Helm_registry.get_bool "matita.noinnertypes" then " -noinnertypes" else ""
+    in
+    already_defined ^ bench ^ system ^ noinnertypes
   in
   let csc = try ["SRC=" ^ Sys.getenv "SRC"] with Not_found -> [] in
   rebuild_makefile development;
@@ -196,7 +227,7 @@ let call_make ?matita_flags development target make =
   let flags = [] in 
   let flags =
     try
-      flags @ [ sprintf "MATITA_FLAGS=\"%s\"" matita_flags ]
+      flags @ [ sprintf "MATITA_FLAGS=%s" matita_flags ]
     with Not_found -> flags in
   let flags = flags @ csc in
   let args = 
@@ -328,7 +359,7 @@ let publish_development_bstract build clean devel =
     let orig_matita_flags = 
       try Sys.getenv "MATITA_FLAGS" with Not_found -> "" 
     in
-    "\"" ^ orig_matita_flags ^ "\"", "\"" ^ orig_matita_flags ^ " -system\"" 
+    orig_matita_flags, orig_matita_flags ^ " -system" 
   in
   HLog.message "cleaning the development before publishing";
   if clean ~matita_flags devel then