[isabelle-dev] Meson's tracing output

[Lawrence Paulson]

Go right ahead. I had no idea this was even still used.
Larry

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:
> 
>  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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev