Adding support for unit testing?

[Mallku2]

For writing unit tests I am aware of at least 2 different approaches:

(declare-const test1 (eo::requires left_hand_side_of_test1 right_hand_side_of_test1 whatever_return_value1))
...
(declare-const testn (eo::requires left_hand_side_of_testn right_hand_side_of_testn whatever_return_valuen))

and

(declare-rule test ()
  :requires ((left_hand_side_of_test1 right_hand_side_of_test1)
              ...
             (left_hand_side_of_testn right_hand_side_of_testn))

  :conclusion whatever_value)

(step test_step whatever_value :rule test)

The first approach requires for you to provide a name for each test, and to indicate some artificial return value. The second approach allows you to define a bunch of related tests faster (you just define left hand-side and right hand-side of each test), grouped together under the same name. But you also need to add some artificial step command, just to trigger testing. In both approaches, we are also including extra information that is not directly related with the tests.

Would it be possible to add direct support for unit-testing into Eunoia?, such that we are not required to find ways to codify them in terms of other concepts, which forces us to include extra information not directly related with testing.

[hansjoergschurr]

It seems I wrote a comment, but never posted it. We had a chance to discuss this during a meeting.

In general, I am of the opinion that we should avoid adding a new feature for this to Ethos, but we might want to invest in building an external test runner that understands a standard form of tests and can generate nice reports.

I tend to prefer the second format, because this would allow for parameterized tests by using :args for :step.

Thinking about it now, I realize that we actually might want to have tests that use step as part of the test (e.g. to test rules with some premises).
Maybe we could have a test runner that accepts two more commands expect-success and expect-failure and the test runner translates these into appropriate step commands.

[Mallku2]

In general, I am of the opinion that we should avoid adding a new feature for this to Ethos, but we might want to invest in building an external test runner that understands a standard form of tests and can generate nice reports.

I agree with this but, maybe, this should be presented as a feature that is also part of Eunoia itself, and maybe Ethos could just call the external test runner, when invoked to do so? I think that having out of the box support for unit testing is important.

Maybe we could have a test runner that accepts two more commands expect-success and expect-failure and the test runner translates these into appropriate step commands.

I like this!