Skip to content

Commit c8399d3

Browse files
ci: migrate to upstreaming-dashboard-action (#547)
The previous script relied on a path in the queueboard repo that no longer exists. We migrate to leanprover-community/upstreaming-dashboard-action which uses the new backend to get its data.
1 parent 9ac500b commit c8399d3

File tree

3 files changed

+8
-104
lines changed

3 files changed

+8
-104
lines changed

.github/workflows/push.yml

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,13 @@ jobs:
4747
mk_all-check: true
4848

4949
- name: Upstreaming dashboard
50-
run: python3 scripts/upstreaming_dashboard.py
50+
uses: leanprover-community/upstreaming-dashboard-action@main
51+
with:
52+
website-directory: ./docs
53+
project-name: Carleson
54+
relevant-labels: carleson
55+
include-drafts: true
56+
branch-name: master
5157

5258
- name: Generate the paper PDF and add it to the website
5359
uses: xu-cheng/texlive-action@22c04326a5d855880f9d39bb955138bf11c6df80 # v3

docs/upstreaming.md

Lines changed: 1 addition & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1 @@
1-
# Upstreaming dashboard
2-
3-
## Files ready to upstream
4-
5-
The following files are `sorry`-free and do not depend on any other files, meaning they can be readily PRed to Mathlib.
6-
7-
{% include ready_to_upstream.md %}
8-
9-
## Files easy to unlock
10-
11-
The following files do not depend on any other Carleson file but still contain `sorry`, usually indicating that working on eliminating those sorries might unblock some part of the project.
12-
13-
{% include easy_to_unlock.md %}
1+
{% include _upstreaming_dashboard/dashboard.md %}

scripts/upstreaming_dashboard.py

Lines changed: 0 additions & 90 deletions
This file was deleted.

0 commit comments

Comments
 (0)