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



> On 8 Nov 2016, at 12:26, Makarius <makarius at sketis.net> wrote:
> 
> On 08/11/16 08:13, Mathias Fleury wrote:
>>> On 1 Nov 2016, at 22:32, Makarius <makarius at sketis.net
>>> <mailto:makarius at sketis.net>> 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 https://isabelle.in.tum.de/repos/isabelle/rev/60916 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
> https://isabelle.in.tum.de/repos/isabelle/log/857acb970dfa/src/Tools/jEdit/etc/options <https://isabelle.in.tum.de/repos/isabelle/log/857acb970dfa/src/Tools/jEdit/etc/options>

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?


Mathias

> 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.