Skip to content
[Jenkins]Jenkins
log in
Failed

Console Output

00:50:07 Started by an SCM change


00:50:07 [EnvInject] - Loading node environment variables.


00:50:07 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-nightly-benchmark


00:50:08 [isabelle-nightly-benchmark] $ hg showconfig paths.default


00:50:08 [isabelle-nightly-benchmark] $ hg pull --rev default


00:50:08 pulling from http://isabelle.in.tum.de/repos/isabelle/


00:50:08 searching for changes


00:50:08 no changes found


00:50:08 [isabelle-nightly-benchmark] $ hg update --clean --rev default


00:50:08 14 files updated, 0 files merged, 1 files removed, 0 files unresolved


00:50:08 [isabelle-nightly-benchmark] $ hg --config extensions.purge= clean --all


00:50:08 [isabelle-nightly-benchmark] $ hg log --rev . --template {node}


00:50:09 [isabelle-nightly-benchmark] $ hg log --rev . --template {rev}


00:50:09 [isabelle-nightly-benchmark] $ hg log --rev 63721ee8c86c528b5fe5f3dce27cd56efc2315a5 --template exists\n


00:50:09 exists


00:50:09 [isabelle-nightly-benchmark] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg><added>{file_adds|stringify|xmlescape}</added><deleted>{file_dels|stringify|xmlescape}</deleted><files>{files|stringify|xmlescape}</files><parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(63721ee8c86c528b5fe5f3dce27cd56efc2315a5)" --encoding UTF-8 --encodingmode replace


00:50:09 No emails were triggered.


00:50:09 [isabelle-nightly-benchmark] $ /bin/sh -xe /tmp/jenkins386781598375730483.sh


00:50:09 + Admin/jenkins/run_build benchmark


00:50:09 + set -e


00:50:09 + PROFILE=benchmark


00:50:09 + shift


00:50:09 + bin/isabelle components -a


00:50:09 + bin/isabelle jedit -bf


00:50:09 ### Building graph browser ...


00:50:09 warning: [options] bootstrap class path not set in conjunction with -source 6


00:50:09 warning: [options] source value 6 is obsolete and will be removed in a future release


00:50:09 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.


00:50:10 Note: Some input files use or override a deprecated API.


00:50:10 Note: Recompile with -Xlint:deprecation for details.


00:50:10 Note: Some input files use unchecked or unsafe operations.


00:50:10 Note: Recompile with -Xlint:unchecked for details.


00:50:10 3 warnings


00:50:10 ### Building Isabelle/Scala ...


00:50:38 ### Building Isabelle/jEdit ...


00:50:57 + bin/isabelle ocaml_setup


00:50:57 # To setup the new switch in the current shell, you need to run:


00:50:57 eval `opam config env`


00:50:57 + bin/isabelle ghc_setup


00:50:58 stack will use a sandboxed GHC it installed


00:50:58 For more information on paths, see 'stack path' and 'stack exec env'


00:50:58 To use this GHC and packages outside of a project, consider using:


00:50:58 stack ghc, stack ghci, stack runghc, or stack exec


00:50:58 The Glorious Glasgow Haskell Compilation System, version 8.4.4


00:50:58 + bin/isabelle ci_build_benchmark


00:51:02 

00:51:02 === CONFIGURATION ===


00:51:02 

00:51:02 ISABELLE_BUILD_OPTIONS=""


00:51:02 

00:51:02 ML_PLATFORM="x86_64-linux"


00:51:02 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64-linux"


00:51:02 ML_SYSTEM="polyml-5.8"


00:51:02 ML_OPTIONS="-H 4000 --maxheap 8G"


00:51:02 jobs = 1, threads = 6, numa = false


00:51:02 

00:51:02 === BUILD ===


00:51:02 

00:51:02 Build started at Wed, 13 Mar 2019 23:51:02 GMT


00:51:02 Isabelle id 4343c1bfa52d


00:51:02 

00:51:02 === LOG ===


00:51:02 

00:51:03 Session Pure/Pure


00:51:03 Session FOL/FOL


00:51:03 Session HOL/HOL (main)


00:51:04 Session HOL/HOL-Eisbach


00:51:04 Session HOL/HOL-Hoare_Parallel (timing)


00:51:04 Session HOL/HOL-Library (main timing)


00:51:05 Session HOL/HOL-Auth (timing)


00:51:05 Session HOL/HOL-UNITY (timing)


00:51:05 Session HOL/HOL-Bali (timing)


00:51:05 Session HOL/HOL-Cardinals (timing)


00:51:05 Session HOL/HOL-Computational_Algebra (main timing)


00:51:05 Session HOL/HOL-Algebra (main timing)


00:51:06 Session HOL/HOL-Decision_Procs (timing)


00:51:06 Session HOL/HOL-Quotient_Examples (timing)


00:51:06 Session HOL/HOL-Analysis (main timing)


00:51:07 Session HOL/HOL-Probability (main timing)


00:51:07 Session HOL/HOL-Probability-ex (timing)


00:51:07 Session HOL/HOL-Nonstandard_Analysis (timing)


00:51:08 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)


00:51:08 Session HOL/HOL-Number_Theory (main timing)


00:51:08 Session HOL/HOL-Data_Structures (timing)


00:51:08 Session HOL/HOL-ex (timing)


00:51:08 Session HOL/HOL-Corec_Examples (timing)


00:51:08 Session HOL/HOL-Datatype_Benchmark


00:51:08 Session HOL/HOL-Datatype_Examples (timing)


00:51:08 Session HOL/HOL-IMP (timing)


00:51:09 Session HOL/HOL-Imperative_HOL (timing)


00:51:09 Session HOL/HOL-Metis_Examples (timing)


00:51:09 Session HOL/HOL-MicroJava (timing)


00:51:09 Session HOL/HOL-Nominal


00:51:09 Session HOL/HOL-Nominal-Examples (timing)


00:51:09 Session HOL/HOL-Predicate_Compile_Examples (timing)


00:51:09 Session HOL/HOL-Quickcheck_Benchmark


00:51:09 Session HOL/HOL-Quickcheck_Examples (timing)


00:51:09 Session HOL/HOL-SET_Protocol (timing)


00:51:09 Session HOL/HOL-Record_Benchmark


00:51:09 Session HOL/HOL-Word (main timing)


00:51:10 Session HOL/HOL-Word-SMT_Examples (timing)


00:51:10 Session HOL/HOLCF (main timing)


00:51:10 Session HOL/IOA (timing)


00:51:10 Session HOL/HOL-Proofs (timing)


00:51:11 Session HOL/HOL-Proofs-Extraction (timing)


00:51:11 Session HOL/HOL-Proofs-Lambda (timing)


00:51:11 Session ZF/ZF (main timing)


00:51:11 Session ZF/ZF-Induct


00:51:11 Session ZF/ZF-UNITY (timing)


00:51:12 Building Pure ...


00:51:32 Pure: theory Pure


00:51:33 Pure: theory ML_Bootstrap


00:51:33 Pure: theory Pure.Sessions


00:51:35 Timing Pure (1 threads, 1.059s elapsed time, 1.064s cpu time, 0.000s GC time, factor 1.00)


00:51:35 Finished Pure (0:00:22 elapsed time, 0:00:22 cpu time, factor 1.00)


00:51:35 Building HOL ...


00:51:38 HOL: theory HOL.Code_Generator


00:51:41 HOL: theory HOL.HOL


00:51:45 HOL: theory HOL.Argo


00:51:45 HOL: theory HOL.Ctr_Sugar


00:51:45 HOL: theory HOL.Orderings


00:51:47 HOL: theory HOL.Groups


00:51:48 HOL: theory HOL.SAT


00:51:51 HOL: theory HOL.Lattices


00:51:53 HOL: theory HOL.Set


00:51:55 HOL: theory HOL.Fun


00:51:55 HOL: theory HOL.Typedef


00:51:56 HOL: theory HOL.Complete_Lattices


00:51:56 HOL: theory HOL.Rings


00:51:58 HOL: theory HOL.Inductive


00:52:00 HOL: theory HOL.Product_Type


00:52:00 HOL: theory HOL.Sum_Type


00:52:02 HOL: theory HOL.Complete_Partial_Order


00:52:07 HOL: theory HOL.Nat


00:52:09 HOL: theory HOL.Fields


00:52:09 HOL: theory HOL.Meson


00:52:10 HOL: theory HOL.ATP


00:52:13 HOL: theory HOL.Metis


00:52:14 HOL: theory HOL.Finite_Set


00:52:15 HOL: theory HOL.Relation


00:52:17 HOL: theory HOL.Transitive_Closure


00:52:18 HOL: theory HOL.Wellfounded


00:52:18 HOL: theory HOL.Fun_Def_Base


00:52:19 HOL: theory HOL.Hilbert_Choice


00:52:19 HOL: theory HOL.Wfrec


00:52:19 HOL: theory HOL.Order_Relation


00:52:19 HOL: theory HOL.BNF_Wellorder_Relation


00:52:20 HOL: theory HOL.BNF_Wellorder_Embedding


00:52:20 HOL: theory HOL.Zorn


00:52:20 HOL: theory HOL.BNF_Wellorder_Constructions


00:52:21 HOL: theory HOL.BNF_Cardinal_Order_Relation


00:52:21 HOL: theory HOL.BNF_Cardinal_Arithmetic


00:52:22 HOL: theory HOL.BNF_Def


00:52:26 HOL: theory HOL.BNF_Composition


00:52:26 HOL: theory HOL.Basic_BNFs


00:52:27 HOL: theory HOL.BNF_Fixpoint_Base


00:52:31 HOL: theory HOL.BNF_Least_Fixpoint


00:52:35 HOL: theory HOL.Basic_BNF_LFPs


00:52:35 HOL: theory HOL.Transfer


00:52:36 HOL: theory HOL.Num


00:52:39 HOL: theory HOL.Power


00:52:42 HOL: theory HOL.Groups_Big


00:52:44 HOL: theory HOL.Equiv_Relations


00:52:45 HOL: theory HOL.Lifting


00:52:46 HOL: theory HOL.Lifting_Set


00:52:46 HOL: theory HOL.Option


00:52:46 HOL: theory HOL.Quotient


00:52:47 HOL: theory HOL.Extraction


00:52:47 HOL: theory HOL.Lattices_Big


00:52:47 HOL: theory HOL.Partial_Function


00:52:48 HOL: theory HOL.Fun_Def


00:52:50 HOL: theory HOL.Int


00:52:53 HOL: theory HOL.Euclidean_Division


00:52:58 HOL: theory HOL.Parity


00:53:01 HOL: theory HOL.Divides


00:53:04 HOL: theory HOL.Code_Numeral


00:53:04 HOL: theory HOL.Numeral_Simprocs


00:53:04 HOL: theory HOL.SMT


00:53:04 HOL: theory HOL.Set_Interval


00:53:05 HOL: theory HOL.Semiring_Normalization


00:53:07 HOL: theory HOL.Groebner_Basis


00:53:08 HOL: theory HOL.Conditionally_Complete_Lattices


00:53:08 HOL: theory HOL.Filter


00:53:09 HOL: theory HOL.Presburger


00:53:12 HOL: theory HOL.Sledgehammer


00:53:14 HOL: theory HOL.List


00:53:23 HOL: theory HOL.Groups_List


00:53:23 HOL: theory HOL.Map


00:53:24 HOL: theory HOL.Factorial


00:53:24 HOL: theory HOL.GCD


00:53:24 HOL: theory HOL.Enum


00:53:24 HOL: theory HOL.Random


00:53:25 HOL: theory HOL.Binomial


00:53:27 HOL: theory HOL.String


00:53:29 HOL: theory HOL.BNF_Greatest_Fixpoint


00:53:29 HOL: theory HOL.Predicate


00:53:29 HOL: theory HOL.Typerep


00:53:30 HOL: theory HOL.Lazy_Sequence


00:53:31 HOL: theory HOL.Limited_Sequence


00:53:31 HOL: theory HOL.Code_Evaluation


00:53:32 HOL: theory HOL.Quickcheck_Random


00:53:34 HOL: theory HOL.Quickcheck_Exhaustive


00:53:35 HOL: theory HOL.Quickcheck_Narrowing


00:53:36 HOL: theory HOL.Random_Pred


00:53:36 HOL: theory HOL.Random_Sequence


00:53:38 HOL: theory HOL.Record


00:53:38 HOL: theory HOL.Predicate_Compile


00:53:40 HOL: theory HOL.Nitpick


00:53:46 HOL: theory HOL.Nunchaku


00:53:48 HOL: theory Main


00:53:49 HOL: theory HOL.Archimedean_Field


00:53:49 HOL: theory HOL.Hull


00:53:49 HOL: theory HOL.Topological_Spaces


00:53:49 HOL: theory HOL.Modules


00:53:50 HOL: theory HOL.Vector_Spaces


00:53:55 HOL: theory HOL.Rat


00:53:57 HOL: theory HOL.Real


00:53:59 HOL: theory HOL.Real_Vector_Spaces


00:54:11 HOL: theory HOL.Inequalities


00:54:11 HOL: theory HOL.Limits


00:54:16 HOL: theory HOL.Deriv


00:54:16 HOL: theory HOL.Series


00:54:18 HOL: theory HOL.NthRoot


00:54:18 HOL: theory HOL.Transcendental


00:54:23 HOL: theory HOL.Complex


00:54:23 HOL: theory HOL.MacLaurin


00:54:25 HOL: theory Complex_Main


00:55:01 Timing HOL (6 threads, 178.242s elapsed time, 625.900s cpu time, 37.940s GC time, factor 3.51)


00:55:01 Finished HOL (0:03:24 elapsed time, 0:11:20 cpu time, factor 3.33)


00:55:01 Building HOL-Analysis ...


00:55:02 HOL-Analysis: theory HOL-Library.Cancellation


00:55:02 HOL-Analysis: theory HOL-Library.FuncSet


00:55:02 HOL-Analysis: theory HOL-Library.Disjoint_Sets


00:55:02 HOL-Analysis: theory HOL-Library.Infinite_Set


00:55:02 HOL-Analysis: theory HOL-Library.Nat_Bijection


00:55:02 HOL-Analysis: theory HOL-Library.Old_Datatype


00:55:03 HOL-Analysis: theory HOL-Library.Phantom_Type


00:55:03 HOL-Analysis: theory HOL-Library.Product_Plus


00:55:03 HOL-Analysis: theory HOL-Library.Product_Order


00:55:03 HOL-Analysis: theory HOL-Library.Set_Algebras


00:55:03 HOL-Analysis: theory HOL-Analysis.Inner_Product


00:55:03 HOL-Analysis: theory HOL-Library.Countable


00:55:03 HOL-Analysis: theory HOL-Library.Multiset


00:55:03 HOL-Analysis: theory HOL-Analysis.L2_Norm


00:55:03 HOL-Analysis: theory HOL-Analysis.Operator_Norm


00:55:03 HOL-Analysis: theory HOL-Analysis.Poly_Roots


00:55:04 HOL-Analysis: theory HOL-Analysis.Product_Vector


00:55:04 HOL-Analysis: theory HOL-Library.Cardinality


00:55:04 HOL-Analysis: theory HOL-Library.Discrete


00:55:04 HOL-Analysis: theory HOL-Library.Indicator_Function


00:55:04 HOL-Analysis: theory HOL-Library.Liminf_Limsup


00:55:05 HOL-Analysis: theory HOL-Library.Nonpos_Ints


00:55:05 HOL-Analysis: theory HOL-Library.Countable_Set


00:55:05 HOL-Analysis: theory HOL-Library.Periodic_Fun


00:55:05 HOL-Analysis: theory HOL-Analysis.Euclidean_Space


00:55:05 HOL-Analysis: theory HOL-Library.Numeral_Type


00:55:05 HOL-Analysis: theory HOL-Library.Sum_of_Squares


00:55:05 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices


00:55:05 HOL-Analysis: theory HOL-Library.Set_Idioms


00:55:06 HOL-Analysis: theory HOL-Analysis.Abstract_Topology


00:55:06 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable


00:55:06 HOL-Analysis: theory HOL-Analysis.Elementary_Topology


00:55:07 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product


00:55:08 HOL-Analysis: theory HOL-Analysis.Linear_Algebra


00:55:09 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring


00:55:09 HOL-Analysis: theory HOL-Library.Permutations


00:55:10 HOL-Analysis: theory HOL-Analysis.Abstract_Limits


00:55:10 HOL-Analysis: theory HOL-Analysis.Convex


00:55:10 HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2


00:55:10 HOL-Analysis: theory HOL-Library.Order_Continuity


00:55:10 HOL-Analysis: theory HOL-Analysis.Cartesian_Space


00:55:11 HOL-Analysis: theory HOL-Analysis.Norm_Arith


00:55:11 HOL-Analysis: theory HOL-Library.Extended_Nat


00:55:11 HOL-Analysis: theory HOL-Analysis.Connected


00:55:11 HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces


00:55:12 HOL-Analysis: theory HOL-Library.Extended_Real


00:55:12 HOL-Analysis: theory HOL-Analysis.Determinants


00:55:13 HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces


00:55:14 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space


00:55:15 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real


00:55:16 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm


00:55:17 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space


00:55:17 HOL-Analysis: theory HOL-Analysis.Tagged_Division


00:55:17 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra


00:55:18 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits


00:55:19 HOL-Analysis: theory HOL-Analysis.Starlike


00:55:19 HOL-Analysis: theory HOL-Analysis.Summation_Tests


00:55:20 HOL-Analysis: theory HOL-Analysis.Uniform_Limit


00:55:20 HOL-Analysis: theory HOL-Analysis.Measurable


00:55:20 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function


00:55:21 HOL-Analysis: theory HOL-Analysis.Measure_Space


00:55:21 HOL-Analysis: theory HOL-Analysis.Continuous_Extension


00:55:21 HOL-Analysis: theory HOL-Analysis.Path_Connected


00:55:22 HOL-Analysis: theory HOL-Computational_Algebra.Primes


00:55:22 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series


00:55:23 HOL-Analysis: theory HOL-Analysis.Homotopy


00:55:23 HOL-Analysis: theory HOL-Analysis.Caratheodory


00:55:26 HOL-Analysis: theory HOL-Analysis.Homeomorphism


00:55:26 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint


00:55:29 HOL-Analysis: theory HOL-Analysis.Derivative


00:55:30 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space


00:55:31 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems


00:55:32 HOL-Analysis: theory HOL-Analysis.Cross3


00:55:32 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem


00:55:32 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space


00:55:32 HOL-Analysis: theory HOL-Analysis.Polytope


00:55:35 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected


00:55:35 HOL-Analysis: theory HOL-Analysis.Borel_Space


00:55:38 HOL-Analysis: theory HOL-Analysis.Lipschitz


00:55:38 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration


00:55:38 HOL-Analysis: theory HOL-Analysis.Regularity


00:55:40 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure


00:55:41 HOL-Analysis: theory HOL-Analysis.Embed_Measure


00:55:41 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure


00:55:42 HOL-Analysis: theory HOL-Analysis.Bochner_Integration


00:55:42 HOL-Analysis: theory HOL-Analysis.Function_Topology


00:55:43 HOL-Analysis: theory HOL-Analysis.T1_Spaces


00:55:44 HOL-Analysis: theory HOL-Analysis.Complete_Measure


00:55:44 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym


00:55:44 HOL-Analysis: theory HOL-Analysis.Set_Integral


00:55:44 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure


00:55:45 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum


00:55:46 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration


00:55:50 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function


00:55:50 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration


00:55:50 HOL-Analysis: theory HOL-Analysis.Integral_Test


00:55:52 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics


00:55:52 HOL-Analysis: theory HOL-Analysis.Improper_Integral


00:55:52 HOL-Analysis: theory HOL-Analysis.Interval_Integral


00:55:53 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution


00:55:53 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental


00:55:56 HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem


00:55:56 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem


00:55:56 HOL-Analysis: theory HOL-Analysis.Infinite_Products


00:55:56 HOL-Analysis: theory HOL-Analysis.Further_Topology


00:55:56 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers


00:55:59 HOL-Analysis: theory HOL-Analysis.Jordan_Curve


00:56:00 HOL-Analysis: theory HOL-Analysis.Conformal_Mappings


00:56:01 HOL-Analysis: theory HOL-Analysis.FPS_Convergence


00:56:01 HOL-Analysis: theory HOL-Analysis.Great_Picard


00:56:01 HOL-Analysis: theory HOL-Analysis.Gamma_Function


00:56:02 HOL-Analysis: theory HOL-Analysis.Riemann_Mapping


00:56:03 HOL-Analysis: theory HOL-Analysis.Winding_Numbers


00:56:05 HOL-Analysis: theory HOL-Analysis.Ball_Volume


00:56:05 HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem


00:56:06 HOL-Analysis: theory HOL-Analysis.Change_Of_Vars


00:56:08 HOL-Analysis: theory HOL-Analysis.Simplex_Content


00:56:08 HOL-Analysis: theory HOL-Analysis.Analysis


01:00:54 Timing HOL-Analysis (6 threads, 329.557s elapsed time, 1616.532s cpu time, 59.796s GC time, factor 4.91)


01:00:54 Finished HOL-Analysis (0:05:51 elapsed time, 0:27:44 cpu time, factor 4.74)


01:00:54 Running HOL-Data_Structures ...


01:00:55 HOL-Data_Structures: theory HOL-Data_Structures.Less_False


01:00:55 HOL-Data_Structures: theory HOL-Data_Structures.Array_Specs


01:00:55 HOL-Data_Structures: theory HOL-Data_Structures.Cmp


01:00:55 HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less


01:00:55 HOL-Data_Structures: theory HOL-Data_Structures.Tree2


01:00:55 HOL-Data_Structures: theory HOL-Data_Structures.Tree23


01:00:55 HOL-Data_Structures: theory HOL-Data_Structures.Tree234


01:00:55 HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del


01:00:55 HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del


01:00:55 HOL-Data_Structures: theory HOL-Library.Cancellation


01:00:55 HOL-Data_Structures: theory HOL-Data_Structures.Set_Specs


01:00:56 HOL-Data_Structures: theory HOL-Data_Structures.Trie


01:00:56 HOL-Data_Structures: theory HOL-Data_Structures.Map_Specs


01:00:56 HOL-Data_Structures: theory HOL-Library.Pattern_Aliases


01:00:56 HOL-Data_Structures: theory HOL-Data_Structures.Base_FDS


01:00:56 HOL-Data_Structures: theory HOL-Library.Tree


01:00:56 HOL-Data_Structures: theory HOL-Library.Multiset


01:00:57 HOL-Data_Structures: theory HOL-Data_Structures.Isin2


01:00:57 HOL-Data_Structures: theory HOL-Data_Structures.Lookup2


01:00:57 HOL-Data_Structures: theory HOL-Data_Structures.AA_Set


01:00:57 HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join


01:00:58 HOL-Data_Structures: theory HOL-Data_Structures.RBT


01:00:58 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set


01:00:59 HOL-Data_Structures: theory HOL-Data_Structures.AA_Map


01:00:59 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set


01:00:59 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set


01:00:59 HOL-Data_Structures: theory HOL-Library.Tree_Real


01:01:00 HOL-Data_Structures: theory HOL-Data_Structures.Balance


01:01:01 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map


01:01:01 HOL-Data_Structures: theory HOL-Data_Structures.Braun_Tree


01:01:02 HOL-Data_Structures: theory HOL-Data_Structures.Array_Braun


01:01:02 HOL-Data_Structures: theory HOL-Number_Theory.Fib


01:01:02 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set


01:01:02 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set


01:01:02 HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue_Specs


01:01:03 HOL-Data_Structures: theory HOL-Data_Structures.Binomial_Heap


01:01:04 HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap


01:01:04 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map


01:01:05 HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join_RBT


01:01:05 HOL-Data_Structures: theory HOL-Data_Structures.Sorting


01:01:07 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map


01:01:08 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set


01:01:08 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map


01:01:25 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map


01:02:17 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Map


01:03:45 Timing HOL-Data_Structures (6 threads, 169.351s elapsed time, 940.220s cpu time, 36.000s GC time, factor 5.55)


01:03:45 Finished HOL-Data_Structures (0:02:50 elapsed time, 0:15:41 cpu time, factor 5.52)


01:03:45 Running HOL-Hoare_Parallel ...


01:03:46 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Graph


01:03:46 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Com


01:03:46 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Quote_Antiquote


01:03:46 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Com


01:03:47 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Tran


01:03:49 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tran


01:03:49 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Hoare


01:03:50 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Hoare


01:03:50 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Syntax


01:03:51 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Examples


01:03:51 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tactics


01:03:51 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Syntax


01:03:52 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Gar_Coll


01:03:52 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Mul_Gar_Coll


01:03:53 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Examples


01:03:57 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Hoare_Parallel


01:04:48 Timing HOL-Hoare_Parallel (6 threads, 61.035s elapsed time, 313.912s cpu time, 5.580s GC time, factor 5.14)


01:04:48 Finished HOL-Hoare_Parallel (0:01:02 elapsed time, 0:05:14 cpu time, factor 5.07)


01:04:48 Building HOL-Library ...


01:04:49 HOL-Library: theory HOL-Library.AList


01:04:49 HOL-Library: theory HOL-Library.Adhoc_Overloading


01:04:49 HOL-Library: theory HOL-Library.BNF_Axiomatization


01:04:49 HOL-Library: theory HOL-Library.BNF_Corec


01:04:49 HOL-Library: theory HOL-Library.Boolean_Algebra


01:04:49 HOL-Library: theory HOL-Library.Bit


01:04:49 HOL-Library: theory HOL-Library.Cancellation


01:04:50 HOL-Library: theory HOL-Library.Monad_Syntax


01:04:50 HOL-Library: theory HOL-Library.State_Monad


01:04:50 HOL-Library: theory HOL-Library.Cardinal_Notations


01:04:50 HOL-Library: theory HOL-Library.Case_Converter


01:04:50 HOL-Library: theory HOL-Library.Char_ord


01:04:50 HOL-Library: theory HOL-Library.Code_Abstract_Nat


01:04:50 HOL-Library: theory HOL-Library.Code_Lazy


01:04:50 HOL-Library: theory HOL-Library.Simps_Case_Conv


01:04:50 HOL-Library: theory HOL-Library.Extended


01:04:50 HOL-Library: theory HOL-Library.Multiset


01:04:51 HOL-Library: theory HOL-Library.Code_Binary_Nat


01:04:51 HOL-Library: theory HOL-Library.Code_Target_Nat


01:04:51 HOL-Library: theory HOL-Library.Code_Prolog


01:04:51 HOL-Library: theory HOL-Library.Code_Target_Int


01:04:51 HOL-Library: theory HOL-Library.DAList


01:04:51 HOL-Library: theory HOL-Library.Code_Target_Numeral


01:04:51 HOL-Library: theory HOL-Library.Code_Test


01:04:52 HOL-Library: theory HOL-Library.Comparator


01:04:52 HOL-Library: theory HOL-Library.Conditional_Parametricity


01:04:52 HOL-Library: theory HOL-Library.Datatype_Records


01:04:53 HOL-Library: theory HOL-Library.Debug


01:04:53 HOL-Library: theory HOL-Library.Disjoint_Sets


01:04:53 HOL-Library: theory HOL-Library.Dlist


01:04:53 HOL-Library: theory HOL-Library.Fun_Lexorder


01:04:53 HOL-Library: theory HOL-Library.FuncSet


01:04:53 HOL-Library: theory HOL-Library.Function_Algebras


01:04:53 HOL-Library: theory HOL-Library.Function_Division


01:04:53 HOL-Library: theory HOL-Library.Groups_Big_Fun


01:04:53 HOL-Library: theory HOL-Library.IArray


01:04:53 HOL-Library: theory HOL-Library.Infinite_Set


01:04:53 HOL-Library: theory HOL-Library.Equipollence


01:04:54 HOL-Library: theory HOL-Library.LaTeXsugar


01:04:54 HOL-Library: theory HOL-Library.Omega_Words_Fun


01:04:54 HOL-Library: theory HOL-Library.Ramsey


01:04:54 HOL-Library: theory HOL-Library.Lattice_Constructions


01:04:54 HOL-Library: theory HOL-Library.Lattice_Syntax


01:04:54 HOL-Library: theory HOL-Library.ListVector


01:04:54 HOL-Library: theory HOL-Library.Combine_PER


01:04:54 HOL-Library: theory HOL-Library.Complete_Partial_Order2


01:04:54 HOL-Library: theory HOL-Library.List_Lexorder


01:04:54 HOL-Library: theory HOL-Library.Mapping


01:04:54 HOL-Library: theory HOL-Library.More_List


01:04:54 HOL-Library: theory HOL-Library.Nat_Bijection


01:04:56 HOL-Library: theory HOL-Library.Stream


01:04:56 HOL-Library: theory HOL-Library.DAList_Multiset


01:04:56 HOL-Library: theory HOL-Library.Multiset_Order


01:04:57 HOL-Library: theory HOL-Library.Permutation


01:04:57 HOL-Library: theory HOL-Library.Permutations


01:04:57 HOL-Library: theory HOL-Library.AList_Mapping


01:04:57 HOL-Library: theory HOL-Library.Old_Datatype


01:04:57 HOL-Library: theory HOL-Library.Old_Recdef


01:04:57 HOL-Library: theory HOL-Library.Open_State_Syntax


01:04:57 HOL-Library: theory HOL-Library.Option_ord


01:04:58 HOL-Library: theory HOL-Library.Parallel


01:04:58 HOL-Library: theory HOL-Library.Pattern_Aliases


01:04:58 HOL-Library: theory HOL-Library.Perm


01:04:58 HOL-Library: theory HOL-Library.Phantom_Type


01:04:58 HOL-Library: theory HOL-Library.Power_By_Squaring


01:04:59 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs


01:04:59 HOL-Library: theory HOL-Library.Preorder


01:04:59 HOL-Library: theory HOL-Library.Product_Lexorder


01:04:59 HOL-Library: theory HOL-Library.Product_Plus


01:04:59 HOL-Library: theory HOL-Library.Quotient_Syntax


01:04:59 HOL-Library: theory HOL-Library.Quotient_Option


01:04:59 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck


01:04:59 HOL-Library: theory HOL-Library.Quotient_Product


01:04:59 HOL-Library: theory HOL-Library.Product_Order


01:04:59 HOL-Library: theory HOL-Library.Quotient_Set


01:04:59 HOL-Library: theory HOL-Library.Quotient_Sum


01:04:59 HOL-Library: theory HOL-Library.Cardinality


01:04:59 HOL-Library: theory HOL-Library.Quotient_List


01:04:59 HOL-Library: theory HOL-Library.Quotient_Type


01:04:59 HOL-Library: theory HOL-Library.RBT_Impl


01:04:59 HOL-Library: theory HOL-Library.Finite_Lattice


01:04:59 HOL-Library: theory HOL-Library.Realizers


01:05:00 HOL-Library: theory HOL-Library.Reflection


01:05:00 HOL-Library: theory HOL-Library.Refute


01:05:00 HOL-Library: theory HOL-Library.Rewrite


01:05:00 HOL-Library: theory HOL-Library.Set_Algebras


01:05:00 HOL-Library: theory HOL-Library.Sorting_Algorithms


01:05:01 HOL-Library: theory HOL-Library.Stirling


01:05:01 HOL-Library: theory HOL-Library.Numeral_Type


01:05:02 HOL-Library: theory HOL-Library.Sublist


01:05:02 HOL-Library: theory HOL-Library.Transitive_Closure_Table


01:05:02 HOL-Library: theory HOL-Library.Tree


01:05:02 HOL-Library: theory HOL-Library.Uprod


01:05:02 HOL-Library: theory HOL-Library.Type_Length


01:05:03 HOL-Library: theory HOL-Library.Saturated


01:05:03 HOL-Library: theory HOL-Library.While_Combinator


01:05:03 HOL-Library: theory HOL-Library.Countable


01:05:03 HOL-Library: theory HOL-Library.Prefix_Order


01:05:03 HOL-Library: theory HOL-Library.Subseq_Order


01:05:03 HOL-Library: theory HOL-Library.BigO


01:05:03 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float


01:05:03 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint


01:05:04 HOL-Library: theory HOL-Library.Diagonal_Subsequence


01:05:04 HOL-Library: theory HOL-Library.Discrete


01:05:04 HOL-Library: theory HOL-Library.Going_To_Filter


01:05:04 HOL-Library: theory HOL-Library.Indicator_Function


01:05:04 HOL-Library: theory HOL-Library.Landau_Symbols


01:05:04 HOL-Library: theory HOL-Library.Countable_Set


01:05:04 HOL-Library: theory HOL-Library.FSet


01:05:05 HOL-Library: theory HOL-Library.Lattice_Algebras


01:05:05 HOL-Library: theory HOL-Library.Tree_Multiset


01:05:05 HOL-Library: theory HOL-Library.Countable_Complete_Lattices


01:05:05 HOL-Library: theory HOL-Library.Countable_Set_Type


01:05:07 HOL-Library: theory HOL-Library.Set_Idioms


01:05:07 HOL-Library: theory HOL-Library.Liminf_Limsup


01:05:07 HOL-Library: theory HOL-Library.Log_Nat


01:05:07 HOL-Library: theory HOL-Library.Lub_Glb


01:05:07 HOL-Library: theory HOL-Library.Multiset_Permutations


01:05:07 HOL-Library: theory HOL-Library.Nonpos_Ints


01:05:08 HOL-Library: theory HOL-Library.OptionalSugar


01:05:08 HOL-Library: theory HOL-Library.Order_Continuity


01:05:08 HOL-Library: theory HOL-Library.Periodic_Fun


01:05:08 HOL-Library: theory HOL-Library.Quadratic_Discriminant


01:05:08 HOL-Library: theory HOL-Library.Finite_Map


01:05:08 HOL-Library: theory HOL-Library.Sum_of_Squares


01:05:08 HOL-Library: theory HOL-Library.Extended_Nat


01:05:08 HOL-Library: theory HOL-Library.Float


01:05:09 HOL-Library: theory HOL-Library.Tree_Real


01:05:09 HOL-Library: theory HOL-Library.Extended_Real


01:05:09 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams


01:05:13 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real


01:05:31 HOL-Library: theory HOL-Library.RBT


01:05:32 HOL-Library: theory HOL-Library.RBT_Mapping


01:05:32 HOL-Library: theory HOL-Library.RBT_Set


01:06:07 HOL-Library FAILED


01:06:07 (see also /media/data/jenkins/workspace/isabelle-nightly-benchmark/heaps/polyml-5.8_x86_64-linux/log/HOL-Library)


01:06:07 ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.rbt_greater_simps_2", "local.rbt_greater_trans"


01:06:07 ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.rbt_greater_simps_2"


01:06:07 ### Metis: Unused theorems: "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_less_trans"


01:06:07 ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.rbt_greater_simps_2", "local.rbt_greater_trans"


01:06:07 ### Metis: Unused theorems: "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_less_trans"


01:06:07 ### Metis: Unused theorems: "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_less_trans"


01:06:07 ### Metis: Unused theorems: "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_3", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_less_trans"


01:06:07 ### Metis: Unused theorems: "local.combine_rbt_greater", "local.combine_rbt_less", "local.ineqs_1", "local.ineqs_2", "local.ineqs_3", "local.ineqs_4", "local.ineqs_5", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_3", "local.ineqs_4", "local.ineqs_5", "local.ineqs_6", "local.rbt_less_simps_2", "local.rbt_greater_simps_2", "local.rbt_less_trans"


01:06:07 ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.rbt_greater_simps_2", "local.rbt_greater_trans"


01:06:07 ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.rbt_greater_simps_2", "local.rbt_greater_trans"


01:06:07 ### Metis: Unused theorems: "local.combine_rbt_greater", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.ineqs_1", "local.ineqs_2", "local.ineqs_4", "local.ineqs_6", "local.rbt_greater_simps_2", "local.rbt_greater_trans"


01:06:07 ### Ignoring duplicate rewrite rule:


01:06:07 ### \<lbrakk>?k1 \<guillemotleft>| ?l1; ?k1 \<guillemotleft>| ?r1\<rbrakk>


01:06:07 ### \<Longrightarrow> ?k1 \<guillemotleft>| combine ?l1 ?r1 \<equiv> True


01:06:07 ### Ignoring duplicate rewrite rule:


01:06:07 ### \<lbrakk>?l1 |\<guillemotleft> ?k1; ?r1 |\<guillemotleft> ?k1\<rbrakk>


01:06:07 ### \<Longrightarrow> combine ?l1 ?r1 |\<guillemotleft> ?k1 \<equiv> True


01:06:07 ### Ignoring duplicate rewrite rule:


01:06:07 ### \<lbrakk>?l1 |\<guillemotleft> ?k1; ?r1 |\<guillemotleft> ?k1\<rbrakk>


01:06:07 ### \<Longrightarrow> combine ?l1 ?r1 |\<guillemotleft> ?k1 \<equiv> True


01:06:07 ### Ignoring duplicate rewrite rule:


01:06:07 ### \<lbrakk>?k1 \<guillemotleft>| ?l1; ?k1 \<guillemotleft>| ?r1\<rbrakk>


01:06:07 ### \<Longrightarrow> ?k1 \<guillemotleft>| combine ?l1 ?r1 \<equiv> True


01:06:07 ### Ignoring duplicate rewrite rule:


01:06:07 ### ?n1 \<le> Suc (length ?kvs1) \<Longrightarrow>


01:06:07 ### entries (fst (rbtreeify_g ?n1 ?kvs1)) \<equiv> take (?n1 - 1) ?kvs1


01:06:07 \<Sqinter> (Sup ` ?A) =


01:06:07 \<Squnion> (Inf ` {f ` ?A |f. \<forall>Y\<in>?A. f Y \<in> Y})


01:06:07 Found termination order:


01:06:07   "(\<lambda>p. size_list size (snd (snd p))) <*mlex*>


01:06:07    (\<lambda>p. size_list size (fst (snd p))) <*mlex*> {}"


01:06:07 Found termination order:


01:06:07   "(\<lambda>p. size_list size (snd (snd p))) <*mlex*>


01:06:07    (\<lambda>p. size_list size (fst (snd p))) <*mlex*> {}"


01:06:07 ### Rule already declared as introduction (intro)


01:06:07 ### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g


01:06:07 ### Introduced fixed type variable(s): 'd in "x__"


01:06:07 *** Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Finite_Map")


01:06:07 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml


01:06:07 *** At command "export_code" (line 1428 of "~~/src/HOL/Library/Finite_Map.thy")


01:06:07 HOL-Auth CANCELLED


01:06:07 HOL-Bali CANCELLED


01:06:07 HOL-Cardinals CANCELLED


01:06:07 HOL-Computational_Algebra CANCELLED


01:06:07 HOL-Algebra CANCELLED


01:06:07 HOL-Corec_Examples CANCELLED


01:06:07 HOL-Datatype_Benchmark CANCELLED


01:06:07 HOL-Datatype_Examples CANCELLED


01:06:07 HOL-Decision_Procs CANCELLED


01:06:07 HOL-IMP CANCELLED


01:06:07 HOL-Imperative_HOL CANCELLED


01:06:07 HOL-Metis_Examples CANCELLED


01:06:07 HOL-MicroJava CANCELLED


01:06:07 HOL-Nominal CANCELLED


01:06:07 HOL-Nominal-Examples CANCELLED


01:06:07 HOL-Nonstandard_Analysis CANCELLED


01:06:07 HOL-Nonstandard_Analysis-Examples CANCELLED


01:06:07 HOL-Number_Theory CANCELLED


01:06:07 HOL-Predicate_Compile_Examples CANCELLED


01:06:07 Building HOL-Probability ...


01:06:08 HOL-Probability: theory HOL-Library.AList


01:06:08 HOL-Probability: theory HOL-Library.Adhoc_Overloading


01:06:08 HOL-Probability: theory HOL-Library.Conditional_Parametricity


01:06:08 HOL-Probability: theory HOL-Library.Lattice_Syntax


01:06:08 HOL-Probability: theory HOL-Library.Mapping


01:06:08 HOL-Probability: theory HOL-Library.Stream


01:06:08 HOL-Probability: theory HOL-Library.Complete_Partial_Order2


01:06:08 HOL-Probability: theory HOL-Library.Monad_Syntax


01:06:09 HOL-Probability: theory HOL-Library.Rewrite


01:06:09 HOL-Probability: theory HOL-Library.Sublist


01:06:09 HOL-Probability: theory HOL-Library.Tree


01:06:10 HOL-Probability: theory HOL-Library.FSet


01:06:10 HOL-Probability: theory HOL-Library.Diagonal_Subsequence


01:06:10 HOL-Probability: theory HOL-Library.Multiset_Permutations


01:06:10 HOL-Probability: theory HOL-Library.AList_Mapping


01:06:10 HOL-Probability: theory HOL-Probability.Discrete_Topology


01:06:11 HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams


01:06:11 HOL-Probability: theory HOL-Probability.Essential_Supremum


01:06:11 HOL-Probability: theory HOL-Probability.Probability_Measure


01:06:11 HOL-Probability: theory HOL-Probability.Stopping_Time


01:06:12 HOL-Probability: theory HOL-Probability.Tree_Space


01:06:13 HOL-Probability: theory HOL-Probability.Conditional_Expectation


01:06:13 HOL-Probability: theory HOL-Probability.Distribution_Functions


01:06:13 HOL-Probability: theory HOL-Probability.Giry_Monad


01:06:13 HOL-Probability: theory HOL-Probability.Weak_Convergence


01:06:13 HOL-Probability: theory HOL-Probability.Helly_Selection


01:06:15 HOL-Probability: theory HOL-Library.Finite_Map


01:06:16 HOL-Probability: theory HOL-Probability.Probability_Mass_Function


01:06:16 HOL-Probability: theory HOL-Probability.Projective_Family


01:06:16 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure


01:06:17 HOL-Probability: theory HOL-Probability.Independent_Family


01:06:17 HOL-Probability: theory HOL-Probability.Stream_Space


01:06:18 HOL-Probability: theory HOL-Probability.PMF_Impl


01:06:18 HOL-Probability: theory HOL-Probability.Random_Permutations


01:06:18 HOL-Probability: theory HOL-Probability.SPMF


01:06:18 HOL-Probability: theory HOL-Probability.Convolution


01:06:18 HOL-Probability: theory HOL-Probability.Information


01:06:21 HOL-Probability: theory HOL-Probability.Distributions


01:06:23 HOL-Probability: theory HOL-Probability.Characteristic_Functions


01:06:23 HOL-Probability: theory HOL-Probability.Sinc_Integral


01:06:23 HOL-Probability: theory HOL-Probability.Levy


01:06:24 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem


01:07:06 HOL-Probability FAILED


01:07:06 (see also /media/data/jenkins/workspace/isabelle-nightly-benchmark/heaps/polyml-5.8_x86_64-linux/log/HOL-Probability)


01:07:06 ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True


01:07:06 ### Ignoring duplicate rewrite rule:


01:07:06 ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True


01:07:06 ### Ignoring duplicate rewrite rule:


01:07:06 ### of_real (?x1 * ?y1) \<equiv> of_real ?x1 * of_real ?y1


01:07:06 ### Ignoring duplicate rewrite rule:


01:07:06 ### \<Prod>x\<in>?A1. ?y1 \<equiv> ?y1 ^ card ?A1


01:07:06 ### Rule already declared as introduction (intro)


01:07:06 ### ((\<lambda>x. x) \<longlongrightarrow> ?a) (at ?a within ?s)


01:07:06 ### Rule already declared as introduction (intro)


01:07:06 ### ((\<lambda>x. ?k) \<longlongrightarrow> ?k) ?F


01:07:06 ### Rule already declared as introduction (intro)


01:07:06 ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow>


01:07:06 ### ((\<lambda>x. ereal (?f x)) \<longlongrightarrow> ereal ?x) ?F


01:07:06 ### Rule already declared as introduction (intro)


01:07:06 ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow>


01:07:06 ### ((\<lambda>x. - ?f x) \<longlongrightarrow> - ?x) ?F


01:07:06 ### Rule already declared as introduction (intro)


01:07:06 ### \<lbrakk>\<bar>?c\<bar> \<noteq> \<infinity>;


01:07:06 ###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>


01:07:06 ### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F


01:07:06 ### Rule already declared as introduction (intro)


01:07:06 ### \<lbrakk>?x \<noteq> 0; (?f \<longlongrightarrow> ?x) ?F\<rbrakk>


01:07:06 ### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F


01:07:06 ### Rule already declared as introduction (intro)


01:07:06 ### \<lbrakk>?y \<noteq> - \<infinity>; ?x \<noteq> - \<infinity>;


01:07:06 ###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>


01:07:06 ### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F


01:07:06 ### Rule already declared as introduction (intro)


01:07:06 ### \<lbrakk>\<bar>?y\<bar> \<noteq> \<infinity>;


01:07:06 ###  (?f \<longlongrightarrow> ?x) ?F\<rbrakk>


01:07:06 ### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F


01:07:06 ### Rule already declared as introduction (intro)


01:07:06 ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow>


01:07:06 ### ((\<lambda>x. ennreal (?f x)) \<longlongrightarrow> ennreal ?x) ?F


01:07:06 *** Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map")


01:07:06 *** Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map")


01:07:06 *** Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit")


01:07:06 *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml


01:07:06 *** At command "export_code" (line 1428 of "~~/src/HOL/Library/Finite_Map.thy")


01:07:06 HOL-Probability-ex CANCELLED


01:07:06 Building HOL-Proofs ...


01:07:09 HOL-Proofs: theory HOL.Code_Generator


01:07:13 HOL-Proofs: theory HOL.HOL


01:07:17 HOL-Proofs: theory HOL.Argo


01:07:17 HOL-Proofs: theory HOL.Ctr_Sugar


01:07:17 HOL-Proofs: theory HOL.Orderings


01:07:20 HOL-Proofs: theory HOL.SAT


01:07:20 HOL-Proofs: theory HOL.Groups


01:07:24 HOL-Proofs: theory HOL.Lattices


01:07:28 HOL-Proofs: theory HOL.Set


01:07:31 HOL-Proofs: theory HOL.Fun


01:07:31 HOL-Proofs: theory HOL.Typedef


01:07:34 HOL-Proofs: theory HOL.Complete_Lattices


01:07:34 HOL-Proofs: theory HOL.Rings


01:07:38 HOL-Proofs: theory HOL.Inductive


01:07:41 HOL-Proofs: theory HOL.Product_Type


01:07:41 HOL-Proofs: theory HOL.Sum_Type


01:07:44 HOL-Proofs: theory HOL.Complete_Partial_Order


01:07:50 HOL-Proofs: theory HOL.Nat


01:07:54 HOL-Proofs: theory HOL.Fields


01:07:54 HOL-Proofs: theory HOL.Meson


01:07:55 HOL-Proofs: theory HOL.ATP


01:07:59 HOL-Proofs: theory HOL.Metis


01:08:01 HOL-Proofs: theory HOL.Finite_Set


01:08:15 HOL-Proofs: theory HOL.Relation


01:08:17 HOL-Proofs: theory HOL.Transitive_Closure


01:08:23 HOL-Proofs: theory HOL.Wellfounded


01:08:24 HOL-Proofs: theory HOL.Fun_Def_Base


01:08:24 HOL-Proofs: theory HOL.Hilbert_Choice


01:08:24 HOL-Proofs: theory HOL.Wfrec


01:08:25 HOL-Proofs: theory HOL.Order_Relation


01:08:26 HOL-Proofs: theory HOL.BNF_Wellorder_Relation


01:08:29 HOL-Proofs: theory HOL.BNF_Wellorder_Embedding


01:08:29 HOL-Proofs: theory HOL.Zorn


01:08:31 HOL-Proofs: theory HOL.BNF_Wellorder_Constructions


01:08:36 HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation


01:08:41 HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic


01:08:42 HOL-Proofs: theory HOL.BNF_Def


01:08:46 HOL-Proofs: theory HOL.BNF_Composition


01:08:46 HOL-Proofs: theory HOL.Basic_BNFs


01:08:47 HOL-Proofs: theory HOL.BNF_Fixpoint_Base


01:08:51 HOL-Proofs: theory HOL.BNF_Least_Fixpoint


01:08:56 HOL-Proofs: theory HOL.Basic_BNF_LFPs


01:08:56 HOL-Proofs: theory HOL.Transfer


01:08:58 HOL-Proofs: theory HOL.Num


01:09:02 HOL-Proofs: theory HOL.Power


01:09:06 HOL-Proofs: theory HOL.Groups_Big


01:09:13 HOL-Proofs: theory HOL.Equiv_Relations


01:09:15 HOL-Proofs: theory HOL.Lifting


01:09:18 HOL-Proofs: theory HOL.Lifting_Set


01:09:18 HOL-Proofs: theory HOL.Option


01:09:18 HOL-Proofs: theory HOL.Quotient


01:09:19 HOL-Proofs: theory HOL.Extraction


01:09:19 HOL-Proofs: theory HOL.Lattices_Big


01:09:19 HOL-Proofs: theory HOL.Partial_Function


01:09:21 HOL-Proofs: theory HOL.Fun_Def


01:09:24 HOL-Proofs: theory HOL.Int


01:09:31 HOL-Proofs: theory HOL.Euclidean_Division


01:09:41 HOL-Proofs: theory HOL.Parity


01:09:46 HOL-Proofs: theory HOL.Divides


01:09:52 HOL-Proofs: theory HOL.Code_Numeral


01:09:52 HOL-Proofs: theory HOL.Numeral_Simprocs


01:09:52 HOL-Proofs: theory HOL.SMT


01:09:52 HOL-Proofs: theory HOL.Set_Interval


01:09:59 HOL-Proofs: theory HOL.Semiring_Normalization


01:10:02 HOL-Proofs: theory HOL.Groebner_Basis


01:10:08 HOL-Proofs: theory HOL.Conditionally_Complete_Lattices


01:10:08 HOL-Proofs: theory HOL.Presburger


01:10:08 HOL-Proofs: theory HOL.Filter


01:10:19 HOL-Proofs: theory HOL.Sledgehammer


01:10:22 HOL-Proofs: theory HOL.List


01:11:40 HOL-Proofs: theory HOL.Groups_List


01:11:40 HOL-Proofs: theory HOL.Map


01:11:42 HOL-Proofs: theory HOL.Factorial


01:11:42 HOL-Proofs: theory HOL.GCD


01:11:42 HOL-Proofs: theory HOL.Random


01:11:44 HOL-Proofs: theory HOL.Enum


01:11:45 HOL-Proofs: theory HOL.Binomial


01:12:09 HOL-Proofs: theory HOL.String


01:13:05 HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint


01:13:13 HOL-Proofs: theory HOL.Predicate


01:13:14 HOL-Proofs: theory HOL.Typerep


01:13:19 HOL-Proofs: theory HOL.Lazy_Sequence


01:13:22 HOL-Proofs: theory HOL.Limited_Sequence


01:13:22 HOL-Proofs: theory HOL.Code_Evaluation


01:13:25 HOL-Proofs: theory HOL.Quickcheck_Random


01:13:30 HOL-Proofs: theory HOL.Quickcheck_Exhaustive


01:13:30 HOL-Proofs: theory HOL.Quickcheck_Narrowing


01:13:30 HOL-Proofs: theory HOL.Random_Pred


01:13:35 HOL-Proofs: theory HOL.Random_Sequence


01:15:13 HOL-Proofs: theory HOL.Record


01:15:13 HOL-Proofs: theory HOL.Predicate_Compile


01:15:15 HOL-Proofs: theory HOL.Nitpick


01:15:23 HOL-Proofs: theory HOL.Nunchaku


01:15:24 HOL-Proofs: theory Main


01:15:26 HOL-Proofs: theory HOL-Library.Realizers


01:19:49 Timing HOL-Proofs (6 threads, 723.611s elapsed time, 1792.740s cpu time, 434.900s GC time, factor 2.48)


01:19:49 Finished HOL-Proofs (0:12:40 elapsed time, 0:31:09 cpu time, factor 2.46)


01:19:49 Running HOL-Proofs-Extraction ...


01:19:50 HOL-Proofs-Extraction: theory HOL-Library.Cancellation


01:19:50 HOL-Proofs-Extraction: theory HOL-Library.Code_Abstract_Nat


01:19:50 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Int


01:19:50 HOL-Proofs-Extraction: theory HOL-Library.Open_State_Syntax


01:19:50 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Warshall


01:19:50 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman


01:19:50 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Nat


01:19:50 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Util


01:19:51 HOL-Proofs-Extraction: theory HOL-Library.Multiset


01:19:51 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Numeral


01:19:51 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.QuotRem


01:19:51 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Pigeonhole


01:19:51 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman_Extraction


01:19:55 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Greatest_Common_Divisor


01:20:12 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Factorial_Ring


01:20:26 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Euclidean_Algorithm


01:20:35 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Primes


01:20:47 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Euclid


01:21:19 Timing HOL-Proofs-Extraction (6 threads, 88.700s elapsed time, 195.020s cpu time, 10.500s GC time, factor 2.20)


01:21:19 Finished HOL-Proofs-Extraction (0:01:29 elapsed time, 0:03:16 cpu time, factor 2.18)


01:21:19 Running HOL-Proofs-Lambda ...


01:21:20 HOL-Proofs-Lambda: theory HOL-Library.Code_Target_Int


01:21:20 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Commutation


01:21:20 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Lambda


01:21:20 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListOrder


01:21:22 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListApplication


01:21:22 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ParRed


01:21:23 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.LambdaType


01:21:23 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListBeta


01:21:24 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Eta


01:21:24 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.InductTermi


01:21:24 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.NormalForm


01:21:25 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.StrongNorm


01:21:25 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Standardization


01:21:25 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.WeakNorm


01:23:06 Timing HOL-Proofs-Lambda (6 threads, 104.932s elapsed time, 138.824s cpu time, 5.764s GC time, factor 1.32)


01:23:06 Finished HOL-Proofs-Lambda (0:01:46 elapsed time, 0:02:19 cpu time, factor 1.32)


01:23:06 HOL-Quickcheck_Benchmark CANCELLED


01:23:06 HOL-Quickcheck_Examples CANCELLED


01:23:06 HOL-Quotient_Examples CANCELLED


01:23:06 Running HOL-Record_Benchmark ...


01:23:06 HOL-Record_Benchmark: theory HOL-Record_Benchmark.Record_Benchmark


01:25:42 Timing HOL-Record_Benchmark (6 threads, 154.562s elapsed time, 235.288s cpu time, 12.824s GC time, factor 1.52)


01:25:42 Finished HOL-Record_Benchmark (0:02:35 elapsed time, 0:03:56 cpu time, factor 1.52)


01:25:42 HOL-SET_Protocol CANCELLED


01:25:42 HOL-UNITY CANCELLED


01:25:42 Building HOL-Word ...


01:25:43 HOL-Word: theory HOL-Library.Bit


01:25:43 HOL-Word: theory HOL-Library.Boolean_Algebra


01:25:43 HOL-Word: theory HOL-Library.Phantom_Type


01:25:43 HOL-Word: theory HOL-Word.Bits


01:25:43 HOL-Word: theory HOL-Word.Misc_Numeric


01:25:43 HOL-Word: theory HOL-Word.Misc_Typedef


01:25:43 HOL-Word: theory HOL-Word.Bit_Representation


01:25:43 HOL-Word: theory HOL-Word.Bits_Bit


01:25:43 HOL-Word: theory HOL-Word.Word_Miscellaneous


01:25:43 HOL-Word: theory HOL-Word.Bits_Int


01:25:43 HOL-Word: theory HOL-Library.Cardinality


01:25:45 HOL-Word: theory HOL-Library.Numeral_Type


01:25:45 HOL-Word: theory HOL-Word.Bit_Comparison


01:25:45 HOL-Word: theory HOL-Word.Bool_List_Representation


01:25:46 HOL-Word: theory HOL-Library.Type_Length


01:25:46 HOL-Word: theory HOL-Word.Word


01:25:51 HOL-Word: theory HOL-Word.WordBitwise


01:25:51 HOL-Word: theory HOL-Word.WordExamples


01:26:00 Timing HOL-Word (6 threads, 9.802s elapsed time, 48.876s cpu time, 2.128s GC time, factor 4.99)


01:26:00 Finished HOL-Word (0:00:17 elapsed time, 0:01:03 cpu time, factor 3.70)


01:26:00 Running HOL-Word-SMT_Examples ...


01:26:00 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.Boogie


01:26:00 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Word_Examples


01:26:00 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Examples


01:26:00 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Tests


01:27:01 Timing HOL-Word-SMT_Examples (6 threads, 59.577s elapsed time, 86.088s cpu time, 0.868s GC time, factor 1.44)


01:27:01 Finished HOL-Word-SMT_Examples (0:01:00 elapsed time, 0:01:29 cpu time, factor 1.48)


01:27:01 HOL-ex CANCELLED


01:27:01 Building HOLCF ...


01:27:01 HOLCF: theory HOL-Library.Nat_Bijection


01:27:01 HOLCF: theory HOL-Library.Old_Datatype


01:27:01 HOLCF: theory HOLCF.Porder


01:27:02 HOLCF: theory HOLCF.Pcpo


01:27:02 HOLCF: theory HOL-Library.Countable


01:27:03 HOLCF: theory HOLCF.Cont


01:27:03 HOLCF: theory HOLCF.Adm


01:27:03 HOLCF: theory HOLCF.Discrete


01:27:03 HOLCF: theory HOLCF.Cpodef


01:27:03 HOLCF: theory HOLCF.Fun_Cpo


01:27:03 HOLCF: theory HOLCF.Product_Cpo


01:27:04 HOLCF: theory HOLCF.Cfun


01:27:04 HOLCF: theory HOLCF.Completion


01:27:04 HOLCF: theory HOLCF.Cprod


01:27:04 HOLCF: theory HOLCF.Deflation


01:27:04 HOLCF: theory HOLCF.Fix


01:27:04 HOLCF: theory HOLCF.Sfun


01:27:04 HOLCF: theory HOLCF.Sprod


01:27:04 HOLCF: theory HOLCF.Up


01:27:05 HOLCF: theory HOLCF.Lift


01:27:06 HOLCF: theory HOLCF.One


01:27:06 HOLCF: theory HOLCF.Tr


01:27:06 HOLCF: theory HOLCF.Ssum


01:27:06 HOLCF: theory HOLCF.Fixrec


01:27:06 HOLCF: theory HOLCF.Map_Functions


01:27:07 HOLCF: theory HOLCF.Bifinite


01:27:07 HOLCF: theory HOLCF.Domain_Aux


01:27:08 HOLCF: theory HOLCF.Universal


01:27:09 HOLCF: theory HOLCF.Algebraic


01:27:09 HOLCF: theory HOLCF.Compact_Basis


01:27:09 HOLCF: theory HOLCF.LowerPD


01:27:09 HOLCF: theory HOLCF.UpperPD


01:27:10 HOLCF: theory HOLCF.Representable


01:27:10 HOLCF: theory HOLCF.ConvexPD


01:27:12 HOLCF: theory HOLCF.Domain


01:27:13 HOLCF: theory HOLCF.Powerdomains


01:27:14 HOLCF: theory HOLCF


01:27:22 Timing HOLCF (6 threads, 12.575s elapsed time, 39.664s cpu time, 2.348s GC time, factor 3.15)


01:27:22 Finished HOLCF (0:00:20 elapsed time, 0:00:57 cpu time, factor 2.73)


01:27:22 Running IOA ...


01:27:23 IOA: theory IOA.Seq


01:27:23 IOA: theory IOA.Asig


01:27:23 IOA: theory IOA.Pred


01:27:23 IOA: theory IOA.Automata


01:27:24 IOA: theory IOA.Sequence


01:27:25 IOA: theory IOA.Traces


01:27:25 IOA: theory IOA.TL


01:27:26 IOA: theory IOA.CompoExecs


01:27:26 IOA: theory IOA.RefMappings


01:27:26 IOA: theory IOA.ShortExecutions


01:27:26 IOA: theory IOA.RefCorrectness


01:27:26 IOA: theory IOA.CompoScheds


01:27:26 IOA: theory IOA.Simulations


01:27:26 IOA: theory IOA.SimCorrectness


01:27:27 IOA: theory IOA.Deadlock


01:27:27 IOA: theory IOA.CompoTraces


01:27:28 IOA: theory IOA.Compositionality


01:27:28 IOA: theory IOA.IOA


01:27:28 IOA: theory IOA.TLS


01:27:29 IOA: theory IOA.LiveIOA


01:27:29 IOA: theory IOA.Abstraction


01:27:31 Timing IOA (6 threads, 7.683s elapsed time, 32.800s cpu time, 1.372s GC time, factor 4.27)


01:27:31 Finished IOA (0:00:08 elapsed time, 0:00:33 cpu time, factor 3.83)


01:27:31 Building ZF ...


01:27:32 ZF: theory IFOL


01:27:33 ZF: theory FOL


01:27:35 ZF: theory ZF.ZF_Base


01:27:36 ZF: theory ZF.upair


01:27:36 ZF: theory ZF.pair


01:27:36 ZF: theory ZF.Bool


01:27:36 ZF: theory ZF.equalities


01:27:37 ZF: theory ZF.Fixedpt


01:27:37 ZF: theory ZF.Sum


01:27:37 ZF: theory ZF.func


01:27:37 ZF: theory ZF.Perm


01:27:37 ZF: theory ZF.QPair


01:27:38 ZF: theory ZF.Trancl


01:27:38 ZF: theory ZF.EquivClass


01:27:38 ZF: theory ZF.WF


01:27:38 ZF: theory ZF.Order


01:27:38 ZF: theory ZF.Ordinal


01:27:38 ZF: theory ZF.OrdQuant


01:27:39 ZF: theory ZF.Nat


01:27:39 ZF: theory ZF.OrderArith


01:27:39 ZF: theory ZF.Epsilon


01:27:39 ZF: theory ZF.Inductive


01:27:39 ZF: theory ZF.OrderType


01:27:40 ZF: theory ZF.Finite


01:27:40 ZF: theory ZF.Cardinal


01:27:40 ZF: theory ZF.Univ


01:27:41 ZF: theory ZF.Arith


01:27:41 ZF: theory ZF.QUniv


01:27:41 ZF: theory ZF.Datatype


01:27:41 ZF: theory ZF.ArithSimp


01:27:41 ZF: theory ZF.Int


01:27:41 ZF: theory ZF.CardinalArith


01:27:41 ZF: theory ZF.List


01:27:42 ZF: theory ZF.Bin


01:27:43 ZF: theory ZF.IntDiv


01:27:43 ZF: theory ZF


01:27:44 ZF: theory ZF.AC


01:27:44 ZF: theory ZF.Zorn


01:27:44 ZF: theory ZF.Cardinal_AC


01:27:44 ZF: theory ZF.InfDatatype


01:27:44 ZF: theory ZFC


01:27:47 Timing ZF (6 threads, 13.363s elapsed time, 47.776s cpu time, 3.200s GC time, factor 3.58)


01:27:47 Finished ZF (0:00:15 elapsed time, 0:00:51 cpu time, factor 3.40)


01:27:47 Building ZF-Induct ...


01:27:47 ZF-Induct: theory ZF-Induct.Acc


01:27:47 ZF-Induct: theory ZF-Induct.Comb


01:27:47 ZF-Induct: theory ZF-Induct.Binary_Trees


01:27:47 ZF-Induct: theory ZF-Induct.Datatypes


01:27:47 ZF-Induct: theory ZF-Induct.ListN


01:27:47 ZF-Induct: theory ZF-Induct.FoldSet


01:27:47 ZF-Induct: theory ZF-Induct.Mutil


01:27:47 ZF-Induct: theory ZF-Induct.Ntree


01:27:47 ZF-Induct: theory ZF-Induct.Primrec


01:27:47 ZF-Induct: theory ZF-Induct.PropLog


01:27:47 ZF-Induct: theory ZF-Induct.Rmap


01:27:47 ZF-Induct: theory ZF-Induct.Term


01:27:47 ZF-Induct: theory ZF-Induct.Tree_Forest


01:27:47 ZF-Induct: theory ZF-Induct.Multiset


01:27:47 ZF-Induct: theory ZF-Induct.Brouwer


01:27:52 Timing ZF-Induct (6 threads, 3.418s elapsed time, 13.156s cpu time, 0.584s GC time, factor 3.85)


01:27:52 Finished ZF-Induct (0:00:05 elapsed time, 0:00:17 cpu time, factor 3.37)


01:27:52 Running ZF-UNITY ...


01:27:53 ZF-UNITY: theory ZF-UNITY.MultisetSum


01:27:53 ZF-UNITY: theory ZF-UNITY.State


01:27:53 ZF-UNITY: theory ZF-UNITY.GenPrefix


01:27:53 ZF-UNITY: theory ZF-UNITY.UNITY


01:27:53 ZF-UNITY: theory ZF-UNITY.Monotonicity


01:27:53 ZF-UNITY: theory ZF-UNITY.Constrains


01:27:53 ZF-UNITY: theory ZF-UNITY.FP


01:27:53 ZF-UNITY: theory ZF-UNITY.WFair


01:27:53 ZF-UNITY: theory ZF-UNITY.Increasing


01:27:54 ZF-UNITY: theory ZF-UNITY.SubstAx


01:27:54 ZF-UNITY: theory ZF-UNITY.Follows


01:27:54 ZF-UNITY: theory ZF-UNITY.Mutex


01:27:54 ZF-UNITY: theory ZF-UNITY.Union


01:27:54 ZF-UNITY: theory ZF-UNITY.Comp


01:27:55 ZF-UNITY: theory ZF-UNITY.Guar


01:27:55 ZF-UNITY: theory ZF-UNITY.AllocBase


01:27:55 ZF-UNITY: theory ZF-UNITY.ClientImpl


01:27:55 ZF-UNITY: theory ZF-UNITY.Distributor


01:27:55 ZF-UNITY: theory ZF-UNITY.AllocImpl


01:27:55 ZF-UNITY: theory ZF-UNITY.Merge


01:27:59 Timing ZF-UNITY (6 threads, 6.282s elapsed time, 32.904s cpu time, 1.596s GC time, factor 5.24)


01:27:59 Finished ZF-UNITY (0:00:06 elapsed time, 0:00:33 cpu time, factor 4.88)


01:27:59 Unfinished session(s): HOL-Algebra, HOL-Auth, HOL-Bali, HOL-Cardinals, HOL-Computational_Algebra, HOL-Corec_Examples, HOL-Datatype_Benchmark, HOL-Datatype_Examples, HOL-Decision_Procs, HOL-IMP, HOL-Imperative_HOL, HOL-Library, HOL-Metis_Examples, HOL-MicroJava, HOL-Nominal, HOL-Nominal-Examples, HOL-Nonstandard_Analysis, HOL-Nonstandard_Analysis-Examples, HOL-Number_Theory, HOL-Predicate_Compile_Examples, HOL-Probability, HOL-Probability-ex, HOL-Quickcheck_Benchmark, HOL-Quickcheck_Examples, HOL-Quotient_Examples, HOL-SET_Protocol, HOL-UNITY, HOL-ex


01:27:59 

01:27:59 === TIMING ===


01:27:59 

01:27:59 Group main: 0:12:25 elapsed time, 0:54:29 cpu time, factor 4.39


01:27:59 Group timing: 0:30:06 elapsed time, 1:43:28 cpu time, factor 3.44


01:27:59 Overall: 0:36:57 elapsed time, 1:59:23 cpu time, factor 3.23


01:27:59 

01:27:59 === FAILED SESSIONS ===


01:27:59 

01:27:59 Session HOL-Probability: FAILED 2


01:27:59 Session HOL-Predicate_Compile_Examples: CANCELLED


01:27:59 Session HOL-Nonstandard_Analysis-Examples: CANCELLED


01:27:59 Session HOL-Nominal: CANCELLED


01:27:59 Session HOL-Datatype_Examples: CANCELLED


01:27:59 Session HOL-Cardinals: CANCELLED


01:27:59 Session HOL-Nominal-Examples: CANCELLED


01:27:59 Session HOL-Auth: CANCELLED


01:27:59 Session HOL-MicroJava: CANCELLED


01:27:59 Session HOL-Corec_Examples: CANCELLED


01:27:59 Session HOL-Bali: CANCELLED


01:27:59 Session HOL-Quickcheck_Benchmark: CANCELLED


01:27:59 Session HOL-UNITY: CANCELLED


01:27:59 Session HOL-ex: CANCELLED


01:27:59 Session HOL-Quickcheck_Examples: CANCELLED


01:27:59 Session HOL-Imperative_HOL: CANCELLED


01:27:59 Session HOL-Probability-ex: CANCELLED


01:27:59 Session HOL-Metis_Examples: CANCELLED


01:27:59 Session HOL-IMP: CANCELLED


01:27:59 Session HOL-Datatype_Benchmark: CANCELLED


01:27:59 Session HOL-SET_Protocol: CANCELLED


01:27:59 Session HOL-Number_Theory: CANCELLED


01:27:59 Session HOL-Decision_Procs: CANCELLED


01:27:59 Session HOL-Library: FAILED 2


01:27:59 Session HOL-Quotient_Examples: CANCELLED


01:27:59 Session HOL-Nonstandard_Analysis: CANCELLED


01:27:59 Session HOL-Computational_Algebra: CANCELLED


01:27:59 Session HOL-Algebra: CANCELLED


01:27:59 Build step 'Execute shell' marked build as failure


01:27:59 Archiving artifacts


01:28:00 Started calculate disk usage of build


01:28:00 Finished Calculation of disk usage of build in 0 seconds


01:28:09 Started calculate disk usage of workspace


01:28:09 Finished Calculation of disk usage of workspace in 0 seconds


01:28:09 No emails were triggered.


01:28:09 Finished: FAILURE