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 MHonArc.