diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml index 767f9ac..184fff7 100644 --- a/.github/workflows/pages.yaml +++ b/.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,13 +50,13 @@ 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 \ @@ -59,7 +64,7 @@ jobs: 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 \ diff --git a/.github/workflows/testbed.yaml b/.github/workflows/testbed.yaml index e69bb62..1032e6b 100644 --- a/.github/workflows/testbed.yaml +++ b/.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 diff --git a/bundle.py b/bundle.py index e33b998..6886122 100755 --- a/bundle.py +++ b/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) diff --git a/query.py b/query.py index c3929c8..382472a 100755 --- a/query.py +++ b/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, diff --git a/testbed-create.py b/testbed-create.py index cb45f2f..e7babb4 100755 --- a/testbed-create.py +++ b/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)) diff --git a/utils.py b/utils.py new file mode 100644 index 0000000..9890431 --- /dev/null +++ b/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