Trying out github-script

.github/workflows/check-deep-tests-reusable.yml

@@ -0,0 +1,19 @@
+name: Integration Tests (Reusable Workflow)
+
+on:
+  workflow_dispatch:
+
+jobs:
+  check-deep-tests:
+    runs-on: ubuntu-18.04
+    steps:
+    - name: Checkout Dafny
+      uses: actions/checkout@v2
+      with:
+        path: dafny
+        submodules: true
+    - uses: actions/github-script@v6
+      with:
+        script: |
+          const script = require('${{ github.workspace }}/dafny/.github/workflowscheck-for-deep-tests-success.js')
+          console.log(script({github, context, core}))

.github/workflows/check-for-deep-tests-success.js

@@ -0,0 +1,27 @@
+module.exports = ({github, context, core}) => {
+  // This API doesn't support filtering by SHA, so we just
+  // fetch the first page and scan manually.
+  // That means if the run is fairly old it may be missed,
+  // but that should be rare.
+  const result = await github.rest.actions.listWorkflowRuns({
+    owner: context.repo.owner,
+    repo: context.repo.repo,
+    workflow_id: 'deep-tests.yml',
+
+  })
+  // These are ordered by creation time, so decide based on the first
+  // run for this SHA we see.
+  console.log(result)
+  for (const run of result.data.workflow_runs) {
+    console.log(run)
+    if (run.sha == context.sha) {
+      if (run.conclusion != "success") {
+        core.setFailed(`Last run of deep tests on $context.sha did not succeed!`)
+      } else {
+        // The SHA is fully-tested, exit with success
+        return
+      }
+    }
+  }
+  core.setFailed(`No run of deep tests found for $context.sha!`)
+}

.github/workflows/msbuild.yml

@@ -51,8 +51,18 @@ jobs:
     - name: Check whitespace and style
       working-directory: dafny
       run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude Dafny/Scanner.cs --exclude Dafny/Parser.cs
-
+
+  check-deep-tests:
+    runs-on: ubuntu-18.04
+    steps:
+    - uses: actions/github-script@v6
+    with:
+      script: |
+        const script = require('check-for-deep-tests-success.js')
+        console.log(script({github, context, core}))   
+ 
   integration-tests:
+    needs: check-deep-tests
     uses: ./.github/workflows/integration-tests-reusable.yml
     with:
       num_shards: 5