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
14 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 b3b84b71e398acb6f4890b47dca776b0c4ea96fa --template exists\n
exists
[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(b3b84b71e398acb6f4890b47dca776b0c4ea96fa)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-nightly-benchmark] $ /bin/sh -xe /tmp/jenkins7367653595949912261.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.4.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/x86_64_32-linux"
ML_SYSTEM="polyml-5.8"
ML_OPTIONS="-H 4000 --maxheap 8G"
jobs = 1, threads = 6, numa = false

=== BUILD ===

Build started at Tue, 24 Sep 2019 22:51:02 GMT
Isabelle id c5232e6fb10b

=== LOG ===

Session Pure/Pure
Session FOL/FOL
Session HOL/HOL (main)
Session HOL/HOL-Cardinals (timing)
Session HOL/HOL-Eisbach
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-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-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 HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-Lambda (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, 1.132s elapsed time, 1.132s cpu time, 0.000s GC time, factor 1.00)
Timing Pure (1 threads, 1.132s elapsed time, 1.132s cpu time, 0.000s GC time, factor 1.00)
Finished Pure (0:00:21 elapsed time, 0:00:21 cpu time, factor 1.00)
Building HOL ...
HOL: theory HOL.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, 197.573s elapsed time, 688.100s cpu time, 54.204s GC time, factor 3.48)
Timing HOL (6 threads, 197.573s elapsed time, 688.100s cpu time, 54.204s GC time, factor 3.48)
Finished HOL (0:03:56 elapsed time, 0:12:48 cpu time, factor 3.25)
Building HOL-Analysis ...
HOL-Analysis: theory HOL-Library.Disjoint_Sets
HOL-Analysis: theory HOL-Library.Cancellation
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.Countable
HOL-Analysis: theory HOL-Analysis.Inner_Product
HOL-Analysis: theory HOL-Library.Multiset
HOL-Analysis: theory HOL-Analysis.L2_Norm
HOL-Analysis: theory HOL-Analysis.Operator_Norm
HOL-Analysis: theory HOL-Analysis.Poly_Roots
HOL-Analysis: theory HOL-Analysis.Product_Vector
HOL-Analysis: theory HOL-Library.Discrete
HOL-Analysis: theory HOL-Library.Cardinality
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-Analysis.Euclidean_Space
HOL-Analysis: theory HOL-Library.Numeral_Type
HOL-Analysis: theory HOL-Library.Periodic_Fun
HOL-Analysis: theory HOL-Library.Countable_Set
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.Continuum_Not_Denumerable
HOL-Analysis: theory HOL-Analysis.Abstract_Topology
HOL-Analysis: theory HOL-Analysis.Elementary_Topology
HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
HOL-Analysis: theory HOL-Analysis.Linear_Algebra
HOL-Analysis: theory HOL-Library.Order_Continuity
HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring
HOL-Analysis: theory HOL-Library.Permutations
HOL-Analysis: theory HOL-Library.Extended_Nat
HOL-Analysis: theory HOL-Analysis.Norm_Arith
HOL-Analysis: theory HOL-Analysis.Cartesian_Space
HOL-Analysis: theory HOL-Analysis.Abstract_Limits
HOL-Analysis: theory HOL-Analysis.Convex
HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2
HOL-Analysis: theory HOL-Library.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-Library.Extended_Nonnegative_Real
HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces
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.Function_Topology
HOL-Analysis: theory HOL-Analysis.Tagged_Division
HOL-Analysis: theory HOL-Analysis.Measurable
HOL-Analysis: theory HOL-Analysis.Product_Topology
HOL-Analysis: theory HOL-Analysis.Measure_Space
HOL-Analysis: theory HOL-Analysis.Summation_Tests
HOL-Analysis: theory HOL-Analysis.T1_Spaces
HOL-Analysis: theory HOL-Analysis.Starlike
HOL-Analysis: theory HOL-Analysis.Lindelof_Spaces
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.Caratheodory
HOL-Analysis: theory HOL-Analysis.Continuous_Extension
HOL-Analysis: theory HOL-Analysis.Path_Connected
HOL-Analysis: theory HOL-Analysis.Derivative
HOL-Analysis: theory HOL-Computational_Algebra.Primes
HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series
HOL-Analysis: theory HOL-Analysis.Homotopy
HOL-Analysis: theory HOL-Analysis.Locally
HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Lipschitz
HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
HOL-Analysis: theory HOL-Analysis.Cross3
HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Polytope
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.Complex_Analysis_Basics
HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem
HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
HOL-Analysis: theory HOL-Analysis.Borel_Space
HOL-Analysis: theory HOL-Analysis.Multivariate_Analysis
HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
HOL-Analysis: theory HOL-Analysis.Retracts
HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
HOL-Analysis: theory HOL-Analysis.Regularity
HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
HOL-Analysis: theory HOL-Analysis.Infinite_Products
HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
HOL-Analysis: theory HOL-Analysis.Embed_Measure
HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
HOL-Analysis: theory HOL-Analysis.Bochner_Integration
HOL-Analysis: theory HOL-Analysis.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.Cauchy_Integral_Theorem
HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
HOL-Analysis: theory HOL-Analysis.Integral_Test
HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers
HOL-Analysis: theory HOL-Analysis.Further_Topology
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.Conformal_Mappings
HOL-Analysis: theory HOL-Analysis.Jordan_Curve
HOL-Analysis: theory HOL-Analysis.FPS_Convergence
HOL-Analysis: theory HOL-Analysis.Great_Picard
HOL-Analysis: theory HOL-Analysis.Gamma_Function
HOL-Analysis: theory HOL-Analysis.Riemann_Mapping
HOL-Analysis: theory HOL-Analysis.Winding_Numbers
HOL-Analysis: theory HOL-Analysis.Ball_Volume
HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem
HOL-Analysis: theory HOL-Analysis.Change_Of_Vars
HOL-Analysis: theory HOL-Analysis.Simplex_Content
HOL-Analysis: theory HOL-Analysis.Analysis
Timing HOL-Analysis (6 threads, 446.120s elapsed time, 1939.144s cpu time, 91.332s GC time, factor 4.35)
Timing HOL-Analysis (6 threads, 446.120s elapsed time, 1939.144s cpu time, 91.332s GC time, factor 4.35)
Finished HOL-Analysis (0:08:34 elapsed time, 0:34:41 cpu time, factor 4.04)
Running HOL-Cardinals ...
HOL-Cardinals: theory HOL-Cardinals.Fun_More
HOL-Cardinals: theory HOL-Cardinals.Order_Relation_More
HOL-Cardinals: theory HOL-Cardinals.Order_Union
HOL-Cardinals: theory HOL-Cardinals.Wellorder_Extension
HOL-Cardinals: theory HOL-Cardinals.Wellfounded_More
HOL-Cardinals: theory HOL-Cardinals.Wellorder_Relation
HOL-Cardinals: theory HOL-Cardinals.Wellorder_Embedding
HOL-Cardinals: theory HOL-Cardinals.Wellorder_Constructions
HOL-Cardinals: theory HOL-Cardinals.Cardinal_Order_Relation
HOL-Cardinals: theory HOL-Cardinals.Ordinal_Arithmetic
HOL-Cardinals: theory HOL-Cardinals.Cardinal_Arithmetic
HOL-Cardinals: theory HOL-Cardinals.Cardinals
HOL-Cardinals: theory HOL-Cardinals.Bounded_Set
Timing HOL-Cardinals (6 threads, 7.761s elapsed time, 43.684s cpu time, 1.608s GC time, factor 5.63)
Timing HOL-Cardinals (6 threads, 7.761s elapsed time, 43.684s cpu time, 1.608s GC time, factor 5.63)
Finished HOL-Cardinals (0:00:08 elapsed time, 0:00:44 cpu time, factor 5.02)
Running HOL-Data_Structures ...
HOL-Data_Structures: theory HOL-Data_Structures.Less_False
HOL-Data_Structures: theory HOL-Data_Structures.Array_Specs
HOL-Data_Structures: theory HOL-Data_Structures.Cmp
HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less
HOL-Data_Structures: theory HOL-Data_Structures.Tree2
HOL-Data_Structures: theory HOL-Data_Structures.Tree23
HOL-Data_Structures: theory HOL-Data_Structures.Tree234
HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del
HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del
HOL-Data_Structures: theory HOL-Library.Cancellation
HOL-Data_Structures: theory HOL-Data_Structures.Set_Specs
HOL-Data_Structures: theory HOL-Data_Structures.Trie_Fun
HOL-Data_Structures: theory HOL-Data_Structures.Map_Specs
HOL-Data_Structures: theory HOL-Data_Structures.Tries_Binary
HOL-Data_Structures: theory HOL-Library.Multiset
HOL-Data_Structures: theory HOL-Library.Pattern_Aliases
HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set
HOL-Data_Structures: theory HOL-Data_Structures.Isin2
HOL-Data_Structures: theory HOL-Data_Structures.Lookup2
HOL-Data_Structures: theory HOL-Data_Structures.AA_Set
HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join
HOL-Data_Structures: theory HOL-Data_Structures.RBT
HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set
HOL-Data_Structures: theory HOL-Data_Structures.AA_Map
HOL-Data_Structures: theory HOL-Library.Tree
HOL-Data_Structures: theory HOL-Number_Theory.Fib
HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set
HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set
HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue_Specs
HOL-Data_Structures: theory HOL-Data_Structures.Binomial_Heap
HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap
HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set
HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map
HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map
HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join_RBT
HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map
HOL-Data_Structures: theory HOL-Data_Structures.Trie_Map
HOL-Data_Structures: theory HOL-Data_Structures.Sorting
HOL-Data_Structures: theory HOL-Library.Tree_Real
HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map
HOL-Data_Structures: theory HOL-Data_Structures.Balance
HOL-Data_Structures: theory HOL-Data_Structures.Braun_Tree
HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set
HOL-Data_Structures: theory HOL-Data_Structures.Array_Braun
HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map
HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Map
Timing HOL-Data_Structures (6 threads, 183.877s elapsed time, 1034.672s cpu time, 54.468s GC time, factor 5.63)
Timing HOL-Data_Structures (6 threads, 183.877s elapsed time, 1034.672s cpu time, 54.468s GC time, factor 5.63)
Finished HOL-Data_Structures (0:03:05 elapsed time, 0:17:16 cpu time, factor 5.59)
Running HOL-Hoare_Parallel ...
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Graph
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Com
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Quote_Antiquote
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Com
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Tran
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tran
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Hoare
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Hoare
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Syntax
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Examples
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tactics
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Syntax
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Gar_Coll
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Mul_Gar_Coll
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Examples
HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Hoare_Parallel
Timing HOL-Hoare_Parallel (6 threads, 63.826s elapsed time, 336.292s cpu time, 7.264s GC time, factor 5.27)
Timing HOL-Hoare_Parallel (6 threads, 63.826s elapsed time, 336.292s cpu time, 7.264s GC time, factor 5.27)
Finished HOL-Hoare_Parallel (0:01:04 elapsed time, 0:05:37 cpu time, factor 5.19)
Running HOL-Homology ...
HOL-Homology: theory HOL-Cardinals.Fun_More
HOL-Homology: theory HOL-Cardinals.Order_Relation_More
HOL-Homology: theory HOL-Cardinals.Order_Union
HOL-Homology: theory HOL-Library.Fun_Lexorder
HOL-Homology: theory HOL-Algebra.Congruence
HOL-Homology: theory HOL-Library.Equipollence
HOL-Homology: theory HOL-Library.Groups_Big_Fun
HOL-Homology: theory HOL-Library.More_List
HOL-Homology: theory HOL-Cardinals.Wellfounded_More
HOL-Homology: theory HOL-Cardinals.Wellorder_Relation
HOL-Homology: theory HOL-Library.Poly_Mapping
HOL-Homology: theory HOL-Cardinals.Wellorder_Embedding
HOL-Homology: theory HOL-Cardinals.Wellorder_Constructions
HOL-Homology: theory HOL-Algebra.Order
HOL-Homology: theory HOL-Cardinals.Cardinal_Order_Relation
HOL-Homology: theory HOL-Algebra.Lattice
HOL-Homology: theory HOL-Cardinals.Cardinal_Arithmetic
HOL-Homology: theory HOL-Algebra.Complete_Lattice
HOL-Homology: theory HOL-Algebra.Group
HOL-Homology: theory HOL-Algebra.Coset
HOL-Homology: theory HOL-Algebra.FiniteProduct
HOL-Homology: theory HOL-Algebra.Ring
HOL-Homology: theory HOL-Algebra.Generated_Groups
HOL-Homology: theory HOL-Algebra.Solvable_Groups
HOL-Homology: theory HOL-Algebra.AbelCoset
HOL-Homology: theory HOL-Algebra.Module
HOL-Homology: theory HOL-Algebra.Ideal
HOL-Homology: theory HOL-Algebra.RingHom
HOL-Homology: theory HOL-Algebra.UnivPoly
HOL-Homology: theory HOL-Algebra.Multiplicative_Group
HOL-Homology: theory HOL-Algebra.Elementary_Groups
HOL-Homology: theory HOL-Algebra.Exact_Sequence
HOL-Homology: theory HOL-Algebra.Product_Groups
HOL-Homology: theory HOL-Algebra.Free_Abelian_Groups
HOL-Homology: theory HOL-Homology.Simplices
HOL-Homology: theory HOL-Homology.Homology_Groups
HOL-Homology: theory HOL-Homology.Brouwer_Degree
HOL-Homology: theory HOL-Homology.Invariance_of_Domain
HOL-Homology: theory HOL-Homology.Homology
Timing HOL-Homology (6 threads, 79.315s elapsed time, 374.752s cpu time, 18.088s GC time, factor 4.72)
Timing HOL-Homology (6 threads, 79.315s elapsed time, 374.752s cpu time, 18.088s GC time, factor 4.72)
Finished HOL-Homology (0:01:21 elapsed time, 0:06:16 cpu time, factor 4.65)
Building HOL-Library ...
HOL-Library: theory HOL-Library.AList
HOL-Library: theory HOL-Library.Adhoc_Overloading
HOL-Library: theory HOL-Library.BNF_Axiomatization
HOL-Library: theory HOL-Library.BNF_Corec
HOL-Library: theory HOL-Library.Boolean_Algebra
HOL-Library: theory HOL-Library.Cancellation
HOL-Library: theory HOL-Library.Monad_Syntax
HOL-Library: theory HOL-Library.Case_Converter
HOL-Library: theory HOL-Library.State_Monad
HOL-Library: theory HOL-Library.Char_ord
HOL-Library: theory HOL-Library.Code_Abstract_Nat
HOL-Library: theory HOL-Library.Code_Binary_Nat
HOL-Library: theory HOL-Library.Code_Lazy
HOL-Library: theory HOL-Library.Simps_Case_Conv
HOL-Library: theory HOL-Library.Extended
HOL-Library: theory HOL-Library.Multiset
HOL-Library: theory HOL-Library.Code_Target_Nat
HOL-Library: theory HOL-Library.Code_Prolog
HOL-Library: theory HOL-Library.Code_Target_Int
HOL-Library: theory HOL-Library.Code_Target_Numeral
HOL-Library: theory HOL-Library.DAList
HOL-Library: theory HOL-Library.Code_Test
HOL-Library: theory HOL-Library.Comparator
HOL-Library: theory HOL-Library.Conditional_Parametricity
HOL-Library: theory HOL-Library.Datatype_Records
HOL-Library: theory HOL-Library.Debug
HOL-Library: theory HOL-Library.Disjoint_Sets
HOL-Library: theory HOL-Library.Dlist
HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
HOL-Library: theory HOL-Library.Fun_Lexorder
HOL-Library: theory HOL-Library.FuncSet
HOL-Library: theory HOL-Library.Function_Algebras
HOL-Library: theory HOL-Library.Function_Division
HOL-Library: theory HOL-Library.Groups_Big_Fun
HOL-Library: theory HOL-Library.IArray
HOL-Library: theory HOL-Library.Equipollence
HOL-Library: theory HOL-Library.Infinite_Set
HOL-Library: theory HOL-Library.LaTeXsugar
HOL-Library: theory HOL-Library.Lattice_Constructions
HOL-Library: theory HOL-Library.Lattice_Syntax
HOL-Library: theory HOL-Library.Combine_PER
HOL-Library: theory HOL-Library.Omega_Words_Fun
HOL-Library: theory HOL-Library.Ramsey
HOL-Library: theory HOL-Library.Complete_Partial_Order2
HOL-Library: theory HOL-Library.ListVector
HOL-Library: theory HOL-Library.List_Lexorder
HOL-Library: theory HOL-Library.Mapping
HOL-Library: theory HOL-Library.More_List
HOL-Library: theory HOL-Library.Poly_Mapping
HOL-Library: theory HOL-Library.AList_Mapping
HOL-Library: theory HOL-Library.DAList_Multiset
HOL-Library: theory HOL-Library.Multiset_Order
HOL-Library: theory HOL-Library.Permutation
HOL-Library: theory HOL-Library.Permutations
HOL-Library: theory HOL-Library.Nat_Bijection
HOL-Library: theory HOL-Library.Old_Datatype
HOL-Library: theory HOL-Library.Old_Recdef
HOL-Library: theory HOL-Library.Stream
HOL-Library: theory HOL-Library.Open_State_Syntax
HOL-Library: theory HOL-Library.Option_ord
HOL-Library: theory HOL-Library.Parallel
HOL-Library: theory HOL-Library.Pattern_Aliases
HOL-Library: theory HOL-Library.Perm
HOL-Library: theory HOL-Library.Phantom_Type
HOL-Library: theory HOL-Library.Power_By_Squaring
HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
HOL-Library: theory HOL-Library.Preorder
HOL-Library: theory HOL-Library.Product_Lexorder
HOL-Library: theory HOL-Library.Product_Plus
HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
HOL-Library: theory HOL-Library.Product_Order
HOL-Library: theory HOL-Library.Quotient_Syntax
HOL-Library: theory HOL-Library.Quotient_Type
HOL-Library: theory HOL-Library.Quotient_Option
HOL-Library: theory HOL-Library.Quotient_Product
HOL-Library: theory HOL-Library.Cardinality
HOL-Library: theory HOL-Library.Quotient_Set
HOL-Library: theory HOL-Library.Quotient_Sum
HOL-Library: theory HOL-Library.Finite_Lattice
HOL-Library: theory HOL-Library.RBT_Impl
HOL-Library: theory HOL-Library.Realizers
HOL-Library: theory HOL-Library.Quotient_List
HOL-Library: theory HOL-Library.Reflection
HOL-Library: theory HOL-Library.Refute
HOL-Library: theory HOL-Library.Rewrite
HOL-Library: theory HOL-Library.Set_Algebras
HOL-Library: theory HOL-Library.Sorting_Algorithms
HOL-Library: theory HOL-Library.Stirling
HOL-Library: theory HOL-Library.Numeral_Type
HOL-Library: theory HOL-Library.Sublist
HOL-Library: theory HOL-Library.Transitive_Closure_Table
HOL-Library: theory HOL-Library.Tree
HOL-Library: theory HOL-Library.Uprod
HOL-Library: theory HOL-Library.Type_Length
HOL-Library: theory HOL-Library.Saturated
HOL-Library: theory HOL-Library.While_Combinator
HOL-Library: theory HOL-Library.Prefix_Order
HOL-Library: theory HOL-Library.Subseq_Order
HOL-Library: theory HOL-Library.Z2
HOL-Library: theory HOL-Library.Countable
HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
HOL-Library: theory HOL-Library.BigO
HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
HOL-Library: theory HOL-Library.Diagonal_Subsequence
HOL-Library: theory HOL-Library.Discrete
HOL-Library: theory HOL-Library.Going_To_Filter
HOL-Library: theory HOL-Library.Indicator_Function
HOL-Library: theory HOL-Library.Landau_Symbols
HOL-Library: theory HOL-Library.Tree_Multiset
HOL-Library: theory HOL-Library.Countable_Set
HOL-Library: theory HOL-Library.FSet
HOL-Library: theory HOL-Library.Lattice_Algebras
HOL-Library: theory HOL-Library.Liminf_Limsup
HOL-Library: theory HOL-Library.Countable_Complete_Lattices
HOL-Library: theory HOL-Library.Countable_Set_Type
HOL-Library: theory HOL-Library.Set_Idioms
HOL-Library: theory HOL-Library.Log_Nat
HOL-Library: theory HOL-Library.Lub_Glb
HOL-Library: theory HOL-Library.Multiset_Permutations
HOL-Library: theory HOL-Library.Nonpos_Ints
HOL-Library: theory HOL-Library.OptionalSugar
HOL-Library: theory HOL-Library.Order_Continuity
HOL-Library: theory HOL-Library.Periodic_Fun
HOL-Library: theory HOL-Library.Quadratic_Discriminant
HOL-Library: theory HOL-Library.Sum_of_Squares
HOL-Library: theory HOL-Library.Tree_Real
HOL-Library: theory HOL-Library.Extended_Nat
HOL-Library: theory HOL-Library.Finite_Map
HOL-Library: theory HOL-Library.Extended_Real
HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
HOL-Library: theory HOL-Library.Float
HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
HOL-Library: theory HOL-Library.Library
HOL-Library: theory HOL-Library.RBT
HOL-Library: theory HOL-Library.RBT_Mapping
HOL-Library: theory HOL-Library.RBT_Set
Timing HOL-Library (6 threads, 87.380s elapsed time, 465.632s cpu time, 36.220s GC time, factor 5.33)
Timing HOL-Library (6 threads, 87.380s elapsed time, 465.632s cpu time, 36.220s GC time, factor 5.33)
Finished HOL-Library (0:02:05 elapsed time, 0:09:40 cpu time, factor 4.64)
Building HOL-Auth ...
HOL-Auth: theory HOL-Auth.Message
HOL-Auth: theory HOL-Auth.All_Symmetric
HOL-Auth: theory HOL-Auth.Event
HOL-Auth: theory HOL-Auth.EventSC
HOL-Auth: theory HOL-Auth.Extensions
HOL-Auth: theory HOL-Auth.Public
HOL-Auth: theory HOL-Auth.Shared
HOL-Auth: theory HOL-Auth.Analz
HOL-Auth: theory HOL-Auth.List_Msg
HOL-Auth: theory HOL-Auth.CertifiedEmail
HOL-Auth: theory HOL-Auth.KerberosIV
HOL-Auth: theory HOL-Auth.Guard
HOL-Auth: theory HOL-Auth.GuardK
HOL-Auth: theory HOL-Auth.KerberosIV_Gets
HOL-Auth: theory HOL-Auth.KerberosV
HOL-Auth: theory HOL-Auth.Guard_Public
HOL-Auth: theory HOL-Auth.Kerberos_BAN
HOL-Auth: theory HOL-Auth.Guard_NS_Public
HOL-Auth: theory HOL-Auth.Proto
HOL-Auth: theory HOL-Auth.Kerberos_BAN_Gets
HOL-Auth: theory HOL-Auth.P2
HOL-Auth: theory HOL-Auth.NS_Public
HOL-Auth: theory HOL-Auth.NS_Public_Bad
HOL-Auth: theory HOL-Auth.NS_Shared
HOL-Auth: theory HOL-Auth.OtwayRees
HOL-Auth: theory HOL-Auth.OtwayReesBella
HOL-Auth: theory HOL-Auth.OtwayRees_AN
HOL-Auth: theory HOL-Auth.OtwayRees_Bad
HOL-Auth: theory HOL-Auth.P1
HOL-Auth: theory HOL-Auth.Recur
HOL-Auth: theory HOL-Auth.WooLam
HOL-Auth: theory HOL-Auth.Yahalom
HOL-Auth: theory HOL-Auth.Yahalom2
HOL-Auth: theory HOL-Auth.Yahalom_Bad
HOL-Auth: theory HOL-Auth.ZhouGollmann
HOL-Auth: theory HOL-Auth.Guard_Shared
HOL-Auth: theory HOL-Auth.Smartcard
HOL-Auth: theory HOL-Auth.TLS
HOL-Auth: theory HOL-Auth.Guard_OtwayRees
HOL-Auth: theory HOL-Auth.Auth_Shared
HOL-Auth: theory HOL-Auth.Guard_Yahalom
HOL-Auth: theory HOL-Auth.ShoupRubin
HOL-Auth: theory HOL-Auth.Auth_Guard_Shared
HOL-Auth: theory HOL-Auth.ShoupRubinBella
HOL-Auth: theory HOL-Auth.Auth_Public
HOL-Auth: theory HOL-Auth.Auth_Smartcard
HOL-Auth: theory HOL-Auth.Auth_Guard_Public
Timing HOL-Auth (6 threads, 68.134s elapsed time, 318.164s cpu time, 9.904s GC time, factor 4.67)
Timing HOL-Auth (6 threads, 68.134s elapsed time, 318.164s cpu time, 9.904s GC time, factor 4.67)
Finished HOL-Auth (0:01:25 elapsed time, 0:05:54 cpu time, factor 4.13)
Running HOL-Bali ...
HOL-Bali: theory HOL-Bali.Basis
HOL-Bali: theory HOL-Bali.Name
HOL-Bali: theory HOL-Bali.Table
HOL-Bali: theory HOL-Bali.Type
HOL-Bali: theory HOL-Bali.Value
HOL-Bali: theory HOL-Bali.Term
HOL-Bali: theory HOL-Bali.Decl
HOL-Bali: theory HOL-Bali.TypeRel
HOL-Bali: theory HOL-Bali.DeclConcepts
HOL-Bali: theory HOL-Bali.State
HOL-Bali: theory HOL-Bali.WellType
HOL-Bali: theory HOL-Bali.Conform
HOL-Bali: theory HOL-Bali.Eval
HOL-Bali: theory HOL-Bali.DefiniteAssignment
HOL-Bali: theory HOL-Bali.WellForm
HOL-Bali: theory HOL-Bali.DefiniteAssignmentCorrect
HOL-Bali: theory HOL-Bali.Example
HOL-Bali: theory HOL-Bali.TypeSafe
HOL-Bali: theory HOL-Bali.Evaln
HOL-Bali: theory HOL-Bali.AxSem
HOL-Bali: theory HOL-Bali.Trans
HOL-Bali: theory HOL-Bali.AxCompl
HOL-Bali: theory HOL-Bali.AxSound
HOL-Bali: theory HOL-Bali.AxExample
Timing HOL-Bali (6 threads, 59.100s elapsed time, 223.860s cpu time, 12.212s GC time, factor 3.79)
Timing HOL-Bali (6 threads, 59.100s elapsed time, 223.860s cpu time, 12.212s GC time, factor 3.79)
Finished HOL-Bali (0:01:00 elapsed time, 0:03:45 cpu time, factor 3.71)
Building HOL-Computational_Algebra ...
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Laurent_Series
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra
Timing HOL-Computational_Algebra (6 threads, 49.460s elapsed time, 176.828s cpu time, 7.004s GC time, factor 3.58)
Timing HOL-Computational_Algebra (6 threads, 49.460s elapsed time, 176.828s cpu time, 7.004s GC time, factor 3.58)
Finished HOL-Computational_Algebra (0:01:06 elapsed time, 0:03:32 cpu time, factor 3.18)
Building HOL-Algebra ...
HOL-Algebra: theory HOL-Cardinals.Fun_More
HOL-Algebra: theory HOL-Cardinals.Order_Relation_More
HOL-Algebra: theory HOL-Algebra.Exponent
HOL-Algebra: theory HOL-Cardinals.Order_Union
HOL-Algebra: theory HOL-Algebra.Congruence
HOL-Algebra: theory HOL-Algebra.Cycles
HOL-Algebra: theory HOL-Cardinals.Wellfounded_More
HOL-Algebra: theory HOL-Cardinals.Wellorder_Relation
HOL-Algebra: theory HOL-Cardinals.Wellorder_Embedding
HOL-Algebra: theory HOL-Cardinals.Wellorder_Constructions
HOL-Algebra: theory HOL-Algebra.Order
HOL-Algebra: theory HOL-Cardinals.Cardinal_Order_Relation
HOL-Algebra: theory HOL-Algebra.Lattice
HOL-Algebra: theory HOL-Cardinals.Cardinal_Arithmetic
HOL-Algebra: theory HOL-Algebra.Complete_Lattice
HOL-Algebra: theory HOL-Algebra.Galois_Connection
HOL-Algebra: theory HOL-Algebra.Group
HOL-Algebra: theory HOL-Algebra.Bij
HOL-Algebra: theory HOL-Algebra.Coset
HOL-Algebra: theory HOL-Algebra.FiniteProduct
HOL-Algebra: theory HOL-Algebra.Ring
HOL-Algebra: theory HOL-Algebra.Group_Action
HOL-Algebra: theory HOL-Algebra.Sylow
HOL-Algebra: theory HOL-Algebra.Divisibility
HOL-Algebra: theory HOL-Algebra.Generated_Groups
HOL-Algebra: theory HOL-Algebra.Zassenhaus
HOL-Algebra: theory HOL-Algebra.Solvable_Groups
HOL-Algebra: theory HOL-Algebra.Sym_Groups
HOL-Algebra: theory HOL-Algebra.AbelCoset
HOL-Algebra: theory HOL-Algebra.Module
HOL-Algebra: theory HOL-Algebra.Ideal
HOL-Algebra: theory HOL-Algebra.Ideal_Product
HOL-Algebra: theory HOL-Algebra.RingHom
HOL-Algebra: theory HOL-Algebra.QuotRing
HOL-Algebra: theory HOL-Algebra.UnivPoly
HOL-Algebra: theory HOL-Algebra.IntRing
HOL-Algebra: theory HOL-Algebra.Weak_Morphisms
HOL-Algebra: theory HOL-Algebra.Chinese_Remainder
HOL-Algebra: theory HOL-Algebra.Multiplicative_Group
HOL-Algebra: theory HOL-Algebra.Elementary_Groups
HOL-Algebra: theory HOL-Algebra.Ring_Divisibility
HOL-Algebra: theory HOL-Algebra.Subrings
HOL-Algebra: theory HOL-Algebra.Exact_Sequence
HOL-Algebra: theory HOL-Algebra.Product_Groups
HOL-Algebra: theory HOL-Algebra.Free_Abelian_Groups
HOL-Algebra: theory HOL-Algebra.Embedded_Algebras
HOL-Algebra: theory HOL-Algebra.Generated_Rings
HOL-Algebra: theory HOL-Algebra.Generated_Fields
HOL-Algebra: theory HOL-Algebra.Polynomials
HOL-Algebra: theory HOL-Algebra.Polynomial_Divisibility
HOL-Algebra: theory HOL-Algebra.Finite_Extensions
HOL-Algebra: theory HOL-Algebra.Indexed_Polynomials
HOL-Algebra: theory HOL-Algebra.Algebraic_Closure
HOL-Algebra: theory HOL-Algebra.Algebra
Timing HOL-Algebra (6 threads, 118.762s elapsed time, 560.428s cpu time, 83.936s GC time, factor 4.72)
Timing HOL-Algebra (6 threads, 118.762s elapsed time, 560.428s cpu time, 83.936s GC time, factor 4.72)
Finished HOL-Algebra (0:02:36 elapsed time, 0:10:40 cpu time, factor 4.08)
Running HOL-Corec_Examples ...
HOL-Corec_Examples: theory HOL-Corec_Examples.Iterate_GPV
HOL-Corec_Examples: theory HOL-Corec_Examples.LFilter
HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Processor
HOL-Corec_Examples: theory HOL-Corec_Examples.Simple_Nesting
HOL-Corec_Examples: theory HOL-Corec_Examples.Paper_Examples
HOL-Corec_Examples: theory HOL-Corec_Examples.GPV_Bare_Bones
HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_A
HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_Poly
HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Mono
HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Poly
HOL-Corec_Examples: theory HOL-Corec_Examples.Small_Concrete
HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_B
HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_C
HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Friends
HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_D
HOL-Corec_Examples: theory HOL-Corec_Examples.TLList_Friends
HOL-Corec_Examples: theory HOL-Corec_Examples.Type_Class
Timing HOL-Corec_Examples (6 threads, 153.362s elapsed time, 498.900s cpu time, 67.852s GC time, factor 3.25)
Timing HOL-Corec_Examples (6 threads, 153.362s elapsed time, 498.900s cpu time, 67.852s GC time, factor 3.25)
Finished HOL-Corec_Examples (0:02:35 elapsed time, 0:08:20 cpu time, factor 3.23)
Running HOL-Datatype_Benchmark ...
HOL-Datatype_Benchmark: theory HOL-Datatype_Benchmark.Brackin
HOL-Datatype_Benchmark: theory HOL-Datatype_Benchmark.IsaFoR
HOL-Datatype_Benchmark: theory HOL-Datatype_Benchmark.Misc_N2M
Timing HOL-Datatype_Benchmark (6 threads, 516.028s elapsed time, 2073.984s cpu time, 802.048s GC time, factor 4.02)
Timing HOL-Datatype_Benchmark (6 threads, 516.028s elapsed time, 2073.984s cpu time, 802.048s GC time, factor 4.02)
Finished HOL-Datatype_Benchmark (0:08:37 elapsed time, 0:34:35 cpu time, factor 4.01)
Running HOL-Datatype_Examples ...
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Compat
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lift_BNF
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Milner_Tofte
HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFI
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Process
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Stream_Processor
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Koenig
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lambda_Term
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Codatatype
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Datatype
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Prelim
HOL-Datatype_Examples: theory HOL-Datatype_Examples.DTree
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Gram_Lang
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Parallel_Composition
HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFsetI
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primcorec
HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primrec
Timing HOL-Datatype_Examples (6 threads, 75.004s elapsed time, 326.108s cpu time, 34.848s GC time, factor 4.35)
Timing HOL-Datatype_Examples (6 threads, 75.004s elapsed time, 326.108s cpu time, 34.848s GC time, factor 4.35)
Finished HOL-Datatype_Examples (0:01:16 elapsed time, 0:05:27 cpu time, factor 4.27)
Running HOL-Decision_Procs ...
HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions
HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library
HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order
HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux
HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper
HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List
HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair
HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring
HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order_Ex
HOL-Decision_Procs: theory HOL-Decision_Procs.Ferrack
HOL-Decision_Procs: theory HOL-Decision_Procs.MIR
HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Bounds
HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation
HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Complete
HOL-Decision_Procs: theory HOL-Decision_Procs.Reflective_Field
HOL-Decision_Procs: theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial
HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex
HOL-Decision_Procs: theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff
HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Ex
HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Quickcheck_Ex
HOL-Decision_Procs: theory HOL-Decision_Procs.Decision_Procs
Timing HOL-Decision_Procs (6 threads, 255.662s elapsed time, 1145.148s cpu time, 155.280s GC time, factor 4.48)
Timing HOL-Decision_Procs (6 threads, 255.662s elapsed time, 1145.148s cpu time, 155.280s GC time, factor 4.48)
Finished HOL-Decision_Procs (0:04:18 elapsed time, 0:19:07 cpu time, factor 4.45)
Running HOL-IMP ...
HOL-IMP: theory HOL-IMP.AExp
HOL-IMP: theory HOL-IMP.C_like
HOL-IMP: theory HOL-IMP.Complete_Lattice
HOL-IMP: theory HOL-IMP.OO
HOL-IMP: theory HOL-IMP.Star
HOL-IMP: theory HOL-IMP.Types
HOL-IMP: theory HOL-IMP.ASM
HOL-IMP: theory HOL-IMP.BExp
HOL-IMP: theory HOL-IMP.Com
HOL-IMP: theory HOL-IMP.Procs
HOL-IMP: theory HOL-IMP.ACom
HOL-IMP: theory HOL-IMP.Abs_Int_Tests
HOL-IMP: theory HOL-IMP.Big_Step
HOL-IMP: theory HOL-IMP.Vars
HOL-IMP: theory HOL-IMP.Procs_Dyn_Vars_Dyn
HOL-IMP: theory HOL-IMP.Denotational
HOL-IMP: theory HOL-IMP.Hoare
HOL-IMP: theory HOL-IMP.Sec_Type_Expr
HOL-IMP: theory HOL-IMP.Hoare_Examples
HOL-IMP: theory HOL-IMP.Hoare_Sound_Complete
HOL-IMP: theory HOL-IMP.Hoare_Total_EX
HOL-IMP: theory HOL-IMP.Hoare_Total
HOL-IMP: theory HOL-IMP.Hoare_Total_EX2
HOL-IMP: theory HOL-IMP.VCG
HOL-IMP: theory HOL-IMP.Sec_Typing
HOL-IMP: theory HOL-IMP.VCG_Total_EX
HOL-IMP: theory HOL-IMP.Sec_TypingT
HOL-IMP: theory HOL-IMP.VCG_Total_EX2
HOL-IMP: theory HOL-IMP.Sem_Equiv
HOL-IMP: theory HOL-IMP.Def_Init
HOL-IMP: theory HOL-IMP.Def_Init_Exp
HOL-IMP: theory HOL-IMP.Def_Init_Big
HOL-IMP: theory HOL-IMP.Fold
HOL-IMP: theory HOL-IMP.Live
HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Dyn
HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Stat
HOL-IMP: theory HOL-IMP.Collecting
HOL-IMP: theory HOL-IMP.Compiler
HOL-IMP: theory HOL-IMP.Def_Init_Small
HOL-IMP: theory HOL-IMP.Small_Step
HOL-IMP: theory HOL-IMP.Collecting1
HOL-IMP: theory HOL-IMP.Collecting_Examples
HOL-IMP: theory HOL-IMP.Abs_Int_init
HOL-IMP: theory HOL-IMP.Live_True
HOL-IMP: theory HOL-IMP.Finite_Reachable
HOL-IMP: theory HOL-IMP.Abs_Int0
HOL-IMP: theory HOL-IMP.Poly_Types
HOL-IMP: theory HOL-IMP.Abs_State
HOL-IMP: theory HOL-IMP.Compiler2
HOL-IMP: theory HOL-IMP.Abs_Int1
HOL-IMP: theory HOL-IMP.Abs_Int1_const
HOL-IMP: theory HOL-IMP.Abs_Int1_parity
HOL-IMP: theory HOL-IMP.Abs_Int2
HOL-IMP: theory HOL-IMP.Abs_Int2_ivl
HOL-IMP: theory HOL-IMP.Abs_Int3
Timing HOL-IMP (6 threads, 56.260s elapsed time, 283.156s cpu time, 17.268s GC time, factor 5.03)
Timing HOL-IMP (6 threads, 56.260s elapsed time, 283.156s cpu time, 17.268s GC time, factor 5.03)
Finished HOL-IMP (0:00:58 elapsed time, 0:04:47 cpu time, factor 4.94)
Running HOL-Imperative_HOL ...
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Sorted_List
HOL-Imperative_HOL: theory HOL-Imperative_HOL.List_Sublist
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Array
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Ref
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Subarray
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Linked_Lists
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Overview
HOL-Imperative_HOL: theory HOL-Imperative_HOL.SatChecker
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse
HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL_ex
Timing HOL-Imperative_HOL (6 threads, 35.919s elapsed time, 82.632s cpu time, 2.648s GC time, factor 2.30)
Timing HOL-Imperative_HOL (6 threads, 35.919s elapsed time, 82.632s cpu time, 2.648s GC time, factor 2.30)
Finished HOL-Imperative_HOL (0:00:37 elapsed time, 0:06:03 cpu time, factor 9.70)
Running HOL-Metis_Examples ...
HOL-Metis_Examples: theory HOL-Decision_Procs.Dense_Linear_Order
HOL-Metis_Examples: theory HOL-Metis_Examples.Abstraction
HOL-Metis_Examples: theory HOL-Metis_Examples.Binary_Tree
HOL-Metis_Examples: theory HOL-Metis_Examples.Message
HOL-Metis_Examples: theory HOL-Metis_Examples.Sets
HOL-Metis_Examples: theory HOL-Metis_Examples.Tarski
HOL-Metis_Examples: theory HOL-Metis_Examples.Trans_Closure
HOL-Metis_Examples: theory HOL-Metis_Examples.Type_Encodings
HOL-Metis_Examples: theory HOL-Metis_Examples.Proxies
HOL-Metis_Examples: theory HOL-Metis_Examples.Clausification
HOL-Metis_Examples: theory HOL-Metis_Examples.Big_O
Timing HOL-Metis_Examples (6 threads, 14.938s elapsed time, 65.116s cpu time, 7.800s GC time, factor 4.36)
Timing HOL-Metis_Examples (6 threads, 14.938s elapsed time, 65.116s cpu time, 7.800s GC time, factor 4.36)
Finished HOL-Metis_Examples (0:00:16 elapsed time, 0:01:24 cpu time, factor 5.12)
Running HOL-MicroJava ...
HOL-MicroJava: theory HOL-Eisbach.Eisbach
HOL-MicroJava: theory HOL-MicroJava.Semilat
HOL-MicroJava: theory HOL-MicroJava.Err
HOL-MicroJava: theory HOL-MicroJava.JBasis
HOL-MicroJava: theory HOL-MicroJava.AuxLemmas
HOL-MicroJava: theory HOL-MicroJava.Type
HOL-MicroJava: theory HOL-MicroJava.Listn
HOL-MicroJava: theory HOL-MicroJava.Opt
HOL-MicroJava: theory HOL-MicroJava.Product
HOL-MicroJava: theory HOL-MicroJava.Typing_Framework
HOL-MicroJava: theory HOL-MicroJava.Semilattices
HOL-MicroJava: theory HOL-MicroJava.SemilatAlg
HOL-MicroJava: theory HOL-MicroJava.Kildall
HOL-MicroJava: theory HOL-MicroJava.LBVSpec
HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_err
HOL-MicroJava: theory HOL-MicroJava.Decl
HOL-MicroJava: theory HOL-MicroJava.Value
HOL-MicroJava: theory HOL-MicroJava.LBVComplete
HOL-MicroJava: theory HOL-MicroJava.LBVCorrect
HOL-MicroJava: theory HOL-MicroJava.SystemClasses
HOL-MicroJava: theory HOL-MicroJava.TypeRel
HOL-MicroJava: theory HOL-MicroJava.Abstract_BV
HOL-MicroJava: theory HOL-MicroJava.WellForm
HOL-MicroJava: theory HOL-MicroJava.State
HOL-MicroJava: theory HOL-MicroJava.Term
HOL-MicroJava: theory HOL-MicroJava.Exceptions
HOL-MicroJava: theory HOL-MicroJava.JType
HOL-MicroJava: theory HOL-MicroJava.JVMType
HOL-MicroJava: theory HOL-MicroJava.WellType
HOL-MicroJava: theory HOL-MicroJava.Conform
HOL-MicroJava: theory HOL-MicroJava.Eval
HOL-MicroJava: theory HOL-MicroJava.TypeInf
HOL-MicroJava: theory HOL-MicroJava.JVMState
HOL-MicroJava: theory HOL-MicroJava.JVMInstructions
HOL-MicroJava: theory HOL-MicroJava.JVMExceptions
HOL-MicroJava: theory HOL-MicroJava.JVMExecInstr
HOL-MicroJava: theory HOL-MicroJava.Effect
HOL-MicroJava: theory HOL-MicroJava.JVMExec
HOL-MicroJava: theory HOL-MicroJava.DefsComp
HOL-MicroJava: theory HOL-MicroJava.JVMDefensive
HOL-MicroJava: theory HOL-MicroJava.Index
HOL-MicroJava: theory HOL-MicroJava.JVMListExample
HOL-MicroJava: theory HOL-MicroJava.TranslCompTp
HOL-MicroJava: theory HOL-MicroJava.Example
HOL-MicroJava: theory HOL-MicroJava.JListExample
HOL-MicroJava: theory HOL-MicroJava.JTypeSafe
HOL-MicroJava: theory HOL-MicroJava.TranslComp
HOL-MicroJava: theory HOL-MicroJava.LemmasComp
HOL-MicroJava: theory HOL-MicroJava.CorrComp
HOL-MicroJava: theory HOL-MicroJava.BVSpec
HOL-MicroJava: theory HOL-MicroJava.EffectMono
HOL-MicroJava: theory HOL-MicroJava.Altern
HOL-MicroJava: theory HOL-MicroJava.Correct
HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_JVM
HOL-MicroJava: theory HOL-MicroJava.BVSpecTypeSafe
HOL-MicroJava: theory HOL-MicroJava.JVM
HOL-MicroJava: theory HOL-MicroJava.LBVJVM
HOL-MicroJava: theory HOL-MicroJava.CorrCompTp
HOL-MicroJava: theory HOL-MicroJava.BVNoTypeError
HOL-MicroJava: theory HOL-MicroJava.BVExample
HOL-MicroJava: theory HOL-MicroJava.MicroJava
Timing HOL-MicroJava (6 threads, 63.028s elapsed time, 284.768s cpu time, 9.756s GC time, factor 4.52)
Timing HOL-MicroJava (6 threads, 63.028s elapsed time, 284.768s cpu time, 9.756s GC time, factor 4.52)
Finished HOL-MicroJava (0:01:04 elapsed time, 0:04:46 cpu time, factor 4.43)
Building HOL-Nominal ...
HOL-Nominal: theory HOL-Nominal.Nominal
Timing HOL-Nominal (6 threads, 6.654s elapsed time, 15.144s cpu time, 1.000s GC time, factor 2.28)
Timing HOL-Nominal (6 threads, 6.654s elapsed time, 15.144s cpu time, 1.000s GC time, factor 2.28)
Finished HOL-Nominal (0:00:17 elapsed time, 0:00:35 cpu time, factor 2.06)
Running HOL-Nominal-Examples ...
HOL-Nominal-Examples: theory HOL-Nominal-Examples.CK_Machine
HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR_Takahashi
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class1
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Compile
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Contexts
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Crary
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Fsub
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Height
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lam_Funs
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lambda_mu
HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR
HOL-Nominal-Examples: theory HOL-Nominal-Examples.SN
HOL-Nominal-Examples: theory HOL-Nominal-Examples.LocalWeakening
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Pattern
HOL-Nominal-Examples: theory HOL-Nominal-Examples.SOS
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Standardization
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Support
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Type_Preservation
HOL-Nominal-Examples: theory HOL-Nominal-Examples.W
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2
HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3
HOL-Nominal-Examples: theory HOL-Nominal-Examples.VC_Condition
Timing HOL-Nominal-Examples (6 threads, 230.237s elapsed time, 1078.620s cpu time, 83.292s GC time, factor 4.68)
Timing HOL-Nominal-Examples (6 threads, 230.237s elapsed time, 1078.620s cpu time, 83.292s GC time, factor 4.68)
Finished HOL-Nominal-Examples (0:03:52 elapsed time, 0:18:00 cpu time, factor 4.65)
Building HOL-Nonstandard_Analysis ...
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Free_Ultrafilter
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.StarDef
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperNat
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperDef
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSA
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSComplex
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Star
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLim
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NatStar
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSEQ
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HDeriv
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSeries
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HTranscendental
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLog
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSCA
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hyperreal
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CStar
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CLim
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hypercomplex
HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Nonstandard_Analysis
Timing HOL-Nonstandard_Analysis (6 threads, 6.996s elapsed time, 31.020s cpu time, 1.584s GC time, factor 4.43)
Timing HOL-Nonstandard_Analysis (6 threads, 6.996s elapsed time, 31.020s cpu time, 1.584s GC time, factor 4.43)
Finished HOL-Nonstandard_Analysis (0:00:18 elapsed time, 0:00:54 cpu time, factor 2.88)
Running HOL-Nonstandard_Analysis-Examples ...
HOL-Nonstandard_Analysis-Examples: theory HOL-Nonstandard_Analysis-Examples.NSPrimes
Timing HOL-Nonstandard_Analysis-Examples (6 threads, 1.767s elapsed time, 3.664s cpu time, 0.000s GC time, factor 2.07)
Timing HOL-Nonstandard_Analysis-Examples (6 threads, 1.767s elapsed time, 3.664s cpu time, 0.000s GC time, factor 2.07)
Finished HOL-Nonstandard_Analysis-Examples (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.54)
Building HOL-Number_Theory ...
HOL-Number_Theory: theory HOL-Number_Theory.Cong
HOL-Number_Theory: theory HOL-Algebra.Congruence
HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes
HOL-Number_Theory: theory HOL-Number_Theory.Fib
HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers
HOL-Number_Theory: theory HOL-Algebra.Order
HOL-Number_Theory: theory HOL-Number_Theory.Mod_Exp
HOL-Number_Theory: theory HOL-Number_Theory.Totient
HOL-Number_Theory: theory HOL-Algebra.Lattice
HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice
HOL-Number_Theory: theory HOL-Algebra.Group
HOL-Number_Theory: theory HOL-Algebra.Coset
HOL-Number_Theory: theory HOL-Algebra.FiniteProduct
HOL-Number_Theory: theory HOL-Algebra.Ring
HOL-Number_Theory: theory HOL-Algebra.Generated_Groups
HOL-Number_Theory: theory HOL-Algebra.AbelCoset
HOL-Number_Theory: theory HOL-Algebra.Module
HOL-Number_Theory: theory HOL-Algebra.Ideal
HOL-Number_Theory: theory HOL-Algebra.RingHom
HOL-Number_Theory: theory HOL-Algebra.UnivPoly
HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group
HOL-Number_Theory: theory HOL-Number_Theory.Residues
HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion
HOL-Number_Theory: theory HOL-Number_Theory.Gauss
HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity
HOL-Number_Theory: theory HOL-Number_Theory.Pocklington
HOL-Number_Theory: theory HOL-Number_Theory.Residue_Primitive_Roots
HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory
Timing HOL-Number_Theory (6 threads, 48.777s elapsed time, 238.680s cpu time, 12.736s GC time, factor 4.89)
Timing HOL-Number_Theory (6 threads, 48.777s elapsed time, 238.680s cpu time, 12.736s GC time, factor 4.89)
Finished HOL-Number_Theory (0:01:11 elapsed time, 0:04:46 cpu time, factor 4.00)
Running HOL-Predicate_Compile_Examples ...
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_2
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_3
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_1
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_4
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Quickcheck_Examples
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Tests
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Examples
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Specialisation_Examples
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Code_Prolog_Examples
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Context_Free_Grammar_Example
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Lambda_Example
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.List_Examples
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example_Prolog
HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Reg_Exp_Example
Timing HOL-Predicate_Compile_Examples (6 threads, 49.854s elapsed time, 206.436s cpu time, 15.420s GC time, factor 4.14)
Timing HOL-Predicate_Compile_Examples (6 threads, 49.854s elapsed time, 206.436s cpu time, 15.420s GC time, factor 4.14)
Finished HOL-Predicate_Compile_Examples (0:00:51 elapsed time, 0:06:20 cpu time, factor 7.37)
Building HOL-Probability ...
HOL-Probability: theory HOL-Library.AList
HOL-Probability: theory HOL-Library.Adhoc_Overloading
HOL-Probability: theory HOL-Library.Conditional_Parametricity
HOL-Probability: theory HOL-Library.Lattice_Syntax
HOL-Probability: theory HOL-Library.Mapping
HOL-Probability: theory HOL-Library.Stream
HOL-Probability: theory HOL-Library.Complete_Partial_Order2
HOL-Probability: theory HOL-Library.Monad_Syntax
HOL-Probability: theory HOL-Library.Rewrite
HOL-Probability: theory HOL-Library.Sublist
HOL-Probability: theory HOL-Library.Tree
HOL-Probability: theory HOL-Library.FSet
HOL-Probability: theory HOL-Library.Diagonal_Subsequence
HOL-Probability: theory HOL-Library.Multiset_Permutations
HOL-Probability: theory HOL-Library.AList_Mapping
HOL-Probability: theory HOL-Probability.Discrete_Topology
HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams
HOL-Probability: theory HOL-Probability.Essential_Supremum
HOL-Probability: theory HOL-Probability.Probability_Measure
HOL-Probability: theory HOL-Probability.Stopping_Time
HOL-Probability: theory HOL-Probability.Tree_Space
HOL-Probability: theory HOL-Probability.Conditional_Expectation
HOL-Probability: theory HOL-Probability.Distribution_Functions
HOL-Probability: theory HOL-Probability.Giry_Monad
HOL-Probability: theory HOL-Probability.Weak_Convergence
HOL-Probability: theory HOL-Probability.Helly_Selection
HOL-Probability: theory HOL-Library.Finite_Map
HOL-Probability: theory HOL-Probability.Probability_Mass_Function
HOL-Probability: theory HOL-Probability.Projective_Family
HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
HOL-Probability: theory HOL-Probability.Independent_Family
HOL-Probability: theory HOL-Probability.Stream_Space
HOL-Probability: theory HOL-Probability.PMF_Impl
HOL-Probability: theory HOL-Probability.Random_Permutations
HOL-Probability: theory HOL-Probability.SPMF
HOL-Probability: theory HOL-Probability.Convolution
HOL-Probability: theory HOL-Probability.Information
HOL-Probability: theory HOL-Probability.Distributions
HOL-Probability: theory HOL-Probability.Characteristic_Functions
HOL-Probability: theory HOL-Probability.Sinc_Integral
HOL-Probability: theory HOL-Probability.Levy
HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
HOL-Probability: theory HOL-Probability.Fin_Map
HOL-Probability: theory HOL-Probability.Projective_Limit
HOL-Probability: theory HOL-Probability.Probability
Timing HOL-Probability (6 threads, 66.590s elapsed time, 316.060s cpu time, 18.512s GC time, factor 4.75)
Timing HOL-Probability (6 threads, 66.590s elapsed time, 316.060s cpu time, 18.512s GC time, factor 4.75)
Finished HOL-Probability (0:01:30 elapsed time, 0:06:40 cpu time, factor 4.40)
Running HOL-Probability-ex ...
HOL-Probability-ex: theory HOL-Library.Permutation
HOL-Probability-ex: theory HOL-Probability-ex.Dining_Cryptographers
HOL-Probability-ex: theory HOL-Probability-ex.Measure_Not_CCC
HOL-Probability-ex: theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure
Timing HOL-Probability-ex (6 threads, 7.672s elapsed time, 25.228s cpu time, 0.992s GC time, factor 3.29)
Timing HOL-Probability-ex (6 threads, 7.672s elapsed time, 25.228s cpu time, 0.992s GC time, factor 3.29)
Finished HOL-Probability-ex (0:00:09 elapsed time, 0:00:27 cpu time, factor 2.83)
Building HOL-Proofs ...
HOL-Proofs: theory HOL.Code_Generator
HOL-Proofs: theory HOL.HOL
HOL-Proofs: theory HOL.Argo
HOL-Proofs: theory HOL.Ctr_Sugar
HOL-Proofs: theory HOL.Orderings
HOL-Proofs: theory HOL.SAT
HOL-Proofs: theory HOL.Groups
HOL-Proofs: theory HOL.Lattices
HOL-Proofs: theory HOL.Set
HOL-Proofs: theory HOL.Fun
HOL-Proofs: theory HOL.Typedef
HOL-Proofs: theory HOL.Complete_Lattices
HOL-Proofs: theory HOL.Rings
HOL-Proofs: theory HOL.Inductive
HOL-Proofs: theory HOL.Product_Type
HOL-Proofs: theory HOL.Sum_Type
HOL-Proofs: theory HOL.Complete_Partial_Order
HOL-Proofs: theory HOL.Nat
HOL-Proofs: theory HOL.Fields
HOL-Proofs: theory HOL.Meson
HOL-Proofs: theory HOL.ATP
HOL-Proofs: theory HOL.Metis
HOL-Proofs: theory HOL.Finite_Set
HOL-Proofs: theory HOL.Relation
HOL-Proofs: theory HOL.Transitive_Closure
HOL-Proofs: theory HOL.Wellfounded
HOL-Proofs: theory HOL.Fun_Def_Base
HOL-Proofs: theory HOL.Hilbert_Choice
HOL-Proofs: theory HOL.Wfrec
HOL-Proofs: theory HOL.Order_Relation
HOL-Proofs: theory HOL.BNF_Wellorder_Relation
HOL-Proofs: theory HOL.BNF_Wellorder_Embedding
HOL-Proofs: theory HOL.Zorn
HOL-Proofs: theory HOL.BNF_Wellorder_Constructions
HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation
HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic
HOL-Proofs: theory HOL.BNF_Def
HOL-Proofs: theory HOL.BNF_Composition
HOL-Proofs: theory HOL.Basic_BNFs
HOL-Proofs: theory HOL.BNF_Fixpoint_Base
HOL-Proofs: theory HOL.BNF_Least_Fixpoint
HOL-Proofs: theory HOL.Basic_BNF_LFPs
HOL-Proofs: theory HOL.Transfer
HOL-Proofs: theory HOL.Num
HOL-Proofs: theory HOL.Power
HOL-Proofs: theory HOL.Groups_Big
HOL-Proofs: theory HOL.Equiv_Relations
HOL-Proofs: theory HOL.Lifting
HOL-Proofs: theory HOL.Lifting_Set
HOL-Proofs: theory HOL.Option
HOL-Proofs: theory HOL.Quotient
HOL-Proofs: theory HOL.Extraction
HOL-Proofs: theory HOL.Lattices_Big
HOL-Proofs: theory HOL.Partial_Function
HOL-Proofs: theory HOL.Fun_Def
HOL-Proofs: theory HOL.Int
HOL-Proofs: theory HOL.Euclidean_Division
HOL-Proofs: theory HOL.Parity
HOL-Proofs: theory HOL.Divides
HOL-Proofs: theory HOL.Code_Numeral
HOL-Proofs: theory HOL.Numeral_Simprocs
HOL-Proofs: theory HOL.SMT
HOL-Proofs: theory HOL.Set_Interval
HOL-Proofs: theory HOL.Semiring_Normalization
HOL-Proofs: theory HOL.Groebner_Basis
HOL-Proofs: theory HOL.Conditionally_Complete_Lattices
HOL-Proofs: theory HOL.Filter
HOL-Proofs: theory HOL.Presburger
HOL-Proofs: theory HOL.Sledgehammer
HOL-Proofs: theory HOL.List
HOL-Proofs: theory HOL.Groups_List
HOL-Proofs: theory HOL.Map
HOL-Proofs: theory HOL.Factorial
HOL-Proofs: theory HOL.GCD
HOL-Proofs: theory HOL.Random
HOL-Proofs: theory HOL.Enum
HOL-Proofs: theory HOL.Binomial
HOL-Proofs: theory HOL.String
HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint
HOL-Proofs: theory HOL.Predicate
HOL-Proofs: theory HOL.Typerep
HOL-Proofs: theory HOL.Lazy_Sequence
HOL-Proofs: theory HOL.Limited_Sequence
HOL-Proofs: theory HOL.Code_Evaluation
HOL-Proofs: theory HOL.Quickcheck_Random
HOL-Proofs: theory HOL.Quickcheck_Exhaustive
HOL-Proofs: theory HOL.Quickcheck_Narrowing
HOL-Proofs: theory HOL.Random_Pred
HOL-Proofs: theory HOL.Random_Sequence
HOL-Proofs: theory HOL.Record
HOL-Proofs: theory HOL.Predicate_Compile
HOL-Proofs: theory HOL.Nitpick
HOL-Proofs: theory HOL.Nunchaku
HOL-Proofs: theory Main
HOL-Proofs: theory HOL-Library.Realizers
Timing HOL-Proofs (6 threads, 314.312s elapsed time, 520.564s cpu time, 69.400s GC time, factor 1.66)
Timing HOL-Proofs (6 threads, 314.312s elapsed time, 520.564s cpu time, 69.400s GC time, factor 1.66)
Finished HOL-Proofs (0:06:56 elapsed time, 0:12:19 cpu time, factor 1.78)
Running HOL-Proofs-Extraction ...
HOL-Proofs-Extraction: theory HOL-Library.Cancellation
HOL-Proofs-Extraction: theory HOL-Library.Code_Abstract_Nat
HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Int
HOL-Proofs-Extraction: theory HOL-Library.Open_State_Syntax
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Warshall
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Util
HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Nat
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.QuotRem
HOL-Proofs-Extraction: theory HOL-Library.Multiset
HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Numeral
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Pigeonhole
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman_Extraction
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Greatest_Common_Divisor
HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Factorial_Ring
HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Euclidean_Algorithm
HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Primes
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Euclid
Timing HOL-Proofs-Extraction (6 threads, 88.151s elapsed time, 159.040s cpu time, 9.260s GC time, factor 1.80)
Timing HOL-Proofs-Extraction (6 threads, 88.151s elapsed time, 159.040s cpu time, 9.260s GC time, factor 1.80)
Finished HOL-Proofs-Extraction (0:01:29 elapsed time, 0:02:40 cpu time, factor 1.79)
Running HOL-Proofs-Lambda ...
HOL-Proofs-Lambda: theory HOL-Library.Code_Target_Int
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Commutation
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Lambda
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListOrder
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListApplication
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ParRed
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.LambdaType
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListBeta
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Eta
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.InductTermi
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.NormalForm
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Standardization
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.StrongNorm
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.WeakNorm
Timing HOL-Proofs-Lambda (6 threads, 98.872s elapsed time, 115.256s cpu time, 5.024s GC time, factor 1.17)
Timing HOL-Proofs-Lambda (6 threads, 98.872s elapsed time, 115.256s cpu time, 5.024s GC time, factor 1.17)
Finished HOL-Proofs-Lambda (0:01:40 elapsed time, 0:01:56 cpu time, factor 1.16)
Running HOL-Quickcheck_Benchmark ...
HOL-Quickcheck_Benchmark: theory HOL-Quickcheck_Benchmark.Needham_Schroeder_Base
HOL-Quickcheck_Benchmark: theory HOL-Quickcheck_Benchmark.Find_Unused_Assms_Examples
HOL-Quickcheck_Benchmark: theory HOL-Quickcheck_Benchmark.Needham_Schroeder_Guided_Attacker_Example
HOL-Quickcheck_Benchmark: theory HOL-Quickcheck_Benchmark.Needham_Schroeder_No_Attacker_Example
HOL-Quickcheck_Benchmark: theory HOL-Quickcheck_Benchmark.Needham_Schroeder_Unguided_Attacker_Example
Timing HOL-Quickcheck_Benchmark (6 threads, 312.013s elapsed time, 1509.168s cpu time, 130.768s GC time, factor 4.84)
Timing HOL-Quickcheck_Benchmark (6 threads, 312.013s elapsed time, 1509.168s cpu time, 130.768s GC time, factor 4.84)
Finished HOL-Quickcheck_Benchmark (0:05:13 elapsed time, 0:25:46 cpu time, factor 4.93)
Running HOL-Quickcheck_Examples ...
HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Completeness
HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Interfaces
HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples
HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting
HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Examples
HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting_Example
HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Hotel_Example
HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Narrowing_Examples
Timing HOL-Quickcheck_Examples (6 threads, 74.113s elapsed time, 160.340s cpu time, 5.052s GC time, factor 2.16)
Timing HOL-Quickcheck_Examples (6 threads, 74.113s elapsed time, 160.340s cpu time, 5.052s GC time, factor 2.16)
Finished HOL-Quickcheck_Examples (0:01:15 elapsed time, 0:04:27 cpu time, factor 3.53)
Running HOL-Quotient_Examples ...
HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Int
HOL-Quotient_Examples: theory HOL-Quotient_Examples.DList
HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_FSet
HOL-Quotient_Examples: theory HOL-Quotient_Examples.Int_Pow
HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_DList
HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_FSet
HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Fun
HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Set
HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lifting_Code_Dt_Test
HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Message
HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Rat
Timing HOL-Quotient_Examples (6 threads, 27.620s elapsed time, 44.792s cpu time, 3.032s GC time, factor 1.62)
Timing HOL-Quotient_Examples (6 threads, 27.620s elapsed time, 44.792s cpu time, 3.032s GC time, factor 1.62)
Finished HOL-Quotient_Examples (0:00:29 elapsed time, 0:01:48 cpu time, factor 3.65)
Running HOL-Record_Benchmark ...
HOL-Record_Benchmark: theory HOL-Record_Benchmark.Record_Benchmark
Timing HOL-Record_Benchmark (6 threads, 148.977s elapsed time, 222.452s cpu time, 9.340s GC time, factor 1.49)
Timing HOL-Record_Benchmark (6 threads, 148.977s elapsed time, 222.452s cpu time, 9.340s GC time, factor 1.49)
Finished HOL-Record_Benchmark (0:02:30 elapsed time, 0:03:43 cpu time, factor 1.49)
Running HOL-SET_Protocol ...
HOL-SET_Protocol: theory HOL-SET_Protocol.Message_SET
HOL-SET_Protocol: theory HOL-SET_Protocol.Event_SET
HOL-SET_Protocol: theory HOL-SET_Protocol.Public_SET
HOL-SET_Protocol: theory HOL-SET_Protocol.Cardholder_Registration
HOL-SET_Protocol: theory HOL-SET_Protocol.Merchant_Registration
HOL-SET_Protocol: theory HOL-SET_Protocol.Purchase
HOL-SET_Protocol: theory HOL-SET_Protocol.SET_Protocol
Timing HOL-SET_Protocol (6 threads, 24.433s elapsed time, 109.620s cpu time, 2.276s GC time, factor 4.49)
Timing HOL-SET_Protocol (6 threads, 24.433s elapsed time, 109.620s cpu time, 2.276s GC time, factor 4.49)
Finished HOL-SET_Protocol (0:00:26 elapsed time, 0:01:51 cpu time, factor 4.27)
Running HOL-UNITY ...
HOL-UNITY: theory HOL-UNITY.ListOrder
HOL-UNITY: theory HOL-UNITY.UNITY
HOL-UNITY: theory HOL-UNITY.Constrains
HOL-UNITY: theory HOL-UNITY.Deadlock
HOL-UNITY: theory HOL-UNITY.FP
HOL-UNITY: theory HOL-UNITY.Network
HOL-UNITY: theory HOL-UNITY.WFair
HOL-UNITY: theory HOL-UNITY.SubstAx
HOL-UNITY: theory HOL-UNITY.Token
HOL-UNITY: theory HOL-UNITY.Detects
HOL-UNITY: theory HOL-UNITY.Follows
HOL-UNITY: theory HOL-UNITY.Union
HOL-UNITY: theory HOL-UNITY.Comp
HOL-UNITY: theory HOL-UNITY.Guar
HOL-UNITY: theory HOL-UNITY.Transformers
HOL-UNITY: theory HOL-UNITY.Extend
HOL-UNITY: theory HOL-UNITY.ProgressSets
HOL-UNITY: theory HOL-UNITY.Project
HOL-UNITY: theory HOL-UNITY.Rename
HOL-UNITY: theory HOL-UNITY.Lift_prog
HOL-UNITY: theory HOL-UNITY.ELT
HOL-UNITY: theory HOL-UNITY.PPROD
HOL-UNITY: theory HOL-UNITY.UNITY_Main
HOL-UNITY: theory HOL-UNITY.AllocBase
HOL-UNITY: theory HOL-UNITY.Channel
HOL-UNITY: theory HOL-UNITY.Common
HOL-UNITY: theory HOL-UNITY.Counter
HOL-UNITY: theory HOL-UNITY.Counterc
HOL-UNITY: theory HOL-UNITY.Handshake
HOL-UNITY: theory HOL-UNITY.Lift
HOL-UNITY: theory HOL-UNITY.Alloc
HOL-UNITY: theory HOL-UNITY.AllocImpl
HOL-UNITY: theory HOL-UNITY.Client
HOL-UNITY: theory HOL-UNITY.Mutex
HOL-UNITY: theory HOL-UNITY.NSP_Bad
HOL-UNITY: theory HOL-UNITY.PriorityAux
HOL-UNITY: theory HOL-UNITY.Progress
HOL-UNITY: theory HOL-UNITY.Priority
HOL-UNITY: theory HOL-UNITY.Reach
HOL-UNITY: theory HOL-UNITY.Reachability
HOL-UNITY: theory HOL-UNITY.TimerArray
Timing HOL-UNITY (6 threads, 21.325s elapsed time, 109.976s cpu time, 4.908s GC time, factor 5.16)
Timing HOL-UNITY (6 threads, 21.325s elapsed time, 109.976s cpu time, 4.908s GC time, factor 5.16)
Finished HOL-UNITY (0:00:23 elapsed time, 0:01:51 cpu time, factor 4.85)
Building HOL-Word ...
HOL-Word: theory HOL-Library.Boolean_Algebra
HOL-Word: theory HOL-Library.Phantom_Type
HOL-Word: theory HOL-Library.Z2
HOL-Word: theory HOL-Word.Bits
HOL-Word: theory HOL-Word.Misc_Auxiliary
HOL-Word: theory HOL-Word.Misc_Typedef
HOL-Word: theory HOL-Word.Bits_Int
HOL-Word: theory HOL-Word.Bits_Z2
HOL-Word: theory HOL-Word.Misc_Arithmetic
HOL-Word: theory HOL-Library.Cardinality
HOL-Word: theory HOL-Library.Numeral_Type
HOL-Word: theory HOL-Word.Bit_Comprehension
HOL-Word: theory HOL-Library.Type_Length
HOL-Word: theory HOL-Word.Word
HOL-Word: theory HOL-Word.Word_Bitwise
HOL-Word: theory HOL-Word.More_Word
HOL-Word: theory HOL-Word.Word_Examples
Timing HOL-Word (6 threads, 9.932s elapsed time, 51.780s cpu time, 2.540s GC time, factor 5.21)
Timing HOL-Word (6 threads, 9.932s elapsed time, 51.780s cpu time, 2.540s GC time, factor 5.21)
Finished HOL-Word (0:00:19 elapsed time, 0:01:11 cpu time, factor 3.60)
Running HOL-Word-SMT_Examples ...
HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.Boogie
HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Word_Examples
HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Examples
HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Tests
Timing HOL-Word-SMT_Examples (6 threads, 57.427s elapsed time, 85.476s cpu time, 1.900s GC time, factor 1.49)
Timing HOL-Word-SMT_Examples (6 threads, 57.427s elapsed time, 85.476s cpu time, 1.900s GC time, factor 1.49)
Finished HOL-Word-SMT_Examples (0:00:58 elapsed time, 0:01:29 cpu time, factor 1.53)
Running HOL-ex ...
HOL-ex: theory HOL-ex.Bubblesort
HOL-ex: theory HOL-ex.MergeSort
HOL-ex: theory HOL-ex.Quicksort
HOL-ex: theory HOL-ex.Simps_Case_Conv_Examples
HOL-ex: theory HOL-ex.Conditional_Parametricity_Examples
HOL-ex: theory HOL-ex.Datatype_Record_Examples
HOL-ex: theory HOL-ex.IArray_Examples
HOL-ex: theory HOL-ex.Perm_Fragments
HOL-ex: theory HOL-ex.Code_Lazy_Demo
HOL-ex: theory HOL-ex.Refute_Examples
HOL-ex: theory HOL-ex.Radix_Sort
HOL-ex: theory HOL-ex.Transitive_Closure_Table_Ex
HOL-ex: theory HOL-ex.While_Combinator_Example
HOL-ex: theory HOL-ex.Code_Timing
HOL-ex: theory HOL-ex.Adhoc_Overloading_Examples
HOL-ex: theory HOL-ex.Antiquote
HOL-ex: theory HOL-ex.Arith_Examples
HOL-ex: theory HOL-ex.Birthday_Paradox
HOL-ex: theory HOL-ex.Bit_Lists
HOL-ex: theory HOL-ex.CTL
HOL-ex: theory HOL-ex.Cartouche_Examples
HOL-ex: theory HOL-ex.Case_Product
HOL-ex: theory HOL-ex.Chinese
HOL-ex: theory HOL-ex.Classical
HOL-ex: theory HOL-ex.Coercion_Examples
HOL-ex: theory HOL-ex.Coherent
HOL-ex: theory HOL-ex.Commands
HOL-ex: theory HOL-ex.Computations
HOL-ex: theory HOL-ex.Erdoes_Szekeres
HOL-ex: theory HOL-ex.Executable_Relation
HOL-ex: theory HOL-ex.Execute_Choice
HOL-ex: theory HOL-ex.Functions
HOL-ex: theory HOL-ex.Groebner_Examples
HOL-ex: theory HOL-ex.Guess
HOL-ex: theory HOL-ex.Hebrew
HOL-ex: theory HOL-ex.Hex_Bin_Examples
HOL-ex: theory HOL-ex.Iff_Oracle
HOL-ex: theory HOL-ex.Induction_Schema
HOL-ex: theory HOL-ex.Intuitionistic
HOL-ex: theory HOL-ex.Join_Theory
HOL-ex: theory HOL-ex.Lagrange
HOL-ex: theory HOL-ex.List_to_Set_Comprehension_Examples
HOL-ex: theory HOL-ex.LocaleTest2
HOL-ex: theory HOL-ex.ML
HOL-ex: theory HOL-ex.MonoidGroup
HOL-ex: theory HOL-ex.Multiquote
HOL-ex: theory HOL-ex.NatSum
HOL-ex: theory HOL-ex.PER
HOL-ex: theory HOL-ex.Peano_Axioms
HOL-ex: theory HOL-ex.PresburgerEx
HOL-ex: theory HOL-ex.Primrec
HOL-ex: theory HOL-ex.Records
HOL-ex: theory HOL-ex.Residue_Ring
HOL-ex: theory HOL-ex.Rewrite_Examples
HOL-ex: theory HOL-ex.Seq
HOL-ex: theory HOL-ex.Serbian
HOL-ex: theory HOL-ex.Set_Comprehension_Pointfree_Examples
HOL-ex: theory HOL-ex.Set_Theory
HOL-ex: theory HOL-ex.Simproc_Tests
HOL-ex: theory HOL-ex.Sketch_and_Explore
HOL-ex: theory HOL-ex.Sorting_Algorithms_Examples
HOL-ex: theory HOL-ex.Sudoku
HOL-ex: theory HOL-ex.Tarski
HOL-ex: theory HOL-ex.Termination
HOL-ex: theory HOL-ex.ThreeDivides
HOL-ex: theory HOL-ex.Transfer_Int_Nat
HOL-ex: theory HOL-ex.Tree23
HOL-ex: theory HOL-ex.Unification
HOL-ex: theory HOL-ex.Word_Type
HOL-ex: theory HOL-ex.veriT_Preprocessing
HOL-ex: theory HOL-ex.Transfer_Debug
HOL-ex: theory HOL-ex.Function_Growth
HOL-ex: theory HOL-ex.SOS
HOL-ex: theory HOL-ex.SOS_Cert
HOL-ex: theory HOL-ex.Argo_Examples
HOL-ex: theory HOL-ex.Ballot
HOL-ex: theory HOL-ex.BinEx
HOL-ex: theory HOL-ex.Code_Binary_Nat_examples
HOL-ex: theory HOL-ex.Cubic_Quartic
HOL-ex: theory HOL-ex.Dedekind_Real
HOL-ex: theory HOL-ex.Eval_Examples
HOL-ex: theory HOL-ex.Gauge_Integration
HOL-ex: theory HOL-ex.HarmonicSeries
HOL-ex: theory HOL-ex.Normalization_by_Evaluation
HOL-ex: theory HOL-ex.Parallel_Example
HOL-ex: theory HOL-ex.Pythagoras
HOL-ex: theory HOL-ex.Reflection_Examples
HOL-ex: theory HOL-ex.Sqrt
HOL-ex: theory HOL-ex.Sqrt_Script
HOL-ex: theory HOL-ex.Sum_of_Powers
HOL-ex: theory HOL-ex.Triangular_Numbers
HOL-ex: theory HOL-ex.Meson_Test
HOL-ex: theory HOL-ex.SAT_Examples
Timing HOL-ex (6 threads, 236.748s elapsed time, 1069.604s cpu time, 69.132s GC time, factor 4.52)
Timing HOL-ex (6 threads, 236.748s elapsed time, 1069.604s cpu time, 69.132s GC time, factor 4.52)
Finished HOL-ex (0:03:58 elapsed time, 0:19:31 cpu time, factor 4.90)
Building HOLCF ...
HOLCF: theory HOL-Library.Nat_Bijection
HOLCF: theory HOL-Library.Old_Datatype
HOLCF: theory HOLCF.Porder
HOLCF: theory HOLCF.Pcpo
HOLCF: theory HOL-Library.Countable
HOLCF: theory HOLCF.Cont
HOLCF: theory HOLCF.Adm
HOLCF: theory HOLCF.Discrete
HOLCF: theory HOLCF.Cpodef
HOLCF: theory HOLCF.Fun_Cpo
HOLCF: theory HOLCF.Product_Cpo
HOLCF: theory HOLCF.Cfun
HOLCF: theory HOLCF.Completion
HOLCF: theory HOLCF.Cprod
HOLCF: theory HOLCF.Deflation
HOLCF: theory HOLCF.Fix
HOLCF: theory HOLCF.Sfun
HOLCF: theory HOLCF.Sprod
HOLCF: theory HOLCF.Up
HOLCF: theory HOLCF.Lift
HOLCF: theory HOLCF.One
HOLCF: theory HOLCF.Tr
HOLCF: theory HOLCF.Ssum
HOLCF: theory HOLCF.Fixrec
HOLCF: theory HOLCF.Map_Functions
HOLCF: theory HOLCF.Bifinite
HOLCF: theory HOLCF.Domain_Aux
HOLCF: theory HOLCF.Universal
HOLCF: theory HOLCF.Algebraic
HOLCF: theory HOLCF.Compact_Basis
HOLCF: theory HOLCF.LowerPD
HOLCF: theory HOLCF.UpperPD
HOLCF: theory HOLCF.Representable
HOLCF: theory HOLCF.ConvexPD
HOLCF: theory HOLCF.Domain
HOLCF: theory HOLCF.Powerdomains
HOLCF: theory HOLCF
Timing HOLCF (6 threads, 12.391s elapsed time, 40.428s cpu time, 2.776s GC time, factor 3.26)
Timing HOLCF (6 threads, 12.391s elapsed time, 40.428s cpu time, 2.776s GC time, factor 3.26)
Finished HOLCF (0:00:21 elapsed time, 0:00:58 cpu time, factor 2.72)
Running IOA ...
IOA: theory IOA.Seq
IOA: theory IOA.Asig
IOA: theory IOA.Pred
IOA: theory IOA.Automata
IOA: theory IOA.Sequence
IOA: theory IOA.Traces
IOA: theory IOA.TL
IOA: theory IOA.CompoExecs
IOA: theory IOA.RefMappings
IOA: theory IOA.ShortExecutions
IOA: theory IOA.RefCorrectness
IOA: theory IOA.CompoScheds
IOA: theory IOA.Simulations
IOA: theory IOA.SimCorrectness
IOA: theory IOA.Deadlock
IOA: theory IOA.CompoTraces
IOA: theory IOA.Compositionality
IOA: theory IOA.IOA
IOA: theory IOA.TLS
IOA: theory IOA.LiveIOA
IOA: theory IOA.Abstraction
Timing IOA (6 threads, 7.031s elapsed time, 31.328s cpu time, 1.540s GC time, factor 4.46)
Timing IOA (6 threads, 7.031s elapsed time, 31.328s cpu time, 1.540s GC time, factor 4.46)
Finished IOA (0:00:08 elapsed time, 0:00:32 cpu time, factor 3.93)
Building ZF ...
ZF: theory IFOL
ZF: theory FOL
ZF: theory ZF.ZF_Base
ZF: theory ZF.upair
ZF: theory ZF.pair
ZF: theory ZF.Bool
ZF: theory ZF.equalities
ZF: theory ZF.Fixedpt
ZF: theory ZF.Sum
ZF: theory ZF.func
ZF: theory ZF.Perm
ZF: theory ZF.QPair
ZF: theory ZF.Trancl
ZF: theory ZF.EquivClass
ZF: theory ZF.WF
ZF: theory ZF.Order
ZF: theory ZF.Ordinal
ZF: theory ZF.OrdQuant
ZF: theory ZF.OrderArith
ZF: theory ZF.Nat
ZF: theory ZF.Epsilon
ZF: theory ZF.Inductive
ZF: theory ZF.OrderType
ZF: theory ZF.Finite
ZF: theory ZF.Cardinal
ZF: theory ZF.Univ
ZF: theory ZF.Arith
ZF: theory ZF.QUniv
ZF: theory ZF.Datatype
ZF: theory ZF.ArithSimp
ZF: theory ZF.Int
ZF: theory ZF.CardinalArith
ZF: theory ZF.List
ZF: theory ZF.Bin
ZF: theory ZF.IntDiv
ZF: theory ZF
ZF: theory ZF.AC
ZF: theory ZF.Zorn
ZF: theory ZF.Cardinal_AC
ZF: theory ZF.InfDatatype
ZF: theory ZFC
Timing ZF (6 threads, 12.453s elapsed time, 45.668s cpu time, 3.020s GC time, factor 3.67)
Timing ZF (6 threads, 12.453s elapsed time, 45.668s cpu time, 3.020s GC time, factor 3.67)
Finished ZF (0:00:14 elapsed time, 0:00:49 cpu time, factor 3.45)
Building ZF-Induct ...
ZF-Induct: theory ZF-Induct.Acc
ZF-Induct: theory ZF-Induct.Binary_Trees
ZF-Induct: theory ZF-Induct.Datatypes
ZF-Induct: theory ZF-Induct.FoldSet
ZF-Induct: theory ZF-Induct.ListN
ZF-Induct: theory ZF-Induct.Comb
ZF-Induct: theory ZF-Induct.Mutil
ZF-Induct: theory ZF-Induct.Ntree
ZF-Induct: theory ZF-Induct.Primrec
ZF-Induct: theory ZF-Induct.PropLog
ZF-Induct: theory ZF-Induct.Rmap
ZF-Induct: theory ZF-Induct.Term
ZF-Induct: theory ZF-Induct.Tree_Forest
ZF-Induct: theory ZF-Induct.Multiset
ZF-Induct: theory ZF-Induct.Brouwer
Timing ZF-Induct (6 threads, 3.441s elapsed time, 12.300s cpu time, 0.620s GC time, factor 3.57)
Timing ZF-Induct (6 threads, 3.441s elapsed time, 12.300s cpu time, 0.620s GC time, factor 3.57)
Finished ZF-Induct (0:00:04 elapsed time, 0:00:14 cpu time, factor 3.00)
Running ZF-UNITY ...
ZF-UNITY: theory ZF-UNITY.MultisetSum
ZF-UNITY: theory ZF-UNITY.GenPrefix
ZF-UNITY: theory ZF-UNITY.State
ZF-UNITY: theory ZF-UNITY.UNITY
ZF-UNITY: theory ZF-UNITY.Monotonicity
ZF-UNITY: theory ZF-UNITY.Constrains
ZF-UNITY: theory ZF-UNITY.FP
ZF-UNITY: theory ZF-UNITY.WFair
ZF-UNITY: theory ZF-UNITY.Increasing
ZF-UNITY: theory ZF-UNITY.SubstAx
ZF-UNITY: theory ZF-UNITY.Follows
ZF-UNITY: theory ZF-UNITY.Mutex
ZF-UNITY: theory ZF-UNITY.Union
ZF-UNITY: theory ZF-UNITY.Comp
ZF-UNITY: theory ZF-UNITY.Guar
ZF-UNITY: theory ZF-UNITY.AllocBase
ZF-UNITY: theory ZF-UNITY.ClientImpl
ZF-UNITY: theory ZF-UNITY.Distributor
ZF-UNITY: theory ZF-UNITY.Merge
ZF-UNITY: theory ZF-UNITY.AllocImpl
Timing ZF-UNITY (6 threads, 6.148s elapsed time, 32.404s cpu time, 1.216s GC time, factor 5.27)
Timing ZF-UNITY (6 threads, 6.148s elapsed time, 32.404s cpu time, 1.216s GC time, factor 5.27)
Finished ZF-UNITY (0:00:06 elapsed time, 0:00:32 cpu time, factor 4.89)

=== TIMING ===

Group main: 0:21:58 elapsed time, 1:25:49 cpu time, factor 3.91
Group timing: 1:00:23 elapsed time, 3:57:22 cpu time, factor 3.93
Overall: 1:21:59 elapsed time, 5:15:28 cpu time, factor 3.85
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: SUCCESS