diff options
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 56 |
1 files changed, 41 insertions, 15 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1cef729916..dde1274152 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -25,17 +25,42 @@ let open_header = ["Nativevalues"; let open_header = List.map mk_open open_header (* Directory where compiled files are stored *) -let output_dir = ".coq-native" +let output_dir = ref ".coq-native" -(* Extension of genereted ml files, stored for debugging purposes *) +(* Extension of generated ml files, stored for debugging purposes *) let source_ext = ".native" let ( / ) = Filename.concat -(* We have to delay evaluation of include_dirs because coqlib cannot be guessed -until flags have been properly initialized *) -let include_dirs () = - [Filename.get_temp_dir_name (); Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] +(* Directory for temporary files for the conversion and normalisation + (as opposed to compiling the library itself, which uses [output_dir]). *) +let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "") + +let () = at_exit (fun () -> + if Lazy.is_val my_temp_dir then + try + let d = Lazy.force my_temp_dir in + Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d); + Unix.rmdir d + with e -> + Feedback.msg_warning + Pp.(str "Native compile: failed to cleanup: " ++ + str(Printexc.to_string e) ++ fnl())) + +(* We have to delay evaluation of include_dirs because coqlib cannot + be guessed until flags have been properly initialized. It also lets + us avoid forcing [my_temp_dir] if we don't need it (eg stdlib file + without native compute or native conv uses). *) +let include_dirs = ref [] +let get_include_dirs () = + let base = match !include_dirs with + | [] -> + [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] + | _::_ as l -> l + in + if Lazy.is_val my_temp_dir + then (Lazy.force my_temp_dir) :: base + else base (* Pointer to the function linking an ML object into coq's toplevel *) let load_obj = ref (fun _x -> () : string -> unit) @@ -44,7 +69,8 @@ let rt1 = ref (dummy_value ()) let rt2 = ref (dummy_value ()) let get_ml_filename () = - let filename = Filename.temp_file "Coq_native" source_ext in + let temp_dir = Lazy.force my_temp_dir in + let filename = Filename.temp_file ~temp_dir "Coq_native" source_ext in let prefix = Filename.chop_extension (Filename.basename filename) ^ "." in filename, prefix @@ -67,8 +93,8 @@ let error_native_compiler_failed e = 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]) (include_dirs () @ load_path)) 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 let f = Filename.chop_extension ml_filename in let link_filename = f ^ ".cmo" in let link_filename = Dynlink.adapt_filename link_filename in @@ -118,7 +144,7 @@ let compile_library dir code fn = let fn = fn ^ source_ext in let basename = Filename.basename fn in let dirname = Filename.dirname fn in - let dirname = dirname / output_dir in + let dirname = dirname / !output_dir in let () = try Unix.mkdir dirname 0o755 with Unix.Unix_error (Unix.EEXIST, _, _) -> () @@ -154,11 +180,11 @@ let call_linker ?(fatal=true) env ~prefix f upds = if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; register_native_file prefix with Dynlink.Error _ as exn -> - let exn = CErrors.push exn in - if fatal then iraise exn + let exn = Exninfo.capture exn in + if fatal then Exninfo.iraise exn 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 + let f = dirname / !output_dir / basename in call_linker env ~fatal:false ~prefix f None |