The Coq mailing list

[Donald Leung <i.donaldl AT me.com>]

Dear coq-clubbers,

It's been close to a year since Coq support was first added to Codewars and I 
am excited to announce that Coq support is now officially stable! Many thanks 
to all of you who have joined Codewars since my last invitation ( 
https://sympa.inria.fr/sympa/arc/coq-club/2019-06/msg00084.html ), especially 
those who have participated in the Beta Process by completing Coq challenges 
in Beta and leaving your satisfaction + ranking votes on them which was 
extremely crucial in getting them approved. In particular, I would like to 
thank Jason Gross for his exceptional contribution by authoring 3 of his own 
Coq challenges on our platform (2 of which have been since approved) and 
participating in the final re-rankings which enabled Coq support on Codewars 
to finally leave Beta.

For those of you new to Codewars, I hereby invite you to sign up for an 
account: https://www.codewars.com/?language=coq . Codewars is a training 
platform where programmers of all disciplines train on code challenges called 
Kata in order to improve their programming skills. For Coq, we currently 
boast 74 Kata (54 approved, 20 in Beta) spanning topics on discrete 
mathematics, mathematical logic, verified functional algorithms, programming 
language theory and more, so I'm sure you will be able to find Coq challenges 
to your liking whether you are a computer science undergraduate just getting 
started with Coq or a programming language researcher working at one of the 
world's top universities.

For those of you who have joined Codewars since my last invitation, here are 
a few highlights on what has changed since then:

- We now have a lot more Coq challenges (74 at the time of writing) compared 
to a year ago (maybe about a dozen or two?) so rest assured you won't run out 
of challenges to solve anytime soon
- The difficulty rankings for Coq Kata have stabilized since then. 
Previously, it was not that uncommon to encounter a beginner-level challenge 
incorrectly labelled as advanced which made it rather inconvenient for 
solvers to search for challenges suited to their own level of ability. This 
has now been fixed and will not happen again for Coq (see 
Codewars/codewars.com#2001)
- We now have a dedicated test framework for Coq which allows you to specify 
what axioms are (dis)allowed on a per-challenge basis. What's more, the 
testing framework is powerful enough to support code-golfing challenges and 
code extraction

You may learn more about the Coq environment on Codewars through our Wiki 
page: https://github.com/Codewars/codewars.com/wiki/Language-Coq . Feel free 
to drop by our Gitter chat ( https://gitter.im/Codewars/codewars.com/ ) if 
you have any questions about Codewars or would just like to chat with fellow 
Codewarriors.

Happy sparring!

Yours sincerely,
Donald