feat: use external index for standalone testbed

.github/workflows/pages.yaml

@@ -12,6 +12,11 @@ on:
         type: boolean
         required: false
         default: true
+      index-artifact:
+        description: 'Use local index artifact instead of the reservoir-index repository'
+        type: boolean
+        required: false
+        default: true
   # Enable running this workflow manually from the Actions tab
   workflow_dispatch:
 
@@ -45,21 +50,21 @@ jobs:
         run: gh run download -n results
         env:
           GH_TOKEN: ${{ github.token }}
-      - name: Download Index (CI)
-        if: inputs.ci
+      - name: Download Index Artifact
+        if: inputs.index-artifact
         uses:  actions/download-artifact@v3
         with:
           name: index
-      - name: Download Index (Standalone)
-        if: (!inputs.ci)
+      - name: Download Index Repository
+        if: (!inputs.index-artifact)
         run: |
           mkdir index
           gh api repos/leanprover/reservoir-index/tarball \
             | tar -xvz -C index --strip-component=1
         env:
           GH_TOKEN: ${{ github.token }}
       - name: Create Manifest
-        run: ./bundle.py ${{ inputs.ci && 'index.json' || 'index' }} results.json -o manifest.json
+        run: ./bundle.py ${{ inputs.index-artifact && 'index.json' || 'index' }} results.json -o manifest.json
         env:
           GH_TOKEN: ${{ github.token }}
       - name: Upload Manifest
@@ -87,7 +92,7 @@ jobs:
         run: npm ci
       - name: Build Site
         run: npm run generate
-      - name: Download Index
+      - name: Download Index Repository
         run: |
           mkdir .output/public/index
           gh api repos/leanprover/reservoir-index/tarball \

.github/workflows/testbed.yaml

@@ -7,8 +7,8 @@ on:
   # Enable running this workflow from ci.yml
   workflow_call:
     inputs:
-      ci:
-        description: 'Used to distinguish a CI workflow call from a standalone workflow'
+      index-artifact:
+        description: 'Use local index artifact instead of the reservoir-index repository'
         type: boolean
         required: false
         default: true
@@ -47,19 +47,24 @@ jobs:
           echo "toolchain=leanprover/lean4:$latest" >> "$GITHUB_OUTPUT"
         env:
           GH_TOKEN: ${{ github.token }}
-      - name: Download Index (CI)
-        if: inputs.ci
+      - name: Download Index Artifact
+        if: inputs.index-artifact
         uses: actions/download-artifact@v3
         with:
           name: index
-      - name: Download Index (Standalone)
-        if: (!inputs.ci)
-        run: gh run download -n index
+      - name: Download Index Repository
+        if: (!inputs.index-artifact)
+        run: |
+          mkdir index
+          gh api repos/leanprover/reservoir-index/tarball \
+            | tar -xvz -C index --strip-component=1
         env:
           GH_TOKEN: ${{ github.token }}
       - name: Create Matrix
         run: |
-          ./testbed-create.py index.json ${{ inputs.toolchain || steps.find-toolchain.outputs.toolchain }} -o matrix.json \
+          ./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)}} \
             -X ${{github.ref_name == 'master' && 'testbed-exclusions.txt' || 'testbed-dev-exclusions.txt'}}
       - name: Upload Matrix

bundle.py

@@ -1,20 +1,17 @@
 #!/usr/bin/env python3
+from utils import run_cmd, load_index
 from datetime import datetime
 import argparse
-import os
-import subprocess
 import json
 
 RELEASE_REPO = 'leanprover/lean4'
 def query_toolchain_releases():
-  child = subprocess.run([
+  out = run_cmd(
     'gh', 'api', '--paginate',
     f'repos/{RELEASE_REPO}/releases',
     '-q', '.[] | .tag_name'
-  ], stdout=subprocess.PIPE, stderr=subprocess.PIPE)
-  if child.returncode != 0:
-    raise RuntimeError(child.stderr.decode().strip())
-  return [f'{RELEASE_REPO}:{ver}' for ver in child.stdout.decode().splitlines()]
+  )
+  return [f'{RELEASE_REPO}:{ver}' for ver in out.decode().splitlines()]
 
 if __name__ == "__main__":
   parser = argparse.ArgumentParser()
@@ -26,19 +23,7 @@ def query_toolchain_releases():
     help='file to output the bundle manifest')
   args = parser.parse_args()
 
-  if os.path.isdir(args.index):
-    pkgs = list()
-    for owner in os.listdir(args.index):
-      owner_dir = os.path.join(args.index, 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))
-    pkgs = sorted(pkgs, key=lambda pkg: pkg['stars'], reverse=True)
-  else:
-    with open(args.index, 'r') as f:
-      pkgs = json.load(f)
-
+  pkgs = load_index(args.index)
   with open(args.results, 'r') as f:
     results: 'dict[str, dict[str, any]]' = json.load(f)
 

query.py

@@ -1,26 +1,11 @@
 #!/usr/bin/env python3
+from utils import paginate, run_cmd
 from datetime import datetime
 import argparse
-import itertools
 import os
-import subprocess
 import json
 import logging
 
-# from https://antonz.org/page-iterator/
-def paginate(iterable, page_size):
-  it = iter(iterable)
-  slicer = lambda: list(itertools.islice(it, page_size))
-  return iter(slicer, [])
-
-def run_cmd(*args: str) -> bytes:
-  child = subprocess.run(args, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
-  if child.returncode != 0:
-    raise RuntimeError(child.stderr.decode().strip())
-  elif len(child.stderr) > 0:
-    logging.error(child.stderr.decode())
-  return child.stdout
-
 REPO_QUERY="""
 query($repoIds: [ID!]!) {
   nodes(ids: $repoIds) {
@@ -73,7 +58,6 @@ def query_lake_repos(limit: int) -> 'list[str]':
     )
   return out.decode().splitlines()
 
-
 if __name__ == "__main__":
   parser = argparse.ArgumentParser()
   parser.add_argument('-L', '--limit', type=int, default=100,

testbed-create.py

@@ -1,14 +1,13 @@
 #!/usr/bin/env python3
-from datetime import datetime
+from utils import load_index
 import json
+import itertools
 import argparse
-import os
-
 
 if __name__ == "__main__":
   parser = argparse.ArgumentParser()
-  parser.add_argument('manifest',
-    help="package index manifest (e.g., from query)")
+  parser.add_argument('index',
+    help="package index (directory or manifest)")
   parser.add_argument('toolchain',
     help="Lean toolchain on build the packages on")
   parser.add_argument('-n', '--num', type=int, default=10,
@@ -24,9 +23,6 @@
     with open(file, 'r') as f:
       for line in f: exclusions.add(line.strip())
 
-  with open(args.manifest, 'r') as f:
-    pkgs = json.load(f)
-
   def create_entry(pkg: 'dict[str, any]'):
     return {
       'id': pkg['id'],
@@ -35,12 +31,13 @@ def create_entry(pkg: 'dict[str, any]'):
       'toolchain': args.toolchain
     }
 
+  pkgs = load_index(args.index)
   pkgs = filter(lambda pkg: pkg['fullName'] not in exclusions, pkgs)
   pkgs = map(create_entry, pkgs)
-  pkgs = list(pkgs)[0:args.num]
+  pkgs = list(itertools.islice(pkgs, args.num))
 
-  if args.output is not None:
-    print(json.dumps(pkgs, indent=2))
+  if args.output is None:
+    print(json.dumps(pkgs))
   else:
     with open(args.output, 'w') as f:
-      f.write(json.dumps(pkgs, indent=2))
+      f.write(json.dumps(pkgs))

utils.py

@@ -0,0 +1,34 @@
+import itertools
+import json
+import logging
+import os
+import subprocess
+
+def load_index(path: str):
+  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))
+    pkgs = sorted(pkgs, key=lambda pkg: pkg['stars'], reverse=True)
+  else:
+    with open(path, 'r') as f:
+      pkgs = json.load(f)
+  return pkgs
+
+# from https://antonz.org/page-iterator/
+def paginate(iterable, page_size):
+  it = iter(iterable)
+  slicer = lambda: list(itertools.islice(it, page_size))
+  return iter(slicer, [])
+
+def run_cmd(*args: str) -> bytes:
+  child = subprocess.run(args, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
+  if child.returncode != 0:
+    raise RuntimeError(child.stderr.decode().strip())
+  elif len(child.stderr) > 0:
+    logging.error(child.stderr.decode())
+  return child.stdout