[isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
christian.urban at kcl.ac.uk
Thu Apr 4 14:45:50 CEST 2013
On Thursday, April 4, 2013 at 12:42:42 (+0200), 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?
Could the reason be that more often than wanted the answer to
emails on the Isabelle mailing lists is:
"person ?X, you have no business here"
"any changes to ?X are restricted to exactly one person"
you are on the wrong mailing list (isabelle vs isabelle-dev)
you did not look up the history from ?X years ago
you did not follow conventions (usually about *informal*
conventions for theory names, ML-styles, source comments etc)
you better refer to changesets with [cryptic] hashes like dd6dd81381fb
this is not a bug, but a running gag
Maybe the latter answers might be more perceived answers
than actual answers, but I hope people get the gist.
More information about the isabelle-dev