Native compute: cleanup temporary files on program exit

We make a temporary directory for these files and cleanup at process
exit. The temporary directory means we don't have to guess what
extensions ocaml will produce, we can just delete everything there.

We use Lazy to avoid spamming unused directories when ahead-of-time
compiling without actually using native casts / nativenorm (typically
stdlib files).

Sadly ocaml has "create temp file" but not "create temp dir", so we
have to copy the name generation code.

Fix #10495

1 files changed, 26 insertions, 5 deletions

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 1cef729916..a62b51e8aa 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -27,15 +27,35 @@ let open_header = List.map mk_open open_header
 (* Directory where compiled files are stored *)
 let output_dir = ".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 *)
+(* 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 () =
-  [Filename.get_temp_dir_name (); Envars.coqlib () / "kernel"; Envars.coqlib () / "library"]
+  let base = [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] 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 +64,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