diff options
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 43 |
1 files changed, 23 insertions, 20 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 494282d4e1..1e1085d5ff 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -25,7 +25,8 @@ let open_header = ["Nativevalues"; let open_header = List.map mk_open open_header (* Directory where compiled files are stored *) -let output_dir = ref ".coq-native" +let dft_output_dir = ".coq-native" +let output_dir = ref dft_output_dir (* Extension of generated ml files, stored for debugging purposes *) let source_ext = ".native" @@ -92,9 +93,14 @@ let error_native_compiler_failed e = CErrors.user_err msg let call_compiler ?profile:(profile=false) ml_filename = - let load_path = !get_load_paths () in - let load_path = List.map (fun dn -> dn / !output_dir) load_path in - let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (get_include_dirs () @ load_path)) in + (* The below path is computed from Require statements, by uniquizing + the paths, see [Library.get_used_load_paths] This is in general + hacky and we should do a bit better once we move loadpath to its + own library *) + let require_load_path = !get_load_paths () in + (* We assume that installed files always go in .coq-native for now *) + let install_load_path = List.map (fun dn -> dn / dft_output_dir) require_load_path in + let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (get_include_dirs () @ install_load_path)) in let f = Filename.chop_extension ml_filename in let link_filename = f ^ ".cmo" in let link_filename = Dynlink.adapt_filename link_filename in @@ -139,8 +145,10 @@ let compile fn code ~profile:profile = if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn; r -let compile_library dir code fn = - let header = mk_library_header dir in +type native_library = Nativecode.global list * Nativevalues.symbols + +let compile_library (code, symb) fn = + let header = mk_library_header symb in let fn = fn ^ source_ext in let basename = Filename.basename fn in let dirname = Filename.dirname fn in @@ -154,19 +162,9 @@ let compile_library dir code fn = let _ = call_compiler fn in if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn -let native_symbols = ref Names.DPmap.empty - -let get_library_native_symbols dir = - try Names.DPmap.find dir !native_symbols - with Not_found -> - CErrors.user_err ~hdr:"get_library_native_symbols" - Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++ - (str "This use case is not supported, but disabling the native compiler may help.")) - (* call_linker links dynamically the code for constants in environment or a *) (* conversion test. *) -let call_linker ?(fatal=true) env ~prefix f upds = - native_symbols := env.Environ.native_symbols; +let call_linker ?(fatal=true) ~prefix f upds = rt1 := dummy_value (); rt2 := dummy_value (); if not (Sys.file_exists f) then @@ -185,6 +183,11 @@ let call_linker ?(fatal=true) env ~prefix f upds = else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); match upds with Some upds -> update_locations upds | _ -> () -let link_library env ~prefix ~dirname ~basename = - let f = dirname / !output_dir / basename in - call_linker env ~fatal:false ~prefix f None +let link_library ~prefix ~dirname ~basename = + (* We try both [output_dir] and [.coq-native], unfortunately from + [Require] we don't know if we are loading a library in the build + dir or in the installed layout *) + let install_location = dirname / dft_output_dir / basename in + let build_location = dirname / !output_dir / basename in + let f = if Sys.file_exists build_location then build_location else install_location in + call_linker ~fatal:false ~prefix f None |