From 80bd794cc090070aad386607a81c2eacc4ba20ad Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Thu, 26 Feb 2026 12:52:47 +0000 Subject: [PATCH] Add proper error message on digest mismatch in require --- src/ecLoader.ml | 5 +++++ src/ecLoader.mli | 2 ++ src/ecScope.ml | 11 +++++++++-- tests/require_test/easycrypt.project | 6 ++++++ tests/require_test/foo1/main.ec | 7 +++++++ tests/require_test/foo2/main.ec | 9 +++++++++ tests/require_test/main.ec | 7 +++++++ tests/require_test/require.ec | 3 +++ 8 files changed, 48 insertions(+), 2 deletions(-) create mode 100644 tests/require_test/easycrypt.project create mode 100644 tests/require_test/foo1/main.ec create mode 100644 tests/require_test/foo2/main.ec create mode 100644 tests/require_test/main.ec create mode 100644 tests/require_test/require.ec diff --git a/src/ecLoader.ml b/src/ecLoader.ml index 25378c19e6..b52f663c25 100644 --- a/src/ecLoader.ml +++ b/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 = []; } diff --git a/src/ecLoader.mli b/src/ecLoader.mli index 3b5fe2d316..2338f6ad73 100644 --- a/src/ecLoader.mli +++ b/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 diff --git a/src/ecScope.ml b/src/ecScope.ml index 77325401de..476bcdae9e 100644 --- a/src/ecScope.ml +++ b/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 diff --git a/tests/require_test/easycrypt.project b/tests/require_test/easycrypt.project new file mode 100644 index 0000000000..ff9bcb9f55 --- /dev/null +++ b/tests/require_test/easycrypt.project @@ -0,0 +1,6 @@ +[general] +provers = CVC5@1.0 +provers = Z3@4.12 + +idirs=Foo2:foo2 +idirs=Foo1:foo1 diff --git a/tests/require_test/foo1/main.ec b/tests/require_test/foo1/main.ec new file mode 100644 index 0000000000..072e1ab23e --- /dev/null +++ b/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. diff --git a/tests/require_test/foo2/main.ec b/tests/require_test/foo2/main.ec new file mode 100644 index 0000000000..60b3fd730a --- /dev/null +++ b/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. diff --git a/tests/require_test/main.ec b/tests/require_test/main.ec new file mode 100644 index 0000000000..072e1ab23e --- /dev/null +++ b/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. diff --git a/tests/require_test/require.ec b/tests/require_test/require.ec new file mode 100644 index 0000000000..c986b4bc01 --- /dev/null +++ b/tests/require_test/require.ec @@ -0,0 +1,3 @@ +from Foo2 require import Main. +fail require import Main. +fail from Foo1 require import Main.