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

1 files changed, 9 insertions, 2 deletions

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 97ec634..8305185 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -47,6 +47,11 @@ let () = at_exit (fun () ->
           Pp.(str "Native compile: failed to cleanup: " ++
               str(Printexc.to_string e) ++ fnl()))
 
+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. It also lets
    us avoid forcing [my_temp_dir] if we don't need it (eg stdlib file
@@ -131,7 +136,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 =
@@ -147,7 +154,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
 
 let native_symbols = ref Names.DPmap.empty