[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
https://isabelle.in.tum.de/repos/isabelle/ real URL is
[isabelle-nightly-benchmark] $ hg update --clean --rev default
2 files updated, 0 files merged, 0 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 d1767bcb79ec835777300b16e971e54b68f5691c --template exists\n
[isabelle-nightly-benchmark] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(d1767bcb79ec835777300b16e971e54b68f5691c)" --encoding UTF-8 --encodingmode replace
[isabelle-nightly-benchmark] $ /bin/sh -xe /tmp/jenkins7452190526733090760.sh
+ Admin/jenkins/run_build benchmark
### Building graph browser ...
warning: [options] bootstrap class path not set in conjunction with -source 7
warning: [options] source value 7 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 ...
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
[NOTE] Package zarith is already installed (current version is 1.7). 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.8.4
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686/x86_64_32-linux"
Session HOL/HOL-Cardinals (timing) Session HOL/HOL-Hoare_Parallel (timing) Session HOL/HOL-Library (main timing) Session HOL/HOL-UNITY (timing) Session HOL/HOL-Combinatorics (main 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-Complex_Analysis (main timing) Session HOL/HOL-Homology (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-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-Lambda (timing) Session HOL/HOL-Quickcheck_Benchmark Session HOL/HOL-MicroJava (timing) Session HOL/HOL-Nominal-Examples (timing) Session HOL/HOL-Predicate_Compile_Examples (timing) Session HOL/HOL-Quickcheck_Examples (timing) Session HOL/HOL-Record_Benchmark Session HOL/HOL-SET_Protocol (timing) Session HOL/HOL-SMT_Examples (timing) Session HOL/HOLCF (main timing) Timing Pure (1 threads, 1.322s elapsed time, 1.377s cpu time, 0.000s GC time, factor 1.04) Finished Pure (0:00:22 elapsed time, 0:00:21 cpu time, factor 0.98) HOL: theory Tools.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, 216.374s elapsed time, 747.756s cpu time, 53.294s GC time, factor 3.46) Finished HOL (0:04:17 elapsed time, 0:13:52 cpu time, factor 3.23) HOL-Analysis: theory HOL-Library.Cancellation HOL-Analysis: theory HOL-Library.Disjoint_Sets HOL-Analysis: theory HOL-Library.FuncSet 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.Set_Algebras HOL-Analysis: theory HOL-Library.Product_Order HOL-Analysis: theory HOL-Library.Multiset HOL-Analysis: theory HOL-Library.Countable HOL-Analysis: theory HOL-Analysis.Metric_Arith HOL-Analysis: theory HOL-Analysis.Inner_Product HOL-Analysis: theory HOL-Analysis.L2_Norm HOL-Analysis: theory HOL-Analysis.Operator_Norm HOL-Analysis: theory HOL-Library.Cardinality HOL-Analysis: theory HOL-Analysis.Poly_Roots HOL-Analysis: theory HOL-Analysis.Product_Vector 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.Numeral_Type HOL-Analysis: theory HOL-Library.Periodic_Fun HOL-Analysis: theory HOL-Analysis.Euclidean_Space 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-Computational_Algebra.Factorial_Ring HOL-Analysis: theory HOL-Combinatorics.Permutations HOL-Analysis: theory HOL-Analysis.Linear_Algebra HOL-Analysis: theory HOL-Library.Order_Continuity HOL-Analysis: theory HOL-Analysis.Norm_Arith HOL-Analysis: theory HOL-Analysis.Abstract_Limits HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2 HOL-Analysis: theory HOL-Library.Extended_Nat HOL-Analysis: theory HOL-Analysis.Affine HOL-Analysis: theory HOL-Analysis.Cartesian_Space HOL-Analysis: theory HOL-Library.Extended_Real HOL-Analysis: theory HOL-Analysis.Convex HOL-Analysis: theory HOL-Analysis.Connected HOL-Analysis: theory HOL-Analysis.Determinants HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces HOL-Analysis: theory HOL-Analysis.Function_Topology HOL-Analysis: theory HOL-Analysis.Product_Topology HOL-Analysis: theory HOL-Analysis.T1_Spaces HOL-Analysis: theory HOL-Analysis.Lindelof_Spaces HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces HOL-Analysis: theory HOL-Analysis.Function_Metric HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Sigma_Algebra HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits HOL-Analysis: theory HOL-Analysis.Line_Segment HOL-Analysis: theory HOL-Analysis.Tagged_Division HOL-Analysis: theory HOL-Analysis.Measurable HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Starlike HOL-Analysis: theory HOL-Analysis.Summation_Tests HOL-Analysis: theory HOL-Analysis.Measure_Space HOL-Analysis: theory HOL-Analysis.Uniform_Limit HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function HOL-Analysis: theory HOL-Analysis.Continuous_Extension HOL-Analysis: theory HOL-Analysis.Path_Connected HOL-Analysis: theory HOL-Analysis.Caratheodory HOL-Analysis: theory HOL-Analysis.Derivative HOL-Analysis: theory HOL-Analysis.Homotopy HOL-Analysis: theory HOL-Analysis.Locally HOL-Analysis: theory HOL-Analysis.Borel_Space HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics HOL-Analysis: theory HOL-Analysis.Lipschitz HOL-Analysis: theory HOL-Analysis.Cross3 HOL-Analysis: theory HOL-Analysis.Homeomorphism HOL-Analysis: theory HOL-Analysis.Abstract_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Polytope HOL-Analysis: theory HOL-Analysis.Complex_Transcendental HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration HOL-Analysis: theory HOL-Analysis.Regularity HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem HOL-Analysis: theory HOL-Computational_Algebra.Primes HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers HOL-Analysis: theory HOL-Analysis.Infinite_Products HOL-Analysis: theory HOL-Analysis.Arcwise_Connected HOL-Analysis: theory HOL-Analysis.Multivariate_Analysis HOL-Analysis: theory HOL-Analysis.Retracts HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure HOL-Analysis: theory HOL-Analysis.Smooth_Paths 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.FPS_Convergence 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.Equivalence_Lebesgue_Henstock_Integration HOL-Analysis: theory HOL-Analysis.Integral_Test HOL-Analysis: theory HOL-Analysis.Further_Topology HOL-Analysis: theory HOL-Analysis.Gamma_Function HOL-Analysis: theory HOL-Analysis.Improper_Integral HOL-Analysis: theory HOL-Analysis.Interval_Integral HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem HOL-Analysis: theory HOL-Analysis.Equivalence_Measurable_On_Borel HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution HOL-Analysis: theory HOL-Analysis.Change_Of_Vars HOL-Analysis: theory HOL-Analysis.Simplex_Content HOL-Analysis: theory HOL-Analysis.Jordan_Curve HOL-Analysis: theory HOL-Analysis.Ball_Volume HOL-Analysis: theory HOL-Analysis.Analysis Timing HOL-Analysis (6 threads, 327.539s elapsed time, 1735.702s cpu time, 90.561s GC time, factor 5.30) Finished HOL-Analysis (0:06:33 elapsed time, 0:31:15 cpu time, factor 4.76) HOL-Auth: theory HOL-Auth.Message HOL-Auth: theory HOL-Library.Case_Converter HOL-Auth: theory HOL-Library.Nat_Bijection HOL-Auth: theory HOL-Library.Simps_Case_Conv HOL-Auth: theory HOL-Auth.All_Symmetric HOL-Auth: theory HOL-Auth.Event HOL-Auth: theory HOL-Auth.EventSC HOL-Auth: theory HOL-Auth.Extensions HOL-Auth: theory HOL-Auth.Public HOL-Auth: theory HOL-Auth.Shared HOL-Auth: theory HOL-Auth.Analz HOL-Auth: theory HOL-Auth.List_Msg HOL-Auth: theory HOL-Auth.CertifiedEmail HOL-Auth: theory HOL-Auth.KerberosIV HOL-Auth: theory HOL-Auth.KerberosIV_Gets HOL-Auth: theory HOL-Auth.Guard HOL-Auth: theory HOL-Auth.GuardK HOL-Auth: theory HOL-Auth.KerberosV HOL-Auth: theory HOL-Auth.Kerberos_BAN HOL-Auth: theory HOL-Auth.Guard_Public HOL-Auth: theory HOL-Auth.Guard_NS_Public HOL-Auth: theory HOL-Auth.Proto HOL-Auth: theory HOL-Auth.Kerberos_BAN_Gets HOL-Auth: theory HOL-Auth.NS_Public HOL-Auth: theory HOL-Auth.NS_Public_Bad HOL-Auth: theory HOL-Auth.NS_Shared HOL-Auth: theory HOL-Auth.OtwayRees HOL-Auth: theory HOL-Auth.OtwayReesBella HOL-Auth: theory HOL-Auth.OtwayRees_AN HOL-Auth: theory HOL-Auth.OtwayRees_Bad HOL-Auth: theory HOL-Auth.Recur HOL-Auth: theory HOL-Auth.WooLam HOL-Auth: theory HOL-Auth.Yahalom HOL-Auth: theory HOL-Auth.Yahalom2 HOL-Auth: theory HOL-Auth.Yahalom_Bad HOL-Auth: theory HOL-Auth.ZhouGollmann HOL-Auth: theory HOL-Auth.Guard_Shared HOL-Auth: theory HOL-Auth.Smartcard HOL-Auth: theory HOL-Auth.Guard_OtwayRees HOL-Auth: theory HOL-Auth.Guard_Yahalom HOL-Auth: theory HOL-Auth.Auth_Shared HOL-Auth: theory HOL-Auth.ShoupRubin HOL-Auth: theory HOL-Auth.Auth_Guard_Shared HOL-Auth: theory HOL-Auth.ShoupRubinBella HOL-Auth: theory HOL-Auth.Auth_Public HOL-Auth: theory HOL-Auth.Auth_Smartcard HOL-Auth: theory HOL-Auth.Auth_Guard_Public Timing HOL-Auth (6 threads, 66.725s elapsed time, 328.684s cpu time, 8.004s GC time, factor 4.93) Finished HOL-Auth (0:01:21 elapsed time, 0:05:58 cpu time, factor 4.39) HOL-Bali: theory HOL-Bali.Basis HOL-Bali: theory HOL-Bali.Name HOL-Bali: theory HOL-Bali.Table HOL-Bali: theory HOL-Bali.Type HOL-Bali: theory HOL-Bali.Value HOL-Bali: theory HOL-Bali.Term HOL-Bali: theory HOL-Bali.Decl HOL-Bali: theory HOL-Bali.TypeRel HOL-Bali: theory HOL-Bali.DeclConcepts HOL-Bali: theory HOL-Bali.State HOL-Bali: theory HOL-Bali.WellType HOL-Bali: theory HOL-Bali.Conform HOL-Bali: theory HOL-Bali.Eval HOL-Bali: theory HOL-Bali.DefiniteAssignment HOL-Bali: theory HOL-Bali.WellForm HOL-Bali: theory HOL-Bali.DefiniteAssignmentCorrect HOL-Bali: theory HOL-Bali.Example HOL-Bali: theory HOL-Bali.TypeSafe HOL-Bali: theory HOL-Bali.Evaln HOL-Bali: theory HOL-Bali.AxSem HOL-Bali: theory HOL-Bali.Trans HOL-Bali: theory HOL-Bali.AxCompl HOL-Bali: theory HOL-Bali.AxSound HOL-Bali: theory HOL-Bali.AxExample Timing HOL-Bali (6 threads, 58.822s elapsed time, 228.399s cpu time, 8.309s GC time, factor 3.88) Finished HOL-Bali (0:01:00 elapsed time, 0:03:50 cpu time, factor 3.80) HOL-Cardinals: theory HOL-Cardinals.Fun_More HOL-Cardinals: theory HOL-Cardinals.Order_Relation_More HOL-Cardinals: theory HOL-Cardinals.Order_Union HOL-Cardinals: theory HOL-Cardinals.Wellorder_Extension HOL-Cardinals: theory HOL-Cardinals.Wellfounded_More HOL-Cardinals: theory HOL-Cardinals.Wellorder_Relation HOL-Cardinals: theory HOL-Cardinals.Wellorder_Embedding HOL-Cardinals: theory HOL-Cardinals.Wellorder_Constructions HOL-Cardinals: theory HOL-Cardinals.Cardinal_Order_Relation HOL-Cardinals: theory HOL-Cardinals.Ordinal_Arithmetic HOL-Cardinals: theory HOL-Cardinals.Cardinal_Arithmetic HOL-Cardinals: theory HOL-Cardinals.Cardinals HOL-Cardinals: theory HOL-Cardinals.Bounded_Set Timing HOL-Cardinals (6 threads, 7.450s elapsed time, 43.895s cpu time, 1.429s GC time, factor 5.89) Finished HOL-Cardinals (0:00:09 elapsed time, 0:00:45 cpu time, factor 5.00) HOL-Combinatorics: theory HOL-Combinatorics.Stirling HOL-Combinatorics: theory HOL-Library.Cancellation HOL-Combinatorics: theory HOL-Library.Disjoint_Sets HOL-Combinatorics: theory HOL-Library.FuncSet HOL-Combinatorics: theory HOL-Library.Multiset HOL-Combinatorics: theory HOL-Combinatorics.Permutations HOL-Combinatorics: theory HOL-Combinatorics.List_Permutation HOL-Combinatorics: theory HOL-Combinatorics.Cycles HOL-Combinatorics: theory HOL-Combinatorics.Multiset_Permutations HOL-Combinatorics: theory HOL-Combinatorics.Combinatorics HOL-Combinatorics: theory HOL-Combinatorics.Guide Timing HOL-Combinatorics (6 threads, 8.457s elapsed time, 44.291s cpu time, 1.625s GC time, factor 5.24) Finished HOL-Combinatorics (0:00:10 elapsed time, 0:00:46 cpu time, factor 4.55) Running HOL-Complex_Analysis ... HOL-Complex_Analysis: theory HOL-Library.Landau_Symbols HOL-Complex_Analysis: theory HOL-Complex_Analysis.Contour_Integration HOL-Complex_Analysis: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem HOL-Complex_Analysis: theory HOL-Complex_Analysis.Winding_Numbers HOL-Complex_Analysis: theory HOL-Complex_Analysis.Cauchy_Integral_Formula HOL-Complex_Analysis: theory HOL-Complex_Analysis.Conformal_Mappings HOL-Complex_Analysis: theory HOL-Complex_Analysis.Complex_Singularities HOL-Complex_Analysis: theory HOL-Complex_Analysis.Great_Picard HOL-Complex_Analysis: theory HOL-Complex_Analysis.Riemann_Mapping HOL-Complex_Analysis: theory HOL-Complex_Analysis.Complex_Residues HOL-Complex_Analysis: theory HOL-Complex_Analysis.Residue_Theorem HOL-Complex_Analysis: theory HOL-Complex_Analysis.Complex_Analysis Timing HOL-Complex_Analysis (6 threads, 38.493s elapsed time, 191.654s cpu time, 3.960s GC time, factor 4.98) Finished HOL-Complex_Analysis (0:00:40 elapsed time, 0:03:14 cpu time, factor 4.75) 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.Sorted_Less HOL-Data_Structures: theory HOL-Data_Structures.Cmp HOL-Data_Structures: theory HOL-Data_Structures.Queue_Spec HOL-Data_Structures: theory HOL-Data_Structures.Reverse HOL-Data_Structures: theory HOL-Data_Structures.Time_Funs HOL-Data_Structures: theory HOL-Data_Structures.Tree23 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-Data_Structures.Queue_2Lists HOL-Data_Structures: theory HOL-Data_Structures.Tree234 HOL-Data_Structures: theory HOL-Data_Structures.Set_Specs HOL-Data_Structures: theory HOL-Library.Cancellation HOL-Data_Structures: theory HOL-Data_Structures.Trie_Fun HOL-Data_Structures: theory HOL-Data_Structures.Map_Specs HOL-Data_Structures: theory HOL-Data_Structures.Tries_Binary HOL-Data_Structures: theory HOL-Library.Multiset HOL-Data_Structures: theory HOL-Library.Pattern_Aliases HOL-Data_Structures: theory HOL-Library.Tree HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set HOL-Data_Structures: theory HOL-Data_Structures.Tree23_of_List HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set HOL-Data_Structures: theory HOL-Number_Theory.Fib HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set HOL-Data_Structures: theory HOL-Data_Structures.Tree2 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set HOL-Data_Structures: theory HOL-Data_Structures.Isin2 HOL-Data_Structures: theory HOL-Data_Structures.AA_Set HOL-Data_Structures: theory HOL-Data_Structures.AVL_Bal2_Set HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue_Specs HOL-Data_Structures: theory HOL-Data_Structures.AVL_Bal_Set HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set_Code HOL-Data_Structures: theory HOL-Data_Structures.Height_Balanced_Tree HOL-Data_Structures: theory HOL-Data_Structures.Interval_Tree HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join HOL-Data_Structures: theory HOL-Data_Structures.Lookup2 HOL-Data_Structures: theory HOL-Data_Structures.RBT HOL-Data_Structures: theory HOL-Data_Structures.AA_Map HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map HOL-Data_Structures: theory HOL-Library.Tree_Multiset HOL-Data_Structures: theory HOL-Data_Structures.Heaps 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_Set HOL-Data_Structures: theory HOL-Data_Structures.Sorting HOL-Data_Structures: theory HOL-Library.Tree_Real HOL-Data_Structures: theory HOL-Data_Structures.Balance HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set2 HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join_RBT HOL-Data_Structures: theory HOL-Data_Structures.Braun_Tree HOL-Data_Structures: theory HOL-Data_Structures.Array_Braun HOL-Data_Structures: theory HOL-Data_Structures.Trie_Map HOL-Data_Structures: theory HOL-Data_Structures.Selection HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set HOL-Data_Structures: theory HOL-Data_Structures.AVL_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, 240.760s elapsed time, 1378.324s cpu time, 104.501s GC time, factor 5.72) Finished HOL-Data_Structures (0:04:02 elapsed time, 0:23:01 cpu time, factor 5.69) 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, 64.562s elapsed time, 341.140s cpu time, 6.134s GC time, factor 5.28) Finished HOL-Hoare_Parallel (0:01:06 elapsed time, 0:05:42 cpu time, factor 5.18) HOL-Homology: theory HOL-Cardinals.Fun_More HOL-Homology: theory HOL-Library.Fun_Lexorder HOL-Homology: theory HOL-Cardinals.Order_Relation_More HOL-Homology: theory HOL-Cardinals.Order_Union HOL-Homology: theory HOL-Algebra.Congruence HOL-Homology: theory HOL-Library.Equipollence HOL-Homology: theory HOL-Library.Groups_Big_Fun HOL-Homology: theory HOL-Library.More_List HOL-Homology: theory HOL-Cardinals.Wellfounded_More HOL-Homology: theory HOL-Cardinals.Wellorder_Relation HOL-Homology: theory HOL-Library.Poly_Mapping HOL-Homology: theory HOL-Cardinals.Wellorder_Embedding HOL-Homology: theory HOL-Cardinals.Wellorder_Constructions HOL-Homology: theory HOL-Algebra.Order HOL-Homology: theory HOL-Cardinals.Cardinal_Order_Relation HOL-Homology: theory HOL-Algebra.Lattice HOL-Homology: theory HOL-Cardinals.Cardinal_Arithmetic HOL-Homology: theory HOL-Algebra.Complete_Lattice HOL-Homology: theory HOL-Algebra.Group HOL-Homology: theory HOL-Algebra.Coset HOL-Homology: theory HOL-Algebra.FiniteProduct HOL-Homology: theory HOL-Algebra.Ring HOL-Homology: theory HOL-Algebra.Generated_Groups HOL-Homology: theory HOL-Algebra.Solvable_Groups HOL-Homology: theory HOL-Algebra.Elementary_Groups HOL-Homology: theory HOL-Algebra.Exact_Sequence HOL-Homology: theory HOL-Algebra.Product_Groups HOL-Homology: theory HOL-Algebra.Free_Abelian_Groups HOL-Homology: theory HOL-Homology.Simplices HOL-Homology: theory HOL-Algebra.AbelCoset HOL-Homology: theory HOL-Algebra.Module HOL-Homology: theory HOL-Homology.Homology_Groups HOL-Homology: theory HOL-Algebra.Ideal HOL-Homology: theory HOL-Algebra.RingHom HOL-Homology: theory HOL-Algebra.UnivPoly HOL-Homology: theory HOL-Algebra.Multiplicative_Group HOL-Homology: theory HOL-Homology.Brouwer_Degree HOL-Homology: theory HOL-Homology.Invariance_of_Domain HOL-Homology: theory HOL-Homology.Homology Timing HOL-Homology (6 threads, 71.980s elapsed time, 354.792s cpu time, 14.235s GC time, factor 4.93) Finished HOL-Homology (0:01:14 elapsed time, 0:05:57 cpu time, factor 4.80) Running HOL-Imperative_HOL ... HOL-Imperative_HOL: theory HOL-Library.Adhoc_Overloading HOL-Imperative_HOL: theory HOL-Imperative_HOL.Sorted_List HOL-Imperative_HOL: theory HOL-Library.Cancellation HOL-Imperative_HOL: theory HOL-Library.Code_Abstract_Nat HOL-Imperative_HOL: theory HOL-Library.Code_Target_Int HOL-Imperative_HOL: theory HOL-Library.LaTeXsugar HOL-Imperative_HOL: theory HOL-Library.Code_Target_Nat HOL-Imperative_HOL: theory HOL-Library.Nat_Bijection HOL-Imperative_HOL: theory HOL-Library.Monad_Syntax HOL-Imperative_HOL: theory HOL-Library.Old_Datatype HOL-Imperative_HOL: theory HOL-Library.RBT_Impl HOL-Imperative_HOL: theory HOL-Library.Code_Target_Numeral HOL-Imperative_HOL: theory HOL-Library.Multiset HOL-Imperative_HOL: theory HOL-Library.Countable HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad HOL-Imperative_HOL: theory HOL-Imperative_HOL.List_Sublist HOL-Imperative_HOL: theory HOL-Imperative_HOL.Array HOL-Imperative_HOL: theory HOL-Imperative_HOL.Ref HOL-Imperative_HOL: theory HOL-Imperative_HOL.Subarray HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL HOL-Imperative_HOL: theory HOL-Imperative_HOL.Linked_Lists HOL-Imperative_HOL: theory HOL-Imperative_HOL.Overview HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse HOL-Imperative_HOL: theory HOL-Imperative_HOL.SatChecker (see also /media/data/jenkins/workspace/isabelle-nightly-benchmark/heaps/polyml-5.8.2_x86_64_32-linux/log/HOL-Imperative_HOL) *** Failed to load theory "HOL-Imperative_HOL.Imperative_HOL_ex" (unresolved "HOL-Imperative_HOL.Imperative_Quicksort", "HOL-Imperative_HOL.Imperative_Reverse", "HOL-Imperative_HOL.Linked_Lists") *** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null *** At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy") *** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null *** At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy") *** At command "by" (line 69 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy") *** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null *** At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy") *** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null *** At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy") *** At command "by" (line 56 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy") *** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null *** At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy") HOL-Library: theory HOL-Library.AList HOL-Library: theory HOL-Library.BNF_Axiomatization HOL-Library: theory HOL-Library.Adhoc_Overloading HOL-Library: theory HOL-Library.Boolean_Algebra HOL-Library: theory HOL-Library.BNF_Corec HOL-Library: theory HOL-Library.Cancellation HOL-Library: theory HOL-Library.Monad_Syntax HOL-Library: theory HOL-Library.Case_Converter HOL-Library: theory HOL-Library.State_Monad HOL-Library: theory HOL-Library.Bit_Operations HOL-Library: theory HOL-Library.Code_Lazy HOL-Library: theory HOL-Library.Multiset HOL-Library: theory HOL-Library.Simps_Case_Conv HOL-Library: theory HOL-Library.Extended HOL-Library: theory HOL-Library.Char_ord HOL-Library: theory HOL-Library.Code_Abstract_Nat HOL-Library: theory HOL-Library.Code_Binary_Nat HOL-Library: theory HOL-Library.DAList 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.Code_Test HOL-Library: theory HOL-Library.Code_Target_Numeral HOL-Library: theory HOL-Library.Comparator HOL-Library: theory HOL-Library.Conditional_Parametricity HOL-Library: theory HOL-Library.Confluence HOL-Library: theory HOL-Library.Datatype_Records HOL-Library: theory HOL-Library.Confluent_Quotient HOL-Library: theory HOL-Library.Dlist HOL-Library: theory HOL-Library.Debug HOL-Library: theory HOL-Library.Disjoint_Sets HOL-Library: theory HOL-Library.Dual_Ordered_Lattice 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.Groups_Big_Fun HOL-Library: theory HOL-Library.Function_Division 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.DAList_Multiset HOL-Library: theory HOL-Library.Multiset_Order HOL-Library: theory HOL-Library.Lattice_Syntax HOL-Library: theory HOL-Library.Combine_PER HOL-Library: theory HOL-Library.Complete_Partial_Order2 HOL-Library: theory HOL-Library.ListVector HOL-Library: theory HOL-Library.List_Lenlexorder 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.Poly_Mapping HOL-Library: theory HOL-Library.Nat_Bijection HOL-Library: theory HOL-Library.Stream 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.Product_Order HOL-Library: theory HOL-Library.Quotient_Product HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck HOL-Library: theory HOL-Library.Cardinality HOL-Library: theory HOL-Library.Quotient_Set HOL-Library: theory HOL-Library.Quotient_Sum HOL-Library: theory HOL-Library.Quotient_List HOL-Library: theory HOL-Library.Finite_Lattice HOL-Library: theory HOL-Library.Quotient_Type HOL-Library: theory HOL-Library.RBT_Impl 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.Signed_Division HOL-Library: theory HOL-Library.Numeral_Type HOL-Library: theory HOL-Library.Sorting_Algorithms 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.While_Combinator HOL-Library: theory HOL-Library.Prefix_Order HOL-Library: theory HOL-Library.Subseq_Order HOL-Library: theory HOL-Library.Saturated HOL-Library: theory HOL-Library.Word HOL-Library: theory HOL-Library.Z2 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint HOL-Library: theory HOL-Library.Countable HOL-Library: theory HOL-Library.BigO HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float 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.Tree_Multiset 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.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.Finite_Map HOL-Library: theory HOL-Library.Log_Nat HOL-Library: theory HOL-Library.Lub_Glb 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.Sum_of_Squares HOL-Library: theory HOL-Library.Extended_Nat HOL-Library: theory HOL-Library.Interval HOL-Library: theory HOL-Library.Float HOL-Library: theory HOL-Library.Extended_Real HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams HOL-Library: theory HOL-Library.Code_Target_Numeral_Float HOL-Library: theory HOL-Library.Interval_Float HOL-Library: theory HOL-Library.Tree_Real 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.2_x86_64_32-linux/log/HOL-Library) *** Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-Library.Finite_Map") *** Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Disjoint_FSets", "HOL-Library.Finite_Map") *** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null *** At command "export_code" (line 1440 of "~~/src/HOL/Library/Finite_Map.thy") HOL-Computational_Algebra CANCELLED HOL-Datatype_Benchmark CANCELLED HOL-Datatype_Examples CANCELLED HOL-MicroJava: theory HOL-Eisbach.Eisbach HOL-MicroJava: theory HOL-Library.While_Combinator HOL-MicroJava: theory HOL-Library.Transitive_Closure_Table HOL-MicroJava: theory HOL-MicroJava.Semilat HOL-MicroJava: theory HOL-MicroJava.JBasis HOL-MicroJava: theory HOL-MicroJava.Err HOL-MicroJava: theory HOL-MicroJava.AuxLemmas HOL-MicroJava: theory HOL-MicroJava.Type HOL-MicroJava: theory HOL-MicroJava.Listn HOL-MicroJava: theory HOL-MicroJava.Opt HOL-MicroJava: theory HOL-MicroJava.Product HOL-MicroJava: theory HOL-MicroJava.Typing_Framework HOL-MicroJava: theory HOL-MicroJava.Semilattices HOL-MicroJava: theory HOL-MicroJava.SemilatAlg HOL-MicroJava: theory HOL-MicroJava.Kildall HOL-MicroJava: theory HOL-MicroJava.LBVSpec HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_err HOL-MicroJava: theory HOL-MicroJava.Decl HOL-MicroJava: theory HOL-MicroJava.Value HOL-MicroJava: theory HOL-MicroJava.SystemClasses HOL-MicroJava: theory HOL-MicroJava.TypeRel HOL-MicroJava: theory HOL-MicroJava.LBVComplete HOL-MicroJava: theory HOL-MicroJava.LBVCorrect HOL-MicroJava: theory HOL-MicroJava.Term HOL-MicroJava: theory HOL-MicroJava.WellForm HOL-MicroJava: theory HOL-MicroJava.State HOL-MicroJava: theory HOL-MicroJava.Abstract_BV HOL-MicroJava: theory HOL-MicroJava.Exceptions HOL-MicroJava: theory HOL-MicroJava.JType HOL-MicroJava: theory HOL-MicroJava.JVMType HOL-MicroJava: theory HOL-MicroJava.WellType HOL-MicroJava: theory HOL-MicroJava.Conform HOL-MicroJava: theory HOL-MicroJava.Eval HOL-MicroJava: theory HOL-MicroJava.TypeInf HOL-MicroJava: theory HOL-MicroJava.JVMState HOL-MicroJava: theory HOL-MicroJava.JVMInstructions HOL-MicroJava: theory HOL-MicroJava.JVMExceptions HOL-MicroJava: theory HOL-MicroJava.JVMExecInstr HOL-MicroJava: theory HOL-MicroJava.Effect HOL-MicroJava: theory HOL-MicroJava.JVMExec HOL-MicroJava: theory HOL-MicroJava.DefsComp HOL-MicroJava: theory HOL-MicroJava.JVMDefensive HOL-MicroJava: theory HOL-MicroJava.JVMListExample HOL-MicroJava: theory HOL-MicroJava.Index HOL-MicroJava: theory HOL-MicroJava.TranslCompTp HOL-MicroJava: theory HOL-MicroJava.TranslComp HOL-MicroJava: theory HOL-MicroJava.Example HOL-MicroJava: theory HOL-MicroJava.JListExample HOL-MicroJava: theory HOL-MicroJava.JTypeSafe HOL-MicroJava: theory HOL-MicroJava.LemmasComp HOL-MicroJava: theory HOL-MicroJava.CorrComp HOL-MicroJava: theory HOL-MicroJava.BVSpec HOL-MicroJava: theory HOL-MicroJava.EffectMono HOL-MicroJava: theory HOL-MicroJava.Altern HOL-MicroJava: theory HOL-MicroJava.Correct HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_JVM HOL-MicroJava: theory HOL-MicroJava.BVSpecTypeSafe HOL-MicroJava: theory HOL-MicroJava.JVM HOL-MicroJava: theory HOL-MicroJava.CorrCompTp HOL-MicroJava: theory HOL-MicroJava.BVNoTypeError HOL-MicroJava: theory HOL-MicroJava.BVExample HOL-MicroJava: theory HOL-MicroJava.LBVJVM HOL-MicroJava: theory HOL-MicroJava.MicroJava Timing HOL-MicroJava (6 threads, 66.984s elapsed time, 316.859s cpu time, 8.326s GC time, factor 4.73) Finished HOL-MicroJava (0:01:08 elapsed time, 0:05:19 cpu time, factor 4.64) HOL-Nominal: theory HOL-Library.Old_Datatype HOL-Nominal: theory HOL-Library.Infinite_Set HOL-Nominal: theory HOL-Nominal.Nominal Timing HOL-Nominal (6 threads, 7.215s elapsed time, 20.914s cpu time, 0.704s GC time, factor 2.90) Finished HOL-Nominal (0:00:15 elapsed time, 0:00:36 cpu time, factor 2.30) Running HOL-Nominal-Examples ... HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR_Takahashi HOL-Nominal-Examples: theory HOL-Nominal-Examples.CK_Machine HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class1 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Contexts HOL-Nominal-Examples: theory HOL-Nominal-Examples.Compile HOL-Nominal-Examples: theory HOL-Nominal-Examples.Crary HOL-Nominal-Examples: theory HOL-Nominal-Examples.Fsub HOL-Nominal-Examples: theory HOL-Nominal-Examples.Height HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lam_Funs HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lambda_mu HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR HOL-Nominal-Examples: theory HOL-Nominal-Examples.SN HOL-Nominal-Examples: theory HOL-Nominal-Examples.LocalWeakening HOL-Nominal-Examples: theory HOL-Nominal-Examples.Pattern HOL-Nominal-Examples: theory HOL-Nominal-Examples.SOS HOL-Nominal-Examples: theory HOL-Nominal-Examples.Standardization HOL-Nominal-Examples: theory HOL-Nominal-Examples.Support HOL-Nominal-Examples: theory HOL-Nominal-Examples.Type_Preservation HOL-Nominal-Examples: theory HOL-Nominal-Examples.W HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3 HOL-Nominal-Examples: theory HOL-Nominal-Examples.VC_Condition Timing HOL-Nominal-Examples (6 threads, 244.525s elapsed time, 1171.104s cpu time, 78.241s GC time, factor 4.79) Finished HOL-Nominal-Examples (0:04:06 elapsed time, 0:19:33 cpu time, factor 4.76) HOL-Nonstandard_Analysis CANCELLED HOL-Nonstandard_Analysis-Examples CANCELLED Running HOL-Predicate_Compile_Examples ... HOL-Predicate_Compile_Examples: theory HOL-Library.Predicate_Compile_Alternative_Defs HOL-Predicate_Compile_Examples: theory HOL-Library.Predicate_Compile_Quickcheck HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Tests HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Examples HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Specialisation_Examples HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_1 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_2 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_3 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_4 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Quickcheck_Examples HOL-Predicate_Compile_Examples: theory HOL-Library.Code_Prolog HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Code_Prolog_Examples HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Lambda_Example HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Context_Free_Grammar_Example HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.List_Examples HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example_Prolog HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Reg_Exp_Example Timing HOL-Predicate_Compile_Examples (6 threads, 50.438s elapsed time, 198.426s cpu time, 12.056s GC time, factor 3.93) Finished HOL-Predicate_Compile_Examples (0:00:52 elapsed time, 0:03:20 cpu time, factor 3.83) HOL-Probability: theory HOL-Library.Lattice_Syntax HOL-Probability: theory HOL-Library.Conditional_Parametricity HOL-Probability: theory HOL-Library.Adhoc_Overloading HOL-Probability: theory HOL-Library.AList 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-Combinatorics.Multiset_Permutations HOL-Probability: theory HOL-Library.AList_Mapping HOL-Probability: theory HOL-Library.Diagonal_Subsequence 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.Product_PMF HOL-Probability: theory HOL-Probability.Hoeffding 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.2_x86_64_32-linux/log/HOL-Probability) *** 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_OCAMLFIND" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null *** At command "export_code" (line 1440 of "~~/src/HOL/Library/Finite_Map.thy") HOL-Proofs: theory Tools.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.Set_Interval HOL-Proofs: theory HOL.Numeral_Simprocs 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, 370.532s elapsed time, 635.346s cpu time, 97.928s GC time, factor 1.71) Finished HOL-Proofs (0:07:53 elapsed time, 0:14:17 cpu time, factor 1.81) Running HOL-Proofs-Extraction ... HOL-Proofs-Extraction: theory HOL-Library.Code_Abstract_Nat HOL-Proofs-Extraction: theory HOL-Library.Cancellation 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-Proofs-Extraction.Util HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Nat HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.QuotRem HOL-Proofs-Extraction: theory HOL-Library.Multiset HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Numeral 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, 97.046s elapsed time, 167.491s cpu time, 7.220s GC time, factor 1.73) Finished HOL-Proofs-Extraction (0:01:39 elapsed time, 0:02:49 cpu time, factor 1.71) 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.Standardization HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.StrongNorm HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.WeakNorm Timing HOL-Proofs-Lambda (6 threads, 101.453s elapsed time, 118.486s cpu time, 3.898s GC time, factor 1.17) Finished HOL-Proofs-Lambda (0:01:43 elapsed time, 0:02:00 cpu time, factor 1.16) HOL-Quickcheck_Benchmark CANCELLED Running HOL-Quickcheck_Examples ... HOL-Quickcheck_Examples: theory HOL-Library.Cancellation HOL-Quickcheck_Examples: theory HOL-Library.AList HOL-Quickcheck_Examples: theory HOL-Library.Confluence HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Interfaces HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Completeness HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples HOL-Quickcheck_Examples: theory HOL-Library.Confluent_Quotient HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting HOL-Quickcheck_Examples: theory HOL-Library.Dlist HOL-Quickcheck_Examples: theory HOL-Library.Multiset HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting_Example HOL-Quickcheck_Examples: theory HOL-Library.DAList HOL-Quickcheck_Examples: theory HOL-Library.DAList_Multiset HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Examples HOL-Quickcheck_Examples: theory HOL-Library.Predicate_Compile_Alternative_Defs HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Narrowing_Examples HOL-Quickcheck_Examples: theory HOL-Library.Predicate_Compile_Quickcheck HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Hotel_Example Timing HOL-Quickcheck_Examples (6 threads, 103.900s elapsed time, 188.889s cpu time, 6.263s GC time, factor 1.82) Finished HOL-Quickcheck_Examples (0:01:45 elapsed time, 0:03:10 cpu time, factor 1.81) HOL-Quotient_Examples CANCELLED Running HOL-Record_Benchmark ... HOL-Record_Benchmark: theory HOL-Record_Benchmark.Record_Benchmark Timing HOL-Record_Benchmark (6 threads, 146.956s elapsed time, 217.233s cpu time, 11.171s GC time, factor 1.48) Finished HOL-Record_Benchmark (0:02:29 elapsed time, 0:03:39 cpu time, factor 1.47) HOL-SET_Protocol: theory HOL-Library.Nat_Bijection HOL-SET_Protocol: theory HOL-SET_Protocol.Message_SET HOL-SET_Protocol: theory HOL-SET_Protocol.Event_SET HOL-SET_Protocol: theory HOL-SET_Protocol.Public_SET HOL-SET_Protocol: theory HOL-SET_Protocol.Cardholder_Registration HOL-SET_Protocol: theory HOL-SET_Protocol.Merchant_Registration HOL-SET_Protocol: theory HOL-SET_Protocol.Purchase HOL-SET_Protocol: theory HOL-SET_Protocol.SET_Protocol Timing HOL-SET_Protocol (6 threads, 24.867s elapsed time, 115.037s cpu time, 1.912s GC time, factor 4.63) Finished HOL-SET_Protocol (0:00:26 elapsed time, 0:01:56 cpu time, factor 4.41) HOL-SMT_Examples: theory HOL-Library.Boolean_Algebra HOL-SMT_Examples: theory HOL-Library.Phantom_Type HOL-SMT_Examples: theory HOL-SMT_Examples.Boogie HOL-SMT_Examples: theory HOL-SMT_Examples.SMT_Examples HOL-SMT_Examples: theory HOL-SMT_Examples.SMT_Examples_Verit HOL-SMT_Examples: theory HOL-SMT_Examples.SMT_Tests HOL-SMT_Examples: theory HOL-Library.Bit_Operations HOL-SMT_Examples: theory HOL-SMT_Examples.SMT_Tests_Verit HOL-SMT_Examples: theory HOL-Library.Cardinality HOL-SMT_Examples: theory HOL-Library.Numeral_Type HOL-SMT_Examples: theory HOL-Library.Type_Length HOL-SMT_Examples: theory HOL-Library.Word HOL-SMT_Examples: theory HOL-SMT_Examples.SMT_Word_Examples Timing HOL-SMT_Examples (6 threads, 63.987s elapsed time, 192.790s cpu time, 4.637s GC time, factor 3.01) Finished HOL-SMT_Examples (0:01:05 elapsed time, 0:03:14 cpu time, factor 2.96) HOL-UNITY: theory HOL-Library.Cancellation HOL-UNITY: theory HOL-UNITY.ListOrder HOL-UNITY: theory HOL-UNITY.UNITY HOL-UNITY: theory HOL-UNITY.Constrains HOL-UNITY: theory HOL-UNITY.Deadlock HOL-UNITY: theory HOL-UNITY.FP HOL-UNITY: theory HOL-UNITY.Network HOL-UNITY: theory HOL-UNITY.WFair HOL-UNITY: theory HOL-Library.Multiset HOL-UNITY: theory HOL-UNITY.SubstAx HOL-UNITY: theory HOL-UNITY.Token HOL-UNITY: theory HOL-UNITY.Detects HOL-UNITY: theory HOL-UNITY.Union HOL-UNITY: theory HOL-UNITY.Comp HOL-UNITY: theory HOL-UNITY.Guar HOL-UNITY: theory HOL-UNITY.Transformers HOL-UNITY: theory HOL-UNITY.Extend HOL-UNITY: theory HOL-UNITY.ProgressSets HOL-UNITY: theory HOL-UNITY.Project HOL-UNITY: theory HOL-UNITY.Rename HOL-UNITY: theory HOL-UNITY.Lift_prog HOL-UNITY: theory HOL-UNITY.ELT HOL-UNITY: theory HOL-UNITY.PPROD HOL-UNITY: theory HOL-Library.Multiset_Order HOL-UNITY: theory HOL-UNITY.Follows HOL-UNITY: theory HOL-UNITY.UNITY_Main HOL-UNITY: theory HOL-UNITY.AllocBase HOL-UNITY: theory HOL-UNITY.Alloc HOL-UNITY: theory HOL-UNITY.AllocImpl HOL-UNITY: theory HOL-UNITY.Client HOL-UNITY: theory HOL-UNITY.Channel HOL-UNITY: theory HOL-UNITY.Common HOL-UNITY: theory HOL-UNITY.Counter HOL-UNITY: theory HOL-UNITY.Counterc HOL-UNITY: theory HOL-UNITY.Handshake HOL-UNITY: theory HOL-UNITY.Lift HOL-UNITY: theory HOL-UNITY.Mutex HOL-UNITY: theory HOL-UNITY.NSP_Bad HOL-UNITY: theory HOL-UNITY.PriorityAux HOL-UNITY: theory HOL-UNITY.Progress HOL-UNITY: theory HOL-UNITY.Reach HOL-UNITY: theory HOL-UNITY.Priority HOL-UNITY: theory HOL-UNITY.TimerArray HOL-UNITY: theory HOL-UNITY.Reachability Timing HOL-UNITY (6 threads, 23.084s elapsed time, 126.660s cpu time, 4.263s GC time, factor 5.49) Finished HOL-UNITY (0:00:24 elapsed time, 0:02:08 cpu time, factor 5.15) 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, 11.706s elapsed time, 37.627s cpu time, 1.697s GC time, factor 3.21) Finished HOLCF (0:00:21 elapsed time, 0:00:57 cpu time, factor 2.63) IOA: theory IOA.ShortExecutions IOA: theory IOA.RefCorrectness IOA: theory IOA.SimCorrectness IOA: theory IOA.Compositionality Timing IOA (6 threads, 7.012s elapsed time, 31.512s cpu time, 0.996s GC time, factor 4.49) Finished IOA (0:00:08 elapsed time, 0:00:33 cpu time, factor 3.77) Timing ZF (6 threads, 12.749s elapsed time, 42.797s cpu time, 1.986s GC time, factor 3.36) Finished ZF (0:00:16 elapsed time, 0:00:47 cpu time, factor 2.87) ZF-Induct: theory ZF-Induct.Acc ZF-Induct: theory ZF-Induct.Binary_Trees ZF-Induct: theory ZF-Induct.Comb ZF-Induct: theory ZF-Induct.Datatypes ZF-Induct: theory ZF-Induct.FoldSet ZF-Induct: theory ZF-Induct.ListN 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.238s elapsed time, 11.747s cpu time, 0.477s GC time, factor 3.63) Finished ZF-Induct (0:00:04 elapsed time, 0:00:14 cpu time, factor 2.86) ZF-UNITY: theory ZF-UNITY.MultisetSum ZF-UNITY: theory ZF-UNITY.GenPrefix ZF-UNITY: theory ZF-UNITY.State 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.Merge ZF-UNITY: theory ZF-UNITY.AllocImpl Timing ZF-UNITY (6 threads, 5.271s elapsed time, 29.295s cpu time, 0.897s GC time, factor 5.56) Finished ZF-UNITY (0:00:06 elapsed time, 0:00:29 cpu time, factor 4.92) Unfinished session(s): HOL-Algebra, 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-Nonstandard_Analysis, HOL-Nonstandard_Analysis-Examples, HOL-Number_Theory, HOL-Probability, HOL-Probability-ex, HOL-Quickcheck_Benchmark, HOL-Quotient_Examples, HOL-ex
Group main: 0:15:45 elapsed time, 1:08:41 cpu time, factor 4.36 Group timing: 0:42:59 elapsed time, 2:44:50 cpu time, factor 3.83 Overall: 0:51:57 elapsed time, 3:03:33 cpu time, factor 3.53
Session HOL-Nonstandard_Analysis-Examples: CANCELLED Session HOL-Algebra: CANCELLED Session HOL-Probability: FAILED 1 Session HOL-Datatype_Examples: CANCELLED Session HOL-Corec_Examples: CANCELLED Session HOL-Quickcheck_Benchmark: CANCELLED Session HOL-Imperative_HOL: FAILED 1 Session HOL-Probability-ex: CANCELLED Session HOL-Metis_Examples: CANCELLED Session HOL-Datatype_Benchmark: 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 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