[isabelle-dev] Testboard problem

[Lars Noschinski]

On 04.07.2014 12:43, Makarius wrote:
> 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.
I have implemented this approach (i.e., Mira sets $USER_HOME to some
arbitrary place before starting Isabelle) and this seems to work. The
only open question is whether you see any problems in $HOME /= $USER_HOME.