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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
