Re: [isabelle] Isabelle2016-1-RC1 processing theories twice



On 08/11/16 15:42, Mathias Fleury wrote:
> 
> I looked a bit more at it and I failed to understand how the
> undefined_blobs is emptied when jedit_auto_resolve triggers a
> reprocessing.

Blobs start out as undefined. Resources.parse_changes and
JEdit_Resources.commit is the place where incoming edits may request
further resolution of dependencies -- via PIDE.deps_changed(). Thus
blobs are loaded eventually and become defined in a later edit.

The problem was caused by the loss of a PIDE.deps_changed() event in a
situation of unfinished pipelining of edits. Then after scrolling, which
is an edit of the document perspective, that was finished and indirectly
caused some theories to be reprocessed.


The deeper conceptual problem behind this: undefined blobs are silently
loaded from the file-system by the prover. This was done on purpose, in
order to be able to load Isabelle/HOL into the Prover IDE, on a small
machine with "only" 8GB. Here the blobs are not part of the PIDE
document content.

At some point this all needs to be revisited, to make it simpler and
more scalable by default, without strange options that can cause problems.


> I find the name loaded_theories for the loaded sessions very confusing by the way.

I don't understand the confusion. The background session image has
certain theories that are already loaded (and cannot be edited). This
set is called loaded_theories.


	Makarius








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