refactor: reorganize manifest info

* build outcome icons now link to the workflow build job
leanprover · Nov 30, 2023 · cb82d5b · cb82d5b
1 parent 96b6fdb
commit cb82d5b
Show file tree

Hide file tree

Showing 14 changed files with 172 additions and 98 deletions.
diff --git a/.github/workflows/index.yaml b/.github/workflows/index.yaml
@@ -22,7 +22,7 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v3
       - name: Query Repositories
-        run: ./query.py -o index.json -v -Q ${{github.ref_name == 'master' && 1000 || 75}}
+        run: ./query.py -o index.json -v -L ${{github.ref_name == 'master' && 1000 || 75}}
         env:
           GH_TOKEN: ${{ github.token }}
       - name: Upload Index

diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml
@@ -57,6 +57,8 @@ jobs:
           GH_TOKEN: ${{ github.token }}
       - name: Create Manifest
         run: ./bundle.py index.json results.json -o manifest.json
+        env:
+          GH_TOKEN: ${{ github.token }}
       - name: Upload Manifest
         uses: actions/upload-artifact@v3
         with:

diff --git a/.github/workflows/testbed.yaml b/.github/workflows/testbed.yaml
@@ -35,7 +35,6 @@ jobs:
     runs-on: ubuntu-latest
     outputs:
       matrix: ${{ steps.output-matrix.outputs.matrix }}
-      toolchain: ${{ inputs.toolchain || steps.find-toolchain.outputs.toolchain }}
     steps:
       - name: Checkout
         uses: actions/checkout@v3
@@ -60,7 +59,7 @@ jobs:
           GH_TOKEN: ${{ github.token }}
       - name: Create Matrix
         run: |
-          ./testbed-create.py index.json -o matrix.json \
+          ./testbed-create.py index.json ${{ inputs.toolchain || steps.find-toolchain.outputs.toolchain }} -o matrix.json \
             -n ${{inputs.repositories || (github.ref_name == 'master' && 200 || 15)}} \
             -X ${{github.ref_name == 'master' && 'testbed-exclusions.txt' || 'testbed-dev-exclusions.txt'}}
       - name: Upload Matrix
@@ -85,7 +84,7 @@ jobs:
       - name: Install Elan
         shell: bash -euo pipefail {0}
         run: |
-          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain ${{ needs.setup.outputs.toolchain }}
+          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain ${{ matrix.toolchain }}
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
       - name: Check Lean
         run: lean --version
@@ -95,7 +94,7 @@ jobs:
         name: Build
         continue-on-error: true
         # Note that this runs arbitrary untrusted code so we cannot give it secrets
-        run: ./build.sh ${{ matrix.url }} testbed ${{ needs.setup.outputs.toolchain }}
+        run: ./build.sh ${{ matrix.url }} testbed ${{ matrix.toolchain }}
       - name: Output Outcome
         run: |
           echo ${{ steps.build.outcome }} > outcome.txt
@@ -117,7 +116,9 @@ jobs:
           # Without a name, downloads all artifacts
           path: testbed
       - name: Collect Outcomes
-        run: ./testbed-collect.py testbed ${{ needs.setup.outputs.toolchain }} ${{ github.run_id }} -o testbed/results.json
+        run: ./testbed-collect.py testbed ${{ github.run_id }} ${{ github.run_attempt }} -o testbed/results.json
+        env:
+          GH_TOKEN: ${{ github.token }}
       - name: Upload Results
         uses: actions/upload-artifact@v3
         with:

diff --git a/bundle.py b/bundle.py
@@ -1,37 +1,48 @@
 #!/usr/bin/env python3
+from datetime import datetime
 import argparse
+import subprocess
 import json
 
+RELEASE_REPO = 'leanprover/lean4'
+def query_toolchain_releases():
+  child = subprocess.run([
+    '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()]
+
 if __name__ == "__main__":
   parser = argparse.ArgumentParser()
   parser.add_argument('index',
-    help="repository metadata")
+    help="package metadata")
   parser.add_argument('results',
     help="testbed results")
   parser.add_argument('-o', '--output',
     help='file to output the bundle manifest')
   args = parser.parse_args()
 
   with open(args.index, 'r') as f:
-    index = json.load(f)
+    index: 'dict[str, any]' = json.load(f)
 
   with open(args.results, 'r') as f:
-    results = json.load(f)
+    results: 'dict[str, dict[str, any]]' = json.load(f)
 
-  repos = dict()
-  for repo in index['matrix']:
+  repos: 'dict[str, any]' = dict()
+  for repo in index['packages']:
     repos[repo['id']] = repo
-    repos[repo['id']]['outcome'] = None
-  for result in results['matrix']:
-    if result['id'] in repos:
-      repos[result['id']]['outcome'] = result['outcome']
+    repos[repo['id']]['builds'] = list()
+  for (id, result) in results.items():
+    repos[id]['builds'].insert(0, result)
 
   data = {
-    "buildId": results['buildId'],
-    'builtAt': results['builtAt'],
-    'toolchain': results['toolchain'],
-    'fetchedAt': index['fetchedAt'],
-    'matrix': list(repos.values())
+    'indexedAt': index['fetchedAt'],
+    'bundledAt': datetime.utcnow().strftime("%Y-%m-%dT%H:%M:%SZ"),
+    'toolchains': query_toolchain_releases(),
+    'packages': list(repos.values())
   }
   if args.output is None:
     print(json.dumps(data))

diff --git a/nuxt.config.ts b/nuxt.config.ts
@@ -37,13 +37,13 @@ export default defineNuxtConfig({
       // Needed to prevent GitHub Pages from automatically adding trailing
       // slashes to URLs (as otherwise they are directories rather than files)
       autoSubfolderIndex: false,
-      routes: ["/", ...manifest.matrix.map((pkg) => `/packages/${pkg.id}`)]
+      routes: ["/", ...manifest.packages.map(pkg => `/packages/${pkg.id}`)]
     },
   },
   site: {
     url: 'https://reservoir.lean-lang.org',
     name: 'Reservoir',
-    description: "Lake's package repository for the Lean community.",
+    description: "Lake's package registry for the Lean community.",
     titleSeparator: '|',
     defaultLocale: 'en-US',
   },

diff --git a/query.py b/query.py
@@ -6,13 +6,15 @@
 import json
 import logging
 
-def query(num: int):
+def query(limit: int):
   query = "language:Lean stars:>1 sort:stars"
-  fields = ["name","fullName","description","license","createdAt","updatedAt","url","homepage","stargazersCount"]
+  fields = ["fullName","description","license","createdAt","updatedAt","pushedAt","url","homepage","stargazersCount"]
   child = subprocess.run([
     "gh", "search", "repos",
-    *query.split(' '), "-L", str(num), "--json", ','.join(fields),
-  ], stdout=subprocess.PIPE)
+    *query.split(' '), "-L", str(limit), "--json", ','.join(fields),
+  ], stdout=subprocess.PIPE, stderr=subprocess.PIPE)
+  if child.returncode != 0:
+    raise RuntimeError(child.stderr.decode().strip())
   return json.loads(child.stdout)
 
 def filter_lake(repo):
@@ -33,13 +35,16 @@ def filter_lake(repo):
 
 def enrich(repo: dict):
   repo['id'] = repo['fullName'].replace("-", "--").replace("/", "-")
+  repo['owner'], repo['name'] = repo['fullName'].split('/')
   repo['license'] = repo['license']['key']
   repo['stars'] = repo.pop('stargazersCount')
+  repo['updatedAt'] = max(repo['updatedAt'], repo['pushedAt'])
+  del repo['pushedAt']
   return repo
 
 if __name__ == "__main__":
   parser = argparse.ArgumentParser()
-  parser.add_argument('-Q', '--query', type=int, default=1000,
+  parser.add_argument('-L', '--limit', type=int, default=50,
     help='(max) number of results to query from GitHub')
   parser.add_argument('-X', '--exclusions', default="query-exclusions.txt",
     help='file containing repos to exclude')
@@ -63,25 +68,20 @@ def enrich(repo: dict):
   with open(args.exclusions, 'r') as f:
     for line in f: exclusions.add(line.strip())
 
-  repos = query(args.query)
-  logging.info(f"found {len(repos)} (max {args.query}) notable Lean repositories")
+  repos = query(args.limit)
+  logging.info(f"found {len(repos)} (max {args.limit}) notable Lean repositories")
   repos = filter(lambda repo: repo['fullName'] not in exclusions, repos)
   repos = filter(filter_lake, repos)
-  repos = map(enrich, repos)
-  repos = list(repos)
-  logging.info(f"found {len(repos)} notable Lean repositories with lakefiles")
+  pkgs = map(enrich, repos)
+  pkgs = list(pkgs)
+  logging.info(f"found {len(pkgs)} notable Lean repositories with lakefiles")
 
   data = {
-    "fetchedAt": datetime.utcnow().strftime("%Y-%m-%dT%H:%M:%SZ"),
-    "matrix": repos
+    'fetchedAt': datetime.utcnow().strftime("%Y-%m-%dT%H:%M:%SZ"),
+    'packages': pkgs
   }
   if args.output is None:
     print(json.dumps(data))
   else:
     with open(args.output, 'w') as f:
       f.write(json.dumps(data))
-
-
-
-
-
diff --git a/site/components/BuildOutcome.vue b/site/components/BuildOutcome.vue
@@ -4,11 +4,11 @@ import FailIcon from '~icons/mdi/close'
 import PassIcon from '~icons/mdi/check'
 import { Tippy } from 'vue-tippy'
 
-const props = defineProps<{outcome?: string | null}>()
-const outcome = props.outcome
+const props = defineProps<{build?: Build | null}>()
+const build = computed<Partial<Build>>(() => props.build || {});
 
 const outcomeIcon = computed(() => {
-  switch (outcome) {
+  switch (build.value.outcome) {
     case 'success':
       return PassIcon
     case 'failure':
@@ -19,24 +19,38 @@ const outcomeIcon = computed(() => {
 })
 
 const outcomeClass = computed(() => {
-  return 'outcome-' + (outcome || 'none')
+  switch (build.value.outcome) {
+    case 'success':
+      return 'outcome-success'
+    case 'failure':
+      return 'outcome-failure'
+    default:
+      return 'outcome-none'
+  }
 })
 </script>
 
 <template>
-<Tippy class="build-outcome" :class="[outcomeClass]">
-  <component width="66%" height="66%" :is="outcomeIcon"/>
+<Tippy class="build-outcome">
+  <NuxtLink v-if="build.jobId" :to="`https://github.com/leanprover/reservoir/actions/runs/${build.runId}/job/${build.jobId}#step:5:1`">
+    <div class="build-outcome-icon" :class="[outcomeClass]">
+      <component width="66%" height="66%" :is="outcomeIcon"/>
+    </div>
+  </NuxtLink>
+  <div v-else class="build-outcome-icon" :class="[outcomeClass]">
+    <component width="66%" height="66%" :is="outcomeIcon"/>
+  </div>
   <template #content>
     <div class="tooltip">
-      <span v-if="outcome == 'success'">
-        Builds on the latest toolchain
+      <span v-if="build.outcome == 'success'">
+        Builds on {{build.toolchain}}
       </span>
-      <span v-else-if="outcome == 'failure'">
-        Builds on the latest toolchain
+      <span v-else-if="build.outcome == 'failure'">
+        Fails to build on {{build.toolchain}}
       </span>
       <span v-else>
         <span class="line">Build data not currently included on Reservoir. </span>
-        <span class="line">See the repository's CI instead.</span>
+        <span class="line">See the package repository's CI instead.</span>
       </span>
     </div>
   </template>
@@ -45,24 +59,30 @@ const outcomeClass = computed(() => {
 
 <style scoped lang="scss">
 .build-outcome {
-  display: flex;
-  align-items: center;
-  justify-content: center;
-  flex: 0 0 auto;
+  a, .build-outcome-icon {
+    width: 100%;
+    height: 100%;
+  }
 
-  color: var(--outcome-icon-color);
-  border-radius: 50%;
+  .build-outcome-icon {
+    display: flex;
+    align-items: center;
+    justify-content: center;
 
-  &.outcome-success {
-    background-color: var(--success-color);
-  }
+    border-radius: 50%;
+    color: var(--outcome-icon-color);
 
-  &.outcome-failure {
-    background-color: var(--failure-color);
-  }
+    &.outcome-success {
+      background-color: var(--success-color);
+    }
+
+    &.outcome-failure {
+      background-color: var(--failure-color);
+    }
 
-  &.outcome-none {
-    background-color: var(--dark-accent-color);
+    &.outcome-none {
+      background-color: var(--dark-accent-color);
+    }
   }
 }
 </style>
diff --git a/site/components/HighlightCategory.vue b/site/components/HighlightCategory.vue
@@ -2,15 +2,15 @@
 import { Tippy } from 'vue-tippy'
 import ForwardIcon from '~icons/mdi/chevron-right'
 import type { RouteLocationRaw } from 'vue-router'
-const props = defineProps<{title: string, list: any[], to: RouteLocationRaw}>()
+const props = defineProps<{title: string, list: Package[], to: RouteLocationRaw}>()
 </script>
 
 <template>
   <div class="highlight-category">
     <h3 class="title">{{ props.title }}</h3>
     <ol class="short-list">
       <li class="card" v-for="pkg in props.list" :key="pkg.id">
-        <BuildOutcome class="prefix icon" :outcome="pkg.outcome"/>
+        <BuildOutcome class="prefix icon" :build="pkg.builds.find(b => b.toolchain === latestToolchain)"/>
         <Tippy class="text" :on-show="() => { if (!pkg.description) return false }">
           <NuxtLink class="soft-link" :to="`/packages/${pkg.id}`">
             <div class="name">{{ pkg.name }}</div>

diff --git a/site/pages/index.vue b/site/pages/index.vue
@@ -28,7 +28,7 @@ defineOgImage({
         </div>
         <div class="landing-callout">
           <div class="landing-search">
-            <h1 class="label">Lake's package repository</h1>
+            <h1 class="label">Lake's package registry</h1>
             <SearchBar/>
           </div>
         </div>

diff --git a/site/pages/packages/[id].vue b/site/pages/packages/[id].vue
@@ -94,7 +94,7 @@ const { data: readme } = await useFetch<string>(`${baseContentUrl}README.md`)
           <h3>Lean</h3>
           <ul>
             <li>
-              <BuildOutcome class="icon" :outcome="pkg.outcome"/>
+              <BuildOutcome class="icon" :build="pkg.builds.find(b => b.toolchain === latestToolchain)"/>
               {{ latestToolchain.split(':')[1] }}
             </li>
           </ul>

diff --git a/site/pages/packages/index.vue b/site/pages/packages/index.vue
@@ -101,7 +101,7 @@ const resultPage = computed(() => {
             </li>
             <li><a class="hard-link" :href="pkg.url">Repository</a></li>
             <li class="stars"><StarIcon class="prefix icon"/>{{ pkg.stars }}</li>
-            <li><BuildOutcome class="icon" :outcome="pkg.outcome"/></li>
+            <li><BuildOutcome class="icon" :build="pkg.builds.find(b => b.toolchain === latestToolchain)"/></li>
           </ul>
         </li>
       </ol>
@@ -222,11 +222,13 @@ const resultPage = computed(() => {
           margin-top: 1em;
 
           & > li {
+            display: flex;
             margin-right: 0.8em;
 
             &.stars {
               display: flex;
               align-items: center;
+              line-height: 1em;
 
               .icon {
                 color: var(--star-color);

diff --git a/site/utils/manifest.ts b/site/utils/manifest.ts
@@ -1,5 +1,6 @@
 import manifest from '~/manifest.json'
 
-export const packages = manifest.matrix
+export const packages = manifest.packages
 export type Package = typeof packages[number]
-export const latestToolchain = manifest.toolchain
+export type Build = Package['builds'][number]
+export const latestToolchain = manifest.toolchains[0]