Coq 8.15.2 now available on Codewars

Coq 8.15.2 is now available on Codewars, a community-driven platform featuring code challenges (Kata) for learners of all levels and disciplines. This release includes the base compiler, plus versions of selected packages compatible with Coq Platform 2022.04.1:

  • Equations
  • mathcomp-ssreflect

A list of Coq Kata is available through the Kata search page. The original request for Coq 8.15 support can be found at codewars/runner#189, and requests for additional packages compatible with Coq Platform 2022.04.1 can be made through the issue tracker at codewars/runner as per codewars/runner#189 (comment). Additionally, contributions to the Coq container image used by Codewars can be submitted to codewars/coq.

Happy sparring, and to support the Codewars community for authoring quality Coq challenges suitable for both undergraduates and researchers alike, don’t forget to exercise your right to vote on Kata as you complete them :wink:

If I’m not mistaken, what’s available for now is mathcomp-ssreflect, not the full mathcomp.

1 Like

You’re right, thanks for the correction.