[isabelle-dev] Concerning AFP 2a0f81020af9
In thys/JinjaThreads/Examples/ApprenticeChallenge.thy: export_code ApprenticeChallenge_annotated exec_J_rr J2JVM Apprentice main Null exec_JVM_rr in SML module_name JT file /tmp/NEW ^^ This is definitely not nice, especially in a shared environment like the NFS at TUM where currently lxbroy10:/tmp/NEW is blocked. What is the intention of this? A mere check could be done also export_code … checking or at least referring to $ISABELLE_TMP_PREFIX. 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
Re: [isabelle-dev] Concerning AFP 2a0f81020af9
The whole export_code - block can be removed, I'll do it in afp-devel, Thanks. but someone has to remove it in the snapshot. What is »the snapshot« in this context? The develepment snapshot on http://afp.sourceforge.net/download.shtml is volatile. 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
Re: [isabelle-dev] Concerning AFP 2a0f81020af9
On Do, 2013-10-31 at 10:57 +0100, Florian Haftmann wrote: The whole export_code - block can be removed, I'll do it in afp-devel, Thanks. but someone has to remove it in the snapshot. I meant the release branch of AFP, that Gerwin made a few days ago. See also: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-October/004787.html What is »the snapshot« in this context? The develepment snapshot on http://afp.sourceforge.net/download.shtml is volatile. Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev