Repository navigation
Add manual candidate list for repos Reservoir does not index - #16
Merged
Merged
Conversation
Reservoir's inclusion criteria (https://reservoir.lean-lang.org/inclusion-criteria) exclude packages that are forks, lack a root lake-manifest.json, have a non-OSI license, or have fewer than two stars. We verified that 11 real, completed Lean formalisation projects in our backlog fail one of those rules and so will never be auto-indexed. Adds aggregator/candidates/manual.txt for hand-curating GitHub URLs to track alongside Reservoir's index. The fetch CLI reads it and queries the GitHub REST API for each entry, saving the results to raw_data/manual_packages.json (gitignored). The render CLI loads both manifests and concatenates them before producing the README table. Manual entries render with a "–" build glyph because we have no toolchain build data for them.
manual.txt grows from the original 11-repo seed to 987 entries (filtered against Reservoir's 617-package index so nothing is duplicated). The fetcher now caches each successful GitHub response to raw_data/manual_cache/<owner>__<name>.json so partial progress survives rate-limit pauses and process interruptions; on re-run cached entries skip the API call. The bulk fetcher also logs and skips failures (rate limits, deleted repos) instead of aborting. Rendered README now contains 1604 packages (617 reservoir + 987 manual).
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
Reservoir's inclusion criteria exclude packages that are forks, lack a root
lake-manifest.json, have a non-OSI license, or have fewer than two stars. Many real Lean projects fail one of those rules and will never be auto-indexed.This adds a hand-curated escape hatch and seeds it with 987 entries (filtered against Reservoir's 617-package index so nothing is duplicated):
aggregator/candidates/manual.txt— committed list of GitHub URLs, one per line,#comments allowed.aggregator.manualmodule — parses the URL list, queriesgh api repos/<owner>/<name>for each entry, builds Reservoir-shaped package dicts.raw_data/manual_cache/<owner>__<name>.jsonimmediately, so partial progress survives rate-limit pauses or process interruptions. Re-runs skip cached entries.fetchCLI extended to also writeraw_data/manual_packages.json(gitignored) alongside the Reservoir manifest.renderCLI extended to concatenate both lists before generating the table.After this PR the rendered README contains 1604 packages (617 Reservoir + 987 manual). Manual entries render with a
–build glyph because we have no toolchain build data for them.Future considerations
gh apicall requiresghto be authenticated locally when runningfetch. CI integration would need a different auth path.manual.txtkeeps growing.decisions.jsonlwill join with both data sources at render time.