Stream: General

Topic: Building a heap image for a built-in theory

view this post on Zulip Gergely Buday (Nov 22 2023 at 11:40):

I want to build a heap image for the Option theory. I created a ROOT file to define a session for it:

session "Option" = "HOL" +
  theories [document = false]
    "~~/src/HOL/Option"

What is the isabelle command to build the heap upon this? I tried

$ isabelle jedit -l Option

but jEdit said the session Option is undefined

I called this from the directory where my ROOT file is.

view this post on Zulip Gergely Buday (Nov 22 2023 at 12:00):

Next I tried this ROOT file:

session "option" = HOL +
  theories [document = false]
    "~~/src/HOL/Option"

but for

$ isabelle jedit -d . -l option

I get

Implicit use of directory "/home/gergelybuday/Isabelle2023/src/HOL" for theory "option.HOL"
Implicit use of directory "/home/gergelybuday/Isabelle2023/src/HOL" for theory "option.Orderings"
Implicit use of directory "/home/gergelybuday/Isabelle2023/src/HOL" for theory "option.Groups"
...
Implicit use of directory "/home/gergelybuday/Isabelle2023/src/HOL" for theory "option.Option"
Implicit use of session directories: "/home/gergelybuday/Isabelle2023/src/HOL"
The error(s) above occurred in session "option" (line 1 of "/home/gergelybuday/gergelyphd/projects/monads/option/ROOT")

How should I do this correctly?

view this post on Zulip Wolfgang Jeltsch (Nov 22 2023 at 12:02):

Isn’t Option already part of HOL, from which you start?

view this post on Zulip Gergely Buday (Nov 22 2023 at 12:04):

Wolfgang Jeltsch said:

Isn’t Option already part of HOL, from which you start?

My original problem was this: I imported Option and Isabelle processed the background theories a lot, so I could not work on my theory. Should I build an image for HOL? I guess isabelle jedit starts with that by default, doesn't it?

view this post on Zulip Wolfgang Jeltsch (Nov 22 2023 at 12:07):

Yes, it does. Therefore, I don’t know what processing took place in your case.

view this post on Zulip Gergely Buday (Nov 22 2023 at 12:09):

I think I have found the culprit: I imported ~~/src/HOL/Option instead of simply Main.

view this post on Zulip Wolfgang Jeltsch (Nov 22 2023 at 12:14):

Hmm, still I don’t understand why Isabelle is not using the heap image in this case, but, then again, I don’t understand these technical details of Isabelle very well. In any case, you should always import Main first (directly or indirectly by importing a theory first about which you know that it imports Main first).

view this post on Zulip Mathias Fleury (Nov 22 2023 at 12:58):

I think that it is because you are writing a path instead of HOL.Option

Last updated: May 02 2024 at 04:18 UTC