Repository navigation
Dedupe candidates by canonical GitHub key - #19
Merged
Merged
Conversation
The previous filter for manual.txt missed entries that differed from their Reservoir counterparts only by a `.lean` suffix or by case, and GitHub URL redirects mean some manual URLs canonicalise to repos already in Reservoir at fetch time. Result: ~80 duplicated rows in the rendered table. Adds canonical_key(owner, name) and package_key(package) in render.py that lowercase and strip `.lean`/`.git` suffixes, deriving the key from the package's source URL rather than its lakefile name (which Reservoir sets independently of the GitHub path). render_table now deduplicates by package_key keeping the first occurrence, so when the CLI puts the Reservoir manifest before the manual list, Reservoir entries win on conflicts and any future overlaps disappear automatically. Also one-shot filters manual.txt with the new helper, removing 10 entries (9 suffix-bug duplicates plus 1 internal duplicate).
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
The rendered candidates table had ~80 duplicate rows where the same GitHub repo appeared once via Reservoir and once via
manual.txt. Two failure modes caused this:.when extracting names from Reservoir source URLs but allowed dots when parsing manual URLs, soargumentcomputer/Blake3andargumentcomputer/Blake3.leanended up as different keys.gh api repos/<old-owner>/<name>returns metadata for the repo's current location, so a manual URL likereaslab/jixiasilently becamefrenzymath/jixiaafter fetch — andfrenzymath/jixiais already in Reservoir.This PR adds canonical keying that handles both cases and dedupes at render time so future drift between Reservoir and
manual.txtresolves itself:canonical_key(owner, name)lowercases and strips.lean/.gitsuffixes.package_key(package)reads fromsources[*].repoUrl/gitUrl(Reservoir'sfullNameis the lakefile name, which can differ from the GitHub path), falling back to splittingfullNameonly when no source URL is present.render_tablenow dedupes bypackage_key, keeping the first occurrence. The CLI passes Reservoir packages before manual ones, so Reservoir always wins on conflicts.manual.txt(9 suffix-bug dupes + 1 internal dup).After this PR the rendered README has 1489 unique packages (down from a 1604-with-duplicates figure on the previous PR).