[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
$USER_HOME/.isabelle/heaps.

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

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



More information about the isabelle-dev mailing list