[isabelle-dev] unable to start Isabelle/jEdit due to error in unused session

[Lars Hupel]

Dear Chris,

> 2) or there was some easy way (e.g., a flag) to exclude specific
> Isabelle components / sessions / ROOT files from checks (without having
> to edit "etc/settings").

I believe I have a solution for this problem.

For a while now, I've been using a custom Isabelle "launcher" based on
libisabelle [0]. It can be downloaded as a shell script [1]. It acts as
a wrapper for the regular Isabelle tool launcher. The twist is that it
supports on-the-fly registration of components.

In my setup, I've defined these two aliases:

alias isabelle='isabellectl --version 2016-1 --internal --afp --user
/home/lars exec'
alias isabelle-dev='isabellectl --devel --internal --component
/home/lars/work/afp --user /home/lars --home /home/lars/work/isabelle exec'

I can launch Isabelle by typing

$ isabelle jedit ...

or

$ isabelle-dev jedit ...

Note that additional arguments passed to the Isabelle tool need to be
separated by "--", as is standard practice in command-line environments:

$ isabelle-dev jedit -- -d . -l HOL-Library

But you can also pass in more components:

$ isabelle-dev --component /path/to/isafor jedit -- -l IsaFoR

Same thing works for using the stable version.

There are two caveats here:

- If you use the launcher for a stable Isabelle version, it'll download
a fresh copy to your home directory (Linux: "~/.local/share").
- The launcher claims control over your
"$ISABELLE_HOME_USER/etc/components" file. If you already have one, you
need to either delete it, or specify a different "--user" setting in the
alias.

This should work pretty much "out of the box" on Linux and OS X. No
guarantees on Windows.  You might also want to pass "--verbose" to get
informed about what is happening.

Cheers
Lars


[0] <https://github.com/larsrh/libisabelle>
[1] <https://dl.bintray.com/larsrh/libisabelle/nightly/isabellectl>