Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 29 insertions, 25 deletions

diff --git a/Makefile.checker b/Makefile.checker
index 3ea0bace..172c64af 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -1,10 +1,12 @@
-#######################################################################
-#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
-# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
-#   \VV/  #############################################################
-#    //   #      This file is distributed under the terms of the      #
-#         #       GNU Lesser General Public License Version 2.1       #
-#######################################################################
+##########################################################################
+##         #   The Coq Proof Assistant / The Coq Development Team       ##
+##  v      #   INRIA, CNRS and contributors - Copyright 1999-2018       ##
+## <O___,, #       (see CREDITS file for the list of authors)           ##
+##   \VV/  ###############################################################
+##    //   #    This file is distributed under the terms of the         ##
+##         #     GNU Lesser General Public License Version 2.1          ##
+##         #     (see LICENSE file for the text of the license)         ##
+##########################################################################
 
 ## Makefile rules for building Coqchk
 
@@ -20,16 +22,22 @@ CHICKEN:=bin/coqchk$(EXE)
 
 # The sources
 
-CHKLIBS:= -I config -I lib -I checker
+CHKLIBS:= -I config -I clib -I lib -I checker
 
 ## NB: currently, both $(OPTFLAGS) and $(BYTEFLAGS) contain -thread
 
 # The rules
 
+CHECKMLDFILE := checker/.mlfiles
+CHECKMLLIBFILE := checker/.mllibfiles
+
+CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE))
+-include $(CHECKERDEPS)
+
 ifeq ($(BEST),opt)
-$(CHICKEN): checker/check.cmxa checker/main.ml
+$(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml
 	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(SYSCMXA) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
+	$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
 	$(STRIP) $@
 	$(CODESIGN) $@
 else
@@ -37,9 +45,9 @@ $(CHICKEN): $(CHICKENBYTE)
 	cp $< $@
 endif
 
-$(CHICKENBYTE): checker/check.cma checker/main.ml
+$(CHICKENBYTE): checker/check.cma checker/main.mli checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(SYSCMA) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^
+	$(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^
 
 checker/check.cma: checker/check.mllib | md5chk
 	$(SHOW)'OCAMLC -a -o $@'
@@ -49,17 +57,13 @@ checker/check.cmxa: checker/check.mllib | md5chk
 	$(SHOW)'OCAMLOPT -a -o $@'
 	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
-checker/%.ml.d: checker/%.ml
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET)
-
-checker/%.mli.d: checker/%.mli
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET)
+$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES))
+	$(SHOW)'OCAMLDEP  checker/MLFILES checker/MLIFILES'
+	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(filter checker/%, $(MLFILES) $(MLIFILES)) $(TOTARGET)
 
-checker/%.mllib.d: checker/%.mllib | $(OCAMLLIBDEP)
-	$(SHOW)'OCAMLLIBDEP  $<'
-	$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) "$<" $(TOTARGET)
+$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) | $(OCAMLLIBDEP)
+	$(SHOW)'OCAMLLIBDEP  checker/MLLIBFILES checker/MLPACKFILES'
+	$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET)
 
 checker/%.cmi: checker/%.mli
 	$(SHOW)'OCAMLC    $<'
@@ -71,12 +75,12 @@ checker/%.cmo: checker/%.ml
 
 checker/%.cmx: checker/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $<
+	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $<
 
 md5chk:
 	$(SHOW)'MD5SUM cic.mli'
-	$(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \
-	       then true; else echo "Error: outdated checker/values.ml"; false; fi
+	$(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