[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
20 files updated, 0 files merged, 1 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 fc87d3becd691e61804aa316f97d944aa3e55366 --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(fc87d3becd691e61804aa316f97d944aa3e55366)" --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
23 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 3a3f930183b74e6e099ea22f869e14216693d8dc --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(3a3f930183b74e6e099ea22f869e14216693d8dc)" --encoding UTF-8 --encodingmode replace
[isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins351610756849331119.sh
+ Admin/jenkins/run_build slow
### 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-e8d82343b692/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.930s elapsed time, 0.932s 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:24 elapsed time, 0:00:24 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, 250.893s elapsed time, 787.468s cpu time, 79.684s 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:48 elapsed time, 0:16:00 cpu time, factor 2.76) 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, 51.703s elapsed time, 230.672s cpu time, 8.196s GC time, factor 4.46) 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:51 elapsed time, 0:05:18 cpu time, factor 2.86) HOL-Analysis: theory HOL-Library.Cancellation HOL-Analysis: theory HOL-Library.Nat_Bijection HOL-Analysis: theory HOL-Library.Product_Plus HOL-Analysis: theory HOL-Library.Old_Datatype HOL-Analysis: theory HOL-Library.Disjoint_Sets HOL-Analysis: theory HOL-Library.Phantom_Type HOL-Analysis: theory HOL-Library.FuncSet HOL-Analysis: theory HOL-Library.Infinite_Set HOL-Analysis: theory HOL-Library.Product_Order HOL-Analysis: theory HOL-Library.Set_Algebras HOL-Analysis: theory HOL-Analysis.L2_Norm HOL-Analysis: theory HOL-Analysis.Infinite_Products HOL-Analysis: theory HOL-Analysis.Inner_Product HOL-Analysis: theory HOL-Analysis.Operator_Norm HOL-Analysis: theory HOL-Library.Multiset HOL-Analysis: theory HOL-Analysis.Poly_Roots HOL-Analysis: theory HOL-Library.Discrete HOL-Analysis: theory HOL-Library.Indicator_Function HOL-Analysis: theory HOL-Library.Liminf_Limsup HOL-Analysis: theory HOL-Library.Cardinality HOL-Analysis: theory HOL-Library.Nonpos_Ints 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.Finite_Cartesian_Product HOL-Analysis: theory HOL-Analysis.Linear_Algebra 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.Summation_Tests HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Tagged_Division 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, 413.484s elapsed time, 2215.236s cpu time, 194.340s GC time, factor 5.36) 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:08:51 elapsed time, 0:39:53 cpu time, factor 4.50) Building Ordinary_Differential_Equations ... 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.Bits Ordinary_Differential_Equations: theory HOL-Library.Log_Nat Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence Ordinary_Differential_Equations: theory HOL-Word.Misc_Numeric 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, 138.242s elapsed time, 618.520s cpu time, 20.016s GC time, factor 4.47) 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:58 elapsed time, 0:11:30 cpu time, factor 3.87) 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.Refine_Util_Bootstrap1 HOL-ODE-Refinement: theory Automatic_Refinement.Prio_List HOL-ODE-Refinement: theory Deriving.Comparator HOL-ODE-Refinement: theory Deriving.Derive_Manager HOL-ODE-Refinement: theory Deriving.Generator_Aux HOL-ODE-Refinement: theory HOL-Library.AList HOL-ODE-Refinement: theory HOL-Library.Bit HOL-ODE-Refinement: theory Automatic_Refinement.Mk_Term_Antiquot HOL-ODE-Refinement: theory Automatic_Refinement.Mpat_Antiquot HOL-ODE-Refinement: theory HOL-Library.Boolean_Algebra HOL-ODE-Refinement: theory Deriving.Equality_Generator HOL-ODE-Refinement: theory HOL-Library.Permutation HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Util 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 HOL-Library.Mapping HOL-ODE-Refinement: theory Deriving.Equality_Instances 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.Autoref_Data HOL-ODE-Refinement: theory Automatic_Refinement.Named_Sorted_Thms 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 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 Deriving.Compare HOL-ODE-Refinement: theory Deriving.Comparator_Generator 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 Affine_Arithmetic.Counterclockwise_2D_Strict HOL-ODE-Refinement: theory Refine_Monadic.Refine_Chapter HOL-ODE-Refinement: theory Show.Show 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 Collections.Assoc_List HOL-ODE-Refinement: theory Collections.Proper_Iterator HOL-ODE-Refinement: theory Collections.SetIteratorGA HOL-ODE-Refinement: theory Collections.It_to_It HOL-ODE-Refinement: theory Automatic_Refinement.Parametricity HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Id_Ops HOL-ODE-Refinement: theory Collections.Diff_Array 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 Collections.Intf_Hash HOL-ODE-Refinement: theory Deriving.Hash_Generator 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.Gen_Hash HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Recursion HOL-ODE-Refinement: theory Deriving.Hash_Instances HOL-ODE-Refinement: theory Deriving.Derive HOL-ODE-Refinement: theory Refine_Monadic.RefineG_While HOL-ODE-Refinement: theory Refine_Monadic.Refine_Basic 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.Iterator HOL-ODE-Refinement: theory Collections.Impl_Cfun_Set 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 Affine_Arithmetic.Affine_Code HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_String 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, 293.996s elapsed time, 1669.928s cpu time, 178.392s GC time, factor 5.68) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Refinement Finished HOL-ODE-Refinement (0:06:02 elapsed time, 0:31:35 cpu time, factor 5.23) 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, 1549.377s elapsed time, 3407.736s cpu time, 314.516s GC time, factor 2.20) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Numerics Finished HOL-ODE-Numerics (0:27:40 elapsed time, 1:00:43 cpu time, factor 2.19) 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, 330.674s elapsed time, 683.376s cpu time, 51.352s GC time, factor 2.07) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Lorenz_Approximation Finished Lorenz_Approximation (0:06:17 elapsed time, 0:12:54 cpu time, factor 2.05) HOL-Library: theory HOL-Library.Adhoc_Overloading HOL-Library: theory HOL-Library.Preorder HOL-Library: theory HOL-Library.Lattice_Syntax HOL-Library: theory HOL-Library.AList HOL-Library: theory HOL-Library.BNF_Axiomatization HOL-Library: theory HOL-Library.Boolean_Algebra HOL-Library: theory HOL-Library.Bit HOL-Library: theory HOL-Library.BNF_Corec HOL-Library: theory HOL-Library.Cancellation 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_Binary_Nat HOL-Library: theory HOL-Library.Code_Target_Nat HOL-Library: theory HOL-Library.Code_Char HOL-Library: theory HOL-Library.Code_Target_Int 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.Multiset HOL-Library: theory HOL-Library.Complete_Partial_Order2 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.ListVector HOL-Library: theory HOL-Library.Omega_Words_Fun HOL-Library: theory HOL-Library.Ramsey 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.Product_Lexorder HOL-Library: theory HOL-Library.Product_Plus HOL-Library: theory HOL-Library.Quotient_Syntax HOL-Library: theory HOL-Library.Product_Order HOL-Library: theory HOL-Library.Quotient_Type HOL-Library: theory HOL-Library.Quotient_Option HOL-Library: theory HOL-Library.Quotient_Product HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck HOL-Library: theory HOL-Library.Quotient_Set HOL-Library: theory HOL-Library.Quotient_Sum HOL-Library: theory HOL-Library.Finite_Lattice HOL-Library: theory HOL-Library.Quotient_List HOL-Library: theory HOL-Library.RBT_Impl HOL-Library: theory HOL-Library.Cardinality 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.Periodic_Fun HOL-Library: theory HOL-Library.Countable_Set HOL-Library: theory HOL-Library.FSet 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, 86.452s elapsed time, 562.784s cpu time, 31.804s GC time, factor 6.51) 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:40 elapsed time, 0:11:32 cpu time, factor 4.32) 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, 21.394s elapsed time, 52.116s cpu time, 2.784s GC time, factor 2.44) 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:46 elapsed time, 0:01:38 cpu time, factor 2.11) HOL-Word: theory HOL-Library.Bit HOL-Word: theory HOL-Word.Misc_Typedef HOL-Word: theory HOL-Library.Boolean_Algebra HOL-Word: theory HOL-Word.Misc_Numeric HOL-Word: theory HOL-Word.Bits HOL-Word: theory HOL-Library.Phantom_Type 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, 13.543s elapsed time, 65.776s cpu time, 2.280s GC time, factor 4.86) 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:31 elapsed time, 0:01:37 cpu time, factor 3.06) Word_Lib: theory HOL-Library.Sublist Word_Lib: theory Word_Lib.Hex_Words Word_Lib: theory Word_Lib.Signed_Words Word_Lib: theory Word_Lib.HOL_Lemmas Word_Lib: theory Word_Lib.More_Divides Word_Lib: theory Word_Lib.Enumeration 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, 73.822s elapsed time, 188.732s cpu time, 4.816s GC time, factor 2.56) 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:31 elapsed time, 0:03:36 cpu time, factor 2.37) IP_Addresses: theory HOL-Eisbach.Eisbach IP_Addresses: theory HOL-Library.Cancellation IP_Addresses: theory HOL-Library.Infinite_Set IP_Addresses: theory IP_Addresses.NumberWang_IPv4 IP_Addresses: theory IP_Addresses.NumberWang_IPv6 IP_Addresses: theory HOL-Library.Option_ord IP_Addresses: theory IP_Addresses.Word_More 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.Lib_Numbers_toString IP_Addresses: theory IP_Addresses.Hs_Compat IP_Addresses: theory IP_Addresses.Word_Next 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, 333.763s elapsed time, 953.212s cpu time, 59.068s GC time, factor 2.86) 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:06:16 elapsed time, 0:17:28 cpu time, factor 2.78) Simple_Firewall: theory HOL-Library.Char_ord Simple_Firewall: theory Simple_Firewall.GroupF Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries Simple_Firewall: theory Simple_Firewall.List_Product_More Simple_Firewall: theory Simple_Firewall.Option_Helpers Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString 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, 26.350s elapsed time, 98.976s cpu time, 4.548s GC time, factor 3.76) 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:54 elapsed time, 0:02:36 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.636s elapsed time, 34.716s cpu time, 1.096s GC time, factor 2.98) 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:30 elapsed time, 0:01:05 cpu time, factor 2.17) Building Iptables_Semantics ... Iptables_Semantics: theory HOL-Library.Code_Target_Int Iptables_Semantics: theory Native_Word.More_Bits_Int Iptables_Semantics: theory HOL-Library.Code_Char Iptables_Semantics: theory HOL-Library.LaTeXsugar Iptables_Semantics: theory Iptables_Semantics.Negation_Type Iptables_Semantics: theory Iptables_Semantics.List_Misc 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.Repeat_Stabilize Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF Iptables_Semantics: theory Iptables_Semantics.Ternary Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors Iptables_Semantics: theory Iptables_Semantics.IpAddresses Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags Iptables_Semantics: theory Iptables_Semantics.Conntrack_State 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.Semantics Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary 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_Lemmas Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString 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.Ports_Normalize Iptables_Semantics: theory Iptables_Semantics.No_Spoof Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize 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, 184.670s elapsed time, 739.132s cpu time, 61.320s GC time, factor 4.00) 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:10 elapsed time, 0:15:19 cpu time, factor 3.67) Building Iptables_Semantics_Examples ... Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall 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, 283.578s elapsed time, 1906.160s cpu time, 194.816s GC time, factor 6.72) 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:17 elapsed time, 0:32:49 cpu time, factor 6.21) Running Iptables_Semantics_Examples_Big ... Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern 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.IP_Address_Space_Examples_All_Large Run out of store - interrupting threads Iptables_Semantics_Examples_Big FAILED 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.Code_Target_Int Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat Flyspeck-Tame: theory HOL-Library.IArray Flyspeck-Tame: theory HOL-Library.While_Combinator Flyspeck-Tame: theory HOL-Library.Code_Target_Nat Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso 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.IArray_Syntax Flyspeck-Tame: theory Flyspeck-Tame.ListSum Flyspeck-Tame: theory Flyspeck-Tame.Rotation 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.TameProps Flyspeck-Tame: theory Flyspeck-Tame.Enumerator 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, 34364.480s elapsed time, 53515.372s cpu time, 2027.936s GC time, factor 1.56) 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 (9:32:55 elapsed time, 14:52:09 cpu time, factor 1.56) 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.A_Aodv_Predicates AODV: theory AODV.A_Loop_Freedom AODV: theory AODV.A_Quality_Increases AODV: theory AODV.A_Seq_Invariants AODV: theory AODV.A_Global_Invariants AODV: theory AODV.A_Aodv_Loop_Freedom 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.C_Aodv_Predicates AODV: theory AODV.C_Loop_Freedom AODV: theory AODV.C_Quality_Increases AODV: theory AODV.C_Seq_Invariants AODV: theory AODV.C_Global_Invariants AODV: theory AODV.C_Aodv_Loop_Freedom 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.B_Aodv_Predicates AODV: theory AODV.E_Global_Invariants AODV: theory AODV.B_Loop_Freedom AODV: theory AODV.B_Quality_Increases AODV: theory AODV.B_Seq_Invariants AODV: theory AODV.E_Aodv_Loop_Freedom AODV: theory AODV.B_Global_Invariants AODV: theory AODV.B_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, 9580.073s elapsed time, 47342.168s cpu time, 4372.380s GC time, factor 4.94) 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:39:53 elapsed time, 13:09:22 cpu time, factor 4.94) 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, 8111.771s elapsed time, 28089.804s cpu time, 1948.632s GC time, factor 3.46) 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:15:17 elapsed time, 7:48:16 cpu time, factor 3.46) JinjaThreads: theory HOL-Eisbach.Eisbach JinjaThreads: theory Automatic_Refinement.Prio_List JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1 JinjaThreads: theory Automatic_Refinement.Foldi JinjaThreads: theory Collections.ICF_Tools JinjaThreads: theory Finger-Trees.FingerTree JinjaThreads: theory HOL-Library.Lattice_Syntax JinjaThreads: theory HOL-Library.Adhoc_Overloading 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 Collections.Ord_Code_Preproc JinjaThreads: theory HOL-Library.Boolean_Algebra JinjaThreads: theory Collections.Locale_Code JinjaThreads: theory Automatic_Refinement.Refine_Util 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_Int JinjaThreads: theory HOL-Library.Code_Char JinjaThreads: theory HOL-Library.Code_Target_Nat 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.Named_Sorted_Thms JinjaThreads: theory Automatic_Refinement.Indep_Vars JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp 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 FinFun.FinFun JinjaThreads: theory HOL-Library.Numeral_Type JinjaThreads: theory Collections.DatRef JinjaThreads: theory HOL-Word.Bits JinjaThreads: theory HOL-Word.Misc_Numeric JinjaThreads: theory HOL-Word.Bit_Representation JinjaThreads: theory HOL-Word.Bits_Bit JinjaThreads: theory HOL-Word.Word_Miscellaneous JinjaThreads: theory HOL-Library.Type_Length JinjaThreads: theory HOL-Word.Bits_Int JinjaThreads: theory HOL-Word.Misc_Typedef JinjaThreads: theory HOL-Library.Countable JinjaThreads: theory JinjaThreads.Set_Monad JinjaThreads: theory JinjaThreads.Set_without_equal JinjaThreads: theory Refine_Monadic.Refine_Chapter JinjaThreads: theory JinjaThreads.Auxiliary JinjaThreads: theory HOL-Word.Bool_List_Representation JinjaThreads: theory HOL-Library.Countable_Set JinjaThreads: theory Native_Word.More_Bits_Int JinjaThreads: theory HOL-Word.Word JinjaThreads: theory HOL-Library.Countable_Complete_Lattices JinjaThreads: theory Binomial-Heaps.BinomialHeap JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap JinjaThreads: theory HOL-ex.Quicksort JinjaThreads: theory Automatic_Refinement.Misc JinjaThreads: theory Native_Word.Bits_Integer JinjaThreads: theory HOL-Library.Order_Continuity JinjaThreads: theory HOL-Library.Extended_Nat JinjaThreads: theory Coinductive.Coinductive_Nat JinjaThreads: theory Native_Word.Word_Misc JinjaThreads: theory Coinductive.Coinductive_List JinjaThreads: theory Automatic_Refinement.Digraph_Basic JinjaThreads: theory Collections.SetIterator JinjaThreads: theory Collections.Sorted_List_Operations JinjaThreads: theory Automatic_Refinement.Refine_Lib JinjaThreads: theory Collections.SetIteratorOperations 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 Automatic_Refinement.Param_Tool JinjaThreads: theory Automatic_Refinement.Param_HOL JinjaThreads: theory Native_Word.Code_Target_Bits_Int JinjaThreads: theory Native_Word.Uint32 JinjaThreads: theory Collections.Assoc_List JinjaThreads: theory Collections.Dlist_add JinjaThreads: theory Collections.Proper_Iterator JinjaThreads: theory Collections.SetIteratorGA JinjaThreads: theory Collections.Code_Target_ICF JinjaThreads: theory Automatic_Refinement.Parametricity JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops JinjaThreads: theory Collections.Diff_Array JinjaThreads: theory Collections.Trie_Impl JinjaThreads: theory Collections.It_to_It JinjaThreads: theory Coinductive.Lazy_LList JinjaThreads: theory Coinductive.TLList JinjaThreads: theory Collections.Trie2 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel JinjaThreads: theory Collections.HashCode 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 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.Fifo JinjaThreads: theory Collections.FTAnnotatedListImpl JinjaThreads: theory Collections.PrioByAnnotatedList JinjaThreads: theory Collections.PrioUniqueByAnnotatedList JinjaThreads: theory Collections.Algos JinjaThreads: theory Collections.SetIndex JinjaThreads: theory Collections.SetIteratorCollectionsGA JinjaThreads: theory Collections.MapGA JinjaThreads: theory Collections.SetGA JinjaThreads: theory Collections.FTPrioImpl 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.Mapping JinjaThreads: theory HOL-Library.Prefix_Order JinjaThreads: theory JinjaThreads.LTS JinjaThreads: theory JinjaThreads.Type JinjaThreads: theory JinjaThreads.FWState JinjaThreads: theory JinjaThreads.ListIndex JinjaThreads: theory JinjaThreads.Orders JinjaThreads: theory JinjaThreads.Semilat 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.JMM_Spec JinjaThreads: theory JinjaThreads.StartConfig 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.SemiType JinjaThreads: theory JinjaThreads.JMM_Heap JinjaThreads: theory JinjaThreads.JVM_SemiType JinjaThreads: theory JinjaThreads.JMM_Type JinjaThreads: theory JinjaThreads.JMM_Type2 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.WellType JinjaThreads: theory JinjaThreads.JVMExecInstr JinjaThreads: theory JinjaThreads.JVMExec JinjaThreads: theory JinjaThreads.J1State JinjaThreads: theory JinjaThreads.Annotate 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.JWellForm JinjaThreads: theory JinjaThreads.Preprocessor JinjaThreads: theory JinjaThreads.J1WellForm JinjaThreads: theory JinjaThreads.JJ1WellForm JinjaThreads: theory JinjaThreads.WellTypeRT JinjaThreads: theory JinjaThreads.JVMExec_Execute JinjaThreads: theory JinjaThreads.ToString JinjaThreads: theory JinjaThreads.JVM_Main JinjaThreads: theory JinjaThreads.BVSpec JinjaThreads: theory JinjaThreads.EffectMono JinjaThreads: theory JinjaThreads.BVConform JinjaThreads: theory JinjaThreads.TypeComp 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.Java2Jinja JinjaThreads: theory JinjaThreads.BV_Main 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.SC_Interp JinjaThreads: theory JinjaThreads.JMM_Compiler 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, 3481.270s elapsed time, 15924.856s cpu time, 4984.344s GC time, factor 4.57) 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:58:59 elapsed time, 4:27:41 cpu time, factor 4.54) Lorenz_C0: theory Lorenz_C0.Lorenz_C0 Timing Lorenz_C0 (8 threads, 1069.475s elapsed time, 8212.168s cpu time, 54.868s GC time, factor 7.68) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Lorenz_C0 Finished Lorenz_C0 (0:17:53 elapsed time, 2:16:55 cpu time, factor 7.65) HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples Timing HOL-ODE-Examples (8 threads, 551.911s elapsed time, 2165.324s cpu time, 67.544s GC time, factor 3.92) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Examples Finished HOL-ODE-Examples (0:09:15 elapsed time, 0:36:08 cpu time, factor 3.90)
Group slow: 17:07:52 elapsed time, 48:11:27 cpu time, factor 2.81 Group AFP: 18:12:12 elapsed time, 51:28:05 cpu time, factor 2.83 Group main: 0:17:51 elapsed time, 1:09:03 cpu time, factor 3.87 Group timing: 0:12:03 elapsed time, 0:53:03 cpu time, factor 4.40 Group very_slow: 10:46:33 elapsed time, 19:53:02 cpu time, factor 1.85 Overall: 18:31:38 elapsed time, 52:37:34 cpu time, factor 2.84
Session Iptables_Semantics_Examples_Big: FAILED 130 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