search

leanprover / reservoir

Package registry for Lean/Lake.
https://reservoir.lean-lang.org
Apache License 2.0
16 stars 1 forks source link

indexing projects that are not the root of the repository #13

Open kim-em opened 10 months ago

kim-em commented 10 months ago

Cedar is a great example of a project where the Lean project is in a subdirectory of the main git repository, but we really ought to have on Reservoir!

tydeu commented 10 months ago

Right now, I do not see an feasible way to do this. There are two major problems:

  1. GitHub code search already has a very low limit on search results (and thus using it already is not heavily scalable). Extending the search to any file in a repository would quickly shoot past the limits.
  2. Repositories can easily have multiple lakefiles. Many of these "pacakges" are things we definitely do not want in Reservoir (e.g., examples). It is thus not clear how to perform such a search without picking up a lot of bad results.
kim-em commented 10 months ago

User registration!