[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