No results found

Inclusion Criteria

Reservoir automatically indexes Lean repositories on GitHub. To be included in its selection, a package must meet a few criteria:

  • Public GitHub source repository. Reservoir does not index forks or private repositories. Repositories generated from a template are considered forks.
  • A root lake-manifest.json. There mut be a file named exactly lake-manifest.json in the top-level directory of the repository. Prior to April 2024, Reservoir required a root lakefile.lean instead.
  • GitHub-recognized OSI-approved license. GitHub displays the license it detects for a repository on the code page in either the right-hand column (desktop) or in the top matter (mobile). That license must then be listed as OSI-approved in the SPDX License List.
  • At least 2 stars. The repository must have at least 2 stars on GitHub. This serves as a very basic quality filter.

Reservoir updates its index approximately daily. If your package meets the above conditions, but does not appear on Reservoir after a few days, you can report this as a bug on Reservoir's issue tracker.