diff options
| author | Gaëtan Gilbert | 2019-02-20 23:22:20 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-21 12:43:17 +0100 |
| commit | 2abf8037772ee1bb9fbfa255800222663daf18e5 (patch) | |
| tree | c605450f5a0e8534e51f9d11e396d20c46e06e2a | |
| parent | 924468eb648750bf2cbb6de0b1c8f7a2960f0bf5 (diff) | |
Fix #9613 use -coqlib when invoking coqchk
In passing add -coqlib to coqchk's usage message.
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | Makefile.build | 6 | ||||
| -rw-r--r-- | 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\ |