-
Notifications
You must be signed in to change notification settings - Fork 219
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Re-rankings for Agda Kata? #2030
Comments
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 ... 🤷♂️ |
I agree with your rankings |
Thanks @ice1000 , I have duplicated my suggested rankings to your column on the table as per your comment. |
@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? |
Unapproved the first two. |
This comment has been minimized.
This comment has been minimized.
@kazk Whoops, sorry about that, you have my word that I will not take advantage of the bug again. |
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. |
I second this. Moderators found to repeatedly abuse the approved ranking can be reported and have their privileges revoked anyway. |
@kazk The first two have been (properly) re-ranked to |
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. |
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. |
I looked at the code and it's little bit more than I thought. The allowed range is
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 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. |
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. |
Sounds good to me 👍
Thanks for the tip, that should make it easier to re-rank @ice1000 's kata at least. |
@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 |
Done |
@DonaldKellett Yes I do. |
@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? 😉 |
I am going to add Cubical Agda kata to the table when I have time. |
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
).
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 than5 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
The text was updated successfully, but these errors were encountered: