Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing
On 19/11/14 11:01, Makarius wrote:
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.
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'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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and