Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:14):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
For the record, I have been running into these issues too on my Mac for the past several months. I have also showed them to Makarius during ITP, so it should be on his radar.

Jasmin

view this post on Zulip Email Gateway (Aug 22 2022 at 14:14):

From: Manuel Eberl <eberlm@in.tum.de>
I also noticed this. Additionally, it seems that the IDE gets very
unresponsive if you change stuff in an "early" theory in the dependency
tree. Sometimes it's so bad that I have to restart the entire thing.

Manuel

view this post on Zulip Email Gateway (Aug 22 2022 at 14:32):

From: Makarius <makarius@sketis.net>
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?

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.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 14:33):

From: Makarius <makarius@sketis.net>
This sounds more like the normal situation when the JVM heap fills up --
this is inherent in JVM memory menagement. The default configuration
for x86_64 platforms has -Xmx2560m in a platform-specific place. A
typical value is -Xmx4096m and more can be tried depending on the hardware.

E.g. the new HOL-Analysis session is so big that it easily exhausts the
defaults. I have tried it on the 32bit Windows version, where the JVM is
confined to 1 or 1.5 GB, and it locks up almost immediately due to
overfull heap.

Here is cumulative information from NEWS for Isabelle2016 and
Isabelle2016-1:

Instead of adding more options next time, I will try once again to tune
the whole system such that it can carry even bigger application. That
game is a variant of Tetris, but so far it could always be continued one
step further.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 14:35):

From: Mathias Fleury <mathias.fleury12@gmail.com>
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@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:

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.

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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:35):

From: Makarius <makarius@sketis.net>
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

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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:36):

From: Mathias Fleury <mathias.fleury12@gmail.com>

On 8 Nov 2016, at 12:26, Makarius <makarius@sketis.net> wrote:

On 08/11/16 08:13, Mathias Fleury wrote:

On 1 Nov 2016, at 22:32, Makarius <makarius@sketis.net

<mailto:makarius@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:

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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:37):

From: Makarius <makarius@sketis.net>
This turned out rather unspectacular. It is just a feature that was not
fully finished in 2015.

See now
https://bitbucket.org/isabelle_project/isabelle-release/commits/812c22e556b9

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 14:37):

From: Makarius <makarius@sketis.net>
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

Last updated: Apr 19 2024 at 16:20 UTC