Avoid running configure when plugins/ modified

We use an indirection, producing the sorted list of subdirectories of
plugins/, so that dune can recognize it hasn't changed and doesn't
rerun configure. Since configure regenerates a timestamp this avoids
recompiling the stdlib.

Fix #12750.

3 files changed, 33 insertions, 10 deletions

diff --git a/config/dune b/config/dune
index bf1aa4f471..a30fdce9aa 100644
--- a/config/dune
+++ b/config/dune
@@ -2,8 +2,14 @@
  (name config)
  (synopsis "Coq Configuration Variables")
  (public_name coq.config)
+ (modules :standard \ list_plugins)
  (wrapped false))
 
+(executable (name list_plugins) (modules list_plugins))
+(rule (targets plugin_list)
+  (deps (source_tree %{project_root}/plugins))
+  (action (with-stdout-to %{targets} (chdir %{project_root} (run config/list_plugins.exe)))))
+
 ; Dune doesn't use configure's output, but it is still necessary for
 ; some Coq files to work; will be fixed in the future.
 (rule
@@ -13,7 +19,7 @@
    %{project_root}/configure.ml
    %{project_root}/dev/ocamldebug-coq.run
    %{project_root}/dev/header.c
-  ; Needed to generate include lists for coq_makefile
-  (source_tree %{project_root}/plugins)
+   ; Needed to generate include lists for coq_makefile
+   plugin_list
   (env_var COQ_CONFIGURE_PREFIX))
  (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
diff --git a/config/list_plugins.ml b/config/list_plugins.ml
new file mode 100644
index 0000000000..5e2827bfe0
--- /dev/null
+++ b/config/list_plugins.ml
@@ -0,0 +1,10 @@
+let plugins =
+  try Sys.readdir "plugins"
+  with _ -> [||]
+
+let () = Array.sort compare plugins
+
+let () =Array.iter (fun f ->
+    let f' = "plugins/"^f in
+    if Sys.is_directory f' && f.[0] <> '.' then print_endline f)
+    plugins
diff --git a/configure.ml b/configure.ml
index c05844198b..6863d412cc 100644
--- a/configure.ml
+++ b/configure.ml
@@ -64,8 +64,7 @@ let rec waitpid_non_intr pid =
 (** Below, we'd better read all lines on a channel before closing it,
     otherwise a SIGPIPE could be encountered by the sub-process *)
 
-let read_lines_and_close fd =
-  let cin = Unix.in_channel_of_descr fd in
+let read_lines_and_close cin =
   let lines = ref [] in
   begin
     try
@@ -78,6 +77,9 @@ let read_lines_and_close fd =
   let lines = List.rev !lines in
   try List.hd lines, lines with Failure _ -> "", []
 
+let read_lines_and_close_fd fd =
+  read_lines_and_close (Unix.in_channel_of_descr fd)
+
 (** Run some unix command and read the first line of its output.
     We avoid Unix.open_process and its non-fully-portable /bin/sh,
     especially when it comes to quoting the filenames.
@@ -109,8 +111,8 @@ let run ?(fatal=true) ?(err=StdErr) prog args =
     let pid = Unix.create_process prog argv Unix.stdin out_w fd_err in
     let () = Unix.close out_w in
     let () = Unix.close nul_w in
-    let line, all = read_lines_and_close out_r in
-    let _ = read_lines_and_close nul_r in
+    let line, all = read_lines_and_close_fd out_r in
+    let _ = read_lines_and_close_fd nul_r in
     let () = check_exit_code (waitpid_non_intr pid) in
     line, all
   with
@@ -1108,11 +1110,16 @@ let write_configml f =
   pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs;
   pr "\nlet plugins_dirs = [\n";
 
-  let plugins =
-    try Sys.readdir "plugins"
-    with _ -> [||]
+  let plugins = match open_in "config/plugin_list" with
+    | exception Sys_error _ ->
+      let plugins =
+        try Sys.readdir "plugins"
+        with _ -> [||]
+      in
+      Array.sort compare plugins;
+      plugins
+    | ch -> Array.of_list (snd (read_lines_and_close ch))
   in
-  Array.sort compare plugins;
   Array.iter
     (fun f ->
       let f' = "plugins/"^f in