Andrea Vezzosi (Jun 13 2023 at 08:43): Andrea Vezzosi (Jun 13 2023 at 08:43):Hi, it looks like whenever I close and reopen jEdit it spends a significant amount of time loading imported theories from the HOL session which my own session is built on. Is this expected, or am I having some caching issues?
Emin Karayel (Jun 13 2023 at 08:51):Hi Andrea,
Assuming the theories are in the AFP, it is possible to switch to a different logic base (that contains some of your dependencies). There is a drop-down in the theories panel, where you can switch to one that is better suited.
Screenshot-from-2023-06-13-10-48-18.png
Once you switch, you need to restart jedit. And the first launch will be slow. But the subsequent ones should be faster.
Manuel Eberl (Jun 13 2023 at 09:35):The HOL session is prebuilt and chosen as the default logic, so I doubt the theories in question really are from the HOL session, unless you switch to e.g. Pure as a default session (which I think is not something people do by accident normally). What theories are you talking about, exactly?
Andrea Vezzosi (Jun 13 2023 at 10:11):things like HOL/Computational_Algebra/Factorial_Ring.thy
Manuel Eberl (Jun 13 2023 at 10:38):That's not part of the HOL session, that's part of HOL-Computational_Algebra. So you ought to choose that as a base session.
Manuel Eberl (Jun 13 2023 at 10:38):You can e.g. launch Isabelle/JEdit with isabelle jedit -l HOL-Computational_Algebra to achieve that.
Manuel Eberl (Jun 13 2023 at 10:39):Note however that theories thus loaded are not explorable interactively, e.g. you cannot "ctrl + click" on things, which can be a bit annoying.
Manuel Eberl (Jun 13 2023 at 10:40):Generally speaking, most subdirectories in the HOL directory contain a separate child session of HOL and it usually makes sense to use that session (or one of its child sessions) as you base sessions if you work with them. The exception being things like HOL-Library, which contains a lot of very diverse, disconnected material, so it rarely makes sense to build on the HOL-Library session image.
Andrea Vezzosi (Jun 13 2023 at 10:49):Thanks, that seems to work.
Last updated: Dec 21 2024 at 16:20 UTC