From 2abf8037772ee1bb9fbfa255800222663daf18e5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 20 Feb 2019 23:22:20 +0100
Subject: Fix #9613 use -coqlib when invoking coqchk

In passing add -coqlib to coqchk's usage message.
---
 .gitlab-ci.yml     | 2 +-
 Makefile.build     | 6 +++---
 checker/checker.ml | 1 +
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b3dc1fa896..ddbd72b16d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -170,7 +170,7 @@ after_script:
     - cd _install_ci
     - find lib/coq/ -name '*.vo' -print0 > vofiles
     - for regexp in 's/.vo//' 's:lib/coq/plugins:Coq:' 's:lib/coq/theories:Coq:' 's:/:.:g'; do sed -z -i "$regexp" vofiles; done
-    - xargs -0 --arg-file=vofiles bin/coqchk -boot -silent -o -m -coqlib lib/coq/
+    - xargs -0 --arg-file=vofiles bin/coqchk -silent -o -m -coqlib lib/coq/
 
 .ci-template: &ci-template
   stage: test
diff --git a/Makefile.build b/Makefile.build
index 8afb498a63..2b401cd9e6 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -550,11 +550,11 @@ $(CSDPCERTBYTE): $(CSDPCERTCMO)
 
 .PHONY: validate check test-suite $(ALLSTDLIB).v
 
-VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m
+VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -coqlib .
 
 validate: $(CHICKEN) | $(ALLVO:.$(VO)=.vo)
 	$(SHOW)'COQCHK <theories & plugins>'
-	$(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
+	$(HIDE)$(CHICKEN) $(VALIDOPTS) $(ALLMODS)
 
 $(ALLSTDLIB).v:
 	$(SHOW)'MAKE $(notdir $@)'
@@ -828,7 +828,7 @@ theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP)
 	$(HIDE)$(BOOTCOQC) $< $(TIMING_ARG) $(TIMING_EXTRA)
 ifdef VALIDATE
 	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
-	$(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
+	$(HIDE)$(CHICKEN) $(VALIDOPTS) -norec $(call vo_to_mod,$@) \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 endif
 
diff --git a/checker/checker.ml b/checker/checker.ml
index 3db7ccdcae..4dac02210b 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -189,6 +189,7 @@ let print_usage_channel co command =
 \n  -admit module          load module and dependencies without checking\
 \n  -norec module          check module but admit dependencies without checking\
 \n\
+\n  -coqlib dir            set coqchk's standard library location\
 \n  -where                 print coqchk's standard library location and exit\
 \n  -v                     print coqchk version and exit\
 \n  -boot                  boot mode\
-- 
cgit v1.2.3