Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing

Dear Makarius,

These DUP exceptions (with varying values) occur several times a day with Isabelle2014. They happen when I heavily use find_theorems (with session image HOL-Probability). Most likely, when I start the search while there is no valid context (e.g., because the current theory file is part of HOL-Probability or because there is a syntax error), or when I restart the search while another search is still going on. A week ago, I switched to the repository version (currently 059ba950a657). Since then I have not experienced any of these greyouts. I'll let you know on isabelle-dev when they reappear.


On 18/11/14 22:05, Makarius wrote:
On Wed, 29 Oct 2014, Andreas Lochbihler wrote:

Here is another datapoint in the greyout story with Isabelle2014. The attached syslog
ends with a DUP exception. This time there were no exceptions on the command line. The
greyout happened again while I was using the query panel to find theorems.

The syslog ultimately says this:

   Isabelle protocol command failure: "Document.update"
   exception DUP ~5951 raised (line 261 of "General/table.ML")

which refers to Table.update_new.

Looking at the source, I did not find a plausible way how this exception could have
happened -- there are normally handlers to say something more specific like ERROR
"Duplicate command: ~5951".

If you see anything like this again, please tell me about it.

In Isabelle/f4e9bd04e1d5 I have reduced the chances of such low-level DUP exceptions,
although that might not be directly relevant. We should continue this on isabelle-dev next



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.