Re: [isabelle-dev] AFP http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/563de86630d9

2011-10-15 Thread Florian Haftmann
Hi Lukas, > The issue can be observed at > > http://isabelle.in.tum.de/reports/Isabelle/report/5497697969e943bda524c4b01be7d12e > > Checking that the generated code in the Depth-First-Search AFP entry > actually compiles with ML is a minor point anyway, so I did not dig into > the details, but r

Re: [isabelle-dev] AFP http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/563de86630d9

2011-10-13 Thread Lukas Bulwahn
On 10/13/2011 10:52 AM, Florian Haftmann wrote: Hi Lukas, »removing checking of generated code because it fails on the mira testing infrastructure due to a missing Pure image« – I don't quite understand this. Why exactly is the check failing? Florian The issue can be observed at htt

[isabelle-dev] AFP http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/563de86630d9

2011-10-13 Thread Florian Haftmann
Hi Lukas, »removing checking of generated code because it fails on the mira testing infrastructure due to a missing Pure image« – I don't quite understand this. Why exactly is the check failing? Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-