Re: [isabelle-dev] Concerning AFP 2a0f81020af9
On 31 Oct 2013, at 9:04 pm, Peter Lammich wrote: > 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 Yes. I’ll move the patch over. Cheers, Gerwin signature.asc Description: Message signed with OpenPGP using GPGMail ___ 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
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
Oops, that was me! Sorry, it was a test of mine, that I obviously forgot to remove. The whole export_code - block can be removed, I'll do it in afp-devel, but someone has to remove it in the snapshot. -- Peter On Do, 2013-10-31 at 08:44 +0100, Florian Haftmann wrote: > 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 > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[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
