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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
