[isabelle-dev] isabelle test failed

[Lukas Bulwahn]

The failure is intended to be fixed with changeset 66ba67adafab and was 
related to changes in 3f1d1ce024cb.

Lukas


On 10/20/2011 12:19 PM, Makarius wrote:
>  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
>  _______________________________________________
>  isabelle-dev mailing list
>  isabelle-dev at in.tum.de
>  https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>