Skip to content

Commit f1a41b1

Browse files
committed
ci(build_template): produce decls.txt + imports.json artifact via mathlib-ci (#39880)
Adds a post-build step that invokes `dumpReasonableDecls.lean` from mathlib-ci and bundles its two outputs into the existing `import-graph` artifact alongside `import_graph.dot`. ## What lands in the artifact - `decls.txt`: sorted list of "reasonable" declarations from the Lean environment. Includes `to_additive` / `to_dual` / `to_op` autogenerated outputs that the regex-based `declarations_diff.sh` silently misses. - `imports.json`: per-module transitive-import counts computed from `Lean.Environment.importGraph`. Format-compatible with `count-trans-deps.py`. Both files come from a single Lean env load in the post-build step. ## Why this PR has no consumer (yet) This is stage 1 of a multi-PR feature. Subsequent PRs (across both repos) add the consumers: a post-build `decls-diff.yml` workflow that downloads the artifact pair, computes the Lean-aware declarations diff, and patches the `### PR summary` comment with the result. The architecture relies on the master-side artifact being available so PRs can do cross-run downloads; hence the conditional `retention-days` (90 days on master pushes, 7 elsewhere). ## Dependency on mathlib-ci Depends on leanprover-community/mathlib-ci#42, which adds `scripts/pr_summary/dumpReasonableDecls.lean`. The mathlib-ci pin in `.github/actions/get-mathlib-ci/action.yml` is bumped to a commit on that PR's branch so CI here is green during review. Once mathlib-ci#42 lands, the pin will be re-bumped to the merged-master SHA before this PR merges. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
1 parent 93231e1 commit f1a41b1

1 file changed

Lines changed: 24 additions & 5 deletions

File tree

.github/workflows/build_template.yml

Lines changed: 24 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -733,17 +733,36 @@ jobs:
733733
run: |
734734
lake exe graph
735735
736+
- name: Checkout local actions
737+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
738+
with:
739+
ref: ${{ github.workflow_sha }}
740+
fetch-depth: 1
741+
sparse-checkout: .github/actions
742+
path: workflow-actions
743+
744+
- name: Get mathlib-ci
745+
uses: ./workflow-actions/.github/actions/get-mathlib-ci
746+
747+
- name: dump declarations and transitive-import counts
748+
run: |
749+
lake env lean --run "${CI_SCRIPTS_DIR}/pr_summary/dumpReasonableDecls.lean" \
750+
--out decls.txt --imports-out imports.json Mathlib
751+
736752
- name: upload the import graph
737753
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
738754
with:
739755
name: import-graph
740-
path: import_graph.dot
741-
## the default is 90, but we build often, so unless there's a reason
742-
## to care about old copies in the future, just say 7 days for now
743-
retention-days: 7
756+
path: |
757+
import_graph.dot
758+
decls.txt
759+
imports.json
760+
## Master pushes: 90 days, so later PRs forked from these commits
761+
## can consume the dumps from the artifact. Other branches: 7 days.
762+
retention-days: ${{ github.ref == 'refs/heads/master' && '90' || '7' }}
744763

745764
- name: clean up the import graph file
746-
run: rm import_graph.dot
765+
run: rm -f import_graph.dot decls.txt imports.json
747766

748767
- name: check all scripts build successfully
749768
run: |

0 commit comments

Comments
 (0)