From 2e17165ef9e63367cc290ad555145b4c22a4582b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 16 Dec 2010 11:51:30 +0000 Subject: [PATCH] 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) ... --- matita/components/library/librarian.ml | 5 +++-- matita/components/library/librarian.mli | 1 + matita/matita/matitaEngine.ml | 27 ++++++++++++++----------- matita/matita/matitaEngine.mli | 2 +- matita/matita/matitac.ml | 25 ++++++++++++----------- 5 files changed, 33 insertions(+), 27 deletions(-) diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml index 791141b88..9ffde2b87 100644 --- 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 040cecf62..af83c56d7 100644 --- 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 fc1de152d..c6f435975 100644 --- 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 5bbac3e2b..2b3efff8f 100644 --- 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 08dab089f..67a1742f0 100644 --- 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) -- 2.39.2