silent regression tests

[wlammen]

Regression tests ensure that the behavior of interfaces remains unchanged across modifications. Due to their nature, they should report any failure, but need not necessarily issue success messages. In automated contexts, like continuous integration checks, messages from passed tests only clutter log files. A developer, on the other hand, might like to watch the progress of tests, or even need to see that all expected tests are executed.

To serve both needs, two versions of the test executable can be created: a silent and a verbose one. In the C sources, the value of TEST_SILENT macro, 'true' or 'false', determines what version is compiled. Although such a switch already exists, it cannot be easily set by the compilation scripts. Instead, source files or scripts have to be patched.

One important goal of this pull request is to expose this switch in the standard compilation scripts, so that it can be set easily:
build.sh -ct t-silent resp. build.sh -ct t-verbose creates a metamath-test executable with the corresponding setting of TEST_SILENT. build.sh -ct still works and produces the verbose version, as does a call to the current script.

In addition, the TEST_SILENT macro is now properly documented; see the attachment. TEST_SILENT is also now used only when regression tests are enabled.

[benjub]

This is indeed a useful mode, but a regular option, like -q for "quiet" seems more appropriate than an extra argument: it is harder for the user to get wrong (with the "argument method", a typo in the argument fails silently), it is easier to parse with getopts, it is consistent with the other settings of build.sh, and is simpler overall (e.g., q) test_silent_define="-DTEST_SILENT=true";; in the getopts case).

[benjub]

Suggested change

	run: ./build.sh -t
	# run: ./build.sh -t t-silent
	run: ./build.sh -tq # remove 'q' for verbose output

As you write yourself, silent/quiet mode is indeed better here.

[wlammen]

Is only the returned code of metamath-exe checked? For a proper failure message the output still needs to be presented. I do not know the details, so I deliberately left this open for comments.

[benjub]

Suggested change

	make "CFLAGS=-DTEST_ENABLE $TEST_SILENT_DEFINE"
	# rebuild src/mmtest.o to take into account changes in TEST_SILENT.
	rm -f src/mmtest.o
	make "CFLAGS=-DTEST_ENABLE $TEST_SILENT_DEFINE"

Then, Lines 48--55 of src/mmtest.h can be deleted.

[wlammen]

I can change between silent/verbose mode without problems using the -c flag.

It is likely that mmtest is on a base position of the dependency tree, but there is no guarantee.

I personally prefer supporting the -c flag, that is useful in all circumstances where a compilation should not rely on previously generated artifacts, as in

1. changing the git branch
2. modifying outside requirements like optimization, (test) modes and so on
3. whenever you are unsure what kind of artifacts you produced last time.

The gain of omitting part of the compilation amounts to a few seconds on my computer. This is nothing compared to tracking down an error induced by an inconsistent state.

[benjub]

Suggested change

	* .\build.sh -tc t-silent
	* ./build.sh -tq

[wlammen]

Backslash replaced.

Using a flag for the silent mode? The silent mode is tied to the -t flag and has no independent meaning. So logically it should be a value of the -t flag (like the -o flag has one). Unfortunately that would break backward compatibility.
You cannot explicitly activate the verbose mode. This creates a dependency of the call syntax on the default behavior of metamath-test.

This all is about how arguments are passed to build.sh. If a majority votes for using flags whenever possible, I will change this PR accordingly. One can accept this PR as it is, though, as it is fully backward compatible. If you are not satisfied with some details like how a new feature is invoked, I can address this in a future PR, or you can even do it yourself.