Console Output

01:35:40 Started by an SCM change
01:35:40 Running as SYSTEM
01:35:40 [EnvInject] - Loading node environment variables.
01:35:40 Building remotely on workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-nightly-benchmark
01:35:40 [isabelle-nightly-benchmark] $ hg showconfig paths.default
01:35:40 [isabelle-nightly-benchmark] $ hg pull --rev default
01:35:40 pulling from http://isabelle.in.tum.de/repos/isabelle/
01:35:40 real URL is https://isabelle.in.tum.de/repos/isabelle/
01:35:40 no changes found
01:35:40 [isabelle-nightly-benchmark] $ hg update --clean --rev default
01:35:42 77 files updated, 0 files merged, 0 files removed, 0 files unresolved
01:35:42 [isabelle-nightly-benchmark] $ hg --config extensions.purge= clean --all
01:35:42 [isabelle-nightly-benchmark] $ hg log --rev . --template {node}
01:35:43 [isabelle-nightly-benchmark] $ hg log --rev . --template {rev}
01:35:43 [isabelle-nightly-benchmark] $ hg log --rev 67d87d224e0004daeac3d050d00376f270c2742a --template exists\n
01:35:43 exists
01:35:43 [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(67d87d224e0004daeac3d050d00376f270c2742a)" --encoding UTF-8 --encodingmode replace
01:35:44 No emails were triggered.
01:35:44 [isabelle-nightly-benchmark] $ /bin/sh -xe /tmp/jenkins2928898308958374761.sh
01:35:44 + Admin/jenkins/run_build benchmark
01:35:44 + set -e
01:35:44 + PROFILE=benchmark
01:35:44 + shift
01:35:44 + bin/isabelle components -a
01:35:46 + bin/isabelle jedit -bf
01:35:55 ### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-nightly-benchmark/lib/classes/isabelle.jar) ...
01:38:09 ### Building graph browser (/media/data/jenkins/workspace/isabelle-nightly-benchmark/lib/classes/isabelle_graphbrowser.jar) ...
01:38:21 Note: Some input files use unchecked or unsafe operations.
01:38:21 Note: Recompile with -Xlint:unchecked for details.
01:38:21 ### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-nightly-benchmark/lib/classes/isabelle_admin.jar) ...
01:38:21 + bin/isabelle ocaml_setup
01:38:24 # Run eval $(opam env) to update the current shell environment
01:38:25 [NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
01:38:25        opam update
01:38:25 
01:38:27 [NOTE] Package zarith is already installed (current version is 1.12).
01:38:27 + bin/isabelle ghc_setup
01:38:32 stack will use a sandboxed GHC it installed
01:38:32 For more information on paths, see 'stack path' and 'stack exec env'
01:38:32 To use this GHC and packages outside of a project, consider using:
01:38:32 stack ghc, stack ghci, stack runghc, or stack exec
01:38:34 The Glorious Glasgow Haskell Compilation System, version 8.10.7
01:38:36 + bin/isabelle ci_build_benchmark
01:39:19 
01:39:19 === CONFIGURATION ===
01:39:19 
01:39:19 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
01:39:19 ISABELLE_BUILD_OPTIONS=""
01:39:19 
01:39:19 ML_PLATFORM="x86_64_32-linux"
01:39:19 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8.2/x86_64_32-linux"
01:39:19 ML_SYSTEM="polyml-5.8.2"
01:39:19 ML_OPTIONS="-H 4000 --maxheap 8G"
01:39:23 jobs = 1, threads = 6, numa = true
01:39:23 
01:39:23 === BUILD ===
01:39:23 
01:39:23 Build started at Wed, 20 Oct 2021 01:39:19 +0200
01:39:23 Isabelle id 375e8e1a2139
01:39:23 
01:39:23 === LOG ===
01:39:23 
01:39:27 Session Pure/Pure
01:39:31 Session FOL/FOL
01:39:31 Session Tools/Tools
01:39:31 Session HOL/HOL (main)
01:39:41 Session HOL/HOL-Cardinals (timing)
01:39:41 Session HOL/HOL-Hoare_Parallel (timing)
01:39:41 Session HOL/HOL-Library (main timing)
01:39:45 Session HOL/HOL-Auth (timing)
01:39:45 Session HOL/HOL-UNITY (timing)
01:39:46 Session HOL/HOL-Bali (timing)
01:39:47 Session HOL/HOL-Combinatorics (main timing)
01:39:48 Session HOL/HOL-Computational_Algebra (main timing)
01:39:49 Session HOL/HOL-Algebra (main timing)
01:39:50 Session HOL/HOL-Decision_Procs (timing)
01:39:53 Session HOL/HOL-Quotient_Examples (timing)
01:39:53 Session HOL/HOL-Analysis (main timing)
01:39:58 Session HOL/HOL-Complex_Analysis (main timing)
01:39:58 Session HOL/HOL-Eisbach
01:39:59 Session HOL/HOL-Homology (timing)
01:39:59 Session HOL/HOL-Probability (main timing)
01:40:00 Session HOL/HOL-Probability-ex (timing)
01:40:00 Session HOL/HOL-Nonstandard_Analysis (timing)
01:40:01 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
01:40:01 Session HOL/HOL-Number_Theory (main timing)
01:40:02 Session HOL/HOL-Data_Structures (timing)
01:40:03 Session HOL/HOL-ex (timing)
01:40:04 Session HOL/HOL-Corec_Examples (timing)
01:40:04 Session HOL/HOL-Datatype_Benchmark
01:40:04 Session HOL/HOL-Datatype_Examples (timing)
01:40:04 Session HOL/HOL-IMP (timing)
01:40:05 Session HOL/HOL-Imperative_HOL (timing)
01:40:06 Session HOL/HOL-Metis_Examples (timing)
01:40:06 Session HOL/HOL-Proofs (timing)
01:40:09 Session HOL/HOL-Proofs-Extraction (timing)
01:40:10 Session HOL/HOL-Proofs-Lambda (timing)
01:40:10 Session HOL/HOL-Quickcheck_Benchmark
01:40:10 Session HOL/HOL-MicroJava (timing)
01:40:10 Session HOL/HOL-Nominal
01:40:11 Session HOL/HOL-Nominal-Examples (timing)
01:40:11 Session HOL/HOL-Predicate_Compile_Examples (timing)
01:40:11 Session HOL/HOL-Quickcheck_Examples (timing)
01:40:13 Session HOL/HOL-Record_Benchmark
01:40:13 Session HOL/HOL-SET_Protocol (timing)
01:40:13 Session HOL/HOL-SMT_Examples (timing)
01:40:14 Session HOL/HOLCF (main timing)
01:40:14 Session HOL/IOA (timing)
01:40:14 Session ZF/ZF (main timing)
01:40:15 Session ZF/ZF-Induct
01:40:15 Session ZF/ZF-UNITY (timing)
01:40:15 Building Pure ...
01:41:10 Pure: theory Pure
01:41:16 Pure: theory ML_Bootstrap
01:41:17 Pure: theory Pure.Sessions
01:41:24 Timing Pure (1 threads, 3.097s elapsed time, 5.729s cpu time, 0.000s GC time, factor 1.85)
01:41:24 Finished Pure (0:01:04 elapsed time, 0:00:59 cpu time, factor 0.92)
01:41:24 Building HOL ...
01:41:27 HOL: theory Tools.Code_Generator
01:41:37 HOL: theory HOL.HOL
01:42:11 HOL: theory HOL.Argo
01:42:11 HOL: theory HOL.Ctr_Sugar
01:42:11 HOL: theory HOL.Orderings
01:42:32 HOL: theory HOL.SAT
01:42:40 HOL: theory HOL.Groups
01:42:59 HOL: theory HOL.Lattices
01:43:08 HOL: theory HOL.Boolean_Algebras
01:43:14 HOL: theory HOL.Set
01:43:35 HOL: theory HOL.Fun
01:43:35 HOL: theory HOL.Typedef
01:43:49 HOL: theory HOL.Complete_Lattices
01:43:49 HOL: theory HOL.Rings
01:44:28 HOL: theory HOL.Inductive
01:44:44 HOL: theory HOL.Product_Type
01:44:44 HOL: theory HOL.Sum_Type
01:45:04 HOL: theory HOL.Complete_Partial_Order
01:45:18 HOL: theory HOL.Nat
01:45:50 HOL: theory HOL.Fields
01:45:50 HOL: theory HOL.Meson
01:45:56 HOL: theory HOL.ATP
01:46:14 HOL: theory HOL.Metis
01:46:27 HOL: theory HOL.Finite_Set
01:46:53 HOL: theory HOL.Relation
01:47:18 HOL: theory HOL.Transitive_Closure
01:47:34 HOL: theory HOL.Wellfounded
01:47:45 HOL: theory HOL.Fun_Def_Base
01:47:45 HOL: theory HOL.Hilbert_Choice
01:47:45 HOL: theory HOL.Wfrec
01:47:48 HOL: theory HOL.Order_Relation
01:47:59 HOL: theory HOL.BNF_Wellorder_Relation
01:48:18 HOL: theory HOL.BNF_Wellorder_Embedding
01:48:18 HOL: theory HOL.Zorn
01:48:28 HOL: theory HOL.BNF_Wellorder_Constructions
01:48:48 HOL: theory HOL.BNF_Cardinal_Order_Relation
01:49:04 HOL: theory HOL.BNF_Cardinal_Arithmetic
01:49:08 HOL: theory HOL.BNF_Def
01:49:52 HOL: theory HOL.BNF_Composition
01:49:52 HOL: theory HOL.Basic_BNFs
01:50:03 HOL: theory HOL.BNF_Fixpoint_Base
01:50:16 HOL: theory HOL.BNF_Least_Fixpoint
01:50:26 HOL: theory HOL.Basic_BNF_LFPs
01:50:29 HOL: theory HOL.Transfer
01:50:38 HOL: theory HOL.Num
01:50:55 HOL: theory HOL.Power
01:51:08 HOL: theory HOL.Groups_Big
01:51:28 HOL: theory HOL.Equiv_Relations
01:51:36 HOL: theory HOL.Lifting
01:51:46 HOL: theory HOL.Lifting_Set
01:51:46 HOL: theory HOL.Quotient
01:51:46 HOL: theory HOL.Option
01:51:57 HOL: theory HOL.Lattices_Big
01:51:57 HOL: theory HOL.Extraction
01:51:57 HOL: theory HOL.Partial_Function
01:52:06 HOL: theory HOL.Fun_Def
01:52:35 HOL: theory HOL.Int
01:53:07 HOL: theory HOL.Euclidean_Division
01:53:36 HOL: theory HOL.Parity
01:53:45 HOL: theory HOL.Divides
01:54:01 HOL: theory HOL.Numeral_Simprocs
01:54:01 HOL: theory HOL.Set_Interval
01:54:09 HOL: theory HOL.Semiring_Normalization
01:54:09 HOL: theory HOL.SMT
01:54:39 HOL: theory HOL.Groebner_Basis
01:55:06 HOL: theory HOL.Conditionally_Complete_Lattices
01:55:06 HOL: theory HOL.Filter
01:55:06 HOL: theory HOL.Presburger
01:55:57 HOL: theory HOL.Sledgehammer
01:56:13 HOL: theory HOL.List
01:58:08 HOL: theory HOL.Groups_List
01:58:08 HOL: theory HOL.Map
01:58:27 HOL: theory HOL.Bit_Operations
01:58:27 HOL: theory HOL.Factorial
01:58:27 HOL: theory HOL.Enum
01:58:46 HOL: theory HOL.Binomial
01:59:56 HOL: theory HOL.Code_Numeral
02:00:06 HOL: theory HOL.GCD
02:00:06 HOL: theory HOL.String
02:00:06 HOL: theory HOL.Random
02:00:17 HOL: theory HOL.BNF_Greatest_Fixpoint
02:00:17 HOL: theory HOL.Predicate
02:00:17 HOL: theory HOL.Typerep
02:00:35 HOL: theory HOL.Lazy_Sequence
02:00:41 HOL: theory HOL.Limited_Sequence
02:00:44 HOL: theory HOL.Code_Evaluation
02:00:48 HOL: theory HOL.Quickcheck_Random
02:00:58 HOL: theory HOL.Quickcheck_Exhaustive
02:00:58 HOL: theory HOL.Random_Pred
02:00:58 HOL: theory HOL.Quickcheck_Narrowing
02:01:01 HOL: theory HOL.Random_Sequence
02:01:30 HOL: theory HOL.Record
02:01:30 HOL: theory HOL.Predicate_Compile
02:01:56 HOL: theory HOL.Mirabelle
02:02:15 HOL: theory HOL.Nitpick
02:02:39 HOL: theory HOL.Nunchaku
02:02:42 HOL: theory Main
02:02:43 HOL: theory HOL.Archimedean_Field
02:02:43 HOL: theory HOL.Hull
02:02:43 HOL: theory HOL.Topological_Spaces
02:02:44 HOL: theory HOL.Modules
02:02:59 HOL: theory HOL.Vector_Spaces
02:04:14 HOL: theory HOL.Rat
02:04:36 HOL: theory HOL.Real
02:05:15 HOL: theory HOL.Real_Vector_Spaces
02:05:51 HOL: theory HOL.Inequalities
02:05:51 HOL: theory HOL.Limits
02:06:33 HOL: theory HOL.Deriv
02:06:33 HOL: theory HOL.Series
02:07:14 HOL: theory HOL.NthRoot
02:07:25 HOL: theory HOL.Transcendental
02:08:54 HOL: theory HOL.Complex
02:09:04 HOL: theory HOL.MacLaurin
02:09:08 HOL: theory Complex_Main
02:12:37 Timing HOL (6 threads, 662.360s elapsed time, 2549.218s cpu time, 120.042s GC time, factor 3.85)
02:12:37 Finished HOL (0:30:46 elapsed time, 0:53:45 cpu time, factor 1.75)
02:12:37 Building HOL-Analysis ...
02:12:41 HOL-Analysis: theory HOL-Library.Cancellation
02:12:41 HOL-Analysis: theory HOL-Combinatorics.Transposition
02:12:41 HOL-Analysis: theory HOL-Library.Disjoint_Sets
02:12:41 HOL-Analysis: theory HOL-Library.FuncSet
02:12:41 HOL-Analysis: theory HOL-Library.Infinite_Set
02:12:41 HOL-Analysis: theory HOL-Library.Nat_Bijection
02:12:48 HOL-Analysis: theory HOL-Library.Old_Datatype
02:12:52 HOL-Analysis: theory HOL-Library.Phantom_Type
02:12:56 HOL-Analysis: theory HOL-Library.Product_Plus
02:12:57 HOL-Analysis: theory HOL-Library.Set_Algebras
02:12:58 HOL-Analysis: theory HOL-Library.Multiset
02:13:00 HOL-Analysis: theory HOL-Library.Product_Order
02:13:02 HOL-Analysis: theory HOL-Analysis.Metric_Arith
02:13:06 HOL-Analysis: theory HOL-Analysis.Inner_Product
02:13:07 HOL-Analysis: theory HOL-Library.Countable
02:13:09 HOL-Analysis: theory HOL-Analysis.L2_Norm
02:13:10 HOL-Analysis: theory HOL-Library.Cardinality
02:13:11 HOL-Analysis: theory HOL-Analysis.Operator_Norm
02:13:14 HOL-Analysis: theory HOL-Analysis.Poly_Roots
02:13:15 HOL-Analysis: theory HOL-Analysis.Product_Vector
02:13:16 HOL-Analysis: theory HOL-Library.Complex_Order
02:13:17 HOL-Analysis: theory HOL-Library.Discrete
02:13:22 HOL-Analysis: theory HOL-Library.Indicator_Function
02:13:24 HOL-Analysis: theory HOL-Library.Numeral_Type
02:13:29 HOL-Analysis: theory HOL-Library.Liminf_Limsup
02:13:30 HOL-Analysis: theory HOL-Library.Countable_Set
02:13:32 HOL-Analysis: theory HOL-Library.Nonpos_Ints
02:13:39 HOL-Analysis: theory HOL-Library.Periodic_Fun
02:13:45 HOL-Analysis: theory HOL-Analysis.Euclidean_Space
02:13:49 HOL-Analysis: theory HOL-Library.Sum_of_Squares
02:13:49 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices
02:13:49 HOL-Analysis: theory HOL-Library.Set_Idioms
02:13:52 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable
02:13:56 HOL-Analysis: theory HOL-Analysis.Abstract_Topology
02:13:57 HOL-Analysis: theory HOL-Analysis.Elementary_Topology
02:14:15 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
02:14:31 HOL-Analysis: theory HOL-Analysis.Linear_Algebra
02:14:45 HOL-Analysis: theory HOL-Library.Order_Continuity
02:14:53 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring
02:15:02 HOL-Analysis: theory HOL-Combinatorics.Permutations
02:15:06 HOL-Analysis: theory HOL-Library.Extended_Nat
02:15:14 HOL-Analysis: theory HOL-Analysis.Affine
02:15:20 HOL-Analysis: theory HOL-Analysis.Cartesian_Space
02:15:22 HOL-Analysis: theory HOL-Analysis.Abstract_Limits
02:15:36 HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2
02:15:38 HOL-Analysis: theory HOL-Analysis.Convex
02:15:39 HOL-Analysis: theory HOL-Library.Extended_Real
02:15:40 HOL-Analysis: theory HOL-Analysis.Norm_Arith
02:16:13 HOL-Analysis: theory HOL-Analysis.Connected
02:16:13 HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces
02:16:17 HOL-Analysis: theory HOL-Analysis.Determinants
02:16:23 HOL-Analysis: theory HOL-Analysis.Function_Topology
02:16:49 HOL-Analysis: theory HOL-Analysis.Product_Topology
02:17:00 HOL-Analysis: theory HOL-Analysis.T1_Spaces
02:17:11 HOL-Analysis: theory HOL-Analysis.Lindelof_Spaces
02:17:22 HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces
02:17:22 HOL-Analysis: theory HOL-Analysis.Function_Metric
02:17:24 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real
02:17:48 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space
02:18:04 HOL-Analysis: theory HOL-Analysis.Infinite_Sum
02:18:04 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra
02:18:08 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm
02:18:28 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space
02:18:28 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits
02:18:28 HOL-Analysis: theory HOL-Analysis.Line_Segment
02:18:30 HOL-Analysis: theory HOL-Analysis.Tagged_Division
02:19:14 HOL-Analysis: theory HOL-Analysis.Summation_Tests
02:19:14 HOL-Analysis: theory HOL-Analysis.Measurable
02:19:16 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
02:19:18 HOL-Analysis: theory HOL-Analysis.Starlike
02:19:31 HOL-Analysis: theory HOL-Analysis.Measure_Space
02:19:39 HOL-Analysis: theory HOL-Analysis.Uniform_Limit
02:20:01 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function
02:20:02 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function
02:20:14 HOL-Analysis: theory HOL-Analysis.Continuous_Extension
02:20:15 HOL-Analysis: theory HOL-Analysis.Path_Connected
02:20:36 HOL-Analysis: theory HOL-Analysis.Caratheodory
02:20:51 HOL-Analysis: theory HOL-Analysis.Derivative
02:21:06 HOL-Analysis: theory HOL-Analysis.Homotopy
02:21:06 HOL-Analysis: theory HOL-Analysis.Locally
02:21:37 HOL-Analysis: theory HOL-Analysis.Borel_Space
02:21:38 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
02:21:42 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics
02:21:46 HOL-Analysis: theory HOL-Analysis.Cross3
02:21:49 HOL-Analysis: theory HOL-Analysis.Lipschitz
02:22:03 HOL-Analysis: theory HOL-Analysis.Homeomorphism
02:22:10 HOL-Analysis: theory HOL-Analysis.Abstract_Euclidean_Space
02:22:14 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
02:22:20 HOL-Analysis: theory HOL-Computational_Algebra.Primes
02:22:23 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series
02:22:28 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint
02:22:36 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
02:22:40 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
02:23:13 HOL-Analysis: theory HOL-Analysis.Regularity
02:23:17 HOL-Analysis: theory HOL-Analysis.Multivariate_Analysis
02:23:36 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem
02:23:42 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
02:23:43 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers
02:23:46 HOL-Analysis: theory HOL-Analysis.Infinite_Products
02:23:53 HOL-Analysis: theory HOL-Analysis.Retracts
02:23:57 HOL-Analysis: theory HOL-Analysis.Polytope
02:24:02 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
02:24:06 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
02:24:33 HOL-Analysis: theory HOL-Analysis.Embed_Measure
02:24:34 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
02:24:49 HOL-Analysis: theory HOL-Analysis.Smooth_Paths
02:25:18 HOL-Analysis: theory HOL-Analysis.Bochner_Integration
02:25:22 HOL-Analysis: theory HOL-Analysis.FPS_Convergence
02:25:53 HOL-Analysis: theory HOL-Analysis.Complete_Measure
02:25:53 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym
02:26:03 HOL-Analysis: theory HOL-Analysis.Set_Integral
02:26:09 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure
02:26:18 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum
02:26:46 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration
02:27:46 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
02:27:46 HOL-Analysis: theory HOL-Analysis.Integral_Test
02:28:22 HOL-Analysis: theory HOL-Analysis.Further_Topology
02:28:22 HOL-Analysis: theory HOL-Analysis.Gamma_Function
02:28:22 HOL-Analysis: theory HOL-Analysis.Improper_Integral
02:28:22 HOL-Analysis: theory HOL-Analysis.Interval_Integral
02:28:22 HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem
02:28:35 HOL-Analysis: theory HOL-Analysis.Equivalence_Measurable_On_Borel
02:28:41 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution
02:28:57 HOL-Analysis: theory HOL-Analysis.Change_Of_Vars
02:29:41 HOL-Analysis: theory HOL-Analysis.Simplex_Content
02:30:00 HOL-Analysis: theory HOL-Analysis.Jordan_Curve
02:30:14 HOL-Analysis: theory HOL-Analysis.Ball_Volume
02:30:22 HOL-Analysis: theory HOL-Analysis.Analysis
03:03:39 Timing HOL-Analysis (6 threads, 833.291s elapsed time, 5200.904s cpu time, 331.776s GC time, factor 6.24)
03:03:39 Finished HOL-Analysis (0:50:35 elapsed time, 1:46:02 cpu time, factor 2.10)
03:03:39 Building HOL-Auth ...
03:03:42 HOL-Auth: theory HOL-Library.Case_Converter
03:03:42 HOL-Auth: theory HOL-Auth.Message
03:03:42 HOL-Auth: theory HOL-Library.Nat_Bijection
03:03:45 HOL-Auth: theory HOL-Library.Simps_Case_Conv
03:03:59 HOL-Auth: theory HOL-Auth.All_Symmetric
03:03:59 HOL-Auth: theory HOL-Auth.Event
03:03:59 HOL-Auth: theory HOL-Auth.EventSC
03:04:03 HOL-Auth: theory HOL-Auth.Extensions
03:04:03 HOL-Auth: theory HOL-Auth.Public
03:04:03 HOL-Auth: theory HOL-Auth.Shared
03:04:14 HOL-Auth: theory HOL-Auth.CertifiedEmail
03:04:15 HOL-Auth: theory HOL-Auth.KerberosIV
03:04:15 HOL-Auth: theory HOL-Auth.Analz
03:04:18 HOL-Auth: theory HOL-Auth.List_Msg
03:04:20 HOL-Auth: theory HOL-Auth.KerberosIV_Gets
03:04:21 HOL-Auth: theory HOL-Auth.KerberosV
03:04:22 HOL-Auth: theory HOL-Auth.Guard
03:04:23 HOL-Auth: theory HOL-Auth.GuardK
03:04:30 HOL-Auth: theory HOL-Auth.Guard_Public
03:04:31 HOL-Auth: theory HOL-Auth.Kerberos_BAN
03:04:38 HOL-Auth: theory HOL-Auth.Guard_NS_Public
03:04:44 HOL-Auth: theory HOL-Auth.Proto
03:04:47 HOL-Auth: theory HOL-Auth.Kerberos_BAN_Gets
03:04:48 HOL-Auth: theory HOL-Auth.NS_Public
03:04:49 HOL-Auth: theory HOL-Auth.NS_Public_Bad
03:04:50 HOL-Auth: theory HOL-Auth.NS_Shared
03:04:52 HOL-Auth: theory HOL-Auth.OtwayRees
03:04:52 HOL-Auth: theory HOL-Auth.P2
03:04:57 HOL-Auth: theory HOL-Auth.OtwayReesBella
03:04:58 HOL-Auth: theory HOL-Auth.OtwayRees_AN
03:05:00 HOL-Auth: theory HOL-Auth.OtwayRees_Bad
03:05:02 HOL-Auth: theory HOL-Auth.P1
03:05:02 HOL-Auth: theory HOL-Auth.Recur
03:05:04 HOL-Auth: theory HOL-Auth.WooLam
03:05:06 HOL-Auth: theory HOL-Auth.Yahalom
03:05:07 HOL-Auth: theory HOL-Auth.Yahalom2
03:05:08 HOL-Auth: theory HOL-Auth.Yahalom_Bad
03:05:08 HOL-Auth: theory HOL-Auth.ZhouGollmann
03:05:11 HOL-Auth: theory HOL-Auth.Guard_Shared
03:05:13 HOL-Auth: theory HOL-Auth.Smartcard
03:05:13 HOL-Auth: theory HOL-Auth.TLS
03:05:17 HOL-Auth: theory HOL-Auth.Auth_Shared
03:05:18 HOL-Auth: theory HOL-Auth.Guard_OtwayRees
03:05:20 HOL-Auth: theory HOL-Auth.Guard_Yahalom
03:05:23 HOL-Auth: theory HOL-Auth.ShoupRubin
03:05:24 HOL-Auth: theory HOL-Auth.Auth_Guard_Shared
03:05:25 HOL-Auth: theory HOL-Auth.ShoupRubinBella
03:05:30 HOL-Auth: theory HOL-Auth.Auth_Public
03:05:43 HOL-Auth: theory HOL-Auth.Auth_Smartcard
03:05:51 HOL-Auth: theory HOL-Auth.Auth_Guard_Public
03:08:06 Timing HOL-Auth (6 threads, 112.012s elapsed time, 640.613s cpu time, 12.991s GC time, factor 5.72)
03:08:06 Finished HOL-Auth (0:04:24 elapsed time, 0:12:56 cpu time, factor 2.94)
03:08:06 Running HOL-Bali ...
03:08:09 HOL-Bali: theory HOL-Bali.Basis
03:08:14 HOL-Bali: theory HOL-Bali.Name
03:08:14 HOL-Bali: theory HOL-Bali.Table
03:08:21 HOL-Bali: theory HOL-Bali.Type
03:08:23 HOL-Bali: theory HOL-Bali.Value
03:08:25 HOL-Bali: theory HOL-Bali.Term
03:09:04 HOL-Bali: theory HOL-Bali.Decl
03:09:14 HOL-Bali: theory HOL-Bali.TypeRel
03:09:21 HOL-Bali: theory HOL-Bali.DeclConcepts
03:09:38 HOL-Bali: theory HOL-Bali.State
03:09:38 HOL-Bali: theory HOL-Bali.WellType
03:09:51 HOL-Bali: theory HOL-Bali.Conform
03:09:51 HOL-Bali: theory HOL-Bali.Eval
03:10:01 HOL-Bali: theory HOL-Bali.DefiniteAssignment
03:10:17 HOL-Bali: theory HOL-Bali.WellForm
03:10:34 HOL-Bali: theory HOL-Bali.DefiniteAssignmentCorrect
03:10:34 HOL-Bali: theory HOL-Bali.Example
03:10:55 HOL-Bali: theory HOL-Bali.TypeSafe
03:11:24 HOL-Bali: theory HOL-Bali.Evaln
03:11:40 HOL-Bali: theory HOL-Bali.AxSem
03:11:40 HOL-Bali: theory HOL-Bali.Trans
03:12:16 HOL-Bali: theory HOL-Bali.AxCompl
03:12:23 HOL-Bali: theory HOL-Bali.AxSound
03:12:24 HOL-Bali: theory HOL-Bali.AxExample
03:14:26 Timing HOL-Bali (6 threads, 113.416s elapsed time, 592.392s cpu time, 14.209s GC time, factor 5.22)
03:14:26 Finished HOL-Bali (0:06:16 elapsed time, 0:11:40 cpu time, factor 1.86)
03:14:26 Running HOL-Cardinals ...
03:14:29 HOL-Cardinals: theory HOL-Cardinals.Fun_More
03:14:29 HOL-Cardinals: theory HOL-Cardinals.Order_Relation_More
03:14:29 HOL-Cardinals: theory HOL-Cardinals.Order_Union
03:14:34 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Extension
03:14:39 HOL-Cardinals: theory HOL-Cardinals.Wellfounded_More
03:14:40 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Relation
03:14:45 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Embedding
03:14:49 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Constructions
03:15:10 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Order_Relation
03:15:10 HOL-Cardinals: theory HOL-Cardinals.Ordinal_Arithmetic
03:15:34 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Arithmetic
03:15:53 HOL-Cardinals: theory HOL-Cardinals.Cardinals
03:15:55 HOL-Cardinals: theory HOL-Cardinals.Bounded_Set
03:16:42 Timing HOL-Cardinals (6 threads, 17.565s elapsed time, 117.205s cpu time, 2.055s GC time, factor 6.67)
03:16:42 Finished HOL-Cardinals (0:02:13 elapsed time, 0:02:43 cpu time, factor 1.22)
03:16:42 Running HOL-Combinatorics ...
03:16:44 HOL-Combinatorics: theory HOL-Combinatorics.Stirling
03:16:44 HOL-Combinatorics: theory HOL-Library.Cancellation
03:16:45 HOL-Combinatorics: theory HOL-Combinatorics.Transposition
03:16:45 HOL-Combinatorics: theory HOL-Library.Disjoint_Sets
03:16:45 HOL-Combinatorics: theory HOL-Library.FuncSet
03:16:49 HOL-Combinatorics: theory HOL-Combinatorics.Perm
03:16:57 HOL-Combinatorics: theory HOL-Library.Multiset
03:18:02 HOL-Combinatorics: theory HOL-Combinatorics.Permutations
03:18:16 HOL-Combinatorics: theory HOL-Combinatorics.List_Permutation
03:18:17 HOL-Combinatorics: theory HOL-Combinatorics.Cycles
03:18:17 HOL-Combinatorics: theory HOL-Combinatorics.Orbits
03:18:17 HOL-Combinatorics: theory HOL-Combinatorics.Multiset_Permutations
03:18:36 HOL-Combinatorics: theory HOL-Combinatorics.Combinatorics
03:19:05 Timing HOL-Combinatorics (6 threads, 28.918s elapsed time, 169.162s cpu time, 3.172s GC time, factor 5.85)
03:19:05 Finished HOL-Combinatorics (0:02:21 elapsed time, 0:03:34 cpu time, factor 1.52)
03:19:05 Running HOL-Complex_Analysis ...
03:19:09 HOL-Complex_Analysis: theory HOL-Library.Landau_Symbols
03:19:09 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Contour_Integration
03:19:26 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
03:19:36 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Winding_Numbers
03:19:54 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
03:20:12 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Conformal_Mappings
03:20:24 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Complex_Singularities
03:20:24 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Great_Picard
03:20:36 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Riemann_Mapping
03:20:45 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Complex_Residues
03:20:52 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Residue_Theorem
03:21:00 HOL-Complex_Analysis: theory HOL-Complex_Analysis.Complex_Analysis
03:24:45 Timing HOL-Complex_Analysis (6 threads, 108.019s elapsed time, 677.537s cpu time, 6.338s GC time, factor 6.27)
03:24:45 Finished HOL-Complex_Analysis (0:05:36 elapsed time, 0:12:45 cpu time, factor 2.27)
03:24:45 Running HOL-Data_Structures ...
03:24:48 HOL-Data_Structures: theory HOL-Data_Structures.Less_False
03:24:49 HOL-Data_Structures: theory HOL-Data_Structures.Cmp
03:24:49 HOL-Data_Structures: theory HOL-Data_Structures.Reverse
03:24:49 HOL-Data_Structures: theory HOL-Data_Structures.Array_Specs
03:24:49 HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less
03:24:49 HOL-Data_Structures: theory HOL-Data_Structures.Queue_Spec
03:24:49 HOL-Data_Structures: theory HOL-Data_Structures.Time_Funs
03:24:50 HOL-Data_Structures: theory HOL-Data_Structures.Tree23
03:24:50 HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del
03:24:50 HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del
03:24:53 HOL-Data_Structures: theory HOL-Data_Structures.Queue_2Lists
03:24:53 HOL-Data_Structures: theory HOL-Data_Structures.Tree234
03:24:53 HOL-Data_Structures: theory HOL-Data_Structures.Set_Specs
03:24:55 HOL-Data_Structures: theory HOL-Library.Cancellation
03:24:56 HOL-Data_Structures: theory HOL-Data_Structures.Trie_Fun
03:24:56 HOL-Data_Structures: theory HOL-Data_Structures.Map_Specs
03:24:57 HOL-Data_Structures: theory HOL-Data_Structures.Tries_Binary
03:25:00 HOL-Data_Structures: theory HOL-Library.Multiset
03:25:03 HOL-Data_Structures: theory HOL-Library.Pattern_Aliases
03:25:04 HOL-Data_Structures: theory HOL-Library.Tree
03:25:06 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set
03:25:06 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_of_List
03:25:17 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set
03:25:19 HOL-Data_Structures: theory HOL-Number_Theory.Fib
03:25:26 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set
03:25:33 HOL-Data_Structures: theory HOL-Data_Structures.Tree2
03:25:33 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set
03:25:37 HOL-Data_Structures: theory HOL-Data_Structures.Isin2
03:25:39 HOL-Data_Structures: theory HOL-Data_Structures.AA_Set
03:25:41 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Bal2_Set
03:25:53 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Bal_Set
03:25:58 HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue_Specs
03:25:58 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set_Code
03:26:00 HOL-Data_Structures: theory HOL-Data_Structures.Height_Balanced_Tree
03:26:01 HOL-Data_Structures: theory HOL-Data_Structures.Interval_Tree
03:26:03 HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join
03:26:06 HOL-Data_Structures: theory HOL-Data_Structures.Lookup2
03:26:09 HOL-Data_Structures: theory HOL-Data_Structures.RBT
03:26:10 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map
03:26:10 HOL-Data_Structures: theory HOL-Data_Structures.AA_Map
03:26:13 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map
03:26:13 HOL-Data_Structures: theory HOL-Library.Tree_Multiset
03:26:13 HOL-Data_Structures: theory HOL-Data_Structures.Binomial_Heap
03:26:14 HOL-Data_Structures: theory HOL-Data_Structures.Heaps
03:26:15 HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap
03:26:18 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set
03:26:23 HOL-Data_Structures: theory HOL-Data_Structures.Sorting
03:26:23 HOL-Data_Structures: theory HOL-Library.Tree_Real
03:26:24 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set
03:26:25 HOL-Data_Structures: theory HOL-Data_Structures.Balance
03:26:27 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map
03:26:30 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set2
03:26:31 HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join_RBT
03:26:33 HOL-Data_Structures: theory HOL-Data_Structures.Braun_Tree
03:26:35 HOL-Data_Structures: theory HOL-Data_Structures.Array_Braun
03:26:35 HOL-Data_Structures: theory HOL-Data_Structures.Trie_Map
03:26:39 HOL-Data_Structures: theory HOL-Data_Structures.Selection
03:26:43 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map
03:26:59 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map
03:27:44 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Map
03:49:52 Timing HOL-Data_Structures (6 threads, 1492.582s elapsed time, 7665.417s cpu time, 244.931s GC time, factor 5.14)
03:49:52 Finished HOL-Data_Structures (0:25:01 elapsed time, 2:07:54 cpu time, factor 5.11)
03:49:52 Running HOL-Hoare_Parallel ...
03:49:54 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Graph
03:49:54 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Com
03:49:54 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Quote_Antiquote
03:49:54 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Com
03:50:01 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Tran
03:50:06 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tran
03:50:13 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Hoare
03:50:20 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Hoare
03:50:23 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Syntax
03:50:25 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Examples
03:50:27 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tactics
03:50:29 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Syntax
03:50:31 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Gar_Coll
03:50:31 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Mul_Gar_Coll
03:50:36 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Examples
03:50:47 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Hoare_Parallel
03:52:11 Timing HOL-Hoare_Parallel (6 threads, 134.019s elapsed time, 801.054s cpu time, 9.710s GC time, factor 5.98)
03:52:11 Finished HOL-Hoare_Parallel (0:02:18 elapsed time, 0:13:25 cpu time, factor 5.82)
03:52:11 Running HOL-Homology ...
03:52:15 HOL-Homology: theory HOL-Cardinals.Fun_More
03:52:15 HOL-Homology: theory HOL-Cardinals.Order_Union
03:52:15 HOL-Homology: theory HOL-Cardinals.Order_Relation_More
03:52:15 HOL-Homology: theory HOL-Library.Fun_Lexorder
03:52:15 HOL-Homology: theory HOL-Library.Equipollence
03:52:15 HOL-Homology: theory HOL-Algebra.Congruence
03:52:17 HOL-Homology: theory HOL-Library.Groups_Big_Fun
03:52:19 HOL-Homology: theory HOL-Library.More_List
03:52:28 HOL-Homology: theory HOL-Cardinals.Wellfounded_More
03:52:29 HOL-Homology: theory HOL-Cardinals.Wellorder_Relation
03:52:34 HOL-Homology: theory HOL-Library.Poly_Mapping
03:52:36 HOL-Homology: theory HOL-Cardinals.Wellorder_Embedding
03:52:39 HOL-Homology: theory HOL-Cardinals.Wellorder_Constructions
03:52:42 HOL-Homology: theory HOL-Algebra.Order
03:53:00 HOL-Homology: theory HOL-Cardinals.Cardinal_Order_Relation
03:53:11 HOL-Homology: theory HOL-Algebra.Lattice
03:53:27 HOL-Homology: theory HOL-Cardinals.Cardinal_Arithmetic
03:53:32 HOL-Homology: theory HOL-Algebra.Complete_Lattice
03:53:45 HOL-Homology: theory HOL-Algebra.Group
03:54:06 HOL-Homology: theory HOL-Algebra.Coset
03:54:06 HOL-Homology: theory HOL-Algebra.FiniteProduct
03:54:14 HOL-Homology: theory HOL-Algebra.Ring
03:54:20 HOL-Homology: theory HOL-Algebra.Generated_Groups
03:54:29 HOL-Homology: theory HOL-Algebra.Solvable_Groups
03:54:29 HOL-Homology: theory HOL-Algebra.Elementary_Groups
03:54:40 HOL-Homology: theory HOL-Algebra.Exact_Sequence
03:54:40 HOL-Homology: theory HOL-Algebra.Product_Groups
03:54:47 HOL-Homology: theory HOL-Algebra.Free_Abelian_Groups
03:54:59 HOL-Homology: theory HOL-Algebra.AbelCoset
03:54:59 HOL-Homology: theory HOL-Algebra.Module
03:54:59 HOL-Homology: theory HOL-Homology.Simplices
03:55:31 HOL-Homology: theory HOL-Homology.Homology_Groups
03:55:39 HOL-Homology: theory HOL-Algebra.Ideal
03:56:00 HOL-Homology: theory HOL-Algebra.RingHom
03:56:04 HOL-Homology: theory HOL-Algebra.UnivPoly
03:57:05 HOL-Homology: theory HOL-Algebra.Multiplicative_Group
03:57:22 HOL-Homology: theory HOL-Homology.Brouwer_Degree
03:57:36 HOL-Homology: theory HOL-Homology.Invariance_of_Domain
03:57:54 HOL-Homology: theory HOL-Homology.Homology
04:00:37 Timing HOL-Homology (6 threads, 221.562s elapsed time, 1245.213s cpu time, 40.156s GC time, factor 5.62)
04:00:37 Finished HOL-Homology (0:08:19 elapsed time, 0:22:51 cpu time, factor 2.74)
04:00:37 Running HOL-Imperative_HOL ...
04:00:39 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Sorted_List
04:00:39 HOL-Imperative_HOL: theory HOL-Library.Adhoc_Overloading
04:00:39 HOL-Imperative_HOL: theory HOL-Library.Cancellation
04:00:39 HOL-Imperative_HOL: theory HOL-Library.Code_Abstract_Nat
04:00:39 HOL-Imperative_HOL: theory HOL-Library.LaTeXsugar
04:00:39 HOL-Imperative_HOL: theory HOL-Library.Code_Target_Int
04:00:40 HOL-Imperative_HOL: theory HOL-Library.Code_Target_Nat
04:00:41 HOL-Imperative_HOL: theory HOL-Library.Nat_Bijection
04:00:42 HOL-Imperative_HOL: theory HOL-Library.Monad_Syntax
04:00:43 HOL-Imperative_HOL: theory HOL-Library.Old_Datatype
04:00:43 HOL-Imperative_HOL: theory HOL-Library.RBT_Impl
04:00:45 HOL-Imperative_HOL: theory HOL-Library.Code_Target_Numeral
04:00:49 HOL-Imperative_HOL: theory HOL-Library.Multiset
04:00:54 HOL-Imperative_HOL: theory HOL-Library.Countable
04:01:10 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap
04:01:25 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad
04:01:44 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Array
04:01:52 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Ref
04:01:55 HOL-Imperative_HOL: theory HOL-Imperative_HOL.List_Sublist
04:01:58 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL
04:01:59 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Linked_Lists
04:01:59 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Overview
04:02:00 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Subarray
04:02:04 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort
04:02:04 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse
04:03:13 HOL-Imperative_HOL: theory HOL-Imperative_HOL.SatChecker
04:04:46 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL_ex
04:06:53 Timing HOL-Imperative_HOL (6 threads, 368.238s elapsed time, 845.328s cpu time, 14.905s GC time, factor 2.30)
04:06:53 Finished HOL-Imperative_HOL (0:06:14 elapsed time, 0:14:11 cpu time, factor 2.27)
04:06:53 Building HOL-Library ...
04:06:56 HOL-Library: theory HOL-Library.AList
04:06:56 HOL-Library: theory HOL-Library.Adhoc_Overloading
04:06:56 HOL-Library: theory HOL-Library.BNF_Axiomatization
04:06:56 HOL-Library: theory HOL-Library.BNF_Corec
04:06:56 HOL-Library: theory HOL-Library.Cancellation
04:06:56 HOL-Library: theory HOL-Library.Case_Converter
04:06:58 HOL-Library: theory HOL-Library.Monad_Syntax
04:06:58 HOL-Library: theory HOL-Library.Char_ord
04:06:59 HOL-Library: theory HOL-Library.State_Monad
04:07:00 HOL-Library: theory HOL-Library.Code_Abstract_Nat
04:07:01 HOL-Library: theory HOL-Library.Code_Lazy
04:07:02 HOL-Library: theory HOL-Library.Simps_Case_Conv
04:07:03 HOL-Library: theory HOL-Library.Extended
04:07:05 HOL-Library: theory HOL-Library.Multiset
04:07:10 HOL-Library: theory HOL-Library.Code_Binary_Nat
04:07:14 HOL-Library: theory HOL-Library.Code_Target_Nat
04:07:17 HOL-Library: theory HOL-Library.Code_Prolog
04:07:18 HOL-Library: theory HOL-Library.Code_Target_Int
04:07:20 HOL-Library: theory HOL-Library.DAList
04:07:20 HOL-Library: theory HOL-Library.Code_Target_Numeral
04:07:21 HOL-Library: theory HOL-Library.Code_Test
04:07:25 HOL-Library: theory HOL-Library.Combine_PER
04:07:25 HOL-Library: theory HOL-Library.Comparator
04:07:26 HOL-Library: theory HOL-Library.Complete_Partial_Order2
04:07:32 HOL-Library: theory HOL-Library.Conditional_Parametricity
04:07:32 HOL-Library: theory HOL-Library.Confluence
04:07:35 HOL-Library: theory HOL-Library.Confluent_Quotient
04:07:39 HOL-Library: theory HOL-Library.Dlist
04:07:42 HOL-Library: theory HOL-Library.Datatype_Records
04:07:43 HOL-Library: theory HOL-Library.Debug
04:07:44 HOL-Library: theory HOL-Library.Disjoint_Sets
04:07:53 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
04:07:53 HOL-Library: theory HOL-Library.Fun_Lexorder
04:07:55 HOL-Library: theory HOL-Library.FuncSet
04:07:55 HOL-Library: theory HOL-Library.Function_Algebras
04:08:02 HOL-Library: theory HOL-Library.Function_Division
04:08:04 HOL-Library: theory HOL-Library.Groups_Big_Fun
04:08:05 HOL-Library: theory HOL-Library.IArray
04:08:10 HOL-Library: theory HOL-Library.Equipollence
04:08:12 HOL-Library: theory HOL-Library.Infinite_Set
04:08:18 HOL-Library: theory HOL-Library.LaTeXsugar
04:08:18 HOL-Library: theory HOL-Library.Lattice_Constructions
04:08:20 HOL-Library: theory HOL-Library.ListVector
04:08:22 HOL-Library: theory HOL-Library.Omega_Words_Fun
04:08:26 HOL-Library: theory HOL-Library.Ramsey
04:08:34 HOL-Library: theory HOL-Library.List_Lenlexorder
04:08:38 HOL-Library: theory HOL-Library.List_Lexorder
04:08:42 HOL-Library: theory HOL-Library.Mapping
04:08:43 HOL-Library: theory HOL-Library.More_List
04:08:48 HOL-Library: theory HOL-Library.Nat_Bijection
04:08:49 HOL-Library: theory HOL-Library.Poly_Mapping
04:08:56 HOL-Library: theory HOL-Library.DAList_Multiset
04:08:58 HOL-Library: theory HOL-Library.Multiset_Order
04:09:05 HOL-Library: theory HOL-Library.Stream
04:09:08 HOL-Library: theory HOL-Library.Old_Datatype
04:09:09 HOL-Library: theory HOL-Library.Old_Recdef
04:09:13 HOL-Library: theory HOL-Library.AList_Mapping
04:09:18 HOL-Library: theory HOL-Library.Open_State_Syntax
04:09:20 HOL-Library: theory HOL-Library.Option_ord
04:09:26 HOL-Library: theory HOL-Library.Parallel
04:09:27 HOL-Library: theory HOL-Library.Pattern_Aliases
04:09:31 HOL-Library: theory HOL-Library.Phantom_Type
04:09:31 HOL-Library: theory HOL-Library.Power_By_Squaring
04:09:32 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
04:09:35 HOL-Library: theory HOL-Library.Preorder
04:09:35 HOL-Library: theory HOL-Library.Product_Lexorder
04:09:36 HOL-Library: theory HOL-Library.Product_Plus
04:09:38 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
04:09:38 HOL-Library: theory HOL-Library.Quotient_Syntax
04:09:38 HOL-Library: theory HOL-Library.Quotient_Type
04:09:39 HOL-Library: theory HOL-Library.Quotient_Option
04:09:40 HOL-Library: theory HOL-Library.Product_Order
04:09:40 HOL-Library: theory HOL-Library.Quotient_Product
04:09:42 HOL-Library: theory HOL-Library.Cardinality
04:09:43 HOL-Library: theory HOL-Library.Quotient_Set
04:09:43 HOL-Library: theory HOL-Library.Quotient_Sum
04:09:43 HOL-Library: theory HOL-Library.RBT_Impl
04:09:45 HOL-Library: theory HOL-Library.Realizers
04:09:46 HOL-Library: theory HOL-Library.Quotient_List
04:09:46 HOL-Library: theory HOL-Library.Reflection
04:09:47 HOL-Library: theory HOL-Library.Finite_Lattice
04:09:47 HOL-Library: theory HOL-Library.Refute
04:09:51 HOL-Library: theory HOL-Library.Rewrite
04:09:53 HOL-Library: theory HOL-Library.Set_Algebras
04:09:55 HOL-Library: theory HOL-Library.Signed_Division
04:09:56 HOL-Library: theory HOL-Library.Code_Cardinality
04:09:58 HOL-Library: theory HOL-Library.Numeral_Type
04:09:59 HOL-Library: theory HOL-Library.Sorting_Algorithms
04:10:00 HOL-Library: theory HOL-Library.Sublist
04:10:02 HOL-Library: theory HOL-Library.Transitive_Closure_Table
04:10:09 HOL-Library: theory HOL-Library.Tree
04:10:10 HOL-Library: theory HOL-Library.Uprod
04:10:15 HOL-Library: theory HOL-Library.Type_Length
04:10:17 HOL-Library: theory HOL-Library.While_Combinator
04:10:23 HOL-Library: theory HOL-Library.Saturated
04:10:25 HOL-Library: theory HOL-Library.Word
04:10:26 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
04:10:29 HOL-Library: theory HOL-Library.Z2
04:10:31 HOL-Library: theory HOL-Library.Countable
04:10:35 HOL-Library: theory HOL-Library.BigO
04:10:35 HOL-Library: theory HOL-Library.Prefix_Order
04:10:35 HOL-Library: theory HOL-Library.Subseq_Order
04:10:36 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
04:10:39 HOL-Library: theory HOL-Library.Tree_Multiset
04:10:43 HOL-Library: theory HOL-Library.Complex_Order
04:10:45 HOL-Library: theory HOL-Library.Diagonal_Subsequence
04:10:48 HOL-Library: theory HOL-Library.Discrete
04:10:49 HOL-Library: theory HOL-Library.Going_To_Filter
04:10:49 HOL-Library: theory HOL-Library.Indicator_Function
04:10:51 HOL-Library: theory HOL-Library.Countable_Set
04:10:52 HOL-Library: theory HOL-Library.FSet
04:10:53 HOL-Library: theory HOL-Library.Landau_Symbols
04:10:56 HOL-Library: theory HOL-Library.Lattice_Algebras
04:11:00 HOL-Library: theory HOL-Library.Countable_Complete_Lattices
04:11:21 HOL-Library: theory HOL-Library.Countable_Set_Type
04:11:28 HOL-Library: theory HOL-Library.Set_Idioms
04:11:35 HOL-Library: theory HOL-Library.Liminf_Limsup
04:11:40 HOL-Library: theory HOL-Library.Finite_Map
04:11:43 HOL-Library: theory HOL-Library.Log_Nat
04:11:47 HOL-Library: theory HOL-Library.Lub_Glb
04:11:49 HOL-Library: theory HOL-Library.Nonpos_Ints
04:11:53 HOL-Library: theory HOL-Library.OptionalSugar
04:11:55 HOL-Library: theory HOL-Library.Order_Continuity
04:11:58 HOL-Library: theory HOL-Library.Periodic_Fun
04:12:02 HOL-Library: theory HOL-Library.Interval
04:12:05 HOL-Library: theory HOL-Library.Float
04:12:07 HOL-Library: theory HOL-Library.Extended_Nat
04:12:30 HOL-Library: theory HOL-Library.Extended_Real
04:12:37 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
04:12:49 HOL-Library: theory HOL-Library.Quadratic_Discriminant
04:12:53 HOL-Library: theory HOL-Library.Sum_of_Squares
04:12:58 HOL-Library: theory HOL-Library.Code_Target_Numeral_Float
04:13:01 HOL-Library: theory HOL-Library.Interval_Float
04:13:01 HOL-Library: theory HOL-Library.Tree_Real
04:13:32 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
04:16:17 HOL-Library: theory HOL-Library.RBT
04:16:22 HOL-Library: theory HOL-Library.RBT_Mapping
04:16:22 HOL-Library: theory HOL-Library.RBT_Set
04:22:23 HOL-Library: theory HOL-Library.Disjoint_FSets
04:22:23 HOL-Library: theory HOL-Library.Library
04:25:12 Timing HOL-Library (6 threads, 961.017s elapsed time, 2139.605s cpu time, 74.646s GC time, factor 2.23)
04:25:12 Finished HOL-Library (0:18:09 elapsed time, 0:39:43 cpu time, factor 2.19)
04:25:12 Building HOL-Computational_Algebra ...
04:25:16 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field
04:25:16 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure
04:25:16 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring
04:25:58 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm
04:25:58 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial
04:27:06 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
04:27:28 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction
04:27:29 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes
04:27:30 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring
04:27:33 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series
04:27:40 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers
04:27:40 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree
04:27:41 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial
04:28:45 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS
04:28:48 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Laurent_Series
04:29:42 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra
04:32:28 Timing HOL-Computational_Algebra (6 threads, 91.133s elapsed time, 469.284s cpu time, 9.032s GC time, factor 5.15)
04:32:28 Finished HOL-Computational_Algebra (0:07:11 elapsed time, 0:11:38 cpu time, factor 1.62)
04:32:28 Building HOL-Algebra ...
04:32:32 HOL-Algebra: theory HOL-Cardinals.Fun_More
04:32:32 HOL-Algebra: theory HOL-Cardinals.Order_Relation_More
04:32:32 HOL-Algebra: theory HOL-Cardinals.Order_Union
04:32:32 HOL-Algebra: theory HOL-Combinatorics.Transposition
04:32:32 HOL-Algebra: theory HOL-Algebra.Exponent
04:32:32 HOL-Algebra: theory HOL-Algebra.Congruence
04:32:40 HOL-Algebra: theory HOL-Combinatorics.Permutations
04:32:41 HOL-Algebra: theory HOL-Cardinals.Wellfounded_More
04:32:42 HOL-Algebra: theory HOL-Cardinals.Wellorder_Relation
04:32:48 HOL-Algebra: theory HOL-Cardinals.Wellorder_Embedding
04:32:54 HOL-Algebra: theory HOL-Cardinals.Wellorder_Constructions
04:32:58 HOL-Algebra: theory HOL-Algebra.Order
04:33:10 HOL-Algebra: theory HOL-Combinatorics.List_Permutation
04:33:10 HOL-Algebra: theory HOL-Combinatorics.Cycles
04:33:17 HOL-Algebra: theory HOL-Cardinals.Cardinal_Order_Relation
04:33:29 HOL-Algebra: theory HOL-Algebra.Lattice
04:33:44 HOL-Algebra: theory HOL-Cardinals.Cardinal_Arithmetic
04:33:50 HOL-Algebra: theory HOL-Algebra.Complete_Lattice
04:33:59 HOL-Algebra: theory HOL-Algebra.Galois_Connection
04:33:59 HOL-Algebra: theory HOL-Algebra.Group
04:34:28 HOL-Algebra: theory HOL-Algebra.Bij
04:34:28 HOL-Algebra: theory HOL-Algebra.Coset
04:34:28 HOL-Algebra: theory HOL-Algebra.FiniteProduct
04:34:40 HOL-Algebra: theory HOL-Algebra.Ring
04:34:52 HOL-Algebra: theory HOL-Algebra.Group_Action
04:34:53 HOL-Algebra: theory HOL-Algebra.Sylow
04:34:54 HOL-Algebra: theory HOL-Algebra.Divisibility
04:34:55 HOL-Algebra: theory HOL-Algebra.Generated_Groups
04:35:00 HOL-Algebra: theory HOL-Algebra.Zassenhaus
04:35:16 HOL-Algebra: theory HOL-Algebra.Solvable_Groups
04:35:18 HOL-Algebra: theory HOL-Algebra.Elementary_Groups
04:35:20 HOL-Algebra: theory HOL-Algebra.Sym_Groups
04:35:34 HOL-Algebra: theory HOL-Algebra.Exact_Sequence
04:35:34 HOL-Algebra: theory HOL-Algebra.Product_Groups
04:35:42 HOL-Algebra: theory HOL-Algebra.Free_Abelian_Groups
04:35:45 HOL-Algebra: theory HOL-Algebra.AbelCoset
04:35:46 HOL-Algebra: theory HOL-Algebra.Module
04:36:19 HOL-Algebra: theory HOL-Algebra.Ideal
04:36:31 HOL-Algebra: theory HOL-Algebra.Ideal_Product
04:36:31 HOL-Algebra: theory HOL-Algebra.RingHom
04:36:39 HOL-Algebra: theory HOL-Algebra.QuotRing
04:36:39 HOL-Algebra: theory HOL-Algebra.UnivPoly
04:36:54 HOL-Algebra: theory HOL-Algebra.IntRing
04:36:54 HOL-Algebra: theory HOL-Algebra.Weak_Morphisms
04:36:59 HOL-Algebra: theory HOL-Algebra.Chinese_Remainder
04:37:55 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group
04:38:20 HOL-Algebra: theory HOL-Algebra.Ring_Divisibility
04:38:20 HOL-Algebra: theory HOL-Algebra.Subrings
04:38:31 HOL-Algebra: theory HOL-Algebra.Embedded_Algebras
04:38:31 HOL-Algebra: theory HOL-Algebra.Generated_Rings
04:38:34 HOL-Algebra: theory HOL-Algebra.Generated_Fields
04:39:00 HOL-Algebra: theory HOL-Algebra.Polynomials
04:40:14 HOL-Algebra: theory HOL-Algebra.Polynomial_Divisibility
04:41:52 HOL-Algebra: theory HOL-Algebra.Finite_Extensions
04:41:53 HOL-Algebra: theory HOL-Algebra.Indexed_Polynomials
04:42:36 HOL-Algebra: theory HOL-Algebra.Algebraic_Closure
04:43:06 HOL-Algebra: theory HOL-Algebra.Algebra
04:45:29 Timing HOL-Algebra (6 threads, 197.448s elapsed time, 1231.980s cpu time, 119.504s GC time, factor 6.24)
04:45:29 Finished HOL-Algebra (0:12:54 elapsed time, 0:27:29 cpu time, factor 2.13)
04:45:29 Running HOL-Corec_Examples ...
04:45:32 HOL-Corec_Examples: theory HOL-Corec_Examples.Iterate_GPV
04:45:32 HOL-Corec_Examples: theory HOL-Corec_Examples.LFilter
04:45:32 HOL-Corec_Examples: theory HOL-Corec_Examples.Simple_Nesting
04:45:32 HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Processor
04:45:32 HOL-Corec_Examples: theory HOL-Corec_Examples.Paper_Examples
04:48:31 HOL-Corec_Examples: theory HOL-Corec_Examples.GPV_Bare_Bones
04:48:31 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_A
04:48:31 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_Poly
04:48:31 HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Poly
04:48:31 HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Mono
04:48:31 HOL-Corec_Examples: theory HOL-Corec_Examples.Small_Concrete
04:48:33 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_B
04:48:34 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_C
04:48:35 HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Friends
04:48:35 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_D
04:48:37 HOL-Corec_Examples: theory HOL-Corec_Examples.TLList_Friends
04:48:37 HOL-Corec_Examples: theory HOL-Corec_Examples.Type_Class
04:50:29 Timing HOL-Corec_Examples (6 threads, 292.466s elapsed time, 1118.755s cpu time, 93.755s GC time, factor 3.83)
04:50:29 Finished HOL-Corec_Examples (0:04:58 elapsed time, 0:18:45 cpu time, factor 3.77)
04:50:29 Running HOL-Datatype_Benchmark ...
04:50:34 HOL-Datatype_Benchmark: theory HOL-Datatype_Benchmark.Brackin
04:50:34 HOL-Datatype_Benchmark: theory HOL-Datatype_Benchmark.Misc_N2M
04:50:34 HOL-Datatype_Benchmark: theory HOL-Datatype_Benchmark.IsaFoR
05:08:43 Timing HOL-Datatype_Benchmark (6 threads, 1084.748s elapsed time, 4675.736s cpu time, 1653.380s GC time, factor 4.31)
05:08:43 Finished HOL-Datatype_Benchmark (0:18:13 elapsed time, 1:18:04 cpu time, factor 4.29)
05:08:43 Running HOL-Datatype_Examples ...
05:08:47 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Compat
05:08:47 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Datatype_Simproc_Tests
05:08:47 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lift_BNF
05:08:47 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TLList
05:08:47 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Milner_Tofte
05:08:47 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFI
05:08:51 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Cyclic_List
05:08:53 HOL-Datatype_Examples: theory HOL-Datatype_Examples.FAE_Sequence
05:08:55 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Free_Idempotent_Monoid
05:08:58 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Regex_ACI
05:08:59 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Regex_ACIDZ
05:09:03 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Koenig
05:09:06 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Process
05:09:09 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Stream_Processor
05:09:11 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lambda_Term
05:09:17 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Codatatype
05:09:18 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Datatype
05:09:23 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Prelim
05:09:24 HOL-Datatype_Examples: theory HOL-Datatype_Examples.DTree
05:09:26 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Gram_Lang
05:09:27 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Parallel_Composition
05:09:30 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFsetI
05:14:06 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primcorec
05:15:03 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primrec
05:15:55 Timing HOL-Datatype_Examples (6 threads, 189.409s elapsed time, 1121.684s cpu time, 93.616s GC time, factor 5.92)
05:15:55 Finished HOL-Datatype_Examples (0:07:10 elapsed time, 0:20:11 cpu time, factor 2.82)
05:15:55 Running HOL-Decision_Procs ...
05:16:01 HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library
05:16:01 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order
05:16:01 HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions
05:16:01 HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper
05:16:01 HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux
05:16:01 HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List
05:16:01 HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair
05:16:21 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring
05:16:32 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order_Ex
05:16:33 HOL-Decision_Procs: theory HOL-Decision_Procs.Ferrack
05:16:33 HOL-Decision_Procs: theory HOL-Decision_Procs.MIR
05:16:38 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Bounds
05:17:08 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation
05:17:13 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Complete
05:17:17 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflective_Field
05:17:20 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial
05:17:35 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex
05:17:49 HOL-Decision_Procs: theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff
05:18:49 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Ex
05:18:50 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Quickcheck_Ex
05:22:16 HOL-Decision_Procs: theory HOL-Decision_Procs.Decision_Procs
05:25:07 Timing HOL-Decision_Procs (6 threads, 490.448s elapsed time, 2778.608s cpu time, 168.293s GC time, factor 5.67)
05:25:07 Finished HOL-Decision_Procs (0:09:07 elapsed time, 0:46:42 cpu time, factor 5.12)
05:25:07 Running HOL-IMP ...
05:25:11 HOL-IMP: theory HOL-IMP.AExp
05:25:11 HOL-IMP: theory HOL-IMP.C_like
05:25:11 HOL-IMP: theory HOL-IMP.OO
05:25:11 HOL-IMP: theory HOL-IMP.Complete_Lattice
05:25:11 HOL-IMP: theory HOL-IMP.Star
05:25:13 HOL-IMP: theory HOL-IMP.Types
05:25:18 HOL-IMP: theory HOL-IMP.ASM
05:25:18 HOL-IMP: theory HOL-IMP.BExp
05:25:27 HOL-IMP: theory HOL-IMP.Com
05:25:27 HOL-IMP: theory HOL-IMP.Procs
05:25:31 HOL-IMP: theory HOL-IMP.ACom
05:25:32 HOL-IMP: theory HOL-IMP.Abs_Int_Tests
05:25:32 HOL-IMP: theory HOL-IMP.Big_Step
05:25:33 HOL-IMP: theory HOL-IMP.Vars
05:25:33 HOL-IMP: theory HOL-IMP.Poly_Types
05:25:33 HOL-IMP: theory HOL-IMP.Procs_Dyn_Vars_Dyn
05:25:36 HOL-IMP: theory HOL-IMP.Denotational
05:25:37 HOL-IMP: theory HOL-IMP.Hoare
05:25:38 HOL-IMP: theory HOL-IMP.Hoare_Examples
05:25:39 HOL-IMP: theory HOL-IMP.Hoare_Sound_Complete
05:25:39 HOL-IMP: theory HOL-IMP.Hoare_Total
05:25:40 HOL-IMP: theory HOL-IMP.Hoare_Total_EX
05:25:40 HOL-IMP: theory HOL-IMP.Hoare_Total_EX2
05:25:40 HOL-IMP: theory HOL-IMP.VCG
05:25:43 HOL-IMP: theory HOL-IMP.Sec_Type_Expr
05:25:44 HOL-IMP: theory HOL-IMP.VCG_Total_EX
05:25:45 HOL-IMP: theory HOL-IMP.VCG_Total_EX2
05:25:46 HOL-IMP: theory HOL-IMP.Sec_Typing
05:25:49 HOL-IMP: theory HOL-IMP.Sec_TypingT
05:25:52 HOL-IMP: theory HOL-IMP.Sem_Equiv
05:25:52 HOL-IMP: theory HOL-IMP.Def_Init
05:25:54 HOL-IMP: theory HOL-IMP.Def_Init_Exp
05:25:54 HOL-IMP: theory HOL-IMP.Live
05:25:54 HOL-IMP: theory HOL-IMP.Fold
05:25:55 HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Dyn
05:25:55 HOL-IMP: theory HOL-IMP.Def_Init_Big
05:25:57 HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Stat
05:25:57 HOL-IMP: theory HOL-IMP.Collecting
05:25:58 HOL-IMP: theory HOL-IMP.Compiler
05:25:59 HOL-IMP: theory HOL-IMP.Def_Init_Small
05:26:00 HOL-IMP: theory HOL-IMP.Small_Step
05:26:01 HOL-IMP: theory HOL-IMP.Live_True
05:26:01 HOL-IMP: theory HOL-IMP.Collecting1
05:26:02 HOL-IMP: theory HOL-IMP.Collecting_Examples
05:26:03 HOL-IMP: theory HOL-IMP.Abs_Int_init
05:26:04 HOL-IMP: theory HOL-IMP.Finite_Reachable
05:26:05 HOL-IMP: theory HOL-IMP.Abs_Int0
05:26:12 HOL-IMP: theory HOL-IMP.Compiler2
05:26:13 HOL-IMP: theory HOL-IMP.Abs_State
05:26:18 HOL-IMP: theory HOL-IMP.Abs_Int1
05:26:22 HOL-IMP: theory HOL-IMP.Abs_Int1_const
05:26:22 HOL-IMP: theory HOL-IMP.Abs_Int1_parity
05:26:22 HOL-IMP: theory HOL-IMP.Abs_Int2
05:26:28 HOL-IMP: theory HOL-IMP.Abs_Int2_ivl
05:26:33 HOL-IMP: theory HOL-IMP.Abs_Int3
05:27:44 Timing HOL-IMP (6 threads, 120.889s elapsed time, 719.584s cpu time, 24.640s GC time, factor 5.95)
05:27:44 Finished HOL-IMP (0:02:35 elapsed time, 0:12:16 cpu time, factor 4.75)
05:27:44 Running HOL-Metis_Examples ...
05:27:48 HOL-Metis_Examples: theory HOL-Metis_Examples.Message
05:27:48 HOL-Metis_Examples: theory HOL-Metis_Examples.Tarski
05:27:48 HOL-Metis_Examples: theory HOL-Decision_Procs.Dense_Linear_Order
05:27:48 HOL-Metis_Examples: theory HOL-Metis_Examples.Sets
05:27:48 HOL-Metis_Examples: theory HOL-Metis_Examples.Abstraction
05:27:48 HOL-Metis_Examples: theory HOL-Metis_Examples.Binary_Tree
05:27:50 HOL-Metis_Examples: theory HOL-Metis_Examples.Trans_Closure
05:27:51 HOL-Metis_Examples: theory HOL-Metis_Examples.Type_Encodings
05:27:51 HOL-Metis_Examples: theory HOL-Metis_Examples.Proxies
05:27:53 HOL-Metis_Examples: theory HOL-Metis_Examples.Clausification
05:28:19 HOL-Metis_Examples: theory HOL-Metis_Examples.Big_O
05:28:57 Timing HOL-Metis_Examples (6 threads, 32.936s elapsed time, 157.103s cpu time, 4.849s GC time, factor 4.77)
05:28:57 Finished HOL-Metis_Examples (0:01:11 elapsed time, 0:02:47 cpu time, factor 2.34)
05:28:57 Running HOL-MicroJava ...
05:28:59 HOL-MicroJava: theory HOL-Eisbach.Eisbach
05:28:59 HOL-MicroJava: theory HOL-Library.Transitive_Closure_Table
05:28:59 HOL-MicroJava: theory HOL-Library.While_Combinator
05:29:10 HOL-MicroJava: theory HOL-MicroJava.Semilat
05:29:13 HOL-MicroJava: theory HOL-MicroJava.JBasis
05:29:15 HOL-MicroJava: theory HOL-MicroJava.Err
05:29:15 HOL-MicroJava: theory HOL-MicroJava.AuxLemmas
05:29:15 HOL-MicroJava: theory HOL-MicroJava.Type
05:29:21 HOL-MicroJava: theory HOL-MicroJava.Listn
05:29:22 HOL-MicroJava: theory HOL-MicroJava.Opt
05:29:22 HOL-MicroJava: theory HOL-MicroJava.Product
05:29:27 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework
05:29:27 HOL-MicroJava: theory HOL-MicroJava.Semilattices
05:29:27 HOL-MicroJava: theory HOL-MicroJava.SemilatAlg
05:29:29 HOL-MicroJava: theory HOL-MicroJava.Kildall
05:29:29 HOL-MicroJava: theory HOL-MicroJava.LBVSpec
05:29:29 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_err
05:29:33 HOL-MicroJava: theory HOL-MicroJava.Decl
05:29:34 HOL-MicroJava: theory HOL-MicroJava.Value
05:29:34 HOL-MicroJava: theory HOL-MicroJava.SystemClasses
05:29:34 HOL-MicroJava: theory HOL-MicroJava.TypeRel
05:29:37 HOL-MicroJava: theory HOL-MicroJava.LBVComplete
05:29:37 HOL-MicroJava: theory HOL-MicroJava.LBVCorrect
05:29:41 HOL-MicroJava: theory HOL-MicroJava.Abstract_BV
05:29:42 HOL-MicroJava: theory HOL-MicroJava.WellForm
05:29:42 HOL-MicroJava: theory HOL-MicroJava.State
05:29:42 HOL-MicroJava: theory HOL-MicroJava.Term
05:29:45 HOL-MicroJava: theory HOL-MicroJava.Exceptions
05:29:48 HOL-MicroJava: theory HOL-MicroJava.JType
05:29:51 HOL-MicroJava: theory HOL-MicroJava.JVMType
05:30:03 HOL-MicroJava: theory HOL-MicroJava.WellType
05:30:07 HOL-MicroJava: theory HOL-MicroJava.Conform
05:30:07 HOL-MicroJava: theory HOL-MicroJava.Eval
05:30:07 HOL-MicroJava: theory HOL-MicroJava.TypeInf
05:30:13 HOL-MicroJava: theory HOL-MicroJava.JVMState
05:30:13 HOL-MicroJava: theory HOL-MicroJava.JVMInstructions
05:30:19 HOL-MicroJava: theory HOL-MicroJava.JVMExceptions
05:30:19 HOL-MicroJava: theory HOL-MicroJava.JVMExecInstr
05:30:20 HOL-MicroJava: theory HOL-MicroJava.Effect
05:30:22 HOL-MicroJava: theory HOL-MicroJava.JVMExec
05:30:25 HOL-MicroJava: theory HOL-MicroJava.DefsComp
05:30:25 HOL-MicroJava: theory HOL-MicroJava.JVMDefensive
05:30:25 HOL-MicroJava: theory HOL-MicroJava.JVMListExample
05:30:26 HOL-MicroJava: theory HOL-MicroJava.Index
05:30:28 HOL-MicroJava: theory HOL-MicroJava.TranslCompTp
05:30:32 HOL-MicroJava: theory HOL-MicroJava.Example
05:30:32 HOL-MicroJava: theory HOL-MicroJava.JListExample
05:30:32 HOL-MicroJava: theory HOL-MicroJava.JTypeSafe
05:30:32 HOL-MicroJava: theory HOL-MicroJava.TranslComp
05:30:34 HOL-MicroJava: theory HOL-MicroJava.LemmasComp
05:30:38 HOL-MicroJava: theory HOL-MicroJava.CorrComp
05:31:26 HOL-MicroJava: theory HOL-MicroJava.BVSpec
05:31:26 HOL-MicroJava: theory HOL-MicroJava.EffectMono
05:31:28 HOL-MicroJava: theory HOL-MicroJava.Altern
05:31:29 HOL-MicroJava: theory HOL-MicroJava.Correct
05:31:29 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_JVM
05:31:32 HOL-MicroJava: theory HOL-MicroJava.BVSpecTypeSafe
05:31:34 HOL-MicroJava: theory HOL-MicroJava.JVM
05:31:37 HOL-MicroJava: theory HOL-MicroJava.CorrCompTp
05:31:37 HOL-MicroJava: theory HOL-MicroJava.LBVJVM
05:31:42 HOL-MicroJava: theory HOL-MicroJava.BVNoTypeError
05:31:42 HOL-MicroJava: theory HOL-MicroJava.BVExample
05:32:02 HOL-MicroJava: theory HOL-MicroJava.MicroJava
05:32:59 Timing HOL-MicroJava (6 threads, 111.775s elapsed time, 665.575s cpu time, 13.697s GC time, factor 5.95)
05:32:59 Finished HOL-MicroJava (0:03:57 elapsed time, 0:11:55 cpu time, factor 3.01)
05:32:59 Building HOL-Nominal ...
05:33:01 HOL-Nominal: theory HOL-Library.Infinite_Set
05:33:01 HOL-Nominal: theory HOL-Library.Old_Datatype
05:33:12 HOL-Nominal: theory HOL-Nominal.Nominal
05:34:52 Timing HOL-Nominal (6 threads, 14.449s elapsed time, 62.386s cpu time, 1.158s GC time, factor 4.32)
05:34:52 Finished HOL-Nominal (0:01:51 elapsed time, 0:02:29 cpu time, factor 1.34)
05:34:52 Running HOL-Nominal-Examples ...
05:34:54 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CK_Machine
05:34:54 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR_Takahashi
05:34:54 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class1
05:34:54 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Compile
05:34:54 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Crary
05:34:54 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Contexts
05:35:07 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Fsub
05:35:09 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Height
05:35:19 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lam_Funs
05:35:20 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lambda_mu
05:35:30 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR
05:35:36 HOL-Nominal-Examples: theory HOL-Nominal-Examples.SN
05:35:44 HOL-Nominal-Examples: theory HOL-Nominal-Examples.LocalWeakening
05:35:48 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Pattern
05:35:55 HOL-Nominal-Examples: theory HOL-Nominal-Examples.SOS
05:35:59 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Standardization
05:36:03 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Support
05:36:06 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Type_Preservation
05:36:13 HOL-Nominal-Examples: theory HOL-Nominal-Examples.W
05:36:18 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening
05:39:42 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2
05:40:13 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3
05:47:09 HOL-Nominal-Examples: theory HOL-Nominal-Examples.VC_Condition
05:47:19 Timing HOL-Nominal-Examples (6 threads, 630.447s elapsed time, 3277.243s cpu time, 184.382s GC time, factor 5.20)
05:47:19 Finished HOL-Nominal-Examples (0:12:19 elapsed time, 0:55:30 cpu time, factor 4.50)
05:47:19 Building HOL-Nonstandard_Analysis ...
05:47:24 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Free_Ultrafilter
05:47:26 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.StarDef
05:47:41 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperNat
05:47:46 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperDef
05:47:53 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSA
05:48:17 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSComplex
05:48:17 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Star
05:48:23 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLim
05:48:23 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NatStar
05:48:30 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HDeriv
05:48:30 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSEQ
05:48:40 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSeries
05:48:42 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HTranscendental
05:48:51 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLog
05:48:51 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSCA
05:48:55 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hyperreal
05:49:02 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CStar
05:49:03 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CLim
05:49:06 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hypercomplex
05:49:07 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Nonstandard_Analysis
05:51:07 Timing HOL-Nonstandard_Analysis (6 threads, 28.372s elapsed time, 132.254s cpu time, 2.295s GC time, factor 4.66)
05:51:07 Finished HOL-Nonstandard_Analysis (0:03:46 elapsed time, 0:05:48 cpu time, factor 1.54)
05:51:07 Running HOL-Nonstandard_Analysis-Examples ...
05:51:11 HOL-Nonstandard_Analysis-Examples: theory HOL-Nonstandard_Analysis-Examples.NSPrimes
05:51:16 Timing HOL-Nonstandard_Analysis-Examples (6 threads, 2.811s elapsed time, 8.850s cpu time, 0.000s GC time, factor 3.15)
05:51:16 Finished HOL-Nonstandard_Analysis-Examples (0:00:08 elapsed time, 0:00:13 cpu time, factor 1.60)
05:51:16 Building HOL-Number_Theory ...
05:51:20 HOL-Number_Theory: theory HOL-Algebra.Congruence
05:51:20 HOL-Number_Theory: theory HOL-Number_Theory.Cong
05:51:20 HOL-Number_Theory: theory HOL-Number_Theory.Fib
05:51:20 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes
05:51:20 HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers
05:51:33 HOL-Number_Theory: theory HOL-Algebra.Order
05:51:37 HOL-Number_Theory: theory HOL-Number_Theory.Mod_Exp
05:51:37 HOL-Number_Theory: theory HOL-Number_Theory.Totient
05:51:46 HOL-Number_Theory: theory HOL-Algebra.Lattice
05:51:57 HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice
05:52:06 HOL-Number_Theory: theory HOL-Algebra.Group
05:52:24 HOL-Number_Theory: theory HOL-Algebra.Coset
05:52:24 HOL-Number_Theory: theory HOL-Algebra.FiniteProduct
05:52:34 HOL-Number_Theory: theory HOL-Algebra.Ring
05:52:44 HOL-Number_Theory: theory HOL-Algebra.Generated_Groups
05:52:51 HOL-Number_Theory: theory HOL-Algebra.Elementary_Groups
05:53:09 HOL-Number_Theory: theory HOL-Algebra.AbelCoset
05:53:09 HOL-Number_Theory: theory HOL-Algebra.Module
05:53:25 HOL-Number_Theory: theory HOL-Algebra.Ideal
05:53:37 HOL-Number_Theory: theory HOL-Algebra.RingHom
05:53:43 HOL-Number_Theory: theory HOL-Algebra.UnivPoly
05:54:46 HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group
05:55:01 HOL-Number_Theory: theory HOL-Number_Theory.Residues
05:55:09 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion
05:55:11 HOL-Number_Theory: theory HOL-Number_Theory.Gauss
05:55:13 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity
05:55:13 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington
05:55:24 HOL-Number_Theory: theory HOL-Number_Theory.Residue_Primitive_Roots
05:55:31 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory
05:57:40 Timing HOL-Number_Theory (6 threads, 100.487s elapsed time, 639.075s cpu time, 15.894s GC time, factor 6.36)
05:57:40 Finished HOL-Number_Theory (0:06:20 elapsed time, 0:14:32 cpu time, factor 2.29)
05:57:40 Running HOL-Predicate_Compile_Examples ...
05:57:43 HOL-Predicate_Compile_Examples: theory HOL-Library.Predicate_Compile_Alternative_Defs
05:57:45 HOL-Predicate_Compile_Examples: theory HOL-Library.Predicate_Compile_Quickcheck
05:57:45 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Tests
05:57:45 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Examples
05:57:45 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Specialisation_Examples
05:57:48 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_1
05:57:49 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_2
05:57:49 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_3
05:57:53 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_4
05:57:53 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Quickcheck_Examples
05:59:01 HOL-Predicate_Compile_Examples: theory HOL-Library.Code_Prolog
05:59:01 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example
05:59:04 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Code_Prolog_Examples
05:59:04 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Context_Free_Grammar_Example
05:59:04 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Lambda_Example
05:59:04 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.List_Examples
05:59:11 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example_Prolog
05:59:21 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Reg_Exp_Example
05:59:24 Timing HOL-Predicate_Compile_Examples (6 threads, 81.456s elapsed time, 395.912s cpu time, 20.264s GC time, factor 4.86)
05:59:24 Finished HOL-Predicate_Compile_Examples (0:01:42 elapsed time, 0:06:43 cpu time, factor 3.94)
05:59:24 Building HOL-Probability ...
05:59:28 HOL-Probability: theory HOL-Library.Adhoc_Overloading
05:59:28 HOL-Probability: theory HOL-Library.Stream
05:59:28 HOL-Probability: theory HOL-Library.Rewrite
05:59:28 HOL-Probability: theory HOL-Library.Conditional_Parametricity
05:59:28 HOL-Probability: theory HOL-Library.AList
05:59:28 HOL-Probability: theory HOL-Library.Complete_Partial_Order2
05:59:30 HOL-Probability: theory HOL-Library.Monad_Syntax
05:59:31 HOL-Probability: theory HOL-Library.Sublist
05:59:34 HOL-Probability: theory HOL-Library.Tree
05:59:36 HOL-Probability: theory HOL-Library.FSet
05:59:54 HOL-Probability: theory HOL-Combinatorics.Multiset_Permutations
05:59:57 HOL-Probability: theory HOL-Library.Mapping
06:00:13 HOL-Probability: theory HOL-Library.Diagonal_Subsequence
06:00:16 HOL-Probability: theory HOL-Probability.Discrete_Topology
06:00:21 HOL-Probability: theory HOL-Probability.Essential_Supremum
06:00:22 HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams
06:00:24 HOL-Probability: theory HOL-Probability.Probability_Measure
06:00:28 HOL-Probability: theory HOL-Probability.Stopping_Time
06:00:29 HOL-Probability: theory HOL-Library.AList_Mapping
06:00:32 HOL-Probability: theory HOL-Probability.Tree_Space
06:00:56 HOL-Probability: theory HOL-Library.Finite_Map
06:00:58 HOL-Probability: theory HOL-Probability.Conditional_Expectation
06:00:58 HOL-Probability: theory HOL-Probability.Distribution_Functions
06:00:58 HOL-Probability: theory HOL-Probability.Giry_Monad
06:01:03 HOL-Probability: theory HOL-Probability.Weak_Convergence
06:01:11 HOL-Probability: theory HOL-Probability.Helly_Selection
06:01:32 HOL-Probability: theory HOL-Probability.Probability_Mass_Function
06:01:32 HOL-Probability: theory HOL-Probability.Projective_Family
06:01:49 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
06:02:02 HOL-Probability: theory HOL-Probability.Independent_Family
06:02:03 HOL-Probability: theory HOL-Probability.Stream_Space
06:02:20 HOL-Probability: theory HOL-Probability.PMF_Impl
06:02:21 HOL-Probability: theory HOL-Probability.Random_Permutations
06:02:22 HOL-Probability: theory HOL-Probability.SPMF
06:02:22 HOL-Probability: theory HOL-Probability.Convolution
06:02:23 HOL-Probability: theory HOL-Probability.Information
06:02:26 HOL-Probability: theory HOL-Probability.Product_PMF
06:02:39 HOL-Probability: theory HOL-Probability.Hoeffding
06:03:00 HOL-Probability: theory HOL-Probability.Distributions
06:03:27 HOL-Probability: theory HOL-Probability.Characteristic_Functions
06:03:27 HOL-Probability: theory HOL-Probability.Sinc_Integral
06:03:36 HOL-Probability: theory HOL-Probability.Levy
06:03:43 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
06:09:07 HOL-Probability: theory HOL-Probability.Fin_Map
06:09:19 HOL-Probability: theory HOL-Probability.Projective_Limit
06:09:30 HOL-Probability: theory HOL-Probability.Probability
06:11:13 Timing HOL-Probability (6 threads, 598.936s elapsed time, 936.757s cpu time, 29.327s GC time, factor 1.56)
06:11:13 Finished HOL-Probability (0:11:43 elapsed time, 0:18:21 cpu time, factor 1.57)
06:11:13 Running HOL-Probability-ex ...
06:11:17 HOL-Probability-ex: theory HOL-Probability-ex.Dining_Cryptographers
06:11:17 HOL-Probability-ex: theory HOL-Probability-ex.Measure_Not_CCC
06:11:17 HOL-Probability-ex: theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure
06:11:38 Timing HOL-Probability-ex (6 threads, 19.095s elapsed time, 94.058s cpu time, 0.716s GC time, factor 4.93)
06:11:38 Finished HOL-Probability-ex (0:00:24 elapsed time, 0:01:39 cpu time, factor 4.11)
06:11:38 Building HOL-Proofs ...
06:11:42 HOL-Proofs: theory Tools.Code_Generator
06:11:53 HOL-Proofs: theory HOL.HOL
06:12:23 HOL-Proofs: theory HOL.Argo
06:12:23 HOL-Proofs: theory HOL.Ctr_Sugar
06:12:23 HOL-Proofs: theory HOL.Orderings
06:12:45 HOL-Proofs: theory HOL.SAT
06:12:55 HOL-Proofs: theory HOL.Groups
06:13:11 HOL-Proofs: theory HOL.Lattices
06:13:19 HOL-Proofs: theory HOL.Boolean_Algebras
06:13:25 HOL-Proofs: theory HOL.Set
06:13:43 HOL-Proofs: theory HOL.Fun
06:13:43 HOL-Proofs: theory HOL.Typedef
06:13:57 HOL-Proofs: theory HOL.Complete_Lattices
06:13:57 HOL-Proofs: theory HOL.Rings
06:14:28 HOL-Proofs: theory HOL.Inductive
06:14:45 HOL-Proofs: theory HOL.Product_Type
06:14:45 HOL-Proofs: theory HOL.Sum_Type
06:15:01 HOL-Proofs: theory HOL.Complete_Partial_Order
06:15:13 HOL-Proofs: theory HOL.Nat
06:15:41 HOL-Proofs: theory HOL.Fields
06:15:41 HOL-Proofs: theory HOL.Meson
06:15:47 HOL-Proofs: theory HOL.ATP
06:16:04 HOL-Proofs: theory HOL.Metis
06:16:19 HOL-Proofs: theory HOL.Finite_Set
06:16:55 HOL-Proofs: theory HOL.Relation
06:17:08 HOL-Proofs: theory HOL.Transitive_Closure
06:17:23 HOL-Proofs: theory HOL.Wellfounded
06:17:34 HOL-Proofs: theory HOL.Hilbert_Choice
06:17:34 HOL-Proofs: theory HOL.Fun_Def_Base
06:17:34 HOL-Proofs: theory HOL.Wfrec
06:17:38 HOL-Proofs: theory HOL.Order_Relation
06:17:50 HOL-Proofs: theory HOL.BNF_Wellorder_Relation
06:18:05 HOL-Proofs: theory HOL.BNF_Wellorder_Embedding
06:18:05 HOL-Proofs: theory HOL.Zorn
06:18:31 HOL-Proofs: theory HOL.BNF_Wellorder_Constructions
06:18:59 HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation
06:19:22 HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic
06:19:31 HOL-Proofs: theory HOL.BNF_Def
06:19:40 HOL-Proofs: theory HOL.BNF_Composition
06:19:40 HOL-Proofs: theory HOL.Basic_BNFs
06:19:48 HOL-Proofs: theory HOL.BNF_Fixpoint_Base
06:20:01 HOL-Proofs: theory HOL.BNF_Least_Fixpoint
06:20:10 HOL-Proofs: theory HOL.Basic_BNF_LFPs
06:20:12 HOL-Proofs: theory HOL.Transfer
06:20:21 HOL-Proofs: theory HOL.Num
06:20:36 HOL-Proofs: theory HOL.Power
06:20:48 HOL-Proofs: theory HOL.Groups_Big
06:21:09 HOL-Proofs: theory HOL.Equiv_Relations
06:21:16 HOL-Proofs: theory HOL.Lifting
06:21:27 HOL-Proofs: theory HOL.Lifting_Set
06:21:27 HOL-Proofs: theory HOL.Option
06:21:27 HOL-Proofs: theory HOL.Quotient
06:21:36 HOL-Proofs: theory HOL.Extraction
06:21:36 HOL-Proofs: theory HOL.Lattices_Big
06:21:36 HOL-Proofs: theory HOL.Partial_Function
06:21:52 HOL-Proofs: theory HOL.Fun_Def
06:22:17 HOL-Proofs: theory HOL.Int
06:22:41 HOL-Proofs: theory HOL.Euclidean_Division
06:23:07 HOL-Proofs: theory HOL.Parity
06:23:14 HOL-Proofs: theory HOL.Divides
06:23:28 HOL-Proofs: theory HOL.Numeral_Simprocs
06:23:28 HOL-Proofs: theory HOL.Set_Interval
06:23:36 HOL-Proofs: theory HOL.Semiring_Normalization
06:23:36 HOL-Proofs: theory HOL.SMT
06:24:00 HOL-Proofs: theory HOL.Groebner_Basis
06:24:29 HOL-Proofs: theory HOL.Conditionally_Complete_Lattices
06:24:29 HOL-Proofs: theory HOL.Filter
06:24:29 HOL-Proofs: theory HOL.Presburger
06:25:17 HOL-Proofs: theory HOL.Sledgehammer
06:25:27 HOL-Proofs: theory HOL.List
06:27:07 HOL-Proofs: theory HOL.Groups_List
06:27:07 HOL-Proofs: theory HOL.Map
06:27:24 HOL-Proofs: theory HOL.Bit_Operations
06:27:24 HOL-Proofs: theory HOL.Factorial
06:27:24 HOL-Proofs: theory HOL.Enum
06:27:42 HOL-Proofs: theory HOL.Binomial
06:28:42 HOL-Proofs: theory HOL.Code_Numeral
06:28:52 HOL-Proofs: theory HOL.GCD
06:28:52 HOL-Proofs: theory HOL.String
06:28:52 HOL-Proofs: theory HOL.Random
06:29:06 HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint
06:29:06 HOL-Proofs: theory HOL.Predicate
06:29:06 HOL-Proofs: theory HOL.Typerep
06:29:21 HOL-Proofs: theory HOL.Lazy_Sequence
06:29:23 HOL-Proofs: theory HOL.Limited_Sequence
06:29:24 HOL-Proofs: theory HOL.Code_Evaluation
06:29:32 HOL-Proofs: theory HOL.Quickcheck_Random
06:29:44 HOL-Proofs: theory HOL.Quickcheck_Exhaustive
06:29:44 HOL-Proofs: theory HOL.Quickcheck_Narrowing
06:29:44 HOL-Proofs: theory HOL.Random_Pred
06:29:45 HOL-Proofs: theory HOL.Random_Sequence
06:30:03 HOL-Proofs: theory HOL.Record
06:30:03 HOL-Proofs: theory HOL.Predicate_Compile
06:30:21 HOL-Proofs: theory HOL.Mirabelle
06:30:36 HOL-Proofs: theory HOL.Nitpick
06:30:58 HOL-Proofs: theory HOL.Nunchaku
06:31:01 HOL-Proofs: theory Main
06:31:02 HOL-Proofs: theory HOL-Library.Realizers
06:35:44 Build timed out (after 300 minutes). Marking the build as aborted.
06:35:44 Build was aborted
06:35:44 Archiving artifacts
06:36:01 Started calculate disk usage of build
06:36:01 Finished Calculation of disk usage of build in 0 seconds
06:36:04 Started calculate disk usage of workspace
06:36:07 Finished Calculation of disk usage of workspace in  2 second
06:36:07 No emails were triggered.
06:36:07 Finished: ABORTED