Should be fixed now, I've inserted the relevant calls to idtac "<PASSED::>" and idtac "<FAILED::>". I don't think it's necessary to open an issue there, as this is a rather esoteric kata with correspondingly esoteric methods of testing.

I'm a bit confused why I need to use Print Assumptions or https://github.com/codewars/coq_codewars ; if the test file runs to completion without throwing errors, then this should be considered succeeding. I can add Print Assumptions I at the bottom just to conform to the way things are set up, but that seems silly, and https://github.com/codewars/coq_codewars isn't flexible enough to do the kind of check needed for this kata. Is there a way to get the right output for the test runner to accept things using idtac?

Yes, this is part of the semantics of Qed.

.

Okay, this time it worked, though I could have sworn I had done that last time.

How do I enable Coq 8.11? If I try to republish after changing the dropdown to 8.11.0, I get "Default Version is not a supported version". (Maybe it's the wrong dropdown that I changed?)

I believe the solutions contributed by others should still work in 8.11. If you don't use axioms and you close your proofs with Defined rather than Qed, the proof you give of trans_12 should work fine. You can inspect what's blocking reflexivity by first running compute after destruct; what do you see if you do that?

This is not a valid solution, and the fact that it is here is a bug in the tests. This function incorrectly returns True on 341 (11*31), and more generally on pseudoprimes

Indeed, thanks for pointing this out. Now fixed.

Indeed, thanks for catching this! I've added tests to forbid this by enforcing that all three reduce on eq_refl

Check eq_refl : Solution.trans1 _ _ _ _ eq_refl eq_refl = eq_refl.
Check eq_refl : Solution.trans2 _ _ _ _ eq_refl eq_refl = eq_refl.
Check eq_refl : Solution.trans3 _ _ _ _ eq_refl eq_refl = eq_refl.

Indeed, thanks, now fixed