Zulip Chat Archive

Stream: new members

Topic: Unit tests tactics

Guilherme Silva (Jun 27 2020 at 02:52):

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 (Jun 27 2020 at 05:34):

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 (Jun 27 2020 at 19:21):

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 (Jun 28 2020 at 03:26):

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 (Jun 28 2020 at 03:39):

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" := ()

Last updated: Dec 20 2023 at 11:08 UTC