How to tag a repository

Stream: lean4

[Patrick Massot]

Today in the FRO meeting, Leo mentioned tracking the number of GitHub repositories using Lean 4, and the FRO meeting has a link to https://github.com/topics/lean4. I think we should tell people how to make sure their repository appears on this list, since this is not automatic. Until 5 minutes ago I assumed this was based on GitHub automatic language detection feature, but it isn't.

[Heather Macbeth]

Indeed, how do you do this?

[Mauricio Collares]

Add the lean4 topic to the repo following the instructions at https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/classifying-your-repository-with-topics#adding-topics-to-your-repository

[Patrick Massot]

I think the relevant area of the GitHub interface is:
image.png

[Patrick Massot]

But knowing this is not enough, we need to know what is the relevant topic. If I understand correctly, it is lean4.

[Eric Wieser]

Or should we instead be tracking https://github.com/search?q=+language%3ALean&type=repositories, which does use that automatic language support?

[Patrick Massot]

I thought this was what was used. I guess the big issue is that it doesn't distinguish between Lean 3 and Lean 4.

[Eric Wieser]

I am in the process of making a PR to fix that

[Heather Macbeth]

Also note that repos can be relevant to Lean without Github identifying the language to be Lean: there are 5 repos like this on the first page of
https://github.com/topics/lean4
(respectively TypeScript, Lua, JavaScript, Python, HTML)

[Patrick Massot]

I think Leo explicitly want to track Lean packages, although the broader question is also interesting.

[Eric Wieser]

Eric Wieser said:

I am in the process of making a PR to fix that

Gitpod is not co-operating so I'm shelving it for now, but https://github.com/github-linguist/linguist/pull/6616 is that PR

[Eric Wieser]

Regarding the topic page, do we know who can fix the highlighted link on the right below to point to Lean 4?

image.png

[Utensil Song]

The description also could use some improvements, it seems to come from https://github.com/leanprover/lean4/blob/master/doc/whatIsLean.md . And the link to the wikipedia is about Lean 3.

[Scott Morrison]

I've also found

gh search code --filename lean-toolchain -L 1000 "leanprover/lean4:v4.2.0"

useful, to lookup all repos using Lean at some version.

[Utensil Song]

Eric Wieser said:

Regarding the topic page, do we know who can fix the highlighted link on the right below to point to Lean 4?

image.png

GTP-4:

As of my last update, GitHub does not allow regular users to directly change the descriptions of topics that appear on repository topic pages.

Topic descriptions are curated by GitHub and are typically sourced from reputable places that are related to the topic, such as official documentation or Wikipedia. If you believe a topic description is inaccurate or could be improved, you might consider reaching out to GitHub support or suggesting an edit through the GitHub community forums.

But at least, the wiki page is open to edits.

[Scott Morrison]

If anyone is interested in the "spectrum" of versions out there:

#!/bin/bash
# Must be run in a copy of the `lean4` repository, and you'll need to login with `gh auth` first.
for v in $(gh release list | cut -f1) nightly stable
do
  sleep 10 # Don't exceed API rate limits!
  echo -n $v
  gh search code --filename lean-toolchain -L 1000 "leanprover/lean4:$v" | wc -l
done | awk '{ printf "%-12s %s\n", $1, $2 }'

printed (two weeks ago):

v4.3.0-rc1   21
v4.2.0       66
v4.2.0-rc4   34
v4.2.0-rc3   6
v4.2.0-rc2   0
v4.2.0-rc1   22
v4.1.0       21
v4.1.0-rc1   5
v4.0.0       40
v4.0.0-rc5   0
v4.0.0-rc4   6
v4.0.0-rc3   0
v4.0.0-rc2   7
v4.0.0-rc1   0
v4.0.0-m5    0
v4.0.0-m4    0
v4.0.0-m3    0
v4.0.0-m2    0
v4.0.0-m1    0
nightly      279
stable       9

[Eric Wieser]

Eric Wieser said:

Or should we instead be tracking https://github.com/search?q=+language%3ALean&type=repositories, which does use that automatic language support?

Patrick Massot said:

I thought this was what was used. I guess the big issue is that it doesn't distinguish between Lean 3 and Lean 4.

Just to note that the vote in another thread was that we specifically did not want GitHub to make this distinction visible, so the result is that GitHub knows the difference for syntax highlighting purposes but not when computing language statistics.

[Utensil Song]

Context: topic PR