[isabelle-dev] Meson's tracing output
lp15 at cam.ac.uk
Thu Jan 30 00:56:50 CET 2014
Go right ahead. I had no idea this was even still used.
On 29 Jan 2014, at 23:33, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> wrote:
> 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:
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev