[isabelle-dev] Fix top-level printing of exception messages containing forced-line breaks

[Thomas Sewell]

None of us reported my problem, because it concerned a somewhat 
elaborate case in some somewhat elaborate code I wrote, which we never 
managed to conveniently reproduce. Noone realised at the time that the 
exception-printing mechanism was at fault all by itself. This would be 
an archetypal bad bug report.

By comparison, David is providing you with what would be considered a 
good bug report in most open-source communities. It comes with a clear 
explanation not only of what the problem is but what causes it to occur, 
and how it might be fixed. In such communities, the proposed patches are 
nearly never applied as-is, but they provide a far more useful starting 
point than the average bug report.

I suppose Isabelle is interesting in that it is largely deterministic, 
so if a complaint can be minimised it can usually be easily reported.

On the topic of mailing lists: we do indeed have a highly reactive 
mailing list, but many of us find that the usual reactions are rarely 
useful. We attempt to improve the quality of information in both 
directions by focusing on issues where there is a quantity of evidence. 
In particular, you do not want a running blog from me of every occasion 
on which Isabelle thwarts me.

Finally, on the issue of "WWW_find", I know that Raf has had a look at 
it, and declared that it isn't a triviality. I think it might be a while 
before any serious work on it is done.

Yours,
     Thomas.

On 04/04/13 21:42, Makarius wrote:

> On Thu, 4 Apr 2013, Thomas Sewell wrote:
>
>> David's investigation explains a problem we had a few years ago where 
>> some custom tactics of mine were killing my colleagues' ProofGeneral 
>> sessions when they encountered errors. The workaround at the time was 
>> to remove all potentially useful debugging information (terms, in 
>> particular) from the relevant exceptions. Unfortunately this made 
>> tracking down the bugs in the tactics somewhat challenging.
>>
>> In hindsight, I should probably put the debug terms in the 
>> tracebuffer and thrown a vanilla exception. Hindsight is perfect, of 
>> course.
>
> So why did none of you guys ever report that?  We have a very reactive 
> isabelle-users mailing list, compared to most other project's "issue 
> trackers".  It is also possible to discuss anything for inter-release 
> Isabelle versions here on isabelle-dev, although its reactivity needs 
> to be specifically slowed down to avoid hazards in the development 
> process.
>
>
> Having a certain observation or undesirable behaviour on someone's 
> TODO list for 1-2 years already, it is like to be a matter of the past 
> now.
>
> Instead we have a lot of wasted time here with patches that are 
> proposed in a way to make it an urgent and immediate issue to be 
> "fixed" while you wait.
>
>
>     Makarius