tests for tactics?

Stream: general

[Jalex Stark]

I wrote an assumption? tactic, following [this thread].(https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Achievement.3A.20multiply.20convergent.20sequences/near/198830593)
The code is in this private branch, and I think it's ready to PR modulo tests.

I'm not sure where to put the tests. the test folder is kind of a big place. I can't tell if there are already tests for assumption that the new tests should live with. Or maybe they should live on their own in the interactive folder?

[Scott Morrison]

I think the standard practice would just be to create test/assumption.lean. As this was a core tactic, it probably didn't have existing tests.

[Jalex Stark]

"was a core tactic"

should i be PRing this to mathlib instead of core?

[Mario Carneiro]

The tests are separated into those that involve server interaction and those that don't. Other than that it's sort of a free for all as far as naming

[Mario Carneiro]

Feel free to make a new file

[Mario Carneiro]

the only assumption test I see is assumption_tac_notation.lean

[Jalex Stark]

okay, so I should make a new file inside of the interactive folder?

[Mario Carneiro]

no, I think this one doesn't need server interaction so it would be in tests/lean

[Jalex Stark]

oh okay, I guess i don't know what server interaction means

[Jalex Stark]

the test for trace is in tests/lean/interactive, I guess you're saying that tests/lean has ~no organization and I can plop down an assumption.lean wherever

[Mario Carneiro]

In this case, you are just printing something. The server interaction would be checking that this gets highlighted, and clicking on it produces a working proof

[Mario Carneiro]

but that is sort of orthogonal to assumption? itself

[Mario Carneiro]

the interactive tests have an expected.out file that consists of the JSON commands that lean is expected to produce when given this input file. interactive/trace.lean for example is testing that the blue highlighted span covers the right characters

[Mario Carneiro]

for non-interactive tests, the expected.out file just contains the output you would get if you ran lean foo.lean on the console

[Mario Carneiro]

So you would use interactive tests for testing things like hovers, getting the goal state, and other things like that that are not reported in non-interactive use

[Jalex Stark]

i see, thanks

[Mario Carneiro]

I'm not sure if there is a tool in the tests folder for producing a valid expected.out file, but it is easy enough for non-interactive tests, you run lean my_test.lean > my_test.lean.expected.out and check that the file looks okay

[Jalex Stark]

how do I get a lean binary that includes the changes I made to core?

[Jalex Stark]

this is now [WIP] lean#281, maybe tomorrow I will figure out how to build the test

[Bryan Gin-ge Chen]

The build instructions are here. The bottom of the file also has info on running the tests.

As far as where to put the tests, there are several types. The simplest tests go in tests/lean/run. The files in that directory are just checked to make sure that they compile without errors. The files in the directory above that have an associated .expected.out file which the test runner checks against the produced output. The interactive tests have their own format, you can put in line comments with carets in them indicating where to run server commands (e.g. this file) and then the server output is compared to the contents of .expected.out (e.g. the corresponding file).