[isabelle-dev] [Fwd: doc test failed]

2011-02-06 Thread Tobias Nipkow
Seit Wochen wenn nicht Monaten bekomme ich alle paar Tage diese Fehlermeldung: Running ZF-IsarRef ... Unknown logic ZF -- no heap file found in: /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux /mnt/home/isatest/isadist/Isabelle_06-Feb-2011/heaps/polyml-5.2_x86-linux ZF-IsarRef

Re: [isabelle-dev] [Fwd: doc test failed]

2011-02-06 Thread Alexander Krauss
(please keep postings to isabelle-dev in English) Tobias Nipkow wrote: Seit Wochen wenn nicht Monaten bekomme ich alle paar Tage diese Fehlermeldung: More precisely, the error occurs (almost) daily since January 11th, according to my email archive. Fuehlt sich hier jemand zustaendig? So

Re: [isabelle-dev] [Fwd: doc test failed]

2011-02-06 Thread Tobias Nipkow
Yes, the missing ZF image is to be the problem. For some reason that has changed, as Slawomir Kolodynski also noticed. So we should either build ZF again or stop that test. Tobias Alexander Krauss schrieb: (please keep postings to isabelle-dev in English) Tobias Nipkow wrote: Seit Wochen

Re: [isabelle-dev] [Fwd: doc test failed]

2011-02-06 Thread Makarius
On Sun, 6 Feb 2011, Tobias Nipkow wrote: Yes, the missing ZF image is to be the problem. For some reason that has changed, as Slawomir Kolodynski also noticed. So we should either build ZF again or stop that test. What Slawomir has noticed is merely the lack of ZF in official Isabelle2011,

Re: [isabelle-dev] Variable ?n has two distinct types

2011-02-06 Thread Makarius
On Sun, 6 Feb 2011, Gerwin Klein wrote: I've managed to get the following error message with Isabelle2011 when running simp: *** exception TYPE raised (line 109 of envir.ML): Variable ?n has two distinct types *** At command apply (line 14 of /Users/kleing/Simp.thy) The end of the

Re: [isabelle-dev] HOL/Word

2011-02-06 Thread Florian Haftmann
Hi Gerwin, Is anyone prepared to leak Florian's new email address so I may haunt him? I am prepared to be haunted ;-), I am still on the users and dev mailing list and will follow them following the walrus strategy (only dive up instantly if you think it is necessary). First, a quick and dirty

Re: [isabelle-dev] HOL/Word

2011-02-06 Thread Gerwin Klein
Hi Florian, On 07/02/2011, at 2:10 AM, Florian Haftmann wrote: Is anyone prepared to leak Florian's new email address so I may haunt him? I am prepared to be haunted ;-), I am still on the users and dev mailing list and will follow them following the walrus strategy (only dive up