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

4 files changed, 49 insertions, 5 deletions

diff --git a/clib/cUnix.ml b/clib/cUnix.ml
index c5f6bebb8e..6e3ad59b1f 100644
--- a/clib/cUnix.ml
+++ b/clib/cUnix.ml
@@ -140,3 +140,20 @@ let same_file f1 =
           Unix.Unix_error _ -> false)
   with
       Unix.Unix_error _ -> (fun _ -> false)
+
+(* Copied from ocaml filename.ml *)
+let prng = lazy(Random.State.make_self_init ())
+
+let temp_file_name temp_dir prefix suffix =
+  let rnd = (Random.State.bits (Lazy.force prng)) land 0xFFFFFF in
+  Filename.concat temp_dir (Printf.sprintf "%s%06x%s" prefix rnd suffix)
+
+let mktemp_dir ?(temp_dir=Filename.get_temp_dir_name()) prefix suffix =
+  let rec try_name counter =
+    let name = temp_file_name temp_dir prefix suffix in
+    match Unix.mkdir name 0o700 with
+    | () -> name
+    | exception (Sys_error _ as e) ->
+      if counter >= 1000 then raise e else try_name (counter + 1)
+  in
+  try_name 0
diff --git a/clib/cUnix.mli b/clib/cUnix.mli
index 17574b3c42..55d307c724 100644
--- a/clib/cUnix.mli
+++ b/clib/cUnix.mli
@@ -65,3 +65,5 @@ val waitpid_non_intr : int -> Unix.process_status
 (** Check if two file names refer to the same (existing) file *)
 val same_file : string -> string -> bool
 
+(** Like [Stdlib.Filename.temp_file] but producing a directory. *)
+val mktemp_dir : ?temp_dir:string -> string -> string -> string
diff --git a/doc/changelog/01-kernel/11081-native-cleanup.rst b/doc/changelog/01-kernel/11081-native-cleanup.rst
new file mode 100644
index 0000000000..b3e3a78b96
--- /dev/null
+++ b/doc/changelog/01-kernel/11081-native-cleanup.rst
@@ -0,0 +1,4 @@
+- **Changed:** the native compilation (:tacn:`native_compute`) now
+  creates a directory to contain temporary files instead of putting
+  them in the root of the system temporary directory. (`#11081
+  <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert).
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