On 04/22/2012 03:04 PM, Florian Haftmann wrote:
I've managed to remove more than 5 GB of old heap files, but this might
be a bit pathethic due to this directory:
225G tmp/shared_results
Does anybody know what it is?
These are the results from the mira runs, which in theory are kept
eternally. There is the mira command »purge« which throws them away
except the most recent ones (however the heuristic is). I personally
don't have any intimate knowledge about the mira setup at TUM any longer
and am reluctant to risk something, so I kindly ask for action from the
current mira administrators at TUM.
Best,
Florian
We manually purge the results when we get close to the quota.
This is now been done just a moment ago.
Supposingly our quota is monitored, and we should get email
notifications, however I have not seen any lately.
Lukas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
