[isabelle-dev] Towards the Isabelle2014 release

[Makarius]

On Tue, 22 Jul 2014, Lars Noschinski wrote:

> While working on bringing a larger library (AutoCorres) to 2014-rc0, I
> relatively often run into prover hiccups (processing theories stops for
> a while). This might be seconds, minutes or "too long, restarted the
> prover instead".

If this is a "PIDE grey-out", i.e. the prover process is busy but comes 
back spontaneously after many seconds, it means the ML heap is overfull 
and the Poly/ML RTS does a lot of online-sharing of values.

It might a sign that the application requires x86_64, but then the time 
for small mobile devices with only 4-8 GB is also over.  I do recall times 
when "4 GB" was synonymous with "inifinite memory", but that is long past.


> A related point is that opening a ML file in an already processed theory 
> seems to reset the processed proof state back to this theory, even if I 
> don't change anything.

That particular aspect is documented in the Isabelle/jEdit manual in the 
section about "Auxiliary files":

   Initially, before an auxiliary file is opened in the editor, the prover
   reads its content from the physical file-system. After the file is
   opened for the first time in the editor, e.g.\ by following the
   hyperlink (\secref{sec:tooltips-hyperlinks}) for the argument of its
   @{command ML_file} command, the content is taken from the jEdit buffer.

   The change of responsibility from prover to editor counts as an update
   of the document content, so subsequent theory sources need to be
   re-checked. When the buffer is closed, the responsibility remains to the
   editor: the file may be opened again without causing another document
   update.

That slightly odd dual-responsiblity was a concession to allow 
Isabelle/HOL source editing within PIDE, on small machines with only 4-8 
GB memory.


Their might be other snags that are not documented, so it is important to 
keep two eyes on it as usual.


 	Makarius