Skip to content

Add In Pool column to candidates table - #44

Merged
justincasher merged 2 commits into
mainfrom
justin/candidates-in-pool-column
May 10, 2026
Merged

justincasher merged 2 commits into
mainfrom
justin/candidates-in-pool-column

Conversation

@justincasher

@justincasher justincasher commented May 10, 2026 •

Copy link
Copy Markdown
Collaborator

Summary

  • Add a ninth In Pool column to the autogenerated candidates README table that renders ✓ for candidates already imported into lean-pool.
  • Source the merged status from an optional source.github_repo field on entries in LeanPool/projects.yml, joined to the manifest by canonical owner/name key (existing canonical_key / package_key machinery).
  • Wire the projects.yml path through the render CLI behind a new --projects-yml flag (defaults to LeanPool/projects.yml).
  • Re-render candidates/README.md. Every cell is currently blank because no projects.yml entry has a github_repo source yet — future imports flip themselves to ✓ by adding the field.

The existing projects.yml schema check in quality.py already accepts dict sources containing arbitrary extra keys (it requires exactly one of {arxiv, doi, url} to be present), so no schema change was needed.

Adds a ninth column to the autogenerated candidates README table that
shows ✓ for candidates already imported into lean-pool. The merged
status is sourced from the optional `source.github_repo` field on each
entry in `LeanPool/projects.yml`, joined to the candidate manifest by
canonical owner/name key. Wires the path through the `render` CLI
behind a `--projects-yml` flag (defaulting to `LeanPool/projects.yml`)
and re-renders the README with the new column.
@github-actions

Copy link
Copy Markdown
Contributor

LLM review skipped: PR touches no .lean files. Push a Lean change or comment /review after one lands to re-trigger.

@justincasher
justincasher merged commit 032a1dc into main May 10, 2026
3 checks passed
@Vilin97
Vilin97 deleted the justin/candidates-in-pool-column 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