Repository navigation
Filter candidates table by classifier decisions - #29
Merged
Merged
Conversation
justincasher
force-pushed
the
justin/render-decisions-filter
branch
from
May 10, 2026 03:47
b6a1f28 to
f5995c3
Compare
justincasher
added a commit
that referenced
this pull request
May 10, 2026
Both comment steps run before actions/checkout so the working dir has no .git, and `gh pr comment` shells out to git to detect the repo. Already exposed by PR #29: the Wait-for-Lean-CI step timed out, the 'not green' comment ran without checkout, and gh aborted with 'fatal: not a git repository'. Pass -R "$REPO" on both comment calls to use the API path that does not need git.
Adds aggregator/candidates/decisions.jsonl (953 verdicts produced by
running the inclusion criteria over every cloned repo with >=2 stars
and >=250 .lean LOC) plus the CRITERIA.txt the classifier follows.
Each line is {repo, include, category, confidence, rationale}.
The render command grows a --decisions flag (default points at the
new file). When loaded, rows whose canonical key has include=false
are dropped from the markdown table; repos with no verdict are kept
so a partial run never silently loses a package. Re-render shrinks
the table from 959 to 498 rows (491 included + 7 unclassified).
justincasher
force-pushed
the
justin/render-decisions-filter
branch
from
May 10, 2026 04:02
f5995c3 to
8187a55
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
aggregator/candidates/CRITERIA.txt(the inclusion policy) andaggregator/candidates/decisions.jsonl(953 per-repo verdicts: 491 include / 462 exclude). Verdicts were produced by running the criteria over every cloned repo that passed the existing--min-stars=2 --min-loc=250filters.decisions.jsonlis{repo, include, category, confidence, rationale}. Categories:mathlib | cslib | physlean | multifor includes;tool | educational | personal | translation | fork | empty | scaffoldfor excludes.--decisionsflag toaggregator render(defaults to the new file). When loaded, rows whose canonical key hasinclude=falseare dropped from the markdown table. Repos with no verdict are kept so a partial run can't silently lose a package.Numbers from the run
Top categories:
mathlib 299,tool 249,cslib 161,educational 129.