Re-rankings for Agda Kata?

[DonaldKellett]

So now that the Coq re-rankings are complete, I noticed that my Agda rank progress is greater than that for Coq, which is BS because I've been exclusively solving and authoring theorem-proving Kata in Coq ever since it was added to Codewars and only briefly played around with Agda before that.

Now, I do not know exactly how many Agda Kata are considered over-ranked and to what extent considering how different Agda is from Coq (do they even have automation?), but I think that many will agree that at least some of the earlier approved Agda Kata could benefit from a re-ranking (and perhaps Idris as well, but no one does Idris anyway :trollface: ).

Take List concatenation is injective? Prove it!, for example, which is currently ranked at 1 kyu. I do not claim to know exactly what rank is suitable for this particular Kata, but after having done an experiment in Coq by trying to prove it from first principles without any help from the standard library and/or automation tactics (in order to establish an upper bound on its difficulty), I am convinced that it cannot deserve any more than 5 kyu. Granted, it's not the most straightforward Kata for a beginner and proving one of the lemmas relating to the main theorem is rather tricky, but there aren't any particularly difficult concepts involved either and it probably dwarfs in comparison, to say, Kata on the univalence axiom and cubical type theory.

Ultimately, the extent to which Agda Kata are re-ranked (or whether to re-rank them at all) is up to the Agda community to decide (which I am not a part of), but IMHO Agda should not be considered as a candidate for leaving Beta, at least until a suitable re-ranking has taken place.

┆Issue is synchronized with this Clickup by Unito

[DonaldKellett]

I went ahead and created a Kata QA page for Agda Kata that require rank adjustment based on the few Agda Kata that I have completed back when Coq was not supported on Codewars. This list is by no means exhaustive - feel free to add other Agda Kata to the table which you think is overranked but not yet listed.

Once these re-rankings are complete, I believe that Agda should be stable enough to leave Beta since we have used the current Agda setup for over a year and haven't encountered any major issues AFAIK.

Special mentions: @ice1000, @monadius, @Bubbler-4, @Voileexperiments

---

P.S. We should probably re-rank some Idris Kata as well, but I doubt that Idris is ready to leave Beta anytime soon either way considering how little attention it got after proper theorem-proving languages were supported on Codewars, so ... 🤷‍♂️

[ice1000]

I agree with your rankings

[DonaldKellett]

Thanks @ice1000 , I have duplicated my suggested rankings to your column on the table as per your comment.

[DonaldKellett]

@kazk : monadius, ice1000 and I have cast our new ranking votes for overranked Agda Kata on the Kata QA page. Should we proceed to unapprove some of them for re-ranking?

[kazk]

Unapproved the first two.

[kazk]

@DonaldKellett Can you stop taking advantage of the bug to set the rank? I commented on the kata not to do it and reverted multiple times.

I hope you just missed my comment and didn't mean to ignore me. I'll revoke your privilege if you continue.

[DonaldKellett]

@kazk Whoops, sorry about that, you have my word that I will not take advantage of the bug again.

[Voileexperiments]

Can we just remove the restrictions of the available ranks based on average ranking votes/estimated rank instead? It's not really doing anything except arbitrarily blocking approver from making reasonable rank when the existing votes are biased.

I think I've raised this issue somewhere else a long time before too.

[DonaldKellett]

Can we just remove the restrictions of the available ranks based on average ranking votes/estimated rank instead? It's not really doing anything except arbitrarily blocking approver from making reasonable rank when the existing votes are biased.

I second this. Moderators found to repeatedly abuse the approved ranking can be reported and have their privileges revoked anyway.

[DonaldKellett]

@kazk The first two have been (properly) re-ranked to 7 kyu.

[kazk]

Unapproved the rest except for the last one.

I agree that the rank restriction is not doing much at the moment. But I think that's because no one knows how to assess ranks. Removing the restriction will create a different problem by allowing single biased approver approve with whatever rank they think is right ignoring others.

[DonaldKellett]

Removing the restriction will create a different problem by allowing single biased approver approve with whatever rank they think is right ignoring others.

AFAIK the current rank restriction mainly prevents under-ranking but allows over-ranking of up to 3 Kyu levels? IMHO even if the rank restriction isn't lifted, it should be modified to allow approving at the average assessed rank(s) plus or minus 1 Kyu level (or 2) to strike a better balance.

[kazk]

I looked at the code and it's little bit more than I thought.

The allowed range is [a, b] (inclusive) where

• a = min(avg, avg_power_user, estimated)
• b = max(avg, avg_power_user, estimated) + 2

I didn't know (haven't spent much time around this area) that the estimate was included.

And I just found out that "power user" in this context is users with at least 500 (!) honor points. Almost everyone assessing rank is "power user" (only [100, 500) are not) and avg is the average of all assessments, so it's pointless. The number is hardcoded and looks like it wasn't updated over time.

Maybe just do the average +/- 2? Reduces the option from 8 to 5 or less depending on the average.

Changing the rule will cause #2112 for all approved kata with ranks out of the new allowed range so I'll need to fix that first.

[kazk]

So I guess you guys can re-rank more easily by adjusting the estimated rank to the target rank. That should make that rank available and won't cause #2112 at least for now.

[DonaldKellett]

Maybe just do the average +/- 2?

Sounds good to me :+1:

So I guess you guys can re-rank more easily by adjusting the estimated rank to the target rank. That should make that rank available and won't cause #2112 at least for now.

Thanks for the tip, that should make it easier to re-rank @ice1000 's kata at least.

[DonaldKellett]

@kazk The 4 Agda Kata previously unapproved have just been re-ranked (but at 1 rank above the agreed average, since it was infeasible to push it down any further), would you mind unapproving the final one (Typeclass is garbage)?

@ice1000 For "Typeclass is garbage", do you agree with @monadius 's 6 kyu rank assessment?

[kazk]

Done

[ice1000]

@DonaldKellett Yes I do.

[DonaldKellett]

@kazk "Typeclass is garbage" has been re-ranked, albeit at one kyu level above the agreed average since it is likely infeasible to push the rank down any further. Now that the Agda rankings have mostly stabilized, should we move Agda out of Beta once and for all? :wink:

[monadius]

I am going to add Cubical Agda kata to the table when I have time.