Migrate almost all CLI tests to use the command based CLI (#5255)

### Description - Migrate almost all CLI tests to use the command based CLI - Tests that use options that are only available in the old CLI have not been migrated ### How has this been tested? - The tests themselves have changed <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
dafny-lang · Apr 3, 2024 · 5c8806f · 5c8806f
1 parent 9135e91
commit 5c8806f
Show file tree

Hide file tree

Showing 189 changed files with 484 additions and 475 deletions.
diff --git a/Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs b/Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs
@@ -17,7 +17,7 @@ class BuilderSyntaxTree<T> : ConcreteSyntaxTree {
  if (Builder is StatementContainer statementContainer) {
  return new BuilderSyntaxTree<StatementContainer>(statementContainer.Fork());
  } else {
- DafnyCodeGenerator.throwGeneralUnsupported(); // Warning: this is an invalid operation: cannot fork builder of type Builder.GetType()
+ DafnyCodeGenerator.ThrowGeneralUnsupported(); // Warning: this is an invalid operation: cannot fork builder of type Builder.GetType()
  throw new InvalidOperationException();
  }
  }

diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs
@@ -62,7 +62,7 @@ public class LitTests {
 
  string[] defaultResolveArgs = new[] { "resolve", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false" };
  string[] defaultVerifyArgs = new[] { "verify", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300", "--resource-limit:50e6" };
- //string[] defaultTranslateArgs = new[] { "translate", "--use-basename-for-filename", "--cores:2", "--standard-libraries:false", "--verification-time-limit:300", "--resource-limit:50e6" };
+ string[] defaultTranslateArgs = new[] { "--use-basename-for-filename", "--cores:2", "--standard-libraries:false", "--verification-time-limit:300", "--resource-limit:50e6" };
  string[] defaultBuildArgs = new[] { "build", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300", "--resource-limit:50e6" };
  string[] defaultRunArgs = new[] { "run", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300", "--resource-limit:50e6" };
 
@@ -82,8 +82,17 @@ public class LitTests {
  "%resolve", (args, config) =>
  DafnyCommand(AddExtraArgs(defaultResolveArgs, args), config, InvokeMainMethodsDirectly)
  }, {
- "%translate", (args, config) =>
- DafnyCommand(AddExtraArgs(new[] { "translate" }, args), config, InvokeMainMethodsDirectly)
+ "%translate", (args, config) => {
+ var totalArgs = args.ToList();
+ if (totalArgs.Any()) {
+ var target = totalArgs.First();
+ totalArgs = new[] { target }.Concat(defaultTranslateArgs).Concat(totalArgs.Skip(1)).ToList();
+ } else {
+ totalArgs = defaultTranslateArgs.ToList();
+ }
+ return DafnyCommand(AddExtraArgs(new[] { "translate" }, totalArgs), config,
+ InvokeMainMethodsDirectly);
+ }
  }, {
  "%verify", (args, config) =>
  DafnyCommand(AddExtraArgs(defaultVerifyArgs, args), config, InvokeMainMethodsDirectly)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/extern.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/extern.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" ExternDefs.h > "%t"
+// RUN: %run --target cpp --unicode-char false "%s" --input ExternDefs.h > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module {:extern "Extern"} Extern {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/functions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/functions.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" ExternDefs.h > "%t"
+// RUN: %run --target cpp --unicode-char false "%s" --input ExternDefs.h > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module {:extern "Extern"} Extern {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 ExternDefs.h "%s" > "%t"
+// RUN: %run --target cpp --unicode-char false --input ExternDefs.h "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 newtype uint32 = i:int | 0 <= i < 0x100000000

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy.expect
@@ -1,3 +1,3 @@
 
-Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 7 verified, 0 errors
 1
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cs "%s" %S/CSharpStyling2.cs > "%t"
+// RUN: %run "%s" --input %S/CSharpStyling2.cs > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Main() {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy.expect
@@ -1,5 +1,5 @@
 
-Dafny program verifier finished with 1 verified, 0 errors
+Dafny program verifier finished with 3 verified, 0 errors
 50
 2
 3

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArguments.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArguments.dfy
@@ -4,8 +4,8 @@
 // RUN: %run --no-verify --target:cpp --unicode-char:false "%s" Cpp Yipee >> "%t"
 // RUN: %run --no-verify --target:java "%s" -- Java --heya >> "%t"
 // RUN: %run --no-verify --target:js "%s" -- Javascript 2 >> "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" --args Python 1 >> "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" --args "Go go" 1 >> "%t"
+// RUN: %run --no-verify --target py "%s" Python 1 >> "%t"
+// RUN: %run --no-verify --target go "%s" "Go go" 1 >> "%t"
 // RUN: %build --no-verify --target:cs "%s" --output:%s.dll
 // RUN: dotnet %s.dll "dotnet" "howdy" >> "%t"
 // RUN: dotnet %s.dll "dotnet" "hello" >> "%t"

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail.dfy
@@ -1,5 +1,5 @@
 // RUN: %verify "%s" > "%t"
-// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:cs "%s" --args csharp 1 >> "%t"
+// RUN: %exits-with 3 %run --no-verify --target cs "%s" csharp 1 >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Main(args: int) {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail2.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail2.dfy
@@ -1,5 +1,5 @@
 // RUN: %verify "%s" > "%t"
-// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:cs "%s" --args csharp 1 >> "%t"
+// RUN: %exits-with 3 %run --no-verify --target cs "%s" csharp 1 >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Main(args: array<string>, dummy: int) {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Extern.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Extern.dfy
@@ -1,9 +1,9 @@
 // RUN: %verify "%s" > "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" %S/Extern2.cs >> "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" %S/Extern3.js >> "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" %S/Extern4.go >> "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" %S/SingletonOptimization.java %S/LibClass.java %S/OtherClass.java %S/AllDafny.java %S/Mixed.java %S/AllExtern.java >> "%t"
-// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" %S/Extern5.py >> "%t"
+// RUN: %run --no-verify --target cs "%s" --input %S/Extern2.cs >> "%t"
+// RUN: %run --no-verify --target js "%s" --input %S/Extern3.js >> "%t"
+// RUN: %run --no-verify --target go "%s" --input %S/Extern4.go >> "%t"
+// RUN: %run --no-verify --target java "%s" --input %S/SingletonOptimization.java --input %S/LibClass.java --input %S/OtherClass.java --input %S/AllDafny.java --input %S/Mixed.java --input %S/AllExtern.java >> "%t"
+// RUN: %run --no-verify --target py "%s" --input %S/Extern5.py >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Main() {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCopyFromTrait.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCopyFromTrait.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:4 /compileTarget:cs "%s" %S/ExternCopyFromTraitLibrary.cs > "%t"
+// RUN: %run --target cs "%s" --input %S/ExternCopyFromTraitLibrary.cs > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 /// This file tests inheritance of `:extern` annotation in traits.

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy
@@ -1,6 +1,6 @@
-// RUN: %dafny /compile:3 /compileTarget:cs "%s" %S/ExternCtors-externs/Library.cs > "%t"
-// RUN: %dafny /compile:3 /compileTarget:java "%s" %S/ExternCtors-externs/Class.java >> "%t"
-// RUN: %dafny /compile:3 /compileTarget:py "%s" %S/ExternCtors-externs/Library.py >> "%t"
+// RUN: %run --target cs "%s" --input %S/ExternCtors-externs/Library.cs > "%t"
+// RUN: %run --target java "%s" --input %S/ExternCtors-externs/Class.java >> "%t"
+// RUN: %run --target py "%s" --input %S/ExternCtors-externs/Library.py >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // FIXME: Extern constructors are currently broken in Go and JavaScript,

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternDafnyString.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternDafnyString.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /unicodeChar:0 /compileTarget:java "%s" %S/Conversions.java %S/ExternDafnyString.java > "%t"
+// RUN: %run --unicode-char false --target java "%s" --input %S/Conversions.java --input %S/ExternDafnyString.java > "%t"
 // RUN: %diff "%s.expect" "%t"
 // In this example, the extern method obtains a Java string and returns it as a Dafny string.
 

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternJavaString.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternJavaString.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /unicodeChar:0 /compileTarget:java "%s" %S/Conversions.java %S/ExternJavaString.java > "%t"
+// RUN: %run --unicode-char false --target java "%s" --input %S/Conversions.java --input %S/ExternJavaString.java > "%t"
 // RUN: %diff "%s.expect" "%t"
 // In this example, the extern method obtains a Java string and returns it as such.
 // The Dafny code converts that Java string to a Dafny string.

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternNestedModule.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternNestedModule.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:4 /spillTargetCode:2 /compileTarget:py %S/ExternNestedModule.py "%s" > "%t"
+// RUN: %run --target py "%s" --input %S/ExternNestedModule.py > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Main(){

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/JsModule.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/JsModule.dfy
@@ -1,6 +1,5 @@
 // NONUNIFORM: Javascript-specific extern test
-// RUN: %dafny /compile:3 /unicodeChar:0 "%s" /compileTarget:js > "%t"
-// note: putting /compileTarget:js after "%s" overrides user-provided option
+// RUN: %run --unicode-char false --target js "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // "url" is a built-in package in node, so it should be accessible to the

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Libraries/consumer.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Libraries/consumer.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /library:"%S/Inputs/directLibrary.dfy" /library:"%S/Inputs/secondLibrary.dfy" /compile:0 /spillTargetCode:3 "%s" > "%t"
+// RUN: %translate cs --library "%S/Inputs/directLibrary.dfy" --library "%S/Inputs/secondLibrary.dfy" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 // RUN: %OutputCheck "%s" --file-to-check="%S/consumer.cs"
 // CHECK: GloballyUniqueProducer

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/MainMethod.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/MainMethod.dfy
@@ -1,55 +1,55 @@
 // NONUNIFORM: multiple testing scenarios (could be split into several uniform tests)
 // RUN: %verify "%s" > "%t"
 
-// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:cs "%s" >> "%t"
+// RUN: %run --no-verify --main-method Cl.Static --target cs "%s" >> "%t"
+// RUN: %run --no-verify --main-method Cl.Instance --target cs "%s" >> "%t"
+// RUN: %run --no-verify --main-method Tr.Static --target cs "%s" >> "%t"
+// RUN: %run --no-verify --main-method Dt.Static --target cs "%s" >> "%t"
+// RUN: %run --no-verify --main-method Dt.Instance --target cs "%s" >> "%t"
+// RUN: %run --no-verify --main-method Co.Static --target cs "%s" >> "%t"
+// RUN: %run --no-verify --main-method Co.Instance --target cs "%s" >> "%t"
+// RUN: %run --no-verify --main-method Nt.Static --target cs "%s" >> "%t"
+// RUN: %run --no-verify --main-method Nt.Instance --target cs "%s" >> "%t"
 
-// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:js "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:js "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:js "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:js "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:js "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:js "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:js "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:js "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:js "%s" >> "%t"
+// RUN: %run --no-verify --main-method Cl.Static --target js "%s" >> "%t"
+// RUN: %run --no-verify --main-method Cl.Instance --target js "%s" >> "%t"
+// RUN: %run --no-verify --main-method Tr.Static --target js "%s" >> "%t"
+// RUN: %run --no-verify --main-method Dt.Static --target js "%s" >> "%t"
+// RUN: %run --no-verify --main-method Dt.Instance --target js "%s" >> "%t"
+// RUN: %run --no-verify --main-method Co.Static --target js "%s" >> "%t"
+// RUN: %run --no-verify --main-method Co.Instance --target js "%s" >> "%t"
+// RUN: %run --no-verify --main-method Nt.Static --target js "%s" >> "%t"
+// RUN: %run --no-verify --main-method Nt.Instance --target js "%s" >> "%t"
 
-// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:go "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:go "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:go "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:go "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:go "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:go "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:go "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:go "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:go "%s" >> "%t"
+// RUN: %run --no-verify --main-method Cl.Static --target go "%s" >> "%t"
+// RUN: %run --no-verify --main-method Cl.Instance --target go "%s" >> "%t"
+// RUN: %run --no-verify --main-method Tr.Static --target go "%s" >> "%t"
+// RUN: %run --no-verify --main-method Dt.Static --target go "%s" >> "%t"
+// RUN: %run --no-verify --main-method Dt.Instance --target go "%s" >> "%t"
+// RUN: %run --no-verify --main-method Co.Static --target go "%s" >> "%t"
+// RUN: %run --no-verify --main-method Co.Instance --target go "%s" >> "%t"
+// RUN: %run --no-verify --main-method Nt.Static --target go "%s" >> "%t"
+// RUN: %run --no-verify --main-method Nt.Instance --target go "%s" >> "%t"
 
-// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:java "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:java "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:java "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:java "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:java "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:java "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:java "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:java "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:java "%s" >> "%t"
+// RUN: %run --no-verify --main-method Cl.Static --target java "%s" >> "%t"
+// RUN: %run --no-verify --main-method Cl.Instance --target java "%s" >> "%t"
+// RUN: %run --no-verify --main-method Tr.Static --target java "%s" >> "%t"
+// RUN: %run --no-verify --main-method Dt.Static --target java "%s" >> "%t"
+// RUN: %run --no-verify --main-method Dt.Instance --target java "%s" >> "%t"
+// RUN: %run --no-verify --main-method Co.Static --target java "%s" >> "%t"
+// RUN: %run --no-verify --main-method Co.Instance --target java "%s" >> "%t"
+// RUN: %run --no-verify --main-method Nt.Static --target java "%s" >> "%t"
+// RUN: %run --no-verify --main-method Nt.Instance --target java "%s" >> "%t"
 
-// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:py "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:py "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:py "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:py "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:py "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:py "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:py "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:py "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:py "%s" >> "%t"
+// RUN: %run --no-verify --main-method Cl.Static --target py "%s" >> "%t"
+// RUN: %run --no-verify --main-method Cl.Instance --target py "%s" >> "%t"
+// RUN: %run --no-verify --main-method Tr.Static --target py "%s" >> "%t"
+// RUN: %run --no-verify --main-method Dt.Static --target py "%s" >> "%t"
+// RUN: %run --no-verify --main-method Dt.Instance --target py "%s" >> "%t"
+// RUN: %run --no-verify --main-method Co.Static --target py "%s" >> "%t"
+// RUN: %run --no-verify --main-method Co.Instance --target py "%s" >> "%t"
+// RUN: %run --no-verify --main-method Nt.Static --target py "%s" >> "%t"
+// RUN: %run --no-verify --main-method Nt.Instance --target py "%s" >> "%t"
 
 // RUN: %diff "%s.expect" "%t"
 

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Print.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Print.dfy
@@ -1,9 +1,9 @@
 // NONUNIFORM: https://github.com/dafny-lang/dafny/issues/4108 and https://github.com/dafny-lang/dafny/issues/2582
 // RUN: %verify --unicode-char false --relax-definite-assignment "%s" > "%t"
-// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:js "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:go "%s" >> "%t"
-// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:java "%s" >> "%t"
+// RUN: %run --no-verify --unicode-char false --target cs "%s" >> "%t"
+// RUN: %run --no-verify --unicode-char false --target js "%s" >> "%t"
+// RUN: %run --no-verify --unicode-char false --target go "%s" >> "%t"
+// RUN: %run --no-verify --unicode-char false --target java "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Python salts hashes so they are not deterministic.

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1quiet/CompileRunQuietly.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1quiet/CompileRunQuietly.dfy
@@ -1,19 +1,19 @@
-// RUN: %dafny /unicodeChar:0 /compileTarget:cs "%s" > "%t"
+// RUN: %build --unicode-char false --target cs "%s" > "%t"
 // RUN: dotnet %S/CompileRunQuietly.dll >> "%t"
 
-// RUN: %dafny /unicodeChar:0 /compileTarget:js "%s" >> "%t"
+// RUN: %build --unicode-char false --target js "%s" >> "%t"
 // RUN: node %S/CompileRunQuietly.js >> "%t"
 
-// RUN: %dafny /unicodeChar:0 /compileTarget:go "%s" >> "%t"
+// RUN: %build --unicode-char false --target go "%s" >> "%t"
 // RUN: %S/CompileRunQuietly >> "%t"
 
-// RUN: %dafny /unicodeChar:0 /compileTarget:java "%s" >> "%t"
-// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/CompileRunQuietly-java CompileRunQuietly >> "%t"
+// RUN: %build --unicode-char false --target java "%s" >> "%t"
+// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/CompileRunQuietly.jar CompileRunQuietly >> "%t"
 
-// RUN: %dafny /unicodeChar:0 /compileTarget:cpp "%s" >> "%t"
+// RUN: %build --unicode-char false --target cpp "%s" >> "%t"
 // RUN: %S/CompileRunQuietly.exe >> "%t"
 
-// RUN: %dafny /unicodeChar:0 /compileTarget:py "%s" >> "%t"
+// RUN: %build --unicode-char false --target py "%s" >> "%t"
 // RUN: python3 %S/CompileRunQuietly-py >> "%t"
 
  // RUN: %diff "%s.expect" "%t"

diff --git a/...ce/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy b/...ce/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy
@@ -1,19 +1,19 @@
-// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:cs "%s" > "%t"
+// RUN: %build --unicode-char false --verbose --target cs "%s" > "%t"
 // RUN: dotnet %S/CompileAndThenRun.dll >> "%t"
 
-// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:js "%s" >> "%t"
+// RUN: %build --unicode-char false --verbose --target js "%s" >> "%t"
 // RUN: node %S/CompileAndThenRun.js >> "%t"
 
-// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:go "%s" >> "%t"
+// RUN: %build --unicode-char false --verbose --target go "%s" >> "%t"
 // RUN: %S/CompileAndThenRun >> "%t"
 
-// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:java "%s" >> "%t"
-// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/CompileAndThenRun-java CompileAndThenRun >> "%t"
+// RUN: %build --unicode-char false --verbose --target java "%s" >> "%t"
+// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/CompileAndThenRun.jar CompileAndThenRun >> "%t"
 
-// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:cpp "%s" >> "%t"
+// RUN: %build --unicode-char false --verbose --target cpp "%s" >> "%t"
 // RUN: %S/CompileAndThenRun.exe >> "%t"
 
-// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:py "%s" >> "%t"
+// RUN: %build --unicode-char false --verbose --target py "%s" >> "%t"
 // RUN: python3 %S/CompileAndThenRun-py >> "%t"
 
 // RUN: %diff "%s.expect" "%t"