Some bugs fixed (and some still open) in recursive compilation of files:

 a) matitac now takes again either a list of files to be compiled or
    nothing (to compile all files in the cwd)
 b) ...

diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml
index 791141b88c23f4233f51f4b990ac543b07f49348..9ffde2b87d0444c6d9ad012b4e26e9641d45a513 100644 (file)
--- a/matita/components/library/librarian.ml
+++ b/matita/components/library/librarian.ml
@@ -23,6 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
+exception FileNotFound of string
 exception NoRootFor of string
 
 let absolutize path =
@@ -83,7 +84,7 @@ let find_root_for ~include_paths file =
        HLog.error ("We are in: " ^ Sys.getcwd ());
        HLog.error ("Unable to find: "^file^"\nPaths explored:");
        List.iter (fun x -> HLog.error (" - "^x)) include_paths;
-       raise (NoRootFor file)
+       raise (FileNotFound file)
    in
    let path = find_path_for file in   
    let path = absolutize path in
@@ -128,7 +129,7 @@ let baseuri_of_script ~include_paths file =
     match l1, l2 with
     | h1::tl1,h2::tl2 when h1 = h2 -> substract tl1 tl2
     | l,[] -> l
-    | _ -> raise (NoRootFor (file ^" "^path^" "^root))
+    | _ -> assert false
   in
   let extra_buri = substract lpath lroot in
   let extra = String.concat "/" extra_buri in

diff --git a/matita/components/library/librarian.mli b/matita/components/library/librarian.mli
index 040cecf62cd0b8a3f4f2223e88f6f657f078bb86..af83c56d7a4ddf0532c45af39d9916fc454ef807 100644 (file)
--- a/matita/components/library/librarian.mli
+++ b/matita/components/library/librarian.mli
@@ -24,6 +24,7 @@
  *)
 
 exception NoRootFor of string
+exception FileNotFound of string
 
 (* make a relative path absolute *)
 val absolutize: string -> string 

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index fc1de152d575c3997d014492351eb7fea78dead7..c6f4359759d4818baf48e51b0c86827c83aa9042 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -162,19 +162,23 @@ let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
   (new_status,None)::intermediate_states
 ;;
 
+let baseuri_of_script ~include_paths fname =
+ try Librarian.baseuri_of_script ~include_paths fname
+ with
+   Librarian.NoRootFor _ -> 
+    HLog.error ("The included file '"^fname^"' has no root file,");
+    HLog.error "please create it.";
+    raise (Failure ("No root file for "^fname))
+  | Librarian.FileNotFound _ -> 
+    raise (Failure ("File not found: "^fname))
+;;
+
 let rec get_ast status ~compiling ~include_paths strm = 
   match GrafiteParser.parse_statement status strm 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))
-      in
-       ignore (assert_ng ~compiling ~include_paths ~root tgt);
+       ignore (assert_ng ~compiling ~include_paths mafilename);
        cmd
    | cmd -> cmd
 
@@ -288,9 +292,8 @@ and compile ~compiling ~include_paths fname =
       pp_times fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri exn
 
-and assert_ng ~compiling ~include_paths ~root mapath =
- let root',baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
- assert (root=root');
+and assert_ng ~compiling ~include_paths mapath =
+ let _,baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
  let baseuri = NUri.uri_of_string baseuri in
  let ngtime_of baseuri =
   let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
@@ -309,7 +312,7 @@ and assert_ng ~compiling ~include_paths ~root mapath =
       let children_bad =
        List.exists
         (fun mapath ->
-             assert_ng ~compiling ~include_paths ~root mapath
+             assert_ng ~compiling ~include_paths mapath
           || let _,baseuri,_,_ =
                Librarian.baseuri_of_script ~include_paths mapath in
              let baseuri = NUri.uri_of_string baseuri in

diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli
index 5bbac3e2b35b7501373144c074c4abe610cea9ad..2b3efff8f08061a26c3200a5bbad5a621789da22 100644 (file)
--- a/matita/matita/matitaEngine.mli
+++ b/matita/matita/matitaEngine.mli
@@ -44,4 +44,4 @@ val eval_ast :
   (GrafiteTypes.status *
    (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) option) list
 
-val assert_ng : include_paths:string list -> root:string -> string -> bool
+val assert_ng : include_paths:string list -> string -> bool

diff --git a/matita/matita/matitac.ml b/matita/matita/matitac.ml
index 08dab089f6e44516c43b836a433fc20cda8e74ee..67a1742f07dc4efbdd3daaa0f421e1c580a1742e 100644 (file)
--- a/matita/matita/matitac.ml
+++ b/matita/matita/matitac.ml
@@ -30,11 +30,13 @@ let main_compiler () =
   MatitaInit.initialize_all ();
   (* targets and deps *)
   let targets = Helm_registry.get_list Helm_registry.string "matita.args" in
-  let target, root = 
+  let targets = 
     match targets with
     | [] ->
       (match Librarian.find_roots_in_dir (Sys.getcwd ()) with
-      | [x] -> [], Filename.dirname x
+      | [x] ->
+         let root = Filename.dirname x in
+          HExtlib.find ~test:(fun path -> Filename.check_suffix path ".ma") root
       | [] -> 
          prerr_endline "No targets and no root found"; exit 1
       | roots -> 
@@ -42,22 +44,21 @@ let main_compiler () =
          prerr_endline ("Too many roots found:\n\t" ^ String.concat "\n\t" roots);
          prerr_endline ("\nEnter one of these directories and retry");
          exit 1);
-    | hds -> 
-      let roots_and_targets = 
-       List.map (fun (root, buri, file, target) -> root,target)
-        (List.map (Librarian.baseuri_of_script ~include_paths:[]) hds) in
-      let roots,targets = List.split roots_and_targets in
-      let root = List.hd roots in
-      if (List.exists (fun root' -> root' <> root) roots) then
-       (prerr_endline "Only targets in the same root can be specified.";exit 1);
-      targets, root
+    | _ -> targets
   in
   (* must be called after init since args are set by cmdline parsing *)
   let system_mode =  Helm_registry.get_bool "matita.system" in
   if system_mode then HLog.message "Compiling in system space";
   (* here we go *)
   if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
-  if List.for_all (MatitaEngine.assert_ng ~include_paths:[] ~root) target then 
+  if List.fold_left
+   (fun b t ->
+     (try
+       ignore (MatitaEngine.assert_ng ~include_paths:[] t); true
+      with
+       MatitaEngine.FailureCompiling _ -> false) && b
+     ) true targets
+  then 
     (HLog.message "Compilation successful"; 0)
   else
     (HLog.message "Compilation failed"; 1)