From cd7b346ec5485138d93bc6a0308b9b8176d6e71f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 18 Aug 2020 15:39:57 +0200
Subject: 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.
---
 config/dune | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'config/dune')

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))))
-- 
cgit v1.2.3