[dev] Autogenerate OCaml dev files.

For now we only copy the templates, but we could do more fancy stuff.

This helps to be compatible with build systems that take care of these
files automatically, see:
https://github.com/coq/coq/pull/6857#discussion_r202096579

11 files changed, 30 insertions, 7 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 192a2b181..042e18bd0 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -313,7 +313,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 a7c8da163..a7c8da163 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 84f86c99a..b60fff0db 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 8f7d21694..59097bd91 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