[isabelle-dev] isabelle test failed

[Makarius]

On Thu, 20 Oct 2011, Account Isatest wrote:

> Test for platform at-poly-test failed. Log file attached.
> [...]
> 3:02:39 elapsed time, 3:11:31 cpu time, factor 1.04
> Logics HOL FAILED!
> ------------------- test FAILED --- Thu Oct 20 03:25:34 CEST 2011 --- macbroy21

Again the same failure.  Here are the relevant parts of the log:

Isabelle version: 3dd426ae6bea
Started at Thu Oct 20 00:22:55 CEST 2011 (polyml-5.4.2_x86-linux on macbroy21)
Running HOL-Proofs-Extraction ...
Linking /tmp/isabelle-isatest24752/Quickcheck_Narrowing893907/isabelle_quickcheck_narrowing ...
Linking /tmp/isabelle-isatest24752/Quickcheck_Narrowing893923/isabelle_quickcheck_narrowing ...

HOL-Predicate_Compile_Examples FAILED
(see also
/home/isatest/isabelle-at-poly-test/heaps/polyml-5.4.2_x86-linux/log/HOL-Pre
dicate_Compile_Examples)

      (unit ->
       int ->
       int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence)
      -> Proof.context -> Proof.context
   val put_dseq_result :
      (unit ->
       int -> int -> int * int -> term list DSequence.dseq * (int * int))
      -> Proof.context -> Proof.context
   val nrandom : int ref val no_higher_order_predicate : string list ref
   val function_flattening : bool ref val debug : bool ref end

*** Error (line 377 of "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"):
*** Value or constructor (instantiate_goals) has not been declared in 
structure Quickcheck
*** Error (line 381 of "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"):
*** Value or constructor (collect_results) has not been declared in 
structure Quickcheck
***


This problem might show up now, because I have updated Poly/ML SVN version 
behind the unofficial "polyml-5.4.2" quoted above.

Also note that raw stderr is for system log only, not user messages or 
side-effect of user command invocation.  So "Linking ..." should probably 
be directed to stdout in the shell script, such that 
Isabelle_System.bash_output could take care of it via regular writeln.


 	Makarius