[isabelle-dev] Meson's tracing output

[Jasmin Christian Blanchette]

Hi all,

The "meson" proof method outputs some annoying messages like

  0 inferences so far.  Searching to depth 0
  3 inferences so far.  Searching to depth 5
  6 inferences so far.  Searching to depth 15
  9 inferences so far.  Searching to depth 25
  12 inferences so far.  Searching to depth 35
  15 inferences so far.  Searching to depth 45
  18 inferences so far.  Giving up at 55

which come from "THEN_ITER_DEEPEN" and cannot be suppressed. Strangely enough, most but not all "tracing" calls in that tactical were protected by a "! trace_DEPTH_FIRST" check.

In this proposed change, I also guard the remaining two "tracing" calls with the check:

  http://isabelle.in.tum.de/testboard/Isabelle/rev/bc937aef36f5

This means that "meson" is quiet by default, and as a result Sledgehammer proof reconstruction can also proceed quietly. (Verbose tools whose output can't be disabled are bad citizens in an interconnected world.)

If nobody objects, I will push the proposed change to the main Isabelle repository.

Jasmin