Inlining tests

Stream: maths

[Yaël Dillies]

I have repeatedly been asked to move tactic/general metaprogramming tests to standalone files under MathlibTest, most recently here.

[Yaël Dillies]

However I still don't understand the point of making standalone test files for meta things that already function the way they're intended to work by the end of their file:

1. Tests can already be made at the end of the file
2. One gets instantaneous feedback when modifying/fixing breakage of the meta thing
3. The tests demonstrate to the wandering user how to use the meta thing
4. The tests don't weigh in the oleans + they are usually instantaneous

[Eric Wieser]

Yaël Dillies said:

The tests don't weigh in the oleans + they are usually instantaneous

Perhaps we should have fast_example defined as example with a lower heartbeat count, to enforce this?

[Damiano Testa]

In some cases, the slightly different environment setup that the test files have may be useful for actual testing. E.g. what options are on, which linters are running, whether declarations are defined in the same module or not,...

[Robert Maxton]

In some cases, yes, but often not, especially for particularly simple tactics.

At any rate, I would heartily support that at the very least, test files should always be linked from their implementation files, because test files are kind of hard to find (examples don't leave searchable theorems behind) while implementations can be easily found with go-to-definition. I quite often end up having to reverse engineer how obscure/undocumented tactics work from their code, and having examples and tests to work from is very helpful when they exist.

[Chris Bailey]

Devils advocate:

1. Inline tests are going to have an effect on the UX in the editor when viewing/modifying the source file, both in time and space. They can also make search more difficult if a given string appears often in a test/example relative to its substantive occurrences.
2. Now someone looking for tests has two places to look instead of one (is it in the file or is it in a test file)
3. Similarly, there will probably be debates about whether a given thing should be an inline test or go in a test file, or when some inline tests should be be extracted into their own file.

[Mario Carneiro]

Inline tests increase the "mandatory build time" of a given file. Sure, mathlib is usually not built by users, but it should be possible to build mathlib only up to some file manually and not have to build tests along the way. In fact, even CI does this - the test step is separate from the build step, so you can see the relative overall performance of the two stages and get separate feedback from them.

[Yaël Dillies]

Sure, but the tests I have been told to move out are syntax or domain tests, not performance.

[Mario Carneiro]

For the same reason that we minimize dependency bloat and try to ensure that only the actual requirements of a given piece of mathlib are in its dependency tree, we don't want things that don't contribute to the build to be in the build

[Mario Carneiro]

testing is a separate activity from building

[Eric Wieser]

But at the same time, we do refrain from over splitting files, as this makes development more painful. In the same way, having the tests elsewhere for notation and tactics does increase the development time when working on them.

[Eric Wieser]

I would heartily support that at the very least, test files should always be linked from their implementation files,

I agree that if we have test files, we at least should have a 1:1 mapping where possible (which we could then document centrally). Very frequently the tests are lumped together into one big file, and so if I tweak one norm_num extension I have to rebuild all the others before I can test my change.

[Damiano Testa]

I also find that having the cache of the MathlibTest files would be useful.

[Eric Wieser]

Why would that be useful?

[Eric Wieser]

If the test fails there's no cache, and if it passes you don't need the cache

[Damiano Testa]

When a lot of them fail, I like to open them all at once to fix/understand the errors, so I would build them and extract that info from there.

[Damiano Testa]

There would be no cache even if the tests are just noisy, but not erroring?

[Eric Wieser]

Does that ever happen?

[Eric Wieser]

Also, even if you did have a cache, I don't think it is used for the file you are currently looking at.

[Damiano Testa]

No, but say that 10 test files are broken, then I would like to build all the test files and catch the errors from the commandline instead of copy-pasting the ones that are broken from the CI workflow.

[Damiano Testa]

As is, I either have to rebuild all of them, also the ones that are ok, or do some copy-pasting.

[Damiano Testa]

It is not the end of the world, but I would have found it convenient to have the cache for the tests, even if only for the non-broken ones.

[Damiano Testa]

In my situation, I would write a new linter and half of the test files do not comply, but they are not "broken", since the linter message may not be caught by a #guard_msg.