From 58e04ab6928e0557fe2ecfd69f96edc6a577fa77 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 21 Jun 2024 22:17:38 +0200
Subject: [PATCH] README

---
 .github/workflows/update-index.yml |  2 +-
 README.md                          | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 README.md

diff --git a/.github/workflows/update-index.yml b/.github/workflows/update-index.yml
index a1ec50b..f0ae46f 100644
--- a/.github/workflows/update-index.yml
+++ b/.github/workflows/update-index.yml
@@ -26,7 +26,7 @@ jobs:
           gh api --paginate repos/leanprover/lean4/releases > releases
           gh api --paginate repos/leanprover/lean4-nightly/releases > releases-nightly
           mkdir output
-          # version 1, all in one file. still needed?
+          # version 1, all in one file.
           jq --compact-output --slurp '
             def preprocess: map(pick(.name, .created_at, (.assets | .[] | .name, .browser_download_url)));
             {version: "1", stable: .[0] | map(select(.prerelease | not)) | preprocess, beta: .[0] | map(select(.prerelease)) | preprocess, nightly: .[1] | preprocess}' \
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..816e025
--- /dev/null
+++ b/README.md
@@ -0,0 +1,18 @@
+Lean repository index
+=====================
+
+This repository fills <https://release.lean-lang.org/> with JSON files listing
+the lean releases.
+
+It is updated upon new Lean releases (stable, beta, nightly; but not PR
+releases) using a GitHub Actions `workflow_dispatch` event. If it stopped working maybe the PAT expired? Then create a new one and set a secret on the lean4 repo.
+
+URLs:
+
+* <https://release.lean-lang.org/> lists all releases, grouped by release channel.
+* <https://release.lean-lang.org/stable.json> lists all stable releases.
+* <https://release.lean-lang.org/beta.jon> lists all beta releases.
+* <https://release.lean-lang.org/nightly.jon> lists all nightly releases.
+
+Since there are many nightly releases (about one every night), the
+`stable.json` is noticably smaller and should be used if it suffices.