Started by an SCM change Running as SYSTEM [EnvInject] - Loading node environment variables. Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-nightly-benchmark [isabelle-nightly-benchmark] $ hg showconfig paths.default [isabelle-nightly-benchmark] $ hg pull --rev default pulling from http://isabelle.in.tum.de/repos/isabelle/ no changes found [isabelle-nightly-benchmark] $ hg update --clean --rev default 1 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 572ab9e64e182bd49bdf1444d4c3c848bd915fd0 --template exists\n exists [isabelle-nightly-benchmark] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(572ab9e64e182bd49bdf1444d4c3c848bd915fd0)" --encoding UTF-8 --encodingmode replace No emails were triggered. [isabelle-nightly-benchmark] $ /bin/sh -xe /tmp/jenkins6514940493936769114.sh + Admin/jenkins/run_build benchmark + set -e + PROFILE=benchmark + shift + bin/isabelle components -a + bin/isabelle jedit -bf ### Building graph browser ... warning: [options] bootstrap class path not set in conjunction with -source 6 warning: [options] source value 6 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. Note: Some input files use or override a deprecated API. Note: Recompile with -Xlint:deprecation for details. Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. 3 warnings ### Building Isabelle/Scala ... ### Building Isabelle/jEdit ... + bin/isabelle ocaml_setup # 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: opam update [NOTE] Package zarith is already installed (current version is 1.7). + bin/isabelle ghc_setup stack will use a sandboxed GHC it installed For more information on paths, see 'stack path' and 'stack exec env' To use this GHC and packages outside of a project, consider using: stack ghc, stack ghci, stack runghc, or stack exec The Glorious Glasgow Haskell Compilation System, version 8.6.4 + bin/isabelle ci_build_benchmark === CONFIGURATION === ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64_32-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8.1-20191124/x86_64_32-linux" ML_SYSTEM="polyml-5.8.1" ML_OPTIONS="-H 4000 --maxheap 8G" jobs = 1, threads = 6, numa = false === BUILD === Build started at Fri, 7 Feb 2020 23:51:02 GMT Isabelle id 5de8c6d92bd0 === LOG === Session Pure/Pure Session FOL/FOL Session Tools/Tools Session HOL/HOL (main) Session HOL/HOL-Cardinals (timing) Session HOL/HOL-Hoare_Parallel (timing) Session HOL/HOL-Library (main timing) Session HOL/HOL-Auth (timing) Session HOL/HOL-UNITY (timing) Session HOL/HOL-Bali (timing) Session HOL/HOL-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-Eisbach 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-ex (timing) Session HOL/HOL-Corec_Examples (timing) Session HOL/HOL-Datatype_Benchmark Session HOL/HOL-Datatype_Examples (timing) Session HOL/HOL-IMP (timing) Session HOL/HOL-Imperative_HOL (timing) Session HOL/HOL-Metis_Examples (timing) Session HOL/HOL-MicroJava (timing) Session HOL/HOL-Nominal Session HOL/HOL-Nominal-Examples (timing) Session HOL/HOL-Predicate_Compile_Examples (timing) Session HOL/HOL-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-Lambda (timing) Session HOL/HOL-Quickcheck_Benchmark Session HOL/HOL-Quickcheck_Examples (timing) Session HOL/HOL-SET_Protocol (timing) Session HOL/HOL-Record_Benchmark Session HOL/HOL-Word (main timing) Session HOL/HOL-Word-SMT_Examples (timing) Session HOL/HOLCF (main timing) Session HOL/IOA (timing) Session ZF/ZF (main timing) Session ZF/ZF-Induct Session ZF/ZF-UNITY (timing) Building Pure ... Pure: theory Pure Pure: theory ML_Bootstrap Pure: theory Pure.Sessions Timing Pure (1 threads, 0.960s elapsed time, 0.964s cpu time, 0.000s GC time, factor 1.00) Timing Pure (1 threads, 0.960s elapsed time, 0.964s cpu time, 0.000s GC time, factor 1.00) Finished Pure (0:00:21 elapsed time, 0:00:20 cpu time, factor 1.00) Building HOL ... HOL: theory Tools.Code_Generator HOL: theory HOL.HOL HOL: theory HOL.Argo HOL: theory HOL.Ctr_Sugar HOL: theory HOL.Orderings HOL: theory HOL.Groups HOL: theory HOL.SAT HOL: theory HOL.Lattices HOL: theory HOL.Set HOL: theory HOL.Fun HOL: theory HOL.Typedef HOL: theory HOL.Complete_Lattices HOL: theory HOL.Rings HOL: theory HOL.Inductive HOL: theory HOL.Product_Type HOL: theory HOL.Sum_Type HOL: theory HOL.Complete_Partial_Order HOL: theory HOL.Nat HOL: theory HOL.Fields HOL: theory HOL.Meson HOL: theory HOL.ATP HOL: theory HOL.Metis HOL: theory HOL.Finite_Set HOL: theory HOL.Relation HOL: theory HOL.Transitive_Closure HOL: theory HOL.Wellfounded HOL: theory HOL.Fun_Def_Base HOL: theory HOL.Hilbert_Choice HOL: theory HOL.Wfrec HOL: theory HOL.Order_Relation HOL: theory HOL.BNF_Wellorder_Relation HOL: theory HOL.BNF_Wellorder_Embedding HOL: theory HOL.Zorn HOL: theory HOL.BNF_Wellorder_Constructions HOL: theory HOL.BNF_Cardinal_Order_Relation HOL: theory HOL.BNF_Cardinal_Arithmetic HOL: theory HOL.BNF_Def HOL: theory HOL.BNF_Composition HOL: theory HOL.Basic_BNFs HOL: theory HOL.BNF_Fixpoint_Base HOL: theory HOL.BNF_Least_Fixpoint HOL: theory HOL.Basic_BNF_LFPs HOL: theory HOL.Transfer HOL: theory HOL.Num HOL: theory HOL.Power HOL: theory HOL.Groups_Big HOL: theory HOL.Equiv_Relations HOL: theory HOL.Lifting HOL: theory HOL.Lifting_Set HOL: theory HOL.Option HOL: theory HOL.Quotient HOL: theory HOL.Extraction HOL: theory HOL.Lattices_Big HOL: theory HOL.Partial_Function HOL: theory HOL.Fun_Def HOL: theory HOL.Int HOL: theory HOL.Euclidean_Division HOL: theory HOL.Parity HOL: theory HOL.Divides HOL: theory HOL.Code_Numeral HOL: theory HOL.Numeral_Simprocs HOL: theory HOL.SMT HOL: theory HOL.Set_Interval HOL: theory HOL.Semiring_Normalization HOL: theory HOL.Groebner_Basis HOL: theory HOL.Conditionally_Complete_Lattices HOL: theory HOL.Filter HOL: theory HOL.Presburger HOL: theory HOL.Sledgehammer HOL: theory HOL.List HOL: theory HOL.Groups_List HOL: theory HOL.Map HOL: theory HOL.Factorial HOL: theory HOL.GCD HOL: theory HOL.Enum HOL: theory HOL.Random HOL: theory HOL.Binomial HOL: theory HOL.String HOL: theory HOL.BNF_Greatest_Fixpoint HOL: theory HOL.Predicate HOL: theory HOL.Typerep HOL: theory HOL.Lazy_Sequence HOL: theory HOL.Limited_Sequence HOL: theory HOL.Code_Evaluation HOL: theory HOL.Quickcheck_Random HOL: theory HOL.Quickcheck_Exhaustive HOL: theory HOL.Quickcheck_Narrowing HOL: theory HOL.Random_Pred HOL: theory HOL.Random_Sequence HOL: theory HOL.Record HOL: theory HOL.Predicate_Compile HOL: theory HOL.Nitpick HOL: theory HOL.Nunchaku HOL: theory Main HOL: theory HOL.Archimedean_Field HOL: theory HOL.Hull HOL: theory HOL.Topological_Spaces HOL: theory HOL.Modules HOL: theory HOL.Vector_Spaces HOL: theory HOL.Rat HOL: theory HOL.Real HOL: theory HOL.Real_Vector_Spaces HOL: theory HOL.Inequalities HOL: theory HOL.Limits HOL: theory HOL.Deriv HOL: theory HOL.Series HOL: theory HOL.NthRoot HOL: theory HOL.Transcendental HOL: theory HOL.Complex HOL: theory HOL.MacLaurin HOL: theory Complex_Main Timing HOL (6 threads, 203.142s elapsed time, 698.256s cpu time, 55.632s GC time, factor 3.44) Timing HOL (6 threads, 203.142s elapsed time, 698.256s cpu time, 55.632s GC time, factor 3.44) Finished HOL (0:04:02 elapsed time, 0:13:00 cpu time, factor 3.22) Building HOL-Analysis ... 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-Analysis.Metric_Arith HOL-Analysis: theory HOL-Library.Countable 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-Analysis.Poly_Roots HOL-Analysis: theory HOL-Library.Cardinality 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-Analysis.Euclidean_Space HOL-Analysis: theory HOL-Library.Periodic_Fun 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-Library.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-Analysis.Convex HOL-Analysis: theory HOL-Library.Extended_Real HOL-Analysis: theory HOL-Analysis.Determinants HOL-Analysis: theory HOL-Analysis.Connected 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.Brouwer_Fixpoint HOL-Analysis: theory HOL-Analysis.Polytope HOL-Analysis: theory HOL-Analysis.Complex_Transcendental HOL-Analysis: theory HOL-Computational_Algebra.Primes HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration HOL-Analysis: theory HOL-Analysis.Regularity HOL-Analysis: theory HOL-Analysis.Arcwise_Connected 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.Fashoda_Theorem 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.Embed_Measure HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure HOL-Analysis: theory HOL-Analysis.Smooth_Paths 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.Equivalence_Measurable_On_Borel HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution 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.Jordan_Curve HOL-Analysis: theory HOL-Analysis.Ball_Volume HOL-Analysis: theory HOL-Analysis.Analysis Timing HOL-Analysis (6 threads, 316.217s elapsed time, 1648.000s cpu time, 90.688s GC time, factor 5.21) Timing HOL-Analysis (6 threads, 316.217s elapsed time, 1648.000s cpu time, 90.688s GC time, factor 5.21) Finished HOL-Analysis (0:06:22 elapsed time, 0:29:44 cpu time, factor 4.67) Running HOL-Cardinals ... HOL-Cardinals: theory HOL-Cardinals.Order_Relation_More HOL-Cardinals: theory HOL-Cardinals.Fun_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.495s elapsed time, 42.484s cpu time, 1.704s GC time, factor 5.67) Timing HOL-Cardinals (6 threads, 7.495s elapsed time, 42.484s cpu time, 1.704s GC time, factor 5.67) Finished HOL-Cardinals (0:00:08 elapsed time, 0:00:43 cpu time, factor 5.00) Running HOL-Complex_Analysis ... 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 Build timed out (after 300 minutes). Marking the build as aborted. Build was aborted Archiving artifacts Started calculate disk usage of build Finished Calculation of disk usage of build in 0 seconds Started calculate disk usage of workspace Finished Calculation of disk usage of workspace in 0 seconds No emails were triggered. Finished: ABORTED