[isabelle-dev] Mira settings
krauss at in.tum.de
Sat Sep 29 00:49:15 CEST 2012
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.
> After the discussion with Alex several weeks ago I also added a tiny
> backdoor for ISABELLE_IDENTIFIER here:
> 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...
More information about the isabelle-dev