Add proper error message on digest mismatch in require

src/ecLoader.ml

@@ -26,6 +26,11 @@ let getkind ext =
   | "eca" -> `EcA
   | _     -> raise (BadExtension ("." ^ ext))
 
+let string_of_namespace ns = 
+  match ns with
+  | `System -> "System"
+  | `Named s -> s
+
 (* -------------------------------------------------------------------- *)
 let create () = { ecl_idirs = []; }
 

src/ecLoader.mli

@@ -12,6 +12,8 @@ val getkind : string -> kind
 (* -------------------------------------------------------------------- *)
 type namespace = [ `System | `Named of string ]
 
+val string_of_namespace : namespace -> string
+
 (* -------------------------------------------------------------------- *)
 val create  : unit -> ecloader
 val aslist  : ecloader -> ((namespace option * string) * idx_t) list

src/ecScope.ml

@@ -1820,8 +1820,15 @@ module Theory = struct
     assert (scope.sc_pr_uc = None);
     List.exists (fun x ->
         if x.rqd_name = name.rqd_name then (
-          (* FIXME: raise an error message *)
-          assert (x.rqd_digest = name.rqd_digest);
+          if (x.rqd_digest <> name.rqd_digest) then begin
+            hierror "Digest mismatch, file %s%s differs from %s%s"
+              Option.(value ~default:"" (map (fun ns -> EcLoader.string_of_namespace ns ^ ":") 
+                x.rqd_namespace)) 
+              x.rqd_name
+              Option.(value ~default:"" (map (fun ns -> EcLoader.string_of_namespace ns ^ ":") 
+                name.rqd_namespace)) 
+              name.rqd_name
+          end ;
           true)
         else false)
       scope.sc_required

tests/require_test/easycrypt.project

@@ -0,0 +1,6 @@
+[general]
+provers = CVC5@1.0
+provers = Z3@4.12
+
+idirs=Foo2:foo2
+idirs=Foo1:foo1

tests/require_test/foo1/main.ec

@@ -0,0 +1,7 @@
+require import AllCore Int Real.
+
+op foo : real = 1%r.
+
+theory A.
+  op add : real -> real -> real = (+)%r.
+end A.

tests/require_test/foo2/main.ec

@@ -0,0 +1,9 @@
+require import AllCore Int.
+
+op foo : int = 2.
+
+op foo2 : int = 3.
+
+theory A.
+  op add : int -> int -> int = (-).
+end A.

tests/require_test/main.ec

@@ -0,0 +1,7 @@
+require import AllCore Int Real.
+
+op foo : real = 1%r.
+
+theory A.
+  op add : real -> real -> real = (+)%r.
+end A.

tests/require_test/require.ec

@@ -0,0 +1,3 @@
+from Foo2 require import Main.
+fail require import Main.
+fail from Foo1 require import Main.