lean-3.4.2 tag on github?

Stream: general

[Scott Morrison]

Is there anyway to work out who keeps recreating the lean-3.4.2 tag on github, and asking them to delete their local copy? Or otherwise prevent it being recreated all the time?

[Keeley Hoek]

One slightly crazy idea is to create it, make it empty with like one commit, then protect it, then the person who tries will get errors next time they do

[Keeley Hoek]

Then get rid of it after a while

[Mario Carneiro]

doesn't its mere existence cause problems? If it's pointing to an empty working dir that would probably be even worse

[Mario Carneiro]

Maybe this will help: https://github.com/leanprover-community/mathlib/tags.atom . It's an Atom RSS feed for tags; if we can hook it up to the zulip bot we might be able to figure out the culprit by timing

[Mario Carneiro]

It looks like mathlib already has some bin-1234 type tags, not sure how often they are created

[Mario Carneiro]

they all date from feb 2019

[Scott Morrison]

I tried deleting them last week, and they all got recreated.

[Mario Carneiro]

So mathlib is supposed to have 0 tags then?

[Scott Morrison]

I think so.

[Reid Barton]

It's probably me, I have a lot of mathlib checkouts...