From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- checker/check.ml | 39 ++++++++++++++++++++++----------------- checker/checker.ml | 35 +++++++++++++++++++++++------------ 2 files changed, 45 insertions(+), 29 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index f8844975..e91516c7 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -209,7 +209,7 @@ let locate_absolute_library dir = if loadpath = [] then raise LibUnmappedDir; try let name = string_of_id base^".vo" in - let _, file = System.where_in_path loadpath name in + let _, file = System.where_in_path false loadpath name in (dir, file) with Not_found -> (* Last chance, removed from the file system but still in memory *) @@ -229,7 +229,7 @@ let locate_qualified_library qid = in if loadpath = [] then raise LibUnmappedDir; let name = qid.basename^".vo" in - let path, file = System.where_in_path loadpath name in + let path, file = System.where_in_path true loadpath name in let dir = extend_dirpath (find_logical_path path) (id_of_string qid.basename) in (* Look if loaded *) @@ -267,10 +267,8 @@ let try_locate_qualified_library qid = (*s Loading from disk to cache (preparation phase) *) -let vo_magic_number = 08190 (* trunk *) - let (raw_extern_library, raw_intern_library) = - System.raw_extern_intern vo_magic_number ".vo" + System.raw_extern_intern Coq_config.vo_magic_number ".vo" let with_magic_number_check f a = try f a @@ -323,7 +321,8 @@ let get_deps (dir, f) = (* Read a compiled library and all dependencies, in reverse order. Do not include files that are already in the context. *) -let rec intern_library (dir, f) needed = +let rec intern_library seen (dir, f) needed = + if LibrarySet.mem dir seen then failwith "Recursive dependencies!"; (* Look if in the current logical environment *) try let _ = find_library dir in needed with Not_found -> @@ -332,28 +331,34 @@ let rec intern_library (dir, f) needed = else (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file (dir,f) in - (dir,m)::List.fold_right intern_mandatory_library m.library_deps needed - -(* digest error with checked modules could be a warning *) -and intern_mandatory_library (dir,_) needed = - intern_library (try_locate_absolute_library dir) needed + let seen' = LibrarySet.add dir seen in + let deps = + List.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps in + (dir,m) :: List.fold_right (intern_library seen') deps needed (* Compute the reflexive transitive dependency closure *) -let rec fold_deps ff (dir,f) s = - if LibrarySet.mem dir s then s +let rec fold_deps seen ff (dir,f) (s,acc) = + if LibrarySet.mem dir seen then failwith "Recursive dependencies!"; + if LibrarySet.mem dir s then (s,acc) else let deps = get_deps (dir,f) in let deps = List.map (fun (d,_) -> try_locate_absolute_library d) deps in - ff dir (List.fold_right (fold_deps ff) deps s) + let seen' = LibrarySet.add dir seen in + let (s',acc') = List.fold_right (fold_deps seen' ff) deps (s,acc) in + (LibrarySet.add dir s', ff dir acc') + +and fold_deps_list seen ff modl needed = + List.fold_right (fold_deps seen ff) modl needed -and fold_deps_list ff modl needed = - List.fold_right (fold_deps ff) modl needed +let fold_deps_list ff modl acc = + snd (fold_deps_list LibrarySet.empty ff modl (LibrarySet.empty,acc)) let recheck_library ~norec ~admit ~check = let ml = List.map try_locate_qualified_library check in let nrl = List.map try_locate_qualified_library norec in let al = List.map try_locate_qualified_library admit in - let needed = List.rev (List.fold_right intern_library (ml@nrl) []) in + let needed = List.rev + (List.fold_right (intern_library LibrarySet.empty) (ml@nrl) []) in (* first compute the closure of norec, remove closure of check, add closure of admit, and finally remove norec and check *) let nochk = fold_deps_list LibrarySet.add nrl LibrarySet.empty in diff --git a/checker/checker.ml b/checker/checker.ml index 1c7ace12..7de25835 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -73,16 +73,14 @@ let convert_string d = failwith "caught" let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = - let dirs = all_subdirs dir in - let prefix = repr_dirpath coq_dirpath in - if dirs <> [] then + if exists_dir dir then + let dirs = all_subdirs dir in + let prefix = repr_dirpath coq_dirpath in let convert_dirs (lp,cp) = - (lp,Names.make_dirpath - ((List.map convert_string (List.rev cp))@prefix)) in + (lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in let dirs = map_succeed convert_dirs dirs in - begin - List.iter Check.add_load_path dirs - end + List.iter Check.add_load_path dirs; + Check.add_load_path (dir,coq_dirpath) else msg_warning (str ("Cannot open " ^ dir)) @@ -101,6 +99,14 @@ let set_default_rec_include d = let p = Check.default_root_prefix in check_coq_overwriting p; push_rec_include (d, p) +let set_include d p = + let p = dirpath_of_string p in + check_coq_overwriting p; + push_include (d,p) +let set_rec_include d p = + let p = dirpath_of_string p in + check_coq_overwriting p; + push_rec_include(d,p) (* Initializes the LoadPath according to COQLIB and Coq_config *) let init_load_path () = @@ -174,9 +180,11 @@ let print_usage_channel co command = output_string co command; output_string co "Coq options are:\n"; output_string co -" -I dir add directory dir in the include path +" -I dir -as coqdir map physical dir to logical coqdir + -I dir map directory dir to the empty logical path -include dir (idem) - -R dir coqdir recursively map physical dir to logical coqdir + -R dir -as coqdir recursively map physical dir to logical coqdir + -R dir coqdir (idem) -admit module load module and dependencies without checking -norec module check module but admit dependencies without checking @@ -297,11 +305,14 @@ let parse_args() = | "-impredicative-set" :: rem -> set_engagement Declarations.ImpredicativeSet; parse rem + | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem + | ("-I"|"-include") :: d :: "-as" :: [] -> usage () | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: p :: rem -> - push_rec_include (d, dirpath_of_string p);parse rem + | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem + | "-R" :: d :: "-as" :: [] -> usage () + | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-debug" :: rem -> set_debug (); parse rem -- cgit v1.2.3