[isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
makarius at sketis.net
Thu Apr 4 12:42:42 CEST 2013
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
More information about the isabelle-dev