CWGroup fails to form nested test groups about coq_codewars HOT 13 CLOSED

I made the following changes:

• Added a new command CWTestCase. This command outputs <IT::>.

• Added a new command CWEnd for finishing test cases. This command is optional because CWEndGroup automatically finishes test cases (and also finishes a group) and CWTestCase finishes previous test cases also.

• Added a new command CWAssert. This is an alias of CWTest. I want to rename the existing command CWTest to CWAssert. But I cannot do it right now without breaking existing kata. So it is a temporary solution: after this update is deployed I would like to replace CWTest in all existing kata (5 kata which use the plugin) to CWAssert. Then I also want to rename CWTestCase to CWTest.

• I also implemented another form of the CWAssert command for type checking.

Example: cw_example/test.v.

@kazk: Please test the updated plugin (specifically, check the output formatting of cw_example/test.v).

The question to everyone: what do you think about command names?

from coq_codewars.

Deployed

from coq_codewars.

I didn't really think of nested groups when I suggested adding it (and apparently monadius also took it lightly and just made it <DESCRIBE::>). The behavior on describe -> describe -> assertion is indeed undocumented, so probably we should add e.g. CWSubgroup to output <IT::>.

from coq_codewars.

The formatting looks good. The example files are renamed.

from coq_codewars.

I decided to follow @DonaldKellett's suggestion and renamed some commands. I made the following changes: CWTest -> CWAssert, CWTestCase -> CWTest, CWEnd -> CWEndTest. When the updated plugin is deployed some kata will be broken but it will not take a long time to fix them. I don't think it will cause any problems.

@DonaldKellett: here is an example of test code for your Mergesort kata:

Require Solution.
Require Import Preloaded FunctionalExtensionality.
From CW Require Import Loader.

CWGroup "Solution.mergesort_correct".
  CWTest "should have the correct type".
    CWAssert Solution.mergesort_correct : (is_a_sorting_algorithm mergesort).
  CWTest "should not assume any axioms other than (dependent) functional extensionality".
    CWAssert Solution.mergesort_correct Assumes functional_extensionality_dep.
CWEndGroup.

from coq_codewars.

Do I understand correctly that it is enough to output <IT::> for nested groups? I am working on it now. I do not plan to introduce new commands: CWGroup will automatically output <IT::> for nested groups. I also want to add time in milliseconds after <COMPLETEDIN::>.

from coq_codewars.

<DESCRIBE::> is for a group and <IT::> is for a test case.

If <PASSED::>/<FAILED::> is inside <IT::>, nested <DESCRIBE::> should work.

from coq_codewars.

describe -> assertion is already hack so I'd prefer each assertion result (or a set of assertion results) to be inside <IT::>.

from coq_codewars.

Is it better to have separate commands for <DESCRIBE::> and <IT::>? Something like CWDescribe (replacing CWGroup) and CWIt? Is it OK to output <IT::> without previous <DESCRIBE::>?

from coq_codewars.

Yeah, it's ok to have a top level <IT::>. Some test frameworks doesn't have <DESCRIBE::>. But we can't have nested <IT::>

• describe -> it -> assertion_result Good
• describe -> describe -> it -> assertion_result Good
• describe -> assertion_result OK (I think this is mainly for Codewars test frameworks that doesn't really care about the test structure)
• it -> assertion_result OK
• assertion_result OK
• describe -> describe -> assertion_result don't work
• it -> it -> assertion_result not allowed

For naming, I think CWGroup is better. I'm not sure what to name <IT::> though (CWTest, CWCase, something like that and fits in Coq better). Words like "describe" and "it" are from BDD style test framework.

from coq_codewars.

cw_example/test.v should look like

Can you change the file names of the example to Preloaded.v, Solution.v, SolutionTest.v? I had to edit test.v to make it run because of the module name difference.

from coq_codewars.

5 kata which use the plugin

Probably 15 or so since I updated all my previously authored Coq Kata (13 in total) to use CW.Loader. Renaming CWTest to CWAssert and such should be an easy fix though so I don't mind if the breaking changes are introduced straight away; just give me a heads-up when they are deployed so I can fix my Kata right away 👍

from coq_codewars.

I'll try deploying this later tonight if I have the time or tomorrow. I'll close this issue when I do.

from coq_codewars.