From 78c3d736a6a1c74d9bc8317e15895a1a0fbab341 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 10 Mar 2018 02:03:08 +0100
Subject: [build] Build checker generated files using a make rule.

Currently, `configure.ml` does copy/link some files from `kernel` to
`checker` in an ad-hoc way. Instead, it is preferable to add a copy
rule to make and let it handle the dependencies properly.

This also fixes a dependency bug in Windows, as files wouldn't be
properly refreshed if `configure` was not run each time.
---
 Makefile.checker | 24 ++++++++++++++++++++----
 configure.ml     | 11 -----------
 2 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/Makefile.checker b/Makefile.checker
index 172c64af3..dd1f6d514 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -34,6 +34,20 @@ CHECKMLLIBFILE := checker/.mllibfiles
 CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE))
 -include $(CHECKERDEPS)
 
+# Copied files
+checker/esubst.mli: kernel/esubst.mli
+	cp -a $< $@
+	sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
+checker/esubst.ml: kernel/esubst.ml
+	cp -a $< $@
+	sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
+checker/names.mli: kernel/names.mli
+	cp -a $< $@
+	sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
+checker/names.ml: kernel/names.ml
+	cp -a $< $@
+	sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
+
 ifeq ($(BEST),opt)
 $(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml
 	$(SHOW)'OCAMLOPT -o $@'
@@ -57,13 +71,15 @@ checker/check.cmxa: checker/check.mllib | md5chk
 	$(SHOW)'OCAMLOPT -a -o $@'
 	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
-$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES))
+CHECKGENFILES:=$(addprefix checker/, names.mli names.ml esubst.mli esubst.ml)
+
+$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES) $(CHECKGENFILES))
 	$(SHOW)'OCAMLDEP  checker/MLFILES checker/MLIFILES'
-	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(filter checker/%, $(MLFILES) $(MLIFILES)) $(TOTARGET)
+	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(filter checker/%, $(MLFILES) $(MLIFILES) $(CHECKGENFILES)) $(TOTARGET)
 
-$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) | $(OCAMLLIBDEP)
+$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES) $(CHECKGENFILES)) | $(OCAMLLIBDEP)
 	$(SHOW)'OCAMLLIBDEP  checker/MLLIBFILES checker/MLPACKFILES'
-	$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET)
+	$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES) $(CHECKGENFILES)) $(TOTARGET)
 
 checker/%.cmi: checker/%.mli
 	$(SHOW)'OCAMLC    $<'
diff --git a/configure.ml b/configure.ml
index e77310eb7..d4750700b 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1247,17 +1247,6 @@ let write_configml f =
 
 let _ = write_configml "config/coq_config.ml"
 
-(** * Symlinks or copies for the checker *)
-
-let _ =
-  let prog, args, prf =
-    if arch = "win32" then "cp", [], ""
-    else "ln", ["-s"], "../" in
-  List.iter (fun file ->
-    ignore(run "rm" ["-f"; "checker/"^file]);
-    ignore(run ~fatal:true prog (args @ [prf^"kernel/"^file;"checker/"^file])))
-  [ "esubst.ml"; "esubst.mli"; "names.ml"; "names.mli" ]
-
 (** * Build the config/Makefile file *)
 
 let write_makefile f =
-- 
cgit v1.2.3