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
