Pristine (Aug 03 2025 at 22:17): Pristine (Aug 03 2025 at 22:17):Hi everyone,
I'm experiencing a problem with my Isabelle setup. Previously, I was able to import theories like "HOL-Analysis.Analysis", "HOL-Analysis.Interval_Integral", "HOL-Probability.Distributions", and "HOL-Probability.Distribution_Functions" in my .thy files without any issues. My code hasn't changed at all.
But after restarting Isabelle, suddenly all these imports fail (showing Bad Theory errors). Sometimes the error messages even disappear after a while, but the imports are still not working.
Does anyone know what could cause this?
Why would these standard theories become unavailable after a restart, even though it worked before?
Any tips on how to debug or fix this would be much appreciated!
Thanks in advance!
Screenshot 2025-08-03 at 23.13.17.png
Mathias Fleury (Aug 04 2025 at 04:55):Why would these standard theories become unavailable after a restart, even though it worked before?
My guess: there are still here but these theories are now very slow to start because you changed the base session
Mathias Fleury (Aug 04 2025 at 04:56):So: do those theories appear in the theory panel?
Pristine (Aug 04 2025 at 19:09):I think you're right, after waiting for a long time, it worked.
Manuel Eberl (Aug 04 2025 at 19:14):Usually you build a session image for big sessions like HOL-Analysis or HOL-Probability to avoid this.
Last updated: Aug 13 2025 at 08:30 UTC