Exercise template

[vzaliva]

( moving here discussion from exercism/generic-track#22 )

We need to decide how exercises will be presented. We discussed 3-file (setting, solution, test) vs 2-file (solution, test) approaches. Let us decide on one, prepare few sample exercises to test how it work.

[vzaliva]

Moving my last comment from old issue here:

@ErikSchierboom How do other languages deal with additional types and functions provided? Do they put it in stub implementation file?

[ErikSchierboom]

@vzaliva Well, it depends. There are a couple of variants as far as I know:

1. The track only provides a test file.
2. The track provides a test file and an empty implementation file.
3. The track provides a test file and a stub implementation file.
4. The track provides a test file and a stub implementation file, but only for the first X exercises.

Only in the third and fourth case is any actual code prepared for the user. There has been a discussion on this topic on the discussions repo, which shows that different tracks have different strategies.

Basically, it comes down what the language track's maintainers feel is the best fit for their track. For the tracks I maintain (C#, F# and Scala), I feel that having a stub implementation file allows the users to not focus on the boring, repetitive parts (which an IDE can do for them), but instead focus on the actual problem itself.

If having three files, or six files, or whatever makes sense for Coq: go for it! You should definitely not feel obligated to follow any other track, although you can of course take inspiration from their solutions :)

Getting some sample exercises is a great idea. If you know any Coq enthusiasts, it might be useful to let them chip in with their thoughts too.

[vzaliva]

In Coq many if not most problems may need some auxiliary code. For example, it may define a function or a type and ask to prove a theorem stating some properties of it.

I think I would prefer to keep these auxiliary definitions outside of the file which user edits and submits for 2 reasons:

1. User not supposed to change these. We want to avoid accidental or intentional changes to them.
2. We want to keep user's submission short. If problem setup is 30 lines of definitions followed by 10 lines of actual proof we would not want to see each submission to start with identical 30 lines. It makes them hard to read.

[vzaliva]

OK, here is my current thinking:

1. Modules were overkill. I got rid of them
2. Solution file has implementation stub with a comment where the user should put his code.
3. The setup file is optional. Some problems may have it some not. If it is present it will be imported from implementation stub.

I've changed my 2 toy examples along these lines: https://github.com/vzaliva/coq-exercism-examples

The remaining issue is whether we need Test file or not.

[vzaliva]

Here is an example of an exercise which needs a test file:

https://github.com/vzaliva/coq-exercism-examples/commit/d560040b44d3deda99f0ba93292d809b8541cafd

For other excericses test files not needed, as long as user solution compiles with Coq. I will remove them.

So in conclusion, each exercise will have 1-3 files:

1. Setup file (e.g. Ex1.v). Definitions required for exercise. Not supposed to be changed by a user. OPTIONAL.
   2.Solution file (e.g. Ex1Solution.v). Initially, includes a stub for a solution with a comment where the user should put his code. This is the only file user supposed to change. MANDATORY
2. Unit test file (e.g. Ex1Test.v). Some unit tests for user solution. OPTIONAL.

All *.v files present should compile within given timeout. If no error produced, the exercise considered to be passing unit tests and ready for submission.

[ErikSchierboom]

Looks good!

[proger]

I've also updated base TRACK_HINTS https://github.com/exercism/xcoq/blob/master/exercises/TRACK_HINTS.md