[isabelle-dev] Testboard problem

Lars Noschinski noschinl at in.tum.de
Wed Jun 4 16:39:54 CEST 2014

On 04.06.2014 13:37, Johannes Hölzl wrote:
> We remove ~isatest/.isabelle/heaps/.../HOL-Proofs on lxbroy10 and now it
> works...
> I don't know why mira is accessing this file, it actually sets up the
> settings file to _not_ look into the users heaps-directory. But it looks
> like there is a problem with this setup.
After looking a bit closer: Mira changes ISABELLE_HOME_USER (by
appending it to $ISABELLE_HOME/etc/settings). Of course, this is too
late to affect ISABELLE_PATH, which still refers to

So, we set $USER_HOME instead before starting Isabelle (see

@Makarius: Does this use fit the intention of USER_HOME?

More information about the isabelle-dev mailing list