Re: [isabelle] Death by tracing



On 06/12/16 14:55, Lars Hupel wrote:
> 
>> I noticed this problem when I proved 1024 theorems with the
>> âapproximationâ method, which outputs one line of tracing information
>> every time. Does this mean that âapproximationâ shouldn't be using
>> âtracingâ to output this information?
> 
> Probably not by default, or at least with the option to disable it.

Tracing is in some sense debugging, and that should have an option to
*enable* it, i.e. it should be *disabled* by default.

We have a long record of really strange effects caused by tools
producing "potentially useful output" by default. I put that phrase into
quotes, because it is a technical term of Isabelle lore.

These effects might be technical (e.g. bombing the front-end) or
psychological (e.g. tons of irrelevant messages hiding one important
message that indicates an error, which is then overlooked).


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.