From d079ec262eacc2149fa46b45ac23097a3333b5fe Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 15 Nov 2018 13:30:26 +0100
Subject: 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).
---
 checker/validate.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'checker/validate.ml')

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))^")")
-- 
cgit v1.2.3