Skip to content

Add LOC column and min-loc filter to candidates render - #26

Merged
justincasher merged 1 commit into
mainfrom
justin/render-loc-filter
May 9, 2026
Merged

justincasher merged 1 commit into
mainfrom
justin/render-loc-filter

Conversation

@justincasher

Copy link
Copy Markdown
Collaborator

Summary

  • Adds a LOC column (between Lean and Updated, right-aligned) showing total .lean lines under each repo's local clone, excluding .lake/.git/build/lake-packages directories.
  • Adds a --min-loc flag (default 250) that drops rows whose clone has fewer .lean lines than the floor. A cheap preliminary filter for empty stubs, MWEs, bug repros, and "first Lean project" homework templates. Pass --min-loc=0 to disable.
  • Repos without a local clone (LOC unknown) are kept regardless — missing data shouldn't silently drop a package. Effective only when --clones-dir exists; otherwise the filter is a no-op.
  • Re-render result: 959 of 1594 packages displayed (down from 1033 at min-stars=2 only). README is ~165KB, comfortably below the rendering threshold.

Counts every .lean line under each local clone (excluding .lake/.git/
build/lake-packages dirs) and surfaces it as a new LOC column between
Lean and Updated. The render command grows a --min-loc flag (default
250) that drops rows whose clone has fewer .lean lines than the floor
— a cheap preliminary filter for empty stubs, MWEs, bug repros, and
homework templates. Repos without a local clone (LOC unknown) are
kept regardless so missing data doesn't silently drop a package.
@justincasher
justincasher merged commit adeff82 into main May 9, 2026
2 checks passed
@Vilin97
Vilin97 deleted the justin/render-loc-filter branch May 11, 2026 02:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant