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



Hi Makarius,


On 19/11/14 11:01, Makarius wrote:
These DUP exceptions (with varying values) occur several times a day with Isabelle2014.

I was not aware of any such problem in the official release.  As usual, problems that are
kept secret will remain so over indefinite time.
I did not get these exceptions during the test phase of release candidates, but I was not working as intensively with Isabelle at that time, either. You cannot complain that I have not reported this problem with DUP. I just did not want to send you an e-mail every time the same failure occurs.

 In Isabelle/f4e9bd04e1d5 I have reduced the chances of such low-level
 DUP exceptions, although that might not be directly relevant.

It could be worth trying this tiny change
http://isabelle.in.tum.de/repos/isabelle/rev/f4e9bd04e1d5 on official Isabelle2014, just
by editing $ISABELLE_HOME/src/Pure/General/table.ML accordingly and rebooting the system.
I'll do that, but I cannot promise that I will have time to thoroughly test it during work. My work now has moved to the repository version and no longer runs with Isabelle2014, but I have a bunch of other theories that I might get back to some time.

Andreas




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