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 /checker/validate.ml | |
| 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 'checker/validate.ml')
| -rw-r--r-- | checker/validate.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/checker/validate.ml b/checker/validate.ml index c214409a2c..b85944f94f 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -143,10 +143,8 @@ let validate debug v x = let o = Obj.repr x in try val_gen v mt_ec o with ValidObjError(msg,ctx,obj) -> - if debug then begin + (if debug then let ctx = List.rev_map print_frame ctx in - print_endline ("Validation failed: "^msg); print_endline ("Context: "^String.concat"/"ctx); - pr_obj obj - end; - failwith "vo structure validation failed" + pr_obj obj); + failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")") |