On Wed, 4 Jun 2014, Lars Noschinski wrote:
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?
Is this question still open? I have lost track of the various Mira
configuration problems.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
