[EnvInject] - Loading node environment variables.
workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-nightly-benchmark Building remotely on
[isabelle-nightly-benchmark] $ hg showconfig paths.default
[isabelle-nightly-benchmark] $ hg pull --rev default
http://isabelle.in.tum.de/repos/isabelle/ pulling from
[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
[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
[isabelle-nightly-benchmark] $ /bin/sh -xe /tmp/jenkins386781598375730483.sh
+ Admin/jenkins/run_build benchmark
### 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.
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
# To setup the new switch in the current shell, you need to run:
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
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64-linux"
Session HOL/HOL-Hoare_Parallel (timing) Session HOL/HOL-Library (main timing) Session HOL/HOL-UNITY (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-Corec_Examples (timing) Session HOL/HOL-Datatype_Benchmark Session HOL/HOL-Datatype_Examples (timing) Session HOL/HOL-Imperative_HOL (timing) Session HOL/HOL-Metis_Examples (timing) Session HOL/HOL-MicroJava (timing) 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/HOL-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-Lambda (timing) 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) HOL: theory HOL.Code_Generator HOL: theory HOL.Complete_Lattices HOL: theory HOL.Complete_Partial_Order HOL: theory HOL.Transitive_Closure HOL: theory HOL.Hilbert_Choice HOL: theory HOL.Order_Relation HOL: theory HOL.BNF_Wellorder_Relation HOL: theory HOL.BNF_Wellorder_Embedding HOL: theory HOL.BNF_Wellorder_Constructions HOL: theory HOL.BNF_Cardinal_Order_Relation HOL: theory HOL.BNF_Cardinal_Arithmetic HOL: theory HOL.BNF_Composition HOL: theory HOL.BNF_Fixpoint_Base HOL: theory HOL.BNF_Least_Fixpoint HOL: theory HOL.Basic_BNF_LFPs HOL: theory HOL.Equiv_Relations HOL: theory HOL.Partial_Function HOL: theory HOL.Euclidean_Division HOL: theory HOL.Numeral_Simprocs HOL: theory HOL.Semiring_Normalization HOL: theory HOL.Groebner_Basis HOL: theory HOL.Conditionally_Complete_Lattices HOL: theory HOL.BNF_Greatest_Fixpoint 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_Sequence HOL: theory HOL.Predicate_Compile HOL: theory HOL.Archimedean_Field HOL: theory HOL.Topological_Spaces HOL: theory HOL.Real_Vector_Spaces HOL: theory HOL.Transcendental 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) 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) 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 (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: ### \<lbrakk>?k1 \<guillemotleft>| ?l1; ?k1 \<guillemotleft>| ?r1\<rbrakk> ### \<Longrightarrow> ?k1 \<guillemotleft>| combine ?l1 ?r1 \<equiv> True ### Ignoring duplicate rewrite rule: ### \<lbrakk>?l1 |\<guillemotleft> ?k1; ?r1 |\<guillemotleft> ?k1\<rbrakk> ### \<Longrightarrow> combine ?l1 ?r1 |\<guillemotleft> ?k1 \<equiv> True ### Ignoring duplicate rewrite rule: ### \<lbrakk>?l1 |\<guillemotleft> ?k1; ?r1 |\<guillemotleft> ?k1\<rbrakk> ### \<Longrightarrow> combine ?l1 ?r1 |\<guillemotleft> ?k1 \<equiv> True ### Ignoring duplicate rewrite rule: ### \<lbrakk>?k1 \<guillemotleft>| ?l1; ?k1 \<guillemotleft>| ?r1\<rbrakk> ### \<Longrightarrow> ?k1 \<guillemotleft>| combine ?l1 ?r1 \<equiv> True ### Ignoring duplicate rewrite rule: ### ?n1 \<le> Suc (length ?kvs1) \<Longrightarrow> ### entries (fst (rbtreeify_g ?n1 ?kvs1)) \<equiv> take (?n1 - 1) ?kvs1 \<Squnion> (Inf ` {f ` ?A |f. \<forall>Y\<in>?A. f Y \<in> Y}) "(\<lambda>p. size_list size (snd (snd p))) <*mlex*> (\<lambda>p. size_list size (fst (snd p))) <*mlex*> {}" "(\<lambda>p. size_list size (snd (snd p))) <*mlex*> (\<lambda>p. size_list size (fst (snd p))) <*mlex*> {}" ### Rule already declared as introduction (intro) ### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?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-Computational_Algebra CANCELLED HOL-Datatype_Benchmark CANCELLED HOL-Datatype_Examples CANCELLED HOL-Nominal-Examples CANCELLED HOL-Nonstandard_Analysis CANCELLED HOL-Nonstandard_Analysis-Examples CANCELLED HOL-Predicate_Compile_Examples CANCELLED 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 (see also /media/data/jenkins/workspace/isabelle-nightly-benchmark/heaps/polyml-5.8_x86_64-linux/log/HOL-Probability) ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### 0 \<le> normal_density ?\<mu>1 ?\<sigma>1 ?x1 \<equiv> True ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \<equiv> of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### \<Prod>x\<in>?A1. ?y1 \<equiv> ?y1 ^ card ?A1 ### Rule already declared as introduction (intro) ### ((\<lambda>x. x) \<longlongrightarrow> ?a) (at ?a within ?s) ### Rule already declared as introduction (intro) ### ((\<lambda>x. ?k) \<longlongrightarrow> ?k) ?F ### Rule already declared as introduction (intro) ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow> ### ((\<lambda>x. ereal (?f x)) \<longlongrightarrow> ereal ?x) ?F ### Rule already declared as introduction (intro) ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow> ### ((\<lambda>x. - ?f x) \<longlongrightarrow> - ?x) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>\<bar>?c\<bar> \<noteq> \<infinity>; ### (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>?x \<noteq> 0; (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>?y \<noteq> - \<infinity>; ?x \<noteq> - \<infinity>; ### (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F ### Rule already declared as introduction (intro) ### \<lbrakk>\<bar>?y\<bar> \<noteq> \<infinity>; ### (?f \<longlongrightarrow> ?x) ?F\<rbrakk> ### \<Longrightarrow> ((\<lambda>x. ?f x + ?y) \<longlongrightarrow> ?x + ?y) ?F ### Rule already declared as introduction (intro) ### (?f \<longlongrightarrow> ?x) ?F \<Longrightarrow> ### ((\<lambda>x. ennreal (?f x)) \<longlongrightarrow> 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-Proofs: theory HOL.Code_Generator HOL-Proofs: theory HOL.Ctr_Sugar HOL-Proofs: theory HOL.Orderings HOL-Proofs: theory HOL.Lattices HOL-Proofs: theory HOL.Typedef HOL-Proofs: theory HOL.Complete_Lattices 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.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.Order_Relation HOL-Proofs: theory HOL.BNF_Wellorder_Relation HOL-Proofs: theory HOL.BNF_Wellorder_Embedding 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.Groups_Big HOL-Proofs: theory HOL.Equiv_Relations HOL-Proofs: theory HOL.Lifting HOL-Proofs: theory HOL.Lifting_Set 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.Euclidean_Division HOL-Proofs: theory HOL.Divides HOL-Proofs: theory HOL.Code_Numeral HOL-Proofs: theory HOL.Numeral_Simprocs 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.Sledgehammer HOL-Proofs: theory HOL.Groups_List HOL-Proofs: theory HOL.Factorial HOL-Proofs: theory HOL.Binomial 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.Predicate_Compile HOL-Proofs: theory HOL.Nitpick HOL-Proofs: theory HOL.Nunchaku 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) 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-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) HOLCF: theory HOL-Library.Nat_Bijection HOLCF: theory HOL-Library.Old_Datatype HOLCF: theory HOL-Library.Countable HOLCF: theory HOLCF.Product_Cpo HOLCF: theory HOLCF.Completion HOLCF: theory HOLCF.Map_Functions HOLCF: theory HOLCF.Domain_Aux HOLCF: theory HOLCF.Compact_Basis HOLCF: theory HOLCF.Representable HOLCF: theory HOLCF.Powerdomains 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) IOA: theory IOA.ShortExecutions IOA: theory IOA.RefCorrectness IOA: theory IOA.SimCorrectness IOA: theory IOA.Compositionality 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) 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) 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) 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.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
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
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-MicroJava: CANCELLED Session HOL-Corec_Examples: CANCELLED Session HOL-Quickcheck_Benchmark: CANCELLED Session HOL-Quickcheck_Examples: CANCELLED Session HOL-Imperative_HOL: CANCELLED Session HOL-Probability-ex: CANCELLED Session HOL-Metis_Examples: CANCELLED Session HOL-Datatype_Benchmark: CANCELLED Session HOL-SET_Protocol: CANCELLED Session HOL-Number_Theory: CANCELLED Session HOL-Decision_Procs: CANCELLED 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 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