Merge branch 'master' into feat-bprint-language-server

dafny-lang · Jul 5, 2023 · a8d9fbe · a8d9fbe
2 parents d29d028 + e45ee62
commit a8d9fbe
Show file tree

Hide file tree

Showing 6 changed files with 10 additions and 12 deletions.
diff --git a/Source/XUnitExtensions/Lit/LitTestCase.cs b/Source/XUnitExtensions/Lit/LitTestCase.cs
@@ -45,8 +45,7 @@ public static LitTestCase Read(string filePath, LitTestConfiguration config) {
       config = config.WithSubstitutions(new Dictionary<string, object> {
         {"%s", filePath.Replace(@"\", "/")},
         // For class path separators
-        {".jar:%S", ".jar" + Path.PathSeparator + fullDirectoryPath},
-        {"-java:", "-java" + Path.PathSeparator}, // In Windows path separators are ";"
+        {"%{pathsep}", Path.PathSeparator.ToString()},
         {"%S", fullDirectoryPath},
         {"%t", Path.Join(fullDirectoryPath, "Output", $"{fileName}.tmp")}
       });

diff --git a/Test/comp/compile1quiet/CompileRunQuietly.dfy b/Test/comp/compile1quiet/CompileRunQuietly.dfy
@@ -8,7 +8,7 @@
 // RUN: %S/CompileRunQuietly >> "%t"
 
 // RUN: %dafny /unicodeChar:0 /compileTarget:java "%s" >> "%t"
-// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileRunQuietly-java CompileRunQuietly >> "%t"
+// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/CompileRunQuietly-java CompileRunQuietly >> "%t"
 
 // RUN: %dafny /unicodeChar:0 /compileTarget:cpp "%s" >> "%t"
 // RUN: %S/CompileRunQuietly.exe >> "%t"

diff --git a/Test/comp/compile1verbose/CompileAndThenRun.dfy b/Test/comp/compile1verbose/CompileAndThenRun.dfy
@@ -8,7 +8,7 @@
 // RUN: %S/CompileAndThenRun >> "%t"
 
 // RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:java "%s" >> "%t"
-// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileAndThenRun-java CompileAndThenRun >> "%t"
+// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/CompileAndThenRun-java CompileAndThenRun >> "%t"
 
 // RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:cpp "%s" >> "%t"
 // RUN: %S/CompileAndThenRun.exe >> "%t"

diff --git a/Test/comp/separate-compilation/usesTimesTwo.dfy b/Test/comp/separate-compilation/usesTimesTwo.dfy
@@ -12,12 +12,12 @@
 // Java
 
 // RUN: %baredafny translate java --output=%S/Inputs/producer/timesTwo %S/Inputs/producer/timesTwo.dfy
-// RUN: javac -cp %binaryDir/DafnyRuntime.jar:%S/Inputs/producer/timesTwo-java %S/Inputs/producer/timesTwo-java/timesTwo.java %S/Inputs/producer/timesTwo-java/*/*.java
+// RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java %S/Inputs/producer/timesTwo-java/timesTwo.java %S/Inputs/producer/timesTwo-java/*/*.java
 
 // RUN: %baredafny translate java --output=%S/consumer/usesTimesTwo --library=%S/Inputs/producer/timesTwo.dfy %s
-// RUN: javac -cp %binaryDir/DafnyRuntime.jar:%S/Inputs/producer/timesTwo-java:%S/consumer/usesTimesTwo-java %S/consumer/usesTimesTwo-java/usesTimesTwo.java %S/consumer/usesTimesTwo-java/*/*.java
+// RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java%{pathsep}%S/consumer/usesTimesTwo-java %S/consumer/usesTimesTwo-java/usesTimesTwo.java %S/consumer/usesTimesTwo-java/*/*.java
 
-// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/Inputs/producer/timesTwo-java:%S/consumer/usesTimesTwo-java usesTimesTwo >> "%t"
+// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java%{pathsep}%S/consumer/usesTimesTwo-java usesTimesTwo >> "%t"
 
 // Python
 
@@ -37,8 +37,7 @@
 
 // RUN: %baredafny translate go --output=%S/consumer/usesTimesTwo --library=%S/Inputs/producer/timesTwo.dfy %s
 
-// TODO: Won't work on windows
-// RUN: env GO111MODULE=auto GOPATH=%S/Inputs/producer/timesTwo-go:%S/consumer/usesTimesTwo-go go run %S/consumer/usesTimesTwo-go/src/usesTimesTwo.go >> "%t"
+// RUN: env GO111MODULE=auto GOPATH=%S/Inputs/producer/timesTwo-go%{pathsep}%S/consumer/usesTimesTwo-go go run %S/consumer/usesTimesTwo-go/src/usesTimesTwo.go >> "%t"
 
 // (Javascript doesn't support this yet)
 

diff --git a/Test/dafny0/JavaUseRuntimeLib.dfy b/Test/dafny0/JavaUseRuntimeLib.dfy
@@ -1,5 +1,5 @@
 // RUN: %dafny "%s" /useRuntimeLib /out:%S/Output/DafnyConsole.jar /compileTarget:java > "%t"
-// RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/Output/DafnyConsole.jar DafnyConsole >> "%t"
+// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Output/DafnyConsole.jar DafnyConsole >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module DafnyConsoleMod { // TODO if we name this DafnyConsole, then Java compilation fails

diff --git a/Test/git-issues/git-issue-2071.dfy b/Test/git-issues/git-issue-2071.dfy
@@ -1,6 +1,6 @@
 // RUN: %dafny /compile:1 /spillTargetCode:2 /compileTarget:java "%s" > "%t"
-// RUN: javac -cp %binaryDir/DafnyRuntime.jar:%S/git-issue-2071-java %S/git-issue-2071-java/git_issue_2071.java %S/git-issue-2071-java/*/*.java >> "%t"
-// RUN: java -ea -cp %binaryDir/DafnyRuntime.jar:%S/git-issue-2071-java git_issue_2071 >> "%t"
+// RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/git-issue-2071-java %S/git-issue-2071-java/git_issue_2071.java %S/git-issue-2071-java/*/*.java >> "%t"
+// RUN: java -ea -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/git-issue-2071-java git_issue_2071 >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function singletonSeq<T>(x: T): seq<T> {