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

> On 8 Nov 2016, at 12:26, Makarius <makarius at> wrote:
> On 08/11/16 08:13, Mathias Fleury wrote:
>>> On 1 Nov 2016, at 22:32, Makarius <makarius at
>>> <mailto:makarius at>> wrote:
>>> If it is reliably reproducible for you, you can also make a bisection on
>>> the repository to see where the problem is located in the history.
>> I've finally done it and the issue is much older than had I expected: it
>> goes back to
>> commit and more
>> precisely to the following part of the change:
>> - if (change.deps_changed && PIDE.options.bool("jedit_auto_load"))
>> PIDE.deps_changed() + if (PIDE.options.bool("jedit_auto_load") &&
>> change.deps_changed || + PIDE.options.bool("jedit_auto_resolve") &&
>> change.version.nodes.undefined_blobs.nonEmpty) + PIDE.deps_changed()
>> jedit_auto_resolve is activated (both in this version by default and in
>> my setup). If there are non-processed blobs (i.e. a lot of SML files
>> here) and I click in the List buffer, the processing restarts. I have no
>> idea why the reprocessing happens only once (i.e. there are no
>> undefined_blobs anymoreâ).
> Thanks for doing the bisection.
> The change above is from August 2015. There are more changes where
> jedit_auto_resolve fluctuates back and forth, without clear conclusion:
> see occurrences of "auto" in
> <>

Indeed, but the culprit is the change in the if condition.

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. I don't even understand why this should happen at all: as far as I got it, the blobs are ML files and theories that have already been loaded in the session (I find the name loaded_theories for the loaded sessions very confusing by the way). So why should a reprocessing be triggered if there is no change in these files?


> It is a genuine "feature": something added on the spot, without being
> properly thought out. I had it on my list over some months in 2015, but
> did not revisit it.
> I will make one round of looking carefully how it behaves at the moment,
> and then see if it is put into proper shape for the release, or removed
> outright.

> There is a bigger plan in the pipeline, to reform the management of all
> source files for a PIDE session. When that happens, both jedit_auto_load
> and jedit_auto_resolve become obsolete.
> 	Makarius

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