Stream: Beginner Questions

Topic: Command "imports" does not end


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Sep 25 2022 at 23:25 UTC