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).

3 files changed, 28 insertions, 23 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))^")")
diff --git a/checker/values.ml b/checker/values.ml
index e21acd8179..0de8a3e03f 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -10,28 +10,15 @@
 
 (** Abstract representations of values in a vo *)
 
-(** NB: UPDATE THIS FILE EACH TIME cic.mli IS MODIFIED !
+(** NB: This needs updating when the types in declarations.ml and
+   their dependencies are changed. *)
 
-To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
-with a copy we maintain here:
-
-MD5 b8f0139f14e3370cd0a45d4cf69882ea checker/cic.mli
-
-*)
-
-(** We reify here the types of values present in a vo (see cic.mli),
+(** We reify here the types of values present in a vo.
     in order to validate its structure. Maybe this reification
     could become automatically generated someday ?
 
-    - [Any] stands for a value that we won't check,
-    - [Fail] means a value that shouldn't be there at all,
-    - [Tuple] provides a name and sub-values in this block
-    - [Sum] provides a name, a number of constant constructors,
-      and sub-values at each position of each possible constructed
-      variant
-    - [List] and [Opt] could have been defined via [Sum], but
-      having them here helps defining some recursive values below
-    - [Annot] is a no-op, just there for improving debug messages *)
+    See values.mli for the meaning of each constructor.
+*)
 
 type value =
   | Any
@@ -45,6 +32,7 @@ type value =
   | String
   | Annot of string * value
   | Dyn
+
   | Proxy of value ref
 
 let fix (f : value -> value) : value =
diff --git a/checker/values.mli b/checker/values.mli
index 1b1437a469..616b69907f 100644
--- a/checker/values.mli
+++ b/checker/values.mli
@@ -10,17 +10,36 @@
 
 type value =
   | Any
+  (** A value that we won't check, *)
+
   | Fail of string
+  (** A value that shouldn't be there at all, *)
+
   | Tuple of string * value array
+  (** A debug name and sub-values in this block *)
+
   | Sum of string * int * value array array
+  (** A debug name, a number of constant constructors, and sub-values
+     at each position of each possible constructed variant *)
+
   | Array of value
   | List of value
   | Opt of value
   | Int
   | String
+  (** Builtin Ocaml types. *)
+
   | Annot of string * value
+  (** Adds a debug note to the inner value *)
+
   | Dyn
+  (** Coq's Dyn.t *)
+
   | Proxy of value ref
+  (** Same as the inner value, used to define recursive types *)
+
+(** NB: List and Opt have their own constructors to make it easy to
+   define eg [let rec foo = List foo]. *)
 
 val v_univopaques : value
 val v_libsum : value