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?
Yes that is the dreaded grey out. Sometimes Isabelle manages to recover from that but it is often faster just to restart jEdit.
Do you know what is it due to?
if we would know, we would all have fixed the problems on our machines…
Well maybe the reason was known but there was not easy fix to it...
From what I could see, there is a strong correlation between large developments and grey outs. So using base sessions helps.
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
Ok thanks! What does "base sessions" means?
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?).
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.
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.
isabelle jedit -R <my_session> is better if you import multiple session (it precompiles more), but isabelle must know your ROOT file for that
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
sessions are compiled
Last updated: Aug 13 2022 at 05:18 UTC