The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Just checking with regard to the IDE. Are you aware of jscoq, a
webinterface for Coq:
https://github.com/ejgallego/jscoq

On Fri, Jun 28, 2019 at 4:11 PM Donald Leung 
<i.donaldl AT me.com>
 wrote:
>
> @Agnishom: Many thanks for your feedback and links to similar websites 
> hosting recreational theorem-proving challenges. Unfortunately, since the 
> Codewars platform was designed to support a wide variety of programming 
> languages, the maintainers decided that it was impractical to support 
> Coq-specific IDE features such as interactively stepping through a proof 
> script. The current recommended way of solving a Coq challenge on Codewars 
> is to simply copy the provided template into an IDE of your choice such as 
> CoqIDE or Proof General and develop your solution locally. The preloaded 
> code is often displayed within the Kata description itself so you may wish 
> to copy those code snippets into your local environment as well in a 
> separate file “Preloaded.v”.
>
> @Vincent: The “omega” tactic (as is the rest of the Coq standard library 
> plus a few external libraries) is available on Codewars - you can use it in 
> your solution by adding “From Coq Require Import omega.Omega” to the top of 
> your solution file.
>
> More information about the Coq environment on Codewars can be found at 
> https://github.com/Codewars/codewars.com/wiki/Language-Coq
>
> Cheers,
> Donald