The afp test is now back to normal operation and the devel website update is working again as well.
The two below are real failures, possibly have been there for a while masked by the problems the test had. Cheers, Gerwin Begin forwarded message: > From: [email protected] (Isabelle ) > Subject: status (AFP) > Date: 16 December 2012 5:59:14 PM AEDT > To: undisclosed-recipients:; > > The status of the following AFP entries changed or remains FAIL: > [Possibilistic_Noninterference] is still on FAIL. > [Separation_Logic_Imperative_HOL] is still on FAIL. > > Full entry status at http://afp.sourceforge.net/status.shtml > > AFP version: development -- hg id 519e8aa3ea9f > Isabelle version: devel -- hg id e4dc37ec1427 > Test ended on: macbroy2, Sun Dec 16 07:59:14 CET 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 InformationFlowSlicing_Intra: ok FunWithFunctions: ok Coinductive: ok Possibilistic_Noninterference: FAIL 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 InformationFlowSlicing_Inter: ok Example-Submission: ok SumSquares: ok JiveDataStoreModel: ok BDD: 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 DPT-SAT-Solver: ok Tarskis_Geometry: ok RIPEMD-160-SPARK: ok Flyspeck-Tame: ok Regular-Sets: ok RSAPSS: ok LightweightJava: ok Gauss-Jordan-Elim-Fun: ok Separation_Logic_Imperative_HOL: FAIL 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 Bondy: ok FunWithTilings: ok SenSocialChoice: ok CCS: ok Open_Induction: 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 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 Sun Dec 16 06:05:45 CET 2012, macbroy2 begin hg pull/update pulling from ssh://[email protected]/hgroot/afp/afp searching for changes no changes found end hg pull/update AFP version: development -- hg id 519e8aa3ea9f Isabelle version: devel -- hg id e4dc37ec1427 Building HOLCF ... Finished HOLCF (0:00:36 elapsed time, 0:00:58 cpu time, factor 1.61) Building HOL-Nominal ... Finished HOL-Nominal (0:00:14 elapsed time, 0:00:22 cpu time, factor 1.57) Building HOL-Multivariate_Analysis ... Finished HOL-Multivariate_Analysis (0:01:54 elapsed time, 0:05:14 cpu time, factor 2.75) Building HOL-Word ... Finished HOL-Word (0:00:28 elapsed time, 0:01:02 cpu time, factor 2.21) Building Jinja ... Finished Jinja (0:04:02 elapsed time, 0:12:23 cpu time, factor 3.07) Building LatticeProperties ... Finished LatticeProperties (0:00:14 elapsed time, 0:00:21 cpu time, factor 1.50) Building HOL-Probability ... Finished HOL-Probability (0:01:30 elapsed time, 0:04:08 cpu time, factor 2.75) Building HRB-Slicing ... Finished HRB-Slicing (0:04:57 elapsed time, 0:15:15 cpu time, factor 3.08) Building Slicing ... Finished Slicing (0:04:43 elapsed time, 0:15:04 cpu time, factor 3.19) Building Group-Ring-Module ... Finished Group-Ring-Module (0:02:17 elapsed time, 0:06:49 cpu time, factor 2.98) Building Simpl ... Finished Simpl (0:01:42 elapsed time, 0:04:49 cpu time, factor 2.83) Building Collections ... Finished Collections (0:04:00 elapsed time, 0:09:28 cpu time, factor 2.36) Building Refine_Monadic ... Finished Refine_Monadic (0:01:05 elapsed time, 0:02:29 cpu time, factor 2.29) Building List-Infinite ... Finished List-Infinite (0:00:32 elapsed time, 0:01:10 cpu time, factor 2.18) Building Nat-Interval-Logic ... Finished Nat-Interval-Logic (0:00:34 elapsed time, 0:01:09 cpu time, factor 2.02) Building HOL-Cardinals-Base ... Finished HOL-Cardinals-Base (0:00:16 elapsed time, 0:00:38 cpu time, factor 2.37) Building HOL-Cardinals ... Finished HOL-Cardinals (0:00:15 elapsed time, 0:00:24 cpu time, factor 1.60) Running Flyspeck-Tame ... Finished Flyspeck-Tame (0:01:29 elapsed time, 0:05:39 cpu time, factor 3.80) Running InformationFlowSlicing_Inter ... Finished InformationFlowSlicing_Inter (0:00:28 elapsed time, 0:01:04 cpu time, factor 2.28) Running InformationFlowSlicing_Intra ... Finished InformationFlowSlicing_Intra (0:00:08 elapsed time, 0:00:06 cpu time, factor 0.75) Running JinjaThreads ... Finished JinjaThreads (0:30:51 elapsed time, 2:06:47 cpu time, factor 4.10) Running AVL-Trees ... Finished AVL-Trees (0:00:11 elapsed time, 0:00:31 cpu time, factor 2.81) Running Abstract-Hoare-Logics ... Finished Abstract-Hoare-Logics (0:00:11 elapsed time, 0:00:29 cpu time, factor 2.63) Running BDD ... Finished BDD (0:00:41 elapsed time, 0:01:54 cpu time, factor 2.78) Running BinarySearchTree ... Finished BinarySearchTree (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.80) Running BytecodeLogicJmlTypes ... Finished BytecodeLogicJmlTypes (0:00:50 elapsed time, 0:02:12 cpu time, factor 2.64) Running CCS ... Finished CCS (0:00:17 elapsed time, 0:00:35 cpu time, factor 2.05) Running Category ... Finished Category (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.50) Running Category2 ... Finished Category2 (0:00:20 elapsed time, 0:00:51 cpu time, factor 2.55) Running Cauchy ... Finished Cauchy (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.80) Running Circus ... Finished Circus (0:00:59 elapsed time, 0:02:19 cpu time, factor 2.35) Running ClockSynchInst ... Finished ClockSynchInst (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.71) Running CofGroups ... Finished CofGroups (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.40) Running Compiling-Exceptions-Correctly ... Finished Compiling-Exceptions-Correctly (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.16) Running Completeness ... Finished Completeness (0:00:14 elapsed time, 0:00:28 cpu time, factor 2.00) Running Depth-First-Search ... Finished Depth-First-Search (0:00:04 elapsed time, 0:00:05 cpu time) Running Dijkstra_Shortest_Path ... Finished Dijkstra_Shortest_Path (0:00:36 elapsed time, 0:01:01 cpu time, factor 1.69) Running DiskPaxos ... Finished DiskPaxos (0:00:20 elapsed time, 0:00:55 cpu time, factor 2.75) Running Example-Submission ... Finished Example-Submission (0:00:04 elapsed time, 0:00:03 cpu time) Running FFT ... Finished FFT (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.20) Running FOL-Fitting ... Finished FOL-Fitting (0:00:31 elapsed time, 0:00:46 cpu time, factor 1.48) Running FeatherweightJava ... Finished FeatherweightJava (0:00:14 elapsed time, 0:00:24 cpu time, factor 1.71) Running FileRefinement ... Finished FileRefinement (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.71) Running FinFun ... Finished FinFun (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.55) Running Functional-Automata ... Finished Functional-Automata (0:00:11 elapsed time, 0:00:21 cpu time, factor 1.90) Running GenClock ... Finished GenClock (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.57) Running General-Triangle ... Finished General-Triangle (0:00:04 elapsed time, 0:00:06 cpu time) Running Huffman ... Finished Huffman (0:00:12 elapsed time, 0:00:22 cpu time, factor 1.83) Running Integration ... Finished Integration (0:00:09 elapsed time, 0:00:18 cpu time, factor 2.00) Running JiveDataStoreModel ... Finished JiveDataStoreModel (0:00:13 elapsed time, 0:00:23 cpu time, factor 1.76) Running KBPs ... Finished KBPs (0:01:23 elapsed time, 0:04:04 cpu time, factor 2.93) Running Lazy-Lists-II ... Finished Lazy-Lists-II (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.57) Running LightweightJava ... Finished LightweightJava (0:00:36 elapsed time, 0:01:14 cpu time, factor 2.05) Running Lower_Semicontinuous ... Finished Lower_Semicontinuous (0:00:09 elapsed time, 0:00:18 cpu time, factor 2.00) Running MiniML ... Finished MiniML (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.54) Running MonoBoolTranAlgebra ... Finished MonoBoolTranAlgebra (0:00:11 elapsed time, 0:00:13 cpu time, factor 1.18) Running MuchAdoAboutTwo ... Finished MuchAdoAboutTwo (0:00:13 elapsed time, 0:00:24 cpu time, factor 1.84) Running NormByEval ... Finished NormByEval (0:00:24 elapsed time, 0:00:53 cpu time, factor 2.20) Running Ordinal ... Finished Ordinal (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.37) Running POPLmark-deBruijn ... Finished POPLmark-deBruijn (0:00:18 elapsed time, 0:00:46 cpu time, factor 2.55) Running Pi_Calculus ... Finished Pi_Calculus (0:01:04 elapsed time, 0:02:47 cpu time, factor 2.60) Running PseudoHoops ... Finished PseudoHoops (0:01:20 elapsed time, 0:01:45 cpu time, factor 1.31) Running Psi_Calculi ... Finished Psi_Calculi (0:04:45 elapsed time, 0:15:23 cpu time, factor 3.23) Running RIPEMD-160-SPARK ... Finished RIPEMD-160-SPARK (0:00:13 elapsed time, 0:00:34 cpu time, factor 2.61) Running RSAPSS ... Finished RSAPSS (0:00:17 elapsed time, 0:00:47 cpu time, factor 2.76) Running Ramsey-Infinite ... Finished Ramsey-Infinite (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.28) Running Recursion-Theory-I ... Finished Recursion-Theory-I (0:00:16 elapsed time, 0:00:35 cpu time, factor 2.18) Running SATSolverVerification ... Finished SATSolverVerification (0:00:57 elapsed time, 0:02:43 cpu time, factor 2.85) Running Separation_Algebra ... Finished Separation_Algebra (0:00:17 elapsed time, 0:00:36 cpu time, factor 2.11) Running Separation_Logic_Imperative_HOL ... Separation_Logic_Imperative_HOL FAILED (see also /home/isatest/afp/isabelle-afp-poly/heaps/polyml-5.5.0_x86-darwin/log/Separation_Logic_Imperative_HOL) Found termination order: "{}" *** Theory loader: failed to load "Hoare_Triple" (unresolved "Assertions") *** Theory loader: failed to load "Automation" (unresolved "Hoare_Triple") *** Theory loader: failed to load "Sep_Main" (unresolved "Automation") *** Theory loader: failed to load "Hash_Table" (unresolved "Sep_Main") *** Theory loader: failed to load "List_Seg" (unresolved "Sep_Main") *** Theory loader: failed to load "Imp_Map_Spec" (unresolved "Sep_Main") *** Theory loader: failed to load "Imp_Set_Spec" (unresolved "Sep_Main") *** Theory loader: failed to load "Hash_Map" (unresolved "Hash_Table") *** Theory loader: failed to load "Imp_List_Spec" (unresolved "Sep_Main") *** Theory loader: failed to load "Circ_List" (unresolved "List_Seg", "Imp_List_Spec") *** Theory loader: failed to load "Open_List" (unresolved "List_Seg", "Imp_List_Spec") *** Theory loader: failed to load "Hash_Map_Impl" (unresolved "Hash_Map", "Imp_Map_Spec") *** Theory loader: failed to load "Hash_Set_Impl" (unresolved "Imp_Set_Spec", "Hash_Map_Impl") *** Theory loader: failed to load "Idioms" (unresolved "Sep_Main", "Circ_List", "Open_List", "Hash_Set_Impl") *** Outer syntax error (line 143 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/Separation_Logic_Imperative_HOL/Assertions.thy"): type variable expected, *** but keyword open (line 143 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/Separation_Logic_Imperative_HOL/Assertions.thy") was found *** At command "<malformed>" (line 143 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/Separation_Logic_Imperative_HOL/Assertions.thy") Running Stream-Fusion ... Finished Stream-Fusion (0:00:14 elapsed time, 0:00:17 cpu time, factor 1.21) Running Tarskis_Geometry ... Finished Tarskis_Geometry (0:01:24 elapsed time, 0:04:35 cpu time, factor 3.27) Running Topology ... Finished Topology (0:00:11 elapsed time, 0:00:27 cpu time, factor 2.45) Running Tycon ... Finished Tycon (0:00:12 elapsed time, 0:00:23 cpu time, factor 1.91) Running Valuation ... Finished Valuation (0:00:32 elapsed time, 0:01:20 cpu time, factor 2.50) Running Verified-Prover ... Finished Verified-Prover (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.55) Running CoreC++ ... Finished CoreC++ (0:03:11 elapsed time, 0:06:32 cpu time, factor 2.05) Running VolpanoSmith ... Finished VolpanoSmith (0:00:12 elapsed time, 0:00:18 cpu time, factor 1.50) Running LinearQuantifierElim ... Finished LinearQuantifierElim (0:00:55 elapsed time, 0:02:51 cpu time, factor 3.10) Running Girth_Chromatic ... Finished Girth_Chromatic (0:00:42 elapsed time, 0:01:35 cpu time, factor 2.26) Running Presburger-Automata ... Finished Presburger-Automata (0:00:21 elapsed time, 0:00:52 cpu time, factor 2.47) Running Tree-Automata ... Finished Tree-Automata (0:03:17 elapsed time, 0:08:40 cpu time, factor 2.63) Running Abortable_Linearizable_Modules ... Finished Abortable_Linearizable_Modules (0:00:25 elapsed time, 0:01:06 cpu time, factor 2.64) Running ArrowImpossibilityGS ... Finished ArrowImpossibilityGS (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.37) Running AutoFocus-Stream ... Finished AutoFocus-Stream (0:00:36 elapsed time, 0:01:31 cpu time, factor 2.52) Running Fermat3_4 ... Finished Fermat3_4 (0:00:23 elapsed time, 0:01:10 cpu time, factor 3.04) Running Free-Groups ... Finished Free-Groups (0:00:38 elapsed time, 0:02:02 cpu time, factor 3.21) Running Heard_Of ... Finished Heard_Of (0:00:24 elapsed time, 0:01:04 cpu time, factor 2.66) Running HotelKeyCards ... Finished HotelKeyCards (0:00:07 elapsed time, 0:00:15 cpu time, factor 2.14) Running Impossible_Geometry ... Finished Impossible_Geometry (0:00:10 elapsed time, 0:00:20 cpu time, factor 2.00) Running Locally-Nameless-Sigma ... Finished Locally-Nameless-Sigma (0:00:23 elapsed time, 0:01:08 cpu time, factor 2.95) Running Ordinary_Differential_Equations ... Finished Ordinary_Differential_Equations (0:01:04 elapsed time, 0:02:31 cpu time, factor 2.35) Running PCF ... Finished PCF (0:00:32 elapsed time, 0:01:18 cpu time, factor 2.43) Running Program-Conflict-Analysis ... Finished Program-Conflict-Analysis (0:00:25 elapsed time, 0:01:09 cpu time, factor 2.76) Running SIFPL ... Finished SIFPL (0:00:31 elapsed time, 0:01:22 cpu time, factor 2.64) Running SenSocialChoice ... Finished SenSocialChoice (0:00:19 elapsed time, 0:00:49 cpu time, factor 2.57) Running Shivers-CFA ... Finished Shivers-CFA (0:00:19 elapsed time, 0:00:48 cpu time, factor 2.52) Running Statecharts ... Finished Statecharts (0:00:42 elapsed time, 0:02:22 cpu time, factor 3.38) Running SumSquares ... Finished SumSquares (0:00:17 elapsed time, 0:00:57 cpu time, factor 3.35) Running TLA ... Finished TLA (0:00:17 elapsed time, 0:00:44 cpu time, factor 2.58) Running Transitive-Closure ... Finished Transitive-Closure (0:00:46 elapsed time, 0:02:49 cpu time, factor 3.67) Running SequentInvertibility ... Finished SequentInvertibility (0:00:46 elapsed time, 0:01:56 cpu time, factor 2.52) Running Bondy ... Finished Bondy (0:00:04 elapsed time, 0:00:04 cpu time) Running Markov_Models ... Finished Markov_Models (0:00:23 elapsed time, 0:01:03 cpu time, factor 2.73) Running Open_Induction ... Finished Open_Induction (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.80) Running Ordinals_and_Cardinals ... Finished Ordinals_and_Cardinals (0:00:05 elapsed time, 0:00:03 cpu time) Running Possibilistic_Noninterference ... Possibilistic_Noninterference FAILED (see also /home/isatest/afp/isabelle-afp-poly/heaps/polyml-5.5.0_x86-darwin/log/Possibilistic_Noninterference) ### but you may still want to disambiguate your grammar or your input. ### Ignoring duplicate rewrite rule: ### PL_Indis.SC_discr aval indis (Atm ?atm1) == ### PL_Indis.presAtm aval indis ?atm1 ### Ignoring duplicate rewrite rule: ### PL_Indis.SC_discr aval indis (?c1.1 ;; ?c2.1) == ### PL_Indis.SC_discr aval indis ?c1.1 & PL_Indis.SC_discr aval indis ?c2.1 ### Ignoring duplicate rewrite rule: ### PL_Indis.SC_discr aval indis (if ?tst1 then ?c1.1 else ?c2.1) == ### PL_Indis.SC_discr aval indis ?c1.1 & PL_Indis.SC_discr aval indis ?c2.1 ### Ignoring duplicate rewrite rule: ### PL_Indis.SC_discr aval indis (while ?tst1 do ?c1) == ### PL_Indis.SC_discr aval indis ?c1 ### Ignoring duplicate rewrite rule: ### PL_Indis.SC_discr aval indis (?c1.1 | ?c2.1) == ### PL_Indis.SC_discr aval indis ?c1.1 & PL_Indis.SC_discr aval indis ?c2.1 *** Unknown proof method: "fastsimp" (line 706 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/Possibilistic_Noninterference/Language_Semantics.thy") *** Unknown proof method: "fastsimp" (line 1038 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/Possibilistic_Noninterference/During_Execution.thy") *** At command "apply" (line 1038 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/Possibilistic_Noninterference/During_Execution.thy") Running WorkerWrapper ... Finished WorkerWrapper (0:00:20 elapsed time, 0:00:37 cpu time, factor 1.85) Running Binomial-Heaps ... Finished Binomial-Heaps (0:00:22 elapsed time, 0:00:54 cpu time, factor 2.45) Running Binomial-Queues ... Finished Binomial-Queues (0:00:09 elapsed time, 0:00:13 cpu time, factor 1.44) Running Datatype_Order_Generator ... Finished Datatype_Order_Generator (0:01:15 elapsed time, 0:01:38 cpu time, factor 1.30) Running Finger-Trees ... Finished Finger-Trees (0:00:15 elapsed time, 0:00:25 cpu time, factor 1.66) Running Inductive_Confidentiality ... Finished Inductive_Confidentiality (0:00:13 elapsed time, 0:00:30 cpu time, factor 2.30) Running Matrix ... Finished Matrix (0:00:28 elapsed time, 0:01:19 cpu time, factor 2.82) Running Max-Card-Matching ... Finished Max-Card-Matching (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.16) Running Myhill-Nerode ... Finished Myhill-Nerode (0:00:21 elapsed time, 0:00:53 cpu time, factor 2.52) Running Polynomials ... Finished Polynomials (0:00:28 elapsed time, 0:01:07 cpu time, factor 2.39) Running Regular-Sets ... Finished Regular-Sets (0:00:26 elapsed time, 0:01:10 cpu time, factor 2.69) Running Stuttering_Equivalence ... Finished Stuttering_Equivalence (0:00:04 elapsed time, 0:00:06 cpu time) Running Transitive-Closure-II ... Finished Transitive-Closure-II (0:00:16 elapsed time, 0:00:24 cpu time, factor 1.50) Running Abstract-Rewriting ... Finished Abstract-Rewriting (0:00:29 elapsed time, 0:01:03 cpu time, factor 2.17) Running Coinductive ... Finished Coinductive (0:00:22 elapsed time, 0:00:58 cpu time, factor 2.63) Running Perfect-Number-Thm ... Finished Perfect-Number-Thm (0:00:10 elapsed time, 0:00:25 cpu time, factor 2.50) Running Well_Quasi_Orders ... Finished Well_Quasi_Orders (0:00:19 elapsed time, 0:00:50 cpu time, factor 2.63) Running Efficient-Mergesort ... Finished Efficient-Mergesort (0:00:16 elapsed time, 0:00:31 cpu time, factor 1.93) Running DPT-SAT-Solver ... Finished DPT-SAT-Solver (0:00:11 elapsed time, 0:00:08 cpu time, factor 0.72) Running DataRefinementIBP ... Finished DataRefinementIBP (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.60) Running Free-Boolean-Algebra ... Finished Free-Boolean-Algebra (0:00:04 elapsed time, 0:00:05 cpu time) Running FunWithFunctions ... Finished FunWithFunctions (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.20) Running FunWithTilings ... Finished FunWithTilings (0:00:10 elapsed time, 0:00:24 cpu time, factor 2.40) Running GraphMarkingIBP ... Finished GraphMarkingIBP (0:00:18 elapsed time, 0:00:44 cpu time, factor 2.44) Running Lam-ml-Normalization ... Finished Lam-ml-Normalization (0:00:11 elapsed time, 0:00:16 cpu time, factor 1.45) Running List-Index ... Finished List-Index (0:00:04 elapsed time, 0:00:03 cpu time) Running Robbins-Conjecture ... Finished Robbins-Conjecture (0:00:09 elapsed time, 0:00:22 cpu time, factor 2.44) Running Gauss-Jordan-Elim-Fun ... Finished Gauss-Jordan-Elim-Fun (0:00:04 elapsed time, 0:00:08 cpu time) Running Marriage ... Finished Marriage (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.33) Unfinished session(s): Possibilistic_Noninterference, Separation_Logic_Imperative_HOL 1:53:07 elapsed time, 5:40:23 cpu time, factor 3.00 End test on Sun Dec 16 07:59:14 CET 2012, macbroy2, elapsed time: 1:56:14
>
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
