[isabelle-dev] isabelle test failed

[Florian Haftmann]

>> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150119/372b5a01/attachment.sig>