Add upstreaming dashboard generation (#77)

Add a workflow and supporting files to generate a GitHub Page with an
upstreaming dashboard, powered by the queueboard and the
[upstreaming-dashboard-action](https://github.com/leanprover-community/upstreaming-dashboard-action).

Updates README with instructions on how to set this up

Author: marcelolynch

.github/workflows/deploy-pages.yml

@@ -0,0 +1,62 @@
+name: Build and Deploy Pages
+
+on:
+  push:
+    branches:
+      - main
+      - master
+  schedule:
+    - cron: '0 6 * * *'
+  workflow_dispatch:
+
+concurrency:
+  group: github-pages
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  build-pages:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v6
+
+      # See https://github.com/leanprover-community/upstreaming-dashboard-action
+      # for more details on how this action works and its parameters
+      - name: Generate upstream dashboard snippets
+        uses: leanprover-community/upstreaming-dashboard-action@e3ee7dc54fd376f093ef62973d7b04cf7beabad0
+        with:
+          website-directory: website
+          project-name: Project
+          branch-name: ${{ github.event.repository.default_branch }}
+          # include-drafts: false             # Include draft PRs in the dashboard?
+          # relevant-labels: "label1,label2"  # Group PRs by 'relevant' based on these labels
+
+      - name: Configure Pages
+        uses: actions/configure-pages@v5
+
+      - name: Build with Jekyll
+        uses: actions/jekyll-build-pages@v1
+        with:
+          source: website
+          destination: ./_site
+
+      - name: Upload Pages artifact
+        uses: actions/upload-pages-artifact@v4
+        with:
+          path: ./_site
+
+  deploy-pages:
+    runs-on: ubuntu-latest
+    needs: build-pages
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4

README.md

@@ -61,6 +61,11 @@ To set up GitHub Pages for your repository, follow these steps:
 2. In the left sidebar, click on the **Pages** section.
 3. In the **Source** dropdown, select `GitHub Actions`.
 
+The workflow [`deploy-pages.yml`](.github/workflows/deploy-pages.yml) builds the Jekyll site in
+[`website`](website), runs the
+[`upstreaming-dashboard-action`](https://github.com/leanprover-community/upstreaming-dashboard-action),
+and deploys the result to GitHub Pages.
+
 ## Repository Layout
 
 The template repository is organized as follows (listing the main folders and files):
@@ -73,6 +78,8 @@ The template repository is organized as follows (listing the main folders and fi
         and can be manually disabled by clicking on the **Actions** tab, selecting **Build Project**
         in the left sidebar, then clicking the horizontal triple dots (⋯) on the right,
         and choosing **Disable workflow**.
+        - [`deploy-pages.yml`](.github/workflows/deploy-pages.yml) defines the workflow for building
+        and deploying the GitHub Pages site, including generation of the upstreaming dashboard.
         - [`create-release.yml`](.github/workflows/create-release.yml): defines the workflow for creating a new Git tag and GitHub release when the `lean-toolchain` file is updated in the `main` branch. Ensure the following settings are configured under **Settings > Actions > General > Workflow permissions**: "Read and write permissions" and "Allow GitHub Actions to create and approve pull requests".
         - [`update.yml`](.github/workflows/update.yml) is the dependency
         update workflow to be triggered manually by default. [It's not documented yet, but it will be soon.]
@@ -86,6 +93,8 @@ The template repository is organized as follows (listing the main folders and fi
     - [`Example.lean`](Project/Example.lean) is a sample Lean file.
 - [`scripts`](scripts) contains scripts to update Mathlib ensuring that the latest version is
 fetched and integrated into the development environment.
+- [`website`](website) contains the Jekyll files for the GitHub Pages homepage that displays the
+upstreaming dashboard.
 - [`.gitignore`](.gitignore) specifies files and folders to be ignored by Git.
 and environment.
 - [`CODE_OF_CONDUCT.md`](CODE_OF_CONDUCT.md) should contain the code of conduct for the project.

scripts/customize_template.py

@@ -49,11 +49,17 @@ def main(project_name):
     lakefile_toml = 'lakefile.toml'
     project_lean = 'Project.lean'
     build_project_yml = '.github/workflows/build-project.yml'
+    deploy_pages_yml = '.github/workflows/deploy-pages.yml'
     citation_bib = 'CITATION.bib'
+    website_config = 'website/_config.yml'
+    website_index = 'website/index.md'
 
     # Replace 'Project' with the actual project name in the necessary files
     replace_text_in_file(lakefile_toml, 'Project', project_name)
     replace_text_in_file(build_project_yml, 'Project', project_name)
+    replace_text_in_file(deploy_pages_yml, 'Project', project_name)
+    replace_text_in_file(website_config, 'Project', project_name)
+    replace_text_in_file(website_index, 'Project', project_name)
 
     # Rename 'Project' folder to match the project name
     rename_directory(project_folder, project_name)

website/_config.yml

@@ -0,0 +1,4 @@
+title: Project
+description: Upstreaming dashboard for Project
+theme: minima
+markdown: kramdown

website/index.md

@@ -0,0 +1,16 @@
+---
+layout: default
+title: Upstreaming Dashboard
+---
+
+<header class="page-header">
+  <h1>{{ site.title }}</h1>
+</header>
+
+This project will typically want to contribute some files into `Mathlib` itself. These files, which we can call 'upstreaming candidates', exist in this repository while they are being developed. This dashboard shows upstreaming candidates that look ready to ingest into `Mathlib`, and also files in the project that look "easy to unlock" for upstreaming.
+
+For the dashboard to be correct, the repository must follow the same directory and filename structure as Mathlib for their upstreaming candidates. Namely, the upstream candidate `A/B/C.lean`, should exist in `Mathlib/A/B/C.lean`.
+
+The dashboard highlights any open PRs to the Mathlib repository containing the corresponding files.
+
+{% include _upstreaming_dashboard/dashboard.md %}