Reorganization of the current library code, under Dafny namespace (#92)

.github/workflows/nightly.yml

@@ -0,0 +1,69 @@
+# This workflow does static verification of the DafnyCore library
+name: Nightly Dafny Core verification
+
+on:
+  # Scheduled to be run sometime after the nightly build of dafny
+  schedule:
+    - cron: "7 10 * * *"
+  workflow_dispatch:
+
+concurrency:
+  group: build-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  verification:
+    continue-on-error: true
+    strategy:
+      fail-fast: false
+      matrix:
+        # nightly-latest to catch anything that breaks these tests in current development
+        # 2/18/2023 version is the first that supports logging
+        # 3.11.0 supports new CLI but does not support logging
+        version: [nightly-latest, nightly-2023-02-18-ef4f346, 3.11.0 ]
+        os: [ ubuntu-latest ]
+
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: Install Dafny
+        uses: dafny-lang/setup-dafny-action@v1.6.0
+        with:
+          dafny-version: ${{ matrix.version }}
+
+      - name: Version information
+        run: |
+          dafny --version
+          echo ${{ matrix.os }} ${{ runner.os }} ${{ matrix.version }}
+
+      - name: Upgrade outdated pip
+        run: python -m pip install --upgrade pip
+
+      - name: Install lit
+        run: pip install lit OutputCheck
+
+      - name: Set up JS dependencies
+        run: npm install bignumber.js
+
+      - name: Verify Code and Examples without logging
+        id: nolog
+        if: matrix.version == '3.11.0'
+        run: lit --time-tests -v .
+
+      - name: Verify Code and Examples
+        id: withlog
+        if: steps.nolog.conclusion == 'skipped'
+        run: |
+          lit --time-tests -v --param 'dafny_params=--log-format trx --log-format csv' .
+
+      - name: Generate Report
+        if: always() && steps.withlog.conclusion != 'skipped'
+        run: find . -name '*.csv' -print0 | xargs -0 --verbose dafny-reportgenerator summarize-csv-results --max-duration-seconds 10
+
+      - uses: actions/upload-artifact@v2  # upload test results
+        if: always() && steps.withlog.conclusion != 'skipped'
+        with:
+          name: verification-results
+          path: '**/TestResults/*.trx'
+          if-no-files-found: error

.github/workflows/tests.yml

@@ -3,12 +3,14 @@ name: Dafny Core verification
 
 on:
   # Scheduled to be run sometime after the nightly build of dafny
-  schedule:
-    - cron: "7 10 * * *"
   workflow_dispatch:
   pull_request:
     branches: [ master ]
 
+concurrency:
+  group: build-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 jobs:
   verification:
     continue-on-error: true
@@ -18,7 +20,7 @@ jobs:
         # nightly-latest to catch anything that breaks these tests in current development
         # 2/18/2023 version is the first that supports logging
         # 3.11.0 supports new CLI but does not support logging
-        version: [ nightly-latest, nightly-2023-02-18-ef4f346, 3.11.0]
+        version: [nightly-2023-02-18-ef4f346, 3.11.0 ]
         os: [ ubuntu-latest ]
 
     runs-on: ${{ matrix.os }}

README-TESTING.md

@@ -24,7 +24,7 @@ each .dfy file. The tests use dafny's new command-line syntax, using the lit
 macros `%verify` and `%run` and the like.
 
 The versions of dafny being run are set in the `tests.yml` file. The versions tested
-must be recent enough to support the new CLI syntax, so 3.11ff. Also, if 
+must be recent enough to support the new CLI syntax, so 3.11 and later. Also, if 
 verification logging is desired, the version must be at least that of 3/18/2023 when
 the logging parameters were implemented in the new CLI.