Stream: Beginner Questions

Topic: Isabelle loosing typecheck memory


view this post on Zulip Nicolò Cavalleri (Jun 30 2021 at 20:49):

Once every while, while I am using Isabelle, it stops typechecking the file I am working on, the coloured line on the left becomes light pink and I can't use it anymore until I restart it. Does anyone know if this is a common problem?

view this post on Zulip Lukas Stevens (Jul 01 2021 at 08:22):

Yes that is the dreaded grey out. Sometimes Isabelle manages to recover from that but it is often faster just to restart jEdit.

view this post on Zulip Nicolò Cavalleri (Jul 01 2021 at 10:27):

Do you know what is it due to?

view this post on Zulip Mathias Fleury (Jul 01 2021 at 10:28):

if we would know, we would all have fixed the problems on our machines…

view this post on Zulip Nicolò Cavalleri (Jul 01 2021 at 10:32):

Well maybe the reason was known but there was not easy fix to it...

view this post on Zulip Mathias Fleury (Jul 01 2021 at 10:35):

From what I could see, there is a strong correlation between large developments and grey outs. So using base sessions helps.

view this post on Zulip Manuel Eberl (Jul 01 2021 at 10:35):

I think it happens particularly easily when you have some proof method running amok. Since you use transfer a lot, things like by (transfer, auto) can sometimes cause a lot of backtracking when they fail due to nondeterminism of transfer.

view this post on Zulip Nicolò Cavalleri (Jul 01 2021 at 10:36):

Ok thanks! What does "base sessions" means?

view this post on Zulip Mathias Fleury (Jul 01 2021 at 10:38):

base session are the theories that is loaded when you start. By default this is HOL, but it can make sense to have a bigger base session (for you HOL-Analysis maybe?).

view this post on Zulip Manuel Eberl (Jul 01 2021 at 10:42):

Yes, you can built tell Isabelle/jEdit to use a session image for e.g. HOL-Analysis by running it as isabelle jedit -l HOL-Analysis. It will then build the image once (might take something like 10–15 minutes on slower machines), but after that, you will always be able to immediately use it.

view this post on Zulip Manuel Eberl (Jul 01 2021 at 10:43):

Theories from those pre-built images also don't get loaded into jEdit, which means that you can't Ctrl+Click around in them or change things in them, but on the up side, they also don't consume resources in jEdit. They just make everything a bit smoother.

view this post on Zulip Mathias Fleury (Jul 01 2021 at 10:44):

Technically the isabelle jedit -R <my_session> is better if you import multiple session (it precompiles more), but isabelle must know your ROOT file for that

view this post on Zulip Jakub Kądziołka (Jul 01 2021 at 11:39):

eh, it can load multiple images like that? I had created a separate session to deal with this... https://github.com/NieDzejkob/isabelle-math-contests/blob/master/ROOT#L3-L9

view this post on Zulip Mathias Fleury (Jul 01 2021 at 11:53):

the sessions are compiled


Last updated: Aug 13 2022 at 05:18 UTC