chem snu (Jun 20 2025 at 19:05): chem snu (Jun 20 2025 at 19:05):I built HOL-Analysis with isabelle build HOL-Analysis, but after that, when I build my own session depending on HOL-Analysis, it builds HOL-Analysis again. Why?
In the first place, why should we, end users, build these libraries?
Mathias Fleury (Jun 20 2025 at 19:19):You can specify the base session in Isabelle (either through jEdit or with -l when starting it)
Mathias Fleury (Jun 20 2025 at 19:19):in the theory panel, the dropbox
chem snu (Jun 20 2025 at 20:05):When I started jedit with -l "HOL-Analysis" option, jedit started to build HOL-Analysis and it took about 15 minutes. If I close jedit and open it again with the same option, then it starts without rebuilding HOL-Analysis. Fine.
After that, If I open jedit without -l option and set the base session to HOL-Analysis in the theory panel, it builds HOL-Analysis again...
I don't know what is going on...
Mathias Fleury (Jun 20 2025 at 20:08):It will do it only once
chem snu (Jun 20 2025 at 20:21):Maybe I'm asking a stupid question, but what I want to understand is,
Why sometimes isabelle doesn't reuse the heap which was obtained in previous build process?
When I opened jedit with -l "HOL-Analysis" option, we already obtained the heap.
But, as I already said, it rebuilds HOL-Analysis if I use theory panel to set the base session to HOL-Analysis. Why is this necessary?
I'm sorry if this is dumb question.
Mathias Fleury (Jun 20 2025 at 20:24):I am not sure. I actually use a different version: I create ROOT files and use -R to focus on the session. It is a bit more work (as you have to update the ROOT file when importing new sessions), but it is way nicer and you can start isabelle in any folder you want
Last updated: Jul 12 2025 at 12:41 UTC