diff options
| author | Gaëtan Gilbert | 2018-11-15 13:30:26 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-21 13:42:14 +0100 |
| commit | d079ec262eacc2149fa46b45ac23097a3333b5fe (patch) | |
| tree | 4bd801060b02da1efa9ef2169890e78333ca7805 /Makefile.build | |
| parent | e0db7f1baef37bb60db2dd1c963572f175392783 (diff) | |
More informative error on vo validation failure
Now that the checker shares code with the kernel using md5 cic.mli
doesn't work. We could md5 declarations.ml but this would miss changes
to constr (and cic.mli already missed changes to names, univs).
Instead we just print a bit of information (the last seen type
name/annotation) when validate fails. This should help debugging when
forgetting to update values.ml without the full verbosity of -debug.
As such there is no need to -debug in the makefile validate
target (NB: CI has an independent implementation of the validate rule
since the vos are installed there).
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index ee856aae8e..fb84a131c7 100644 --- a/Makefile.build +++ b/Makefile.build @@ -612,7 +612,7 @@ VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m validate: $(CHICKEN) | $(ALLVO) $(SHOW)'COQCHK <theories & plugins>' - $(HIDE)$(CHICKEN) -boot -debug $(VALIDOPTS) $(ALLMODS) + $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) $(ALLSTDLIB).v: $(SHOW)'MAKE $(notdir $@)' |