[isabelle-dev] Fwd: status (AFP)
Hi all, JinjaThreads currently probably fails because of the changeset 6e422d180de8 (http://isabelle.in.tum.de/repos/isabelle/rev/6e422d180de8) *** empty result sequence -- proof command failed *** At command "apply" (line 2941 of "/home/kleing/afp/devel/thys/JinjaThreads/Compiler/JVMJ1.thy") val it = (): unit Exception- TOPLEVEL_ERROR raised *** ML error I could not even inspect the proof state where it fails, as my machine is not able to load the theory. If anyone here has an educated guess how this proof can be fixed, you should try. There are at least two machines, lxbroy10 in Munich, and one in Australia, running regularly that can check these guesses once you push them. Lukas Original Message Subject:status (AFP) Date: Fri, 21 Oct 2011 06:31:55 +1100 From: Gerwin Klein To: undisclosed-recipients:; The status of the following AFP entries changed or remains FAIL: [JinjaThreads] is still on FAIL. Full entry status athttp://afp.sourceforge.net/status.shtml AFP version: development -- hg id a98f0ac6930a Isabelle version: devel -- hg id c4fab1099cd0 Test ended on: lemma, Fri Oct 21 06:31:55 EST 2011. Have a nice day, isatest ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] QuickCheck interface question
Hi, I'm currently updating IsaPlanner and IsaCoSy to Isabelle2011-1. I noticed there are some changes to the QuickCheck interface: The function test_term now takes an extra first argument of type compile_generator. What is this thing an how do I create one? Or even better, is there a default one? I noticed that test_terms (in plural) curiously does not take this extra argument. Best, Moa ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle test failed
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle test failed
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
