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.


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.


isabelle-dev mailing list

Reply via email to