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