Yosuke Ito (Sep 12 2021 at 03:03): Yosuke Ito (Sep 12 2021 at 03:03):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.
Wenda Li (Sep 13 2021 at 06:17):Dear Yosuke,
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.
Yosuke Ito (Sep 14 2021 at 13:01):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 21 2024 at 16:20 UTC