Upgrades release smoke tests to use new CLI (#3707)

Fixes #3277. Fixes #3679.

Changes the tests of release downloads to use the new CLI
Puts all such tests in quicktests.sh and not inline in the workflow


By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.
---------

Co-authored-by: davidcok <davidcok@github.com>
Co-authored-by: Fabio Madge <fmadge@amazon.com>
Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
Co-authored-by: Remy Willems <rwillems@amazon.com>
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
Co-authored-by: stefan-aws <120379523+stefan-aws@users.noreply.github.com>
Co-authored-by: Aaron Tomb <aarontomb@gmail.com>
Co-authored-by: Alex Chew <alex-chew@users.noreply.github.com>

.github/workflows/release-downloads-nuget.yml

@@ -71,13 +71,7 @@ jobs:
       run: $((Resolve-Path -Path "bin").providerPath) | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append   
     - name: Download NuGet package
       run: dotnet tool install --global Dafny
-    ## Create a simple smoke test program
-    - name: Make test program
-      run: |
-        echo 'method Main() { assert true; print 42, "\n"; }' > a.dfy
-        echo "method m() { assert false; }" > b.dfy
-        echo "42" > expect.txt
-    ## Check that dafny and z3 run and that a simple program verifies or fails
+    ## Record versions, checking that executables run
     - name: Versions
       run: |
         z3 -version
@@ -93,40 +87,12 @@ jobs:
       if: "${{ steps.dafny.outputs.release != '' }}"
       run: version="${{ steps.dafny.outputs.release }}"; dafny -version | grep -iE "Dafny "${version:1}".[0-9]{5}"
       shell: bash
-    - name: Check
-      run: dafny /compileVerbose:0 /compile:0 a.dfy
-    - name: Check bad
-      run: dafny /compile:0 b.dfy || echo "EXPECTED FAILURE" ; exit 0
     ## Check that a simple program compiles and runs on each supported platform
-    - name: Check C# compile
-      run: |
-        dafny /compileVerbose:0 /compile:3 /compileTarget:cs /spillTargetCode:3 a.dfy
-    - name: Check Go compile
-      run: |
-        dafny /compile:3 /spillTargetCode:3 /compileTarget:go a.dfy
-    - name: Running Go artifacts
-      if: runner.os != 'Windows'
-      run: |
-        GO111MODULE=auto GOPATH=$PWD/a-go go run a-go/src/a.go | diff expect.txt -
-    - name: Running Go artifacts - Windows
-      shell: pwsh
-      if: runner.os == 'Windows'
-      run: |
-        $Env:GO111MODULE="auto"
-        $Env:GOPATH="$PWD/a-go"
-        go run a-go/src/a.go > actual.txt
-        diff expect.txt actual.txt
-    - name: Check Javascript compile
+    - name: run quicktests
       run: |
         npm install bignumber.js
-        dafny /compile:3 /spillTargetCode:3 /compileTarget:js a.dfy
-        node a.js dafny/DafnyRuntime.js > actual.txt
-        diff expect.txt actual.txt
-    - name: Check Java compile
-      run: |
-        dafny build -t:java a.dfy
-        java -jar a.jar > actual.txt
-        diff expect.txt actual.txt
+        dafny/quicktest.sh > log.txt
+        diff log.txt dafny/quicktest.out
 
   test-dafny-libraries:
 

.github/workflows/release-downloads.yml

@@ -57,77 +57,16 @@ jobs:
         Expand-Archive dafny*.zip
         mv dafny*/dafny dafny
 
-    ## Check that a simple program compiles and runs on each supported platform
-    - name: run quicktests
-      run: |
-        npm install bignumber.js
-        dafny/quicktest.sh > log.txt
-        diff log.txt dafny/quicktest.out
-    
-    ## Create a simple smoke test program
-    - name: Make test program
-      run: |
-        echo 'method Main() { assert true; print 42, "\n"; }' > a.dfy
-        echo "method m() { assert false; }" > b.dfy
-        echo "42" > expect.txt
-    ## Check that dafny and z3 run and that a simple program verifies or fails
+    ## Record versions, checking that dafny runs
     - name: Versions
       run: |
         dafny/z3/bin/z3-4.8.5 -version
         dafny/z3/bin/z3-4.12.1 -version
         dafny/dafny -version
-    - name: Check
-      run: dafny/dafny /compileVerbose:0 /compile:0 a.dfy
-    - name: Check - non Windows
-      if: runner.os != 'Windows'
-      run: |
-        dafny/dafny /compileVerbose:0 /compile:0 a.dfy
-    - name: Check - Windows
-      if: runner.os == 'Windows'
-      run: dafny/dafny /compileVerbose:0 /compile:0 a.dfy
-    - name: Check bad
-      run: dafny/dafny /compile:0 b.dfy || echo "EXPECTED FAILURE" ; exit 0
-    - name: Check bad - non Windows
-      if: runner.os != 'Windows'
-      run: dafny/dafny /compile:0 b.dfy || echo "EXPECTED FAILURE"
-    - name: Check bad - Windows
-      if: runner.os == 'Windows'
-      run: (dafny/Dafny.exe /compile:0 b.dfy || echo "EXPECTED FAILURE") ; exit 0
-    - name: Check C# compile
-      run: |
-        dafny/dafny /compileVerbose:0 /compile:3 /compileTarget:cs /spillTargetCode:3 a.dfy
-    - name: Check Go compile
-      run: |
-        dafny/dafny /compile:3 /spillTargetCode:3 /compileTarget:go a.dfy
-    - name: Running Go artifacts
-      if: runner.os != 'Windows'
-      run: |
-        GO111MODULE=auto GOPATH=$PWD/a-go go run a-go/src/a.go > actual.txt
-        diff expect.txt actual.txt
-    - name: Running Go artifacts - Windows
-      shell: pwsh
-      if: runner.os == 'Windows'
-      run: |
-        $Env:GO111MODULE="auto"
-        $Env:GOPATH="$PWD/a-go"
-        go run a-go/src/a.go > actual.txt
-        diff expect.txt actual.txt
-    - name: Check Javascript compile
-      run: |
-        dafny/dafny /compile:3 /spillTargetCode:3 /compileTarget:js a.dfy
-        node a.js dafny/DafnyRuntime.js > actual.txt
-        diff expect.txt actual.txt
-    - name: Check Java compile
-      run: |
-        (ls dafny/DafnyRuntime.jar || echo NO DafnyRuntime.jar )
-        dafny/dafny /compile:3 /spillTargetCode:3 /compileTarget:java a.dfy
-    - name: Check Java artifacts
-      if: runner.os != 'Windows'
-      run: |
-        java -cp a-java:dafny/DafnyRuntime.jar a > actual.txt
-        diff expect.txt actual.txt
-    - name: Check Java artifacts - Windows
-      if: runner.os == 'Windows'
+    
+    ## Check that a simple program compiles and runs on each supported platform
+    - name: run quicktests
       run: |
-        java -cp "a-java;dafny/DafnyRuntime.jar" a > actual.txt
-        diff expect.txt actual.txt
+        npm install bignumber.js
+        dafny/quicktest.sh > log.txt
+        diff log.txt dafny/quicktest.out

Scripts/dafny

@@ -8,7 +8,8 @@ while [ -h "$SOURCE" ]; do
     SOURCE="$(readlink "$SOURCE")"
     [[ $SOURCE != /* ]] && SOURCE="$DIR/$SOURCE"
 done
-DAFNY_ROOT="$( cd -P "$( dirname $( dirname "$SOURCE" ))" && pwd )"
+DIR=$(dirname "$SOURCE")
+DAFNY_ROOT=$( cd -P "$DIR" && pwd )/..
 
 MY_OS=$(uname -s)
 if [ "${MY_OS:0:5}" == "MINGW" ] || [ "${MY_OS:0:6}" == "CYGWIN" ]; then

Scripts/quicktest.out

@@ -1,27 +1,49 @@
+Using: ../../Scripts/dafny
 Should succeed
 
 Dafny program verifier finished with 1 verified, 0 errors
 Should fail
 b.dfy(1,24): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 1 error
-Compiling on C#
+Running with C#
 
 Dafny program verifier finished with 0 verified, 0 errors
 (42, 131)
-Compiling to Javascript
+Running with Javascript
 
 Dafny program verifier finished with 0 verified, 0 errors
 (42, 131)
-Compiling to Java
+Running with Java
 
 Dafny program verifier finished with 0 verified, 0 errors
 (42, 131)
-Compiling to Go
+Running with Go
 
 Dafny program verifier finished with 0 verified, 0 errors
 (42, 131)
-Compiling to Python
+Running with Python
+
+Dafny program verifier finished with 0 verified, 0 errors
+(42, 131)
+Building with C#
+
+Dafny program verifier finished with 0 verified, 0 errors
+(42, 131)
+Building with Javascript
+
+Dafny program verifier finished with 0 verified, 0 errors
+(42, 131)
+Building with Java
+
+Dafny program verifier finished with 0 verified, 0 errors
+(42, 131)
+Building with Go
+
+Dafny program verifier finished with 0 verified, 0 errors
+(42, 131)
+(42, 131)
+Building with Python
 
 Dafny program verifier finished with 0 verified, 0 errors
 (42, 131)

Scripts/quicktest.sh

@@ -5,18 +5,43 @@ echo "method m() { assert 1+1 == 3; }" > b.dfy
 echo 'method Main() { print (42,131), "\n"; }' > c.dfy
 
 DIR="$(dirname ${BASH_SOURCE[0]})"
+if [ -n "$1" ]; then
+  DAFNY=$1
+else
+  DAFNY=$DIR/dafny
+fi
+echo "Using:" $DAFNY
+
 echo Should succeed
-$DIR/dafny /compile:0 a.dfy
+$DAFNY verify a.dfy
 echo Should fail
-$DIR/dafny /compile:0 -useBaseNameForFileName b.dfy
-echo Compiling on C#
-$DIR/dafny /compile:3 /compileVerbose:0 /compileTarget:cs c.dfy
-echo Compiling to Javascript
-$DIR/dafny /compile:3 /compileVerbose:0 /compileTarget:js c.dfy
-echo Compiling to Java
-$DIR/dafny /compile:3 /compileVerbose:0 /compileTarget:java c.dfy
-echo Compiling to Go
-$DIR/dafny /compile:3 /compileVerbose:0 /compileTarget:go c.dfy
-echo Compiling to Python
-$DIR/dafny /compile:3 /compileVerbose:0 /compileTarget:py c.dfy
-rm -rf a.dfy b.dfy c.dfy c-go c-java c-py c.jar c
+$DAFNY verify --use-basename-for-filename  b.dfy
+echo Running with C#
+$DAFNY run -t:cs c.dfy
+echo Running with Javascript
+$DAFNY run -t:js c.dfy
+echo Running with Java
+$DAFNY run -t:java c.dfy
+echo Running with Go
+$DAFNY run -t:go c.dfy
+echo Running with Python
+$DAFNY run -t:py c.dfy
+echo Building with C#
+rm -rf c-go c-java c-py c.jar c c.dll c.exe c.js c.runtimeconfig.json
+$DAFNY build -t:cs c.dfy
+dotnet c.dll
+echo Building with Javascript
+$DAFNY build -t:js c.dfy
+node c.js
+echo Building with Java
+$DAFNY build -t:java c.dfy
+java -jar c.jar
+echo Building with Go
+$DAFNY build -t:go c.dfy
+./c
+(cd c-go; GO111MODULE=auto GOPATH=`pwd` go run src/c.go)
+echo Building with Python
+$DAFNY build -t:py c.dfy
+python c-py/c.py
+
+rm -rf a.dfy b.dfy c.dfy c-go c-java c-py c.jar c c.dll c.exe c.js c.runtimeconfig.json