Re: [isabelle] 2014-RC1 issues

On Wed, 30 Jul 2014, Lars Noschinski wrote:

Here is a list of issues that I encountered with RC1:
Another issue I encountered with RC1 today (I didn't encounter the issue
with RC0, but my usage intensity might have been to low): I modified
some file (in a ML block), did some jumping around (through other
buffers), came back to the changed line and didn't see the change
anymore. I redid the change, which lead to an error message which made
it clear that the system saw something else than I was seeing in the
buffer. I reloaded the buffer and the error went away.

I have completed two rounds through the new auxiliary file management in the Prover IDE, and robustified it wrt. various fine points. When the next release candidate is published, please keep an extra eye on that aspect.


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