Coq: [documentation] Document adding tests to the test suite

[jashug]

Currently, how to run the test suite is documented in CONTRIBUTING, but I wasn't able to find any documentation on when or how to add a test to the test suite.

The process I have been attempting to follow was:

1. Report an issue (hopefully with a small, reproducible test case)
2. (In my fork of Coq) Add the test case to the test suite (how? where?) and see the test suite fail.
3. Fix the issue, and see the test suite succeed.
4. Submit the test and fix as a PR.

I took a guess and tried putting my tests in test-suite/bugs, but I'm still unsure whether to put them in opened or closed, nor what the meaning of messages like "(bug semes to be opened, please check)" is.

So my questions are,

• When should a bug-fix include a test case?
• Where should that test case be put?

[Zimmi48]

Good questions! After contributing to Coq for a while I'm still not fully sure how the full test-suite works.
What I know:

• Most bug reports can have tests added in test-suite/bugs: these are the bugs where something is failing (or succeeding). Basically files in this directory are just tested to compile (with coqc). There is a way to pass additional options to coqc using comments at the beginning of files. I don't think it is documented anywhere but looking at examples helps to understand.
• "(bug seems to be opened, please check)" just means that a test in the test-suite/bugs/closed/ directory failed.
• If a bug is in the opened/ sub-directory it is supposed to mean that it is still open, so to test it, the logic must be inverted (often by adding Fail in front of the command we would like to see succeed). I don't know in which case opened bugs should be added to the test-suite. I'm not sure what purpose they serve (detecting when we accidentally fix a bug, I suppose). @JasonGross added a bunch so he may have an opinion. There is also a current open PR that questions the status of some bugs in the opened/ sub-directory: #500.
• Bugs where the problem is not that a command is failing or succeeding but rather that the output is not correct can have a corresponding test in test-suite/output. Bugs there have both a .v file and a .out file that contains the expected output.

Here is what I don't know:

• All the kinds of tests that the test-suite contains. For instance, there is a part of the test-suite that tests complexity results and is supposed to adapt to the machine but I think most Coq developers don't even know how this works. I think that at least @herbelin knows.
• What is the recommended practice on how to run a single test, or how to get detailed reports on the errors. @JasonGross may have advice.
• In which case, we are supposed to add tests for fixed bugs: I suppose "most of the time" is the answer.

@jashug Would you be willing to create a PR to start this documentation (it should go in dev/doc I suppose or as a README in the test-suite/ directory but then with a link from CONTRIBUTING)? We could tag this PR as "help wanted" and ask other Coq developers to contribute with their knowledge.

[jashug]

Thanks for the response; I'll try to put something together.

[jashug]

I made a PR with some simple documentation.

[JasonGross]

I don't know in which case opened bugs should be added to the test-suite. I'm not sure what purpose they serve (detecting when we accidentally fix a bug, I suppose). @JasonGross added a bunch so he may have an opinion.

Yes, that purpose. My opinion is that if we had the manpower or the automaton, every open bug which is testable and which we agree is a bug would get a test case. (If nothing else, the fact that there is a but means that we didn't have test coverage for that part of the code.)

All the kinds of tests that the test-suite contains.

I personally have added tests in bugs/{opened,closed}, output/, output-modulo-time ( which is perhaps poorly named and contains tests of LtacProf with some Makefile post processing to make the output mostly deterministic), and coq-makefile, which contains bash scripts which are run and indicate success or failure with error codes. I believe any tests in bugs/ ( and not in a subdirectory) are a mistake, if there are any left ( there were at one point). Note also that command line options can be passed to coqtop via an emacs variable comment at the top of a bug file ( used to test things like -indices-matter and -impredicative-set).

What is the recommended practice on how to run a single test, or how to get detailed reports on the errors. @JasonGross may have advice.

Each file has a .log file that is generated by the Makefile. These logs are processed to print the status. I don't recall the exact naming convention, but if you invoke make on the test-suite Makefile, you can have it hill build just one of these logs. There's another target to just print a summary of the existing logs, I believe. Logs can be inspected to see detailed output. Failing logs can be displayed by defining variables such as TRAVIS_CI.

Having written this, I think we should improve the system by: (1) adding test-suite/%.log targets to the top-level Makefile; (2) ( maybe) adding the display status target to the top-level level Makefile; (3) providing a verbose printout option variable which does not end in _CI, documented for user consumption; (4) adding a verbose status option variable which causes .log targets to display the status of each built log immediately after the test is done running.

[JasonGross]

Oh, and:

In which case, we are supposed to add tests for fixed bugs: I suppose "most of the time" is the answer.

We don't actually have a good story for testing timing ( rather, idk how the complexity test-suite works and if it's good enough for things like "this bit is now 2x faster"). Some bugs are easier to fix than to test (some tests are very big and haven't yet been minimized or consolidated into one file, or are things like "coqdep takes too long when you have 5000 files"). We also don't yet have a story for unit tests, and I think we should get one. But insofar as a test can be added to prevent an unnoticed regression, it should be. Ideally, every time a PR breaks one of the CIs in a non-stupid way, we should add a test case to cover that behavior before fixing the PR. That may be too much to ask, though.