MESON_TAC works by first converting the problem instance it is given into an internal format where it can do proof search efficiently, without having to do proof search at the level of HOL inference. If a proof is found, this is translated back into applications of HOL inference rules, proving the goal.

The feedback given by MESON_TAC is controlled by the level of the integer reference variable mesonLib.chatting. At level zero, nothing is printed. At the default level of one, a line of dots is printed out as the proof progresses. At all other values for this variable, MESON_TAC is most verbose. If the proof is progressing quickly then it is often worth waiting for it to go quite deep into its search. Once a proof slows down, it is not usually worth waiting for it after it has gone through a few (no more than five or six) levels. (At level one, a “level” is represented by the printing of a single dot.)