Unit tests tactics

Stream: new members

[Guilherme Silva]

I was looking at tactics. Is it possible to do some unit tests with them?
I know that tacticis defined as interaction_monad tactic_state.
I wish to create some tactic state, run a tactic in it and after, see the new tactic state.

[Floris van Doorn]

I don't think you can print the whole tactic state. However, since most tactics only change a few things in the tactic state, you can easily trace those.
You can look at the test folder in mathlib for some unit tests.

[Guilherme Silva]

I saw how they made some tests. It were really useful.
But it is different of the traditional way of doing test, like
example : double 2 = 4 := rfl.
Because they tested the tactics using it as tactics.
I do not know if it is possible to test tactics in the traditional way.

[Scott Morrison]

I don't think I understand what you want, or what distinction you're making between "the traditional way" and what exists in test/.

[Guilherme Silva]

In traditional way, it is not allowed to use tactics. It would be a function for example:
testTactic (old_state : tactic_state) (Tactic : tactic unit) (new_state : tactic_state) : Type
One way of testing it would be for example:
example : testTactic "A -> B" intro "Goal B. H : A" := ()