[isabelle-dev] Mira settings

[Alexander Krauss]

On 09/25/2012 08:04 PM, Florian Haftmann wrote:
> Maybe it is high time now to version the mira settings also in the
> config-tum repository and forget about the old templates entirely –

This would be a big improvement. I'll happily follow any convention that 
you set up.

Makarius wrote:
> After the discussion with Alex several weeks ago I also added a tiny
> backdoor for ISABELLE_IDENTIFIER here:
> http://isabelle.in.tum.de/repos/isabelle/file/a4893c509aa2/etc/settings#l99
> This should allow Mira to provide its own isolated ISABELLE_HOME
> location to run tests in isolation from any other version, without
> further ado.

This is an unrelated topic. Here, my main concern is that 
ISABELLE_HOME_USER will still be hardwired under .isabelle/..., just in 
a subdirectory whose name I can choose. However, a mira build should 
generally not have any side effects outside its build directory, so it 
does not solve my problem. However, the hack required is not that big, 
so I am ok with the current state of affairs.

The main thing where mira is lagging behind is that it still relies on 
old contrib_devel. This is not so easy, since I do not want to reinstall 
components on every build. But using a central location raises 
concurrency issues and requires at least some basic locking...


Alex