[isabelle-dev] NEWS: more informative errors in lazy enumerations
makarius at sketis.net
Wed Oct 17 12:19:58 CEST 2012
On Wed, 17 Oct 2012, Peter Lammich wrote:
> On Mi, 2012-10-17 at 11:09 +0200, Makarius wrote:
>> *** ML ***
>> * Type Seq.results and related operations support embedded error
>> messages within lazy enumerations, and thus allow to provide
>> informative errors in the absence of any usable results.
> Cool, no more writing of error messages to the trace buffer when
> debugging tactics.
It probably does not help here:
On Wed, 17 Oct 2012, Makarius wrote:
> note that plain tactics are inherently restricted to the classic failure
> and backtracking model without error messages.
BTW, the trace buffer is only relevant for Proof General in order to get
messages past its built-in filtering and priority model of
writeln/warning/error. In Isabelle/jEdit you would just use plain writeln
by default and then inspect the output or hover over the squiggles in the
Tracing did get a new meaning in Isabelle/jEdit recently, when I
introduced some means to restrict its volume at the very source of the
message stream. Thus a simp trace gone wild would just expire the command
transaction. For example in Isabelle/b0d6d2e7a522:
datatype foo = Foo | Bar foo
This gives you 0.5 MB of message content -- 184 Tracing messages shown in
the Output window if the radio button is enabled -- and finally some error
"Tracing limit exceeded: 509725" before any further harm is done.
This is a relatively cheap trick to address an ancient problem. I would
be interested to hear from early adopters how it works out in hard work.
More information about the isabelle-dev