Re: [isabelle-dev] Ordinary_Differential_Equations FAILED
Yes, you can commit freely to AFP-devel. Cheers, Gerwin On 31 Oct 2013, at 9:33 pm, Fabian Immler wrote: > Hi, > > complete_univ has been renamed to complete_UNIV in Isabelle 1a13325269c2 > (after the fork for the release). > I therefore assume that I can commit the relevant changes to afp-devel. > > Best, > Fabian > > > Am 31.10.2013 um 10:53 schrieb Florian Haftmann > : > >>> Ordinary_Differential_Equations FAILED >>> (see also >>> /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.1_x86-linux/log/Ordinary_Differential_Equations) >>> >>> sr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb>>> -dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb>>> pe1/public/amsfonts/cm/cmmi7.pfb>>> onts/cm/cmmi8.pfb>>> fb>>> texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb>>> s/type1/public/amsfonts/cm/cmr7.pfb>>> msfonts/cm/cmr8.pfb>>> 10.pfb>>> hare/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb>>> /fonts/type1/public/amsfonts/cm/cmsy7.pfb>>> blic/amsfonts/cm/cmti10.pfb>>> symbols/msbm10.pfb> >>> Output written on root.pdf (97 pages, 436697 bytes). >>> Transcript written on root.log. >>> >>> *** Unknown fact "complete_univ" (line 449 of >>> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Initial_Value_Problem.thy") >>> *** At command "using" (line 448 of >>> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Initial_Value_Problem.thy") >>> *** Unknown fact "complete_univ" (line 384 of >>> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Auxiliarities.thy") >>> *** At command "using" (line 384 of >>> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Auxiliarities.thy") >> >> This refers to Isabelle 6d0688ce4ee2 and AFP 2a0f81020af9 >> >> Any ideas? >> >> Florian >> >> -- >> >> PGP available: >> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de >> >> ___ >> 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 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 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] Ordinary_Differential_Equations FAILED
Hi, complete_univ has been renamed to complete_UNIV in Isabelle 1a13325269c2 (after the fork for the release). I therefore assume that I can commit the relevant changes to afp-devel. Best, Fabian Am 31.10.2013 um 10:53 schrieb Florian Haftmann : >> Ordinary_Differential_Equations FAILED >> (see also >> /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.1_x86-linux/log/Ordinary_Differential_Equations) >> >> sr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb>> -dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb>> pe1/public/amsfonts/cm/cmmi7.pfb>> onts/cm/cmmi8.pfb>> fb>> texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb>> s/type1/public/amsfonts/cm/cmr7.pfb>> msfonts/cm/cmr8.pfb>> 10.pfb>> hare/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb>> /fonts/type1/public/amsfonts/cm/cmsy7.pfb>> blic/amsfonts/cm/cmti10.pfb>> symbols/msbm10.pfb> >> Output written on root.pdf (97 pages, 436697 bytes). >> Transcript written on root.log. >> >> *** Unknown fact "complete_univ" (line 449 of >> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Initial_Value_Problem.thy") >> *** At command "using" (line 448 of >> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Initial_Value_Problem.thy") >> *** Unknown fact "complete_univ" (line 384 of >> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Auxiliarities.thy") >> *** At command "using" (line 384 of >> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Auxiliarities.thy") > > This refers to Isabelle 6d0688ce4ee2 and AFP 2a0f81020af9 > > Any ideas? > > Florian > > -- > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > > ___ > 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
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
[isabelle-dev] Ordinary_Differential_Equations FAILED
> Ordinary_Differential_Equations FAILED > (see also > /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.1_x86-linux/log/Ordinary_Differential_Equations) > > sr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb> -dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb> pe1/public/amsfonts/cm/cmmi7.pfb> onts/cm/cmmi8.pfb> fb> texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb> s/type1/public/amsfonts/cm/cmr7.pfb> msfonts/cm/cmr8.pfb> 10.pfb> hare/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb> /fonts/type1/public/amsfonts/cm/cmsy7.pfb> blic/amsfonts/cm/cmti10.pfb> symbols/msbm10.pfb> > Output written on root.pdf (97 pages, 436697 bytes). > Transcript written on root.log. > > *** Unknown fact "complete_univ" (line 449 of > "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Initial_Value_Problem.thy") > *** At command "using" (line 448 of > "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Initial_Value_Problem.thy") > *** Unknown fact "complete_univ" (line 384 of > "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Auxiliarities.thy") > *** At command "using" (line 384 of > "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Auxiliarities.thy") This refers to Isabelle 6d0688ce4ee2 and AFP 2a0f81020af9 Any ideas? 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
