Unit testing

[vzaliva]

We need to figure out how unit tests will work. It looks like we will have 2 types of exercises:

1. Proofs. For this type of exercise, the unit test is a compilation. Once it compiles we are good to go.
2. Functional programs. For these, we may have actual unit tests. They could be executed either using Compute or simple reflection-based proofs asserting results.

I've added an example exercise for each:

1. https://github.com/exercism/xcoq/tree/master/exercises/tautology (track-specific)
2. https://github.com/exercism/xcoq/tree/master/exercises/rna-transcription (based on x-common)

Please try to set up unit testing for these.

[bagnalla]

Hi, I just discovered Exercism and I'm interested in contributing to the Coq track.

Is it really necessary to make such a distinction between proofs and programs? After all, Coq has its foundation in the fact that "proofs ARE programs". It also seems natural that exercises may want to combine the two (e.g., the user must provide a functional program along with an accompanying proof about its behavior).

Here's one potential way to do the unit tests. We ask the user to fill in the functions and/or proofs for the problem. In the test file, we use simple assertions for regular test cases, and also check that all of the proofs have been completed. Unfinished proofs can get past the typechecker if they are admitted, so we use "Print Assumptions" command to print out any admitted proofs.

Here's a little example of what I mean.
exercise file: https://pastebin.com/5K0mPput
test file: https://pastebin.com/EvdmdchR

Both files could probably be generated automatically from some specification of the problem.

[vzaliva]

I agree that exercise can contain both proofs and programs.
I like your idea about "Print Assumptions" for checking for admitted proofs.

[bagnalla]

Here's a possible Coq exercise for the leap year problem in that style.

leap.v https://pastebin.com/EYcTc3JS
leap_example.v https://pastebin.com/gDNa1tRz (not necessarily the best style but it could be much worse)
tests.v https://pastebin.com/xJUi4GZi

One issue with Coq is that exercises have the potential to be many times more difficult/time-consuming than equivalent exercises in other languages. We could simply port the exercises directly (which I suppose is the normal thing to do) but then we would be missing out on the interesting part of Coq - actually proving the correctness rather than simply passing a few test cases. I think it would be a real shame to omit the theorem-proving side of Coq, and would render the track essentially pointless IMO.

So, it seems natural to just include a lemma or two to be proven in addition to passing the regular test cases. But even then, it's not always clear what those lemmas should be. Even in the leap year problem, which is quite straightforward, there are many different things of varying difficulty that could be proven. Perhaps small and simple proofs should be favored (maybe even smaller than the one in the example above).

Alternatively, I guess the proof bits could be split out into separate exercises, but it seems that language-specific exercises aren't really a thing on Exercism from what I can tell.

I wouldn't mind putting a few exercises together but I can't really proceed until this stuff is decided.

[vzaliva]

Unfortunately, when I initiated this track I did not fully understand how exercism works. I did not realize that exercises are unified across the languages. You can read this thread for some discussion on this exercism/discussions#158 My original idea was to have for Coq a totally separate set of exercises, slowly introducing basic aspects of Coq theorem proving as well as writing functional code in Gallina. Something along the lines of "Software Foundations" exercises.

I am skeptical about replicating current standard exerocsim exercises for Coq. Gallina is not a general purpose programming language and may miss many required facilities. Even if such exercises could be written, proving any meaningfully properties such as correctness could too complex and demanding for a new Coq learner.

Frankly, I am not sure where we can go from here.

[kytrinyx]

I did not realize that exercises are unified across the languages.

@vzaliva They are mostly unified across languages, but it is a historical accident. As discussed in the issue you reference, we will be moving away from this model. You should consider the exercises in the common pool of specifications as completely optional—for some languages many of the exercises are useful, and in that case it makes it easier to bootstrap a language track.

My original idea was to have for Coq a totally separate set of exercises, slowly introducing basic aspects of Coq theorem proving as well as writing functional code in Gallina.

I think this is the most useful thing you could do, and it aligns perfectly with my vision for Exercism: https://github.com/exercism/docs/blob/master/about/goal-of-exercism.md It should be about introducing the core concepts of the language in question, not artificially following exercises that might be completely useless within the context of that language.

We will soon be introducing a change in how the exercises flow:

https://github.com/exercism/docs/blob/master/about/conception/progression.md

In order to move towards that new model, it would be useful to add topics and difficulties to the exercises that you create, and consider whether the exercise is on the mainline of the track ("core") or whether it is a "side quest". If it's not on the mainline, consider which exercise would unlock it.

[bagnalla]

Interesting. I can imagine some of the standard exercises as sort of "side quest chains" which begin by implementing the functional program in Gallina and progress by proving increasingly more difficult properties, leading up to some overall proof of correctness/safety.

@kytrinyx Could it be possible to have such chains where the first quest in the chain is unlocked by reaching some point in the main quest line, but subsequent quests are unlocked by progressing through that particular chain?

@vzaliva If you have a vision in mind for the main quest line then I don't mind just sticking to side quests.

[kytrinyx]

Could it be possible to have such chains where the first quest in the chain is unlocked by reaching some point in the main quest line, but subsequent quests are unlocked by progressing through that particular chain?

I don't know! @iHiD what do you think?