Console Output

01:33:23 Started by an SCM change
01:33:23 [EnvInject] - Loading node environment variables.
01:33:23 Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow
01:33:24 [isabelle-nightly-slow] $ hg showconfig paths.default
01:33:24 [isabelle-nightly-slow] $ hg pull --rev default
01:33:24 pulling from http://isabelle.in.tum.de/repos/isabelle/
01:33:24 searching for changes
01:33:24 no changes found
01:33:24 [isabelle-nightly-slow] $ hg update --clean --rev default
01:33:24 63 files updated, 0 files merged, 0 files removed, 0 files unresolved
01:33:24 [isabelle-nightly-slow] $ hg --config extensions.purge= clean --all
01:33:24 [isabelle-nightly-slow] $ hg log --rev . --template {node}
01:33:25 [isabelle-nightly-slow] $ hg log --rev . --template {rev}
01:33:25 [isabelle-nightly-slow] $ hg log --rev f435640193b65f419f2c6ca3162c140eac10bbd3 --template exists\n
01:33:25 exists
01:33:25 [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(f435640193b65f419f2c6ca3162c140eac10bbd3)" --encoding UTF-8 --encodingmode replace
01:33:25 [afp] $ hg showconfig paths.default
01:33:25 [afp] $ hg pull --rev default
01:33:26 pulling from https://bitbucket.org/isa-afp/afp-devel/
01:33:26 no changes found
01:33:26 [afp] $ hg update --clean --rev default
01:33:26 3 files updated, 0 files merged, 0 files removed, 0 files unresolved
01:33:26 [afp] $ hg --config extensions.purge= clean --all
01:33:27 [afp] $ hg log --rev . --template {node}
01:33:27 [afp] $ hg log --rev . --template {rev}
01:33:27 [afp] $ hg log --rev ee8091b2d624b2d7817de06f152ccfebe06a4ac3 --template exists\n
01:33:27 exists
01:33:27 [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(ee8091b2d624b2d7817de06f152ccfebe06a4ac3)" --encoding UTF-8 --encodingmode replace
01:33:27 No emails were triggered.
01:33:27 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/hudson3626931559025786477.sh
01:33:27 + Admin/jenkins/run_build slow
01:33:27 + set -e
01:33:27 + PROFILE=slow
01:33:27 + shift
01:33:27 + bin/isabelle components -a
01:33:27 + bin/isabelle jedit -bf
01:33:27 ### Building graph browser ...
01:33:27 warning: [options] bootstrap class path not set in conjunction with -source 1.4
01:33:27 warning: [options] source value 1.4 is obsolete and will be removed in a future release
01:33:27 warning: [options] target value 1.4 is obsolete and will be removed in a future release
01:33:27 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
01:33:28 Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.
01:33:28 Note: Recompile with -Xlint:deprecation for details.
01:33:28 4 warnings
01:33:29 ### Building Isabelle/Scala ...
01:34:44 ### Building Isabelle/jEdit ...
01:35:13 + bin/isabelle ci_build_slow
01:35:19 
01:35:19 === CONFIGURATION ===
01:35:19 
01:35:19 ISABELLE_BUILD_OPTIONS=""
01:35:19 
01:35:19 ML_PLATFORM="x86_64-linux"
01:35:19 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"
01:35:19 ML_SYSTEM="polyml-5.6"
01:35:19 ML_OPTIONS="-H 4000 --maxheap 10G"
01:35:19 
01:35:19 === BUILD ===
01:35:19 
01:35:19 Build started at Thu, 16 Mar 2017 01:35:19 +0100
01:35:19 Isabelle id 7611c55c39d0
01:35:19 Build for AFP id 71767e8d023f
01:35:19 
01:35:19 === LOG ===
01:35:19 
01:35:20 Session Pure/Pure
01:35:21 Session HOL/HOL (main)
01:35:22 Session AFP/AWN (AFP)
01:35:22 Session AFP/AODV (AFP slow)
01:35:22 Session HOL/HOL-Analysis (main timing)
01:35:23 Session AFP/Ordinary_Differential_Equations (AFP)
01:35:23 Session AFP/HOL-ODE (AFP)
01:35:23 Session AFP/HOL-ODE-Refinement (AFP)
01:35:23 Session AFP/HOL-ODE-Numerics (AFP)
01:35:23 Session AFP/HOL-ODE-Examples (AFP slow)
01:35:23 Session HOL/HOL-Library (main timing)
01:35:24 Session AFP/ConcurrentIMP (AFP)
01:35:24 Session AFP/ConcurrentGC (AFP slow)
01:35:24 Session AFP/Flyspeck-Tame (AFP slow very_slow)
01:35:24 Session HOL/HOL-Word (main timing)
01:35:24 Session AFP/JinjaThreads (AFP slow)
01:35:25 Session AFP/Word_Lib (AFP)
01:35:25 Session AFP/IP_Addresses (AFP)
01:35:25 Session AFP/Simple_Firewall (AFP)
01:35:25 Session AFP/Routing (AFP)
01:35:25 Session AFP/Iptables_Semantics (AFP)
01:35:25 Session AFP/Iptables_Semantics_Examples (AFP slow very_slow)
01:35:25 Building Pure ...
01:35:41 Pure: theory Pure
01:35:42 Pure: theory ML_Bootstrap
01:35:45 Warning: missing document directory
01:35:45 Timing Pure (1 threads, 0.793s elapsed time, 0.796s cpu time, 0.000s GC time, factor 1.00)
01:35:45 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure
01:35:45 Finished Pure (0:00:19 elapsed time, 0:00:18 cpu time, factor 0.99)
01:35:46 Building HOL ...
01:35:47 HOL: theory Code_Generator
01:35:50 HOL: theory HOL
01:35:54 HOL: theory Argo
01:35:54 HOL: theory Orderings
01:35:54 HOL: theory Ctr_Sugar
01:35:56 HOL: theory SAT
01:35:56 HOL: theory Groups
01:35:59 HOL: theory Lattices
01:36:01 HOL: theory Set
01:36:03 HOL: theory Fun
01:36:03 HOL: theory Typedef
01:36:03 HOL: theory Rings
01:36:04 HOL: theory Complete_Lattices
01:36:07 HOL: theory Inductive
01:36:09 HOL: theory Product_Type
01:36:09 HOL: theory Sum_Type
01:36:11 HOL: theory Complete_Partial_Order
01:36:16 HOL: theory Nat
01:36:18 HOL: theory Fields
01:36:18 HOL: theory Meson
01:36:19 HOL: theory ATP
01:36:22 HOL: theory Metis
01:36:24 HOL: theory Finite_Set
01:36:26 HOL: theory Relation
01:36:28 HOL: theory Transitive_Closure
01:36:29 HOL: theory Wellfounded
01:36:30 HOL: theory Fun_Def_Base
01:36:30 HOL: theory Hilbert_Choice
01:36:30 HOL: theory Wfrec
01:36:30 HOL: theory Order_Relation
01:36:31 HOL: theory BNF_Wellorder_Relation
01:36:31 HOL: theory Zorn
01:36:31 HOL: theory BNF_Wellorder_Embedding
01:36:32 HOL: theory BNF_Wellorder_Constructions
01:36:33 HOL: theory BNF_Cardinal_Order_Relation
01:36:34 HOL: theory BNF_Cardinal_Arithmetic
01:36:34 HOL: theory BNF_Def
01:36:36 HOL: theory BNF_Composition
01:36:36 HOL: theory Basic_BNFs
01:36:37 HOL: theory BNF_Fixpoint_Base
01:36:41 HOL: theory BNF_Least_Fixpoint
01:36:43 HOL: theory Basic_BNF_LFPs
01:36:44 HOL: theory Transfer
01:36:45 HOL: theory Num
01:36:49 HOL: theory Power
01:36:52 HOL: theory Groups_Big
01:36:55 HOL: theory Equiv_Relations
01:36:55 HOL: theory Lifting
01:36:57 HOL: theory Lifting_Set
01:36:57 HOL: theory Quotient
01:36:57 HOL: theory Option
01:36:58 HOL: theory Extraction
01:36:58 HOL: theory Lattices_Big
01:36:58 HOL: theory Partial_Function
01:36:59 HOL: theory Fun_Def
01:37:01 HOL: theory Int
01:37:04 HOL: theory Nat_Transfer
01:37:05 HOL: theory Euclidean_Division
01:37:11 HOL: theory Parity
01:37:13 HOL: theory Divides
01:37:24 HOL: theory Code_Numeral
01:37:24 HOL: theory Numeral_Simprocs
01:37:24 HOL: theory SMT
01:37:24 HOL: theory Set_Interval
01:37:25 HOL: theory Semiring_Normalization
01:37:28 HOL: theory Conditionally_Complete_Lattices
01:37:28 HOL: theory Filter
01:37:29 HOL: theory Groebner_Basis
01:37:30 HOL: theory Presburger
01:37:33 HOL: theory Sledgehammer
01:37:36 HOL: theory List
01:37:47 HOL: theory Groups_List
01:37:47 HOL: theory Map
01:37:48 HOL: theory Enum
01:37:48 HOL: theory Random
01:37:51 HOL: theory String
01:37:53 HOL: theory BNF_Greatest_Fixpoint
01:37:53 HOL: theory Typerep
01:37:53 HOL: theory Predicate
01:37:55 HOL: theory Lazy_Sequence
01:37:56 HOL: theory Limited_Sequence
01:37:56 HOL: theory Code_Evaluation
01:37:58 HOL: theory Quickcheck_Random
01:38:01 HOL: theory Quickcheck_Exhaustive
01:38:01 HOL: theory Random_Pred
01:38:01 HOL: theory Quickcheck_Narrowing
01:38:02 HOL: theory Random_Sequence
01:38:06 HOL: theory Record
01:38:06 HOL: theory Predicate_Compile
01:38:09 HOL: theory Nitpick
01:38:15 HOL: theory Main
01:38:17 HOL: theory Archimedean_Field
01:38:17 HOL: theory Binomial
01:38:17 HOL: theory GCD
01:38:17 HOL: theory Topological_Spaces
01:38:28 HOL: theory Rat
01:38:32 HOL: theory Real
01:38:35 HOL: theory Real_Vector_Spaces
01:38:51 HOL: theory Inequalities
01:38:51 HOL: theory Limits
01:38:56 HOL: theory Deriv
01:38:56 HOL: theory Series
01:38:58 HOL: theory NthRoot
01:39:00 HOL: theory Transcendental
01:39:07 HOL: theory Complex
01:39:09 HOL: theory MacLaurin
01:39:09 HOL: theory Complex_Main
01:40:59 Timing HOL (8 threads, 220.024s elapsed time, 683.940s cpu time, 44.640s GC time, factor 3.11)
01:40:59 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL
01:40:59 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf
01:40:59 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf
01:40:59 Finished HOL (0:05:12 elapsed time, 0:14:42 cpu time, factor 2.83)
01:41:02 Building HOL-Library ...
01:41:06 HOL-Library: theory Adhoc_Overloading
01:41:06 HOL-Library: theory AList
01:41:06 HOL-Library: theory BNF_Axiomatization
01:41:06 HOL-Library: theory BNF_Corec
01:41:06 HOL-Library: theory Lattice_Syntax
01:41:06 HOL-Library: theory Stirling
01:41:06 HOL-Library: theory Bits
01:41:06 HOL-Library: theory Bit
01:41:06 HOL-Library: theory Boolean_Algebra
01:41:06 HOL-Library: theory Cancellation
01:41:06 HOL-Library: theory Cardinal_Notations
01:41:06 HOL-Library: theory Char_ord
01:41:06 HOL-Library: theory Code_Abstract_Nat
01:41:06 HOL-Library: theory Code_Prolog
01:41:07 HOL-Library: theory Code_Binary_Nat
01:41:07 HOL-Library: theory Code_Target_Nat
01:41:07 HOL-Library: theory Code_Char
01:41:07 HOL-Library: theory Multiset
01:41:07 HOL-Library: theory Code_Test
01:41:07 HOL-Library: theory Bits_Bit
01:41:07 HOL-Library: theory Combine_PER
01:41:07 HOL-Library: theory Complete_Partial_Order2
01:41:07 HOL-Library: theory Debug
01:41:07 HOL-Library: theory Disjoint_Sets
01:41:07 HOL-Library: theory Dlist
01:41:08 HOL-Library: theory FSet
01:41:08 HOL-Library: theory Fraction_Field
01:41:09 HOL-Library: theory Fun_Lexorder
01:41:09 HOL-Library: theory FuncSet
01:41:09 HOL-Library: theory DAList
01:41:09 HOL-Library: theory Function_Algebras
01:41:10 HOL-Library: theory Code_Target_Int
01:41:10 HOL-Library: theory Function_Division
01:41:10 HOL-Library: theory Code_Target_Numeral
01:41:10 HOL-Library: theory Groups_Big_Fun
01:41:10 HOL-Library: theory IArray
01:41:10 HOL-Library: theory Infinite_Set
01:41:11 HOL-Library: theory LaTeXsugar
01:41:11 HOL-Library: theory Lattice_Constructions
01:41:11 HOL-Library: theory ListVector
01:41:11 HOL-Library: theory Omega_Words_Fun
01:41:12 HOL-Library: theory Ramsey
01:41:12 HOL-Library: theory List_lexord
01:41:12 HOL-Library: theory Mapping
01:41:12 HOL-Library: theory Misc_Numeric
01:41:12 HOL-Library: theory Misc_Typedef
01:41:12 HOL-Library: theory Bit_Representation
01:41:12 HOL-Library: theory Monad_Syntax
01:41:12 HOL-Library: theory More_List
01:41:13 HOL-Library: theory Nat_Bijection
01:41:13 HOL-Library: theory Finite_Map
01:41:13 HOL-Library: theory Old_Datatype
01:41:13 HOL-Library: theory Bits_Int
01:41:14 HOL-Library: theory AList_Mapping
01:41:14 HOL-Library: theory Stream
01:41:14 HOL-Library: theory Old_Recdef
01:41:14 HOL-Library: theory DAList_Multiset
01:41:15 HOL-Library: theory Multiset_Order
01:41:15 HOL-Library: theory Permutation
01:41:15 HOL-Library: theory Permutations
01:41:15 HOL-Library: theory Factorial_Ring
01:41:15 HOL-Library: theory Countable
01:41:15 HOL-Library: theory Bool_List_Representation
01:41:15 HOL-Library: theory Option_ord
01:41:15 HOL-Library: theory Parallel
01:41:15 HOL-Library: theory Perm
01:41:15 HOL-Library: theory Phantom_Type
01:41:16 HOL-Library: theory Predicate_Compile_Alternative_Defs
01:41:16 HOL-Library: theory Product_Lexorder
01:41:16 HOL-Library: theory Predicate_Compile_Quickcheck
01:41:17 HOL-Library: theory Product_Plus
01:41:17 HOL-Library: theory Quotient_Syntax
01:41:17 HOL-Library: theory Cardinality
01:41:17 HOL-Library: theory Quotient_Option
01:41:17 HOL-Library: theory Quotient_Product
01:41:17 HOL-Library: theory Product_Order
01:41:17 HOL-Library: theory Quotient_Set
01:41:17 HOL-Library: theory Quotient_Sum
01:41:17 HOL-Library: theory Quotient_Type
01:41:17 HOL-Library: theory RBT_Impl
01:41:17 HOL-Library: theory Quotient_List
01:41:17 HOL-Library: theory Finite_Lattice
01:41:17 HOL-Library: theory Reflection
01:41:18 HOL-Library: theory Refute
01:41:18 HOL-Library: theory Countable_Set
01:41:18 HOL-Library: theory Rewrite
01:41:18 HOL-Library: theory Set_Algebras
01:41:18 HOL-Library: theory Simps_Case_Conv
01:41:18 HOL-Library: theory Extended
01:41:18 HOL-Library: theory State_Monad
01:41:18 HOL-Library: theory Numeral_Type
01:41:18 HOL-Library: theory Countable_Complete_Lattices
01:41:18 HOL-Library: theory Countable_Set_Type
01:41:19 HOL-Library: theory Sublist
01:41:20 HOL-Library: theory Type_Length
01:41:20 HOL-Library: theory Prefix_Order
01:41:20 HOL-Library: theory Saturated
01:41:20 HOL-Library: theory Sublist_Order
01:41:20 HOL-Library: theory Polynomial
01:41:21 HOL-Library: theory BigO
01:41:21 HOL-Library: theory Code_Real_Approx_By_Float
01:41:22 HOL-Library: theory Diagonal_Subsequence
01:41:22 HOL-Library: theory Discrete
01:41:22 HOL-Library: theory Indicator_Function
01:41:22 HOL-Library: theory Lattice_Algebras
01:41:23 HOL-Library: theory Liminf_Limsup
01:41:23 HOL-Library: theory Log_Nat
01:41:23 HOL-Library: theory Lub_Glb
01:41:23 HOL-Library: theory Multiset_Permutations
01:41:23 HOL-Library: theory Nonpos_Ints
01:41:23 HOL-Library: theory OptionalSugar
01:41:24 HOL-Library: theory Order_Continuity
01:41:24 HOL-Library: theory Periodic_Fun
01:41:24 HOL-Library: theory Quadratic_Discriminant
01:41:24 HOL-Library: theory Sum_of_Squares
01:41:24 HOL-Library: theory Transitive_Closure_Table
01:41:25 HOL-Library: theory Tree
01:41:25 HOL-Library: theory While_Combinator
01:41:25 HOL-Library: theory Extended_Nat
01:41:26 HOL-Library: theory Bourbaki_Witt_Fixpoint
01:41:26 HOL-Library: theory Word_Miscellaneous
01:41:27 HOL-Library: theory Extended_Real
01:41:27 HOL-Library: theory Linear_Temporal_Logic_on_Streams
01:41:28 HOL-Library: theory Euclidean_Algorithm
01:41:29 HOL-Library: theory Word
01:41:30 HOL-Library: theory Preorder
01:41:30 HOL-Library: theory Function_Growth
01:41:30 HOL-Library: theory Tree_Multiset
01:41:31 HOL-Library: theory Fundamental_Theorem_Algebra
01:41:32 HOL-Library: theory Float
01:41:33 HOL-Library: theory Extended_Nonnegative_Real
01:41:37 HOL-Library: theory Old_SMT
01:41:41 HOL-Library: theory Normalized_Fraction
01:41:41 HOL-Library: theory Field_as_Ring
01:41:41 HOL-Library: theory Formal_Power_Series
01:41:43 HOL-Library: theory Polynomial_Factorial
01:41:48 HOL-Library: theory Polynomial_FPS
01:41:49 HOL-Library: theory Library
01:42:24 HOL-Library: theory RBT
01:42:26 HOL-Library: theory RBT_Mapping
01:42:26 HOL-Library: theory RBT_Set
01:45:08 Timing HOL-Library (8 threads, 149.346s elapsed time, 850.204s cpu time, 74.512s GC time, factor 5.69)
01:45:08 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library
01:45:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf
01:45:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf
01:45:08 Finished HOL-Library (0:04:05 elapsed time, 0:17:49 cpu time, factor 4.36)
01:45:11 Building HOL-Word ...
01:45:13 HOL-Word: theory Bits
01:45:13 HOL-Word: theory Bit
01:45:13 HOL-Word: theory Boolean_Algebra
01:45:13 HOL-Word: theory Misc_Numeric
01:45:13 HOL-Word: theory Misc_Typedef
01:45:13 HOL-Word: theory Phantom_Type
01:45:14 HOL-Word: theory Bit_Representation
01:45:15 HOL-Word: theory Bits_Bit
01:45:15 HOL-Word: theory Word_Miscellaneous
01:45:15 HOL-Word: theory Bits_Int
01:45:15 HOL-Word: theory Cardinality
01:45:17 HOL-Word: theory Numeral_Type
01:45:17 HOL-Word: theory Bool_List_Representation
01:45:18 HOL-Word: theory Type_Length
01:45:19 HOL-Word: theory Word
01:45:45 Timing HOL-Word (8 threads, 12.870s elapsed time, 60.188s cpu time, 1.848s GC time, factor 4.68)
01:45:45 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word
01:45:45 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf
01:45:45 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf
01:45:45 Finished HOL-Word (0:00:34 elapsed time, 0:01:45 cpu time, factor 3.09)
01:45:46 Building AWN ...
01:45:48 AWN: theory Lib
01:45:48 AWN: theory TransitionSystems
01:45:48 AWN: theory AWN
01:45:49 AWN: theory Invariants
01:45:50 AWN: theory OInvariants
01:46:03 AWN: theory AWN_Cterms
01:46:03 AWN: theory AWN_SOS
01:46:03 AWN: theory OAWN_SOS
01:46:07 AWN: theory AWN_Labels
01:46:10 AWN: theory Inv_Cterms
01:46:10 AWN: theory AWN_Invariants
01:46:10 AWN: theory Pnet
01:46:11 AWN: theory AWN_SOS_Labels
01:46:11 AWN: theory Closed
01:46:11 AWN: theory Qmsg
01:46:13 AWN: theory OAWN_SOS_Labels
01:46:13 AWN: theory ONode_Lifting
01:46:13 AWN: theory OAWN_Invariants
01:46:13 AWN: theory OPnet
01:46:14 AWN: theory OPnet_Lifting
01:46:15 AWN: theory OClosed_Lifting
01:46:15 AWN: theory OClosed_Transfer
01:46:15 AWN: theory OAWN_Convert
01:46:15 AWN: theory Qmsg_Lifting
01:46:16 AWN: theory AWN_Main
01:46:17 AWN: theory Toy
01:47:10 Timing AWN (8 threads, 49.637s elapsed time, 248.680s cpu time, 7.344s GC time, factor 5.01)
01:47:10 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN
01:47:10 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf
01:47:10 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf
01:47:10 Finished AWN (0:01:24 elapsed time, 0:05:29 cpu time, factor 3.92)
01:47:11 Building ConcurrentIMP ...
01:47:20 ConcurrentIMP: theory CIMP_pred
01:47:20 ConcurrentIMP: theory CIMP_lang
01:47:33 ConcurrentIMP: theory CIMP_vcg
01:47:35 ConcurrentIMP: theory CIMP
01:47:35 ConcurrentIMP: theory CIMP_one_place_buffer_ex
01:47:35 ConcurrentIMP: theory CIMP_unbounded_buffer_ex
01:48:10 Timing ConcurrentIMP (8 threads, 21.266s elapsed time, 50.672s cpu time, 2.560s GC time, factor 2.38)
01:48:10 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP
01:48:10 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf
01:48:10 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf
01:48:10 Finished ConcurrentIMP (0:00:58 elapsed time, 0:02:13 cpu time, factor 2.26)
01:48:10 Building Word_Lib ...
01:48:13 Word_Lib: theory Sublist
01:48:13 Word_Lib: theory WordBitwise
01:48:15 Word_Lib: theory Prefix_Order
01:48:16 Word_Lib: theory HOL_Lemmas
01:48:16 Word_Lib: theory More_Divides
01:48:16 Word_Lib: theory Enumeration
01:48:16 Word_Lib: theory Hex_Words
01:48:16 Word_Lib: theory Signed_Words
01:48:16 Word_Lib: theory Norm_Words
01:48:16 Word_Lib: theory WordBitwise_Signed
01:48:16 Word_Lib: theory Word_Syntax
01:48:17 Word_Lib: theory Word_Lib
01:48:18 Word_Lib: theory Aligned
01:48:18 Word_Lib: theory Word_Enum
01:48:18 Word_Lib: theory Word_Setup_32
01:48:18 Word_Lib: theory Word_Setup_64
01:48:18 Word_Lib: theory Word_Lemmas
01:48:25 Word_Lib: theory Word_Lemmas_32
01:48:25 Word_Lib: theory Word_Lemmas_64
01:49:28 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib
01:49:28 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf
01:49:28 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf
01:49:28 Word_Lib FAILED
01:49:28 (see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.6_x86_64-linux/log/Word_Lib)
01:49:28 ***         \<not> y !! n; x !! n\<rbrakk>
01:49:28 ***        \<Longrightarrow> False
01:49:28 ***  4. \<And>n.
01:49:28 ***        \<lbrakk>n < LENGTH('a); \<not> m !! n; \<not> y !! n;
01:49:28 ***         \<not> (~~ m) !! n; x !! n\<rbrakk>
01:49:28 ***        \<Longrightarrow> False
01:49:28 ***  5. \<And>n.
01:49:28 ***        \<lbrakk>n < LENGTH('a); \<not> m !! n; \<not> x !! n;
01:49:28 ***         \<not> (~~ m) !! n; y !! n\<rbrakk>
01:49:28 ***        \<Longrightarrow> False
01:49:28 ***  6. \<And>n.
01:49:28 ***        \<lbrakk>n < LENGTH('a); \<not> m !! n; \<not> (~~ m) !! n;
01:49:28 ***         \<not> y !! n; x !! n\<rbrakk>
01:49:28 ***        \<Longrightarrow> False
01:49:28 ***  7. \<And>n.
01:49:28 ***        \<lbrakk>n < LENGTH('a); \<not> m !! n; \<not> (~~ m) !! n;
01:49:28 ***         x !! n\<rbrakk>
01:49:28 ***        \<Longrightarrow> y !! n
01:49:28 ***  8. \<And>n.
01:49:28 ***        \<lbrakk>n < LENGTH('a); \<not> m !! n; \<not> (~~ m) !! n;
01:49:28 ***         y !! n\<rbrakk>
01:49:28 ***        \<Longrightarrow> x !! n
01:49:28 *** At command "done" (line 2107 of "~~/afp/thys/Word_Lib/Word_Lemmas.thy")
01:49:28 *** Failed to finish proof:
01:49:28 *** goal (1 subgoal):
01:49:28 ***  1. \<And>x n.
01:49:28 ***        \<lbrakk>LENGTH('a) < LENGTH('b);
01:49:28 ***         (x !! n \<and> n < LENGTH('a) \<and> n < LENGTH('b)) =
01:49:28 ***         x !! n\<rbrakk>
01:49:28 ***        \<Longrightarrow> n < LENGTH('b) \<longrightarrow>
01:49:28 ***                          x !! n = (x !! n \<and> n < LENGTH('a))
01:49:28 *** At command "done" (line 1321 of "~~/afp/thys/Word_Lib/Word_Lemmas.thy")
01:49:28 *** Failed to finish proof:
01:49:28 *** goal (1 subgoal):
01:49:28 ***  1. \<And>n.
01:49:28 ***        \<lbrakk>LENGTH('a) \<le> LENGTH('b); LENGTH('b) \<le> LENGTH('c);
01:49:28 ***         (x !! n \<and> n < LENGTH('c)) =
01:49:28 ***         (y !! n \<and> n < LENGTH('a) \<and> n < LENGTH('c))\<rbrakk>
01:49:28 ***        \<Longrightarrow> n < LENGTH('a) \<longrightarrow> x !! n = y !! n
01:49:28 *** At command "done" (line 170 of "~~/afp/thys/Word_Lib/Word_Lemmas.thy")
01:49:28 IP_Addresses CANCELLED
01:49:28 Simple_Firewall CANCELLED
01:49:28 Routing CANCELLED
01:49:28 Iptables_Semantics CANCELLED
01:49:28 Building HOL-Analysis ...
01:49:32 HOL-Analysis: theory Cancellation
01:49:32 HOL-Analysis: theory Disjoint_Sets
01:49:32 HOL-Analysis: theory Infinite_Set
01:49:32 HOL-Analysis: theory FuncSet
01:49:32 HOL-Analysis: theory Nat_Bijection
01:49:32 HOL-Analysis: theory Old_Datatype
01:49:32 HOL-Analysis: theory Phantom_Type
01:49:32 HOL-Analysis: theory Product_Plus
01:49:33 HOL-Analysis: theory Product_Order
01:49:33 HOL-Analysis: theory Set_Algebras
01:49:33 HOL-Analysis: theory L2_Norm
01:49:33 HOL-Analysis: theory Discrete
01:49:33 HOL-Analysis: theory Indicator_Function
01:49:33 HOL-Analysis: theory Inner_Product
01:49:33 HOL-Analysis: theory Multiset
01:49:34 HOL-Analysis: theory Liminf_Limsup
01:49:34 HOL-Analysis: theory Nonpos_Ints
01:49:34 HOL-Analysis: theory Operator_Norm
01:49:34 HOL-Analysis: theory Cardinality
01:49:35 HOL-Analysis: theory Periodic_Fun
01:49:35 HOL-Analysis: theory Poly_Roots
01:49:35 HOL-Analysis: theory Sum_of_Squares
01:49:35 HOL-Analysis: theory Countable
01:49:36 HOL-Analysis: theory Product_Vector
01:49:36 HOL-Analysis: theory Numeral_Type
01:49:36 HOL-Analysis: theory Euclidean_Space
01:49:37 HOL-Analysis: theory Countable_Set
01:49:38 HOL-Analysis: theory Countable_Complete_Lattices
01:49:38 HOL-Analysis: theory Continuum_Not_Denumerable
01:49:38 HOL-Analysis: theory Norm_Arith
01:49:39 HOL-Analysis: theory Finite_Cartesian_Product
01:49:39 HOL-Analysis: theory Linear_Algebra
01:49:41 HOL-Analysis: theory Permutations
01:49:41 HOL-Analysis: theory Factorial_Ring
01:49:42 HOL-Analysis: theory Order_Continuity
01:49:43 HOL-Analysis: theory Topology_Euclidean_Space
01:49:43 HOL-Analysis: theory Extended_Nat
01:49:45 HOL-Analysis: theory Extended_Real
01:49:51 HOL-Analysis: theory Extended_Nonnegative_Real
01:49:51 HOL-Analysis: theory Summation_Tests
01:49:53 HOL-Analysis: theory Euclidean_Algorithm
01:49:54 HOL-Analysis: theory Sigma_Algebra
01:49:57 HOL-Analysis: theory Bounded_Linear_Function
01:49:57 HOL-Analysis: theory Convex_Euclidean_Space
01:49:57 HOL-Analysis: theory Extended_Real_Limits
01:49:57 HOL-Analysis: theory Tagged_Division
01:49:57 HOL-Analysis: theory Uniform_Limit
01:49:58 HOL-Analysis: theory Measurable
01:50:00 HOL-Analysis: theory Measure_Space
01:50:04 HOL-Analysis: theory Caratheodory
01:50:04 HOL-Analysis: theory Primes
01:50:05 HOL-Analysis: theory Continuous_Extension
01:50:06 HOL-Analysis: theory Path_Connected
01:50:12 HOL-Analysis: theory Homeomorphism
01:50:13 HOL-Analysis: theory Brouwer_Fixpoint
01:50:17 HOL-Analysis: theory Derivative
01:50:20 HOL-Analysis: theory Cartesian_Euclidean_Space
01:50:20 HOL-Analysis: theory Weierstrass_Theorems
01:50:24 HOL-Analysis: theory Determinants
01:50:24 HOL-Analysis: theory Fashoda_Theorem
01:50:24 HOL-Analysis: theory Ordered_Euclidean_Space
01:50:24 HOL-Analysis: theory Polytope
01:50:32 HOL-Analysis: theory Arcwise_Connected
01:50:33 HOL-Analysis: theory Borel_Space
01:50:37 HOL-Analysis: theory Nonnegative_Lebesgue_Integration
01:50:37 HOL-Analysis: theory Regularity
01:50:40 HOL-Analysis: theory Binary_Product_Measure
01:50:42 HOL-Analysis: theory Embed_Measure
01:50:42 HOL-Analysis: theory Finite_Product_Measure
01:50:44 HOL-Analysis: theory Bochner_Integration
01:50:44 HOL-Analysis: theory Function_Topology
01:50:48 HOL-Analysis: theory Complete_Measure
01:50:48 HOL-Analysis: theory Radon_Nikodym
01:50:49 HOL-Analysis: theory Set_Integral
01:50:49 HOL-Analysis: theory Lebesgue_Measure
01:50:52 HOL-Analysis: theory Henstock_Kurzweil_Integration
01:50:58 HOL-Analysis: theory Bounded_Continuous_Function
01:50:58 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration
01:50:58 HOL-Analysis: theory Integral_Test
01:51:00 HOL-Analysis: theory Complex_Analysis_Basics
01:51:00 HOL-Analysis: theory Interval_Integral
01:51:02 HOL-Analysis: theory Lebesgue_Integral_Substitution
01:51:03 HOL-Analysis: theory Complex_Transcendental
01:51:06 HOL-Analysis: theory Generalised_Binomial_Theorem
01:51:06 HOL-Analysis: theory Harmonic_Numbers
01:51:07 HOL-Analysis: theory Cauchy_Integral_Theorem
01:51:07 HOL-Analysis: theory Further_Topology
01:51:12 HOL-Analysis: theory Jordan_Curve
01:51:14 HOL-Analysis: theory Conformal_Mappings
01:51:14 HOL-Analysis: theory Gamma_Function
01:51:14 HOL-Analysis: theory Winding_Numbers
01:51:16 HOL-Analysis: theory Great_Picard
01:51:21 HOL-Analysis: theory Analysis
01:58:44 Timing HOL-Analysis (8 threads, 433.373s elapsed time, 2056.128s cpu time, 132.000s GC time, factor 4.74)
01:58:44 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis
01:58:44 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/document.pdf
01:58:44 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/outline.pdf
01:58:44 Finished HOL-Analysis (0:09:14 elapsed time, 0:37:49 cpu time, factor 4.09)
01:58:45 Building Ordinary_Differential_Equations ...
01:58:52 Ordinary_Differential_Equations: theory Dense_Linear_Order
01:58:52 Ordinary_Differential_Equations: theory Code_Abstract_Nat
01:58:52 Ordinary_Differential_Equations: theory Code_Target_Int
01:58:52 Ordinary_Differential_Equations: theory Diagonal_Subsequence
01:58:52 Ordinary_Differential_Equations: theory Lattice_Algebras
01:58:52 Ordinary_Differential_Equations: theory Log_Nat
01:58:52 Ordinary_Differential_Equations: theory Code_Target_Nat
01:58:53 Ordinary_Differential_Equations: theory Code_Target_Numeral
01:59:01 Ordinary_Differential_Equations: theory Float
01:59:04 Ordinary_Differential_Equations: theory Approximation
02:00:06 Ordinary_Differential_Equations: theory Bounded_Linear_Operator
02:00:06 Ordinary_Differential_Equations: theory ODE_Auxiliarities
02:00:12 Ordinary_Differential_Equations: theory Initial_Value_Problem
02:00:12 Ordinary_Differential_Equations: theory MVT_Ex
02:00:13 Ordinary_Differential_Equations: theory Multivariate_Taylor
02:00:15 Ordinary_Differential_Equations: theory Picard_Lindeloef_Qualitative
02:00:17 Ordinary_Differential_Equations: theory Flow
02:00:22 Ordinary_Differential_Equations: theory Reachability_Analysis
02:00:22 Ordinary_Differential_Equations: theory Upper_Lower_Solution
02:00:23 Ordinary_Differential_Equations: theory Linear_ODE
02:00:24 Ordinary_Differential_Equations: theory ODE_Analysis
02:02:22 Timing Ordinary_Differential_Equations (8 threads, 171.287s elapsed time, 508.984s cpu time, 11.672s GC time, factor 2.97)
02:02:22 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations
02:02:22 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/document.pdf
02:02:22 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/outline.pdf
02:02:22 Finished Ordinary_Differential_Equations (0:03:35 elapsed time, 0:10:07 cpu time, factor 2.81)
02:02:23 Building HOL-ODE ...
02:02:49 Timing HOL-ODE (8 threads, 0.152s elapsed time, 0.208s cpu time, 0.000s GC time, factor 1.37)
02:02:49 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE
02:02:49 Finished HOL-ODE (0:00:25 elapsed time, 0:00:49 cpu time, factor 1.91)
02:02:49 Building HOL-ODE-Refinement ...
02:02:58 HOL-ODE-Refinement: theory Adhoc_Overloading
02:02:58 HOL-ODE-Refinement: theory AList
02:02:58 HOL-ODE-Refinement: theory Foldi
02:02:58 HOL-ODE-Refinement: theory Boolean_Algebra
02:02:58 HOL-ODE-Refinement: theory Bits
02:02:58 HOL-ODE-Refinement: theory Bit
02:02:58 HOL-ODE-Refinement: theory Quicksort
02:02:58 HOL-ODE-Refinement: theory Omega_Words_Fun
02:02:59 HOL-ODE-Refinement: theory List_More
02:02:59 HOL-ODE-Refinement: theory Misc_Numeric
02:02:59 HOL-ODE-Refinement: theory Misc_Typedef
02:02:59 HOL-ODE-Refinement: theory Bit_Representation
02:02:59 HOL-ODE-Refinement: theory Monad_Syntax
02:02:59 HOL-ODE-Refinement: theory Option_ord
02:02:59 HOL-ODE-Refinement: theory Type_Length
02:03:00 HOL-ODE-Refinement: theory Prio_List
02:03:00 HOL-ODE-Refinement: theory Bits_Bit
02:03:00 HOL-ODE-Refinement: theory RBT_Impl
02:03:00 HOL-ODE-Refinement: theory Refine_Chapter
02:03:00 HOL-ODE-Refinement: theory Refine_Util
02:03:00 HOL-ODE-Refinement: theory While_Combinator
02:03:00 HOL-ODE-Refinement: theory Word_Miscellaneous
02:03:00 HOL-ODE-Refinement: theory Misc
02:03:00 HOL-ODE-Refinement: theory Anti_Unification
02:03:00 HOL-ODE-Refinement: theory Bits_Int
02:03:00 HOL-ODE-Refinement: theory Attr_Comb
02:03:01 HOL-ODE-Refinement: theory Autoref_Data
02:03:01 HOL-ODE-Refinement: theory Named_Sorted_Thms
02:03:01 HOL-ODE-Refinement: theory Mk_Term_Antiquot
02:03:01 HOL-ODE-Refinement: theory Mpat_Antiquot
02:03:01 HOL-ODE-Refinement: theory Tagged_Solver
02:03:01 HOL-ODE-Refinement: theory Select_Solve
02:03:01 HOL-ODE-Refinement: theory Indep_Vars
02:03:01 HOL-ODE-Refinement: theory Mk_Record_Simp
02:03:03 HOL-ODE-Refinement: theory Bool_List_Representation
02:03:04 HOL-ODE-Refinement: theory More_Bits_Int
02:03:04 HOL-ODE-Refinement: theory Word
02:03:07 HOL-ODE-Refinement: theory Bits_Integer
02:03:08 HOL-ODE-Refinement: theory SetIterator
02:03:08 HOL-ODE-Refinement: theory Digraph_Basic
02:03:09 HOL-ODE-Refinement: theory Refine_Lib
02:03:10 HOL-ODE-Refinement: theory SetIteratorOperations
02:03:10 HOL-ODE-Refinement: theory Autoref_Phases
02:03:10 HOL-ODE-Refinement: theory Autoref_Tagging
02:03:11 HOL-ODE-Refinement: theory Refine_Mono_Prover
02:03:11 HOL-ODE-Refinement: theory Relators
02:03:11 HOL-ODE-Refinement: theory Word_Misc
02:03:12 HOL-ODE-Refinement: theory Param_Tool
02:03:12 HOL-ODE-Refinement: theory Param_HOL
02:03:14 HOL-ODE-Refinement: theory Parametricity
02:03:14 HOL-ODE-Refinement: theory Assoc_List
02:03:14 HOL-ODE-Refinement: theory Autoref_Id_Ops
02:03:14 HOL-ODE-Refinement: theory Proper_Iterator
02:03:14 HOL-ODE-Refinement: theory SetIteratorGA
02:03:15 HOL-ODE-Refinement: theory Diff_Array
02:03:15 HOL-ODE-Refinement: theory It_to_It
02:03:15 HOL-ODE-Refinement: theory Autoref_Fix_Rel
02:03:16 HOL-ODE-Refinement: theory Autoref_Translate
02:03:16 HOL-ODE-Refinement: theory Autoref_Relator_Interface
02:03:16 HOL-ODE-Refinement: theory Autoref_Gen_Algo
02:03:16 HOL-ODE-Refinement: theory Autoref_Tool
02:03:18 HOL-ODE-Refinement: theory Autoref_Bindings_HOL
02:03:24 HOL-ODE-Refinement: theory Automatic_Refinement
02:03:24 HOL-ODE-Refinement: theory Idx_Iterator
02:03:24 HOL-ODE-Refinement: theory Intf_Comp
02:03:25 HOL-ODE-Refinement: theory Refine_Misc
02:03:25 HOL-ODE-Refinement: theory Code_Target_Bits_Int
02:03:25 HOL-ODE-Refinement: theory Impl_Array_Stack
02:03:25 HOL-ODE-Refinement: theory Uint
02:03:25 HOL-ODE-Refinement: theory Code_Target_ICF
02:03:26 HOL-ODE-Refinement: theory Uint32
02:03:26 HOL-ODE-Refinement: theory RefineG_Domain
02:03:26 HOL-ODE-Refinement: theory RefineG_Transfer
02:03:26 HOL-ODE-Refinement: theory RefineG_Assert
02:03:26 HOL-ODE-Refinement: theory RefineG_Recursion
02:03:27 HOL-ODE-Refinement: theory Refine_Basic
02:03:27 HOL-ODE-Refinement: theory RefineG_While
02:03:28 HOL-ODE-Refinement: theory Refine_Det
02:03:29 HOL-ODE-Refinement: theory HashCode
02:03:30 HOL-ODE-Refinement: theory Intf_Hash
02:03:31 HOL-ODE-Refinement: theory Gen_Hash
02:03:32 HOL-ODE-Refinement: theory Refine_Heuristics
02:03:32 HOL-ODE-Refinement: theory Refine_Leof
02:03:32 HOL-ODE-Refinement: theory Refine_Pfun
02:03:32 HOL-ODE-Refinement: theory Refine_While
02:03:35 HOL-ODE-Refinement: theory Refine_Transfer
02:03:35 HOL-ODE-Refinement: theory Autoref_Monadic
02:03:36 HOL-ODE-Refinement: theory Refine_Automation
02:03:36 HOL-ODE-Refinement: theory Refine_Foreach
02:03:39 HOL-ODE-Refinement: theory Refine_Monadic
02:03:40 HOL-ODE-Refinement: theory Gen_Iterator
02:03:40 HOL-ODE-Refinement: theory Intf_Map
02:03:41 HOL-ODE-Refinement: theory Intf_Set
02:03:41 HOL-ODE-Refinement: theory Iterator
02:03:42 HOL-ODE-Refinement: theory Impl_Cfun_Set
02:03:42 HOL-ODE-Refinement: theory Array_Iterator
02:03:42 HOL-ODE-Refinement: theory Gen_Map
02:03:42 HOL-ODE-Refinement: theory Gen_Map2Set
02:03:42 HOL-ODE-Refinement: theory Gen_Set
02:03:43 HOL-ODE-Refinement: theory Impl_Bit_Set
02:03:43 HOL-ODE-Refinement: theory Impl_List_Set
02:03:43 HOL-ODE-Refinement: theory Impl_Uv_Set
02:03:44 HOL-ODE-Refinement: theory Impl_Array_Map
02:03:44 HOL-ODE-Refinement: theory Impl_List_Map
02:03:45 HOL-ODE-Refinement: theory Impl_Array_Hash_Map
02:03:54 HOL-ODE-Refinement: theory RBT_add
02:03:57 HOL-ODE-Refinement: theory Impl_RBT_Map
02:04:07 HOL-ODE-Refinement: theory GenCF_No_Comp
02:04:15 HOL-ODE-Refinement: theory Refine_Dflt_No_Comp
02:05:49 Timing HOL-ODE-Refinement (8 threads, 113.724s elapsed time, 601.200s cpu time, 28.196s GC time, factor 5.29)
02:05:49 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Refinement
02:05:49 Finished HOL-ODE-Refinement (0:02:59 elapsed time, 0:13:59 cpu time, factor 4.68)
02:05:50 Building HOL-ODE-Numerics ...
02:06:07 HOL-ODE-Numerics: theory Permutation
02:06:07 HOL-ODE-Numerics: theory Quotient_Syntax
02:06:07 HOL-ODE-Numerics: theory Float_Real
02:06:07 HOL-ODE-Numerics: theory Euclidean_Space_Explicit
02:06:07 HOL-ODE-Numerics: theory Counterclockwise
02:06:07 HOL-ODE-Numerics: theory Quotient_Set
02:06:07 HOL-ODE-Numerics: theory Affine_Form
02:06:07 HOL-ODE-Numerics: theory Executable_Euclidean_Space
02:06:09 HOL-ODE-Numerics: theory Counterclockwise_Vector
02:06:10 HOL-ODE-Numerics: theory Counterclockwise_2D_Strict
02:06:11 HOL-ODE-Numerics: theory Counterclockwise_2D_Arbitrary
02:06:11 HOL-ODE-Numerics: theory Polygon
02:06:12 HOL-ODE-Numerics: theory Affine_Approximation
02:06:34 HOL-ODE-Numerics: theory Affine_Code
02:06:37 HOL-ODE-Numerics: theory Straight_Line_Program
02:06:37 HOL-ODE-Numerics: theory Ex_Affine_Approximation
02:06:37 HOL-ODE-Numerics: theory Ex_Ineqs
02:06:38 HOL-ODE-Numerics: theory Intersection
02:06:43 HOL-ODE-Numerics: theory Ex_Inter
02:08:01 HOL-ODE-Numerics: theory Affine_Arithmetic
02:08:03 HOL-ODE-Numerics: theory Char_ord
02:08:03 HOL-ODE-Numerics: theory Generator_Aux
02:08:03 HOL-ODE-Numerics: theory ICF_Tools
02:08:03 HOL-ODE-Numerics: theory Derive_Manager
02:08:03 HOL-ODE-Numerics: theory Optimize_Integer
02:08:03 HOL-ODE-Numerics: theory One_Step_Method
02:08:03 HOL-ODE-Numerics: theory Autoref_Misc
02:08:03 HOL-ODE-Numerics: theory Ord_Code_Preproc
02:08:03 HOL-ODE-Numerics: theory Code_Char
02:08:03 HOL-ODE-Numerics: theory Show
02:08:03 HOL-ODE-Numerics: theory Locale_Code
02:08:03 HOL-ODE-Numerics: theory Optimize_Float
02:08:04 HOL-ODE-Numerics: theory Runge_Kutta
02:08:05 HOL-ODE-Numerics: theory Show_Instances
02:08:07 HOL-ODE-Numerics: theory Print
02:08:11 HOL-ODE-Numerics: theory Refine_Folds
02:08:11 HOL-ODE-Numerics: theory Refine_String
02:08:11 HOL-ODE-Numerics: theory Weak_Set
02:08:14 HOL-ODE-Numerics: theory Plot
02:08:22 HOL-ODE-Numerics: theory Refine_Rigorous_Numerics
02:08:52 HOL-ODE-Numerics: theory Refine_Reachability_Analysis
02:19:23 HOL-ODE-Numerics: theory Refine_Rigorous_Numerics_Aform
02:19:34 HOL-ODE-Numerics: theory ODE_Numerics
02:20:53 Timing HOL-ODE-Numerics (8 threads, 821.742s elapsed time, 2000.300s cpu time, 69.496s GC time, factor 2.43)
02:20:53 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Numerics
02:20:53 Finished HOL-ODE-Numerics (0:15:02 elapsed time, 0:36:31 cpu time, factor 2.43)
02:20:54 Running Flyspeck-Tame ...
02:21:03 Flyspeck-Tame: theory Trie
02:21:06 Flyspeck-Tame: theory Tries
02:21:27 Flyspeck-Tame: theory Arch
02:21:27 Flyspeck-Tame: theory ListAux
02:21:27 Flyspeck-Tame: theory Quasi_Order
02:21:27 Flyspeck-Tame: theory IArray_Syntax
02:21:27 Flyspeck-Tame: theory RTranCl
02:21:27 Flyspeck-Tame: theory PlaneGraphIso
02:21:27 Flyspeck-Tame: theory Worklist
02:21:28 Flyspeck-Tame: theory Maps
02:21:28 Flyspeck-Tame: theory ListSum
02:21:28 Flyspeck-Tame: theory Rotation
02:21:29 Flyspeck-Tame: theory Graph
02:21:31 Flyspeck-Tame: theory Enumerator
02:21:31 Flyspeck-Tame: theory FaceDivision
02:21:31 Flyspeck-Tame: theory GraphProps
02:21:32 Flyspeck-Tame: theory Tame
02:21:32 Flyspeck-Tame: theory Plane
02:21:32 Flyspeck-Tame: theory EnumeratorProps
02:21:32 Flyspeck-Tame: theory TameProps
02:21:32 Flyspeck-Tame: theory Plane1
02:21:33 Flyspeck-Tame: theory FaceDivisionProps
02:21:33 Flyspeck-Tame: theory Generator
02:21:33 Flyspeck-Tame: theory TameEnum
02:21:37 Flyspeck-Tame: theory Invariants
02:21:41 Flyspeck-Tame: theory PlaneProps
02:21:41 Flyspeck-Tame: theory Plane1Props
02:21:42 Flyspeck-Tame: theory ScoreProps
02:21:44 Flyspeck-Tame: theory LowerBound
02:21:44 Flyspeck-Tame: theory GeneratorProps
02:21:46 Flyspeck-Tame: theory TameEnumProps
02:21:47 Flyspeck-Tame: theory ArchCompAux
02:21:49 Flyspeck-Tame: theory ArchCompProps
02:21:49 Flyspeck-Tame: theory ArchComp
02:21:49 Flyspeck-Tame: theory Completeness
09:47:02 Timing Flyspeck-Tame (8 threads, 26750.256s elapsed time, 39931.576s cpu time, 661.480s GC time, factor 1.49)
09:47:02 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame
09:47:02 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf
09:47:02 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf
09:47:02 Finished Flyspeck-Tame (7:26:08 elapsed time, 11:05:53 cpu time, factor 1.49)
09:47:03 Iptables_Semantics_Examples CANCELLED
09:47:03 Running AODV ...
09:47:08 AODV: theory Aodv_Basic
09:47:09 AODV: theory A_Norreqid
09:47:09 AODV: theory Aodv_Data
09:47:09 AODV: theory Aodv_Message
09:47:09 AODV: theory E_All_ABCD
09:47:09 AODV: theory D_Fwdrreqs
09:47:09 AODV: theory C_Gtobcast
09:47:09 AODV: theory B_Fwdrreps
09:47:10 AODV: theory A_Aodv_Data
09:47:10 AODV: theory A_Aodv_Message
09:47:10 AODV: theory D_Aodv_Data
09:47:10 AODV: theory D_Aodv_Message
09:47:10 AODV: theory C_Aodv_Data
09:47:10 AODV: theory B_Aodv_Data
09:47:12 AODV: theory B_Aodv_Message
09:47:12 AODV: theory Fresher
09:47:12 AODV: theory C_Fresher
09:47:12 AODV: theory A_Fresher
09:47:12 AODV: theory B_Fresher
09:47:12 AODV: theory C_Aodv_Message
09:47:12 AODV: theory D_Fresher
09:47:13 AODV: theory E_Aodv_Data
09:47:13 AODV: theory E_Aodv_Message
09:47:13 AODV: theory A_Aodv
09:47:13 AODV: theory Aodv
09:47:13 AODV: theory D_Aodv
09:47:14 AODV: theory B_Aodv
09:47:14 AODV: theory E_Fresher
09:47:14 AODV: theory C_Aodv
09:47:15 AODV: theory E_Aodv
09:48:25 AODV: theory Aodv_Predicates
09:48:25 AODV: theory Loop_Freedom
09:48:25 AODV: theory Quality_Increases
09:48:26 AODV: theory Seq_Invariants
09:48:27 AODV: theory OAodv
09:48:27 AODV: theory Global_Invariants
09:48:28 AODV: theory Aodv_Loop_Freedom
09:48:40 AODV: theory A_Aodv_Predicates
09:48:40 AODV: theory A_OAodv
09:48:41 AODV: theory A_Loop_Freedom
09:48:41 AODV: theory A_Quality_Increases
09:48:41 AODV: theory A_Seq_Invariants
09:48:42 AODV: theory A_Global_Invariants
09:48:43 AODV: theory A_Aodv_Loop_Freedom
09:48:52 AODV: theory C_Aodv_Predicates
09:48:52 AODV: theory C_OAodv
09:48:52 AODV: theory C_Loop_Freedom
09:48:53 AODV: theory C_Quality_Increases
09:48:53 AODV: theory C_Seq_Invariants
09:48:53 AODV: theory D_Aodv_Predicates
09:48:53 AODV: theory D_OAodv
09:48:53 AODV: theory C_Global_Invariants
09:48:54 AODV: theory D_Loop_Freedom
09:48:54 AODV: theory D_Quality_Increases
09:48:54 AODV: theory D_Seq_Invariants
09:48:55 AODV: theory C_Aodv_Loop_Freedom
09:48:55 AODV: theory D_Global_Invariants
09:48:56 AODV: theory D_Aodv_Loop_Freedom
09:48:57 AODV: theory E_Aodv_Predicates
09:48:57 AODV: theory E_OAodv
09:48:57 AODV: theory E_Loop_Freedom
09:48:57 AODV: theory E_Quality_Increases
09:48:58 AODV: theory E_Seq_Invariants
09:48:58 AODV: theory B_Aodv_Predicates
09:48:58 AODV: theory B_OAodv
09:48:59 AODV: theory E_Global_Invariants
09:48:59 AODV: theory B_Loop_Freedom
09:48:59 AODV: theory B_Quality_Increases
09:48:59 AODV: theory B_Seq_Invariants
09:49:00 AODV: theory E_Aodv_Loop_Freedom
09:49:00 AODV: theory B_Global_Invariants
09:49:01 AODV: theory B_Aodv_Loop_Freedom
09:49:07 AODV: theory All
12:37:10 Timing AODV (8 threads, 10190.555s elapsed time, 53353.652s cpu time, 4865.348s GC time, factor 5.24)
12:37:10 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV
12:37:10 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/document.pdf
12:37:10 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/outline.pdf
12:37:10 Finished AODV (2:50:06 elapsed time, 14:49:35 cpu time, factor 5.23)
12:37:11 Running ConcurrentGC ...
12:37:21 ConcurrentGC: theory Model
12:37:40 ConcurrentGC: theory Tactics
12:37:48 ConcurrentGC: theory Proofs_basis
12:37:52 ConcurrentGC: theory TSO
12:38:07 ConcurrentGC: theory Handshakes
12:40:45 ConcurrentGC: theory MarkObject
12:43:30 ConcurrentGC: theory StrongTricolour
12:44:35 ConcurrentGC: theory Proofs
12:44:36 ConcurrentGC: theory Concrete_heap
12:44:38 ConcurrentGC: theory Concrete
14:52:59 Timing ConcurrentGC (8 threads, 8135.317s elapsed time, 26795.424s cpu time, 2390.484s GC time, factor 3.29)
14:52:59 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC
14:52:59 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf
14:52:59 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf
14:52:59 Finished ConcurrentGC (2:15:48 elapsed time, 7:26:50 cpu time, factor 3.29)
14:53:00 Running JinjaThreads ...
14:53:09 JinjaThreads: theory Adhoc_Overloading
14:53:09 JinjaThreads: theory Lattice_Syntax
14:53:09 JinjaThreads: theory AList
14:53:09 JinjaThreads: theory Cancellation
14:53:09 JinjaThreads: theory Char_ord
14:53:09 JinjaThreads: theory Code_Abstract_Nat
14:53:09 JinjaThreads: theory Dlist
14:53:09 JinjaThreads: theory FingerTree
14:53:09 JinjaThreads: theory Complete_Partial_Order2
14:53:09 JinjaThreads: theory Foldi
14:53:09 JinjaThreads: theory Code_Target_Nat
14:53:10 JinjaThreads: theory Code_Char
14:53:10 JinjaThreads: theory Code_Target_Int
14:53:10 JinjaThreads: theory ICF_Tools
14:53:10 JinjaThreads: theory Infinite_Set
14:53:10 JinjaThreads: theory More_Bits_Int
14:53:10 JinjaThreads: theory Multiset
14:53:10 JinjaThreads: theory Code_Target_Numeral
14:53:10 JinjaThreads: theory Omega_Words_Fun
14:53:10 JinjaThreads: theory Monad_Syntax
14:53:11 JinjaThreads: theory Nat_Bijection
14:53:11 JinjaThreads: theory Old_Datatype
14:53:12 JinjaThreads: theory Option_ord
14:53:12 JinjaThreads: theory Ord_Code_Preproc
14:53:12 JinjaThreads: theory Trie
14:53:12 JinjaThreads: theory Locale_Code
14:53:12 JinjaThreads: theory FinFun
14:53:13 JinjaThreads: theory Predicate_Compile_Alternative_Defs
14:53:13 JinjaThreads: theory Prio_List
14:53:13 JinjaThreads: theory RBT_Impl
14:53:14 JinjaThreads: theory Bits_Integer
14:53:14 JinjaThreads: theory Countable
14:53:15 JinjaThreads: theory Record_Intf
14:53:15 JinjaThreads: theory Refine_Chapter
14:53:15 JinjaThreads: theory Refine_Util
14:53:15 JinjaThreads: theory Set_Monad
14:53:15 JinjaThreads: theory Set_without_equal
14:53:16 JinjaThreads: theory Anti_Unification
14:53:16 JinjaThreads: theory Attr_Comb
14:53:16 JinjaThreads: theory Named_Sorted_Thms
14:53:16 JinjaThreads: theory Autoref_Data
14:53:16 JinjaThreads: theory Mk_Term_Antiquot
14:53:16 JinjaThreads: theory Mpat_Antiquot
14:53:16 JinjaThreads: theory Tagged_Solver
14:53:16 JinjaThreads: theory Countable_Set
14:53:16 JinjaThreads: theory Indep_Vars
14:53:16 JinjaThreads: theory Mk_Record_Simp
14:53:16 JinjaThreads: theory Select_Solve
14:53:16 JinjaThreads: theory Simps_Case_Conv
14:53:16 JinjaThreads: theory Sublist
14:53:16 JinjaThreads: theory Transitive_Closure_Table
14:53:16 JinjaThreads: theory While_Combinator
14:53:17 JinjaThreads: theory Countable_Complete_Lattices
14:53:17 JinjaThreads: theory Auxiliary
14:53:18 JinjaThreads: theory DatRef
14:53:18 JinjaThreads: theory Word_Misc
14:53:18 JinjaThreads: theory BinomialHeap
14:53:19 JinjaThreads: theory Quicksort
14:53:19 JinjaThreads: theory List_More
14:53:20 JinjaThreads: theory SkewBinomialHeap
14:53:20 JinjaThreads: theory Misc
14:53:22 JinjaThreads: theory Order_Continuity
14:53:23 JinjaThreads: theory Extended_Nat
14:53:25 JinjaThreads: theory Coinductive_Nat
14:53:28 JinjaThreads: theory Coinductive_List
14:53:32 JinjaThreads: theory SetIterator
14:53:32 JinjaThreads: theory Digraph_Basic
14:53:33 JinjaThreads: theory Sorted_List_Operations
14:53:34 JinjaThreads: theory Refine_Lib
14:53:34 JinjaThreads: theory Code_Target_Bits_Int
14:53:34 JinjaThreads: theory Code_Target_ICF
14:53:34 JinjaThreads: theory Uint32
14:53:35 JinjaThreads: theory SetIteratorOperations
14:53:35 JinjaThreads: theory Autoref_Phases
14:53:35 JinjaThreads: theory Autoref_Tagging
14:53:35 JinjaThreads: theory Refine_Mono_Prover
14:53:35 JinjaThreads: theory Relators
14:53:36 JinjaThreads: theory Param_Tool
14:53:37 JinjaThreads: theory Param_HOL
14:53:37 JinjaThreads: theory HashCode
14:53:38 JinjaThreads: theory Parametricity
14:53:39 JinjaThreads: theory Autoref_Id_Ops
14:53:39 JinjaThreads: theory Assoc_List
14:53:39 JinjaThreads: theory Dlist_add
14:53:39 JinjaThreads: theory Proper_Iterator
14:53:39 JinjaThreads: theory SetIteratorGA
14:53:39 JinjaThreads: theory Diff_Array
14:53:40 JinjaThreads: theory Trie_Impl
14:53:40 JinjaThreads: theory It_to_It
14:53:40 JinjaThreads: theory Autoref_Fix_Rel
14:53:40 JinjaThreads: theory Trie2
14:53:41 JinjaThreads: theory Autoref_Translate
14:53:41 JinjaThreads: theory Autoref_Relator_Interface
14:53:41 JinjaThreads: theory Autoref_Gen_Algo
14:53:41 JinjaThreads: theory Autoref_Tool
14:53:42 JinjaThreads: theory Lazy_LList
14:53:42 JinjaThreads: theory TLList
14:53:42 JinjaThreads: theory Autoref_Bindings_HOL
14:53:46 JinjaThreads: theory Lazy_TLList
14:53:48 JinjaThreads: theory Automatic_Refinement
14:53:48 JinjaThreads: theory Idx_Iterator
14:53:48 JinjaThreads: theory Refine_Misc
14:53:50 JinjaThreads: theory RefineG_Domain
14:53:50 JinjaThreads: theory RefineG_Transfer
14:53:50 JinjaThreads: theory RefineG_Assert
14:53:51 JinjaThreads: theory RefineG_Recursion
14:53:51 JinjaThreads: theory Refine_Basic
14:53:51 JinjaThreads: theory RefineG_While
14:53:52 JinjaThreads: theory Refine_Det
14:53:56 JinjaThreads: theory Refine_Heuristics
14:53:56 JinjaThreads: theory Refine_Leof
14:53:57 JinjaThreads: theory Refine_Pfun
14:53:57 JinjaThreads: theory Refine_While
14:53:59 JinjaThreads: theory Refine_Transfer
14:54:00 JinjaThreads: theory Autoref_Monadic
14:54:00 JinjaThreads: theory Refine_Automation
14:54:00 JinjaThreads: theory Refine_Foreach
14:54:04 JinjaThreads: theory Refine_Monadic
14:54:05 JinjaThreads: theory Gen_Iterator
14:54:05 JinjaThreads: theory Intf_Map
14:54:05 JinjaThreads: theory Intf_Set
14:54:06 JinjaThreads: theory Iterator
14:54:07 JinjaThreads: theory Array_Iterator
14:54:07 JinjaThreads: theory ICF_Spec_Base
14:54:07 JinjaThreads: theory AnnotatedListSpec
14:54:07 JinjaThreads: theory ListSpec
14:54:08 JinjaThreads: theory MapSpec
14:54:08 JinjaThreads: theory PrioSpec
14:54:08 JinjaThreads: theory PrioUniqueSpec
14:54:10 JinjaThreads: theory SetSpec
14:54:10 JinjaThreads: theory BinoPrioImpl
14:54:10 JinjaThreads: theory RBT
14:54:11 JinjaThreads: theory ListGA
14:54:11 JinjaThreads: theory SkewPrioImpl
14:54:11 JinjaThreads: theory FTAnnotatedListImpl
14:54:12 JinjaThreads: theory PrioByAnnotatedList
14:54:12 JinjaThreads: theory Fifo
14:54:13 JinjaThreads: theory PrioUniqueByAnnotatedList
14:54:13 JinjaThreads: theory RBT_add
14:54:15 JinjaThreads: theory FTPrioImpl
14:54:16 JinjaThreads: theory Algos
14:54:16 JinjaThreads: theory SetIndex
14:54:16 JinjaThreads: theory SetIteratorCollectionsGA
14:54:16 JinjaThreads: theory FTPrioUniqueImpl
14:54:17 JinjaThreads: theory MapGA
14:54:17 JinjaThreads: theory SetGA
14:54:21 JinjaThreads: theory ArrayMapImpl
14:54:21 JinjaThreads: theory ListMapImpl
14:54:22 JinjaThreads: theory ListMapImpl_Invar
14:54:22 JinjaThreads: theory TrieMapImpl
14:54:22 JinjaThreads: theory RBTMapImpl
14:54:24 JinjaThreads: theory ArrayHashMap_Impl
14:54:25 JinjaThreads: theory ListSetImpl
14:54:25 JinjaThreads: theory ListSetImpl_Invar
14:54:25 JinjaThreads: theory ListSetImpl_NotDist
14:54:26 JinjaThreads: theory ListSetImpl_Sorted
14:54:27 JinjaThreads: theory SetByMap
14:54:27 JinjaThreads: theory HashMap_Impl
14:54:29 JinjaThreads: theory ArrayHashMap
14:54:30 JinjaThreads: theory ArraySetImpl
14:54:30 JinjaThreads: theory TrieSetImpl
14:54:30 JinjaThreads: theory RBTSetImpl
14:54:30 JinjaThreads: theory HashMap
14:54:33 JinjaThreads: theory ArrayHashSet
14:54:34 JinjaThreads: theory HashSet
14:54:34 JinjaThreads: theory MapStdImpl
14:54:39 JinjaThreads: theory SetStdImpl
14:54:45 JinjaThreads: theory ICF_Impl
14:54:52 JinjaThreads: theory ICF_Refine_Monadic
14:54:54 JinjaThreads: theory ICF_Autoref
14:55:00 JinjaThreads: theory Collections
14:55:00 JinjaThreads: theory CollectionsV1
14:55:14 JinjaThreads: theory JT_ICF
14:55:14 JinjaThreads: theory Basic_Main
14:55:54 JinjaThreads: theory ListIndex
14:55:54 JinjaThreads: theory Mapping
14:55:54 JinjaThreads: theory Orders
14:55:54 JinjaThreads: theory Prefix_Order
14:55:54 JinjaThreads: theory FWState
14:55:54 JinjaThreads: theory Type
14:55:54 JinjaThreads: theory LTS
14:55:54 JinjaThreads: theory Semilat
14:55:55 JinjaThreads: theory Err
14:55:57 JinjaThreads: theory AList_Mapping
14:55:58 JinjaThreads: theory Listn
14:55:58 JinjaThreads: theory Opt
14:55:58 JinjaThreads: theory Product
14:55:59 JinjaThreads: theory Semilattices
14:56:00 JinjaThreads: theory Typing_Framework
14:56:01 JinjaThreads: theory SemilatAlg
14:56:01 JinjaThreads: theory Decl
14:56:01 JinjaThreads: theory Kildall
14:56:01 JinjaThreads: theory LBVSpec
14:56:03 JinjaThreads: theory Typing_Framework_err
14:56:03 JinjaThreads: theory Bisimulation
14:56:04 JinjaThreads: theory LBVComplete
14:56:04 JinjaThreads: theory LBVCorrect
14:56:12 JinjaThreads: theory Abstract_BV
14:56:14 JinjaThreads: theory TypeRel
14:56:19 JinjaThreads: theory TypeRelRefine
14:56:19 JinjaThreads: theory Value
14:56:23 JinjaThreads: theory Exceptions
14:56:23 JinjaThreads: theory Heap
14:56:24 JinjaThreads: theory SystemClasses
14:56:26 JinjaThreads: theory MM
14:56:27 JinjaThreads: theory State
14:56:34 JinjaThreads: theory FWCondAction
14:56:34 JinjaThreads: theory FWInterrupt
14:56:34 JinjaThreads: theory FWWait
14:56:34 JinjaThreads: theory FWThread
14:56:34 JinjaThreads: theory FWLock
14:56:34 JinjaThreads: theory Observable_Events
14:56:37 JinjaThreads: theory FWLocking
14:56:38 JinjaThreads: theory FWLockingThread
14:56:38 JinjaThreads: theory FWWellform
14:56:39 JinjaThreads: theory FWLifting
14:56:39 JinjaThreads: theory FWSemantics
14:56:42 JinjaThreads: theory JMM_Spec
14:56:42 JinjaThreads: theory JVMState
14:56:42 JinjaThreads: theory StartConfig
14:56:43 JinjaThreads: theory FWLiftingSem
14:56:43 JinjaThreads: theory FWProgressAux
14:56:44 JinjaThreads: theory Conform
14:56:44 JinjaThreads: theory State_Refinement
14:56:45 JinjaThreads: theory FWDeadlock
14:56:45 JinjaThreads: theory FWLTS
14:56:48 JinjaThreads: theory ConformThreaded
14:56:48 JinjaThreads: theory ExternalCall
14:56:49 JinjaThreads: theory FWProgress
14:56:49 JinjaThreads: theory SC
14:56:50 JinjaThreads: theory SC_Collections
14:56:56 JinjaThreads: theory JMM_DRF
14:56:56 JinjaThreads: theory SC_Legal
14:56:57 JinjaThreads: theory FWBisimulation
14:56:57 JinjaThreads: theory FWInitFinLift
14:56:58 JinjaThreads: theory Non_Speculative
14:56:58 JinjaThreads: theory Scheduler
14:57:01 JinjaThreads: theory HB_Completion
14:57:01 JinjaThreads: theory SC_Completion
14:57:35 JinjaThreads: theory ExternalCall_Execute
14:57:36 JinjaThreads: theory WellForm
14:57:42 JinjaThreads: theory BinOp
14:57:42 JinjaThreads: theory ExternalCallWF
14:57:42 JinjaThreads: theory JMM_Heap
14:57:56 JinjaThreads: theory SemiType
14:57:57 JinjaThreads: theory Random_Scheduler
14:57:59 JinjaThreads: theory JMM_Type
14:58:00 JinjaThreads: theory JMM_Type2
14:58:04 JinjaThreads: theory JVM_SemiType
14:58:05 JinjaThreads: theory Round_Robin
14:58:07 JinjaThreads: theory JMM_Framework
14:58:19 JinjaThreads: theory SC_Schedulers
14:58:20 JinjaThreads: theory Expr
14:58:22 JinjaThreads: theory JVMInstructions
14:58:26 JinjaThreads: theory PCompiler
14:58:27 JinjaThreads: theory PCompilerRefine
14:58:37 JinjaThreads: theory JVMExceptions
14:58:37 JinjaThreads: theory Effect
14:58:37 JinjaThreads: theory JVMHeap
14:58:44 JinjaThreads: theory CallExpr
14:58:45 JinjaThreads: theory DefAss
14:58:46 JinjaThreads: theory WWellForm
14:58:46 JinjaThreads: theory JHeap
14:58:48 JinjaThreads: theory WellType
14:58:57 JinjaThreads: theory JVMExecInstr
14:58:57 JinjaThreads: theory ToString
14:59:00 JinjaThreads: theory J1State
14:59:01 JinjaThreads: theory Annotate
14:59:02 JinjaThreads: theory JVMExec
14:59:04 JinjaThreads: theory Compiler1
14:59:04 JinjaThreads: theory Compiler2
14:59:06 JinjaThreads: theory JVMDefensive
14:59:10 JinjaThreads: theory JVMExec_Execute
14:59:11 JinjaThreads: theory J1Heap
14:59:13 JinjaThreads: theory JVMThreaded
14:59:18 JinjaThreads: theory J1WellType
14:59:19 JinjaThreads: theory SmallStep
14:59:21 JinjaThreads: theory Compiler
14:59:22 JinjaThreads: theory Exception_Tables
14:59:25 JinjaThreads: theory J1WellForm
14:59:25 JinjaThreads: theory JWellForm
14:59:27 JinjaThreads: theory WellTypeRT
14:59:27 JinjaThreads: theory JMM_Typesafe
14:59:28 JinjaThreads: theory JJ1WellForm
14:59:28 JinjaThreads: theory Preprocessor
14:59:36 JinjaThreads: theory JMM_JVM
14:59:36 JinjaThreads: theory JVM_Main
15:03:16 JinjaThreads: theory JMM_Common
15:03:21 JinjaThreads: theory BVSpec
15:03:21 JinjaThreads: theory EffectMono
15:03:21 JinjaThreads: theory TF_JVM
15:03:21 JinjaThreads: theory BVConform
15:03:21 JinjaThreads: theory TypeComp
15:03:23 JinjaThreads: theory JMM_Typesafe2
15:03:25 JinjaThreads: theory BVExec
15:03:26 JinjaThreads: theory LBVJVM
15:03:27 JinjaThreads: theory BVSpecTypeSafe
15:03:35 JinjaThreads: theory BVNoTypeError
15:03:38 JinjaThreads: theory JVMTau
15:03:38 JinjaThreads: theory BCVExec
15:03:38 JinjaThreads: theory JVMExec_Execute2
15:03:38 JinjaThreads: theory BVProgressThreaded
15:03:56 JinjaThreads: theory FWBisimDeadlock
15:03:56 JinjaThreads: theory J1
15:03:56 JinjaThreads: theory FWBisimLift
15:04:00 JinjaThreads: theory Execs
15:04:13 JinjaThreads: theory DefAssPreservation
15:04:14 JinjaThreads: theory Threaded
15:04:15 JinjaThreads: theory Progress
15:04:18 JinjaThreads: theory Common_Main
15:04:20 JinjaThreads: theory TypeSafe
15:04:26 JinjaThreads: theory J1Deadlock
15:04:34 JinjaThreads: theory J0
15:04:34 JinjaThreads: theory JMM_J
15:04:34 JinjaThreads: theory ProgressThreaded
15:04:35 JinjaThreads: theory J_Execute
15:04:45 JinjaThreads: theory J1JVMBisim
15:04:54 JinjaThreads: theory JVMDeadlocked
15:04:55 JinjaThreads: theory DRF_JVM
15:04:55 JinjaThreads: theory JVM_Execute
15:04:55 JinjaThreads: theory JVM_Execute2
15:04:58 JinjaThreads: theory DRF_J
15:04:59 JinjaThreads: theory Deadlocked
15:05:06 JinjaThreads: theory J_Main
15:05:21 JinjaThreads: theory J0Bisim
15:05:24 JinjaThreads: theory BV_Main
15:05:24 JinjaThreads: theory J0J1Bisim
15:05:39 JinjaThreads: theory Code_Generation
15:06:05 JinjaThreads: theory ApprenticeChallenge
15:06:06 JinjaThreads: theory BufferExample
15:06:15 JinjaThreads: theory Java2Jinja
15:06:19 JinjaThreads: theory Correctness1
15:06:22 JinjaThreads: theory Correctness1Threaded
15:11:17 JinjaThreads: theory Examples_Main
15:12:30 JinjaThreads: theory JMM_J_Typesafe
15:12:33 JinjaThreads: theory JMM_JVM_Typesafe
15:13:22 JinjaThreads: theory Execute_Main
15:14:22 JinjaThreads: theory J1JVM
15:14:23 JinjaThreads: theory JVMJ1
15:15:58 JinjaThreads: theory Correctness2
15:18:54 JinjaThreads: theory Correctness
15:29:36 JinjaThreads: theory Compiler_Main
15:29:38 JinjaThreads: theory JMM_Compiler
15:29:45 JinjaThreads: theory SC_Interp
15:34:13 JinjaThreads: theory JMM_Interp
15:34:17 JinjaThreads: theory JMM_Compiler_Type2
15:34:19 JinjaThreads: theory JMM
15:34:22 JinjaThreads: theory MM_Main
15:34:32 JinjaThreads: theory JinjaThreads
15:38:27 Timing JinjaThreads (8 threads, 2659.509s elapsed time, 12513.152s cpu time, 3527.412s GC time, factor 4.71)
15:38:27 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads
15:38:27 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf
15:38:27 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf
15:38:27 Finished JinjaThreads (0:45:22 elapsed time, 3:30:42 cpu time, factor 4.64)
15:38:28 Running HOL-ODE-Examples ...
15:38:52 HOL-ODE-Examples: theory Parallel
15:38:52 HOL-ODE-Examples: theory Initials
15:38:52 HOL-ODE-Examples: theory Example_Utilities
15:38:52 HOL-ODE-Examples: theory Example1
15:38:52 HOL-ODE-Examples: theory Example3
15:38:52 HOL-ODE-Examples: theory Example_Bessel
15:38:52 HOL-ODE-Examples: theory Example_Exp
15:38:52 HOL-ODE-Examples: theory Example_Lorenz_Classic
15:38:52 HOL-ODE-Examples: theory Example_Oil
15:38:53 HOL-ODE-Examples: theory Example_Variational_Equation
15:39:06 HOL-ODE-Examples: theory Example_van_der_Pol
15:41:43 HOL-ODE-Examples: theory Lorenz_Approximation
15:44:55 HOL-ODE-Examples: theory Lorenz_Parallel
15:51:07 HOL-ODE-Examples: theory ODE_Examples
15:51:13 Timing HOL-ODE-Examples (8 threads, 740.598s elapsed time, 3672.536s cpu time, 705.692s GC time, factor 4.96)
15:51:13 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Examples
15:51:13 Finished HOL-ODE-Examples (0:12:44 elapsed time, 1:01:36 cpu time, factor 4.83)
15:51:14 Unfinished session(s): IP_Addresses, Iptables_Semantics, Iptables_Semantics_Examples, Routing, Simple_Firewall, Word_Lib
15:51:14 
15:51:14 === TIMING ===
15:51:14 
15:51:14 Group slow: 13:30:11 elapsed time, 37:54:38 cpu time, factor 2.81
15:51:14 Group AFP: 13:55:55 elapsed time, 39:06:56 cpu time, factor 2.81
15:51:14 Group main: 0:19:06 elapsed time, 1:12:07 cpu time, factor 3.77
15:51:14 Group timing: 0:13:54 elapsed time, 0:57:24 cpu time, factor 4.13
15:51:14 Group very_slow: 7:26:08 elapsed time, 11:05:53 cpu time, factor 1.49
15:51:14 Overall: 14:15:54 elapsed time, 40:19:23 cpu time, factor 2.83
15:51:14 
15:51:14 === FAILED SESSIONS ===
15:51:14 
15:51:14 Session Routing: CANCELLED
15:51:14 Session Simple_Firewall: CANCELLED
15:51:14 Session Iptables_Semantics_Examples: CANCELLED
15:51:14 Session Iptables_Semantics: CANCELLED
15:51:14 Session Word_Lib: FAILED 2
15:51:14 Session IP_Addresses: CANCELLED
15:51:14 Build step 'Execute shell' marked build as failure
15:51:14 Archiving artifacts
15:51:15 Started calculate disk usage of build
15:51:15 Finished Calculation of disk usage of build in 0 seconds
15:51:15 Started calculate disk usage of workspace
15:51:16 Finished Calculation of disk usage of workspace in 0 seconds
15:51:16 No emails were triggered.
15:51:16 Finished: FAILURE