>> 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)?
The generated matter is not interesting at all. It is just there since
the examples contain full-blown export_code statements. I will give it
another turn for experimentation.
> 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.
But the warning should persist since it reminds of a policy violation.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
