Nicolò Cavalleri (Jun 30 2021 at 20:49): 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?
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.
Nicolò Cavalleri (Jul 01 2021 at 10:27):Do you know what is it due to?
Mathias Fleury (Jul 01 2021 at 10:28):if we would know, we would all have fixed the problems on our machines…
Nicolò Cavalleri (Jul 01 2021 at 10:32):Well maybe the reason was known but there was not easy fix to it...
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.
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.
Nicolò Cavalleri (Jul 01 2021 at 10:36):Ok thanks! What does "base sessions" means?
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?).
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.
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.
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
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
Mathias Fleury (Jul 01 2021 at 11:53):the sessions are compiled
Last updated: Apr 16 2024 at 08:18 UTC