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

3 files changed, 14 insertions, 6 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index dbc6afd..8b8464b 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,7 +19,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2020-11-26-V93"
+  CACHEKEY: "bionic_coq-v8.13-V2020-11-26-V94"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 7398f2f..d2c7e64 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-11-26-V93"
+# CACHEKEY: "bionic_coq-v8.13-V2020-11-26-V94"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -64,11 +64,12 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.11.1" \
-    BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3"
+    BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3" \
+    COQIDE_OPAM_EDGE="lablgtk3-sourceview3.3.1.2"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
 RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \
-    opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM $CI_OPAM
+    opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
 
 RUN opam clean -a -c
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 1e1085d..54aad98 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -48,6 +48,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
@@ -142,7 +147,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
 
 type native_library = Nativecode.global list * Nativevalues.symbols
@@ -160,7 +167,7 @@ let compile_library (code, symb) 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. *)