Console Output

01:33:10 Started by an SCM change
01:33:10 [EnvInject] - Loading node environment variables.
01:33:10 Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow
01:33:10 [isabelle-nightly-slow] $ hg showconfig paths.default
01:33:10 [isabelle-nightly-slow] $ hg pull --rev default
01:33:10 pulling from http://isabelle.in.tum.de/repos/isabelle/
01:33:10 searching for changes
01:33:10 no changes found
01:33:10 [isabelle-nightly-slow] $ hg update --clean --rev default
01:33:10 14 files updated, 0 files merged, 0 files removed, 0 files unresolved
01:33:10 [isabelle-nightly-slow] $ hg --config extensions.purge= clean --all
01:33:11 [isabelle-nightly-slow] $ hg log --rev . --template {node}
01:33:11 [isabelle-nightly-slow] $ hg log --rev . --template {rev}
01:33:11 [isabelle-nightly-slow] $ hg log --rev 4d088fe6185ec2c16442a5568951da50c0fbde4e --template exists\n
01:33:11 exists
01:33:11 [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(4d088fe6185ec2c16442a5568951da50c0fbde4e)" --encoding UTF-8 --encodingmode replace
01:33:11 [afp] $ hg showconfig paths.default
01:33:11 [afp] $ hg pull --rev default
01:33:12 pulling from https://bitbucket.org/isa-afp/afp-devel/
01:33:12 no changes found
01:33:12 [afp] $ hg update --clean --rev default
01:33:12 3 files updated, 0 files merged, 0 files removed, 0 files unresolved
01:33:12 [afp] $ hg --config extensions.purge= clean --all
01:33:13 [afp] $ hg log --rev . --template {node}
01:33:13 [afp] $ hg log --rev . --template {rev}
01:33:13 [afp] $ hg log --rev d8c2252ee9991ad7463ab13671514c70dd0bb353 --template exists\n
01:33:13 exists
01:33:13 [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(d8c2252ee9991ad7463ab13671514c70dd0bb353)" --encoding UTF-8 --encodingmode replace
01:33:13 No emails were triggered.
01:33:13 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/hudson2605151717466314589.sh
01:33:13 + Admin/jenkins/run_build slow
01:33:13 + set -e
01:33:13 + PROFILE=slow
01:33:13 + shift
01:33:13 + bin/isabelle components -a
01:33:13 + bin/isabelle jedit -bf
01:33:13 ### Building graph browser ...
01:33:14 warning: [options] bootstrap class path not set in conjunction with -source 1.4
01:33:14 warning: [options] source value 1.4 is obsolete and will be removed in a future release
01:33:14 warning: [options] target value 1.4 is obsolete and will be removed in a future release
01:33:14 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
01:33:14 Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.
01:33:14 Note: Recompile with -Xlint:deprecation for details.
01:33:14 4 warnings
01:33:15 ### Building Isabelle/Scala ...
01:34:29 ### Building Isabelle/jEdit ...
01:34:58 + bin/isabelle ci_build_slow
01:35:04 
01:35:04 === CONFIGURATION ===
01:35:04 
01:35:04 ISABELLE_BUILD_OPTIONS=""
01:35:04 
01:35:04 ML_PLATFORM="x86_64-linux"
01:35:04 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"
01:35:04 ML_SYSTEM="polyml-5.6"
01:35:04 ML_OPTIONS="-H 4000 --maxheap 10G"
01:35:05 
01:35:05 === BUILD ===
01:35:05 
01:35:05 Build started at Tue, 7 Mar 2017 01:35:04 +0100
01:35:05 Isabelle id 158cba86140f
01:35:05 Build for AFP id 35409c478655
01:35:05 
01:35:05 === LOG ===
01:35:05 
01:35:06 Session Pure/Pure
01:35:06 Session HOL/HOL (main)
01:35:07 Session AFP/AWN (AFP)
01:35:07 Session AFP/AODV (AFP slow)
01:35:08 Session HOL/HOL-Analysis (main timing)
01:35:08 Session AFP/Ordinary_Differential_Equations (AFP)
01:35:08 Session AFP/HOL-ODE (AFP)
01:35:08 Session AFP/HOL-ODE-Refinement (AFP)
01:35:09 Session AFP/HOL-ODE-Numerics (AFP)
01:35:09 Session AFP/HOL-ODE-Examples (AFP slow)
01:35:09 Session HOL/HOL-Library (main timing)
01:35:09 Session AFP/ConcurrentIMP (AFP)
01:35:09 Session AFP/ConcurrentGC (AFP slow)
01:35:09 Session AFP/Flyspeck-Tame (AFP slow very_slow)
01:35:09 Session HOL/HOL-Word (main timing)
01:35:10 Session AFP/JinjaThreads (AFP slow)
01:35:10 Session AFP/Word_Lib (AFP)
01:35:10 Session AFP/IP_Addresses (AFP)
01:35:11 Session AFP/Simple_Firewall (AFP)
01:35:11 Session AFP/Routing (AFP)
01:35:11 Session AFP/Iptables_Semantics (AFP)
01:35:11 Session AFP/Iptables_Semantics_Examples (AFP slow very_slow)
01:35:11 Building Pure ...
01:35:27 Pure: theory Pure
01:35:28 Pure: theory ML_Bootstrap
01:35:31 Warning: missing document directory
01:35:31 Timing Pure (1 threads, 0.801s elapsed time, 0.800s cpu time, 0.000s GC time, factor 1.00)
01:35:31 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure
01:35:31 Finished Pure (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.99)
01:35:31 Building HOL ...
01:35:32 HOL: theory Code_Generator
01:35:35 HOL: theory HOL
01:35:40 HOL: theory Argo
01:35:40 HOL: theory Ctr_Sugar
01:35:40 HOL: theory Orderings
01:35:42 HOL: theory SAT
01:35:42 HOL: theory Groups
01:35:45 HOL: theory Lattices
01:35:47 HOL: theory Set
01:35:49 HOL: theory Fun
01:35:49 HOL: theory Rings
01:35:49 HOL: theory Typedef
01:35:49 HOL: theory Complete_Lattices
01:35:52 HOL: theory Inductive
01:35:54 HOL: theory Product_Type
01:35:54 HOL: theory Sum_Type
01:35:56 HOL: theory Complete_Partial_Order
01:36:01 HOL: theory Nat
01:36:04 HOL: theory Meson
01:36:04 HOL: theory Fields
01:36:04 HOL: theory ATP
01:36:07 HOL: theory Metis
01:36:10 HOL: theory Finite_Set
01:36:12 HOL: theory Relation
01:36:13 HOL: theory Transitive_Closure
01:36:15 HOL: theory Wellfounded
01:36:16 HOL: theory Fun_Def_Base
01:36:16 HOL: theory Hilbert_Choice
01:36:16 HOL: theory Wfrec
01:36:16 HOL: theory Order_Relation
01:36:16 HOL: theory BNF_Wellorder_Relation
01:36:17 HOL: theory Zorn
01:36:17 HOL: theory BNF_Wellorder_Embedding
01:36:17 HOL: theory BNF_Wellorder_Constructions
01:36:18 HOL: theory BNF_Cardinal_Order_Relation
01:36:19 HOL: theory BNF_Cardinal_Arithmetic
01:36:20 HOL: theory BNF_Def
01:36:22 HOL: theory BNF_Composition
01:36:22 HOL: theory Basic_BNFs
01:36:23 HOL: theory BNF_Fixpoint_Base
01:36:27 HOL: theory BNF_Least_Fixpoint
01:36:29 HOL: theory Basic_BNF_LFPs
01:36:30 HOL: theory Transfer
01:36:31 HOL: theory Num
01:36:35 HOL: theory Power
01:36:38 HOL: theory Groups_Big
01:36:41 HOL: theory Equiv_Relations
01:36:42 HOL: theory Lifting
01:36:43 HOL: theory Lifting_Set
01:36:43 HOL: theory Option
01:36:43 HOL: theory Quotient
01:36:44 HOL: theory Extraction
01:36:44 HOL: theory Lattices_Big
01:36:44 HOL: theory Partial_Function
01:36:45 HOL: theory Fun_Def
01:36:47 HOL: theory Int
01:36:51 HOL: theory Nat_Transfer
01:36:51 HOL: theory Euclidean_Division
01:36:57 HOL: theory Parity
01:37:00 HOL: theory Divides
01:37:11 HOL: theory Code_Numeral
01:37:11 HOL: theory Set_Interval
01:37:11 HOL: theory Numeral_Simprocs
01:37:11 HOL: theory SMT
01:37:12 HOL: theory Semiring_Normalization
01:37:15 HOL: theory Conditionally_Complete_Lattices
01:37:15 HOL: theory Filter
01:37:15 HOL: theory Groebner_Basis
01:37:17 HOL: theory Presburger
01:37:20 HOL: theory Sledgehammer
01:37:22 HOL: theory List
01:37:33 HOL: theory Groups_List
01:37:33 HOL: theory Map
01:37:35 HOL: theory Enum
01:37:35 HOL: theory Random
01:37:38 HOL: theory String
01:37:39 HOL: theory BNF_Greatest_Fixpoint
01:37:39 HOL: theory Typerep
01:37:39 HOL: theory Predicate
01:37:41 HOL: theory Lazy_Sequence
01:37:42 HOL: theory Limited_Sequence
01:37:43 HOL: theory Code_Evaluation
01:37:44 HOL: theory Quickcheck_Random
01:37:48 HOL: theory Quickcheck_Exhaustive
01:37:48 HOL: theory Random_Pred
01:37:48 HOL: theory Quickcheck_Narrowing
01:37:48 HOL: theory Random_Sequence
01:37:53 HOL: theory Record
01:37:53 HOL: theory Predicate_Compile
01:37:55 HOL: theory Nitpick
01:38:02 HOL: theory Main
01:38:04 HOL: theory Archimedean_Field
01:38:04 HOL: theory Binomial
01:38:04 HOL: theory GCD
01:38:04 HOL: theory Topological_Spaces
01:38:16 HOL: theory Rat
01:38:19 HOL: theory Real
01:38:22 HOL: theory Real_Vector_Spaces
01:38:38 HOL: theory Limits
01:38:38 HOL: theory Inequalities
01:38:43 HOL: theory Deriv
01:38:43 HOL: theory Series
01:38:45 HOL: theory NthRoot
01:38:46 HOL: theory Transcendental
01:38:53 HOL: theory Complex
01:38:55 HOL: theory MacLaurin
01:38:56 HOL: theory Complex_Main
01:40:48 Timing HOL (8 threads, 220.105s elapsed time, 682.852s cpu time, 40.280s GC time, factor 3.10)
01:40:48 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL
01:40:48 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf
01:40:48 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf
01:40:48 Finished HOL (0:05:16 elapsed time, 0:14:39 cpu time, factor 2.78)
01:40:52 Building HOL-Library ...
01:40:56 HOL-Library: theory Adhoc_Overloading
01:40:56 HOL-Library: theory Lattice_Syntax
01:40:56 HOL-Library: theory AList
01:40:56 HOL-Library: theory BNF_Axiomatization
01:40:56 HOL-Library: theory BNF_Corec
01:40:56 HOL-Library: theory Stirling
01:40:56 HOL-Library: theory Bit
01:40:56 HOL-Library: theory Bits
01:40:56 HOL-Library: theory Boolean_Algebra
01:40:56 HOL-Library: theory Cancellation
01:40:56 HOL-Library: theory Cardinal_Notations
01:40:56 HOL-Library: theory Char_ord
01:40:56 HOL-Library: theory Code_Abstract_Nat
01:40:57 HOL-Library: theory Code_Binary_Nat
01:40:57 HOL-Library: theory Code_Target_Nat
01:40:57 HOL-Library: theory Code_Char
01:40:57 HOL-Library: theory Code_Prolog
01:40:57 HOL-Library: theory Code_Test
01:40:57 HOL-Library: theory Multiset
01:40:57 HOL-Library: theory Combine_PER
01:40:57 HOL-Library: theory Complete_Partial_Order2
01:40:57 HOL-Library: theory Bits_Bit
01:40:57 HOL-Library: theory Debug
01:40:57 HOL-Library: theory Disjoint_Sets
01:40:58 HOL-Library: theory Dlist
01:40:58 HOL-Library: theory FSet
01:40:58 HOL-Library: theory Fraction_Field
01:40:59 HOL-Library: theory Fun_Lexorder
01:40:59 HOL-Library: theory FuncSet
01:40:59 HOL-Library: theory DAList
01:41:00 HOL-Library: theory Function_Algebras
01:41:00 HOL-Library: theory Code_Target_Int
01:41:00 HOL-Library: theory Function_Division
01:41:00 HOL-Library: theory Code_Target_Numeral
01:41:00 HOL-Library: theory Groups_Big_Fun
01:41:00 HOL-Library: theory IArray
01:41:00 HOL-Library: theory Infinite_Set
01:41:01 HOL-Library: theory LaTeXsugar
01:41:01 HOL-Library: theory Lattice_Constructions
01:41:01 HOL-Library: theory Omega_Words_Fun
01:41:01 HOL-Library: theory Ramsey
01:41:01 HOL-Library: theory ListVector
01:41:02 HOL-Library: theory List_lexord
01:41:02 HOL-Library: theory Mapping
01:41:02 HOL-Library: theory Misc_Numeric
01:41:02 HOL-Library: theory Misc_Typedef
01:41:02 HOL-Library: theory Bit_Representation
01:41:02 HOL-Library: theory Monad_Syntax
01:41:02 HOL-Library: theory More_List
01:41:03 HOL-Library: theory Nat_Bijection
01:41:03 HOL-Library: theory Old_Datatype
01:41:03 HOL-Library: theory Finite_Map
01:41:03 HOL-Library: theory Bits_Int
01:41:03 HOL-Library: theory Stream
01:41:04 HOL-Library: theory AList_Mapping
01:41:04 HOL-Library: theory Old_Recdef
01:41:05 HOL-Library: theory DAList_Multiset
01:41:05 HOL-Library: theory Multiset_Order
01:41:05 HOL-Library: theory Permutation
01:41:05 HOL-Library: theory Permutations
01:41:05 HOL-Library: theory Factorial_Ring
01:41:05 HOL-Library: theory Countable
01:41:05 HOL-Library: theory Bool_List_Representation
01:41:05 HOL-Library: theory Option_ord
01:41:06 HOL-Library: theory Parallel
01:41:06 HOL-Library: theory Perm
01:41:06 HOL-Library: theory Phantom_Type
01:41:06 HOL-Library: theory Predicate_Compile_Alternative_Defs
01:41:07 HOL-Library: theory Product_Lexorder
01:41:07 HOL-Library: theory Predicate_Compile_Quickcheck
01:41:07 HOL-Library: theory Product_Plus
01:41:07 HOL-Library: theory Quotient_Syntax
01:41:07 HOL-Library: theory Cardinality
01:41:07 HOL-Library: theory Product_Order
01:41:07 HOL-Library: theory Quotient_Option
01:41:07 HOL-Library: theory Quotient_Product
01:41:07 HOL-Library: theory Quotient_Set
01:41:07 HOL-Library: theory Quotient_Sum
01:41:07 HOL-Library: theory Quotient_Type
01:41:07 HOL-Library: theory Quotient_List
01:41:07 HOL-Library: theory RBT_Impl
01:41:07 HOL-Library: theory Finite_Lattice
01:41:08 HOL-Library: theory Reflection
01:41:08 HOL-Library: theory Refute
01:41:08 HOL-Library: theory Countable_Set
01:41:08 HOL-Library: theory Rewrite
01:41:08 HOL-Library: theory Set_Algebras
01:41:08 HOL-Library: theory Simps_Case_Conv
01:41:08 HOL-Library: theory State_Monad
01:41:08 HOL-Library: theory Extended
01:41:08 HOL-Library: theory Numeral_Type
01:41:09 HOL-Library: theory Countable_Complete_Lattices
01:41:09 HOL-Library: theory Countable_Set_Type
01:41:09 HOL-Library: theory Sublist
01:41:10 HOL-Library: theory Type_Length
01:41:10 HOL-Library: theory Prefix_Order
01:41:10 HOL-Library: theory Saturated
01:41:10 HOL-Library: theory Sublist_Order
01:41:10 HOL-Library: theory Polynomial
01:41:11 HOL-Library: theory BigO
01:41:11 HOL-Library: theory Code_Real_Approx_By_Float
01:41:12 HOL-Library: theory Diagonal_Subsequence
01:41:12 HOL-Library: theory Discrete
01:41:12 HOL-Library: theory Indicator_Function
01:41:13 HOL-Library: theory Lattice_Algebras
01:41:13 HOL-Library: theory Liminf_Limsup
01:41:13 HOL-Library: theory Log_Nat
01:41:13 HOL-Library: theory Lub_Glb
01:41:13 HOL-Library: theory Multiset_Permutations
01:41:13 HOL-Library: theory Nonpos_Ints
01:41:13 HOL-Library: theory OptionalSugar
01:41:13 HOL-Library: theory Order_Continuity
01:41:14 HOL-Library: theory Periodic_Fun
01:41:14 HOL-Library: theory Quadratic_Discriminant
01:41:14 HOL-Library: theory Sum_of_Squares
01:41:14 HOL-Library: theory Transitive_Closure_Table
01:41:15 HOL-Library: theory Tree
01:41:15 HOL-Library: theory Extended_Nat
01:41:15 HOL-Library: theory While_Combinator
01:41:16 HOL-Library: theory Bourbaki_Witt_Fixpoint
01:41:16 HOL-Library: theory Extended_Real
01:41:17 HOL-Library: theory Linear_Temporal_Logic_on_Streams
01:41:18 HOL-Library: theory Euclidean_Algorithm
01:41:19 HOL-Library: theory Word_Miscellaneous
01:41:19 HOL-Library: theory Preorder
01:41:19 HOL-Library: theory Word
01:41:20 HOL-Library: theory Function_Growth
01:41:20 HOL-Library: theory Tree_Multiset
01:41:21 HOL-Library: theory Fundamental_Theorem_Algebra
01:41:22 HOL-Library: theory Float
01:41:23 HOL-Library: theory Extended_Nonnegative_Real
01:41:27 HOL-Library: theory Old_SMT
01:41:31 HOL-Library: theory Normalized_Fraction
01:41:31 HOL-Library: theory Field_as_Ring
01:41:31 HOL-Library: theory Formal_Power_Series
01:41:34 HOL-Library: theory Polynomial_Factorial
01:41:38 HOL-Library: theory Polynomial_FPS
01:41:39 HOL-Library: theory Library
01:42:12 HOL-Library: theory RBT
01:42:14 HOL-Library: theory RBT_Mapping
01:42:14 HOL-Library: theory RBT_Set
01:44:58 Timing HOL-Library (8 threads, 147.683s elapsed time, 835.156s cpu time, 73.416s GC time, factor 5.66)
01:44:58 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library
01:44:58 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf
01:44:58 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf
01:44:58 Finished HOL-Library (0:04:05 elapsed time, 0:17:38 cpu time, factor 4.31)
01:45:01 Building HOL-Word ...
01:45:03 HOL-Word: theory Bit
01:45:03 HOL-Word: theory Bits
01:45:03 HOL-Word: theory Boolean_Algebra
01:45:03 HOL-Word: theory Misc_Numeric
01:45:03 HOL-Word: theory Phantom_Type
01:45:03 HOL-Word: theory Misc_Typedef
01:45:03 HOL-Word: theory Bit_Representation
01:45:05 HOL-Word: theory Bits_Bit
01:45:05 HOL-Word: theory Word_Miscellaneous
01:45:05 HOL-Word: theory Bits_Int
01:45:05 HOL-Word: theory Cardinality
01:45:07 HOL-Word: theory Numeral_Type
01:45:07 HOL-Word: theory Bool_List_Representation
01:45:08 HOL-Word: theory Type_Length
01:45:09 HOL-Word: theory Word
01:45:36 Timing HOL-Word (8 threads, 13.204s elapsed time, 61.464s cpu time, 1.956s GC time, factor 4.65)
01:45:36 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word
01:45:36 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf
01:45:36 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf
01:45:36 Finished HOL-Word (0:00:34 elapsed time, 0:01:46 cpu time, factor 3.06)
01:45:36 Building AWN ...
01:45:39 AWN: theory Lib
01:45:39 AWN: theory TransitionSystems
01:45:39 AWN: theory AWN
01:45:39 AWN: theory Invariants
01:45:40 AWN: theory OInvariants
01:45:54 AWN: theory AWN_SOS
01:45:54 AWN: theory OAWN_SOS
01:45:54 AWN: theory AWN_Cterms
01:45:58 AWN: theory AWN_Labels
01:46:00 AWN: theory Inv_Cterms
01:46:01 AWN: theory AWN_Invariants
01:46:01 AWN: theory Pnet
01:46:02 AWN: theory AWN_SOS_Labels
01:46:02 AWN: theory Closed
01:46:03 AWN: theory Qmsg
01:46:04 AWN: theory OAWN_Invariants
01:46:04 AWN: theory OAWN_SOS_Labels
01:46:04 AWN: theory OPnet
01:46:04 AWN: theory ONode_Lifting
01:46:05 AWN: theory OPnet_Lifting
01:46:06 AWN: theory OClosed_Lifting
01:46:06 AWN: theory OClosed_Transfer
01:46:06 AWN: theory OAWN_Convert
01:46:06 AWN: theory Qmsg_Lifting
01:46:07 AWN: theory AWN_Main
01:46:08 AWN: theory Toy
01:47:01 Timing AWN (8 threads, 49.909s elapsed time, 248.708s cpu time, 7.516s GC time, factor 4.98)
01:47:01 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN
01:47:01 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf
01:47:01 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf
01:47:01 Finished AWN (0:01:24 elapsed time, 0:05:30 cpu time, factor 3.92)
01:47:01 Building ConcurrentIMP ...
01:47:10 ConcurrentIMP: theory CIMP_pred
01:47:10 ConcurrentIMP: theory CIMP_lang
01:47:23 ConcurrentIMP: theory CIMP_vcg
01:47:25 ConcurrentIMP: theory CIMP
01:47:26 ConcurrentIMP: theory CIMP_one_place_buffer_ex
01:47:26 ConcurrentIMP: theory CIMP_unbounded_buffer_ex
01:48:01 Timing ConcurrentIMP (8 threads, 21.431s elapsed time, 52.108s cpu time, 2.640s GC time, factor 2.43)
01:48:01 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP
01:48:01 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf
01:48:01 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf
01:48:01 Finished ConcurrentIMP (0:00:59 elapsed time, 0:02:16 cpu time, factor 2.29)
01:48:01 Building Word_Lib ...
01:48:04 Word_Lib: theory Sublist
01:48:04 Word_Lib: theory WordBitwise
01:48:06 Word_Lib: theory Prefix_Order
01:48:07 Word_Lib: theory HOL_Lemmas
01:48:07 Word_Lib: theory Enumeration
01:48:07 Word_Lib: theory More_Divides
01:48:07 Word_Lib: theory Hex_Words
01:48:07 Word_Lib: theory Signed_Words
01:48:07 Word_Lib: theory Norm_Words
01:48:07 Word_Lib: theory WordBitwise_Signed
01:48:07 Word_Lib: theory Word_Syntax
01:48:08 Word_Lib: theory Word_Lib
01:48:09 Word_Lib: theory Aligned
01:48:09 Word_Lib: theory Word_Enum
01:48:09 Word_Lib: theory Word_Setup_32
01:48:09 Word_Lib: theory Word_Setup_64
01:48:10 Word_Lib: theory Word_Lemmas
01:48:16 Word_Lib: theory Word_Lemmas_32
01:48:16 Word_Lib: theory Word_Lemmas_64
01:49:32 Timing Word_Lib (8 threads, 71.347s elapsed time, 179.612s cpu time, 3.312s GC time, factor 2.52)
01:49:32 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib
01:49:32 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf
01:49:32 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf
01:49:32 Finished Word_Lib (0:01:30 elapsed time, 0:03:38 cpu time, factor 2.41)
01:49:32 Building IP_Addresses ...
01:49:36 IP_Addresses: theory Cancellation
01:49:36 IP_Addresses: theory Char_ord
01:49:36 IP_Addresses: theory Code_Target_Int
01:49:36 IP_Addresses: theory Infinite_Set
01:49:36 IP_Addresses: theory Code_Abstract_Nat
01:49:36 IP_Addresses: theory Option_ord
01:49:36 IP_Addresses: theory NumberWang_IPv4
01:49:36 IP_Addresses: theory NumberWang_IPv6
01:49:36 IP_Addresses: theory Word_More
01:49:36 IP_Addresses: theory Code_Target_Nat
01:49:37 IP_Addresses: theory Code_Char
01:49:37 IP_Addresses: theory Multiset
01:49:44 IP_Addresses: theory Quicksort
01:49:44 IP_Addresses: theory List_More
01:49:45 IP_Addresses: theory Misc
01:50:12 IP_Addresses: theory Lib_Numbers_toString
01:50:12 IP_Addresses: theory Product_Lexorder
01:50:12 IP_Addresses: theory Word_Next
01:50:12 IP_Addresses: theory Hs_Compat
01:50:13 IP_Addresses: theory Lib_List_toString
01:50:13 IP_Addresses: theory Lib_Word_toString
01:50:13 IP_Addresses: theory WordInterval
01:50:19 IP_Addresses: theory IP_Address
01:50:19 IP_Addresses: theory WordInterval_Sorted
01:50:23 IP_Addresses: theory IPv4
01:50:24 IP_Addresses: theory IPv6
01:50:25 IP_Addresses: theory Prefix_Match
01:50:26 IP_Addresses: theory CIDR_Split
01:51:56 IP_Addresses: theory IP_Address_Parser
01:51:56 IP_Addresses: theory IP_Address_toString
01:56:25 Timing IP_Addresses (8 threads, 354.840s elapsed time, 1039.320s cpu time, 55.648s GC time, factor 2.93)
01:56:25 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses
01:56:25 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf
01:56:25 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf
01:56:25 Finished IP_Addresses (0:06:52 elapsed time, 0:19:57 cpu time, factor 2.90)
01:56:26 Building Simple_Firewall ...
01:56:32 Simple_Firewall: theory Iface
01:56:32 Simple_Firewall: theory Firewall_Common_Decision_State
01:56:32 Simple_Firewall: theory GroupF
01:56:32 Simple_Firewall: theory IP_Partition_Preliminaries
01:56:32 Simple_Firewall: theory Lib_Enum_toString
01:56:32 Simple_Firewall: theory Option_Helpers
01:56:32 Simple_Firewall: theory List_Product_More
01:56:32 Simple_Firewall: theory IP_Addr_WordInterval_toString
01:56:33 Simple_Firewall: theory L4_Protocol
01:56:38 Simple_Firewall: theory Simple_Packet
01:56:38 Simple_Firewall: theory Primitives_toString
01:56:41 Simple_Firewall: theory SimpleFw_Syntax
01:56:45 Simple_Firewall: theory SimpleFw_Semantics
01:56:48 Simple_Firewall: theory Generic_SimpleFw
01:56:48 Simple_Firewall: theory Shadowed
01:56:48 Simple_Firewall: theory Service_Matrix
01:57:27 Timing Simple_Firewall (8 threads, 25.657s elapsed time, 99.792s cpu time, 3.976s GC time, factor 3.89)
01:57:27 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall
01:57:27 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf
01:57:27 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf
01:57:27 Finished Simple_Firewall (0:01:01 elapsed time, 0:03:03 cpu time, factor 2.99)
01:57:28 Building Routing ...
01:57:35 Routing: theory Adhoc_Overloading
01:57:35 Routing: theory Monad_Syntax
01:57:35 Routing: theory Linorder_Helper
01:57:35 Routing: theory Prefix_Match_toString
01:57:37 Routing: theory Routing_Table
01:57:41 Routing: theory IpRoute_Parser
01:57:42 Routing: theory Linux_Router
01:58:08 Timing Routing (8 threads, 12.912s elapsed time, 45.356s cpu time, 0.976s GC time, factor 3.51)
01:58:08 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing
01:58:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf
01:58:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf
01:58:08 Finished Routing (0:00:39 elapsed time, 0:01:38 cpu time, factor 2.48)
01:58:08 Building Iptables_Semantics ...
01:58:16 Iptables_Semantics: theory LaTeXsugar
01:58:16 Iptables_Semantics: theory More_Bits_Int
01:58:16 Iptables_Semantics: theory Negation_Type
01:58:16 Iptables_Semantics: theory List_Misc
01:58:18 Iptables_Semantics: theory WordInterval_Lists
01:58:19 Iptables_Semantics: theory Bits_Integer
01:58:31 Iptables_Semantics: theory Code_Target_Bits_Int
01:58:34 Iptables_Semantics: theory Datatype_Selectors
01:58:34 Iptables_Semantics: theory Conntrack_State
01:58:34 Iptables_Semantics: theory Negation_Type_DNF
01:58:34 Iptables_Semantics: theory Remdups_Rev
01:58:34 Iptables_Semantics: theory Repeat_Stabilize
01:58:34 Iptables_Semantics: theory Ternary
01:58:34 Iptables_Semantics: theory SimpleFw_toString
01:58:34 Iptables_Semantics: theory L4_Protocol_Flags
01:58:35 Iptables_Semantics: theory IpAddresses
01:58:35 Iptables_Semantics: theory Firewall_Common
01:58:35 Iptables_Semantics: theory Word_Upto
01:58:36 Iptables_Semantics: theory Ports
01:58:36 Iptables_Semantics: theory Tagged_Packet
01:58:39 Iptables_Semantics: theory Common_Primitive_Syntax
01:58:55 Iptables_Semantics: theory Semantics
01:58:55 Iptables_Semantics: theory Semantics_Goto
01:58:55 Iptables_Semantics: theory Matching_Ternary
01:58:57 Iptables_Semantics: theory Matching
01:58:57 Iptables_Semantics: theory Semantics_Stateful
01:58:57 Iptables_Semantics: theory Ruleset_Update
01:58:58 Iptables_Semantics: theory Call_Return_Unfolding
01:58:59 Iptables_Semantics: theory Semantics_Ternary
01:58:59 Iptables_Semantics: theory Unknown_Match_Tacs
01:59:00 Iptables_Semantics: theory Matching_Embeddings
01:59:00 Iptables_Semantics: theory Fixed_Action
01:59:01 Iptables_Semantics: theory Optimizing
01:59:01 Iptables_Semantics: theory Common_Primitive_Matcher_Generic
01:59:01 Iptables_Semantics: theory Normalized_Matches
01:59:03 Iptables_Semantics: theory Negation_Type_Matching
01:59:05 Iptables_Semantics: theory Primitive_Normalization
01:59:07 Iptables_Semantics: theory Common_Primitive_Matcher
01:59:10 Iptables_Semantics: theory MatchExpr_Fold
01:59:10 Iptables_Semantics: theory Ipassmt
01:59:14 Iptables_Semantics: theory Routing_IpAssmt
02:00:07 Iptables_Semantics: theory Common_Primitive_Lemmas
02:00:07 Iptables_Semantics: theory Conntrack_State_Transform
02:00:07 Iptables_Semantics: theory Example_Semantics
02:00:07 Iptables_Semantics: theory Common_Primitive_toString
02:00:07 Iptables_Semantics: theory Interfaces_Normalize
02:00:07 Iptables_Semantics: theory IpAddresses_Normalize
02:00:07 Iptables_Semantics: theory Ports_Normalize
02:00:07 Iptables_Semantics: theory No_Spoof
02:00:07 Iptables_Semantics: theory Protocols_Normalize
02:00:18 Iptables_Semantics: theory Output_Interface_Replace
02:00:26 Iptables_Semantics: theory Interface_Replace
02:00:30 Iptables_Semantics: theory Transform
02:00:36 Iptables_Semantics: theory Primitive_Abstract
02:00:37 Iptables_Semantics: theory SimpleFw_Compliance
02:00:44 Iptables_Semantics: theory Code_Interface
02:00:44 Iptables_Semantics: theory Semantics_Embeddings
02:00:45 Iptables_Semantics: theory Iptables_Semantics
02:00:45 Iptables_Semantics: theory No_Spoof_Embeddings
02:00:55 Iptables_Semantics: theory Parser
02:00:55 Iptables_Semantics: theory Documentation
02:00:55 Iptables_Semantics: theory Code_haskell
02:02:40 Timing Iptables_Semantics (8 threads, 182.820s elapsed time, 778.536s cpu time, 59.468s GC time, factor 4.26)
02:02:40 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics
02:02:40 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf
02:02:40 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf
02:02:40 Finished Iptables_Semantics (0:04:31 elapsed time, 0:17:14 cpu time, factor 3.81)
02:02:42 Building HOL-Analysis ...
02:02:46 HOL-Analysis: theory Disjoint_Sets
02:02:46 HOL-Analysis: theory Cancellation
02:02:46 HOL-Analysis: theory FuncSet
02:02:46 HOL-Analysis: theory Nat_Bijection
02:02:46 HOL-Analysis: theory Infinite_Set
02:02:46 HOL-Analysis: theory Old_Datatype
02:02:46 HOL-Analysis: theory Phantom_Type
02:02:46 HOL-Analysis: theory Product_Plus
02:02:47 HOL-Analysis: theory Product_Order
02:02:47 HOL-Analysis: theory Set_Algebras
02:02:47 HOL-Analysis: theory L2_Norm
02:02:47 HOL-Analysis: theory Discrete
02:02:47 HOL-Analysis: theory Multiset
02:02:47 HOL-Analysis: theory Indicator_Function
02:02:47 HOL-Analysis: theory Inner_Product
02:02:47 HOL-Analysis: theory Liminf_Limsup
02:02:47 HOL-Analysis: theory Nonpos_Ints
02:02:48 HOL-Analysis: theory Operator_Norm
02:02:48 HOL-Analysis: theory Cardinality
02:02:48 HOL-Analysis: theory Periodic_Fun
02:02:48 HOL-Analysis: theory Poly_Roots
02:02:48 HOL-Analysis: theory Sum_of_Squares
02:02:49 HOL-Analysis: theory Countable
02:02:49 HOL-Analysis: theory Product_Vector
02:02:50 HOL-Analysis: theory Numeral_Type
02:02:50 HOL-Analysis: theory Euclidean_Space
02:02:51 HOL-Analysis: theory Countable_Set
02:02:52 HOL-Analysis: theory Countable_Complete_Lattices
02:02:52 HOL-Analysis: theory Continuum_Not_Denumerable
02:02:53 HOL-Analysis: theory Norm_Arith
02:02:53 HOL-Analysis: theory Finite_Cartesian_Product
02:02:53 HOL-Analysis: theory Linear_Algebra
02:02:54 HOL-Analysis: theory Permutations
02:02:54 HOL-Analysis: theory Factorial_Ring
02:02:56 HOL-Analysis: theory Order_Continuity
02:02:57 HOL-Analysis: theory Extended_Nat
02:02:57 HOL-Analysis: theory Topology_Euclidean_Space
02:02:59 HOL-Analysis: theory Extended_Real
02:03:05 HOL-Analysis: theory Extended_Nonnegative_Real
02:03:05 HOL-Analysis: theory Summation_Tests
02:03:07 HOL-Analysis: theory Euclidean_Algorithm
02:03:08 HOL-Analysis: theory Sigma_Algebra
02:03:12 HOL-Analysis: theory Bounded_Linear_Function
02:03:12 HOL-Analysis: theory Convex_Euclidean_Space
02:03:12 HOL-Analysis: theory Tagged_Division
02:03:12 HOL-Analysis: theory Extended_Real_Limits
02:03:12 HOL-Analysis: theory Uniform_Limit
02:03:13 HOL-Analysis: theory Measurable
02:03:14 HOL-Analysis: theory Measure_Space
02:03:19 HOL-Analysis: theory Caratheodory
02:03:20 HOL-Analysis: theory Primes
02:03:21 HOL-Analysis: theory Continuous_Extension
02:03:21 HOL-Analysis: theory Path_Connected
02:03:28 HOL-Analysis: theory Homeomorphism
02:03:29 HOL-Analysis: theory Brouwer_Fixpoint
02:03:32 HOL-Analysis: theory Derivative
02:03:36 HOL-Analysis: theory Cartesian_Euclidean_Space
02:03:36 HOL-Analysis: theory Weierstrass_Theorems
02:03:40 HOL-Analysis: theory Determinants
02:03:40 HOL-Analysis: theory Fashoda_Theorem
02:03:40 HOL-Analysis: theory Ordered_Euclidean_Space
02:03:40 HOL-Analysis: theory Polytope
02:03:48 HOL-Analysis: theory Arcwise_Connected
02:03:48 HOL-Analysis: theory Borel_Space
02:03:53 HOL-Analysis: theory Nonnegative_Lebesgue_Integration
02:03:53 HOL-Analysis: theory Regularity
02:03:56 HOL-Analysis: theory Binary_Product_Measure
02:03:57 HOL-Analysis: theory Finite_Product_Measure
02:03:57 HOL-Analysis: theory Embed_Measure
02:03:59 HOL-Analysis: theory Bochner_Integration
02:03:59 HOL-Analysis: theory Function_Topology
02:04:03 HOL-Analysis: theory Complete_Measure
02:04:03 HOL-Analysis: theory Radon_Nikodym
02:04:04 HOL-Analysis: theory Set_Integral
02:04:04 HOL-Analysis: theory Lebesgue_Measure
02:04:07 HOL-Analysis: theory Henstock_Kurzweil_Integration
02:04:13 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration
02:04:13 HOL-Analysis: theory Bounded_Continuous_Function
02:04:13 HOL-Analysis: theory Integral_Test
02:04:15 HOL-Analysis: theory Complex_Analysis_Basics
02:04:15 HOL-Analysis: theory Interval_Integral
02:04:17 HOL-Analysis: theory Lebesgue_Integral_Substitution
02:04:17 HOL-Analysis: theory Complex_Transcendental
02:04:22 HOL-Analysis: theory Generalised_Binomial_Theorem
02:04:22 HOL-Analysis: theory Cauchy_Integral_Theorem
02:04:22 HOL-Analysis: theory Harmonic_Numbers
02:04:22 HOL-Analysis: theory Further_Topology
02:04:27 HOL-Analysis: theory Jordan_Curve
02:04:29 HOL-Analysis: theory Conformal_Mappings
02:04:29 HOL-Analysis: theory Winding_Numbers
02:04:29 HOL-Analysis: theory Gamma_Function
02:04:32 HOL-Analysis: theory Great_Picard
02:04:36 HOL-Analysis: theory Analysis
02:12:02 Timing HOL-Analysis (8 threads, 439.587s elapsed time, 2087.720s cpu time, 132.424s GC time, factor 4.75)
02:12:02 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis
02:12:02 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/document.pdf
02:12:02 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/outline.pdf
02:12:02 Finished HOL-Analysis (0:09:19 elapsed time, 0:38:20 cpu time, factor 4.11)
02:12:04 Building Ordinary_Differential_Equations ...
02:12:11 Ordinary_Differential_Equations: theory Code_Abstract_Nat
02:12:11 Ordinary_Differential_Equations: theory Code_Target_Int
02:12:11 Ordinary_Differential_Equations: theory Log_Nat
02:12:11 Ordinary_Differential_Equations: theory Dense_Linear_Order
02:12:11 Ordinary_Differential_Equations: theory Diagonal_Subsequence
02:12:11 Ordinary_Differential_Equations: theory Lattice_Algebras
02:12:11 Ordinary_Differential_Equations: theory Code_Target_Nat
02:12:12 Ordinary_Differential_Equations: theory Code_Target_Numeral
02:12:19 Ordinary_Differential_Equations: theory Float
02:12:23 Ordinary_Differential_Equations: theory Approximation
02:13:26 Ordinary_Differential_Equations: theory ODE_Auxiliarities
02:13:26 Ordinary_Differential_Equations: theory Bounded_Linear_Operator
02:13:32 Ordinary_Differential_Equations: theory Initial_Value_Problem
02:13:32 Ordinary_Differential_Equations: theory MVT_Ex
02:13:32 Ordinary_Differential_Equations: theory Multivariate_Taylor
02:13:35 Ordinary_Differential_Equations: theory Picard_Lindeloef_Qualitative
02:13:36 Ordinary_Differential_Equations: theory Flow
02:13:41 Ordinary_Differential_Equations: theory Reachability_Analysis
02:13:41 Ordinary_Differential_Equations: theory Upper_Lower_Solution
02:13:41 Ordinary_Differential_Equations: theory Linear_ODE
02:13:44 Ordinary_Differential_Equations: theory ODE_Analysis
02:15:42 Timing Ordinary_Differential_Equations (8 threads, 172.472s elapsed time, 501.432s cpu time, 11.412s GC time, factor 2.91)
02:15:42 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations
02:15:42 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/document.pdf
02:15:42 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/outline.pdf
02:15:42 Finished Ordinary_Differential_Equations (0:03:37 elapsed time, 0:10:00 cpu time, factor 2.76)
02:15:43 Building HOL-ODE ...
02:16:09 Timing HOL-ODE (8 threads, 0.150s elapsed time, 0.180s cpu time, 0.000s GC time, factor 1.20)
02:16:09 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE
02:16:09 Finished HOL-ODE (0:00:26 elapsed time, 0:00:50 cpu time, factor 1.93)
02:16:09 Building HOL-ODE-Refinement ...
02:16:19 HOL-ODE-Refinement: theory AList
02:16:19 HOL-ODE-Refinement: theory Bit
02:16:19 HOL-ODE-Refinement: theory Adhoc_Overloading
02:16:19 HOL-ODE-Refinement: theory Bits
02:16:19 HOL-ODE-Refinement: theory Boolean_Algebra
02:16:19 HOL-ODE-Refinement: theory Quicksort
02:16:19 HOL-ODE-Refinement: theory Foldi
02:16:19 HOL-ODE-Refinement: theory Omega_Words_Fun
02:16:19 HOL-ODE-Refinement: theory List_More
02:16:19 HOL-ODE-Refinement: theory Misc_Numeric
02:16:19 HOL-ODE-Refinement: theory Misc_Typedef
02:16:19 HOL-ODE-Refinement: theory Bit_Representation
02:16:20 HOL-ODE-Refinement: theory Monad_Syntax
02:16:20 HOL-ODE-Refinement: theory Option_ord
02:16:20 HOL-ODE-Refinement: theory Type_Length
02:16:20 HOL-ODE-Refinement: theory Prio_List
02:16:20 HOL-ODE-Refinement: theory Bits_Bit
02:16:20 HOL-ODE-Refinement: theory RBT_Impl
02:16:20 HOL-ODE-Refinement: theory Refine_Chapter
02:16:20 HOL-ODE-Refinement: theory Refine_Util
02:16:20 HOL-ODE-Refinement: theory While_Combinator
02:16:20 HOL-ODE-Refinement: theory Word_Miscellaneous
02:16:20 HOL-ODE-Refinement: theory Misc
02:16:21 HOL-ODE-Refinement: theory Bits_Int
02:16:21 HOL-ODE-Refinement: theory Anti_Unification
02:16:21 HOL-ODE-Refinement: theory Attr_Comb
02:16:21 HOL-ODE-Refinement: theory Named_Sorted_Thms
02:16:21 HOL-ODE-Refinement: theory Autoref_Data
02:16:21 HOL-ODE-Refinement: theory Mk_Term_Antiquot
02:16:21 HOL-ODE-Refinement: theory Mpat_Antiquot
02:16:21 HOL-ODE-Refinement: theory Tagged_Solver
02:16:21 HOL-ODE-Refinement: theory Select_Solve
02:16:22 HOL-ODE-Refinement: theory Indep_Vars
02:16:22 HOL-ODE-Refinement: theory Mk_Record_Simp
02:16:23 HOL-ODE-Refinement: theory Bool_List_Representation
02:16:24 HOL-ODE-Refinement: theory More_Bits_Int
02:16:24 HOL-ODE-Refinement: theory Word
02:16:27 HOL-ODE-Refinement: theory Bits_Integer
02:16:28 HOL-ODE-Refinement: theory SetIterator
02:16:28 HOL-ODE-Refinement: theory Digraph_Basic
02:16:30 HOL-ODE-Refinement: theory Refine_Lib
02:16:31 HOL-ODE-Refinement: theory SetIteratorOperations
02:16:31 HOL-ODE-Refinement: theory Autoref_Phases
02:16:31 HOL-ODE-Refinement: theory Autoref_Tagging
02:16:31 HOL-ODE-Refinement: theory Refine_Mono_Prover
02:16:32 HOL-ODE-Refinement: theory Relators
02:16:32 HOL-ODE-Refinement: theory Word_Misc
02:16:33 HOL-ODE-Refinement: theory Param_Tool
02:16:33 HOL-ODE-Refinement: theory Param_HOL
02:16:34 HOL-ODE-Refinement: theory Assoc_List
02:16:35 HOL-ODE-Refinement: theory Proper_Iterator
02:16:35 HOL-ODE-Refinement: theory Parametricity
02:16:35 HOL-ODE-Refinement: theory Autoref_Id_Ops
02:16:35 HOL-ODE-Refinement: theory SetIteratorGA
02:16:35 HOL-ODE-Refinement: theory Diff_Array
02:16:36 HOL-ODE-Refinement: theory It_to_It
02:16:36 HOL-ODE-Refinement: theory Autoref_Fix_Rel
02:16:37 HOL-ODE-Refinement: theory Autoref_Translate
02:16:37 HOL-ODE-Refinement: theory Autoref_Relator_Interface
02:16:37 HOL-ODE-Refinement: theory Autoref_Gen_Algo
02:16:38 HOL-ODE-Refinement: theory Autoref_Tool
02:16:39 HOL-ODE-Refinement: theory Autoref_Bindings_HOL
02:16:45 HOL-ODE-Refinement: theory Automatic_Refinement
02:16:45 HOL-ODE-Refinement: theory Code_Target_Bits_Int
02:16:45 HOL-ODE-Refinement: theory Uint
02:16:45 HOL-ODE-Refinement: theory Idx_Iterator
02:16:45 HOL-ODE-Refinement: theory Intf_Comp
02:16:46 HOL-ODE-Refinement: theory Refine_Misc
02:16:46 HOL-ODE-Refinement: theory Code_Target_ICF
02:16:46 HOL-ODE-Refinement: theory Impl_Array_Stack
02:16:46 HOL-ODE-Refinement: theory Uint32
02:16:47 HOL-ODE-Refinement: theory RefineG_Domain
02:16:47 HOL-ODE-Refinement: theory RefineG_Transfer
02:16:48 HOL-ODE-Refinement: theory RefineG_Assert
02:16:48 HOL-ODE-Refinement: theory RefineG_Recursion
02:16:48 HOL-ODE-Refinement: theory Refine_Basic
02:16:48 HOL-ODE-Refinement: theory RefineG_While
02:16:49 HOL-ODE-Refinement: theory HashCode
02:16:49 HOL-ODE-Refinement: theory Refine_Det
02:16:50 HOL-ODE-Refinement: theory Intf_Hash
02:16:51 HOL-ODE-Refinement: theory Gen_Hash
02:16:53 HOL-ODE-Refinement: theory Refine_Heuristics
02:16:53 HOL-ODE-Refinement: theory Refine_Leof
02:16:53 HOL-ODE-Refinement: theory Refine_Pfun
02:16:53 HOL-ODE-Refinement: theory Refine_While
02:16:56 HOL-ODE-Refinement: theory Refine_Transfer
02:16:56 HOL-ODE-Refinement: theory Autoref_Monadic
02:16:56 HOL-ODE-Refinement: theory Refine_Automation
02:16:57 HOL-ODE-Refinement: theory Refine_Foreach
02:17:00 HOL-ODE-Refinement: theory Refine_Monadic
02:17:01 HOL-ODE-Refinement: theory Gen_Iterator
02:17:01 HOL-ODE-Refinement: theory Intf_Map
02:17:01 HOL-ODE-Refinement: theory Intf_Set
02:17:02 HOL-ODE-Refinement: theory Impl_Cfun_Set
02:17:02 HOL-ODE-Refinement: theory Iterator
02:17:03 HOL-ODE-Refinement: theory Array_Iterator
02:17:03 HOL-ODE-Refinement: theory Gen_Map
02:17:03 HOL-ODE-Refinement: theory Gen_Map2Set
02:17:03 HOL-ODE-Refinement: theory Gen_Set
02:17:03 HOL-ODE-Refinement: theory Impl_Bit_Set
02:17:03 HOL-ODE-Refinement: theory Impl_List_Set
02:17:04 HOL-ODE-Refinement: theory Impl_Uv_Set
02:17:04 HOL-ODE-Refinement: theory Impl_Array_Map
02:17:04 HOL-ODE-Refinement: theory Impl_List_Map
02:17:06 HOL-ODE-Refinement: theory Impl_Array_Hash_Map
02:17:19 HOL-ODE-Refinement: theory RBT_add
02:17:22 HOL-ODE-Refinement: theory Impl_RBT_Map
02:17:32 HOL-ODE-Refinement: theory GenCF_No_Comp
02:17:39 HOL-ODE-Refinement: theory Refine_Dflt_No_Comp
02:19:11 Timing HOL-ODE-Refinement (8 threads, 115.581s elapsed time, 610.992s cpu time, 27.820s GC time, factor 5.29)
02:19:11 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Refinement
02:19:11 Finished HOL-ODE-Refinement (0:03:01 elapsed time, 0:14:05 cpu time, factor 4.66)
02:19:13 Building HOL-ODE-Numerics ...
02:19:29 HOL-ODE-Numerics: theory Float_Real
02:19:29 HOL-ODE-Numerics: theory Quotient_Syntax
02:19:29 HOL-ODE-Numerics: theory Permutation
02:19:29 HOL-ODE-Numerics: theory Counterclockwise
02:19:29 HOL-ODE-Numerics: theory Euclidean_Space_Explicit
02:19:29 HOL-ODE-Numerics: theory Quotient_Set
02:19:30 HOL-ODE-Numerics: theory Executable_Euclidean_Space
02:19:30 HOL-ODE-Numerics: theory Affine_Form
02:19:31 HOL-ODE-Numerics: theory Counterclockwise_Vector
02:19:32 HOL-ODE-Numerics: theory Counterclockwise_2D_Strict
02:19:33 HOL-ODE-Numerics: theory Counterclockwise_2D_Arbitrary
02:19:33 HOL-ODE-Numerics: theory Polygon
02:19:34 HOL-ODE-Numerics: theory Affine_Approximation
02:19:57 HOL-ODE-Numerics: theory Affine_Code
02:19:58 HOL-ODE-Numerics: theory Straight_Line_Program
02:20:00 HOL-ODE-Numerics: theory Ex_Affine_Approximation
02:20:01 HOL-ODE-Numerics: theory Ex_Ineqs
02:20:01 HOL-ODE-Numerics: theory Intersection
02:20:06 HOL-ODE-Numerics: theory Ex_Inter
02:21:29 HOL-ODE-Numerics: theory Affine_Arithmetic
02:21:30 HOL-ODE-Numerics: theory ICF_Tools
02:21:30 HOL-ODE-Numerics: theory Generator_Aux
02:21:30 HOL-ODE-Numerics: theory Derive_Manager
02:21:30 HOL-ODE-Numerics: theory Optimize_Integer
02:21:30 HOL-ODE-Numerics: theory One_Step_Method
02:21:30 HOL-ODE-Numerics: theory Autoref_Misc
02:21:30 HOL-ODE-Numerics: theory Char_ord
02:21:30 HOL-ODE-Numerics: theory Ord_Code_Preproc
02:21:31 HOL-ODE-Numerics: theory Show
02:21:31 HOL-ODE-Numerics: theory Code_Char
02:21:31 HOL-ODE-Numerics: theory Locale_Code
02:21:31 HOL-ODE-Numerics: theory Optimize_Float
02:21:32 HOL-ODE-Numerics: theory Runge_Kutta
02:21:32 HOL-ODE-Numerics: theory Show_Instances
02:21:34 HOL-ODE-Numerics: theory Print
02:21:38 HOL-ODE-Numerics: theory Refine_Folds
02:21:38 HOL-ODE-Numerics: theory Refine_String
02:21:38 HOL-ODE-Numerics: theory Weak_Set
02:21:41 HOL-ODE-Numerics: theory Plot
02:21:50 HOL-ODE-Numerics: theory Refine_Rigorous_Numerics
02:22:19 HOL-ODE-Numerics: theory Refine_Reachability_Analysis
02:33:00 HOL-ODE-Numerics: theory Refine_Rigorous_Numerics_Aform
02:33:11 HOL-ODE-Numerics: theory ODE_Numerics
02:34:31 Timing HOL-ODE-Numerics (8 threads, 837.180s elapsed time, 2030.584s cpu time, 71.968s GC time, factor 2.43)
02:34:31 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Numerics
02:34:31 Finished HOL-ODE-Numerics (0:15:17 elapsed time, 0:37:00 cpu time, factor 2.42)
02:34:32 Running Flyspeck-Tame ...
02:34:41 Flyspeck-Tame: theory Trie
02:34:43 Flyspeck-Tame: theory Tries
02:35:04 Flyspeck-Tame: theory Arch
02:35:04 Flyspeck-Tame: theory IArray_Syntax
02:35:04 Flyspeck-Tame: theory ListAux
02:35:04 Flyspeck-Tame: theory Quasi_Order
02:35:04 Flyspeck-Tame: theory RTranCl
02:35:05 Flyspeck-Tame: theory PlaneGraphIso
02:35:05 Flyspeck-Tame: theory Worklist
02:35:06 Flyspeck-Tame: theory Maps
02:35:06 Flyspeck-Tame: theory ListSum
02:35:06 Flyspeck-Tame: theory Rotation
02:35:07 Flyspeck-Tame: theory Graph
02:35:09 Flyspeck-Tame: theory Enumerator
02:35:09 Flyspeck-Tame: theory FaceDivision
02:35:09 Flyspeck-Tame: theory GraphProps
02:35:09 Flyspeck-Tame: theory Tame
02:35:10 Flyspeck-Tame: theory Plane
02:35:10 Flyspeck-Tame: theory EnumeratorProps
02:35:10 Flyspeck-Tame: theory TameProps
02:35:10 Flyspeck-Tame: theory Plane1
02:35:10 Flyspeck-Tame: theory FaceDivisionProps
02:35:11 Flyspeck-Tame: theory Generator
02:35:11 Flyspeck-Tame: theory TameEnum
02:35:14 Flyspeck-Tame: theory Invariants
02:35:18 Flyspeck-Tame: theory PlaneProps
02:35:19 Flyspeck-Tame: theory Plane1Props
02:35:19 Flyspeck-Tame: theory ScoreProps
02:35:21 Flyspeck-Tame: theory LowerBound
02:35:21 Flyspeck-Tame: theory GeneratorProps
02:35:22 Flyspeck-Tame: theory TameEnumProps
02:35:25 Flyspeck-Tame: theory ArchCompAux
02:35:26 Flyspeck-Tame: theory ArchCompProps
02:35:27 Flyspeck-Tame: theory ArchComp
02:35:27 Flyspeck-Tame: theory Completeness
10:06:57 Timing Flyspeck-Tame (8 threads, 27125.152s elapsed time, 40470.512s cpu time, 667.188s GC time, factor 1.49)
10:06:57 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame
10:06:57 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf
10:06:57 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf
10:06:57 Finished Flyspeck-Tame (7:32:24 elapsed time, 11:14:52 cpu time, factor 1.49)
10:06:57 Running Iptables_Semantics_Examples ...
10:07:13 Iptables_Semantics_Examples: theory Analyze_Ringofsaturn_com
10:07:13 Iptables_Semantics_Examples: theory Analyze_SQRL_Shorewall
10:07:13 Iptables_Semantics_Examples: theory Analyze_medium_sized_company
10:07:13 Iptables_Semantics_Examples: theory Analyze_TUM_Net_Firewall
10:07:13 Iptables_Semantics_Examples: theory Analyze_topos_generated
10:07:13 Iptables_Semantics_Examples: theory Contrived_Example
10:07:13 Iptables_Semantics_Examples: theory IP_Address_Space_Examples_All_Small
10:07:13 Iptables_Semantics_Examples: theory Parser_Test
10:07:22 Iptables_Semantics_Examples: theory SNS_IAS_Eduroam_Spoofing
10:07:22 Iptables_Semantics_Examples: theory SQRL_2015_nospoof
10:07:23 Iptables_Semantics_Examples: theory TUM_Spoofing_new3
10:07:24 Iptables_Semantics_Examples: theory Parser6
10:07:25 Iptables_Semantics_Examples: theory Parser6_Test
10:07:32 Iptables_Semantics_Examples: theory Ports_Fail
10:07:33 Iptables_Semantics_Examples: theory Small_Examples
10:07:33 Iptables_Semantics_Examples: theory iptables_Ln_tuned_parsed
10:07:35 Iptables_Semantics_Examples: theory Analyze_Synology_Diskstation
10:11:23 Iptables_Semantics_Examples: theory IP_Address_Space_Examples_All_Large
11:34:18 Iptables_Semantics_Examples: theory TUM_Simple_FW
13:06:01 Timing Iptables_Semantics_Examples (8 threads, 10723.931s elapsed time, 66788.764s cpu time, 9267.492s GC time, factor 6.23)
13:06:01 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples
13:06:01 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf
13:06:01 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf
13:06:01 Finished Iptables_Semantics_Examples (2:59:03 elapsed time, 18:33:37 cpu time, factor 6.22)
13:06:02 Running AODV ...
13:06:06 AODV: theory Aodv_Basic
13:06:08 AODV: theory A_Norreqid
13:06:08 AODV: theory Aodv_Data
13:06:08 AODV: theory Aodv_Message
13:06:08 AODV: theory C_Gtobcast
13:06:08 AODV: theory E_All_ABCD
13:06:08 AODV: theory D_Fwdrreqs
13:06:08 AODV: theory B_Fwdrreps
13:06:08 AODV: theory A_Aodv_Data
13:06:08 AODV: theory A_Aodv_Message
13:06:08 AODV: theory B_Aodv_Data
13:06:08 AODV: theory B_Aodv_Message
13:06:08 AODV: theory C_Aodv_Message
13:06:08 AODV: theory C_Aodv_Data
13:06:10 AODV: theory C_Fresher
13:06:10 AODV: theory D_Aodv_Data
13:06:10 AODV: theory Fresher
13:06:10 AODV: theory A_Fresher
13:06:10 AODV: theory B_Fresher
13:06:10 AODV: theory D_Aodv_Message
13:06:11 AODV: theory E_Aodv_Data
13:06:11 AODV: theory E_Aodv_Message
13:06:11 AODV: theory A_Aodv
13:06:11 AODV: theory Aodv
13:06:11 AODV: theory B_Aodv
13:06:11 AODV: theory C_Aodv
13:06:12 AODV: theory E_Fresher
13:06:12 AODV: theory D_Fresher
13:06:12 AODV: theory D_Aodv
13:06:13 AODV: theory E_Aodv
13:07:15 AODV: theory C_Aodv_Predicates
13:07:15 AODV: theory C_Loop_Freedom
13:07:15 AODV: theory C_Quality_Increases
13:07:16 AODV: theory C_Seq_Invariants
13:07:16 AODV: theory C_OAodv
13:07:17 AODV: theory C_Global_Invariants
13:07:18 AODV: theory C_Aodv_Loop_Freedom
13:07:33 AODV: theory A_Aodv_Predicates
13:07:33 AODV: theory A_Loop_Freedom
13:07:33 AODV: theory A_Quality_Increases
13:07:33 AODV: theory A_Seq_Invariants
13:07:34 AODV: theory A_OAodv
13:07:35 AODV: theory A_Global_Invariants
13:07:36 AODV: theory A_Aodv_Loop_Freedom
13:07:45 AODV: theory Aodv_Predicates
13:07:46 AODV: theory OAodv
13:07:46 AODV: theory Loop_Freedom
13:07:46 AODV: theory Quality_Increases
13:07:46 AODV: theory Seq_Invariants
13:07:47 AODV: theory Global_Invariants
13:07:48 AODV: theory Aodv_Loop_Freedom
13:07:49 AODV: theory E_Aodv_Predicates
13:07:49 AODV: theory E_OAodv
13:07:50 AODV: theory E_Loop_Freedom
13:07:50 AODV: theory E_Quality_Increases
13:07:50 AODV: theory E_Seq_Invariants
13:07:51 AODV: theory B_Aodv_Predicates
13:07:51 AODV: theory B_OAodv
13:07:51 AODV: theory E_Global_Invariants
13:07:51 AODV: theory B_Loop_Freedom
13:07:51 AODV: theory B_Quality_Increases
13:07:52 AODV: theory B_Seq_Invariants
13:07:52 AODV: theory E_Aodv_Loop_Freedom
13:07:53 AODV: theory B_Global_Invariants
13:07:54 AODV: theory B_Aodv_Loop_Freedom
13:08:03 AODV: theory D_Aodv_Predicates
13:08:03 AODV: theory D_OAodv
13:08:03 AODV: theory D_Loop_Freedom
13:08:03 AODV: theory D_Quality_Increases
13:08:03 AODV: theory D_Seq_Invariants
13:08:04 AODV: theory D_Global_Invariants
13:08:05 AODV: theory D_Aodv_Loop_Freedom
13:08:11 AODV: theory All
15:46:39 Timing AODV (8 threads, 9621.700s elapsed time, 50643.528s cpu time, 3866.604s GC time, factor 5.26)
15:46:39 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV
15:46:39 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/document.pdf
15:46:39 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/outline.pdf
15:46:39 Finished AODV (2:40:37 elapsed time, 14:04:25 cpu time, factor 5.26)
15:46:40 Running ConcurrentGC ...
15:46:50 ConcurrentGC: theory Model
15:47:09 ConcurrentGC: theory Tactics
15:47:17 ConcurrentGC: theory Proofs_basis
15:47:21 ConcurrentGC: theory TSO
15:47:37 ConcurrentGC: theory Handshakes
15:50:15 ConcurrentGC: theory MarkObject
15:53:08 ConcurrentGC: theory StrongTricolour
15:54:12 ConcurrentGC: theory Proofs
15:54:14 ConcurrentGC: theory Concrete_heap
15:54:15 ConcurrentGC: theory Concrete
18:02:10 Timing ConcurrentGC (8 threads, 8116.143s elapsed time, 26855.636s cpu time, 2320.920s GC time, factor 3.31)
18:02:10 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC
18:02:10 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf
18:02:10 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf
18:02:10 Finished ConcurrentGC (2:15:29 elapsed time, 7:27:50 cpu time, factor 3.31)
18:02:10 Running JinjaThreads ...
18:02:19 JinjaThreads: theory Adhoc_Overloading
18:02:19 JinjaThreads: theory AList
18:02:19 JinjaThreads: theory Cancellation
18:02:19 JinjaThreads: theory Lattice_Syntax
18:02:19 JinjaThreads: theory Char_ord
18:02:19 JinjaThreads: theory Code_Abstract_Nat
18:02:19 JinjaThreads: theory Dlist
18:02:19 JinjaThreads: theory FingerTree
18:02:19 JinjaThreads: theory Complete_Partial_Order2
18:02:19 JinjaThreads: theory Foldi
18:02:19 JinjaThreads: theory Code_Target_Nat
18:02:19 JinjaThreads: theory Code_Char
18:02:19 JinjaThreads: theory Code_Target_Int
18:02:19 JinjaThreads: theory ICF_Tools
18:02:20 JinjaThreads: theory Infinite_Set
18:02:20 JinjaThreads: theory Code_Target_Numeral
18:02:20 JinjaThreads: theory More_Bits_Int
18:02:20 JinjaThreads: theory Multiset
18:02:20 JinjaThreads: theory Monad_Syntax
18:02:20 JinjaThreads: theory Omega_Words_Fun
18:02:20 JinjaThreads: theory Nat_Bijection
18:02:21 JinjaThreads: theory Old_Datatype
18:02:21 JinjaThreads: theory Option_ord
18:02:22 JinjaThreads: theory Ord_Code_Preproc
18:02:22 JinjaThreads: theory Trie
18:02:22 JinjaThreads: theory FinFun
18:02:22 JinjaThreads: theory Locale_Code
18:02:22 JinjaThreads: theory Predicate_Compile_Alternative_Defs
18:02:23 JinjaThreads: theory Prio_List
18:02:23 JinjaThreads: theory RBT_Impl
18:02:23 JinjaThreads: theory Countable
18:02:23 JinjaThreads: theory Bits_Integer
18:02:24 JinjaThreads: theory Record_Intf
18:02:24 JinjaThreads: theory Refine_Chapter
18:02:24 JinjaThreads: theory Refine_Util
18:02:25 JinjaThreads: theory Set_Monad
18:02:25 JinjaThreads: theory Anti_Unification
18:02:25 JinjaThreads: theory Attr_Comb
18:02:25 JinjaThreads: theory Named_Sorted_Thms
18:02:25 JinjaThreads: theory Autoref_Data
18:02:25 JinjaThreads: theory Mk_Term_Antiquot
18:02:25 JinjaThreads: theory Mpat_Antiquot
18:02:25 JinjaThreads: theory Tagged_Solver
18:02:25 JinjaThreads: theory Select_Solve
18:02:25 JinjaThreads: theory Indep_Vars
18:02:26 JinjaThreads: theory Mk_Record_Simp
18:02:26 JinjaThreads: theory Set_without_equal
18:02:26 JinjaThreads: theory Simps_Case_Conv
18:02:26 JinjaThreads: theory Countable_Set
18:02:26 JinjaThreads: theory Sublist
18:02:26 JinjaThreads: theory Transitive_Closure_Table
18:02:26 JinjaThreads: theory While_Combinator
18:02:26 JinjaThreads: theory Auxiliary
18:02:27 JinjaThreads: theory Countable_Complete_Lattices
18:02:27 JinjaThreads: theory DatRef
18:02:27 JinjaThreads: theory Word_Misc
18:02:28 JinjaThreads: theory BinomialHeap
18:02:29 JinjaThreads: theory Quicksort
18:02:29 JinjaThreads: theory List_More
18:02:29 JinjaThreads: theory SkewBinomialHeap
18:02:30 JinjaThreads: theory Misc
18:02:31 JinjaThreads: theory Order_Continuity
18:02:33 JinjaThreads: theory Extended_Nat
18:02:35 JinjaThreads: theory Coinductive_Nat
18:02:38 JinjaThreads: theory Coinductive_List
18:02:41 JinjaThreads: theory SetIterator
18:02:41 JinjaThreads: theory Digraph_Basic
18:02:41 JinjaThreads: theory Sorted_List_Operations
18:02:41 JinjaThreads: theory Code_Target_Bits_Int
18:02:42 JinjaThreads: theory Code_Target_ICF
18:02:42 JinjaThreads: theory Uint32
18:02:42 JinjaThreads: theory Refine_Lib
18:02:43 JinjaThreads: theory SetIteratorOperations
18:02:44 JinjaThreads: theory Autoref_Phases
18:02:44 JinjaThreads: theory Autoref_Tagging
18:02:44 JinjaThreads: theory Refine_Mono_Prover
18:02:44 JinjaThreads: theory Relators
18:02:45 JinjaThreads: theory HashCode
18:02:45 JinjaThreads: theory Param_Tool
18:02:46 JinjaThreads: theory Param_HOL
18:02:47 JinjaThreads: theory Assoc_List
18:02:47 JinjaThreads: theory Dlist_add
18:02:47 JinjaThreads: theory Proper_Iterator
18:02:47 JinjaThreads: theory SetIteratorGA
18:02:48 JinjaThreads: theory Parametricity
18:02:48 JinjaThreads: theory Autoref_Id_Ops
18:02:48 JinjaThreads: theory Diff_Array
18:02:48 JinjaThreads: theory Trie_Impl
18:02:48 JinjaThreads: theory It_to_It
18:02:49 JinjaThreads: theory Trie2
18:02:49 JinjaThreads: theory Autoref_Fix_Rel
18:02:50 JinjaThreads: theory Lazy_LList
18:02:50 JinjaThreads: theory TLList
18:02:50 JinjaThreads: theory Autoref_Relator_Interface
18:02:50 JinjaThreads: theory Autoref_Translate
18:02:50 JinjaThreads: theory Autoref_Gen_Algo
18:02:50 JinjaThreads: theory Autoref_Tool
18:02:52 JinjaThreads: theory Autoref_Bindings_HOL
18:02:55 JinjaThreads: theory Lazy_TLList
18:02:58 JinjaThreads: theory Automatic_Refinement
18:02:58 JinjaThreads: theory Idx_Iterator
18:02:58 JinjaThreads: theory Refine_Misc
18:03:00 JinjaThreads: theory RefineG_Domain
18:03:00 JinjaThreads: theory RefineG_Transfer
18:03:00 JinjaThreads: theory RefineG_Assert
18:03:00 JinjaThreads: theory RefineG_Recursion
18:03:01 JinjaThreads: theory Refine_Basic
18:03:01 JinjaThreads: theory RefineG_While
18:03:02 JinjaThreads: theory Refine_Det
18:03:07 JinjaThreads: theory Refine_Heuristics
18:03:07 JinjaThreads: theory Refine_Leof
18:03:07 JinjaThreads: theory Refine_Pfun
18:03:07 JinjaThreads: theory Refine_While
18:03:10 JinjaThreads: theory Refine_Transfer
18:03:11 JinjaThreads: theory Autoref_Monadic
18:03:11 JinjaThreads: theory Refine_Automation
18:03:11 JinjaThreads: theory Refine_Foreach
18:03:15 JinjaThreads: theory Refine_Monadic
18:03:17 JinjaThreads: theory Gen_Iterator
18:03:17 JinjaThreads: theory Intf_Map
18:03:18 JinjaThreads: theory Intf_Set
18:03:18 JinjaThreads: theory Iterator
18:03:19 JinjaThreads: theory Array_Iterator
18:03:19 JinjaThreads: theory ICF_Spec_Base
18:03:20 JinjaThreads: theory AnnotatedListSpec
18:03:20 JinjaThreads: theory ListSpec
18:03:20 JinjaThreads: theory MapSpec
18:03:20 JinjaThreads: theory PrioSpec
18:03:20 JinjaThreads: theory PrioUniqueSpec
18:03:22 JinjaThreads: theory SetSpec
18:03:22 JinjaThreads: theory BinoPrioImpl
18:03:24 JinjaThreads: theory ListGA
18:03:24 JinjaThreads: theory SkewPrioImpl
18:03:25 JinjaThreads: theory FTAnnotatedListImpl
18:03:26 JinjaThreads: theory Fifo
18:03:27 JinjaThreads: theory PrioByAnnotatedList
18:03:28 JinjaThreads: theory PrioUniqueByAnnotatedList
18:03:28 JinjaThreads: theory RBT
18:03:30 JinjaThreads: theory RBT_add
18:03:39 JinjaThreads: theory FTPrioImpl
18:03:40 JinjaThreads: theory Algos
18:03:40 JinjaThreads: theory SetIndex
18:03:40 JinjaThreads: theory SetIteratorCollectionsGA
18:03:41 JinjaThreads: theory FTPrioUniqueImpl
18:03:41 JinjaThreads: theory MapGA
18:03:41 JinjaThreads: theory SetGA
18:03:45 JinjaThreads: theory ArrayMapImpl
18:03:45 JinjaThreads: theory ListMapImpl
18:03:45 JinjaThreads: theory ListMapImpl_Invar
18:03:45 JinjaThreads: theory TrieMapImpl
18:03:45 JinjaThreads: theory RBTMapImpl
18:03:47 JinjaThreads: theory ArrayHashMap_Impl
18:03:49 JinjaThreads: theory ListSetImpl
18:03:49 JinjaThreads: theory ListSetImpl_Invar
18:03:49 JinjaThreads: theory ListSetImpl_NotDist
18:03:50 JinjaThreads: theory ListSetImpl_Sorted
18:03:51 JinjaThreads: theory SetByMap
18:03:51 JinjaThreads: theory HashMap_Impl
18:03:53 JinjaThreads: theory ArrayHashMap
18:03:53 JinjaThreads: theory ArraySetImpl
18:03:53 JinjaThreads: theory TrieSetImpl
18:03:53 JinjaThreads: theory RBTSetImpl
18:03:54 JinjaThreads: theory HashMap
18:03:57 JinjaThreads: theory ArrayHashSet
18:03:57 JinjaThreads: theory HashSet
18:03:57 JinjaThreads: theory MapStdImpl
18:04:02 JinjaThreads: theory SetStdImpl
18:04:07 JinjaThreads: theory ICF_Impl
18:04:14 JinjaThreads: theory ICF_Refine_Monadic
18:04:15 JinjaThreads: theory ICF_Autoref
18:04:20 JinjaThreads: theory Collections
18:04:21 JinjaThreads: theory CollectionsV1
18:04:32 JinjaThreads: theory JT_ICF
18:04:32 JinjaThreads: theory Basic_Main
18:05:11 JinjaThreads: theory Mapping
18:05:11 JinjaThreads: theory ListIndex
18:05:11 JinjaThreads: theory Orders
18:05:11 JinjaThreads: theory Prefix_Order
18:05:11 JinjaThreads: theory FWState
18:05:11 JinjaThreads: theory LTS
18:05:11 JinjaThreads: theory Type
18:05:11 JinjaThreads: theory Semilat
18:05:12 JinjaThreads: theory Err
18:05:13 JinjaThreads: theory AList_Mapping
18:05:14 JinjaThreads: theory Listn
18:05:14 JinjaThreads: theory Opt
18:05:14 JinjaThreads: theory Product
18:05:14 JinjaThreads: theory Semilattices
18:05:15 JinjaThreads: theory Typing_Framework
18:05:15 JinjaThreads: theory SemilatAlg
18:05:15 JinjaThreads: theory Kildall
18:05:16 JinjaThreads: theory LBVSpec
18:05:16 JinjaThreads: theory Decl
18:05:17 JinjaThreads: theory LBVComplete
18:05:17 JinjaThreads: theory LBVCorrect
18:05:17 JinjaThreads: theory Bisimulation
18:05:17 JinjaThreads: theory Typing_Framework_err
18:05:17 JinjaThreads: theory Abstract_BV
18:05:19 JinjaThreads: theory TypeRel
18:05:24 JinjaThreads: theory TypeRelRefine
18:05:25 JinjaThreads: theory Value
18:05:30 JinjaThreads: theory Exceptions
18:05:30 JinjaThreads: theory Heap
18:05:30 JinjaThreads: theory SystemClasses
18:05:33 JinjaThreads: theory MM
18:05:33 JinjaThreads: theory State
18:05:40 JinjaThreads: theory FWCondAction
18:05:40 JinjaThreads: theory FWLock
18:05:40 JinjaThreads: theory FWThread
18:05:40 JinjaThreads: theory FWWait
18:05:40 JinjaThreads: theory Observable_Events
18:05:40 JinjaThreads: theory FWInterrupt
18:05:43 JinjaThreads: theory FWLocking
18:05:44 JinjaThreads: theory FWLockingThread
18:05:44 JinjaThreads: theory FWWellform
18:05:45 JinjaThreads: theory FWLifting
18:05:45 JinjaThreads: theory FWSemantics
18:05:48 JinjaThreads: theory JMM_Spec
18:05:48 JinjaThreads: theory JVMState
18:05:48 JinjaThreads: theory StartConfig
18:05:49 JinjaThreads: theory FWLiftingSem
18:05:49 JinjaThreads: theory FWProgressAux
18:05:50 JinjaThreads: theory Conform
18:05:50 JinjaThreads: theory State_Refinement
18:05:51 JinjaThreads: theory FWDeadlock
18:05:51 JinjaThreads: theory FWLTS
18:05:54 JinjaThreads: theory ConformThreaded
18:05:55 JinjaThreads: theory FWProgress
18:05:55 JinjaThreads: theory ExternalCall
18:05:56 JinjaThreads: theory SC
18:05:56 JinjaThreads: theory SC_Collections
18:06:03 JinjaThreads: theory JMM_DRF
18:06:03 JinjaThreads: theory SC_Legal
18:06:03 JinjaThreads: theory FWBisimulation
18:06:04 JinjaThreads: theory FWInitFinLift
18:06:04 JinjaThreads: theory Non_Speculative
18:06:05 JinjaThreads: theory Scheduler
18:06:08 JinjaThreads: theory HB_Completion
18:06:08 JinjaThreads: theory SC_Completion
18:06:42 JinjaThreads: theory ExternalCall_Execute
18:06:42 JinjaThreads: theory WellForm
18:06:47 JinjaThreads: theory BinOp
18:06:48 JinjaThreads: theory ExternalCallWF
18:06:48 JinjaThreads: theory JMM_Heap
18:06:53 JinjaThreads: theory SemiType
18:06:53 JinjaThreads: theory Random_Scheduler
18:06:56 JinjaThreads: theory JMM_Type
18:06:57 JinjaThreads: theory JMM_Type2
18:07:03 JinjaThreads: theory JVM_SemiType
18:07:05 JinjaThreads: theory Round_Robin
18:07:08 JinjaThreads: theory JMM_Framework
18:07:38 JinjaThreads: theory SC_Schedulers
18:07:39 JinjaThreads: theory Expr
18:07:41 JinjaThreads: theory JVMInstructions
18:07:42 JinjaThreads: theory PCompiler
18:07:44 JinjaThreads: theory PCompilerRefine
18:07:52 JinjaThreads: theory JVMExceptions
18:07:52 JinjaThreads: theory JVMHeap
18:07:53 JinjaThreads: theory Effect
18:08:00 JinjaThreads: theory CallExpr
18:08:00 JinjaThreads: theory DefAss
18:08:02 JinjaThreads: theory WWellForm
18:08:02 JinjaThreads: theory JHeap
18:08:03 JinjaThreads: theory JVMExecInstr
18:08:04 JinjaThreads: theory WellType
18:08:06 JinjaThreads: theory ToString
18:08:08 JinjaThreads: theory JVMExec
18:08:09 JinjaThreads: theory J1State
18:08:12 JinjaThreads: theory Annotate
18:08:13 JinjaThreads: theory JVMDefensive
18:08:13 JinjaThreads: theory JVMExec_Execute
18:08:14 JinjaThreads: theory Compiler1
18:08:21 JinjaThreads: theory JVMThreaded
18:08:21 JinjaThreads: theory Compiler2
18:08:22 JinjaThreads: theory J1Heap
18:08:22 JinjaThreads: theory J1WellType
18:08:30 JinjaThreads: theory J1WellForm
18:08:32 JinjaThreads: theory SmallStep
18:08:33 JinjaThreads: theory JWellForm
18:08:36 JinjaThreads: theory JJ1WellForm
18:08:38 JinjaThreads: theory JMM_Typesafe
18:08:40 JinjaThreads: theory Preprocessor
18:08:46 JinjaThreads: theory WellTypeRT
18:08:57 JinjaThreads: theory Compiler
18:08:57 JinjaThreads: theory JMM_JVM
18:08:57 JinjaThreads: theory JVM_Main
18:08:58 JinjaThreads: theory Exception_Tables
18:12:24 JinjaThreads: theory JMM_Common
18:12:31 JinjaThreads: theory BVSpec
18:12:31 JinjaThreads: theory EffectMono
18:12:31 JinjaThreads: theory TF_JVM
18:12:32 JinjaThreads: theory BVConform
18:12:32 JinjaThreads: theory JMM_Typesafe2
18:12:32 JinjaThreads: theory TypeComp
18:12:35 JinjaThreads: theory BVExec
18:12:36 JinjaThreads: theory LBVJVM
18:12:38 JinjaThreads: theory BVSpecTypeSafe
18:12:46 JinjaThreads: theory BVNoTypeError
18:12:49 JinjaThreads: theory BCVExec
18:12:49 JinjaThreads: theory JVMExec_Execute2
18:12:49 JinjaThreads: theory BVProgressThreaded
18:12:49 JinjaThreads: theory JVMTau
18:13:06 JinjaThreads: theory FWBisimDeadlock
18:13:06 JinjaThreads: theory FWBisimLift
18:13:07 JinjaThreads: theory J1
18:13:13 JinjaThreads: theory Execs
18:13:29 JinjaThreads: theory Common_Main
18:13:36 JinjaThreads: theory DefAssPreservation
18:13:36 JinjaThreads: theory Threaded
18:13:36 JinjaThreads: theory Progress
18:13:37 JinjaThreads: theory J1Deadlock
18:13:41 JinjaThreads: theory TypeSafe
18:13:57 JinjaThreads: theory J0
18:13:57 JinjaThreads: theory JMM_J
18:13:57 JinjaThreads: theory ProgressThreaded
18:13:57 JinjaThreads: theory J_Execute
18:13:57 JinjaThreads: theory J1JVMBisim
18:14:07 JinjaThreads: theory JVMDeadlocked
18:14:08 JinjaThreads: theory DRF_JVM
18:14:08 JinjaThreads: theory JVM_Execute
18:14:09 JinjaThreads: theory JVM_Execute2
18:14:24 JinjaThreads: theory DRF_J
18:14:25 JinjaThreads: theory Deadlocked
18:14:33 JinjaThreads: theory J_Main
18:14:37 JinjaThreads: theory BV_Main
18:14:49 JinjaThreads: theory J0Bisim
18:14:50 JinjaThreads: theory J0J1Bisim
18:14:51 JinjaThreads: theory Code_Generation
18:15:15 JinjaThreads: theory ApprenticeChallenge
18:15:24 JinjaThreads: theory BufferExample
18:15:24 JinjaThreads: theory Java2Jinja
18:15:43 JinjaThreads: theory Correctness1
18:15:45 JinjaThreads: theory Correctness1Threaded
18:20:20 JinjaThreads: theory Examples_Main
18:21:34 JinjaThreads: theory JMM_JVM_Typesafe
18:21:46 JinjaThreads: theory JMM_J_Typesafe
18:22:19 JinjaThreads: theory Execute_Main
18:23:13 JinjaThreads: theory J1JVM
18:23:14 JinjaThreads: theory JVMJ1
18:24:51 JinjaThreads: theory Correctness2
18:27:43 JinjaThreads: theory Correctness
18:38:51 JinjaThreads: theory Compiler_Main
18:38:53 JinjaThreads: theory JMM_Compiler
18:38:54 JinjaThreads: theory SC_Interp
18:43:17 JinjaThreads: theory JMM_Interp
18:43:21 JinjaThreads: theory JMM_Compiler_Type2
18:43:23 JinjaThreads: theory JMM
18:43:26 JinjaThreads: theory MM_Main
18:43:35 JinjaThreads: theory JinjaThreads
18:46:38 Timing JinjaThreads (8 threads, 2607.306s elapsed time, 12548.144s cpu time, 3570.768s GC time, factor 4.81)
18:46:38 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads
18:46:38 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf
18:46:38 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf
18:46:38 Finished JinjaThreads (0:44:23 elapsed time, 3:31:16 cpu time, factor 4.76)
18:46:39 Running HOL-ODE-Examples ...
18:47:03 HOL-ODE-Examples: theory Parallel
18:47:03 HOL-ODE-Examples: theory Initials
18:47:03 HOL-ODE-Examples: theory Example_Utilities
18:47:04 HOL-ODE-Examples: theory Example1
18:47:04 HOL-ODE-Examples: theory Example_Bessel
18:47:04 HOL-ODE-Examples: theory Example_Exp
18:47:04 HOL-ODE-Examples: theory Example3
18:47:04 HOL-ODE-Examples: theory Example_Lorenz_Classic
18:47:04 HOL-ODE-Examples: theory Example_Oil
18:47:05 HOL-ODE-Examples: theory Example_Variational_Equation
18:47:18 HOL-ODE-Examples: theory Example_van_der_Pol
18:49:50 HOL-ODE-Examples: theory Lorenz_Approximation
18:52:55 HOL-ODE-Examples: theory Lorenz_Parallel
18:59:13 HOL-ODE-Examples: theory ODE_Examples
18:59:19 Timing HOL-ODE-Examples (8 threads, 734.625s elapsed time, 3654.520s cpu time, 702.548s GC time, factor 4.97)
18:59:19 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Examples
18:59:19 Finished HOL-ODE-Examples (0:12:39 elapsed time, 1:01:19 cpu time, factor 4.84)
18:59:19 
18:59:19 === TIMING ===
18:59:19 
18:59:19 Group slow: 16:24:37 elapsed time, 55:53:21 cpu time, factor 3.41
18:59:19 Group AFP: 17:03:59 elapsed time, 57:48:37 cpu time, factor 3.39
18:59:19 Group main: 0:19:16 elapsed time, 1:12:25 cpu time, factor 3.76
18:59:19 Group timing: 0:13:59 elapsed time, 0:57:45 cpu time, factor 4.13
18:59:19 Group very_slow: 10:31:28 elapsed time, 29:48:29 cpu time, factor 2.83
18:59:19 Overall: 17:24:14 elapsed time, 59:01:22 cpu time, factor 3.39
18:59:19 Archiving artifacts
18:59:22 Started calculate disk usage of build
18:59:22 Finished Calculation of disk usage of build in 0 seconds
18:59:30 Started calculate disk usage of workspace
18:59:31 Finished Calculation of disk usage of workspace in  1 second
18:59:31 No emails were triggered.
18:59:31 Finished: SUCCESS