Thanks to Dmitriy's effort, all AFP entries run successfully again.
-------- Original Message -------- Subject: status (AFP) Date: Fri, 21 Sep 2012 09:10:43 +0200 (CEST) From: [email protected] (Isabelle ) To: undisclosed-recipients:; The status of the following AFP entries changed or remains FAIL: [KBPs] changed from FAIL to ok. Full entry status at http://afp.sourceforge.net/status.shtml AFP version: development -- hg id c3a75d6d802a Isabelle version: devel -- hg id 7bb0d515ccbc Test ended on: macbroy2, Fri Sep 21 09:10:43 CEST 2012. Have a nice day, isatest
Stream-Fusion: ok Ramsey-Infinite: ok Binomial-Heaps: ok Ordinals_and_Cardinals: ok ClockSynchInst: ok Huffman: ok Completeness: ok Well_Quasi_Orders: ok Abstract-Hoare-Logics: ok Free-Boolean-Algebra: ok Stuttering_Equivalence: ok Girth_Chromatic: ok Valuation: ok FunWithFunctions: ok Coinductive: ok Heard_Of: ok Abstract-Rewriting: ok Matrix: ok POPLmark-deBruijn: ok MonoBoolTranAlgebra: ok FeatherweightJava: ok DiskPaxos: ok Free-Groups: ok Functional-Automata: ok GraphMarkingIBP: ok Transitive-Closure-II: ok Tycon: ok BytecodeLogicJmlTypes: ok Finger-Trees: ok WorkerWrapper: ok Separation_Algebra: ok General-Triangle: ok Program-Conflict-Analysis: ok LinearQuantifierElim: ok GenClock: ok Inductive_Confidentiality: ok Recursion-Theory-I: ok Efficient-Mergesort: ok BinarySearchTree: ok TLA: ok Lam-ml-Normalization: ok CoreC++: ok Marriage: ok Shivers-CFA: ok SATSolverVerification: ok Example-Submission: ok SumSquares: ok BDD: ok JiveDataStoreModel: ok Polynomials: ok Datatype_Order_Generator: ok Verified-Prover: ok Topology: ok KBPs: ok ArrowImpossibilityGS: ok Lazy-Lists-II: ok Locally-Nameless-Sigma: ok DataRefinementIBP: ok JinjaThreads: ok HRB-Slicing: ok DPT-SAT-Solver: ok RIPEMD-160-SPARK: ok Flyspeck-Tame: ok Regular-Sets: ok RSAPSS: ok LightweightJava: ok Gauss-Jordan-Elim-Fun: ok AVL-Trees: ok Category: ok AutoFocus-Stream: ok CofGroups: ok Perfect-Number-Thm: ok Depth-First-Search: ok Abortable_Linearizable_Modules: ok Statecharts: ok PseudoHoops: ok Max-Card-Matching: ok FunWithTilings: ok SenSocialChoice: ok CCS: ok List-Index: ok Markov_Models: ok Cauchy: ok Ordinal: ok Myhill-Nerode: ok Binomial-Queues: ok Fermat3_4: ok FOL-Fitting: ok MuchAdoAboutTwo: ok Slicing: ok Dijkstra_Shortest_Path: ok SIFPL: ok Presburger-Automata: ok Circus: ok Transitive-Closure: ok Impossible_Geometry: ok Category2: ok Integration: ok MiniML: ok NormByEval: ok PCF: ok SequentInvertibility: ok Pi_Calculus: ok FileRefinement: ok FFT: ok Robbins-Conjecture: ok Compiling-Exceptions-Correctly: ok Ordinary_Differential_Equations: ok VolpanoSmith: ok HotelKeyCards: ok Tree-Automata: ok FinFun: ok Psi_Calculi: ok Lower_Semicontinuous: ok
Start test for /home/isatest/afp/devel at Fri Sep 21 06:31:44 CEST 2012, macbroy2 begin hg pull/update pulling from ssh://[email protected]/hgroot/afp/afp searching for changes adding changesets adding manifests adding file changes added 1 changesets with 1 changes to 1 files 1 files updated, 0 files merged, 0 files removed, 0 files unresolved remote: Running preoutgoing hook remote: Use of uninitialized value in concatenation (.) or string at /etc/mercurial/preoutgoing line 36. end hg pull/update AFP version: development -- hg id c3a75d6d802a Isabelle version: devel -- hg id 7bb0d515ccbc Building HOLCF ... Finished HOLCF (0:00:50 elapsed time, 0:01:01 cpu time, factor 1.22) Building HOL-Nominal ... Finished HOL-Nominal (0:00:21 elapsed time, 0:00:23 cpu time, factor 1.09) Building HOL-Multivariate_Analysis ... Finished HOL-Multivariate_Analysis (0:03:00 elapsed time, 0:06:32 cpu time, factor 2.17) Building HOL-Word ... Finished HOL-Word (0:00:38 elapsed time, 0:01:07 cpu time, factor 1.76) Building Jinja ... Finished Jinja (0:05:48 elapsed time, 0:13:16 cpu time, factor 2.28) Building LatticeProperties ... Finished LatticeProperties (0:00:20 elapsed time, 0:00:22 cpu time, factor 1.10) Building HOL-Probability ... Finished HOL-Probability (0:01:43 elapsed time, 0:03:24 cpu time, factor 1.98) Building Group-Ring-Module ... Finished Group-Ring-Module (0:03:22 elapsed time, 0:07:08 cpu time, factor 2.11) Building Simpl ... Finished Simpl (0:02:35 elapsed time, 0:04:55 cpu time, factor 1.90) Building Collections ... Finished Collections (0:05:32 elapsed time, 0:08:31 cpu time, factor 1.53) Building Refine_Monadic ... Finished Refine_Monadic (0:01:51 elapsed time, 0:02:51 cpu time, factor 1.54) Building List-Infinite ... Finished List-Infinite (0:00:45 elapsed time, 0:01:18 cpu time, factor 1.73) Building Nat-Interval-Logic ... Finished Nat-Interval-Logic (0:00:50 elapsed time, 0:01:19 cpu time, factor 1.58) Running Flyspeck-Tame ... Finished Flyspeck-Tame (0:03:12 elapsed time, 0:06:10 cpu time, factor 1.92) Running JinjaThreads ... Finished JinjaThreads (0:57:08 elapsed time, 1:51:07 cpu time, factor 1.94) Running HRB-Slicing ... Finished HRB-Slicing (0:05:54 elapsed time, 0:14:39 cpu time, factor 2.48) Running Slicing ... Finished Slicing (0:05:38 elapsed time, 0:15:20 cpu time, factor 2.72) Running AVL-Trees ... Finished AVL-Trees (0:00:13 elapsed time, 0:00:31 cpu time, factor 2.38) Running Abstract-Hoare-Logics ... Finished Abstract-Hoare-Logics (0:00:13 elapsed time, 0:00:28 cpu time, factor 2.15) Running BDD ... Finished BDD (0:00:56 elapsed time, 0:02:14 cpu time, factor 2.39) Running BinarySearchTree ... Finished BinarySearchTree (0:00:05 elapsed time, 0:00:10 cpu time, factor 2.00) Running BytecodeLogicJmlTypes ... Finished BytecodeLogicJmlTypes (0:01:02 elapsed time, 0:02:23 cpu time, factor 2.30) Running CCS ... Finished CCS (0:00:21 elapsed time, 0:00:41 cpu time, factor 1.95) Running Category ... Finished Category (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.50) Running Category2 ... Finished Category2 (0:00:25 elapsed time, 0:00:54 cpu time, factor 2.16) Running Cauchy ... Finished Cauchy (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.66) Running Circus ... Finished Circus (0:01:12 elapsed time, 0:02:28 cpu time, factor 2.05) Running ClockSynchInst ... Finished ClockSynchInst (0:00:07 elapsed time, 0:00:13 cpu time, factor 1.85) Running CofGroups ... Finished CofGroups (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.16) Running Compiling-Exceptions-Correctly ... Finished Compiling-Exceptions-Correctly (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.33) Running Completeness ... Finished Completeness (0:00:17 elapsed time, 0:00:32 cpu time, factor 1.88) Running Depth-First-Search ... Finished Depth-First-Search (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.00) Running Dijkstra_Shortest_Path ... Finished Dijkstra_Shortest_Path (0:00:50 elapsed time, 0:01:12 cpu time, factor 1.44) Running DiskPaxos ... Finished DiskPaxos (0:00:25 elapsed time, 0:01:04 cpu time, factor 2.56) Running Example-Submission ... Finished Example-Submission (0:00:03 elapsed time, 0:00:03 cpu time) Running FFT ... Finished FFT (0:00:04 elapsed time, 0:00:07 cpu time) Running FOL-Fitting ... Finished FOL-Fitting (0:00:37 elapsed time, 0:00:46 cpu time, factor 1.24) Running FeatherweightJava ... Finished FeatherweightJava (0:00:16 elapsed time, 0:00:27 cpu time, factor 1.68) Running FileRefinement ... Finished FileRefinement (0:00:08 elapsed time, 0:00:14 cpu time, factor 1.75) Running FinFun ... Finished FinFun (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.66) Running Functional-Automata ... Finished Functional-Automata (0:00:15 elapsed time, 0:00:26 cpu time, factor 1.73) Running GenClock ... Finished GenClock (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.71) Running General-Triangle ... Finished General-Triangle (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.20) Running Huffman ... Finished Huffman (0:00:14 elapsed time, 0:00:23 cpu time, factor 1.64) Running Integration ... Finished Integration (0:00:10 elapsed time, 0:00:20 cpu time, factor 2.00) Running JiveDataStoreModel ... Finished JiveDataStoreModel (0:00:15 elapsed time, 0:00:25 cpu time, factor 1.66) Running KBPs ... Finished KBPs (0:01:51 elapsed time, 0:04:13 cpu time, factor 2.27) Running Lazy-Lists-II ... Finished Lazy-Lists-II (0:00:09 elapsed time, 0:00:12 cpu time, factor 1.33) Running LightweightJava ... Finished LightweightJava (0:00:47 elapsed time, 0:01:25 cpu time, factor 1.80) Running Lower_Semicontinuous ... Finished Lower_Semicontinuous (0:00:13 elapsed time, 0:00:21 cpu time, factor 1.61) Running MiniML ... Finished MiniML (0:00:13 elapsed time, 0:00:19 cpu time, factor 1.46) Running MonoBoolTranAlgebra ... Finished MonoBoolTranAlgebra (0:00:14 elapsed time, 0:00:15 cpu time, factor 1.07) Running MuchAdoAboutTwo ... Finished MuchAdoAboutTwo (0:00:15 elapsed time, 0:00:28 cpu time, factor 1.86) Running NormByEval ... Finished NormByEval (0:00:31 elapsed time, 0:01:02 cpu time, factor 2.00) Running Ordinal ... Finished Ordinal (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.50) Running POPLmark-deBruijn ... Finished POPLmark-deBruijn (0:00:23 elapsed time, 0:00:51 cpu time, factor 2.21) Running Pi_Calculus ... Finished Pi_Calculus (0:01:21 elapsed time, 0:03:02 cpu time, factor 2.24) Running PseudoHoops ... Finished PseudoHoops (0:01:38 elapsed time, 0:02:01 cpu time, factor 1.23) Running Psi_Calculi ... Finished Psi_Calculi (0:06:04 elapsed time, 0:15:55 cpu time, factor 2.62) Running RIPEMD-160-SPARK ... Finished RIPEMD-160-SPARK (0:00:22 elapsed time, 0:00:39 cpu time, factor 1.77) Running RSAPSS ... Finished RSAPSS (0:00:23 elapsed time, 0:00:54 cpu time, factor 2.34) Running Ramsey-Infinite ... Finished Ramsey-Infinite (0:00:08 elapsed time, 0:00:10 cpu time, factor 1.25) Running Recursion-Theory-I ... Finished Recursion-Theory-I (0:00:20 elapsed time, 0:00:40 cpu time, factor 2.00) Running SATSolverVerification ... Finished SATSolverVerification (0:01:16 elapsed time, 0:03:07 cpu time, factor 2.46) Running Separation_Algebra ... Finished Separation_Algebra (0:00:20 elapsed time, 0:00:38 cpu time, factor 1.90) Running Stream-Fusion ... Finished Stream-Fusion (0:00:16 elapsed time, 0:00:20 cpu time, factor 1.25) Running Topology ... Finished Topology (0:00:15 elapsed time, 0:00:28 cpu time, factor 1.86) Running Tycon ... Finished Tycon (0:00:14 elapsed time, 0:00:26 cpu time, factor 1.85) Running Valuation ... Finished Valuation (0:00:42 elapsed time, 0:01:26 cpu time, factor 2.04) Running Verified-Prover ... Finished Verified-Prover (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.50) Running CoreC++ ... Finished CoreC++ (0:01:08 elapsed time, 0:02:35 cpu time, factor 2.27) Running VolpanoSmith ... Finished VolpanoSmith (0:00:15 elapsed time, 0:00:20 cpu time, factor 1.33) Running LinearQuantifierElim ... Finished LinearQuantifierElim (0:01:20 elapsed time, 0:02:35 cpu time, factor 1.93) Running Girth_Chromatic ... Finished Girth_Chromatic (0:00:58 elapsed time, 0:01:52 cpu time, factor 1.93) Running Presburger-Automata ... Finished Presburger-Automata (0:00:27 elapsed time, 0:00:58 cpu time, factor 2.14) Running Tree-Automata ... Finished Tree-Automata (0:04:14 elapsed time, 0:07:43 cpu time, factor 1.82) Running Abortable_Linearizable_Modules ... Finished Abortable_Linearizable_Modules (0:00:32 elapsed time, 0:01:17 cpu time, factor 2.40) Running ArrowImpossibilityGS ... Finished ArrowImpossibilityGS (0:00:09 elapsed time, 0:00:18 cpu time, factor 2.00) Running AutoFocus-Stream ... Finished AutoFocus-Stream (0:00:46 elapsed time, 0:01:45 cpu time, factor 2.28) Running Fermat3_4 ... Finished Fermat3_4 (0:00:32 elapsed time, 0:01:22 cpu time, factor 2.56) Running Free-Groups ... Finished Free-Groups (0:00:56 elapsed time, 0:02:17 cpu time, factor 2.44) Running Heard_Of ... Finished Heard_Of (0:00:31 elapsed time, 0:01:10 cpu time, factor 2.25) Running HotelKeyCards ... Finished HotelKeyCards (0:00:09 elapsed time, 0:00:17 cpu time, factor 1.88) Running Impossible_Geometry ... Finished Impossible_Geometry (0:00:13 elapsed time, 0:00:23 cpu time, factor 1.76) Running Locally-Nameless-Sigma ... Finished Locally-Nameless-Sigma (0:00:31 elapsed time, 0:01:15 cpu time, factor 2.41) Running Ordinary_Differential_Equations ... Finished Ordinary_Differential_Equations (0:01:22 elapsed time, 0:02:56 cpu time, factor 2.14) Running PCF ... Finished PCF (0:00:41 elapsed time, 0:01:29 cpu time, factor 2.17) Running Program-Conflict-Analysis ... Finished Program-Conflict-Analysis (0:00:34 elapsed time, 0:01:15 cpu time, factor 2.20) Running SIFPL ... Finished SIFPL (0:00:41 elapsed time, 0:01:33 cpu time, factor 2.26) Running SenSocialChoice ... Finished SenSocialChoice (0:00:24 elapsed time, 0:00:50 cpu time, factor 2.08) Running Shivers-CFA ... Finished Shivers-CFA (0:00:24 elapsed time, 0:00:52 cpu time, factor 2.16) Running Statecharts ... Finished Statecharts (0:00:54 elapsed time, 0:02:36 cpu time, factor 2.88) Running SumSquares ... Finished SumSquares (0:00:25 elapsed time, 0:01:06 cpu time, factor 2.64) Running TLA ... Finished TLA (0:00:21 elapsed time, 0:00:49 cpu time, factor 2.33) Running Transitive-Closure ... Finished Transitive-Closure (0:00:47 elapsed time, 0:02:08 cpu time, factor 2.72) Running SequentInvertibility ... Finished SequentInvertibility (0:00:58 elapsed time, 0:02:12 cpu time, factor 2.27) Running Markov_Models ... Finished Markov_Models (0:00:34 elapsed time, 0:01:21 cpu time, factor 2.38) Running Ordinals_and_Cardinals ... Finished Ordinals_and_Cardinals (0:00:22 elapsed time, 0:00:49 cpu time, factor 2.22) Running WorkerWrapper ... Finished WorkerWrapper (0:00:25 elapsed time, 0:00:42 cpu time, factor 1.68) Running Binomial-Heaps ... Finished Binomial-Heaps (0:00:31 elapsed time, 0:01:00 cpu time, factor 1.93) Running Binomial-Queues ... Finished Binomial-Queues (0:00:10 elapsed time, 0:00:14 cpu time, factor 1.40) Running Datatype_Order_Generator ... Finished Datatype_Order_Generator (0:01:40 elapsed time, 0:02:05 cpu time, factor 1.25) Running Finger-Trees ... Finished Finger-Trees (0:00:17 elapsed time, 0:00:26 cpu time, factor 1.52) Running Inductive_Confidentiality ... Finished Inductive_Confidentiality (0:00:16 elapsed time, 0:00:34 cpu time, factor 2.12) Running Matrix ... Finished Matrix (0:00:37 elapsed time, 0:01:21 cpu time, factor 2.18) Running Max-Card-Matching ... Finished Max-Card-Matching (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.40) Running Myhill-Nerode ... Finished Myhill-Nerode (0:00:26 elapsed time, 0:00:55 cpu time, factor 2.11) Running Polynomials ... Finished Polynomials (0:00:35 elapsed time, 0:01:16 cpu time, factor 2.17) Running Regular-Sets ... Finished Regular-Sets (0:00:34 elapsed time, 0:01:19 cpu time, factor 2.32) Running Stuttering_Equivalence ... Finished Stuttering_Equivalence (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.20) Running Transitive-Closure-II ... Finished Transitive-Closure-II (0:00:20 elapsed time, 0:00:28 cpu time, factor 1.40) Running Abstract-Rewriting ... Finished Abstract-Rewriting (0:00:38 elapsed time, 0:01:10 cpu time, factor 1.84) Running Coinductive ... Finished Coinductive (0:00:30 elapsed time, 0:01:04 cpu time, factor 2.13) Running Perfect-Number-Thm ... Finished Perfect-Number-Thm (0:00:12 elapsed time, 0:00:28 cpu time, factor 2.33) Running Well_Quasi_Orders ... Finished Well_Quasi_Orders (0:00:24 elapsed time, 0:00:56 cpu time, factor 2.33) Running Efficient-Mergesort ... Finished Efficient-Mergesort (0:00:20 elapsed time, 0:00:36 cpu time, factor 1.80) Running DPT-SAT-Solver ... Finished DPT-SAT-Solver (0:00:11 elapsed time, 0:00:09 cpu time, factor 0.81) Running DataRefinementIBP ... Finished DataRefinementIBP (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.50) Running Free-Boolean-Algebra ... Finished Free-Boolean-Algebra (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.20) Running FunWithFunctions ... Finished FunWithFunctions (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.20) Running FunWithTilings ... Finished FunWithTilings (0:00:12 elapsed time, 0:00:27 cpu time, factor 2.25) Running GraphMarkingIBP ... Finished GraphMarkingIBP (0:00:22 elapsed time, 0:00:50 cpu time, factor 2.27) Running Lam-ml-Normalization ... Finished Lam-ml-Normalization (0:00:14 elapsed time, 0:00:19 cpu time, factor 1.35) Running List-Index ... Finished List-Index (0:00:04 elapsed time, 0:00:05 cpu time) Running Robbins-Conjecture ... Finished Robbins-Conjecture (0:00:11 elapsed time, 0:00:24 cpu time, factor 2.18) Running Gauss-Jordan-Elim-Fun ... Finished Gauss-Jordan-Elim-Fun (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.60) Running Marriage ... Finished Marriage (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.28) 2:38:49 elapsed time, 5:22:47 cpu time, factor 2.03 End test on Fri Sep 21 09:10:42 CEST 2012, macbroy2, elapsed time: 2:42:42
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
