From 3fd14dcbb64b8ab008fe742736b7a4663854c674 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Wed, 25 Sep 2024 15:32:19 -0400
Subject: [PATCH] Chore: Rust refactorings followup

---
 Makefile                                           |  2 +-
 .../Backends/Rust/Dafny-compiler-rust.dfy          |  3 ++-
 Source/DafnyCore/GeneratedFromDafny/DCOMP.cs       |  2 +-
 Source/DafnyRuntime/DafnyRuntimeRust/Cargo.lock    | 14 --------------
 4 files changed, 4 insertions(+), 17 deletions(-)

diff --git a/Makefile b/Makefile
index 10a27751966..2be7e1665f0 100644
--- a/Makefile
+++ b/Makefile
@@ -47,7 +47,7 @@ test-dafny:
 		echo "$$count test files found."; \
 		for file in $$files; do \
 			filedir=$$(dirname "$$file"); \
-			(cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest/$${filedir}"; "${DIR}"/Binaries/Dafny $(action)  "$$(basename $$file)" ); \
+			(cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest/$${filedir}"; dotnet run --project "${DIR}"/Source/Dafny -- $(action)  "$$(basename $$file)" ); \
 		done; \
 	fi
 
diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
index 278c755e94e..4a78198fb53 100644
--- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
+++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
@@ -2201,7 +2201,8 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
               case Eq(referential) => {
                 if (referential) {
                   if pointerType.Raw? {
-                    r := Error("Raw pointer comparison not properly implemented yet (need to make comp/rust/traits.dfy to pass with --raw-pointer)");
+                    // Need to make comp/rust/traits.dfy to pass with --raw-pointer)
+                    r := Error("Raw pointer comparison not properly implemented yet");
                   } else {
                     r := R.BinaryOp("==", left, right, DAST.Format.BinaryOpFormat.NoFormat());
                   }
diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
index c2cf9b0153c..d4a7ebe0d61 100644
--- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
+++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
@@ -3215,7 +3215,7 @@ public void GenExprBinary(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._
                   if (_14_referential) {
                     if (((this).pointerType).is_Raw) {
                       RAST._IExpr _out6;
-                      _out6 = (this).Error(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Raw pointer comparison not properly implemented yet (need to make comp/rust/traits.dfy to pass with --raw-pointer)"), (this).InitEmptyExpr());
+                      _out6 = (this).Error(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Raw pointer comparison not properly implemented yet"), (this).InitEmptyExpr());
                       r = _out6;
                     } else {
                       r = RAST.Expr.create_BinaryOp(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("=="), _8_left, _11_right, DAST.Format.BinaryOpFormat.create_NoFormat());
diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/Cargo.lock b/Source/DafnyRuntime/DafnyRuntimeRust/Cargo.lock
index 8acb8403031..12934c463b1 100644
--- a/Source/DafnyRuntime/DafnyRuntimeRust/Cargo.lock
+++ b/Source/DafnyRuntime/DafnyRuntimeRust/Cargo.lock
@@ -2,12 +2,6 @@
 # It is not intended for manual editing.
 version = 3
 
-[[package]]
-name = "as-any"
-version = "0.3.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5b8a30a44e99a1c83ccb2a6298c563c888952a1c9134953db26876528f84c93a"
-
 [[package]]
 name = "autocfg"
 version = "1.1.0"
@@ -18,11 +12,9 @@ checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
 name = "dafny_runtime"
 version = "0.1.0"
 dependencies = [
- "as-any",
  "itertools",
  "num",
  "once_cell",
- "paste",
 ]
 
 [[package]]
@@ -121,9 +113,3 @@ name = "once_cell"
 version = "1.18.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d"
-
-[[package]]
-name = "paste"
-version = "1.0.14"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "de3145af08024dea9fa9914f381a17b8fc6034dfb00f3a84013f7ff43f29ed4c"