From a1bdaf0635b5d5b9e007662f324dd526ba0fe8d3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 9 Oct 2018 18:21:04 +0200
Subject: [checker] Refactor by sharing code with the kernel

For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.

With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.

We also rename some files from the checker so that they don't clash with
kernel files.
---
 Makefile.checker | 45 ++++++++++++---------------------------------
 1 file changed, 12 insertions(+), 33 deletions(-)

(limited to 'Makefile.checker')

diff --git a/Makefile.checker b/Makefile.checker
index 3d1d251701..a0f0778d49 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -22,7 +22,7 @@ CHICKEN:=bin/coqchk$(EXE)
 
 # The sources
 
-CHKLIBS:= -I config -I clib -I lib -I checker
+CHKLIBS:= -I config -I clib -I lib -I checker -I kernel -I kernel/byterun
 
 ## NB: currently, both $(OPTFLAGS) and $(BYTEFLAGS) contain -thread
 
@@ -34,22 +34,9 @@ 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): config/config.cmxa checker/check.cmxa checker/coqchk.mli checker/coqchk.ml
+$(CHICKEN): config/config.cmxa clib/clib.cmxa lib/lib.cmxa kernel/kernel.cmxa \
+checker/check.cmxa $(LIBCOQRUN) checker/coqchk.mli checker/coqchk.ml
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
 	$(STRIP_HIDE) $@
@@ -59,30 +46,29 @@ $(CHICKEN): $(CHICKENBYTE)
 	cp $< $@
 endif
 
-$(CHICKENBYTE): config/config.cma checker/check.cma checker/coqchk.mli checker/coqchk.ml
+$(CHICKENBYTE): config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma \
+checker/check.cma $(LIBCOQRUN) checker/coqchk.mli checker/coqchk.ml
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^
+	$(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) -cclib -lcoqrun $(VMBYTEFLAGS) -o $@ $^
 
-checker/check.cma: checker/check.mllib | md5chk
+checker/check.cma: checker/check.mllib
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
-checker/check.cmxa: checker/check.mllib | md5chk
+checker/check.cmxa: checker/check.mllib
 	$(SHOW)'OCAMLOPT -a -o $@'
 	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
-CHECKGENFILES:=$(addprefix checker/, names.mli names.ml esubst.mli esubst.ml)
-
-CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) $(CHECKGENFILES) \
+CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) \
   $(filter dev/checker_%, $(MLFILES) $(MLIFILES))
 
-$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES) $(CHECKGENFILES))
+$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES))
 	$(SHOW)'OCAMLDEP  checker/MLFILES checker/MLIFILES'
 	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(CHECKMLFILES) $(TOTARGET)
 
-$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES) $(CHECKGENFILES)) | $(OCAMLLIBDEP)
+$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) | $(OCAMLLIBDEP)
 	$(SHOW)'OCAMLLIBDEP  checker/MLLIBFILES checker/MLPACKFILES'
-	$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES) $(CHECKGENFILES)) $(TOTARGET)
+	$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET)
 
 checker/%.cmi: checker/%.mli
 	$(SHOW)'OCAMLC    $<'
@@ -104,13 +90,6 @@ dev/checker_%.cmi: dev/checker_%.mli
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $<
 
-md5chk:
-	$(SHOW)'MD5SUM cic.mli'
-	$(HIDE)if grep -q "^MD5 $$($(OCAML) tools/md5sum.ml checker/cic.mli)$$" checker/values.ml; \
-	       then true; else echo "Error: outdated checker/values.ml" >&2; false; fi
-
-.PHONY: md5chk
-
 # For emacs:
 # Local Variables:
 # mode: makefile
-- 
cgit v1.2.3