On Sat, 17 Jan 2015, Account Isatest wrote:
Test for platform mac-poly-M2 failed. Log file attached.
[...]
Unfinished session(s): Codegen, Codegen_Basics
Finished at Sat Jan 17 04:34:07 CET 2015
2:52:32 elapsed time, 5:48:49 cpu time, factor 2.02
I have repaired this already in Isabelle/4a0b34ef0563.
The Codegen setup seems to keep around persistent ISABELLE_TMP files for
its examples, but that directory is meant to be empty in the end.
Violating this assumption leads results in the following warning:
Running Codegen ...
rmdir: failed to remove ‘/tmp/isabelle-makarius8953’: Directory not empty
and remaining garbage in the file-system.
What is the idea behind these temporary examples? Could it be done
somewhere in $ISABELLE_HOME_USER/tmp (which is a singleton place for the
user)?
It is also thinkable to reform the policy of ISABELLE_TMP cleanup, and do
it more aggresively like Isabelle_System.with_tmp_dir with rm_tree.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
