[isabelle-dev] isabelle test failed -- HOL-Library-Codegenerator_Test

[Makarius]

On Mon, 2 Apr 2012, isatest at macbroy28.informatik.tu-muenchen.de wrote:

> macbroy28
> Isabelle version: 4c7548e7df86
> Started at Mon Apr  2 00:24:47 CEST 2012 (polyml-5.3.0_x86-linux on ...
>
> HOL-Library-Codegenerator_Test FAILED
>
> ROOT.scala:7920: warning: match is not exhaustive!
> missing combination          Coset
>
> def pred_of_set[A](x0: set[A]): pred[A] = x0 match {
>                                           ^
> ROOT.scala:8130: warning: match is not exhaustive!
> missing combination          Coset             *
>
> def infi[A, B : complete_lattice](x0: set[A], f: A => B): B = (x0, f) 
> match
> {
>                                                               ^
> warning: there were unchecked warnings; re-run with -unchecked for 
> details
> 45 warnings found
> Loading theory "Generate"
> > val it = () : unit
> val commit = fn : unit -> bool
> /mnt/home/isatest/isadist/Isabelle_02-Apr-2012/lib/scripts/run-polyml: 
line 77: 27590 Killed                  "$POLY" -q $ML_OPTIONS
> *** Code check failed for SML: "$ISABELLE_PROCESS" -r -q -u Pure
> *** At command "export_code" (line 17 of "~~/src/HOL/Codegenerator_Test/Generate.thy")

Does anybody understand this failure of isatest?  The process is 
terminated after many hours.

I've tried to reproduce it by hand, loading 
Codegenerator_Test/Generate.thy into HOL-Library.  It works for 
polyml-5.4.1_x86_64-darwin and polyml-5.4.1_x86-darwin, but 
polyml-5.3.0_x86-darwin does not seem to terminate.

Any ideas?


 	Makarius