Minh D (Feb 07 2024 at 13:18): Minh D (Feb 07 2024 at 13:18):When I was trying to open an AFP entry (Automated Stateful Protocol Verification) by:
isa23 -d ./afp-2023/thys/Automated_Stateful_Protocol_Verification -l HOL-Eisbach -l Stateful_Protocol_Composition_and_Typing ./afp-2023/thys/Automated_Stateful_Protocol_Verification/Eisbach_Protocol_Verification.thy
Although I have already built the heap image for both HOL-Eisbach and Stateful_Protocol_Composition_and_Typing, both of them appear in
~/.isabelle/Isabelle2023/heaps/polyml-5.9_x86_64_32-linux/
There was still a message saying "Bad parent session "Stateful_Protocol_Composition_and_Typing" for "Automated_Stateful_Protocol_Verification" ".
I am wondering why is it the case, and what is the correct way to open a session with a prebuilt parent session image like this? I am using Ubuntu 22.04 if that helps.
Fabian Huch (Feb 07 2024 at 13:22):-l twice just overwrites the first again -A: does that for all AFP sessions. Minh D (Feb 07 2024 at 13:29):Fabian Huch said:
- You can only have one base logic - specifying
-ltwice just overwrites the first again- You need to add the sessions to your namespace. using
-A:does that for all AFP sessions.
In the above command, I was specifying -l for Stateful_Protocol_Composition_and_Typing after the HOL-Eisbach, so according to overwriting rule, shouldn't the message be for HOL-Eisbach instead?
Also when I try remove one of them (remove the -l HOL-Eisbach) and use -A:
, the problem is still there.
Minh D (Feb 07 2024 at 13:51):Fabian Huch said:
- You can only have one base logic - specifying
-ltwice just overwrites the first again- You need to add the sessions to your namespace. using
-A:does that for all AFP sessions.
Oh I was missing something, I used isabelle jedit, not isabelle build
Mathias Fleury (Feb 07 2024 at 13:52):Stateful_Protocol_Composition_and_Typing is in the AFP, but not in any path you have added with -d
Mathias Fleury (Feb 07 2024 at 13:53):Please install the AFP with the instruction from https://www.isa-afp.org/help/ then there is no -d problem anymore
Minh D (Feb 07 2024 at 13:54):Mathias Fleury said:
Stateful_Protocol_Composition_and_Typingis in the AFP, but not in any path you have added with-d
I have the heap image for Stateful_Protocol_Composition_and_Typing in my ~/.isabelle/Isabelle2023/heaps/polyml-5.9_x86_64_32-linux/, would that make any difference?
Fabian Huch (Feb 07 2024 at 14:00):No.
Fabian Huch (Feb 07 2024 at 14:16):Fabian Huch said:
- You can only have one base logic - specifying
-ltwice just overwrites the first again
2. You need to add the sessions to your namespace. usingSince this appears to be-A:does that for all AFP sessions.isabelle jedit, you simply need to install the AFP as stated on the help page.
Minh D (Feb 07 2024 at 15:02):I got it to run, thank you both. By the way, what should be the right process to build the image for parent sessions, and then open jedit, with the already built image so that I don't have to load all parent sessions' theory files again every time I open the theory?
Mathias Fleury (Feb 07 2024 at 15:05):Isabelle/jEdit caches the built image…
Fabian Huch (Feb 07 2024 at 15:11):You simply need to start jEdit with the right base logic (-l). However, you can only have a single base logic, so you need to decide on one and re-load all needed theory files from the other. In your case, using Stateful_Protocol_Composition_and_Typing as a base logic should be fast (HOL-Eisbach is tiny so loading those theory files in should not take long).
Fabian Huch (Feb 07 2024 at 15:12):If you depend on multiple larger sessions then I would create a single parent session that depends on all of them and build a heap image for that parent session.
Minh D (Feb 07 2024 at 23:01):Thanks, that teaches me a lot on how to use Isabelle
Mathias Fleury (Feb 08 2024 at 08:36):Fabian Huch said:
If you depend on multiple larger sessions then I would create a single parent session that depends on all of them and build a heap image for that parent session.
That is not necessary anymore I think. You have a root file for your current project and put the sessions to import as "sessions" in the ROOT file, then they are already included.
Yong Kiam (Feb 08 2024 at 08:39):may I know how you produce a heap with this approach? do you just -l the ROOT for your current project?
Mathias Fleury (Feb 08 2024 at 08:46):I just -l ROOT it
Fabian Huch (Feb 08 2024 at 08:57):Mathias Fleury said:
Fabian Huch said:
If you depend on multiple larger sessions then I would create a single parent session that depends on all of them and build a heap image for that parent session.
That is not necessary anymore I think. You have a root file for your current project and put the sessions to import as "sessions" in the ROOT file, then they are already included.
What do you mean with 'included'? If I have two large sessions A and B and want to work on C that needs both, which heap image can I build so I don't have to re-load any theories from A and B while working on C?
Mathias Fleury (Feb 08 2024 at 12:49):Isabelle/jEdit -l MyProject will compile all required imports, but I do not know how it works internally
Fabian Huch (Feb 08 2024 at 13:25):If you build the logic image for the whole project (here -l C) then that image contains everything, but then you can't edit C. Or am I missing something?
Fabian Huch (Feb 08 2024 at 13:26):Maybe we were talking past each other here.
Mathias Fleury (Feb 08 2024 at 14:25):Ahh no you are right: I meant Isabelle/jEdit -R MyProject
Fabian Huch (Feb 08 2024 at 14:45):Ah yes that actually works, great - I didn't know it did this automatically!
Last updated: Apr 27 2024 at 20:14 UTC