Zulip Chat Archive

Stream: general

Topic: tests for tactics?


Jalex Stark (May 27 2020 at 02:05):

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 (May 27 2020 at 02:10):

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 (May 27 2020 at 02:11):

"was a core tactic"

should i be PRing this to mathlib instead of core?

Mario Carneiro (May 27 2020 at 02:13):

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 (May 27 2020 at 02:13):

Feel free to make a new file

Mario Carneiro (May 27 2020 at 02:14):

the only assumption test I see is assumption_tac_notation.lean

Jalex Stark (May 27 2020 at 02:14):

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

Mario Carneiro (May 27 2020 at 02:15):

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

Jalex Stark (May 27 2020 at 02:16):

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

Jalex Stark (May 27 2020 at 02:17):

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 (May 27 2020 at 02:17):

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 (May 27 2020 at 02:17):

but that is sort of orthogonal to assumption? itself

Mario Carneiro (May 27 2020 at 02:19):

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 (May 27 2020 at 02:20):

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 (May 27 2020 at 02:22):

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 (May 27 2020 at 02:22):

i see, thanks

Mario Carneiro (May 27 2020 at 02:25):

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 (May 27 2020 at 02:28):

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

Jalex Stark (May 27 2020 at 02:35):

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

Bryan Gin-ge Chen (May 27 2020 at 05:11):

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).


Last updated: Dec 20 2023 at 11:08 UTC