Marco David (Jan 26 2022 at 17:06): Marco David (Jan 26 2022 at 17:06):Why does Isabelle have to "recompile" the HOL library every time when I import theories like HOL-Number_Theory.Number_Theory? I understand for this behavior for the AFP, but why don't the sessions of type HOL-<Name> behave exactly like HOL itself and are ready-to-use?
Lukas Stevens (Jan 26 2022 at 17:09):You can achieve what you want by launching jedit with the the option -l HOL-Number_Theory or by basing your session on HOL-Number_Theory by modifying your ROOT file.
Lukas Stevens (Jan 26 2022 at 17:10):Of course, you can base your session on any other session including AFP sessions.
Mathias Fleury (Jan 26 2022 at 17:10):Graphically, you can do than in the theory panel of Isabelle/jEdit.
Mathias Fleury (Jan 26 2022 at 17:11):But I am a big fan of the -R option
Marco David (Jan 26 2022 at 17:14):What is the difference between -R and -l? The isabelle jedit --help explanation of -l reads "logic session name" which is not clear to me.
Mathias Fleury (Jan 26 2022 at 17:16):isabelle jedit -l HOL-Number_Theory vs isabelle jedit -R my_session
Mathias Fleury (Jan 26 2022 at 17:17):Requires a ROOT file for your project however.
Lukas Stevens (Jan 26 2022 at 17:19):Basically -l chooses one of the predefined "logic" sessions to base your interactive session on while -R pre-builds all sessions that your session depends on as defined in your ROOT file.
Marco David (Jan 26 2022 at 17:20):Thanks!
Notification Bot (Jan 26 2022 at 17:20):Marco David has marked this topic as resolved.
Notification Bot (Feb 02 2022 at 17:31):Marco David has marked this topic as unresolved.
Marco David (Feb 02 2022 at 17:34):Actually, a follow-up question. I've managed to launch Isabelle with isabelle jedit -d . -R My_Session but the wanted sessions are only pre-compiled if they are the parent of my session, not if they are simply included via the sessions command. More precisely, I have a file like
session My_Session = "HOL-Computational_Algebra" +
...
sessions
"HOL-Number_Theory"
and on the above command, only computational algebra is pre-compiled. Is this intended?
Marco David (Feb 02 2022 at 17:41):I found the answer myself: I only specified the top-level theory file in the ROOT file under theories, but this theory file did not properly import those lower-level theories that depend on HOL-Number_Theory. Hence, Isabelle/jEdit was just being efficient by not building sessions that are not imported anyhow.
Notification Bot (Feb 02 2022 at 17:44):Marco David has marked this topic as resolved.
Last updated: Apr 19 2024 at 20:15 UTC