2
$\begingroup$

I use Isabelle, and I have a theory that is processed for long interactively so I wanted to build a heap image. Therefore I created a ROOT file:

$ cat ROOT 
session MYTHEORY = HOL +
  description "The definition of my theory"
  theories [document = false]
    MyTheory

upon which I built an image:

$ isabelle build -c -D .
Cleaned MYTHEORY
Running MYTHEORY ...
Finished MYTHEORY (0:00:01 elapsed time)
0:00:03 elapsed time

and then I tried to use that heap image, but then I got an error message:

$ isabelle jedit -l MYTHEORY
16:51:07 [AWT-EventQueue-0] [error] ErrorListDialog$ErrorEntry: *** Undefined session(s): "MYTHEORY"

What did I wrong, what did I not understand?

Improve this question
$\endgroup$
1
  • $\begingroup$ I'm able to reproduce in an old version of Isabelle, I'll try the development one (I'm actually unable to re-build some old project of mine; once I find out I'll post an answer.) $\endgroup$
    – Pedro Sánchez Terraf
    Commented Feb 15 at 19:41

1 Answer 1

Reset to default
2
$\begingroup$

It seems that Isabelle/jEdit is not aware of this session that are proving. You can indicate that by feeding the directory where the session is stored:

$ isabelle jedit -d . -l MYTHEORY

assuming that the session lies (as it seems) in the present directory. (Note. This does not requires prior building.)

I'm trying to recall how did manage to avoid the -d . option, but in the meantime this might work for you.

EDIT. In order to make Isabelle aware of your session, you should add it as a component:

$ isabelle components -u /absolute/path/to/Session/

After that, you will be able to simply run isabelle jedit -l MYTHEORY.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.