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