repo is not indexed

[Seasawher]

repo https://github.com/lean-ja/lean-by-example has not been indexed by Reservoir

I think this repo satisfies the inclusion criteria https://reservoir.lean-lang.org/inclusion-criteria.

[tydeu]

@Seasawher I have now figured out the problem. Lean by example is a repository generated from a template. GitHub treats categorizes thus repositories as forks from the perspective of repository / code search. Reservoir does not include forks in its indexing (and cannot, as this would produce to many results), thus it does not pick up Lean by example.

It is probably worth clarifying this in the inclusion criteria.

[Seasawher]

Thank you. In the future, will there be a feature that allows a repository to be indexed by Reservoir even if it is a fork?

[tydeu]

@Seasawher Yes, probably. It will likely be part of a manual package registration process that will also solve #13.

[Seasawher]

Thanks!

[Seasawher]

@tydeu

why this repo is included? This is also generated from template.
https://reservoir.lean-lang.org/@Joonas-vonlerber/Game

[tydeu]

@Seasawher I am not sure. 😕 When searching repositories the way Riposte does manually, it does not appear in the search, but it apparently appeared once and got indexed then. I am not sure what caused to appear in the search at the time and not now. As a generated repository, it theoretically should not have appeared in the search according to GitHub's apparent rules. Maybe its owner created it as a normal repository first and then recreated as a generated one and that is why it got indexed? Alternatively maybe there is some race condition in GitHub were the search saw it as normal repository before it got recorded as fork? I sadly have no clue. 😞

[Seasawher]

Could the following repositories be added to Reservoir?

• https://github.com/lean-ja/lean-by-example
• https://github.com/lean-ja/lean99

[tydeu]

@Seasawher Sorry for the late reply! I would be happy to do this; however, I do not currently have a process for manually adding repositories to the Reservoir index, so this will have until I have the time to do so.