Unit tests for lean server

Stream: general

[Jason Rute]

I cleaned up the Lean Python client making sure it properly parses the output of the Lean server. I'm now (slowly) writing unit tests. It would really help to have a list of expected outputs of the Lean server, under different situations. I want to make sure I properly handle various edge cases such as this response to the "hole_commands" request.

{"message":"hole not found","response":"ok","seq_num":11}

Are there lists of these sort of things, possibly as tests for the Lean server? I could find a few such tests for the new widgets feature but that is it.

[Reid Barton]

there's tests/lean/interactive, is this what you are after?

[Jason Rute]

It is a good start and I'll use them for testing. (I was looking in the /tests/lean/server, which is why I didn't find it.) However, I think a number of edge cases like the one above are missing, but I'll work with what I can...

[Reid Barton]

git grep -- '--^' shows a few other tests which also use this magic syntax

[Utensil Song]

I might suggest trying a record-and-replay method to establish a unit test coverage baseline instead of explicit handwritten unit test which would be hard to cover edge cases.

By "record-and-replay", I mean using unit tests in Lean (or some selected mathlib files in different areas and styles) as Lean files, program some different ways (input in one go, input line by line, random insertion and deletion like a monkey etc.) to input them or stepping through them to generate the requests, record the output of Lean server, use them as the expected result of unit tests and do pruning later for efficiency.

Of course, this is not as clear as well designed unit tests based on white-box understanding of the system internals but it could serve as a baseline and quickly have good test coverage. Depends on the purpose of the tests.

[Johan Commelin]

I think a lot of the tests are already of this form