Merge PR #8054: [dev] Autogenerate OCaml dev files.

11 files changed, 30 insertions, 7 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index d3b347862..384e46723 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -303,7 +303,7 @@
 
 /configure*       @ejgallego
 
-/META.coq         @ejgallego
+/META.coq.in      @ejgallego
 
 /dev/build/windows @MSoegtropIMC
 # Secondary maintainer @maximedenes
diff --git a/.gitignore b/.gitignore
index 14ec71b93..0e41d6a77 100644
--- a/.gitignore
+++ b/.gitignore
@@ -179,3 +179,7 @@ test-suite/.nra.cache
 
 plugins/ssr/ssrparser.ml
 plugins/ssr/ssrvernac.ml
+
+# ocaml dev files
+.merlin
+META.coq
diff --git a/.merlin b/.merlin.in
index 404a7e793..404a7e793 100644
--- a/.merlin
+++ b/.merlin.in
diff --git a/META.coq b/META.coq.in
index b2924e324..b2924e324 100644
--- a/META.coq
+++ b/META.coq.in
diff --git a/Makefile b/Makefile
index df5caf0b7..636093d7a 100644
--- a/Makefile
+++ b/Makefile
@@ -80,7 +80,9 @@ export MLPACKFILES := $(call find, '*.mlpack')
 export ML4FILES := $(call find, '*.ml4')
 export MLGFILES := $(call find, '*.mlg')
 export CFILES := $(call findindir, 'kernel/byterun', '*.c')
-export MERLINFILES := $(call find, '.merlin')
+
+export MERLININFILES := $(call find, '.merlin.in')
+export MERLINFILES := $(MERLININFILES:.in=)
 
 # NB: The lists of currently existing .ml and .mli files will change
 # before and after a build or a make clean. Hence we do not export
@@ -175,7 +177,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ;
 
 .PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean alienclean
 
-clean: objclean cruftclean depclean docclean devdocclean
+clean: objclean cruftclean depclean docclean devdocclean camldevfilesclean
 
 cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean devdocclean
 
@@ -185,6 +187,9 @@ cruftclean: ml4clean
 	find . -name '*~' -o -name '*.annot' | xargs rm -f
 	rm -f gmon.out core
 
+camldevfilesclean:
+	rm -f $(MERLINFILES) META.coq
+
 indepclean:
 	rm -f $(GENFILES)
 	rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE)
diff --git a/Makefile.build b/Makefile.build
index c100eda40..05633cecc 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -64,7 +64,7 @@ AFTER ?=
 
 # build the different subsystems:
 
-world: coq coqide documentation revision
+world: camldevfiles coq coqide documentation revision
 
 coq: coqlib coqbinaries tools
 
diff --git a/Makefile.dev b/Makefile.dev
index 7fc1076a8..ea1a3d40a 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -15,7 +15,7 @@
 # Debug printers in dev/
 #########################
 
-.PHONY: devel printers
+.PHONY: devel printers camldevfiles
 
 DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo
 
@@ -85,13 +85,27 @@ endif
 # But these partial targets could be quite handy for quick builds
 # of specific components of Coq.
 
+###########################################################################
+# OCaml dev files
+###########################################################################
+camldevfiles: $(MERLINFILES) META.coq
+
+.merlin: .merlin.in
+	cp -a "$<" "$@"
+
+%/.merlin: %/.merlin.in
+	cp -a "$<" "$@"
+
+META.coq: META.coq.in
+	cp -a "$<" "$@"
+
 ###############################
 ### 1) general-purpose targets
 ###############################
 
 coqlight: theories-light tools coqbinaries
 
-states: theories/Init/Prelude.vo
+states: camldevfiles theories/Init/Prelude.vo
 
 miniopt: $(COQTOPEXE) pluginsopt
 minibyte: $(COQTOPBYTE) pluginsbyte
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 70a9756e5..ec72f9650 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -33,7 +33,7 @@
 
 (defun coqdev-default-directory ()
   "Return the Coq repository containing `default-directory'."
-  (let ((dir (locate-dominating-file default-directory "META.coq")))
+  (let ((dir (locate-dominating-file default-directory "META.coq.in")))
     (when dir (expand-file-name dir))))
 
 (defun coqdev-setup-compile-command ()
diff --git a/ide/.merlin b/ide/.merlin.in
index 953b5dce4..953b5dce4 100644
--- a/ide/.merlin
+++ b/ide/.merlin.in
diff --git a/plugins/.merlin b/plugins/.merlin.in
index 2ba616962..2ba616962 100644
--- a/plugins/.merlin
+++ b/plugins/.merlin.in
diff --git a/test-suite/unit-tests/.merlin b/test-suite/unit-tests/.merlin.in
index b2279de74..b2279de74 100644
--- a/test-suite/unit-tests/.merlin
+++ b/test-suite/unit-tests/.merlin.in