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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
