Started by an SCM change [EnvInject] - Loading node environment variables. Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-nightly-benchmark [isabelle-nightly-benchmark] $ hg showconfig paths.default [isabelle-nightly-benchmark] $ hg pull --rev default pulling from http://isabelle.in.tum.de/repos/isabelle/ searching for changes no changes found [isabelle-nightly-benchmark] $ hg update --clean --rev default 14 files updated, 0 files merged, 1 files removed, 0 files unresolved [isabelle-nightly-benchmark] $ hg --config extensions.purge= clean --all [isabelle-nightly-benchmark] $ hg log --rev . --template {node} [isabelle-nightly-benchmark] $ hg log --rev . --template {rev} [isabelle-nightly-benchmark] $ hg log --rev 63721ee8c86c528b5fe5f3dce27cd56efc2315a5 --template exists\n exists [isabelle-nightly-benchmark] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(63721ee8c86c528b5fe5f3dce27cd56efc2315a5)" --encoding UTF-8 --encodingmode replace No emails were triggered. [isabelle-nightly-benchmark] $ /bin/sh -xe /tmp/jenkins386781598375730483.sh + Admin/jenkins/run_build benchmark + set -e + PROFILE=benchmark + shift + bin/isabelle components -a + bin/isabelle jedit -bf ### Building graph browser ... warning: [options] bootstrap class path not set in conjunction with -source 6 warning: [options] source value 6 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. Note: Some input files use or override a deprecated API. Note: Recompile with -Xlint:deprecation for details. Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. 3 warnings ### Building Isabelle/Scala ... ### Building Isabelle/jEdit ... + bin/isabelle ocaml_setup # To setup the new switch in the current shell, you need to run: eval `opam config env` + bin/isabelle ghc_setup stack will use a sandboxed GHC it installed For more information on paths, see 'stack path' and 'stack exec env' To use this GHC and packages outside of a project, consider using: stack ghc, stack ghci, stack runghc, or stack exec The Glorious Glasgow Haskell Compilation System, version 8.4.4 + bin/isabelle ci_build_benchmark === CONFIGURATION === ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64-linux" ML_SYSTEM="polyml-5.8" ML_OPTIONS="-H 4000 --maxheap 8G" jobs = 1, threads = 6, numa = false === BUILD === Build started at Wed, 13 Mar 2019 23:51:02 GMT Isabelle id 4343c1bfa52d === LOG === Session Pure/Pure Session FOL/FOL Session HOL/HOL (main) Session HOL/HOL-Eisbach Session HOL/HOL-Hoare_Parallel (timing) Session HOL/HOL-Library (main timing) Session HOL/HOL-Auth (timing) Session HOL/HOL-UNITY (timing) Session HOL/HOL-Bali (timing) Session HOL/HOL-Cardinals (timing) Session HOL/HOL-Computational_Algebra (main timing) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Decision_Procs (timing) Session HOL/HOL-Quotient_Examples (timing) Session HOL/HOL-Analysis (main timing) Session HOL/HOL-Probability (main timing) Session HOL/HOL-Probability-ex (timing) Session HOL/HOL-Nonstandard_Analysis (timing) Session HOL/HOL-Nonstandard_Analysis-Examples (timing) Session HOL/HOL-Number_Theory (main timing) Session HOL/HOL-Data_Structures (timing) Session HOL/HOL-ex (timing) Session HOL/HOL-Corec_Examples (timing) Session HOL/HOL-Datatype_Benchmark Session HOL/HOL-Datatype_Examples (timing) Session HOL/HOL-IMP (timing) Session HOL/HOL-Imperative_HOL (timing) Session HOL/HOL-Metis_Examples (timing) Session HOL/HOL-MicroJava (timing) Session HOL/HOL-Nominal Session HOL/HOL-Nominal-Examples (timing) Session HOL/HOL-Predicate_Compile_Examples (timing) Session HOL/HOL-Quickcheck_Benchmark Session HOL/HOL-Quickcheck_Examples (timing) Session HOL/HOL-SET_Protocol (timing) Session HOL/HOL-Record_Benchmark Session HOL/HOL-Word (main timing) Session HOL/HOL-Word-SMT_Examples (timing) Session HOL/HOLCF (main timing) Session HOL/IOA (timing) Session HOL/HOL-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-Lambda (timing) Session ZF/ZF (main timing) Session ZF/ZF-Induct Session ZF/ZF-UNITY (timing) Building Pure ... Pure: theory Pure Pure: theory ML_Bootstrap Pure: theory Pure.Sessions Timing Pure (1 threads, 1.059s elapsed time, 1.064s cpu time, 0.000s GC time, factor 1.00) Finished Pure (0:00:22 elapsed time, 0:00:22 cpu time, factor 1.00) Building HOL ... HOL: theory HOL.Code_Generator HOL: theory HOL.HOL HOL: theory HOL.Argo HOL: theory HOL.Ctr_Sugar HOL: theory HOL.Orderings HOL: theory HOL.Groups HOL: theory HOL.SAT HOL: theory HOL.Lattices HOL: theory HOL.Set HOL: theory HOL.Fun HOL: theory HOL.Typedef HOL: theory HOL.Complete_Lattices HOL: theory HOL.Rings HOL: theory HOL.Inductive HOL: theory HOL.Product_Type HOL: theory HOL.Sum_Type HOL: theory HOL.Complete_Partial_Order HOL: theory HOL.Nat HOL: theory HOL.Fields HOL: theory HOL.Meson HOL: theory HOL.ATP HOL: theory HOL.Metis HOL: theory HOL.Finite_Set HOL: theory HOL.Relation HOL: theory HOL.Transitive_Closure HOL: theory HOL.Wellfounded HOL: theory HOL.Fun_Def_Base HOL: theory HOL.Hilbert_Choice HOL: theory HOL.Wfrec HOL: theory HOL.Order_Relation HOL: theory HOL.BNF_Wellorder_Relation HOL: theory HOL.BNF_Wellorder_Embedding HOL: theory HOL.Zorn HOL: theory HOL.BNF_Wellorder_Constructions HOL: theory HOL.BNF_Cardinal_Order_Relation HOL: theory HOL.BNF_Cardinal_Arithmetic HOL: theory HOL.BNF_Def HOL: theory HOL.BNF_Composition HOL: theory HOL.Basic_BNFs HOL: theory HOL.BNF_Fixpoint_Base HOL: theory HOL.BNF_Least_Fixpoint HOL: theory HOL.Basic_BNF_LFPs HOL: theory HOL.Transfer HOL: theory HOL.Num HOL: theory HOL.Power HOL: theory HOL.Groups_Big HOL: theory HOL.Equiv_Relations HOL: theory HOL.Lifting HOL: theory HOL.Lifting_Set HOL: theory HOL.Option HOL: theory HOL.Quotient HOL: theory HOL.Extraction HOL: theory HOL.Lattices_Big HOL: theory HOL.Partial_Function HOL: theory HOL.Fun_Def HOL: theory HOL.Int HOL: theory HOL.Euclidean_Division HOL: theory HOL.Parity HOL: theory HOL.Divides HOL: theory HOL.Code_Numeral HOL: theory HOL.Numeral_Simprocs HOL: theory HOL.SMT HOL: theory HOL.Set_Interval HOL: theory HOL.Semiring_Normalization HOL: theory HOL.Groebner_Basis HOL: theory HOL.Conditionally_Complete_Lattices HOL: theory HOL.Filter HOL: theory HOL.Presburger HOL: theory HOL.Sledgehammer HOL: theory HOL.List HOL: theory HOL.Groups_List HOL: theory HOL.Map HOL: theory HOL.Factorial HOL: theory HOL.GCD HOL: theory HOL.Enum HOL: theory HOL.Random HOL: theory HOL.Binomial HOL: theory HOL.String HOL: theory HOL.BNF_Greatest_Fixpoint HOL: theory HOL.Predicate HOL: theory HOL.Typerep HOL: theory HOL.Lazy_Sequence HOL: theory HOL.Limited_Sequence HOL: theory HOL.Code_Evaluation HOL: theory HOL.Quickcheck_Random HOL: theory HOL.Quickcheck_Exhaustive HOL: theory HOL.Quickcheck_Narrowing HOL: theory HOL.Random_Pred HOL: theory HOL.Random_Sequence HOL: theory HOL.Record HOL: theory HOL.Predicate_Compile HOL: theory HOL.Nitpick HOL: theory HOL.Nunchaku HOL: theory Main HOL: theory HOL.Archimedean_Field HOL: theory HOL.Hull HOL: theory HOL.Topological_Spaces HOL: theory HOL.Modules HOL: theory HOL.Vector_Spaces HOL: theory HOL.Rat HOL: theory HOL.Real HOL: theory HOL.Real_Vector_Spaces HOL: theory HOL.Inequalities HOL: theory HOL.Limits HOL: theory HOL.Deriv HOL: theory HOL.Series HOL: theory HOL.NthRoot HOL: theory HOL.Transcendental HOL: theory HOL.Complex HOL: theory HOL.MacLaurin HOL: theory Complex_Main Timing HOL (6 threads, 178.242s elapsed time, 625.900s cpu time, 37.940s GC time, factor 3.51) Finished HOL (0:03:24 elapsed time, 0:11:20 cpu time, factor 3.33) Building HOL-Analysis ... HOL-Analysis: theory HOL-Library.Cancellation HOL-Analysis: theory HOL-Library.FuncSet HOL-Analysis: theory HOL-Library.Disjoint_Sets HOL-Analysis: theory HOL-Library.Infinite_Set HOL-Analysis: theory HOL-Library.Nat_Bijection HOL-Analysis: theory HOL-Library.Old_Datatype HOL-Analysis: theory HOL-Library.Phantom_Type HOL-Analysis: theory HOL-Library.Product_Plus HOL-Analysis: theory HOL-Library.Product_Order HOL-Analysis: theory HOL-Library.Set_Algebras HOL-Analysis: theory HOL-Analysis.Inner_Product HOL-Analysis: theory HOL-Library.Countable HOL-Analysis: theory HOL-Library.Multiset HOL-Analysis: theory HOL-Analysis.L2_Norm HOL-Analysis: theory HOL-Analysis.Operator_Norm HOL-Analysis: theory HOL-Analysis.Poly_Roots HOL-Analysis: theory HOL-Analysis.Product_Vector HOL-Analysis: theory HOL-Library.Cardinality HOL-Analysis: theory HOL-Library.Discrete HOL-Analysis: theory HOL-Library.Indicator_Function HOL-Analysis: theory HOL-Library.Liminf_Limsup HOL-Analysis: theory HOL-Library.Nonpos_Ints HOL-Analysis: theory HOL-Library.Countable_Set HOL-Analysis: theory HOL-Library.Periodic_Fun HOL-Analysis: theory HOL-Analysis.Euclidean_Space HOL-Analysis: theory HOL-Library.Numeral_Type HOL-Analysis: theory HOL-Library.Sum_of_Squares HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices HOL-Analysis: theory HOL-Library.Set_Idioms HOL-Analysis: theory HOL-Analysis.Abstract_Topology HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable HOL-Analysis: theory HOL-Analysis.Elementary_Topology HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product HOL-Analysis: theory HOL-Analysis.Linear_Algebra HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring HOL-Analysis: theory HOL-Library.Permutations HOL-Analysis: theory HOL-Analysis.Abstract_Limits HOL-Analysis: theory HOL-Analysis.Convex HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2 HOL-Analysis: theory HOL-Library.Order_Continuity HOL-Analysis: theory HOL-Analysis.Cartesian_Space HOL-Analysis: theory HOL-Analysis.Norm_Arith HOL-Analysis: theory HOL-Library.Extended_Nat HOL-Analysis: theory HOL-Analysis.Connected HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces HOL-Analysis: theory HOL-Library.Extended_Real HOL-Analysis: theory HOL-Analysis.Determinants HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Tagged_Division HOL-Analysis: theory HOL-Analysis.Sigma_Algebra HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits HOL-Analysis: theory HOL-Analysis.Starlike HOL-Analysis: theory HOL-Analysis.Summation_Tests HOL-Analysis: theory HOL-Analysis.Uniform_Limit HOL-Analysis: theory HOL-Analysis.Measurable HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function HOL-Analysis: theory HOL-Analysis.Measure_Space HOL-Analysis: theory HOL-Analysis.Continuous_Extension HOL-Analysis: theory HOL-Analysis.Path_Connected HOL-Analysis: theory HOL-Computational_Algebra.Primes HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series HOL-Analysis: theory HOL-Analysis.Homotopy HOL-Analysis: theory HOL-Analysis.Caratheodory HOL-Analysis: theory HOL-Analysis.Homeomorphism HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint HOL-Analysis: theory HOL-Analysis.Derivative HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems HOL-Analysis: theory HOL-Analysis.Cross3 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Polytope HOL-Analysis: theory HOL-Analysis.Arcwise_Connected HOL-Analysis: theory HOL-Analysis.Borel_Space HOL-Analysis: theory HOL-Analysis.Lipschitz HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration HOL-Analysis: theory HOL-Analysis.Regularity HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure HOL-Analysis: theory HOL-Analysis.Embed_Measure HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure HOL-Analysis: theory HOL-Analysis.Bochner_Integration HOL-Analysis: theory HOL-Analysis.Function_Topology HOL-Analysis: theory HOL-Analysis.T1_Spaces HOL-Analysis: theory HOL-Analysis.Complete_Measure HOL-Analysis: theory HOL-Analysis.Radon_Nikodym HOL-Analysis: theory HOL-Analysis.Set_Integral HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration HOL-Analysis: theory HOL-Analysis.Integral_Test HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics HOL-Analysis: theory HOL-Analysis.Improper_Integral HOL-Analysis: theory HOL-Analysis.Interval_Integral HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution HOL-Analysis: theory HOL-Analysis.Complex_Transcendental HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem HOL-Analysis: theory HOL-Analysis.Infinite_Products HOL-Analysis: theory HOL-Analysis.Further_Topology HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers HOL-Analysis: theory HOL-Analysis.Jordan_Curve HOL-Analysis: theory HOL-Analysis.Conformal_Mappings HOL-Analysis: theory HOL-Analysis.FPS_Convergence HOL-Analysis: theory HOL-Analysis.Great_Picard HOL-Analysis: theory HOL-Analysis.Gamma_Function HOL-Analysis: theory HOL-Analysis.Riemann_Mapping HOL-Analysis: theory HOL-Analysis.Winding_Numbers HOL-Analysis: theory HOL-Analysis.Ball_Volume HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem HOL-Analysis: theory HOL-Analysis.Change_Of_Vars HOL-Analysis: theory HOL-Analysis.Simplex_Content HOL-Analysis: theory HOL-Analysis.Analysis Timing HOL-Analysis (6 threads, 329.557s elapsed time, 1616.532s cpu time, 59.796s GC time, factor 4.91) Finished HOL-Analysis (0:05:51 elapsed time, 0:27:44 cpu time, factor 4.74) Running HOL-Data_Structures ... HOL-Data_Structures: theory HOL-Data_Structures.Less_False HOL-Data_Structures: theory HOL-Data_Structures.Array_Specs HOL-Data_Structures: theory HOL-Data_Structures.Cmp HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less HOL-Data_Structures: theory HOL-Data_Structures.Tree2 HOL-Data_Structures: theory HOL-Data_Structures.Tree23 HOL-Data_Structures: theory HOL-Data_Structures.Tree234 HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del HOL-Data_Structures: theory HOL-Library.Cancellation HOL-Data_Structures: theory HOL-Data_Structures.Set_Specs HOL-Data_Structures: theory HOL-Data_Structures.Trie HOL-Data_Structures: theory HOL-Data_Structures.Map_Specs HOL-Data_Structures: theory HOL-Library.Pattern_Aliases HOL-Data_Structures: theory HOL-Data_Structures.Base_FDS HOL-Data_Structures: theory HOL-Library.Tree HOL-Data_Structures: theory HOL-Library.Multiset HOL-Data_Structures: theory HOL-Data_Structures.Isin2 HOL-Data_Structures: theory HOL-Data_Structures.Lookup2 HOL-Data_Structures: theory HOL-Data_Structures.AA_Set HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join HOL-Data_Structures: theory HOL-Data_Structures.RBT HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set HOL-Data_Structures: theory HOL-Data_Structures.AA_Map HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set HOL-Data_Structures: theory HOL-Library.Tree_Real HOL-Data_Structures: theory HOL-Data_Structures.Balance HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map HOL-Data_Structures: theory HOL-Data_Structures.Braun_Tree HOL-Data_Structures: theory HOL-Data_Structures.Array_Braun HOL-Data_Structures: theory HOL-Number_Theory.Fib HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue_Specs HOL-Data_Structures: theory HOL-Data_Structures.Binomial_Heap HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join_RBT HOL-Data_Structures: theory HOL-Data_Structures.Sorting HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Map Timing HOL-Data_Structures (6 threads, 169.351s elapsed time, 940.220s cpu time, 36.000s GC time, factor 5.55) Finished HOL-Data_Structures (0:02:50 elapsed time, 0:15:41 cpu time, factor 5.52) Running HOL-Hoare_Parallel ... HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Graph HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Com HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Quote_Antiquote HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Com HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Tran HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tran HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Hoare HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Hoare HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Syntax HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Examples HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tactics HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Syntax HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Gar_Coll HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Mul_Gar_Coll HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Examples HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Hoare_Parallel Timing HOL-Hoare_Parallel (6 threads, 61.035s elapsed time, 313.912s cpu time, 5.580s GC time, factor 5.14) Finished HOL-Hoare_Parallel (0:01:02 elapsed time, 0:05:14 cpu time, factor 5.07) Building HOL-Library ... HOL-Library: theory HOL-Library.AList HOL-Library: theory HOL-Library.Adhoc_Overloading HOL-Library: theory HOL-Library.BNF_Axiomatization HOL-Library: theory HOL-Library.BNF_Corec HOL-Library: theory HOL-Library.Boolean_Algebra HOL-Library: theory HOL-Library.Bit HOL-Library: theory HOL-Library.Cancellation HOL-Library: theory HOL-Library.Monad_Syntax HOL-Library: theory HOL-Library.State_Monad HOL-Library: theory HOL-Library.Cardinal_Notations HOL-Library: theory HOL-Library.Case_Converter HOL-Library: theory HOL-Library.Char_ord HOL-Library: theory HOL-Library.Code_Abstract_Nat HOL-Library: theory HOL-Library.Code_Lazy HOL-Library: theory HOL-Library.Simps_Case_Conv HOL-Library: theory HOL-Library.Extended HOL-Library: theory HOL-Library.Multiset HOL-Library: theory HOL-Library.Code_Binary_Nat HOL-Library: theory HOL-Library.Code_Target_Nat HOL-Library: theory HOL-Library.Code_Prolog HOL-Library: theory HOL-Library.Code_Target_Int HOL-Library: theory HOL-Library.DAList HOL-Library: theory HOL-Library.Code_Target_Numeral HOL-Library: theory HOL-Library.Code_Test HOL-Library: theory HOL-Library.Comparator HOL-Library: theory HOL-Library.Conditional_Parametricity HOL-Library: theory HOL-Library.Datatype_Records HOL-Library: theory HOL-Library.Debug HOL-Library: theory HOL-Library.Disjoint_Sets HOL-Library: theory HOL-Library.Dlist HOL-Library: theory HOL-Library.Fun_Lexorder HOL-Library: theory HOL-Library.FuncSet HOL-Library: theory HOL-Library.Function_Algebras HOL-Library: theory HOL-Library.Function_Division HOL-Library: theory HOL-Library.Groups_Big_Fun HOL-Library: theory HOL-Library.IArray HOL-Library: theory HOL-Library.Infinite_Set HOL-Library: theory HOL-Library.Equipollence HOL-Library: theory HOL-Library.LaTeXsugar HOL-Library: theory HOL-Library.Omega_Words_Fun HOL-Library: theory HOL-Library.Ramsey HOL-Library: theory HOL-Library.Lattice_Constructions HOL-Library: theory HOL-Library.Lattice_Syntax HOL-Library: theory HOL-Library.ListVector HOL-Library: theory HOL-Library.Combine_PER HOL-Library: theory HOL-Library.Complete_Partial_Order2 HOL-Library: theory HOL-Library.List_Lexorder HOL-Library: theory HOL-Library.Mapping HOL-Library: theory HOL-Library.More_List HOL-Library: theory HOL-Library.Nat_Bijection HOL-Library: theory HOL-Library.Stream HOL-Library: theory HOL-Library.DAList_Multiset HOL-Library: theory HOL-Library.Multiset_Order HOL-Library: theory HOL-Library.Permutation HOL-Library: theory HOL-Library.Permutations HOL-Library: theory HOL-Library.AList_Mapping HOL-Library: theory HOL-Library.Old_Datatype HOL-Library: theory HOL-Library.Old_Recdef HOL-Library: theory HOL-Library.Open_State_Syntax HOL-Library: theory HOL-Library.Option_ord HOL-Library: theory HOL-Library.Parallel HOL-Library: theory HOL-Library.Pattern_Aliases HOL-Library: theory HOL-Library.Perm HOL-Library: theory HOL-Library.Phantom_Type HOL-Library: theory HOL-Library.Power_By_Squaring HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs HOL-Library: theory HOL-Library.Preorder HOL-Library: theory HOL-Library.Product_Lexorder HOL-Library: theory HOL-Library.Product_Plus HOL-Library: theory HOL-Library.Quotient_Syntax HOL-Library: theory HOL-Library.Quotient_Option HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck HOL-Library: theory HOL-Library.Quotient_Product HOL-Library: theory HOL-Library.Product_Order HOL-Library: theory HOL-Library.Quotient_Set HOL-Library: theory HOL-Library.Quotient_Sum HOL-Library: theory HOL-Library.Cardinality HOL-Library: theory HOL-Library.Quotient_List HOL-Library: theory HOL-Library.Quotient_Type HOL-Library: theory HOL-Library.RBT_Impl HOL-Library: theory HOL-Library.Finite_Lattice HOL-Library: theory HOL-Library.Realizers HOL-Library: theory HOL-Library.Reflection HOL-Library: theory HOL-Library.Refute HOL-Library: theory HOL-Library.Rewrite HOL-Library: theory HOL-Library.Set_Algebras HOL-Library: theory HOL-Library.Sorting_Algorithms HOL-Library: theory HOL-Library.Stirling HOL-Library: theory HOL-Library.Numeral_Type HOL-Library: theory HOL-Library.Sublist HOL-Library: theory HOL-Library.Transitive_Closure_Table HOL-Library: theory HOL-Library.Tree HOL-Library: theory HOL-Library.Uprod HOL-Library: theory HOL-Library.Type_Length HOL-Library: theory HOL-Library.Saturated HOL-Library: theory HOL-Library.While_Combinator HOL-Library: theory HOL-Library.Countable HOL-Library: theory HOL-Library.Prefix_Order HOL-Library: theory HOL-Library.Subseq_Order HOL-Library: theory HOL-Library.BigO HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint HOL-Library: theory HOL-Library.Diagonal_Subsequence HOL-Library: theory HOL-Library.Discrete HOL-Library: theory HOL-Library.Going_To_Filter HOL-Library: theory HOL-Library.Indicator_Function HOL-Library: theory HOL-Library.Landau_Symbols HOL-Library: theory HOL-Library.Countable_Set HOL-Library: theory HOL-Library.FSet HOL-Library: theory HOL-Library.Lattice_Algebras HOL-Library: theory HOL-Library.Tree_Multiset HOL-Library: theory HOL-Library.Countable_Complete_Lattices HOL-Library: theory HOL-Library.Countable_Set_Type HOL-Library: theory HOL-Library.Set_Idioms HOL-Library: theory HOL-Library.Liminf_Limsup HOL-Library: theory HOL-Library.Log_Nat HOL-Library: theory HOL-Library.Lub_Glb HOL-Library: theory HOL-Library.Multiset_Permutations HOL-Library: theory HOL-Library.Nonpos_Ints HOL-Library: theory HOL-Library.OptionalSugar HOL-Library: theory HOL-Library.Order_Continuity HOL-Library: theory HOL-Library.Periodic_Fun HOL-Library: theory HOL-Library.Quadratic_Discriminant HOL-Library: theory HOL-Library.Finite_Map HOL-Library: theory HOL-Library.Sum_of_Squares HOL-Library: theory HOL-Library.Extended_Nat HOL-Library: theory HOL-Library.Float HOL-Library: theory HOL-Library.Tree_Real HOL-Library: theory HOL-Library.Extended_Real HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams HOL-Library: theory HOL-Library.Extended_Nonnegative_Real HOL-Library: theory HOL-Library.RBT HOL-Library: theory HOL-Library.RBT_Mapping HOL-Library: theory HOL-Library.RBT_Set HOL-Library FAILED (see also /media/data/jenkins/workspace/isabelle-nightly-benchmark/heaps/polyml-5.8_x86_64-linux/log/HOL-Library) ### 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" ### 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" ### 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" ### 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" ### 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" ### 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" ### 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" ### 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" ### 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" ### 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" ### 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" ### Ignoring duplicate rewrite rule: ### \?k1 \| ?l1; ?k1 \| ?r1\ ### \ ?k1 \| combine ?l1 ?r1 \ True ### Ignoring duplicate rewrite rule: ### \?l1 |\ ?k1; ?r1 |\ ?k1\ ### \ combine ?l1 ?r1 |\ ?k1 \ True ### Ignoring duplicate rewrite rule: ### \?l1 |\ ?k1; ?r1 |\ ?k1\ ### \ combine ?l1 ?r1 |\ ?k1 \ True ### Ignoring duplicate rewrite rule: ### \?k1 \| ?l1; ?k1 \| ?r1\ ### \ ?k1 \| combine ?l1 ?r1 \ True ### Ignoring duplicate rewrite rule: ### ?n1 \ Suc (length ?kvs1) \ ### entries (fst (rbtreeify_g ?n1 ?kvs1)) \ take (?n1 - 1) ?kvs1 \ (Sup ` ?A) = \ (Inf ` {f ` ?A |f. \Y\?A. f Y \ Y}) Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> (\p. size_list size (fst (snd p))) <*mlex*> {}" Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> (\p. size_list size (fst (snd p))) <*mlex*> {}" ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Introduced fixed type variable(s): 'd in "x__" *** Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Finite_Map") *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml *** At command "export_code" (line 1428 of "~~/src/HOL/Library/Finite_Map.thy") HOL-Auth CANCELLED HOL-Bali CANCELLED HOL-Cardinals CANCELLED HOL-Computational_Algebra CANCELLED HOL-Algebra CANCELLED HOL-Corec_Examples CANCELLED HOL-Datatype_Benchmark CANCELLED HOL-Datatype_Examples CANCELLED HOL-Decision_Procs CANCELLED HOL-IMP CANCELLED HOL-Imperative_HOL CANCELLED HOL-Metis_Examples CANCELLED HOL-MicroJava CANCELLED HOL-Nominal CANCELLED HOL-Nominal-Examples CANCELLED HOL-Nonstandard_Analysis CANCELLED HOL-Nonstandard_Analysis-Examples CANCELLED HOL-Number_Theory CANCELLED HOL-Predicate_Compile_Examples CANCELLED Building HOL-Probability ... HOL-Probability: theory HOL-Library.AList HOL-Probability: theory HOL-Library.Adhoc_Overloading HOL-Probability: theory HOL-Library.Conditional_Parametricity HOL-Probability: theory HOL-Library.Lattice_Syntax HOL-Probability: theory HOL-Library.Mapping HOL-Probability: theory HOL-Library.Stream HOL-Probability: theory HOL-Library.Complete_Partial_Order2 HOL-Probability: theory HOL-Library.Monad_Syntax HOL-Probability: theory HOL-Library.Rewrite HOL-Probability: theory HOL-Library.Sublist HOL-Probability: theory HOL-Library.Tree HOL-Probability: theory HOL-Library.FSet HOL-Probability: theory HOL-Library.Diagonal_Subsequence HOL-Probability: theory HOL-Library.Multiset_Permutations HOL-Probability: theory HOL-Library.AList_Mapping HOL-Probability: theory HOL-Probability.Discrete_Topology HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams HOL-Probability: theory HOL-Probability.Essential_Supremum HOL-Probability: theory HOL-Probability.Probability_Measure HOL-Probability: theory HOL-Probability.Stopping_Time HOL-Probability: theory HOL-Probability.Tree_Space HOL-Probability: theory HOL-Probability.Conditional_Expectation HOL-Probability: theory HOL-Probability.Distribution_Functions HOL-Probability: theory HOL-Probability.Giry_Monad HOL-Probability: theory HOL-Probability.Weak_Convergence HOL-Probability: theory HOL-Probability.Helly_Selection HOL-Probability: theory HOL-Library.Finite_Map HOL-Probability: theory HOL-Probability.Probability_Mass_Function HOL-Probability: theory HOL-Probability.Projective_Family HOL-Probability: theory HOL-Probability.Infinite_Product_Measure HOL-Probability: theory HOL-Probability.Independent_Family HOL-Probability: theory HOL-Probability.Stream_Space HOL-Probability: theory HOL-Probability.PMF_Impl HOL-Probability: theory HOL-Probability.Random_Permutations HOL-Probability: theory HOL-Probability.SPMF HOL-Probability: theory HOL-Probability.Convolution HOL-Probability: theory HOL-Probability.Information HOL-Probability: theory HOL-Probability.Distributions HOL-Probability: theory HOL-Probability.Characteristic_Functions HOL-Probability: theory HOL-Probability.Sinc_Integral HOL-Probability: theory HOL-Probability.Levy HOL-Probability: theory HOL-Probability.Central_Limit_Theorem HOL-Probability FAILED (see also /media/data/jenkins/workspace/isabelle-nightly-benchmark/heaps/polyml-5.8_x86_64-linux/log/HOL-Probability) ### 0 \ normal_density ?\1 ?\1 ?x1 \ True ### Ignoring duplicate rewrite rule: ### 0 \ normal_density ?\1 ?\1 ?x1 \ True ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \ of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### \x\?A1. ?y1 \ ?y1 ^ card ?A1 ### Rule already declared as introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Rule already declared as introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Rule already declared as introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. ereal (?f x)) \ ereal ?x) ?F ### Rule already declared as introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. - ?f x) \ - ?x) ?F ### Rule already declared as introduction (intro) ### \\?c\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \?x \ 0; (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \?y \ - \; ?x \ - \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Rule already declared as introduction (intro) ### \\?y\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Rule already declared as introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. ennreal (?f x)) \ ennreal ?x) ?F *** Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map") *** Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map") *** Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit") *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml *** At command "export_code" (line 1428 of "~~/src/HOL/Library/Finite_Map.thy") HOL-Probability-ex CANCELLED Building HOL-Proofs ... HOL-Proofs: theory HOL.Code_Generator HOL-Proofs: theory HOL.HOL HOL-Proofs: theory HOL.Argo HOL-Proofs: theory HOL.Ctr_Sugar HOL-Proofs: theory HOL.Orderings HOL-Proofs: theory HOL.SAT HOL-Proofs: theory HOL.Groups HOL-Proofs: theory HOL.Lattices HOL-Proofs: theory HOL.Set HOL-Proofs: theory HOL.Fun HOL-Proofs: theory HOL.Typedef HOL-Proofs: theory HOL.Complete_Lattices HOL-Proofs: theory HOL.Rings HOL-Proofs: theory HOL.Inductive HOL-Proofs: theory HOL.Product_Type HOL-Proofs: theory HOL.Sum_Type HOL-Proofs: theory HOL.Complete_Partial_Order HOL-Proofs: theory HOL.Nat HOL-Proofs: theory HOL.Fields HOL-Proofs: theory HOL.Meson HOL-Proofs: theory HOL.ATP HOL-Proofs: theory HOL.Metis HOL-Proofs: theory HOL.Finite_Set HOL-Proofs: theory HOL.Relation HOL-Proofs: theory HOL.Transitive_Closure HOL-Proofs: theory HOL.Wellfounded HOL-Proofs: theory HOL.Fun_Def_Base HOL-Proofs: theory HOL.Hilbert_Choice HOL-Proofs: theory HOL.Wfrec HOL-Proofs: theory HOL.Order_Relation HOL-Proofs: theory HOL.BNF_Wellorder_Relation HOL-Proofs: theory HOL.BNF_Wellorder_Embedding HOL-Proofs: theory HOL.Zorn HOL-Proofs: theory HOL.BNF_Wellorder_Constructions HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic HOL-Proofs: theory HOL.BNF_Def HOL-Proofs: theory HOL.BNF_Composition HOL-Proofs: theory HOL.Basic_BNFs HOL-Proofs: theory HOL.BNF_Fixpoint_Base HOL-Proofs: theory HOL.BNF_Least_Fixpoint HOL-Proofs: theory HOL.Basic_BNF_LFPs HOL-Proofs: theory HOL.Transfer HOL-Proofs: theory HOL.Num HOL-Proofs: theory HOL.Power HOL-Proofs: theory HOL.Groups_Big HOL-Proofs: theory HOL.Equiv_Relations HOL-Proofs: theory HOL.Lifting HOL-Proofs: theory HOL.Lifting_Set HOL-Proofs: theory HOL.Option HOL-Proofs: theory HOL.Quotient HOL-Proofs: theory HOL.Extraction HOL-Proofs: theory HOL.Lattices_Big HOL-Proofs: theory HOL.Partial_Function HOL-Proofs: theory HOL.Fun_Def HOL-Proofs: theory HOL.Int HOL-Proofs: theory HOL.Euclidean_Division HOL-Proofs: theory HOL.Parity HOL-Proofs: theory HOL.Divides HOL-Proofs: theory HOL.Code_Numeral HOL-Proofs: theory HOL.Numeral_Simprocs HOL-Proofs: theory HOL.SMT HOL-Proofs: theory HOL.Set_Interval HOL-Proofs: theory HOL.Semiring_Normalization HOL-Proofs: theory HOL.Groebner_Basis HOL-Proofs: theory HOL.Conditionally_Complete_Lattices HOL-Proofs: theory HOL.Presburger HOL-Proofs: theory HOL.Filter HOL-Proofs: theory HOL.Sledgehammer HOL-Proofs: theory HOL.List HOL-Proofs: theory HOL.Groups_List HOL-Proofs: theory HOL.Map HOL-Proofs: theory HOL.Factorial HOL-Proofs: theory HOL.GCD HOL-Proofs: theory HOL.Random HOL-Proofs: theory HOL.Enum HOL-Proofs: theory HOL.Binomial HOL-Proofs: theory HOL.String HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint HOL-Proofs: theory HOL.Predicate HOL-Proofs: theory HOL.Typerep HOL-Proofs: theory HOL.Lazy_Sequence HOL-Proofs: theory HOL.Limited_Sequence HOL-Proofs: theory HOL.Code_Evaluation HOL-Proofs: theory HOL.Quickcheck_Random HOL-Proofs: theory HOL.Quickcheck_Exhaustive HOL-Proofs: theory HOL.Quickcheck_Narrowing HOL-Proofs: theory HOL.Random_Pred HOL-Proofs: theory HOL.Random_Sequence HOL-Proofs: theory HOL.Record HOL-Proofs: theory HOL.Predicate_Compile HOL-Proofs: theory HOL.Nitpick HOL-Proofs: theory HOL.Nunchaku HOL-Proofs: theory Main HOL-Proofs: theory HOL-Library.Realizers Timing HOL-Proofs (6 threads, 723.611s elapsed time, 1792.740s cpu time, 434.900s GC time, factor 2.48) Finished HOL-Proofs (0:12:40 elapsed time, 0:31:09 cpu time, factor 2.46) Running HOL-Proofs-Extraction ... HOL-Proofs-Extraction: theory HOL-Library.Cancellation HOL-Proofs-Extraction: theory HOL-Library.Code_Abstract_Nat HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Int HOL-Proofs-Extraction: theory HOL-Library.Open_State_Syntax HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Warshall HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Nat HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Util HOL-Proofs-Extraction: theory HOL-Library.Multiset HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Numeral HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.QuotRem HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Pigeonhole HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman_Extraction HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Greatest_Common_Divisor HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Factorial_Ring HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Euclidean_Algorithm HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Primes HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Euclid Timing HOL-Proofs-Extraction (6 threads, 88.700s elapsed time, 195.020s cpu time, 10.500s GC time, factor 2.20) Finished HOL-Proofs-Extraction (0:01:29 elapsed time, 0:03:16 cpu time, factor 2.18) Running HOL-Proofs-Lambda ... HOL-Proofs-Lambda: theory HOL-Library.Code_Target_Int HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Commutation HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Lambda HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListOrder HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListApplication HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ParRed HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.LambdaType HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListBeta HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Eta HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.InductTermi HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.NormalForm HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.StrongNorm HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Standardization HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.WeakNorm Timing HOL-Proofs-Lambda (6 threads, 104.932s elapsed time, 138.824s cpu time, 5.764s GC time, factor 1.32) Finished HOL-Proofs-Lambda (0:01:46 elapsed time, 0:02:19 cpu time, factor 1.32) HOL-Quickcheck_Benchmark CANCELLED HOL-Quickcheck_Examples CANCELLED HOL-Quotient_Examples CANCELLED Running HOL-Record_Benchmark ... HOL-Record_Benchmark: theory HOL-Record_Benchmark.Record_Benchmark Timing HOL-Record_Benchmark (6 threads, 154.562s elapsed time, 235.288s cpu time, 12.824s GC time, factor 1.52) Finished HOL-Record_Benchmark (0:02:35 elapsed time, 0:03:56 cpu time, factor 1.52) HOL-SET_Protocol CANCELLED HOL-UNITY CANCELLED Building HOL-Word ... HOL-Word: theory HOL-Library.Bit HOL-Word: theory HOL-Library.Boolean_Algebra HOL-Word: theory HOL-Library.Phantom_Type HOL-Word: theory HOL-Word.Bits HOL-Word: theory HOL-Word.Misc_Numeric HOL-Word: theory HOL-Word.Misc_Typedef HOL-Word: theory HOL-Word.Bit_Representation HOL-Word: theory HOL-Word.Bits_Bit HOL-Word: theory HOL-Word.Word_Miscellaneous HOL-Word: theory HOL-Word.Bits_Int HOL-Word: theory HOL-Library.Cardinality HOL-Word: theory HOL-Library.Numeral_Type HOL-Word: theory HOL-Word.Bit_Comparison HOL-Word: theory HOL-Word.Bool_List_Representation HOL-Word: theory HOL-Library.Type_Length HOL-Word: theory HOL-Word.Word HOL-Word: theory HOL-Word.WordBitwise HOL-Word: theory HOL-Word.WordExamples Timing HOL-Word (6 threads, 9.802s elapsed time, 48.876s cpu time, 2.128s GC time, factor 4.99) Finished HOL-Word (0:00:17 elapsed time, 0:01:03 cpu time, factor 3.70) Running HOL-Word-SMT_Examples ... HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.Boogie HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Word_Examples HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Examples HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Tests Timing HOL-Word-SMT_Examples (6 threads, 59.577s elapsed time, 86.088s cpu time, 0.868s GC time, factor 1.44) Finished HOL-Word-SMT_Examples (0:01:00 elapsed time, 0:01:29 cpu time, factor 1.48) HOL-ex CANCELLED Building HOLCF ... HOLCF: theory HOL-Library.Nat_Bijection HOLCF: theory HOL-Library.Old_Datatype HOLCF: theory HOLCF.Porder HOLCF: theory HOLCF.Pcpo HOLCF: theory HOL-Library.Countable HOLCF: theory HOLCF.Cont HOLCF: theory HOLCF.Adm HOLCF: theory HOLCF.Discrete HOLCF: theory HOLCF.Cpodef HOLCF: theory HOLCF.Fun_Cpo HOLCF: theory HOLCF.Product_Cpo HOLCF: theory HOLCF.Cfun HOLCF: theory HOLCF.Completion HOLCF: theory HOLCF.Cprod HOLCF: theory HOLCF.Deflation HOLCF: theory HOLCF.Fix HOLCF: theory HOLCF.Sfun HOLCF: theory HOLCF.Sprod HOLCF: theory HOLCF.Up HOLCF: theory HOLCF.Lift HOLCF: theory HOLCF.One HOLCF: theory HOLCF.Tr HOLCF: theory HOLCF.Ssum HOLCF: theory HOLCF.Fixrec HOLCF: theory HOLCF.Map_Functions HOLCF: theory HOLCF.Bifinite HOLCF: theory HOLCF.Domain_Aux HOLCF: theory HOLCF.Universal HOLCF: theory HOLCF.Algebraic HOLCF: theory HOLCF.Compact_Basis HOLCF: theory HOLCF.LowerPD HOLCF: theory HOLCF.UpperPD HOLCF: theory HOLCF.Representable HOLCF: theory HOLCF.ConvexPD HOLCF: theory HOLCF.Domain HOLCF: theory HOLCF.Powerdomains HOLCF: theory HOLCF Timing HOLCF (6 threads, 12.575s elapsed time, 39.664s cpu time, 2.348s GC time, factor 3.15) Finished HOLCF (0:00:20 elapsed time, 0:00:57 cpu time, factor 2.73) Running IOA ... IOA: theory IOA.Seq IOA: theory IOA.Asig IOA: theory IOA.Pred IOA: theory IOA.Automata IOA: theory IOA.Sequence IOA: theory IOA.Traces IOA: theory IOA.TL IOA: theory IOA.CompoExecs IOA: theory IOA.RefMappings IOA: theory IOA.ShortExecutions IOA: theory IOA.RefCorrectness IOA: theory IOA.CompoScheds IOA: theory IOA.Simulations IOA: theory IOA.SimCorrectness IOA: theory IOA.Deadlock IOA: theory IOA.CompoTraces IOA: theory IOA.Compositionality IOA: theory IOA.IOA IOA: theory IOA.TLS IOA: theory IOA.LiveIOA IOA: theory IOA.Abstraction Timing IOA (6 threads, 7.683s elapsed time, 32.800s cpu time, 1.372s GC time, factor 4.27) Finished IOA (0:00:08 elapsed time, 0:00:33 cpu time, factor 3.83) Building ZF ... ZF: theory IFOL ZF: theory FOL ZF: theory ZF.ZF_Base ZF: theory ZF.upair ZF: theory ZF.pair ZF: theory ZF.Bool ZF: theory ZF.equalities ZF: theory ZF.Fixedpt ZF: theory ZF.Sum ZF: theory ZF.func ZF: theory ZF.Perm ZF: theory ZF.QPair ZF: theory ZF.Trancl ZF: theory ZF.EquivClass ZF: theory ZF.WF ZF: theory ZF.Order ZF: theory ZF.Ordinal ZF: theory ZF.OrdQuant ZF: theory ZF.Nat ZF: theory ZF.OrderArith ZF: theory ZF.Epsilon ZF: theory ZF.Inductive ZF: theory ZF.OrderType ZF: theory ZF.Finite ZF: theory ZF.Cardinal ZF: theory ZF.Univ ZF: theory ZF.Arith ZF: theory ZF.QUniv ZF: theory ZF.Datatype ZF: theory ZF.ArithSimp ZF: theory ZF.Int ZF: theory ZF.CardinalArith ZF: theory ZF.List ZF: theory ZF.Bin ZF: theory ZF.IntDiv ZF: theory ZF ZF: theory ZF.AC ZF: theory ZF.Zorn ZF: theory ZF.Cardinal_AC ZF: theory ZF.InfDatatype ZF: theory ZFC Timing ZF (6 threads, 13.363s elapsed time, 47.776s cpu time, 3.200s GC time, factor 3.58) Finished ZF (0:00:15 elapsed time, 0:00:51 cpu time, factor 3.40) Building ZF-Induct ... ZF-Induct: theory ZF-Induct.Acc ZF-Induct: theory ZF-Induct.Comb ZF-Induct: theory ZF-Induct.Binary_Trees ZF-Induct: theory ZF-Induct.Datatypes ZF-Induct: theory ZF-Induct.ListN ZF-Induct: theory ZF-Induct.FoldSet ZF-Induct: theory ZF-Induct.Mutil ZF-Induct: theory ZF-Induct.Ntree ZF-Induct: theory ZF-Induct.Primrec ZF-Induct: theory ZF-Induct.PropLog ZF-Induct: theory ZF-Induct.Rmap ZF-Induct: theory ZF-Induct.Term ZF-Induct: theory ZF-Induct.Tree_Forest ZF-Induct: theory ZF-Induct.Multiset ZF-Induct: theory ZF-Induct.Brouwer Timing ZF-Induct (6 threads, 3.418s elapsed time, 13.156s cpu time, 0.584s GC time, factor 3.85) Finished ZF-Induct (0:00:05 elapsed time, 0:00:17 cpu time, factor 3.37) Running ZF-UNITY ... ZF-UNITY: theory ZF-UNITY.MultisetSum ZF-UNITY: theory ZF-UNITY.State ZF-UNITY: theory ZF-UNITY.GenPrefix ZF-UNITY: theory ZF-UNITY.UNITY ZF-UNITY: theory ZF-UNITY.Monotonicity ZF-UNITY: theory ZF-UNITY.Constrains ZF-UNITY: theory ZF-UNITY.FP ZF-UNITY: theory ZF-UNITY.WFair ZF-UNITY: theory ZF-UNITY.Increasing ZF-UNITY: theory ZF-UNITY.SubstAx ZF-UNITY: theory ZF-UNITY.Follows ZF-UNITY: theory ZF-UNITY.Mutex ZF-UNITY: theory ZF-UNITY.Union ZF-UNITY: theory ZF-UNITY.Comp ZF-UNITY: theory ZF-UNITY.Guar ZF-UNITY: theory ZF-UNITY.AllocBase ZF-UNITY: theory ZF-UNITY.ClientImpl ZF-UNITY: theory ZF-UNITY.Distributor ZF-UNITY: theory ZF-UNITY.AllocImpl ZF-UNITY: theory ZF-UNITY.Merge Timing ZF-UNITY (6 threads, 6.282s elapsed time, 32.904s cpu time, 1.596s GC time, factor 5.24) Finished ZF-UNITY (0:00:06 elapsed time, 0:00:33 cpu time, factor 4.88) 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 === TIMING === Group main: 0:12:25 elapsed time, 0:54:29 cpu time, factor 4.39 Group timing: 0:30:06 elapsed time, 1:43:28 cpu time, factor 3.44 Overall: 0:36:57 elapsed time, 1:59:23 cpu time, factor 3.23 === FAILED SESSIONS === Session HOL-Probability: FAILED 2 Session HOL-Predicate_Compile_Examples: CANCELLED Session HOL-Nonstandard_Analysis-Examples: CANCELLED Session HOL-Nominal: CANCELLED Session HOL-Datatype_Examples: CANCELLED Session HOL-Cardinals: CANCELLED Session HOL-Nominal-Examples: CANCELLED Session HOL-Auth: CANCELLED Session HOL-MicroJava: CANCELLED Session HOL-Corec_Examples: CANCELLED Session HOL-Bali: CANCELLED Session HOL-Quickcheck_Benchmark: CANCELLED Session HOL-UNITY: CANCELLED Session HOL-ex: CANCELLED Session HOL-Quickcheck_Examples: CANCELLED Session HOL-Imperative_HOL: CANCELLED Session HOL-Probability-ex: CANCELLED Session HOL-Metis_Examples: CANCELLED Session HOL-IMP: CANCELLED Session HOL-Datatype_Benchmark: CANCELLED Session HOL-SET_Protocol: CANCELLED Session HOL-Number_Theory: CANCELLED Session HOL-Decision_Procs: CANCELLED Session HOL-Library: FAILED 2 Session HOL-Quotient_Examples: CANCELLED Session HOL-Nonstandard_Analysis: CANCELLED Session HOL-Computational_Algebra: CANCELLED Session HOL-Algebra: CANCELLED Build step 'Execute shell' marked build as failure Archiving artifacts Started calculate disk usage of build Finished Calculation of disk usage of build in 0 seconds Started calculate disk usage of workspace Finished Calculation of disk usage of workspace in 0 seconds No emails were triggered. Finished: FAILURE