diff options
| author | mdenes | 2013-10-28 20:32:41 +0000 |
|---|---|---|
| committer | mdenes | 2013-10-28 20:32:41 +0000 |
| commit | 1e301c9921a8b24e52e05fdcc7a92f67f99ba31c (patch) | |
| tree | 7fda8c7fd32e28f2d98c83d3ff505095afdfabac | |
| parent | 3c36e46caf34e5033ba9378674caee0efa93d809 (diff) | |
Native compiler: library compilation errors are now non fatal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16944 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | kernel/nativelib.ml | 2 | ||||
| -rw-r--r-- | library/library.ml | 18 |
2 files changed, 9 insertions, 11 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index c9da5222f6..49f84bc43b 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -76,7 +76,7 @@ let compile ml_filename code = write_ml_code ml_filename code; call_compiler ml_filename (!get_load_paths()) -(* call_linker dynamic links code for constants in environment or a *) +(* call_linker links dynamically the code for constants in environment or a *) (* conversion test. Silently fails if the file does not exist in bytecode *) (* mode, since the standard library is not compiled to bytecode with default *) (* settings. *) diff --git a/library/library.ml b/library/library.ml index d2d67f4847..1219fedec2 100644 --- a/library/library.ml +++ b/library/library.ml @@ -628,16 +628,14 @@ let save_library_to dir f = System.digest_out ch (Digest.file f'); (* 2nd checksum *) close_out ch; (* Writing native code files *) - if not !Flags.no_native_compiler then begin - let lp = Loadpath.get_load_paths () in - let map_path p = CUnix.string_of_physical_path (Loadpath.physical p) in - let lp = List.map map_path lp in - let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in - match Nativelibrary.compile_library dir ast lp fn with - | 0 -> () - | _ -> anomaly (Pp.str "Library compilation failure") - end - with reraise -> + if not !Flags.no_native_compiler then + let lp = Loadpath.get_load_paths () in + let map_path p = CUnix.string_of_physical_path (Loadpath.physical p) in + let lp = List.map map_path lp in + let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in + if not (Int.equal (Nativelibrary.compile_library dir ast lp fn) 0) then + msg_error (str "Could not compile the library to native code. Skipping.") + with reraise -> let reraise = Errors.push reraise in let () = msg_warning (str ("Removed file "^f')) in let () = close_out ch in |