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



Hello Makarius and Isabelle list,


@Jasmin and Manuel: a possible workaround consists in deactivating the auto_resolve in the Isabelle options.



Now the technical details:

> On 1 Nov 2016, at 22:32, Makarius <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 <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â).


>> Is there anyway to give more informations?
> 
> Any particular jEdit plugins and preferences. In particular, what is the
> Look-and-feel?
> 


Having a look at this part of the question showed me that opening and closing the option panel triggers the same reprocessing. Or even just activating the auto_resolve option.

* Mac OSX Look-and-feel.
* No plugin.

Is there a good way to give the list of the Isabelle-relevant options?



Mathias



> 
> On 31/10/16 18:37, Mathias Fleury wrote:
>> 
>> Steps to reproduce:
>> Run isabelle such that it loads some theories, e.g.:
>>   isabelle jedit -l Pure src/HOL/List.thy
>> 
>> Wait until all of the theories are processed. 
>> 
>> Scroll in the buffer List.
>> 
>> 
>> Isabelle/jEdit first starts processing List and then restarts processing the buffers from the beginning.
>> 
>> Instead of waiting that all theories are processed, one can also do some random clicking in the List buffer.
> 
> I still cannot reproduce it -- I've seen it last summer on the machine
> of Jasmin once, but never anywhere else.
> 
> Is that really a fresh Isabelle2016-1-RC1 without any special options or
> preferences?
> 
> 
>> The described reprocessing of the files is done only once. It appears on both macOS (running Sierra) and Linux (archlinux, so another unsupported OSâ).
> 
> Arch Linux is just untested, but not unsupported. The reason for that is
> due to the nature of it being individually configured in every respect.
> It means anything could go wrong, but Arch users are the master of their
> system and can make it work.
> 
> In practice, I have never heard of a specific Arch Linux problem with
> Isabelle, although I occasionally see users of that platform.
> 
> 
>> Is there anyway to give more informations?
> 
> Any particular jEdit plugins and preferences. In particular, what is the
> Look-and-feel?
> 
> 
> 	Makarius
> 
> 




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