Better diagnostic when version mismatch in VSUpile

PrincetonUniversity · Oct 10, 2023 · 848a90f · 848a90f
1 parent e3e5d42
commit 848a90f
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/progs/VSUpile/verif_stdlib.v b/progs/VSUpile/verif_stdlib.v
@@ -10,8 +10,11 @@ Lemma version_test: False.
          VST.veric.version.compcert_version = "3.13"%string /\
 	       stdlib.Info.version = "3.12"%string \/
          VST.veric.version.compcert_version = "3.13"%string /\
-	       stdlib.Info.version = "3.11"%string) by (compute; auto).
- assert (VST.veric.version.bitsize = stdlib.Info.bitsize) by reflexivity.
+	       stdlib.Info.version = "3.11"%string)
+       by (compute; auto;
+            match goal with |- ?G => fail 100 "Version mismatch; cannot prove" G end).
+ assert (VST.veric.version.bitsize = stdlib.Info.bitsize) by
+    (try reflexivity; match goal with |- ?G => fail 100 "Bitsize mismatch; cannot prove" G end).
 Abort.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.