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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
