[EnvInject] - Loading node environment variables.
Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow
[isabelle-nightly-slow] $ hg showconfig paths.default
[isabelle-nightly-slow] $ hg pull --rev default
http://isabelle.in.tum.de/repos/isabelle/ pulling from
[isabelle-nightly-slow] $ hg update --clean --rev default
15 files updated, 0 files merged, 0 files removed, 0 files unresolved
[isabelle-nightly-slow] $ hg --config extensions.purge= clean --all
[isabelle-nightly-slow] $ hg log --rev . --template {node}
[isabelle-nightly-slow] $ hg log --rev . --template {rev}
[isabelle-nightly-slow] $ hg log --rev eed58245b57925065d4661e80f2486d5fc823842 --template exists\n
[isabelle-nightly-slow] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg><added>{file_adds|stringify|xmlescape}</added><deleted>{file_dels|stringify|xmlescape}</deleted><files>{files|stringify|xmlescape}</files><parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(eed58245b57925065d4661e80f2486d5fc823842)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
https://bitbucket.org/isa-afp/afp-devel/ pulling from
[afp] $ hg update --clean --rev default
7 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg --config extensions.purge= clean --all
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg log --rev 9ad8f3af760fdc8cfefd77f5796e59c43da8f939 --template exists\n
[afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg><added>{file_adds|stringify|xmlescape}</added><deleted>{file_dels|stringify|xmlescape}</deleted><files>{files|stringify|xmlescape}</files><parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(9ad8f3af760fdc8cfefd77f5796e59c43da8f939)" --encoding UTF-8 --encodingmode replace
[isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins2697361290688556923.sh
+ Admin/jenkins/run_build slow
### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/polyml-test-79534495ee94"
### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/scala-2.12.4"
https://isabelle.in.tum.de/components/polyml-test-79534495ee94.tar.gz" Getting "
Unpacking "/media/data/jenkins/.isabelle/contrib/polyml-test-79534495ee94.tar.gz"
https://isabelle.in.tum.de/components/scala-2.12.4.tar.gz" Getting "
Unpacking "/media/data/jenkins/.isabelle/contrib/scala-2.12.4.tar.gz"
### Building graph browser ...
warning: [options] bootstrap class path not set in conjunction with -source 1.4
warning: [options] source value 1.4 is obsolete and will be removed in a future release
warning: [options] target value 1.4 is obsolete and will be removed in a future release
warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.
Note: Recompile with -Xlint:deprecation for details.
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-79534495ee94/x86_64-linux"
Session HOL/HOL-Library (main timing)
Session AFP/Binomial-Heaps (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/ConcurrentGC (AFP slow)
Session AFP/Finger-Trees (AFP)
Session HOL/HOL-Computational_Algebra (timing)
Session HOL/HOL-Algebra (main timing)
Session HOL/HOL-Decision_Procs (timing)
Session HOL/HOL-Analysis (main timing)
Session HOL/HOL-Number_Theory (timing)
Session AFP/Automatic_Refinement (AFP)
Session HOL/HOL-Imperative_HOL (timing)
Session AFP/Flyspeck-Tame (AFP slow very_slow)
Session HOL/HOL-Word (main timing)
Session AFP/Refine_Monadic (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow)
Session AFP/JinjaThreads (AFP slow)
Session AFP/Affine_Arithmetic (AFP)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/HOL-ODE-Refinement (AFP)
Session AFP/HOL-ODE-Numerics (AFP)
Session AFP/HOL-ODE-Examples (AFP slow)
Session AFP/Lorenz_Approximation (AFP)
Session AFP/Lorenz_C0 (AFP slow)
Timing Pure (1 threads, 0.918s elapsed time, 0.920s cpu time, 0.000s GC time, factor 1.00)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure
Finished Pure (0:00:25 elapsed time, 0:00:25 cpu time, factor 0.98)
HOL: theory HOL.Code_Generator
HOL: theory HOL.Complete_Lattices
HOL: theory HOL.Complete_Partial_Order
HOL: theory HOL.Transitive_Closure
HOL: theory HOL.Hilbert_Choice
HOL: theory HOL.Order_Relation
HOL: theory HOL.BNF_Wellorder_Relation
HOL: theory HOL.BNF_Wellorder_Embedding
HOL: theory HOL.BNF_Wellorder_Constructions
HOL: theory HOL.BNF_Cardinal_Order_Relation
HOL: theory HOL.BNF_Cardinal_Arithmetic
HOL: theory HOL.BNF_Composition
HOL: theory HOL.BNF_Fixpoint_Base
HOL: theory HOL.BNF_Least_Fixpoint
HOL: theory HOL.Basic_BNF_LFPs
HOL: theory HOL.Equiv_Relations
HOL: theory HOL.Partial_Function
HOL: theory HOL.Euclidean_Division
HOL: theory HOL.Numeral_Simprocs
HOL: theory HOL.Semiring_Normalization
HOL: theory HOL.Groebner_Basis
HOL: theory HOL.Conditionally_Complete_Lattices
HOL: theory HOL.BNF_Greatest_Fixpoint
HOL: theory HOL.Limited_Sequence
HOL: theory HOL.Code_Evaluation
HOL: theory HOL.Quickcheck_Random
HOL: theory HOL.Quickcheck_Exhaustive
HOL: theory HOL.Quickcheck_Narrowing
HOL: theory HOL.Random_Sequence
HOL: theory HOL.Predicate_Compile
HOL: theory HOL.Archimedean_Field
HOL: theory HOL.Topological_Spaces
HOL: theory HOL.Real_Vector_Spaces
HOL: theory HOL.Transcendental
Timing HOL (8 threads, 244.305s elapsed time, 767.732s cpu time, 97.804s GC time, factor 3.14)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf
Finished HOL (0:05:40 elapsed time, 0:15:36 cpu time, factor 2.76)
HOL-Library: theory HOL-Library.Adhoc_Overloading
HOL-Library: theory HOL-Library.BNF_Corec
HOL-Library: theory HOL-Library.Bit
HOL-Library: theory HOL-Library.BNF_Axiomatization
HOL-Library: theory HOL-Library.AList
HOL-Library: theory HOL-Library.Cancellation
HOL-Library: theory HOL-Library.Lattice_Syntax
HOL-Library: theory HOL-Library.Boolean_Algebra
HOL-Library: theory HOL-Library.Cardinal_Notations
HOL-Library: theory HOL-Library.Char_ord
HOL-Library: theory HOL-Library.Code_Abstract_Nat
HOL-Library: theory HOL-Library.Code_Prolog
HOL-Library: theory HOL-Library.Code_Char
HOL-Library: theory HOL-Library.Code_Target_Int
HOL-Library: theory HOL-Library.Code_Binary_Nat
HOL-Library: theory HOL-Library.Code_Target_Nat
HOL-Library: theory HOL-Library.Code_Test
HOL-Library: theory HOL-Library.Combine_PER
HOL-Library: theory HOL-Library.Code_Target_Numeral
HOL-Library: theory HOL-Library.Complete_Partial_Order2
HOL-Library: theory HOL-Library.Multiset
HOL-Library: theory HOL-Library.Debug
HOL-Library: theory HOL-Library.Disjoint_Sets
HOL-Library: theory HOL-Library.Dlist
HOL-Library: theory HOL-Library.Fun_Lexorder
HOL-Library: theory HOL-Library.FuncSet
HOL-Library: theory HOL-Library.Function_Algebras
HOL-Library: theory HOL-Library.Function_Division
HOL-Library: theory HOL-Library.Groups_Big_Fun
HOL-Library: theory HOL-Library.IArray
HOL-Library: theory HOL-Library.Infinite_Set
HOL-Library: theory HOL-Library.DAList
HOL-Library: theory HOL-Library.LaTeXsugar
HOL-Library: theory HOL-Library.Lattice_Constructions
HOL-Library: theory HOL-Library.Omega_Words_Fun
HOL-Library: theory HOL-Library.Ramsey
HOL-Library: theory HOL-Library.ListVector
HOL-Library: theory HOL-Library.List_lexord
HOL-Library: theory HOL-Library.Mapping
HOL-Library: theory HOL-Library.Monad_Syntax
HOL-Library: theory HOL-Library.More_List
HOL-Library: theory HOL-Library.State_Monad
HOL-Library: theory HOL-Library.Nat_Bijection
HOL-Library: theory HOL-Library.Old_Datatype
HOL-Library: theory HOL-Library.Stream
HOL-Library: theory HOL-Library.AList_Mapping
HOL-Library: theory HOL-Library.Old_Recdef
HOL-Library: theory HOL-Library.Open_State_Syntax
HOL-Library: theory HOL-Library.Option_ord
HOL-Library: theory HOL-Library.Parallel
HOL-Library: theory HOL-Library.Pattern_Aliases
HOL-Library: theory HOL-Library.Perm
HOL-Library: theory HOL-Library.Phantom_Type
HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
HOL-Library: theory HOL-Library.Preorder
HOL-Library: theory HOL-Library.Product_Lexorder
HOL-Library: theory HOL-Library.Product_Plus
HOL-Library: theory HOL-Library.Quotient_Syntax
HOL-Library: theory HOL-Library.Quotient_Option
HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
HOL-Library: theory HOL-Library.Quotient_Product
HOL-Library: theory HOL-Library.Quotient_Set
HOL-Library: theory HOL-Library.Product_Order
HOL-Library: theory HOL-Library.Quotient_Sum
HOL-Library: theory HOL-Library.Quotient_List
HOL-Library: theory HOL-Library.Quotient_Type
HOL-Library: theory HOL-Library.RBT_Impl
HOL-Library: theory HOL-Library.Cardinality
HOL-Library: theory HOL-Library.Finite_Lattice
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.Simps_Case_Conv
HOL-Library: theory HOL-Library.Extended
HOL-Library: theory HOL-Library.Stirling
HOL-Library: theory HOL-Library.Sublist
HOL-Library: theory HOL-Library.Numeral_Type
HOL-Library: theory HOL-Library.Transitive_Closure_Table
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.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.Prefix_Order
HOL-Library: theory HOL-Library.Subseq_Order
HOL-Library: theory HOL-Library.While_Combinator
HOL-Library: theory HOL-Library.Countable
HOL-Library: theory HOL-Library.BigO
HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
HOL-Library: theory HOL-Library.Diagonal_Subsequence
HOL-Library: theory HOL-Library.Discrete
HOL-Library: theory HOL-Library.Going_To_Filter
HOL-Library: theory HOL-Library.Indicator_Function
HOL-Library: theory HOL-Library.Lattice_Algebras
HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
HOL-Library: theory HOL-Library.Liminf_Limsup
HOL-Library: theory HOL-Library.Log_Nat
HOL-Library: theory HOL-Library.Lub_Glb
HOL-Library: theory HOL-Library.Multiset_Permutations
HOL-Library: theory HOL-Library.Nonpos_Ints
HOL-Library: theory HOL-Library.OptionalSugar
HOL-Library: theory HOL-Library.Countable_Set
HOL-Library: theory HOL-Library.FSet
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.Countable_Complete_Lattices
HOL-Library: theory HOL-Library.Countable_Set_Type
HOL-Library: theory HOL-Library.Tree_Multiset
HOL-Library: theory HOL-Library.Tree_Real
HOL-Library: theory HOL-Library.Order_Continuity
HOL-Library: theory HOL-Library.Extended_Nat
HOL-Library: theory HOL-Library.Finite_Map
HOL-Library: theory HOL-Library.Float
HOL-Library: theory HOL-Library.Extended_Real
HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
HOL-Library: theory HOL-Library.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 (8 threads, 83.709s elapsed time, 541.872s cpu time, 32.780s GC time, factor 6.47)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf
Finished HOL-Library (0:02:34 elapsed time, 0:11:11 cpu time, factor 4.34)
HOL-Analysis: theory HOL-Library.Disjoint_Sets
HOL-Analysis: theory HOL-Library.FuncSet
HOL-Analysis: theory HOL-Library.Infinite_Set
HOL-Analysis: theory HOL-Library.Nat_Bijection
HOL-Analysis: theory HOL-Library.Old_Datatype
HOL-Analysis: theory HOL-Library.Phantom_Type
HOL-Analysis: theory HOL-Library.Product_Plus
HOL-Analysis: theory HOL-Library.Cancellation
HOL-Analysis: theory HOL-Library.Product_Order
HOL-Analysis: theory HOL-Library.Set_Algebras
HOL-Analysis: theory HOL-Analysis.Infinite_Products
HOL-Analysis: theory HOL-Analysis.Inner_Product
HOL-Analysis: theory HOL-Analysis.L2_Norm
HOL-Analysis: theory HOL-Analysis.Operator_Norm
HOL-Analysis: theory HOL-Analysis.Poly_Roots
HOL-Analysis: theory HOL-Library.Discrete
HOL-Analysis: theory HOL-Library.Multiset
HOL-Analysis: theory HOL-Library.Indicator_Function
HOL-Analysis: theory HOL-Library.Liminf_Limsup
HOL-Analysis: theory HOL-Library.Nonpos_Ints
HOL-Analysis: theory HOL-Library.Cardinality
HOL-Analysis: theory HOL-Library.Periodic_Fun
HOL-Analysis: theory HOL-Library.Sum_of_Squares
HOL-Analysis: theory HOL-Library.Countable
HOL-Analysis: theory HOL-Analysis.Product_Vector
HOL-Analysis: theory HOL-Library.Numeral_Type
HOL-Analysis: theory HOL-Analysis.Euclidean_Space
HOL-Analysis: theory HOL-Library.Countable_Set
HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices
HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable
HOL-Analysis: theory HOL-Analysis.Linear_Algebra
HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
HOL-Analysis: theory HOL-Analysis.Norm_Arith
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.Topology_Euclidean_Space
HOL-Analysis: theory HOL-Library.Extended_Real
HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real
HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function
HOL-Analysis: theory HOL-Analysis.Connected
HOL-Analysis: theory HOL-Analysis.Sigma_Algebra
HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits
HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm
HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Tagged_Division
HOL-Analysis: theory HOL-Analysis.Summation_Tests
HOL-Analysis: theory HOL-Analysis.Uniform_Limit
HOL-Analysis: theory HOL-Analysis.Measurable
HOL-Analysis: theory HOL-Analysis.Measure_Space
HOL-Analysis: theory HOL-Analysis.Starlike
HOL-Analysis: theory HOL-Analysis.Caratheodory
HOL-Analysis: theory HOL-Analysis.Continuous_Extension
HOL-Analysis: theory HOL-Analysis.Path_Connected
HOL-Analysis: theory HOL-Computational_Algebra.Primes
HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series
HOL-Analysis: theory HOL-Analysis.Homeomorphism
HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint
HOL-Analysis: theory HOL-Analysis.Derivative
HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
HOL-Analysis: theory HOL-Analysis.Determinants
HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem
HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Polytope
HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
HOL-Analysis: theory HOL-Analysis.Borel_Space
HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
HOL-Analysis: theory HOL-Analysis.Regularity
HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
HOL-Analysis: theory HOL-Analysis.Embed_Measure
HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
HOL-Analysis: theory HOL-Analysis.Bochner_Integration
HOL-Analysis: theory HOL-Analysis.Function_Topology
HOL-Analysis: theory HOL-Analysis.Complete_Measure
HOL-Analysis: theory HOL-Analysis.Radon_Nikodym
HOL-Analysis: theory HOL-Analysis.Set_Integral
HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure
HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum
HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration
HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function
HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
HOL-Analysis: theory HOL-Analysis.Integral_Test
HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics
HOL-Analysis: theory HOL-Analysis.Improper_Integral
HOL-Analysis: theory HOL-Analysis.Interval_Integral
HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution
HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers
HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem
HOL-Analysis: theory HOL-Analysis.Further_Topology
HOL-Analysis: theory HOL-Analysis.Jordan_Curve
HOL-Analysis: theory HOL-Analysis.Conformal_Mappings
HOL-Analysis: theory HOL-Analysis.FPS_Convergence
HOL-Analysis: theory HOL-Analysis.Gamma_Function
HOL-Analysis: theory HOL-Analysis.Great_Picard
HOL-Analysis: theory HOL-Analysis.Riemann_Mapping
HOL-Analysis: theory HOL-Analysis.Winding_Numbers
HOL-Analysis: theory HOL-Analysis.Analysis
Timing HOL-Analysis (8 threads, 388.254s elapsed time, 2070.296s cpu time, 145.280s GC time, factor 5.33)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/outline.pdf
Finished HOL-Analysis (0:09:46 elapsed time, 0:37:29 cpu time, factor 3.84)
Building HOL-Computational_Algebra ...
HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field
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.Computational_Algebra
Timing HOL-Computational_Algebra (8 threads, 50.715s elapsed time, 150.824s cpu time, 5.808s GC time, factor 2.97)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Computational_Algebra
Finished HOL-Computational_Algebra (0:01:19 elapsed time, 0:03:17 cpu time, factor 2.48)
HOL-Word: theory HOL-Library.Phantom_Type
HOL-Word: theory HOL-Library.Boolean_Algebra
HOL-Word: theory HOL-Word.Bits
HOL-Word: theory HOL-Library.Bit
HOL-Word: theory HOL-Word.Misc_Numeric
HOL-Word: theory HOL-Word.Misc_Typedef
HOL-Word: theory HOL-Word.Bit_Representation
HOL-Word: theory HOL-Word.Bits_Bit
HOL-Word: theory HOL-Word.Word_Miscellaneous
HOL-Word: theory HOL-Word.Bits_Int
HOL-Word: theory HOL-Library.Cardinality
HOL-Word: theory HOL-Library.Numeral_Type
HOL-Word: theory HOL-Word.Bit_Comparison
HOL-Word: theory HOL-Word.Bool_List_Representation
HOL-Word: theory HOL-Library.Type_Length
HOL-Word: theory HOL-Word.Word
HOL-Word: theory HOL-Word.WordBitwise
Timing HOL-Word (8 threads, 12.932s elapsed time, 62.324s cpu time, 2.296s GC time, factor 4.82)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf
Finished HOL-Word (0:00:30 elapsed time, 0:01:33 cpu time, factor 3.01)
Building Ordinary_Differential_Equations ...
Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras
Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order
Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int
Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat
Ordinary_Differential_Equations: theory HOL-Word.Misc_Numeric
Ordinary_Differential_Equations: theory HOL-Library.Log_Nat
Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence
Ordinary_Differential_Equations: theory HOL-Word.Bits
Ordinary_Differential_Equations: theory HOL-Word.Bit_Representation
Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat
Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator
Ordinary_Differential_Equations: theory Triangle.Angles
Ordinary_Differential_Equations: theory List-Index.List_Index
Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral
Ordinary_Differential_Equations: theory Triangle.Triangle
Ordinary_Differential_Equations: theory HOL-Word.Bits_Int
Ordinary_Differential_Equations: theory HOL-Word.Bool_List_Representation
Ordinary_Differential_Equations: theory HOL-Library.Float
Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds
Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space
Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis
Timing Ordinary_Differential_Equations (8 threads, 130.589s elapsed time, 589.276s cpu time, 20.092s GC time, factor 4.51)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/outline.pdf
Finished Ordinary_Differential_Equations (0:02:50 elapsed time, 0:11:02 cpu time, factor 3.88)
Building Automatic_Refinement ...
Automatic_Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1
Automatic_Refinement: theory HOL-Library.Infinite_Set
Automatic_Refinement: theory HOL-Library.Option_ord
Automatic_Refinement: theory Automatic_Refinement.Foldi
Automatic_Refinement: theory Automatic_Refinement.Prio_List
Automatic_Refinement: theory HOL-Library.Cancellation
Automatic_Refinement: theory HOL-Eisbach.Eisbach
Automatic_Refinement: theory Automatic_Refinement.Mk_Term_Antiquot
Automatic_Refinement: theory Automatic_Refinement.Mpat_Antiquot
Automatic_Refinement: theory Automatic_Refinement.Refine_Util
Automatic_Refinement: theory HOL-Library.Omega_Words_Fun
Automatic_Refinement: theory HOL-Library.Multiset
Automatic_Refinement: theory Automatic_Refinement.Anti_Unification
Automatic_Refinement: theory Automatic_Refinement.Attr_Comb
Automatic_Refinement: theory Automatic_Refinement.Indep_Vars
Automatic_Refinement: theory Automatic_Refinement.Mk_Record_Simp
Automatic_Refinement: theory Automatic_Refinement.Named_Sorted_Thms
Automatic_Refinement: theory Automatic_Refinement.Tagged_Solver
Automatic_Refinement: theory Automatic_Refinement.Select_Solve
Automatic_Refinement: theory HOL-ex.Quicksort
Automatic_Refinement: theory Automatic_Refinement.Misc
Automatic_Refinement: theory Automatic_Refinement.Digraph_Basic
Automatic_Refinement: theory Automatic_Refinement.Refine_Lib
Automatic_Refinement: theory Automatic_Refinement.Param_Chapter
Automatic_Refinement: theory Automatic_Refinement.Relators
Automatic_Refinement: theory Automatic_Refinement.Param_Tool
Automatic_Refinement: theory Automatic_Refinement.Param_HOL
Automatic_Refinement: theory Automatic_Refinement.Parametricity
Automatic_Refinement: theory Automatic_Refinement.Autoref_Data
Automatic_Refinement: theory Automatic_Refinement.Autoref_Tagging
Automatic_Refinement: theory Automatic_Refinement.Autoref_Phases
Automatic_Refinement: theory Automatic_Refinement.Autoref_Id_Ops
Automatic_Refinement: theory Automatic_Refinement.Autoref_Fix_Rel
Automatic_Refinement: theory Automatic_Refinement.Autoref_Translate
Automatic_Refinement: theory Automatic_Refinement.Autoref_Relator_Interface
Automatic_Refinement: theory Automatic_Refinement.Autoref_Gen_Algo
Automatic_Refinement: theory Automatic_Refinement.Autoref_Chapter
Automatic_Refinement: theory Automatic_Refinement.Autoref_Tool
Automatic_Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL
Automatic_Refinement: theory Automatic_Refinement.Automatic_Refinement
Timing Automatic_Refinement (8 threads, 32.045s elapsed time, 108.936s cpu time, 4.384s GC time, factor 3.40)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Automatic_Refinement
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Automatic_Refinement/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Automatic_Refinement/outline.pdf
Finished Automatic_Refinement (0:00:49 elapsed time, 0:02:20 cpu time, factor 2.82)
Refine_Monadic: theory HOL-Library.Adhoc_Overloading
Refine_Monadic: theory HOL-Library.Bit
Refine_Monadic: theory HOL-Library.Phantom_Type
Refine_Monadic: theory HOL-Library.Boolean_Algebra
Refine_Monadic: theory HOL-Word.Bits
Refine_Monadic: theory HOL-Library.While_Combinator
Refine_Monadic: theory HOL-Word.Misc_Numeric
Refine_Monadic: theory HOL-Word.Misc_Typedef
Refine_Monadic: theory HOL-Word.Bit_Representation
Refine_Monadic: theory HOL-Library.Monad_Syntax
Refine_Monadic: theory Refine_Monadic.Example_Chapter
Refine_Monadic: theory Refine_Monadic.Refine_Chapter
Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover
Refine_Monadic: theory Refine_Monadic.Refine_Misc
Refine_Monadic: theory HOL-Word.Bits_Bit
Refine_Monadic: theory HOL-Word.Word_Miscellaneous
Refine_Monadic: theory HOL-Word.Bits_Int
Refine_Monadic: theory HOL-Library.Cardinality
Refine_Monadic: theory Refine_Monadic.RefineG_Domain
Refine_Monadic: theory Refine_Monadic.RefineG_Transfer
Refine_Monadic: theory Refine_Monadic.RefineG_Assert
Refine_Monadic: theory Refine_Monadic.RefineG_Recursion
Refine_Monadic: theory HOL-Library.Numeral_Type
Refine_Monadic: theory HOL-Word.Bool_List_Representation
Refine_Monadic: theory Refine_Monadic.RefineG_While
Refine_Monadic: theory Refine_Monadic.Refine_Basic
Refine_Monadic: theory Refine_Monadic.Refine_Det
Refine_Monadic: theory HOL-Library.Type_Length
Refine_Monadic: theory HOL-Word.Word
Refine_Monadic: theory Refine_Monadic.Refine_Heuristics
Refine_Monadic: theory Refine_Monadic.Refine_Leof
Refine_Monadic: theory Refine_Monadic.Refine_Pfun
Refine_Monadic: theory Refine_Monadic.Refine_More_Comb
Refine_Monadic: theory Refine_Monadic.Refine_While
Refine_Monadic: theory Refine_Monadic.Refine_Transfer
Refine_Monadic: theory Refine_Monadic.Autoref_Monadic
Refine_Monadic: theory Refine_Monadic.Refine_Automation
Refine_Monadic: theory Refine_Monadic.Refine_Foreach
Refine_Monadic: theory Refine_Monadic.Refine_Monadic
Refine_Monadic: theory Refine_Monadic.Breadth_First_Search
Refine_Monadic: theory Refine_Monadic.WordRefine
Refine_Monadic: theory Refine_Monadic.Examples
Timing Refine_Monadic (8 threads, 30.034s elapsed time, 148.144s cpu time, 7.116s GC time, factor 4.93)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Refine_Monadic
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Refine_Monadic/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Refine_Monadic/outline.pdf
Finished Refine_Monadic (0:00:55 elapsed time, 0:03:13 cpu time, factor 3.50)
AWN: theory AWN.TransitionSystems
AWN: theory AWN.AWN_Invariants
AWN: theory AWN.AWN_SOS_Labels
AWN: theory AWN.OAWN_Invariants
AWN: theory AWN.OAWN_SOS_Labels
AWN: theory AWN.OClosed_Lifting
AWN: theory AWN.OClosed_Transfer
AWN: theory AWN.AWN_Term_Graph
Timing AWN (8 threads, 47.037s elapsed time, 223.520s cpu time, 8.004s GC time, factor 4.75)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf
Finished AWN (0:01:41 elapsed time, 0:05:05 cpu time, factor 3.01)
Deriving: theory Deriving.Comparator
Deriving: theory Deriving.Derive_Manager
Deriving: theory HOL-Word.Misc_Numeric
Deriving: theory HOL-Word.Bits
Deriving: theory Deriving.Generator_Aux
Deriving: theory HOL-Word.Misc_Typedef
Deriving: theory HOL-Word.Bit_Representation
Deriving: theory HOL-Word.Word_Miscellaneous
Deriving: theory Deriving.Countable_Generator
Deriving: theory HOL-Word.Bits_Bit
Deriving: theory Deriving.Equality_Generator
Deriving: theory Deriving.Equality_Instances
Deriving: theory HOL-Word.Bits_Int
Deriving: theory Deriving.Compare
Deriving: theory Deriving.Comparator_Generator
Deriving: theory Deriving.RBT_Comparator_Impl
Deriving: theory Deriving.RBT_Compare_Order_Impl
Deriving: theory Deriving.Compare_Generator
Deriving: theory Deriving.Compare_Instances
Deriving: theory Deriving.Compare_Rat
Deriving: theory Deriving.Compare_Real
Deriving: theory HOL-Word.Bool_List_Representation
Deriving: theory Deriving.Compare_Order_Instances
Deriving: theory Native_Word.More_Bits_Int
Deriving: theory HOL-Word.Word
Deriving: theory Native_Word.Bits_Integer
Deriving: theory Native_Word.Word_Misc
Deriving: theory Native_Word.Uint32
Deriving: theory Collections.HashCode
Deriving: theory Deriving.Hash_Generator
Deriving: theory Deriving.Hash_Instances
Deriving: theory Deriving.Derive
Deriving: theory Deriving.Derive_Examples
Timing Deriving (8 threads, 42.766s elapsed time, 120.460s cpu time, 5.516s GC time, factor 2.82)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Deriving
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Deriving/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Deriving/outline.pdf
Finished Deriving (0:01:13 elapsed time, 0:03:31 cpu time, factor 2.88)
ConcurrentIMP: theory ConcurrentIMP.CIMP_pred
ConcurrentIMP: theory ConcurrentIMP.CIMP_lang
ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg
ConcurrentIMP: theory ConcurrentIMP.CIMP
ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer_ex
ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer_ex
Timing ConcurrentIMP (8 threads, 20.613s elapsed time, 49.796s cpu time, 3.000s GC time, factor 2.42)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf
Finished ConcurrentIMP (0:00:45 elapsed time, 0:01:35 cpu time, factor 2.08)
Timing HOL-ODE (8 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE
Finished HOL-ODE (0:00:02 elapsed time)
Building HOL-ODE-Refinement ...
HOL-ODE-Refinement: theory HOL-Eisbach.Eisbach
HOL-ODE-Refinement: theory HOL-Library.Adhoc_Overloading
HOL-ODE-Refinement: theory Automatic_Refinement.Foldi
HOL-ODE-Refinement: theory Automatic_Refinement.Prio_List
HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1
HOL-ODE-Refinement: theory Deriving.Comparator
HOL-ODE-Refinement: theory Deriving.Derive_Manager
HOL-ODE-Refinement: theory Deriving.Generator_Aux
HOL-ODE-Refinement: theory Automatic_Refinement.Mk_Term_Antiquot
HOL-ODE-Refinement: theory Automatic_Refinement.Mpat_Antiquot
HOL-ODE-Refinement: theory HOL-Library.AList
HOL-ODE-Refinement: theory HOL-Library.Bit
HOL-ODE-Refinement: theory HOL-Library.Boolean_Algebra
HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Util
HOL-ODE-Refinement: theory HOL-Library.Permutation
HOL-ODE-Refinement: theory Deriving.Equality_Generator
HOL-ODE-Refinement: theory HOL-ex.Quicksort
HOL-ODE-Refinement: theory HOL-Library.Char_ord
HOL-ODE-Refinement: theory HOL-Library.Omega_Words_Fun
HOL-ODE-Refinement: theory HOL-Library.Code_Char
HOL-ODE-Refinement: theory Deriving.Equality_Instances
HOL-ODE-Refinement: theory HOL-Library.Mapping
HOL-ODE-Refinement: theory HOL-Library.Monad_Syntax
HOL-ODE-Refinement: theory Automatic_Refinement.Anti_Unification
HOL-ODE-Refinement: theory Automatic_Refinement.Attr_Comb
HOL-ODE-Refinement: theory Automatic_Refinement.Named_Sorted_Thms
HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Data
HOL-ODE-Refinement: theory Automatic_Refinement.Indep_Vars
HOL-ODE-Refinement: theory Automatic_Refinement.Mk_Record_Simp
HOL-ODE-Refinement: theory Automatic_Refinement.Tagged_Solver
HOL-ODE-Refinement: theory Automatic_Refinement.Select_Solve
HOL-ODE-Refinement: theory HOL-Library.Option_ord
HOL-ODE-Refinement: theory Deriving.Compare
HOL-ODE-Refinement: theory Deriving.Comparator_Generator
HOL-ODE-Refinement: theory HOL-Library.Type_Length
HOL-ODE-Refinement: theory HOL-Library.RBT_Impl
HOL-ODE-Refinement: theory HOL-Library.While_Combinator
HOL-ODE-Refinement: theory HOL-Word.Bits_Bit
HOL-ODE-Refinement: theory Automatic_Refinement.Misc
HOL-ODE-Refinement: theory Native_Word.More_Bits_Int
HOL-ODE-Refinement: theory HOL-Word.Word_Miscellaneous
HOL-ODE-Refinement: theory HOL-Word.Misc_Typedef
HOL-ODE-Refinement: theory Deriving.Countable_Generator
HOL-ODE-Refinement: theory Affine_Arithmetic.Optimize_Integer
HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise
HOL-ODE-Refinement: theory Deriving.Compare_Generator
HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Form
HOL-ODE-Refinement: theory HOL-Word.Word
HOL-ODE-Refinement: theory Affine_Arithmetic.Optimize_Float
HOL-ODE-Refinement: theory Deriving.Compare_Instances
HOL-ODE-Refinement: theory Affine_Arithmetic.Float_Real
HOL-ODE-Refinement: theory Affine_Arithmetic.Floatarith_Expression
HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_Vector
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Chapter
HOL-ODE-Refinement: theory Show.Show
HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_2D_Strict
HOL-ODE-Refinement: theory Native_Word.Bits_Integer
HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
HOL-ODE-Refinement: theory Affine_Arithmetic.Polygon
HOL-ODE-Refinement: theory Show.Show_Instances
HOL-ODE-Refinement: theory Affine_Arithmetic.Intersection
HOL-ODE-Refinement: theory Native_Word.Word_Misc
HOL-ODE-Refinement: theory Automatic_Refinement.Digraph_Basic
HOL-ODE-Refinement: theory Collections.SetIterator
HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Lib
HOL-ODE-Refinement: theory Collections.SetIteratorOperations
HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Phases
HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Tagging
HOL-ODE-Refinement: theory Automatic_Refinement.Relators
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Mono_Prover
HOL-ODE-Refinement: theory Automatic_Refinement.Param_Tool
HOL-ODE-Refinement: theory Automatic_Refinement.Param_HOL
HOL-ODE-Refinement: theory Automatic_Refinement.Parametricity
HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Id_Ops
HOL-ODE-Refinement: theory Collections.Assoc_List
HOL-ODE-Refinement: theory Collections.Proper_Iterator
HOL-ODE-Refinement: theory Collections.SetIteratorGA
HOL-ODE-Refinement: theory Collections.Diff_Array
HOL-ODE-Refinement: theory Collections.It_to_It
HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Fix_Rel
HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Translate
HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Relator_Interface
HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Gen_Algo
HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Tool
HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL
HOL-ODE-Refinement: theory Native_Word.Code_Target_Bits_Int
HOL-ODE-Refinement: theory Native_Word.Uint
HOL-ODE-Refinement: theory Collections.Code_Target_ICF
HOL-ODE-Refinement: theory Native_Word.Uint32
HOL-ODE-Refinement: theory Automatic_Refinement.Automatic_Refinement
HOL-ODE-Refinement: theory Collections.Intf_Comp
HOL-ODE-Refinement: theory Collections.Idx_Iterator
HOL-ODE-Refinement: theory Collections.Impl_Array_Stack
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Misc
HOL-ODE-Refinement: theory Collections.HashCode
HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Domain
HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Transfer
HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Assert
HOL-ODE-Refinement: theory Collections.Intf_Hash
HOL-ODE-Refinement: theory Deriving.Hash_Generator
HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Recursion
HOL-ODE-Refinement: theory Refine_Monadic.RefineG_While
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Basic
HOL-ODE-Refinement: theory Collections.Gen_Hash
HOL-ODE-Refinement: theory Deriving.Hash_Instances
HOL-ODE-Refinement: theory Deriving.Derive
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Det
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Heuristics
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Leof
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Pfun
HOL-ODE-Refinement: theory Refine_Monadic.Refine_More_Comb
HOL-ODE-Refinement: theory Refine_Monadic.Refine_While
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Transfer
HOL-ODE-Refinement: theory Refine_Monadic.Autoref_Monadic
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Automation
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Foreach
HOL-ODE-Refinement: theory Refine_Monadic.Refine_Monadic
HOL-ODE-Refinement: theory Collections.Gen_Iterator
HOL-ODE-Refinement: theory Collections.Intf_Map
HOL-ODE-Refinement: theory Collections.Intf_Set
HOL-ODE-Refinement: theory Collections.Impl_Cfun_Set
HOL-ODE-Refinement: theory Collections.Iterator
HOL-ODE-Refinement: theory Collections.Array_Iterator
HOL-ODE-Refinement: theory Collections.Gen_Map
HOL-ODE-Refinement: theory Collections.Gen_Map2Set
HOL-ODE-Refinement: theory Collections.Gen_Set
HOL-ODE-Refinement: theory Collections.Impl_Bit_Set
HOL-ODE-Refinement: theory Collections.Impl_List_Set
HOL-ODE-Refinement: theory Collections.Impl_Array_Map
HOL-ODE-Refinement: theory Collections.Impl_List_Map
HOL-ODE-Refinement: theory Collections.Impl_Uv_Set
HOL-ODE-Refinement: theory Collections.Impl_Array_Hash_Map
HOL-ODE-Refinement: theory HOL-Library.RBT
HOL-ODE-Refinement: theory Collections.RBT_add
HOL-ODE-Refinement: theory HOL-Library.RBT_Mapping
HOL-ODE-Refinement: theory Affine_Arithmetic.Straight_Line_Program
HOL-ODE-Refinement: theory Collections.Impl_RBT_Map
HOL-ODE-Refinement: theory HOL-ODE-Refinement.GenCF_No_Comp
HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Approximation
HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Dflt_No_Comp
HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Misc
HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Folds
HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_String
HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Code
HOL-ODE-Refinement: theory HOL-ODE-Refinement.Weak_Set
HOL-ODE-Refinement: theory Affine_Arithmetic.Print
HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Affine_Approximation
HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Ineqs
HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Inter
HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Arithmetic
Timing HOL-ODE-Refinement (8 threads, 296.234s elapsed time, 1643.644s cpu time, 210.544s GC time, factor 5.55)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Refinement
Finished HOL-ODE-Refinement (0:06:05 elapsed time, 0:31:06 cpu time, factor 5.11)
HOL-ODE-Numerics: theory Collections.ICF_Tools
HOL-ODE-Numerics: theory HOL-Library.Parallel
HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
HOL-ODE-Numerics: theory Collections.Ord_Code_Preproc
HOL-ODE-Numerics: theory Collections.Locale_Code
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
Timing HOL-ODE-Numerics (8 threads, 1501.528s elapsed time, 3263.356s cpu time, 316.956s GC time, factor 2.17)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Numerics
Finished HOL-ODE-Numerics (0:26:51 elapsed time, 0:58:15 cpu time, factor 2.17)
Building Lorenz_Approximation ...
Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
Timing Lorenz_Approximation (8 threads, 317.836s elapsed time, 662.952s cpu time, 60.672s GC time, factor 2.09)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Lorenz_Approximation
Finished Lorenz_Approximation (0:06:04 elapsed time, 0:12:34 cpu time, factor 2.07)
Word_Lib: theory HOL-Library.Sublist
Word_Lib: theory Word_Lib.Signed_Words
Word_Lib: theory Word_Lib.Hex_Words
Word_Lib: theory Word_Lib.HOL_Lemmas
Word_Lib: theory Word_Lib.Enumeration
Word_Lib: theory Word_Lib.More_Divides
Word_Lib: theory Word_Lib.Norm_Words
Word_Lib: theory Word_Lib.WordBitwise_Signed
Word_Lib: theory Word_Lib.Word_Syntax
Word_Lib: theory Word_Lib.Word_Lib
Word_Lib: theory Word_Lib.Word_Enum
Word_Lib: theory Word_Lib.Aligned
Word_Lib: theory HOL-Library.Prefix_Order
Word_Lib: theory Word_Lib.Word_Setup_32
Word_Lib: theory Word_Lib.Word_Setup_64
Word_Lib: theory Word_Lib.Word_Lemmas
Word_Lib: theory Word_Lib.Word_Lemmas_32
Word_Lib: theory Word_Lib.Word_Lemmas_64
Timing Word_Lib (8 threads, 71.834s elapsed time, 179.172s cpu time, 4.700s GC time, factor 2.49)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf
Finished Word_Lib (0:01:29 elapsed time, 0:03:27 cpu time, factor 2.32)
IP_Addresses: theory HOL-Eisbach.Eisbach
IP_Addresses: theory HOL-Library.Cancellation
IP_Addresses: theory HOL-Library.Infinite_Set
IP_Addresses: theory HOL-Library.Option_ord
IP_Addresses: theory IP_Addresses.NumberWang_IPv6
IP_Addresses: theory IP_Addresses.Word_More
IP_Addresses: theory IP_Addresses.NumberWang_IPv4
IP_Addresses: theory HOL-Library.Multiset
IP_Addresses: theory HOL-ex.Quicksort
IP_Addresses: theory Automatic_Refinement.Misc
IP_Addresses: theory HOL-Library.Code_Abstract_Nat
IP_Addresses: theory HOL-Library.Product_Lexorder
IP_Addresses: theory IP_Addresses.Hs_Compat
IP_Addresses: theory IP_Addresses.Word_Next
IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
IP_Addresses: theory HOL-Library.Code_Target_Nat
IP_Addresses: theory IP_Addresses.WordInterval
IP_Addresses: theory IP_Addresses.Lib_List_toString
IP_Addresses: theory IP_Addresses.Lib_Word_toString
IP_Addresses: theory IP_Addresses.IP_Address
IP_Addresses: theory IP_Addresses.WordInterval_Sorted
IP_Addresses: theory IP_Addresses.IPv4
IP_Addresses: theory IP_Addresses.IPv6
IP_Addresses: theory IP_Addresses.Prefix_Match
IP_Addresses: theory IP_Addresses.CIDR_Split
IP_Addresses: theory IP_Addresses.IP_Address_Parser
IP_Addresses: theory IP_Addresses.IP_Address_toString
IP_Addresses: theory IP_Addresses.Prefix_Match_toString
Timing IP_Addresses (8 threads, 312.089s elapsed time, 903.964s cpu time, 57.728s GC time, factor 2.90)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf
Finished IP_Addresses (0:05:54 elapsed time, 0:16:36 cpu time, factor 2.81)
Simple_Firewall: theory HOL-Library.Char_ord
Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
Simple_Firewall: theory Simple_Firewall.GroupF
Simple_Firewall: theory Simple_Firewall.List_Product_More
Simple_Firewall: theory Simple_Firewall.Option_Helpers
Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
Simple_Firewall: theory Simple_Firewall.Iface
Simple_Firewall: theory Simple_Firewall.L4_Protocol
Simple_Firewall: theory Simple_Firewall.Simple_Packet
Simple_Firewall: theory Simple_Firewall.Primitives_toString
Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
Simple_Firewall: theory Simple_Firewall.SimpleFw_toString
Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
Simple_Firewall: theory Simple_Firewall.Shadowed
Simple_Firewall: theory Simple_Firewall.Service_Matrix
Timing Simple_Firewall (8 threads, 24.885s elapsed time, 95.264s cpu time, 4.772s GC time, factor 3.83)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf
Finished Simple_Firewall (0:00:52 elapsed time, 0:02:31 cpu time, factor 2.88)
Routing: theory HOL-Library.Adhoc_Overloading
Routing: theory Routing.Linorder_Helper
Routing: theory HOL-Library.Monad_Syntax
Routing: theory Routing.Routing_Table
Routing: theory Routing.IpRoute_Parser
Routing: theory Routing.Linux_Router
Timing Routing (8 threads, 11.020s elapsed time, 33.572s cpu time, 1.120s GC time, factor 3.05)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf
Finished Routing (0:00:29 elapsed time, 0:01:04 cpu time, factor 2.18)
Building Iptables_Semantics ...
Iptables_Semantics: theory HOL-Library.Code_Target_Int
Iptables_Semantics: theory HOL-Library.LaTeXsugar
Iptables_Semantics: theory Native_Word.More_Bits_Int
Iptables_Semantics: theory HOL-Library.Code_Char
Iptables_Semantics: theory Iptables_Semantics.List_Misc
Iptables_Semantics: theory Iptables_Semantics.Negation_Type
Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
Iptables_Semantics: theory Native_Word.Bits_Integer
Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int
Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
Iptables_Semantics: theory Iptables_Semantics.Ternary
Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
Iptables_Semantics: theory Iptables_Semantics.IpAddresses
Iptables_Semantics: theory Iptables_Semantics.Word_Upto
Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
Iptables_Semantics: theory Iptables_Semantics.Ports
Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
Iptables_Semantics: theory Iptables_Semantics.Semantics
Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
Iptables_Semantics: theory Iptables_Semantics.Matching
Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
Iptables_Semantics: theory Iptables_Semantics.Optimizing
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
Iptables_Semantics: theory Iptables_Semantics.Ipassmt
Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
Iptables_Semantics: theory Iptables_Semantics.No_Spoof
Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
Iptables_Semantics: theory Iptables_Semantics.Transform
Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
Iptables_Semantics: theory Iptables_Semantics.Code_Interface
Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Parser
Iptables_Semantics: theory Iptables_Semantics.Documentation
Iptables_Semantics: theory Iptables_Semantics.Code_haskell
Timing Iptables_Semantics (8 threads, 180.093s elapsed time, 708.020s cpu time, 62.368s GC time, factor 3.93)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf
Finished Iptables_Semantics (0:04:06 elapsed time, 0:14:49 cpu time, factor 3.60)
Building Iptables_Semantics_Examples ...
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation
Timing Iptables_Semantics_Examples (8 threads, 270.073s elapsed time, 1835.796s cpu time, 189.256s GC time, factor 6.80)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf
Finished Iptables_Semantics_Examples (0:05:06 elapsed time, 0:31:45 cpu time, factor 6.23)
HOL-Algebra: theory HOL-Algebra.Exponent
HOL-Algebra: theory HOL-Algebra.Congruence
HOL-Algebra: theory HOL-Algebra.Order
HOL-Algebra: theory HOL-Algebra.Lattice
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.Sylow
HOL-Algebra: theory HOL-Algebra.Divisibility
HOL-Algebra: theory HOL-Algebra.AbelCoset
HOL-Algebra: theory HOL-Algebra.Module
HOL-Algebra: theory HOL-Algebra.More_Group
HOL-Algebra: theory HOL-Algebra.More_Ring
HOL-Algebra: theory HOL-Algebra.More_Finite_Product
HOL-Algebra: theory HOL-Algebra.Ideal
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.Multiplicative_Group
Timing HOL-Algebra (8 threads, 75.686s elapsed time, 235.208s cpu time, 12.576s GC time, factor 3.11)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Algebra
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Algebra/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Algebra/outline.pdf
Finished HOL-Algebra (0:02:21 elapsed time, 0:05:29 cpu time, factor 2.32)
Building HOL-Number_Theory ...
HOL-Number_Theory: theory HOL-Number_Theory.Cong
HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers
HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes
HOL-Number_Theory: theory HOL-Number_Theory.Fib
HOL-Number_Theory: theory HOL-Algebra.Congruence
HOL-Number_Theory: theory HOL-Algebra.Order
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.AbelCoset
HOL-Number_Theory: theory HOL-Algebra.Module
HOL-Number_Theory: theory HOL-Algebra.More_Group
HOL-Number_Theory: theory HOL-Algebra.More_Ring
HOL-Number_Theory: theory HOL-Algebra.More_Finite_Product
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.Pocklington
HOL-Number_Theory: theory HOL-Number_Theory.Gauss
HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity
HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory
Timing HOL-Number_Theory (8 threads, 91.074s elapsed time, 297.168s cpu time, 13.088s GC time, factor 3.26)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Number_Theory
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Number_Theory/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Number_Theory/outline.pdf
Finished HOL-Number_Theory (0:02:25 elapsed time, 0:06:17 cpu time, factor 2.59)
Running Iptables_Semantics_Examples_Big ...
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large
Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Iptables_Semantics_Examples_Big FAILED
(see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.7.1_x86_64-linux/log/Iptables_Semantics_Examples_Big)
((char list \<times> char list) list \<times>
(char list \<times> char list) list) \<times>
(char list \<times> char list) list \<times>
(char list \<times> char list) list"
"[''distinct: passed'', ''ipassmt_sanity_nowildcards: passed'',
''ipassmt_sanity_defined (interfaces defined in the ruleset are also in ipassmt): passed'',
''ipassmt_sanity_disjoint (no zone-spanning interfaces): fail: [(eth1.110,eth1.1024), (eth1.1024,eth1.110)]'',
''ipassmt_sanity_disjoint excluding UNIV interfaces: fail: [(eth1.110,eth1.1024), (eth1.1024,eth1.110)]'',
''ipassmt_sanity_complete: the following is not covered: {188.95.232.192 .. 188.95.232.223}'',
''ipassmt_sanity_complete excluding UNIV interfaces: the following is not covered: {188.95.232.192 .. 188.95.232.223}'']"
"[''{0.0.0.0 .. 255.255.255.255}'']"
"[''{192.168.16.0 .. 192.168.16.255} u {192.168.134.0 .. 192.168.134.255}'',
''{0.0.0.0 .. 127.0.0.0} u {127.0.0.2 .. 192.168.15.255} u {192.168.17.0 .. 192.168.133.255} u {192.168.135.0 .. 255.255.255.255}'',
Simplified term (3077.478 seconds)
checked sanity with sanity_wf_ruleset (2145.255 seconds)
Defining constant `net_fw_1_def'
Defining constant `net_fw_1_INPUT_default_policy_def'
Defining constant `net_fw_1_FORWARD_default_policy_def'
Defining constant `net_fw_1_OUTPUT_default_policy_def'
loading file /media/data/jenkins/workspace/isabelle-nightly-slow/afp/thys/Iptables_Semantics/Examples/TUM_Net_Firewall/iptables-save-2015-05-15_14-14-46_cheating
Loaded 4903 lines of the filter table
unfolding (this may take a while) ...
checked sanity with sanity_wf_ruleset (642.498 seconds)
Defining constant `net_fw_def'
Defining constant `net_fw_INPUT_default_policy_def'
Defining constant `net_fw_FORWARD_default_policy_def'
Defining constant `net_fw_OUTPUT_default_policy_def'
loading file /media/data/jenkins/workspace/isabelle-nightly-slow/afp/thys/Iptables_Semantics/Examples/IPPartEval/TUM_Net/iptables-save-2015-09-03_15-56-50
Loaded 5038 lines of the filter table
unfolding (this may take a while) ...
Flyspeck-Tame: theory Flyspeck-Tame.ListAux
Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order
Flyspeck-Tame: theory Flyspeck-Tame.RTranCl
Flyspeck-Tame: theory HOL-Library.AList
Flyspeck-Tame: theory HOL-Library.While_Combinator
Flyspeck-Tame: theory HOL-Library.Code_Target_Int
Flyspeck-Tame: theory HOL-Library.IArray
Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat
Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso
Flyspeck-Tame: theory HOL-Library.Code_Target_Nat
Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral
Flyspeck-Tame: theory Flyspeck-Tame.Arch
Flyspeck-Tame: theory Flyspeck-Tame.Worklist
Flyspeck-Tame: theory Flyspeck-Tame.ListSum
Flyspeck-Tame: theory Flyspeck-Tame.Rotation
Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax
Flyspeck-Tame: theory Flyspeck-Tame.Graph
Flyspeck-Tame: theory Flyspeck-Tame.Maps
Flyspeck-Tame: theory Trie.Trie
Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision
Flyspeck-Tame: theory Flyspeck-Tame.GraphProps
Flyspeck-Tame: theory Flyspeck-Tame.Tame
Flyspeck-Tame: theory Trie.Tries
Flyspeck-Tame: theory Flyspeck-Tame.Enumerator
Flyspeck-Tame: theory Flyspeck-Tame.TameProps
Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps
Flyspeck-Tame: theory Flyspeck-Tame.Plane
Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps
Flyspeck-Tame: theory Flyspeck-Tame.Plane1
Flyspeck-Tame: theory Flyspeck-Tame.Generator
Flyspeck-Tame: theory Flyspeck-Tame.TameEnum
Flyspeck-Tame: theory Flyspeck-Tame.Invariants
Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux
Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps
Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps
Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props
Flyspeck-Tame: theory Flyspeck-Tame.LowerBound
Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps
Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps
Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps
Flyspeck-Tame: theory Flyspeck-Tame.ArchComp
Flyspeck-Tame: theory Flyspeck-Tame.Completeness
Timing Flyspeck-Tame (8 threads, 29901.064s elapsed time, 46026.416s cpu time, 1647.824s GC time, factor 1.54)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf
Finished Flyspeck-Tame (8:18:31 elapsed time, 12:47:20 cpu time, factor 1.54)
AODV: theory AODV.Aodv_Message
AODV: theory AODV.A_Aodv_Message
AODV: theory AODV.B_Aodv_Message
AODV: theory AODV.C_Aodv_Message
AODV: theory AODV.D_Aodv_Message
AODV: theory AODV.E_Aodv_Message
AODV: theory AODV.Aodv_Predicates
AODV: theory AODV.Loop_Freedom
AODV: theory AODV.Quality_Increases
AODV: theory AODV.Seq_Invariants
AODV: theory AODV.Global_Invariants
AODV: theory AODV.Aodv_Loop_Freedom
AODV: theory AODV.B_Aodv_Predicates
AODV: theory AODV.B_Loop_Freedom
AODV: theory AODV.B_Quality_Increases
AODV: theory AODV.B_Seq_Invariants
AODV: theory AODV.B_Global_Invariants
AODV: theory AODV.B_Aodv_Loop_Freedom
AODV: theory AODV.C_Aodv_Predicates
AODV: theory AODV.C_Loop_Freedom
AODV: theory AODV.C_Quality_Increases
AODV: theory AODV.C_Seq_Invariants
AODV: theory AODV.A_Aodv_Predicates
AODV: theory AODV.C_Global_Invariants
AODV: theory AODV.A_Loop_Freedom
AODV: theory AODV.A_Quality_Increases
AODV: theory AODV.A_Seq_Invariants
AODV: theory AODV.E_Aodv_Predicates
AODV: theory AODV.E_Loop_Freedom
AODV: theory AODV.E_Quality_Increases
AODV: theory AODV.E_Seq_Invariants
AODV: theory AODV.A_Global_Invariants
AODV: theory AODV.C_Aodv_Loop_Freedom
AODV: theory AODV.E_Global_Invariants
AODV: theory AODV.A_Aodv_Loop_Freedom
AODV: theory AODV.E_Aodv_Loop_Freedom
AODV: theory AODV.D_Aodv_Predicates
AODV: theory AODV.D_Loop_Freedom
AODV: theory AODV.D_Quality_Increases
AODV: theory AODV.D_Seq_Invariants
AODV: theory AODV.D_Global_Invariants
AODV: theory AODV.D_Aodv_Loop_Freedom
Timing AODV (8 threads, 8923.910s elapsed time, 44752.256s cpu time, 4116.604s GC time, factor 5.01)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/outline.pdf
Finished AODV (2:28:57 elapsed time, 12:26:11 cpu time, factor 5.01)
ConcurrentGC: theory ConcurrentGC.Model
ConcurrentGC: theory ConcurrentGC.Tactics
ConcurrentGC: theory ConcurrentGC.Proofs_basis
ConcurrentGC: theory ConcurrentGC.TSO
ConcurrentGC: theory ConcurrentGC.Handshakes
ConcurrentGC: theory ConcurrentGC.MarkObject
ConcurrentGC: theory ConcurrentGC.StrongTricolour
ConcurrentGC: theory ConcurrentGC.Proofs
ConcurrentGC: theory ConcurrentGC.Concrete_heap
ConcurrentGC: theory ConcurrentGC.Concrete
Timing ConcurrentGC (8 threads, 7658.812s elapsed time, 26003.264s cpu time, 1775.076s GC time, factor 3.40)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf
Finished ConcurrentGC (2:07:43 elapsed time, 7:13:29 cpu time, factor 3.39)
JinjaThreads: theory HOL-Library.Adhoc_Overloading
JinjaThreads: theory HOL-Eisbach.Eisbach
JinjaThreads: theory HOL-Library.Lattice_Syntax
JinjaThreads: theory Automatic_Refinement.Foldi
JinjaThreads: theory Automatic_Refinement.Prio_List
JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1
JinjaThreads: theory Collections.ICF_Tools
JinjaThreads: theory Finger-Trees.FingerTree
JinjaThreads: theory HOL-Library.AList
JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot
JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot
JinjaThreads: theory HOL-Library.Bit
JinjaThreads: theory HOL-Library.Boolean_Algebra
JinjaThreads: theory Collections.Ord_Code_Preproc
JinjaThreads: theory Automatic_Refinement.Refine_Util
JinjaThreads: theory Collections.Locale_Code
JinjaThreads: theory Collections.Record_Intf
JinjaThreads: theory HOL-Library.Cancellation
JinjaThreads: theory HOL-Library.Char_ord
JinjaThreads: theory HOL-Library.Code_Abstract_Nat
JinjaThreads: theory HOL-Library.Code_Target_Nat
JinjaThreads: theory HOL-Library.Code_Target_Int
JinjaThreads: theory HOL-Library.Code_Char
JinjaThreads: theory HOL-Library.Complete_Partial_Order2
JinjaThreads: theory HOL-Library.Dlist
JinjaThreads: theory Automatic_Refinement.Anti_Unification
JinjaThreads: theory Automatic_Refinement.Attr_Comb
JinjaThreads: theory Automatic_Refinement.Autoref_Data
JinjaThreads: theory Automatic_Refinement.Indep_Vars
JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp
JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms
JinjaThreads: theory Automatic_Refinement.Tagged_Solver
JinjaThreads: theory Automatic_Refinement.Select_Solve
JinjaThreads: theory HOL-Library.Code_Target_Numeral
JinjaThreads: theory HOL-Library.Infinite_Set
JinjaThreads: theory HOL-Library.Multiset
JinjaThreads: theory HOL-Library.Monad_Syntax
JinjaThreads: theory HOL-Library.Nat_Bijection
JinjaThreads: theory HOL-Library.Old_Datatype
JinjaThreads: theory HOL-Library.Omega_Words_Fun
JinjaThreads: theory HOL-Library.Option_ord
JinjaThreads: theory Trie.Trie
JinjaThreads: theory HOL-Library.Phantom_Type
JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs
JinjaThreads: theory HOL-Library.RBT_Impl
JinjaThreads: theory HOL-Library.Simps_Case_Conv
JinjaThreads: theory HOL-Library.Sublist
JinjaThreads: theory HOL-Library.Transitive_Closure_Table
JinjaThreads: theory HOL-Library.Cardinality
JinjaThreads: theory HOL-Library.While_Combinator
JinjaThreads: theory HOL-Word.Bits
JinjaThreads: theory FinFun.FinFun
JinjaThreads: theory HOL-Library.Numeral_Type
JinjaThreads: theory Collections.DatRef
JinjaThreads: theory HOL-Word.Bits_Bit
JinjaThreads: theory HOL-Word.Misc_Numeric
JinjaThreads: theory HOL-Word.Misc_Typedef
JinjaThreads: theory HOL-Word.Bit_Representation
JinjaThreads: theory HOL-Word.Word_Miscellaneous
JinjaThreads: theory HOL-Library.Countable
JinjaThreads: theory HOL-Library.Type_Length
JinjaThreads: theory JinjaThreads.Set_Monad
JinjaThreads: theory JinjaThreads.Set_without_equal
JinjaThreads: theory Refine_Monadic.Refine_Chapter
JinjaThreads: theory HOL-Word.Bits_Int
JinjaThreads: theory JinjaThreads.Auxiliary
JinjaThreads: theory HOL-Library.Countable_Set
JinjaThreads: theory HOL-Word.Bool_List_Representation
JinjaThreads: theory HOL-Library.Countable_Complete_Lattices
JinjaThreads: theory Binomial-Heaps.BinomialHeap
JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap
JinjaThreads: theory HOL-ex.Quicksort
JinjaThreads: theory Native_Word.More_Bits_Int
JinjaThreads: theory Automatic_Refinement.Misc
JinjaThreads: theory HOL-Word.Word
JinjaThreads: theory HOL-Library.Order_Continuity
JinjaThreads: theory Native_Word.Bits_Integer
JinjaThreads: theory HOL-Library.Extended_Nat
JinjaThreads: theory Coinductive.Coinductive_Nat
JinjaThreads: theory Coinductive.Coinductive_List
JinjaThreads: theory Native_Word.Word_Misc
JinjaThreads: theory Automatic_Refinement.Digraph_Basic
JinjaThreads: theory Collections.SetIterator
JinjaThreads: theory Collections.Sorted_List_Operations
JinjaThreads: theory Automatic_Refinement.Refine_Lib
JinjaThreads: theory Automatic_Refinement.Autoref_Phases
JinjaThreads: theory Automatic_Refinement.Autoref_Tagging
JinjaThreads: theory Automatic_Refinement.Relators
JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover
JinjaThreads: theory Collections.SetIteratorOperations
JinjaThreads: theory Automatic_Refinement.Param_Tool
JinjaThreads: theory Automatic_Refinement.Param_HOL
JinjaThreads: theory Collections.Assoc_List
JinjaThreads: theory Collections.Dlist_add
JinjaThreads: theory Collections.Proper_Iterator
JinjaThreads: theory Collections.SetIteratorGA
JinjaThreads: theory Automatic_Refinement.Parametricity
JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops
JinjaThreads: theory Collections.It_to_It
JinjaThreads: theory Collections.Diff_Array
JinjaThreads: theory Collections.Trie_Impl
JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel
JinjaThreads: theory Native_Word.Code_Target_Bits_Int
JinjaThreads: theory Native_Word.Uint32
JinjaThreads: theory Collections.Trie2
JinjaThreads: theory Collections.Code_Target_ICF
JinjaThreads: theory Coinductive.Lazy_LList
JinjaThreads: theory Coinductive.TLList
JinjaThreads: theory Automatic_Refinement.Autoref_Translate
JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface
JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo
JinjaThreads: theory Automatic_Refinement.Autoref_Tool
JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL
JinjaThreads: theory Collections.HashCode
JinjaThreads: theory Coinductive.Lazy_TLList
JinjaThreads: theory Automatic_Refinement.Automatic_Refinement
JinjaThreads: theory Collections.Idx_Iterator
JinjaThreads: theory Refine_Monadic.Refine_Misc
JinjaThreads: theory Refine_Monadic.RefineG_Domain
JinjaThreads: theory Refine_Monadic.RefineG_Transfer
JinjaThreads: theory Refine_Monadic.RefineG_Assert
JinjaThreads: theory Refine_Monadic.RefineG_Recursion
JinjaThreads: theory Refine_Monadic.RefineG_While
JinjaThreads: theory Refine_Monadic.Refine_Basic
JinjaThreads: theory Refine_Monadic.Refine_Det
JinjaThreads: theory Refine_Monadic.Refine_Heuristics
JinjaThreads: theory Refine_Monadic.Refine_Leof
JinjaThreads: theory Refine_Monadic.Refine_Pfun
JinjaThreads: theory Refine_Monadic.Refine_More_Comb
JinjaThreads: theory Refine_Monadic.Refine_While
JinjaThreads: theory Refine_Monadic.Refine_Transfer
JinjaThreads: theory Refine_Monadic.Autoref_Monadic
JinjaThreads: theory Refine_Monadic.Refine_Automation
JinjaThreads: theory Refine_Monadic.Refine_Foreach
JinjaThreads: theory Refine_Monadic.Refine_Monadic
JinjaThreads: theory Collections.Gen_Iterator
JinjaThreads: theory Collections.Intf_Map
JinjaThreads: theory Collections.Intf_Set
JinjaThreads: theory Collections.Iterator
JinjaThreads: theory Collections.Array_Iterator
JinjaThreads: theory Collections.ICF_Spec_Base
JinjaThreads: theory Collections.AnnotatedListSpec
JinjaThreads: theory Collections.ListSpec
JinjaThreads: theory Collections.MapSpec
JinjaThreads: theory Collections.PrioSpec
JinjaThreads: theory Collections.PrioUniqueSpec
JinjaThreads: theory Collections.SetSpec
JinjaThreads: theory Collections.BinoPrioImpl
JinjaThreads: theory Collections.SkewPrioImpl
JinjaThreads: theory HOL-Library.RBT
JinjaThreads: theory Collections.RBT_add
JinjaThreads: theory Collections.ListGA
JinjaThreads: theory Collections.FTAnnotatedListImpl
JinjaThreads: theory Collections.PrioByAnnotatedList
JinjaThreads: theory Collections.PrioUniqueByAnnotatedList
JinjaThreads: theory Collections.Fifo
JinjaThreads: theory Collections.Algos
JinjaThreads: theory Collections.SetIndex
JinjaThreads: theory Collections.SetIteratorCollectionsGA
JinjaThreads: theory Collections.FTPrioImpl
JinjaThreads: theory Collections.MapGA
JinjaThreads: theory Collections.SetGA
JinjaThreads: theory Collections.FTPrioUniqueImpl
JinjaThreads: theory Collections.ArrayMapImpl
JinjaThreads: theory Collections.ListMapImpl
JinjaThreads: theory Collections.ListMapImpl_Invar
JinjaThreads: theory Collections.TrieMapImpl
JinjaThreads: theory Collections.RBTMapImpl
JinjaThreads: theory Collections.ArrayHashMap_Impl
JinjaThreads: theory Collections.ListSetImpl
JinjaThreads: theory Collections.ListSetImpl_Invar
JinjaThreads: theory Collections.ListSetImpl_NotDist
JinjaThreads: theory Collections.ListSetImpl_Sorted
JinjaThreads: theory Collections.SetByMap
JinjaThreads: theory Collections.HashMap_Impl
JinjaThreads: theory Collections.ArrayHashMap
JinjaThreads: theory Collections.ArraySetImpl
JinjaThreads: theory Collections.TrieSetImpl
JinjaThreads: theory Collections.RBTSetImpl
JinjaThreads: theory Collections.HashMap
JinjaThreads: theory Collections.ArrayHashSet
JinjaThreads: theory Collections.HashSet
JinjaThreads: theory Collections.MapStdImpl
JinjaThreads: theory Collections.SetStdImpl
JinjaThreads: theory Collections.ICF_Impl
JinjaThreads: theory Collections.ICF_Refine_Monadic
JinjaThreads: theory Collections.ICF_Autoref
JinjaThreads: theory Collections.Collections
JinjaThreads: theory Collections.CollectionsV1
JinjaThreads: theory JinjaThreads.JT_ICF
JinjaThreads: theory JinjaThreads.Basic_Main
JinjaThreads: theory HOL-Library.Prefix_Order
JinjaThreads: theory JinjaThreads.FWState
JinjaThreads: theory JinjaThreads.LTS
JinjaThreads: theory JinjaThreads.Type
JinjaThreads: theory JinjaThreads.ListIndex
JinjaThreads: theory JinjaThreads.Orders
JinjaThreads: theory JinjaThreads.Semilat
JinjaThreads: theory HOL-Library.Mapping
JinjaThreads: theory JinjaThreads.Err
JinjaThreads: theory HOL-Library.AList_Mapping
JinjaThreads: theory JinjaThreads.Listn
JinjaThreads: theory JinjaThreads.Opt
JinjaThreads: theory JinjaThreads.Product
JinjaThreads: theory JinjaThreads.Semilattices
JinjaThreads: theory JinjaThreads.Typing_Framework
JinjaThreads: theory JinjaThreads.SemilatAlg
JinjaThreads: theory JinjaThreads.Decl
JinjaThreads: theory JinjaThreads.Kildall
JinjaThreads: theory JinjaThreads.LBVSpec
JinjaThreads: theory JinjaThreads.Bisimulation
JinjaThreads: theory JinjaThreads.Typing_Framework_err
JinjaThreads: theory JinjaThreads.LBVComplete
JinjaThreads: theory JinjaThreads.LBVCorrect
JinjaThreads: theory JinjaThreads.Abstract_BV
JinjaThreads: theory JinjaThreads.TypeRel
JinjaThreads: theory JinjaThreads.TypeRelRefine
JinjaThreads: theory JinjaThreads.Value
JinjaThreads: theory JinjaThreads.Exceptions
JinjaThreads: theory JinjaThreads.Heap
JinjaThreads: theory JinjaThreads.SystemClasses
JinjaThreads: theory JinjaThreads.MM
JinjaThreads: theory JinjaThreads.State
JinjaThreads: theory JinjaThreads.FWCondAction
JinjaThreads: theory JinjaThreads.FWInterrupt
JinjaThreads: theory JinjaThreads.FWLock
JinjaThreads: theory JinjaThreads.FWThread
JinjaThreads: theory JinjaThreads.FWWait
JinjaThreads: theory JinjaThreads.Observable_Events
JinjaThreads: theory JinjaThreads.FWLocking
JinjaThreads: theory JinjaThreads.FWLockingThread
JinjaThreads: theory JinjaThreads.FWWellform
JinjaThreads: theory JinjaThreads.FWLifting
JinjaThreads: theory JinjaThreads.FWSemantics
JinjaThreads: theory JinjaThreads.JVMState
JinjaThreads: theory JinjaThreads.StartConfig
JinjaThreads: theory JinjaThreads.JMM_Spec
JinjaThreads: theory JinjaThreads.FWLiftingSem
JinjaThreads: theory JinjaThreads.FWProgressAux
JinjaThreads: theory JinjaThreads.Conform
JinjaThreads: theory JinjaThreads.State_Refinement
JinjaThreads: theory JinjaThreads.FWDeadlock
JinjaThreads: theory JinjaThreads.FWLTS
JinjaThreads: theory JinjaThreads.ConformThreaded
JinjaThreads: theory JinjaThreads.ExternalCall
JinjaThreads: theory JinjaThreads.FWProgress
JinjaThreads: theory JinjaThreads.SC
JinjaThreads: theory JinjaThreads.SC_Collections
JinjaThreads: theory JinjaThreads.JMM_DRF
JinjaThreads: theory JinjaThreads.SC_Legal
JinjaThreads: theory JinjaThreads.FWBisimulation
JinjaThreads: theory JinjaThreads.FWInitFinLift
JinjaThreads: theory JinjaThreads.Non_Speculative
JinjaThreads: theory JinjaThreads.Scheduler
JinjaThreads: theory JinjaThreads.HB_Completion
JinjaThreads: theory JinjaThreads.SC_Completion
JinjaThreads: theory JinjaThreads.WellForm
JinjaThreads: theory JinjaThreads.ExternalCall_Execute
JinjaThreads: theory JinjaThreads.BinOp
JinjaThreads: theory JinjaThreads.ExternalCallWF
JinjaThreads: theory JinjaThreads.JMM_Heap
JinjaThreads: theory JinjaThreads.SemiType
JinjaThreads: theory JinjaThreads.JMM_Type
JinjaThreads: theory JinjaThreads.JMM_Type2
JinjaThreads: theory JinjaThreads.JVM_SemiType
JinjaThreads: theory JinjaThreads.Expr
JinjaThreads: theory JinjaThreads.JVMInstructions
JinjaThreads: theory JinjaThreads.PCompiler
JinjaThreads: theory JinjaThreads.Random_Scheduler
JinjaThreads: theory JinjaThreads.PCompilerRefine
JinjaThreads: theory JinjaThreads.Round_Robin
JinjaThreads: theory JinjaThreads.JMM_Framework
JinjaThreads: theory JinjaThreads.JVMExceptions
JinjaThreads: theory JinjaThreads.JVMHeap
JinjaThreads: theory JinjaThreads.Effect
JinjaThreads: theory JinjaThreads.SC_Schedulers
JinjaThreads: theory JinjaThreads.CallExpr
JinjaThreads: theory JinjaThreads.DefAss
JinjaThreads: theory JinjaThreads.WWellForm
JinjaThreads: theory JinjaThreads.JHeap
JinjaThreads: theory JinjaThreads.JVMExecInstr
JinjaThreads: theory JinjaThreads.J1State
JinjaThreads: theory JinjaThreads.WellType
JinjaThreads: theory JinjaThreads.JVMExec
JinjaThreads: theory JinjaThreads.Compiler2
JinjaThreads: theory JinjaThreads.JVMDefensive
JinjaThreads: theory JinjaThreads.J1Heap
JinjaThreads: theory JinjaThreads.SmallStep
JinjaThreads: theory JinjaThreads.JVMThreaded
JinjaThreads: theory JinjaThreads.Compiler1
JinjaThreads: theory JinjaThreads.Exception_Tables
JinjaThreads: theory JinjaThreads.J1WellType
JinjaThreads: theory JinjaThreads.Compiler
JinjaThreads: theory JinjaThreads.Annotate
JinjaThreads: theory JinjaThreads.J1WellForm
JinjaThreads: theory JinjaThreads.JWellForm
JinjaThreads: theory JinjaThreads.JJ1WellForm
JinjaThreads: theory JinjaThreads.WellTypeRT
JinjaThreads: theory JinjaThreads.JVMExec_Execute
JinjaThreads: theory JinjaThreads.Preprocessor
JinjaThreads: theory JinjaThreads.ToString
JinjaThreads: theory JinjaThreads.JVM_Main
JinjaThreads: theory JinjaThreads.BVSpec
JinjaThreads: theory JinjaThreads.BVConform
JinjaThreads: theory JinjaThreads.TypeComp
JinjaThreads: theory JinjaThreads.EffectMono
JinjaThreads: theory JinjaThreads.TF_JVM
JinjaThreads: theory JinjaThreads.BVExec
JinjaThreads: theory JinjaThreads.LBVJVM
JinjaThreads: theory JinjaThreads.BVSpecTypeSafe
JinjaThreads: theory JinjaThreads.JMM_JVM
JinjaThreads: theory JinjaThreads.JMM_Typesafe
JinjaThreads: theory JinjaThreads.BVNoTypeError
JinjaThreads: theory JinjaThreads.JVMTau
JinjaThreads: theory JinjaThreads.BVProgressThreaded
JinjaThreads: theory JinjaThreads.BCVExec
JinjaThreads: theory JinjaThreads.JVMExec_Execute2
JinjaThreads: theory JinjaThreads.JMM_Common
JinjaThreads: theory JinjaThreads.JMM_Typesafe2
JinjaThreads: theory JinjaThreads.Execs
JinjaThreads: theory JinjaThreads.DefAssPreservation
JinjaThreads: theory JinjaThreads.Threaded
JinjaThreads: theory JinjaThreads.Progress
JinjaThreads: theory JinjaThreads.TypeSafe
JinjaThreads: theory JinjaThreads.JMM_J
JinjaThreads: theory JinjaThreads.ProgressThreaded
JinjaThreads: theory JinjaThreads.J_Execute
JinjaThreads: theory JinjaThreads.FWBisimDeadlock
JinjaThreads: theory JinjaThreads.FWBisimLift
JinjaThreads: theory JinjaThreads.J1
JinjaThreads: theory JinjaThreads.J0
JinjaThreads: theory JinjaThreads.DRF_J
JinjaThreads: theory JinjaThreads.Deadlocked
JinjaThreads: theory JinjaThreads.J_Main
JinjaThreads: theory JinjaThreads.J1Deadlock
JinjaThreads: theory JinjaThreads.J1JVMBisim
JinjaThreads: theory JinjaThreads.Common_Main
JinjaThreads: theory JinjaThreads.J0Bisim
JinjaThreads: theory JinjaThreads.J0J1Bisim
JinjaThreads: theory JinjaThreads.DRF_JVM
JinjaThreads: theory JinjaThreads.JVMDeadlocked
JinjaThreads: theory JinjaThreads.JVM_Execute
JinjaThreads: theory JinjaThreads.JVM_Execute2
JinjaThreads: theory JinjaThreads.Correctness1
JinjaThreads: theory JinjaThreads.Correctness1Threaded
JinjaThreads: theory JinjaThreads.Code_Generation
JinjaThreads: theory JinjaThreads.ApprenticeChallenge
JinjaThreads: theory JinjaThreads.BufferExample
JinjaThreads: theory JinjaThreads.BV_Main
JinjaThreads: theory JinjaThreads.Java2Jinja
JinjaThreads: theory JinjaThreads.Examples_Main
JinjaThreads: theory JinjaThreads.Execute_Main
JinjaThreads: theory JinjaThreads.JMM_J_Typesafe
JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe
JinjaThreads: theory JinjaThreads.J1JVM
JinjaThreads: theory JinjaThreads.JVMJ1
JinjaThreads: theory JinjaThreads.Correctness2
JinjaThreads: theory JinjaThreads.Correctness
JinjaThreads: theory JinjaThreads.JMM_Compiler
JinjaThreads: theory JinjaThreads.SC_Interp
JinjaThreads: theory JinjaThreads.Compiler_Main
JinjaThreads: theory JinjaThreads.JMM_Interp
JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2
JinjaThreads: theory JinjaThreads.JMM
JinjaThreads: theory JinjaThreads.MM_Main
JinjaThreads: theory JinjaThreads.JinjaThreads
Timing JinjaThreads (8 threads, 3389.547s elapsed time, 15394.792s cpu time, 5012.512s GC time, factor 4.54)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf
Finished JinjaThreads (0:57:41 elapsed time, 4:18:50 cpu time, factor 4.49)
Lorenz_C0: theory Lorenz_C0.Lorenz_C0
Timing Lorenz_C0 (8 threads, 820.864s elapsed time, 6215.024s cpu time, 56.976s GC time, factor 7.57)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Lorenz_C0
Finished Lorenz_C0 (0:13:44 elapsed time, 1:43:38 cpu time, factor 7.54)
HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
Timing HOL-ODE-Examples (8 threads, 505.132s elapsed time, 1966.372s cpu time, 74.088s GC time, factor 3.89)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Examples
Finished HOL-ODE-Examples (0:08:29 elapsed time, 0:32:49 cpu time, factor 3.87)
Affine_Arithmetic: theory Deriving.Comparator
Affine_Arithmetic: theory Deriving.Derive_Manager
Affine_Arithmetic: theory HOL-Library.Bit
Affine_Arithmetic: theory HOL-Decision_Procs.Dense_Linear_Order
Affine_Arithmetic: theory Deriving.Generator_Aux
Affine_Arithmetic: theory HOL-Library.Permutation
Affine_Arithmetic: theory HOL-Library.Boolean_Algebra
Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading
Affine_Arithmetic: theory HOL-Library.Char_ord
Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat
Affine_Arithmetic: theory HOL-Library.Code_Target_Nat
Affine_Arithmetic: theory HOL-Library.Code_Target_Int
Affine_Arithmetic: theory Deriving.Equality_Generator
Affine_Arithmetic: theory HOL-Library.Code_Char
Affine_Arithmetic: theory HOL-Library.Mapping
Affine_Arithmetic: theory HOL-Library.Monad_Syntax
Affine_Arithmetic: theory HOL-Library.Type_Length
Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral
Affine_Arithmetic: theory HOL-Library.RBT_Impl
Affine_Arithmetic: theory HOL-Word.Bits
Affine_Arithmetic: theory HOL-Word.Misc_Numeric
Affine_Arithmetic: theory HOL-Word.Bit_Representation
Affine_Arithmetic: theory Deriving.Equality_Instances
Affine_Arithmetic: theory HOL-Word.Word_Miscellaneous
Affine_Arithmetic: theory HOL-Word.Bits_Bit
Affine_Arithmetic: theory HOL-Word.Misc_Typedef
Affine_Arithmetic: theory Deriving.Countable_Generator
Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer
Affine_Arithmetic: theory Deriving.Compare
Affine_Arithmetic: theory Deriving.Comparator_Generator
Affine_Arithmetic: theory HOL-Library.Lattice_Algebras
Affine_Arithmetic: theory HOL-Word.Bits_Int
Affine_Arithmetic: theory HOL-Library.Log_Nat
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise
Affine_Arithmetic: theory List-Index.List_Index
Affine_Arithmetic: theory Show.Show
Affine_Arithmetic: theory Deriving.Compare_Generator
Affine_Arithmetic: theory Deriving.Compare_Instances
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict
Affine_Arithmetic: theory HOL-Word.Bool_List_Representation
Affine_Arithmetic: theory Show.Show_Instances
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
Affine_Arithmetic: theory Affine_Arithmetic.Polygon
Affine_Arithmetic: theory Native_Word.More_Bits_Int
Affine_Arithmetic: theory HOL-Word.Word
Affine_Arithmetic: theory Native_Word.Bits_Integer
Affine_Arithmetic: theory HOL-Library.Float
Affine_Arithmetic: theory Native_Word.Word_Misc
Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float
Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds
Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space
Affine_Arithmetic: theory Affine_Arithmetic.Float_Real
Affine_Arithmetic: theory HOL-Decision_Procs.Approximation
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form
Affine_Arithmetic: theory Affine_Arithmetic.Intersection
Affine_Arithmetic: theory Native_Word.Uint32
Affine_Arithmetic: theory Collections.HashCode
Affine_Arithmetic: theory Deriving.Hash_Generator
Affine_Arithmetic: theory Deriving.Hash_Instances
Affine_Arithmetic: theory Deriving.Derive
Affine_Arithmetic: theory HOL-Library.RBT
Affine_Arithmetic: theory HOL-Library.RBT_Mapping
Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression
Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code
Affine_Arithmetic: theory Affine_Arithmetic.Print
Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation
Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs
Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic
Timing Affine_Arithmetic (8 threads, 237.536s elapsed time, 1309.224s cpu time, 114.876s GC time, factor 5.51)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Affine_Arithmetic
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Affine_Arithmetic/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Affine_Arithmetic/outline.pdf
Finished Affine_Arithmetic (0:04:09 elapsed time, 0:22:45 cpu time, factor 5.48)
Collections: theory Collections.ICF_Tools
Collections: theory Collections.Partial_Equivalence_Relation
Collections: theory Finger-Trees.FingerTree
Collections: theory HOL-Library.AList
Collections: theory Binomial-Heaps.BinomialHeap
Collections: theory HOL-Library.Code_Abstract_Nat
Collections: theory HOL-Library.Code_Target_Int
Collections: theory Binomial-Heaps.SkewBinomialHeap
Collections: theory HOL-Library.Code_Target_Nat
Collections: theory Collections.Ord_Code_Preproc
Collections: theory HOL-Library.Dlist
Collections: theory Collections.Locale_Code
Collections: theory Collections.Record_Intf
Collections: theory HOL-Library.Code_Target_Numeral
Collections: theory Collections.SetIterator
Collections: theory Collections.Sorted_List_Operations
Collections: theory HOL-Library.RBT_Impl
Collections: theory Collections.DatRef
Collections: theory Native_Word.More_Bits_Int
Collections: theory Collections.Idx_Iterator
Collections: theory Collections.SetAbstractionIterator
Collections: theory Collections.SetIteratorOperations
Collections: theory Native_Word.Bits_Integer
Collections: theory Native_Word.Word_Misc
Collections: theory Collections.Assoc_List
Collections: theory Collections.Dlist_add
Collections: theory Collections.Proper_Iterator
Collections: theory Collections.SetIteratorGA
Collections: theory Collections.Diff_Array
Collections: theory Collections.It_to_It
Collections: theory Collections.Gen_Iterator
Collections: theory Collections.Iterator
Collections: theory Collections.ICF_Spec_Base
Collections: theory Collections.MapSpec
Collections: theory Collections.Robdd
Collections: theory Native_Word.Code_Target_Bits_Int
Collections: theory Native_Word.Uint32
Collections: theory Collections.Code_Target_ICF
Collections: theory Collections.Locale_Code_Ex
Collections: theory Collections.HashCode
Collections: theory Collections.RBT_add
Collections: theory Collections.GenCF_Gen_Chapter
Collections: theory Collections.GenCF_Chapter
Collections: theory Collections.Impl_Array_Stack
Collections: theory Collections.GenCF_Intf_Chapter
Collections: theory Collections.Intf_Comp
Collections: theory Collections.GenCF_Impl_Chapter
Collections: theory HOL-Library.Product_Lexorder
Collections: theory Collections.Intf_Hash
Collections: theory Collections.Array_Iterator
Collections: theory Collections.Intf_Map
Collections: theory Collections.Intf_Set
Collections: theory Collections.Gen_Map
Collections: theory Collections.Gen_Set
Collections: theory Collections.Impl_Cfun_Set
Collections: theory Collections.Impl_List_Set
Collections: theory Collections.Impl_Array_Map
Collections: theory Collections.Gen_Comp
Collections: theory Collections.Impl_List_Map
Collections: theory Collections.Impl_RBT_Map
Collections: theory Collections.Gen_Map2Set
Collections: theory Collections.Impl_Array_Hash_Map
Collections: theory Native_Word.Uint
Collections: theory Collections.Gen_Hash
Collections: theory Collections.Impl_Bit_Set
Collections: theory Collections.Impl_Uv_Set
Collections: theory Collections.GenCF
Collections: theory Collections.ICF_Spec_Chapter
Collections: theory Collections.ICF_Gen_Algo_Chapter
Collections: theory Collections.ICF_Chapter
Collections: theory Collections.ICF_Impl_Chapter
Collections: theory HOL-Library.RBT
Collections: theory Collections.AnnotatedListSpec
Collections: theory Collections.ListSpec
Collections: theory Collections.PrioSpec
Collections: theory Collections.PrioUniqueSpec
Collections: theory Collections.SetSpec
Collections: theory Collections.BinoPrioImpl
Collections: theory Collections.SkewPrioImpl
Collections: theory Collections.Trie_Impl
Collections: theory Collections.ListGA
Collections: theory Collections.Trie2
Collections: theory Collections.FTAnnotatedListImpl
Collections: theory Collections.PrioByAnnotatedList
Collections: theory Collections.PrioUniqueByAnnotatedList
Collections: theory Collections.Fifo
Collections: theory Collections.Algos
Collections: theory Collections.SetIndex
Collections: theory Collections.SetIteratorCollectionsGA
Collections: theory Collections.MapGA
Collections: theory Collections.SetGA
Collections: theory Collections.FTPrioImpl
Collections: theory Collections.FTPrioUniqueImpl
Collections: theory Collections.ArrayMapImpl
Collections: theory Collections.ListMapImpl
Collections: theory Collections.ListMapImpl_Invar
Collections: theory Collections.TrieMapImpl
Collections: theory Collections.RBTMapImpl
Collections: theory Collections.ArrayHashMap_Impl
Collections: theory Collections.HashMap_Impl
Collections: theory Collections.ListSetImpl
Collections: theory Collections.ListSetImpl_Invar
Collections: theory Collections.ListSetImpl_Sorted
Collections: theory Collections.SetByMap
Collections: theory Collections.ListSetImpl_NotDist
Collections: theory Collections.ArrayHashMap
Collections: theory Collections.HashMap
Collections: theory Collections.ArraySetImpl
Collections: theory Collections.TrieSetImpl
Collections: theory Collections.RBTSetImpl
Collections: theory Collections.ArrayHashSet
Collections: theory Collections.MapStdImpl
Collections: theory Collections.HashSet
Collections: theory Collections.SetStdImpl
Collections: theory Collections.ICF_Impl
Collections: theory Collections.ICF_Refine_Monadic
Collections: theory Collections.ICF_Autoref
Collections: theory Collections.Collections_Entrypoints_Chapter
Collections: theory Collections.ICF_Entrypoints_Chapter
Collections: theory Collections.Userguides_Chapter
Collections: theory Collections.Collections
Collections: theory Collections.Refine_Dflt
Collections: theory Collections.CollectionsV1
Collections: theory Collections.ICF_Userguide
Collections: theory Collections.Refine_Dflt_ICF
Collections: theory Collections.Refine_Dflt_Only_ICF
Collections: theory Collections.Refine_Monadic_Userguide
Timing Collections (8 threads, 151.853s elapsed time, 665.852s cpu time, 43.356s GC time, factor 4.38)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Collections
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Collections/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Collections/outline.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Collections/userguide.pdf
Finished Collections (0:02:47 elapsed time, 0:12:39 cpu time, factor 4.54)
Native_Word: theory HOL-Library.Adhoc_Overloading
Native_Word: theory HOL-Library.Char_ord
Native_Word: theory HOL-Library.Code_Target_Int
Native_Word: theory Native_Word.More_Bits_Int
Native_Word: theory HOL-Library.Old_Datatype
Native_Word: theory HOL-Library.Code_Test
Native_Word: theory HOL-Library.Nat_Bijection
Native_Word: theory HOL-Library.Monad_Syntax
Native_Word: theory HOL-Library.Code_Char
Native_Word: theory HOL-Library.Countable
Native_Word: theory Native_Word.Bits_Integer
Native_Word: theory Native_Word.Word_Misc
Native_Word: theory HOL-Imperative_HOL.Heap
Native_Word: theory HOL-Imperative_HOL.Heap_Monad
Native_Word: theory Native_Word.Native_Word_Imperative_HOL
Native_Word: theory Native_Word.Code_Target_Bits_Int
Native_Word: theory Native_Word.Uint
Native_Word: theory Native_Word.Uint16
Native_Word: theory Native_Word.Uint32
Native_Word: theory Native_Word.Uint64
Native_Word: theory Native_Word.Uint8
Native_Word: theory Native_Word.Native_Cast
Native_Word: theory Native_Word.Native_Word_Test
Native_Word: theory Native_Word.Native_Word_Test_Emu
Native_Word: theory Native_Word.Native_Word_Test_PolyML
Native_Word: theory Native_Word.Native_Word_Test_Scala
Native_Word: theory Native_Word.Native_Word_Test_PolyML2
Native_Word: theory Native_Word.Native_Word_Test_PolyML64
Native_Word: theory Native_Word.Native_Word_Test_GHC
Native_Word: theory Native_Word.Native_Word_Test_MLton
Native_Word: theory Native_Word.Native_Word_Test_MLton2
Native_Word: theory Native_Word.Native_Word_Test_OCaml2
Native_Word: theory Native_Word.Native_Word_Test_OCaml
Native_Word: theory Native_Word.Native_Word_Test_SMLNJ2
Native_Word: theory Native_Word.Native_Word_Test_SMLNJ
Native_Word: theory Native_Word.Uint_Userguide
Timing Native_Word (8 threads, 269.917s elapsed time, 281.376s cpu time, 6.576s GC time, factor 1.04)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Native_Word
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Native_Word/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Native_Word/outline.pdf
Finished Native_Word (0:04:36 elapsed time, 0:12:54 cpu time, factor 2.80)
Binomial-Heaps: theory Binomial-Heaps.BinomialHeap
Binomial-Heaps: theory Binomial-Heaps.SkewBinomialHeap
Binomial-Heaps: theory Binomial-Heaps.Test
Timing Binomial-Heaps (8 threads, 14.800s elapsed time, 46.360s cpu time, 3.624s GC time, factor 3.13)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Binomial-Heaps
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Binomial-Heaps/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Binomial-Heaps/outline.pdf
Finished Binomial-Heaps (0:00:20 elapsed time, 0:00:52 cpu time, factor 2.61)
Coinductive: theory HOL-Analysis.Inner_Product
Coinductive: theory Coinductive.Resumption
Coinductive: theory HOL-Analysis.L2_Norm
Coinductive: theory Coinductive.Coinductive_Nat
Coinductive: theory HOL-Analysis.Norm_Arith
Coinductive: theory HOL-Analysis.Product_Vector
Coinductive: theory Coinductive.Coinductive_List
Coinductive: theory HOL-Analysis.Euclidean_Space
Coinductive: theory HOL-Analysis.Linear_Algebra
Coinductive: theory HOL-Analysis.Topology_Euclidean_Space
Coinductive: theory Coinductive.Coinductive_List_Prefix
Coinductive: theory Coinductive.Hamming_Stream
Coinductive: theory Coinductive.Koenigslemma
Coinductive: theory Coinductive.LMirror
Coinductive: theory Coinductive.Lazy_LList
Coinductive: theory Coinductive.Quotient_Coinductive_List
Coinductive: theory Coinductive.TLList
Coinductive: theory Coinductive.Coinductive_Stream
Coinductive: theory Coinductive.Lazy_TLList
Coinductive: theory Coinductive.Quotient_TLList
Coinductive: theory Coinductive.TLList_CCPO
Coinductive: theory Coinductive.TLList_CCPO_Examples
Coinductive: theory Coinductive.Coinductive
Coinductive: theory HOL-Analysis.Extended_Real_Limits
Coinductive: theory Coinductive.CCPO_Topology
Coinductive: theory Coinductive.LList_CCPO_Topology
Coinductive: theory Coinductive.Coinductive_Examples
Timing Coinductive (8 threads, 33.933s elapsed time, 202.916s cpu time, 8.092s GC time, factor 5.98)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Coinductive
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Coinductive/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Coinductive/outline.pdf
Finished Coinductive (0:00:43 elapsed time, 0:03:49 cpu time, factor 5.26)
FinFun: theory HOL-Library.Phantom_Type
FinFun: theory HOL-Library.Cardinality
FinFun: theory FinFun.FinFunPred
Timing FinFun (8 threads, 6.790s elapsed time, 14.380s cpu time, 0.616s GC time, factor 2.12)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/FinFun
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/FinFun/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/FinFun/outline.pdf
Finished FinFun (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.76)
Finger-Trees: theory Finger-Trees.FingerTree
Finger-Trees: theory Finger-Trees.Test
Timing Finger-Trees (8 threads, 15.498s elapsed time, 32.772s cpu time, 2.160s GC time, factor 2.11)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Finger-Trees
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Finger-Trees/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Finger-Trees/outline.pdf
Finished Finger-Trees (0:00:20 elapsed time, 0:00:38 cpu time, factor 1.90)
List-Index: theory List-Index.List_Index
Timing List-Index (8 threads, 1.954s elapsed time, 8.720s cpu time, 0.100s GC time, factor 4.46)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/List-Index
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/List-Index/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/List-Index/outline.pdf
Finished List-Index (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.40)
Show: theory HOL-Computational_Algebra.Factorial_Ring
Show: theory Show.Show_Instances
Show: theory Show.Show_Complex
Show: theory Show.Show_Real_Impl
Show: theory HOL-Computational_Algebra.Polynomial
Timing Show (8 threads, 21.896s elapsed time, 50.996s cpu time, 2.108s GC time, factor 2.33)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Show
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Show/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Show/outline.pdf
Finished Show (0:00:26 elapsed time, 0:00:55 cpu time, factor 2.13)
Triangle: theory Triangle.Angles
Triangle: theory Triangle.Triangle
Timing Triangle (8 threads, 5.171s elapsed time, 8.740s cpu time, 0.120s GC time, factor 1.69)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Triangle
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Triangle/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Triangle/outline.pdf
Finished Triangle (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.43)
Timing Trie (8 threads, 23.180s elapsed time, 27.612s cpu time, 0.860s GC time, factor 1.19)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Trie
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Trie/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Trie/outline.pdf
Finished Trie (0:00:27 elapsed time, 0:00:31 cpu time, factor 1.17)
Timing FOL (8 threads, 3.737s elapsed time, 3.984s cpu time, 0.144s GC time, factor 1.07)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/FOL/FOL
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/FOL/FOL/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/FOL/FOL/outline.pdf
Finished FOL (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.14)
Running HOL-Decision_Procs ...
HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions
HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux
HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper
HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order
HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library
HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair
HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List
HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring
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.Dense_Linear_Order_Ex
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.Parametric_Ferrante_Rackoff
HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex
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 (8 threads, 492.876s elapsed time, 2015.116s cpu time, 231.068s GC time, factor 4.09)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Decision_Procs
Finished HOL-Decision_Procs (0:08:16 elapsed time, 0:33:38 cpu time, factor 4.07)
HOL-Eisbach: theory HOL-Eisbach.Eisbach
HOL-Eisbach: theory HOL-Eisbach.Eisbach_Old_Appl_Syntax
HOL-Eisbach: theory HOL-Eisbach.Eisbach_Tools
HOL-Eisbach: theory HOL-Eisbach.Examples
HOL-Eisbach: theory HOL-Eisbach.Tests
HOL-Eisbach: theory HOL-Eisbach.Examples_FOL
Timing HOL-Eisbach (8 threads, 3.752s elapsed time, 8.444s cpu time, 0.188s GC time, factor 2.25)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Eisbach
Finished HOL-Eisbach (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.77)
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 (8 threads, 65.274s elapsed time, 96.532s cpu time, 2.580s GC time, factor 1.48)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Imperative_HOL
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Imperative_HOL/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Imperative_HOL/outline.pdf
Finished HOL-Imperative_HOL (0:01:09 elapsed time, 0:06:05 cpu time, factor 5.27)
HOL-Types_To_Sets: theory HOL-Types_To_Sets.Prerequisites
HOL-Types_To_Sets: theory HOL-Types_To_Sets.Types_To_Sets
HOL-Types_To_Sets: theory HOL-Types_To_Sets.Finite
HOL-Types_To_Sets: theory HOL-Types_To_Sets.T2_Spaces
Timing HOL-Types_To_Sets (8 threads, 1.092s elapsed time, 1.672s cpu time, 0.000s GC time, factor 1.53)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Types_To_Sets
Finished HOL-Types_To_Sets (0:00:02 elapsed time)
HOL-ex: theory HOL-ex.Computations
HOL-ex: theory HOL-ex.Bubblesort
HOL-ex: theory HOL-ex.MergeSort
HOL-ex: theory HOL-ex.IArray_Examples
HOL-ex: theory HOL-ex.Perm_Fragments
HOL-ex: theory HOL-ex.Quicksort
HOL-ex: theory HOL-ex.Refute_Examples
HOL-ex: theory HOL-ex.Simps_Case_Conv_Examples
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.Cartouche_Examples
HOL-ex: theory HOL-ex.Case_Product
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.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.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.Lagrange
HOL-ex: theory HOL-ex.List_to_Set_Comprehension_Examples
HOL-ex: theory HOL-ex.LocaleTest2
HOL-ex: theory HOL-ex.MonoidGroup
HOL-ex: theory HOL-ex.Multiquote
HOL-ex: theory HOL-ex.Peano_Axioms
HOL-ex: theory HOL-ex.PresburgerEx
HOL-ex: theory HOL-ex.Rewrite_Examples
HOL-ex: theory HOL-ex.SAT_Examples
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.Termination
HOL-ex: theory HOL-ex.ThreeDivides
HOL-ex: theory HOL-ex.Transfer_Int_Nat
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_Cert
HOL-ex: theory HOL-ex.Argo_Examples
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_Script
HOL-ex: theory HOL-ex.Sum_of_Powers
HOL-ex: theory HOL-ex.Meson_Test
Timing HOL-ex (8 threads, 246.506s elapsed time, 1151.036s cpu time, 65.624s GC time, factor 4.67)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-ex
Finished HOL-ex (0:04:09 elapsed time, 0:19:56 cpu time, factor 4.79)
Group slow: 17:37:08 elapsed time, 55:27:27 cpu time, factor 3.15
Group AFP: 18:56:42 elapsed time, 59:42:20 cpu time, factor 3.15
Group main: 0:20:53 elapsed time, 1:11:20 cpu time, factor 3.41
Group timing: 0:32:34 elapsed time, 2:04:58 cpu time, factor 3.84
Group very_slow: 11:40:32 elapsed time, 29:12:27 cpu time, factor 2.50
Overall: 19:37:11 elapsed time, 62:03:41 cpu time, factor 3.16
Session Iptables_Semantics_Examples_Big: FAILED 1
Build step 'Execute shell' marked build as failure
Started calculate disk usage of build
Finished Calculation of disk usage of build in 0 seconds
Started calculate disk usage of workspace
Finished Calculation of disk usage of workspace in 0 seconds
Email was triggered for: Failure - 1st
Trigger Failure - Any was overridden by another trigger and will not send an email.
Trigger Failure - Still was overridden by another trigger and will not send an email.
Sending email for trigger: Failure - 1st
Sending email to: isabelle-ci@mail46.informatik.tu-muenchen.de