Reservoir

xubaiw/Reservoir.lean

WIP unofficial package registry of Lean 4

GitHub Link Documentation

Pick a version!

TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.

README

Reservoir.lean

WIP unofficial package registry of Lean 4.

Index

The default index of Reservoir is reservoir-index, and a rendered version is served on GitHub Pages.

Implementation

This is based on the GitHub Search API:

" \ --location "https://api.github.com/search/code?q=Lake&language:Lean" \ --header "Accept: application/vnd.github.v3+json" ">

curl -s \
  -H "Authorization: token " \
  --location "https://api.github.com/search/code?q=Lake&language:Lean" \
  --header "Accept: application/vnd.github.v3+json"

Since SSL utilities for Lean 4 are not yet finished, this package requires the existence of commandline curl.