Dear Isabelle users,
I tried to import
HOL-Analysis.Analysis, but it didn't succeed. The import process remained stuck for about a half day long. Here is the script.
theory Scratch imports Main "HOL-Analysis.Analysis" begin end
Does anyone know a workaround?
I use Isabelle/jEdit for Isabelle2021 on macOS Big Sur (ver. 11.5.2). The PC is MacBook Air (13-inch, Mid 2013):
For what it's worth, importing
HOL-Analysis.Convex worked fine.
I am suspecting that your laptop memory could be the limiting factor for loading
HOL-Analysis directly. FYI, I am using 15' 2016 MacBook Pro with 4 cores and 16GB RAM, and still feels that the memory is not enough when editing large theories. A trick here is to start from the HOL-Analysis heap image (rather than HOL) to reduce the memory usage. The instruction is to select
HOL-Analysis in the
theory tab on the right-most part of the jEdit interface: image.png, and then restart Isabelle.
Dear Wenda Li,
Thank you for the reply. I followed your advice, and succeeded in importing
HOL-Analysis! (After I restarted the Isabelle, Isabelle Build process lasted for a few hours, but successfully finished.) I really appreciate your help.
Last updated: Dec 07 2023 at 20:16 UTC