Add Coq - Githubissues

DonaldKellett commented 5 years ago

Please complete the following information about the language:

The following are optional, but will help us add the language:

Test Frameworks: None - as discussed in #719 , we probably need to special-case this language such that successful compilation results in an automatic pass
How to install: coq/coq/INSTALL. I'll try to see if there is an easier way in the meantime - I personally installed Coq on my Mac using Homebrew (which does all the hard work for you) so I'm not exactly sure how it's done on Linux
How to compile/run: coqc solution.v to compile the user solution solution.v. AFAIK only 1 file can be compiled at a time so the entire suite (preloaded, solution, test cases) may need 3 separate calls to coqc. There is also coqchk which checks the compiled .v files, e.g. coqchk solution.vo where solution.vo was compiled from coqc solution.v
Any comments: (e.g., what's interesting about this language) Coq is a dedicated proof assistant which is often used in the industry to prove the correctness of certain programs. Its support for theorem proving far surpasses that of Haskell/Idris so including it on Codewars should open up a huge variety of non-trivial (where "trivial" means toy proofs like A + B = B + A) theorem-proving Kata. Also, unlike Idris, Coq always enforces totality so it shouldn't be possible to subvert proofs using escape hatches like believe_me or assert_total.

:+1: reaction might help. Special mentions: @ice1000 , @MarisaKirisame

kazk commented 5 years ago

I wish I can merge issues. This is a duplicate of #90 and #425. #90 is way out of date and #425 contains potentially useful information.

DonaldKellett commented 5 years ago

This is a duplicate of #90 and #425.

I'll close this Issue then and move the provided information to #425 .

codewars / codewars-runner-cli