Merge PR #16235: [v8.10] Backport #15271: Delay removing native_compute .ml files until exitv8.10

1 files changed, 9 insertions, 2 deletions

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 9a3cd76..86e5f51 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -33,6 +33,11 @@ let source_ext = ".native"
 
 let ( / ) = Filename.concat
 
+let delay_cleanup_file =
+  let toclean = ref [] in
+  let () = at_exit (fun () -> List.iter (fun f -> if Sys.file_exists f then Sys.remove f) !toclean) in
+  fun f -> if not !Flags.debug then toclean := f :: !toclean
+
 (* We have to delay evaluation of include_dirs because coqlib cannot be guessed
 until flags have been properly initialized *)
 let include_dirs () =
@@ -111,7 +116,9 @@ let call_compiler ?profile:(profile=false) ml_filename =
 let compile fn code ~profile:profile =
   write_ml_code fn code;
   let r = call_compiler ~profile fn in
-  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
+  (* NB: to prevent reusing the same filename we MUST NOT remove the file until exit
+     cf #15263 *)
+  delay_cleanup_file fn;
   r
 
 let compile_library dir code fn =
@@ -127,7 +134,7 @@ let compile_library dir code fn =
   let fn = dirname / basename in
   write_ml_code fn ~header code;
   let _ = call_compiler fn in
-  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn
+  delay_cleanup_file fn
 
 (* call_linker links dynamically the code for constants in environment or a  *)
 (* conversion test. *)