[isabelle-dev] Fwd: status (AFP)

Lukas Bulwahn bulwahn at in.tum.de
Fri Sep 21 09:12:53 CEST 2012


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: 	isatest at macbroy2.informatik.tu-muenchen.de (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



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120921/329fbdf1/attachment.html>
-------------- next part --------------
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

-------------- next part --------------
Start test for /home/isatest/afp/devel at Fri Sep 21 06:31:44 CEST 2012, macbroy2

begin hg pull/update
pulling from ssh://isatest@afp.hg.sourceforge.net/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



More information about the isabelle-dev mailing list