Re: [isabelle] No blast_trace anymore; assumption trace?
On Wed, 9 Oct 2013, Gottfried Barrow wrote:
It was using "declare[[blast_trace=false]]" and
"declare[[blast_stats=false]]" with Isabelle2013 that showed me that
auto sometimes calls blast, but those traces cause an error now. Did
anything replace them?
These options are a leftover when Larry implemented the tool, and were not
meant for end-user consumption, as far as I can tell.
In Isabelle2013-1-RC2 you can refer to them nonetheless, using regular ML
operations for configuration options:
setup "Config.put_global Blast.trace true"
That is a rather indirect way to see when blast happens to be invoked by
other proof tools. Generally, producing a meaningful trace is very
difficult for anything non-trivial.
This archive was generated by a fusion of
Pipermail (Mailman edition) and