feat: option to persist testbed runs in index

.github/workflows/ci.yml

@@ -23,6 +23,19 @@ on:
           - local
         required: true
         default: current
+      toolchain:
+        description: "Lean toolchain to test against"
+        type: string
+        required: false
+      testbed-size:
+        description: "Number of packages to test"
+        type: number
+        required: false
+      save-testbed:
+        description: "Save testbed results to reservoir-index"
+        type: boolean
+        required: false
+        default: true
 
 # GITHUB_TOKEN permissions needed for deployment (copied from pages.yaml)
 permissions:
@@ -47,6 +60,9 @@ jobs:
     uses: ./.github/workflows/testbed.yaml
     with:
       index-artifact: ${{ !inputs.index || inputs.index == 'local' }}
+      toolchain: ${{ inputs.toolchain }}
+      testbed-size: ${{ inputs.testbed-size || 0 }}
+      update-index: ${{ inputs.save-testbed == true }}
   pages:
     needs: [index, testbed]
     # Run even if `index` is skipped

.github/workflows/index.yaml

@@ -8,15 +8,15 @@ on:
   workflow_call:
     inputs:
       update-index:
-        description: "Upadte reservoir-index"
+        description: "Update reservoir-index"
         type: boolean
         required: false
         default: false
   # Enable running this workflow manually from the Actions tab
   workflow_dispatch:
     inputs:
       update-index:
-        description: "Upadte reservoir-index"
+        description: "Update reservoir-index"
         type: boolean
         required: false
         default: true

.github/workflows/testbed.yaml

@@ -12,17 +12,35 @@ on:
         type: boolean
         required: false
         default: true
+      toolchain:
+        description: "Lean toolchain to test against"
+        type: string
+        required: false
+      testbed-size:
+        description: "Number of packages to test"
+        type: number
+        required: false
+      update-index:
+        description: "Save to reservoir-index"
+        type: boolean
+        required: false
+        default: false
   # Enable running this workflow manually from the Actions tab
   workflow_dispatch:
     inputs:
       toolchain:
-        description: "The Lean toolchain to test against"
+        description: "Lean toolchain to test against"
         type: string
         required: false
-      repositories:
-        description: "The number of repositories to test"
+      testbed-size:
+        description: "Number of packages to test"
         type: number
         required: false
+      update-index:
+        description: "Save to reservoir-index"
+        type: boolean
+        required: false
+        default: true
 
 # Permit only 1 concurrent run per branch, cancelling previous ones
 concurrency:
@@ -65,7 +83,7 @@ jobs:
           ./testbed-create.py -o matrix.json \
             ${{ inputs.index-artifact && 'index.json' || 'index' }} \
             ${{ inputs.toolchain || steps.find-toolchain.outputs.toolchain }}  \
-            -n ${{inputs.repositories || (github.ref_name == 'master' && 200 || 15)}} \
+            -n ${{inputs.testbed-size || (github.ref_name == 'master' && 200 || 15)}} \
             -X ${{github.ref_name == 'master' && 'testbed-exclusions.txt' || 'testbed-dev-exclusions.txt'}}
       - name: Upload Matrix
         uses: actions/upload-artifact@v3
@@ -115,16 +133,37 @@ jobs:
     steps:
       - name: Checkout
         uses: actions/checkout@v3
+      - name: Checkout External Index
+        if: inputs.update-index
+        uses: actions/checkout@v3
+        with:
+          token: ${{ secrets.PUSH_RESERVOIR_INDEX_TOKEN }}
+          repository: leanprover/reservoir-index
+          path: index
       - name: Download Individual Results
         uses: actions/download-artifact@v3
         with:
           # Without a name, downloads all artifacts
           path: testbed
       - name: Collect Outcomes
-        run: ./testbed-collect.py testbed ${{ github.run_id }} ${{ github.run_attempt }} -o testbed/results.json
+        run: |
+          ./testbed-collect.py \
+            testbed ${{ github.run_id }} ${{ github.run_attempt }} \
+            -o testbed/results.json ${{ inputs.update-index && '-D index' || '' }}
         env:
           GH_TOKEN: ${{ github.token }}
-      - name: Upload Results
+      - name: Update External Index
+        if: inputs.update-index
+        uses: EndBug/add-and-commit@v9
+        with:
+          cwd: index
+          fetch: false
+          message: |
+            chore: update w/ testbed run results
+
+            ${{github.server_url}}/${{github.repository}}/actions/runs/${{github.run_id}}/attempts/${{github.run_attempt}}
+          default_author: github_actions
+      - name: Upload Results Artifact
         uses: actions/upload-artifact@v3
         with:
           name: results

bundle.py

@@ -1,5 +1,5 @@
 #!/usr/bin/env python3
-from utils import run_cmd, load_index
+from utils import run_cmd, load_index, add_build
 from datetime import datetime
 import argparse
 import json
@@ -17,23 +17,22 @@ def query_toolchain_releases():
   parser = argparse.ArgumentParser()
   parser.add_argument('index',
     help="package index (directory or manifest)")
-  parser.add_argument('results',
+  parser.add_argument('results', nargs='?', default=None,
     help="testbed results")
   parser.add_argument('-o', '--output',
     help='file to output the bundle manifest')
   args = parser.parse_args()
 
-  pkgs = load_index(args.index)
-  with open(args.results, 'r') as f:
-    results: 'dict[str, dict[str, any]]' = json.load(f)
-
+  pkgs = load_index(args.index, include_builds=True)
   fullPkgs: 'dict[str, any]' = dict()
   for pkg in pkgs:
     fullPkgs[pkg['fullName']] = pkg
-    if 'builds' not in pkg:
-      fullPkgs[pkg['fullName']]['builds'] = list()
-  for (fullName, result) in results.items():
-    fullPkgs[fullName]['builds'].insert(0, result)
+  if args.results is not None:
+    with open(args.results, 'r') as f:
+      results: 'dict[str, dict[str, any]]' = json.load(f)
+    for (fullName, result) in results.items():
+      pkg = fullPkgs[fullName]
+      pkg['builds'] = add_build(pkg['builds'], result)
 
   data = {
     'bundledAt': datetime.utcnow().strftime("%Y-%m-%dT%H:%M:%SZ"),

testbed-collect.py

@@ -1,4 +1,5 @@
 #!/usr/bin/env python3
+from utils import add_build
 from typing import TypedDict
 from datetime import datetime
 import json
@@ -37,6 +38,8 @@ def is_build_job(job: Job, repo: str):
     help="the testbed run attempt")
   parser.add_argument('-m', '--matrix',
     help="file containing the JSON build matrix")
+  parser.add_argument('-D', '--index-dir', default=None,
+    help='directory to output hierarchical index')
   parser.add_argument('-o', '--output',
     help='file to output the bundle manifest')
   args = parser.parse_args()
@@ -68,6 +71,22 @@ def find_build_job(repo: str) -> Job:
       result['outcome'] = None
     results[entry['fullName']] = result
 
+  if args.index_dir is not None:
+    for entry in matrix:
+      pkg_dir = os.path.join(args.index_dir, entry['fullName'])
+      if not os.path.exists(pkg_dir):
+        continue
+      builds_file = os.path.join(pkg_dir, "builds.json")
+      if os.path.exists(builds_file):
+        with open(os.path.join(pkg_dir, "builds.json"), 'r') as f:
+          builds = json.loads(f)
+        builds = add_build(builds, results[entry['fullName']])
+      else:
+        builds = list()
+      with open(builds_file, 'w') as f:
+        f.write(json.dumps([results[entry['fullName']]], indent=2))
+        f.write("\n")
+
   if args.output is None:
     print(json.dumps(results, indent=2))
   else:

utils.py

@@ -4,21 +4,37 @@
 import os
 import subprocess
 
-def load_index(path: str):
+def load_index(path: str, include_builds=False):
   if os.path.isdir(path):
     pkgs = list()
     for owner in os.listdir(path):
       owner_dir = os.path.join(path, owner)
       for pkg in os.listdir(owner_dir):
-        md_file = os.path.join(owner_dir, pkg, 'metadata.json')
-        with open(md_file, 'r') as f:
-          pkgs.append(json.load(f))
+        pkg_dir = os.path.join(owner_dir, pkg)
+        with open(os.path.join(pkg_dir, 'metadata.json'), 'r') as f:
+          pkg = json.load(f)
+        if include_builds:
+          builds_file = os.path.join(pkg_dir, 'builds.json')
+          if os.path.exists(builds_file):
+            with open(builds_file, 'r') as f:
+              pkg['builds'] = json.load(f)
+          else:
+            pkg['builds'] = list()
+        pkgs.append(pkg)
     pkgs = sorted(pkgs, key=lambda pkg: pkg['stars'], reverse=True)
   else:
     with open(path, 'r') as f:
       pkgs = json.load(f)
+    if include_builds:
+      for pkg in pkgs:
+        pkg['builds'] = list()
   return pkgs
 
+def add_build(builds: list, result: dict) -> list:
+  builds = list(filter(lambda build: build['toolchain'] != result['toolchain'], builds))
+  builds.append(result)
+  return sorted(builds, key=lambda build: build['toolchain'], reverse=True)
+
 # from https://antonz.org/page-iterator/
 def paginate(iterable, page_size):
   it = iter(iterable)