Skip to content
Failed

Console Output

01:33:18 Started by an SCM change

01:33:18 [EnvInject] - Loading node environment variables.

01:33:18 Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow

01:33:19 [isabelle-nightly-slow] $ hg showconfig paths.default

01:33:19 [isabelle-nightly-slow] $ hg pull --rev default

01:33:19 pulling from http://isabelle.in.tum.de/repos/isabelle/

01:33:19 searching for changes

01:33:19 no changes found

01:33:19 [isabelle-nightly-slow] $ hg update --clean --rev default

01:33:24 10 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:25 [isabelle-nightly-slow] $ hg log --rev . --template {node}

01:33:25 [isabelle-nightly-slow] $ hg log --rev . --template {rev}

01:33:26 [isabelle-nightly-slow] $ hg log --rev 314246c6eeaa5d1ed84d9e2db97dcb1db5099fc0 --template exists\n

01:33:26 exists

01:33:26 [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(314246c6eeaa5d1ed84d9e2db97dcb1db5099fc0)" --encoding UTF-8 --encodingmode replace

01:33:26 [afp] $ hg showconfig paths.default

01:33:26 [afp] $ hg pull --rev default

01:33:27 pulling from https://bitbucket.org/isa-afp/afp-devel/

01:33:27 no changes found

01:33:27 [afp] $ hg update --clean --rev default

01:33:33 7 files updated, 0 files merged, 0 files removed, 0 files unresolved

01:33:33 [afp] $ hg --config extensions.purge= clean --all

01:33:33 [afp] $ hg log --rev . --template {node}

01:33:33 [afp] $ hg log --rev . --template {rev}

01:33:33 [afp] $ hg log --rev 9cafe22c0d2533bb65234961c661305306bec4d2 --template exists\n

01:33:33 exists

01:33:33 [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(9cafe22c0d2533bb65234961c661305306bec4d2)" --encoding UTF-8 --encodingmode replace

01:33:33 No emails were triggered.

01:33:33 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/hudson42335050163823676.sh

01:33:33 + Admin/jenkins/run_build slow

01:33:33 + set -e

01:33:33 + PROFILE=slow

01:33:33 + shift

01:33:33 + bin/isabelle components -a

01:33:41 + bin/isabelle jedit -bf

01:33:41 ### Building graph browser ...

01:33:53 warning: [options] bootstrap class path not set in conjunction with -source 1.4

01:33:53 warning: [options] source value 1.4 is obsolete and will be removed in a future release

01:33:53 warning: [options] target value 1.4 is obsolete and will be removed in a future release

01:33:53 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.

01:33:56 Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.

01:33:56 Note: Recompile with -Xlint:deprecation for details.

01:33:56 4 warnings

01:33:56 ### Building Isabelle/Scala ...

01:35:24 ### Building Isabelle/jEdit ...

01:36:15 + bin/isabelle ci_build_slow

01:36:22

01:36:22 === CONFIGURATION ===

01:36:22

01:36:22 ISABELLE_BUILD_OPTIONS=""

01:36:22

01:36:22 ML_PLATFORM="x86_64-linux"

01:36:22 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"

01:36:22 ML_SYSTEM="polyml-5.6"

01:36:22 ML_OPTIONS="-H 4000 --maxheap 10G"

01:36:22

01:36:22 === BUILD ===

01:36:22

01:36:22 Build started at Wed, 15 Mar 2017 01:36:22 +0100

01:36:22 Isabelle id f435640193b6

01:36:23 Build for AFP id ee8091b2d624

01:36:23

01:36:23 === LOG ===

01:36:23

01:36:29 Session Pure/Pure

01:36:32 Session HOL/HOL (main)

01:36:38 Session AFP/AWN (AFP)

01:36:38 Session AFP/AODV (AFP slow)

01:36:39 Session HOL/HOL-Analysis (main timing)

01:36:41 Session AFP/Ordinary_Differential_Equations (AFP)

01:36:41 Session AFP/HOL-ODE (AFP)

01:36:41 Session AFP/HOL-ODE-Refinement (AFP)

01:36:43 Session AFP/HOL-ODE-Numerics (AFP)

01:36:43 Session AFP/HOL-ODE-Examples (AFP slow)

01:36:43 Session HOL/HOL-Library (main timing)

01:36:45 Session AFP/ConcurrentIMP (AFP)

01:36:45 Session AFP/ConcurrentGC (AFP slow)

01:36:45 Session AFP/Flyspeck-Tame (AFP slow very_slow)

01:36:46 Session HOL/HOL-Word (main timing)

01:36:46 Session AFP/JinjaThreads (AFP slow)

01:36:48 Session AFP/Word_Lib (AFP)

01:36:49 Session AFP/IP_Addresses (AFP)

01:36:49 Session AFP/Simple_Firewall (AFP)

01:36:49 Session AFP/Routing (AFP)

01:36:49 Session AFP/Iptables_Semantics (AFP)

01:36:50 Session AFP/Iptables_Semantics_Examples (AFP slow very_slow)

01:36:51 Building Pure ...

01:37:18 Pure: theory Pure

01:37:19 Pure: theory ML_Bootstrap

01:37:23 Warning: missing document directory

01:37:23 Timing Pure (1 threads, 0.817s elapsed time, 0.816s cpu time, 0.000s GC time, factor 1.00)

01:37:23 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure

01:37:23 Finished Pure (0:00:20 elapsed time, 0:00:18 cpu time, factor 0.92)

01:37:23 Building HOL ...

01:37:24 HOL: theory Code_Generator

01:37:27 HOL: theory HOL

01:37:31 HOL: theory Argo

01:37:31 HOL: theory Orderings

01:37:31 HOL: theory Ctr_Sugar

01:37:33 HOL: theory SAT

01:37:33 HOL: theory Groups

01:37:36 HOL: theory Lattices

01:37:39 HOL: theory Set

01:37:40 HOL: theory Fun

01:37:40 HOL: theory Rings

01:37:40 HOL: theory Typedef

01:37:41 HOL: theory Complete_Lattices

01:37:44 HOL: theory Inductive

01:37:46 HOL: theory Product_Type

01:37:46 HOL: theory Sum_Type

01:37:48 HOL: theory Complete_Partial_Order

01:37:53 HOL: theory Nat

01:37:55 HOL: theory Fields

01:37:55 HOL: theory Meson

01:37:56 HOL: theory ATP

01:37:59 HOL: theory Metis

01:38:01 HOL: theory Finite_Set

01:38:03 HOL: theory Relation

01:38:05 HOL: theory Transitive_Closure

01:38:06 HOL: theory Wellfounded

01:38:07 HOL: theory Fun_Def_Base

01:38:07 HOL: theory Hilbert_Choice

01:38:07 HOL: theory Wfrec

01:38:07 HOL: theory Order_Relation

01:38:08 HOL: theory BNF_Wellorder_Relation

01:38:08 HOL: theory Zorn

01:38:08 HOL: theory BNF_Wellorder_Embedding

01:38:09 HOL: theory BNF_Wellorder_Constructions

01:38:10 HOL: theory BNF_Cardinal_Order_Relation

01:38:11 HOL: theory BNF_Cardinal_Arithmetic

01:38:11 HOL: theory BNF_Def

01:38:13 HOL: theory Basic_BNFs

01:38:13 HOL: theory BNF_Composition

01:38:14 HOL: theory BNF_Fixpoint_Base

01:38:18 HOL: theory BNF_Least_Fixpoint

01:38:20 HOL: theory Basic_BNF_LFPs

01:38:21 HOL: theory Transfer

01:38:22 HOL: theory Num

01:38:26 HOL: theory Power

01:38:29 HOL: theory Groups_Big

01:38:32 HOL: theory Equiv_Relations

01:38:33 HOL: theory Lifting

01:38:34 HOL: theory Lifting_Set

01:38:34 HOL: theory Quotient

01:38:34 HOL: theory Option

01:38:35 HOL: theory Extraction

01:38:35 HOL: theory Partial_Function

01:38:35 HOL: theory Lattices_Big

01:38:36 HOL: theory Fun_Def

01:38:38 HOL: theory Int

01:38:41 HOL: theory Nat_Transfer

01:38:42 HOL: theory Euclidean_Division

01:38:47 HOL: theory Parity

01:38:50 HOL: theory Divides

01:39:00 HOL: theory Code_Numeral

01:39:00 HOL: theory Numeral_Simprocs

01:39:00 HOL: theory Set_Interval

01:39:00 HOL: theory SMT

01:39:01 HOL: theory Semiring_Normalization

01:39:04 HOL: theory Conditionally_Complete_Lattices

01:39:04 HOL: theory Filter

01:39:05 HOL: theory Groebner_Basis

01:39:06 HOL: theory Presburger

01:39:09 HOL: theory Sledgehammer

01:39:12 HOL: theory List

01:39:22 HOL: theory Groups_List

01:39:22 HOL: theory Map

01:39:23 HOL: theory Enum

01:39:23 HOL: theory Random

01:39:27 HOL: theory String

01:39:28 HOL: theory BNF_Greatest_Fixpoint

01:39:28 HOL: theory Typerep

01:39:28 HOL: theory Predicate

01:39:30 HOL: theory Lazy_Sequence

01:39:31 HOL: theory Limited_Sequence

01:39:31 HOL: theory Code_Evaluation

01:39:33 HOL: theory Quickcheck_Random

01:39:36 HOL: theory Quickcheck_Exhaustive

01:39:36 HOL: theory Quickcheck_Narrowing

01:39:36 HOL: theory Random_Pred

01:39:37 HOL: theory Random_Sequence

01:39:41 HOL: theory Record

01:39:41 HOL: theory Predicate_Compile

01:39:43 HOL: theory Nitpick

01:39:50 HOL: theory Main

01:39:52 HOL: theory Archimedean_Field

01:39:52 HOL: theory Topological_Spaces

01:39:52 HOL: theory GCD

01:39:52 HOL: theory Binomial

01:40:03 HOL: theory Rat

01:40:06 HOL: theory Real

01:40:09 HOL: theory Real_Vector_Spaces

01:40:24 HOL: theory Inequalities

01:40:24 HOL: theory Limits

01:40:29 HOL: theory Deriv

01:40:29 HOL: theory Series

01:40:31 HOL: theory NthRoot

01:40:32 HOL: theory Transcendental

01:40:39 HOL: theory Complex

01:40:41 HOL: theory MacLaurin

01:40:42 HOL: theory Complex_Main

01:42:33 Timing HOL (8 threads, 213.970s elapsed time, 670.636s cpu time, 43.256s GC time, factor 3.13)

01:42:33 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL

01:42:33 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf

01:42:33 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf

01:42:33 Finished HOL (0:05:09 elapsed time, 0:14:30 cpu time, factor 2.81)

01:42:36 Building HOL-Library ...

01:42:40 HOL-Library: theory Adhoc_Overloading

01:42:40 HOL-Library: theory Lattice_Syntax

01:42:40 HOL-Library: theory BNF_Axiomatization

01:42:40 HOL-Library: theory AList

01:42:40 HOL-Library: theory Stirling

01:42:40 HOL-Library: theory Bit

01:42:40 HOL-Library: theory BNF_Corec

01:42:40 HOL-Library: theory Bits

01:42:40 HOL-Library: theory Boolean_Algebra

01:42:40 HOL-Library: theory Cancellation

01:42:40 HOL-Library: theory Cardinal_Notations

01:42:41 HOL-Library: theory Char_ord

01:42:41 HOL-Library: theory Code_Abstract_Nat

01:42:41 HOL-Library: theory Code_Binary_Nat

01:42:41 HOL-Library: theory Code_Target_Nat

01:42:41 HOL-Library: theory Code_Char

01:42:41 HOL-Library: theory Code_Prolog

01:42:41 HOL-Library: theory Code_Test

01:42:41 HOL-Library: theory Multiset

01:42:41 HOL-Library: theory Combine_PER

01:42:41 HOL-Library: theory Bits_Bit

01:42:41 HOL-Library: theory Complete_Partial_Order2

01:42:42 HOL-Library: theory Debug

01:42:42 HOL-Library: theory Disjoint_Sets

01:42:42 HOL-Library: theory Dlist

01:42:42 HOL-Library: theory FSet

01:42:43 HOL-Library: theory Fraction_Field

01:42:43 HOL-Library: theory Fun_Lexorder

01:42:43 HOL-Library: theory FuncSet

01:42:43 HOL-Library: theory DAList

01:42:44 HOL-Library: theory Function_Algebras

01:42:44 HOL-Library: theory Code_Target_Int

01:42:44 HOL-Library: theory Function_Division

01:42:44 HOL-Library: theory Code_Target_Numeral

01:42:44 HOL-Library: theory Groups_Big_Fun

01:42:44 HOL-Library: theory IArray

01:42:45 HOL-Library: theory Infinite_Set

01:42:45 HOL-Library: theory LaTeXsugar

01:42:45 HOL-Library: theory Lattice_Constructions

01:42:45 HOL-Library: theory Omega_Words_Fun

01:42:45 HOL-Library: theory Ramsey

01:42:46 HOL-Library: theory ListVector

01:42:46 HOL-Library: theory List_lexord

01:42:46 HOL-Library: theory Mapping

01:42:46 HOL-Library: theory Misc_Numeric

01:42:46 HOL-Library: theory Misc_Typedef

01:42:46 HOL-Library: theory Bit_Representation

01:42:46 HOL-Library: theory Monad_Syntax

01:42:46 HOL-Library: theory More_List

01:42:47 HOL-Library: theory Nat_Bijection

01:42:47 HOL-Library: theory Old_Datatype

01:42:47 HOL-Library: theory Finite_Map

01:42:47 HOL-Library: theory Bits_Int

01:42:47 HOL-Library: theory AList_Mapping

01:42:47 HOL-Library: theory Stream

01:42:48 HOL-Library: theory Old_Recdef

01:42:48 HOL-Library: theory DAList_Multiset

01:42:49 HOL-Library: theory Multiset_Order

01:42:49 HOL-Library: theory Permutation

01:42:49 HOL-Library: theory Permutations

01:42:49 HOL-Library: theory Factorial_Ring

01:42:49 HOL-Library: theory Countable

01:42:49 HOL-Library: theory Option_ord

01:42:49 HOL-Library: theory Bool_List_Representation

01:42:49 HOL-Library: theory Parallel

01:42:49 HOL-Library: theory Perm

01:42:49 HOL-Library: theory Phantom_Type

01:42:50 HOL-Library: theory Predicate_Compile_Alternative_Defs

01:42:50 HOL-Library: theory Predicate_Compile_Quickcheck

01:42:50 HOL-Library: theory Product_Lexorder

01:42:51 HOL-Library: theory Product_Plus

01:42:51 HOL-Library: theory Quotient_Syntax

01:42:51 HOL-Library: theory Cardinality

01:42:51 HOL-Library: theory Quotient_Option

01:42:51 HOL-Library: theory Quotient_Product

01:42:51 HOL-Library: theory Quotient_Set

01:42:51 HOL-Library: theory Product_Order

01:42:51 HOL-Library: theory Quotient_Sum

01:42:51 HOL-Library: theory Quotient_Type

01:42:51 HOL-Library: theory Quotient_List

01:42:51 HOL-Library: theory RBT_Impl

01:42:51 HOL-Library: theory Reflection

01:42:51 HOL-Library: theory Finite_Lattice

01:42:51 HOL-Library: theory Refute

01:42:51 HOL-Library: theory Rewrite

01:42:52 HOL-Library: theory Set_Algebras

01:42:52 HOL-Library: theory Countable_Set

01:42:52 HOL-Library: theory Simps_Case_Conv

01:42:52 HOL-Library: theory Extended

01:42:52 HOL-Library: theory State_Monad

01:42:52 HOL-Library: theory Numeral_Type

01:42:52 HOL-Library: theory Sublist

01:42:52 HOL-Library: theory Countable_Complete_Lattices

01:42:52 HOL-Library: theory Countable_Set_Type

01:42:54 HOL-Library: theory Prefix_Order

01:42:54 HOL-Library: theory Type_Length

01:42:54 HOL-Library: theory Sublist_Order

01:42:54 HOL-Library: theory Polynomial

01:42:54 HOL-Library: theory Saturated

01:42:55 HOL-Library: theory BigO

01:42:55 HOL-Library: theory Code_Real_Approx_By_Float

01:42:56 HOL-Library: theory Diagonal_Subsequence

01:42:56 HOL-Library: theory Discrete

01:42:57 HOL-Library: theory Indicator_Function

01:42:57 HOL-Library: theory Lattice_Algebras

01:42:57 HOL-Library: theory Liminf_Limsup

01:42:57 HOL-Library: theory Log_Nat

01:42:57 HOL-Library: theory Lub_Glb

01:42:57 HOL-Library: theory Multiset_Permutations

01:42:57 HOL-Library: theory Nonpos_Ints

01:42:58 HOL-Library: theory OptionalSugar

01:42:58 HOL-Library: theory Order_Continuity

01:42:58 HOL-Library: theory Periodic_Fun

01:42:58 HOL-Library: theory Quadratic_Discriminant

01:42:58 HOL-Library: theory Sum_of_Squares

01:42:58 HOL-Library: theory Transitive_Closure_Table

01:42:59 HOL-Library: theory Tree

01:42:59 HOL-Library: theory Extended_Nat

01:42:59 HOL-Library: theory While_Combinator

01:43:00 HOL-Library: theory Bourbaki_Witt_Fixpoint

01:43:01 HOL-Library: theory Extended_Real

01:43:01 HOL-Library: theory Linear_Temporal_Logic_on_Streams

01:43:02 HOL-Library: theory Euclidean_Algorithm

01:43:02 HOL-Library: theory Word_Miscellaneous

01:43:03 HOL-Library: theory Word

01:43:03 HOL-Library: theory Preorder

01:43:03 HOL-Library: theory Function_Growth

01:43:04 HOL-Library: theory Tree_Multiset

01:43:05 HOL-Library: theory Fundamental_Theorem_Algebra

01:43:05 HOL-Library: theory Float

01:43:07 HOL-Library: theory Extended_Nonnegative_Real

01:43:11 HOL-Library: theory Old_SMT

01:43:15 HOL-Library: theory Normalized_Fraction

01:43:15 HOL-Library: theory Field_as_Ring

01:43:15 HOL-Library: theory Formal_Power_Series

01:43:17 HOL-Library: theory Polynomial_Factorial

01:43:21 HOL-Library: theory Polynomial_FPS

01:43:22 HOL-Library: theory Library

01:43:51 HOL-Library: theory RBT

01:43:53 HOL-Library: theory RBT_Mapping

01:43:53 HOL-Library: theory RBT_Set

01:46:33 Timing HOL-Library (8 threads, 141.031s elapsed time, 799.088s cpu time, 69.308s GC time, factor 5.67)

01:46:33 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library

01:46:33 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf

01:46:33 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf

01:46:33 Finished HOL-Library (0:03:56 elapsed time, 0:16:58 cpu time, factor 4.31)

01:46:36 Building HOL-Word ...

01:46:40 HOL-Word: theory Bit

01:46:40 HOL-Word: theory Boolean_Algebra

01:46:40 HOL-Word: theory Bits

01:46:40 HOL-Word: theory Misc_Typedef

01:46:40 HOL-Word: theory Misc_Numeric

01:46:40 HOL-Word: theory Phantom_Type

01:46:40 HOL-Word: theory Bit_Representation

01:46:41 HOL-Word: theory Bits_Bit

01:46:41 HOL-Word: theory Word_Miscellaneous

01:46:42 HOL-Word: theory Bits_Int

01:46:42 HOL-Word: theory Cardinality

01:46:44 HOL-Word: theory Numeral_Type

01:46:44 HOL-Word: theory Bool_List_Representation

01:46:45 HOL-Word: theory Type_Length

01:46:45 HOL-Word: theory Word

01:47:11 Timing HOL-Word (8 threads, 12.806s elapsed time, 60.608s cpu time, 1.904s GC time, factor 4.73)

01:47:11 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word

01:47:11 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf

01:47:11 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf

01:47:11 Finished HOL-Word (0:00:35 elapsed time, 0:01:43 cpu time, factor 2.92)

01:47:12 Building AWN ...

01:47:15 AWN: theory Lib

01:47:15 AWN: theory TransitionSystems

01:47:15 AWN: theory AWN

01:47:15 AWN: theory Invariants

01:47:16 AWN: theory OInvariants

01:47:29 AWN: theory AWN_Cterms

01:47:29 AWN: theory OAWN_SOS

01:47:29 AWN: theory AWN_SOS

01:47:34 AWN: theory AWN_Labels

01:47:36 AWN: theory Pnet

01:47:36 AWN: theory Inv_Cterms

01:47:36 AWN: theory AWN_Invariants

01:47:37 AWN: theory Closed

01:47:37 AWN: theory AWN_SOS_Labels

01:47:38 AWN: theory Qmsg

01:47:39 AWN: theory OAWN_Invariants

01:47:39 AWN: theory OPnet

01:47:39 AWN: theory ONode_Lifting

01:47:39 AWN: theory OAWN_SOS_Labels

01:47:40 AWN: theory OPnet_Lifting

01:47:41 AWN: theory OClosed_Lifting

01:47:41 AWN: theory OClosed_Transfer

01:47:41 AWN: theory OAWN_Convert

01:47:41 AWN: theory Qmsg_Lifting

01:47:42 AWN: theory AWN_Main

01:47:43 AWN: theory Toy

01:48:35 Timing AWN (8 threads, 49.193s elapsed time, 247.684s cpu time, 7.044s GC time, factor 5.03)

01:48:35 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN

01:48:35 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf

01:48:35 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf

01:48:35 Finished AWN (0:01:22 elapsed time, 0:05:27 cpu time, factor 3.96)

01:48:35 Building ConcurrentIMP ...

01:48:45 ConcurrentIMP: theory CIMP_pred

01:48:45 ConcurrentIMP: theory CIMP_lang

01:48:57 ConcurrentIMP: theory CIMP_vcg

01:49:00 ConcurrentIMP: theory CIMP

01:49:00 ConcurrentIMP: theory CIMP_one_place_buffer_ex

01:49:00 ConcurrentIMP: theory CIMP_unbounded_buffer_ex

01:49:35 Timing ConcurrentIMP (8 threads, 20.684s elapsed time, 50.508s cpu time, 2.676s GC time, factor 2.44)

01:49:35 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP

01:49:35 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf

01:49:35 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf

01:49:35 Finished ConcurrentIMP (0:00:58 elapsed time, 0:02:13 cpu time, factor 2.27)

01:49:35 Building Word_Lib ...

01:49:38 Word_Lib: theory WordBitwise

01:49:38 Word_Lib: theory Sublist

01:49:40 Word_Lib: theory Prefix_Order

01:49:40 Word_Lib: theory Enumeration

01:49:40 Word_Lib: theory HOL_Lemmas

01:49:40 Word_Lib: theory More_Divides

01:49:40 Word_Lib: theory Hex_Words

01:49:40 Word_Lib: theory Signed_Words

01:49:41 Word_Lib: theory Norm_Words

01:49:41 Word_Lib: theory WordBitwise_Signed

01:49:41 Word_Lib: theory Word_Syntax

01:49:42 Word_Lib: theory Word_Lib

01:49:42 Word_Lib: theory Aligned

01:49:42 Word_Lib: theory Word_Enum

01:49:43 Word_Lib: theory Word_Setup_32

01:49:43 Word_Lib: theory Word_Setup_64

01:49:43 Word_Lib: theory Word_Lemmas

01:49:50 Word_Lib: theory Word_Lemmas_32

01:49:50 Word_Lib: theory Word_Lemmas_64

01:51:04 Timing Word_Lib (8 threads, 69.841s elapsed time, 178.584s cpu time, 3.404s GC time, factor 2.56)

01:51:04 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib

01:51:04 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf

01:51:04 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf

01:51:04 Finished Word_Lib (0:01:28 elapsed time, 0:03:37 cpu time, factor 2.44)

01:51:04 Building IP_Addresses ...

01:51:08 IP_Addresses: theory Cancellation

01:51:08 IP_Addresses: theory Char_ord

01:51:08 IP_Addresses: theory Code_Abstract_Nat

01:51:08 IP_Addresses: theory Infinite_Set

01:51:08 IP_Addresses: theory Code_Target_Int

01:51:08 IP_Addresses: theory Option_ord

01:51:08 IP_Addresses: theory NumberWang_IPv4

01:51:08 IP_Addresses: theory NumberWang_IPv6

01:51:08 IP_Addresses: theory Word_More

01:51:08 IP_Addresses: theory Code_Target_Nat

01:51:08 IP_Addresses: theory Code_Char

01:51:09 IP_Addresses: theory Multiset

01:51:16 IP_Addresses: theory Quicksort

01:51:16 IP_Addresses: theory List_More

01:51:16 IP_Addresses: theory Misc

01:51:45 IP_Addresses: theory Lib_Numbers_toString

01:51:45 IP_Addresses: theory Hs_Compat

01:51:45 IP_Addresses: theory Product_Lexorder

01:51:45 IP_Addresses: theory Word_Next

01:51:45 IP_Addresses: theory WordInterval

01:51:45 IP_Addresses: theory Lib_List_toString

01:51:45 IP_Addresses: theory Lib_Word_toString

01:51:51 IP_Addresses: theory IP_Address

01:51:51 IP_Addresses: theory WordInterval_Sorted

01:51:55 IP_Addresses: theory IPv4

01:51:56 IP_Addresses: theory IPv6

01:51:57 IP_Addresses: theory Prefix_Match

01:51:58 IP_Addresses: theory CIDR_Split

01:53:25 IP_Addresses: theory IP_Address_Parser

01:53:25 IP_Addresses: theory IP_Address_toString

01:57:49 Timing IP_Addresses (8 threads, 347.990s elapsed time, 1029.188s cpu time, 56.432s GC time, factor 2.96)

01:57:49 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses

01:57:49 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf

01:57:49 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf

01:57:49 Finished IP_Addresses (0:06:44 elapsed time, 0:19:40 cpu time, factor 2.92)

01:57:50 Building Simple_Firewall ...

01:57:56 Simple_Firewall: theory GroupF

01:57:56 Simple_Firewall: theory Option_Helpers

01:57:56 Simple_Firewall: theory List_Product_More

01:57:56 Simple_Firewall: theory Firewall_Common_Decision_State

01:57:56 Simple_Firewall: theory IP_Partition_Preliminaries

01:57:56 Simple_Firewall: theory Iface

01:57:56 Simple_Firewall: theory Lib_Enum_toString

01:57:56 Simple_Firewall: theory IP_Addr_WordInterval_toString

01:57:57 Simple_Firewall: theory L4_Protocol

01:58:02 Simple_Firewall: theory Simple_Packet

01:58:02 Simple_Firewall: theory Primitives_toString

01:58:05 Simple_Firewall: theory SimpleFw_Syntax

01:58:08 Simple_Firewall: theory SimpleFw_Semantics

01:58:11 Simple_Firewall: theory Generic_SimpleFw

01:58:11 Simple_Firewall: theory Shadowed

01:58:11 Simple_Firewall: theory Service_Matrix

01:58:51 Timing Simple_Firewall (8 threads, 25.384s elapsed time, 99.184s cpu time, 3.900s GC time, factor 3.91)

01:58:51 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall

01:58:51 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf

01:58:51 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf

01:58:51 Finished Simple_Firewall (0:01:00 elapsed time, 0:03:01 cpu time, factor 2.97)

01:58:51 Building Routing ...

01:59:04 Routing: theory Adhoc_Overloading

01:59:04 Routing: theory Monad_Syntax

01:59:04 Routing: theory Linorder_Helper

01:59:04 Routing: theory Prefix_Match_toString

01:59:06 Routing: theory Routing_Table

01:59:10 Routing: theory IpRoute_Parser

01:59:11 Routing: theory Linux_Router

01:59:37 Timing Routing (8 threads, 13.256s elapsed time, 49.188s cpu time, 1.076s GC time, factor 3.71)

01:59:37 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing

01:59:37 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf

01:59:37 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf

01:59:37 Finished Routing (0:00:45 elapsed time, 0:01:43 cpu time, factor 2.27)

01:59:37 Building Iptables_Semantics ...

01:59:45 Iptables_Semantics: theory Negation_Type

01:59:45 Iptables_Semantics: theory List_Misc

01:59:45 Iptables_Semantics: theory More_Bits_Int

01:59:45 Iptables_Semantics: theory LaTeXsugar

01:59:47 Iptables_Semantics: theory WordInterval_Lists

01:59:48 Iptables_Semantics: theory Bits_Integer

02:00:14 Iptables_Semantics: theory Code_Target_Bits_Int

02:00:25 Iptables_Semantics: theory Datatype_Selectors

02:00:25 Iptables_Semantics: theory Conntrack_State

02:00:25 Iptables_Semantics: theory Negation_Type_DNF

02:00:25 Iptables_Semantics: theory Remdups_Rev

02:00:25 Iptables_Semantics: theory Repeat_Stabilize

02:00:25 Iptables_Semantics: theory Ternary

02:00:25 Iptables_Semantics: theory L4_Protocol_Flags

02:00:25 Iptables_Semantics: theory SimpleFw_toString

02:00:26 Iptables_Semantics: theory IpAddresses

02:00:26 Iptables_Semantics: theory Firewall_Common

02:00:26 Iptables_Semantics: theory Word_Upto

02:00:27 Iptables_Semantics: theory Ports

02:00:27 Iptables_Semantics: theory Tagged_Packet

02:00:30 Iptables_Semantics: theory Common_Primitive_Syntax

02:00:44 Iptables_Semantics: theory Matching_Ternary

02:00:44 Iptables_Semantics: theory Semantics_Goto

02:00:44 Iptables_Semantics: theory Semantics

02:00:46 Iptables_Semantics: theory Matching

02:00:46 Iptables_Semantics: theory Semantics_Stateful

02:00:46 Iptables_Semantics: theory Ruleset_Update

02:00:46 Iptables_Semantics: theory Call_Return_Unfolding

02:00:47 Iptables_Semantics: theory Semantics_Ternary

02:00:48 Iptables_Semantics: theory Unknown_Match_Tacs

02:00:49 Iptables_Semantics: theory Matching_Embeddings

02:00:49 Iptables_Semantics: theory Fixed_Action

02:00:49 Iptables_Semantics: theory Optimizing

02:00:49 Iptables_Semantics: theory Common_Primitive_Matcher_Generic

02:00:50 Iptables_Semantics: theory Normalized_Matches

02:00:51 Iptables_Semantics: theory Negation_Type_Matching

02:00:53 Iptables_Semantics: theory Primitive_Normalization

02:00:55 Iptables_Semantics: theory Common_Primitive_Matcher

02:00:57 Iptables_Semantics: theory MatchExpr_Fold

02:00:57 Iptables_Semantics: theory Ipassmt

02:01:02 Iptables_Semantics: theory Routing_IpAssmt

02:01:56 Iptables_Semantics: theory Common_Primitive_Lemmas

02:01:56 Iptables_Semantics: theory Example_Semantics

02:01:56 Iptables_Semantics: theory Common_Primitive_toString

02:01:56 Iptables_Semantics: theory Conntrack_State_Transform

02:01:57 Iptables_Semantics: theory Interfaces_Normalize

02:01:57 Iptables_Semantics: theory No_Spoof

02:01:57 Iptables_Semantics: theory IpAddresses_Normalize

02:01:57 Iptables_Semantics: theory Ports_Normalize

02:01:57 Iptables_Semantics: theory Protocols_Normalize

02:02:05 Iptables_Semantics: theory Output_Interface_Replace

02:02:09 Iptables_Semantics: theory Interface_Replace

02:02:18 Iptables_Semantics: theory Transform

02:02:23 Iptables_Semantics: theory Primitive_Abstract

02:02:25 Iptables_Semantics: theory SimpleFw_Compliance

02:02:33 Iptables_Semantics: theory Code_Interface

02:02:33 Iptables_Semantics: theory Semantics_Embeddings

02:02:34 Iptables_Semantics: theory Iptables_Semantics

02:02:34 Iptables_Semantics: theory No_Spoof_Embeddings

02:02:44 Iptables_Semantics: theory Parser

02:02:44 Iptables_Semantics: theory Documentation

02:02:45 Iptables_Semantics: theory Code_haskell

02:04:26 Timing Iptables_Semantics (8 threads, 203.167s elapsed time, 775.688s cpu time, 58.264s GC time, factor 3.82)

02:04:26 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics

02:04:26 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf

02:04:26 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf

02:04:26 Finished Iptables_Semantics (0:04:47 elapsed time, 0:17:10 cpu time, factor 3.58)

02:04:28 Building HOL-Analysis ...

02:04:36 HOL-Analysis: theory Disjoint_Sets

02:04:36 HOL-Analysis: theory Infinite_Set

02:04:36 HOL-Analysis: theory FuncSet

02:04:36 HOL-Analysis: theory Cancellation

02:04:36 HOL-Analysis: theory Nat_Bijection

02:04:36 HOL-Analysis: theory Old_Datatype

02:04:36 HOL-Analysis: theory Phantom_Type

02:04:36 HOL-Analysis: theory Product_Plus

02:04:37 HOL-Analysis: theory Product_Order

02:04:37 HOL-Analysis: theory Set_Algebras

02:04:37 HOL-Analysis: theory L2_Norm

02:04:37 HOL-Analysis: theory Discrete

02:04:38 HOL-Analysis: theory Indicator_Function

02:04:38 HOL-Analysis: theory Multiset

02:04:38 HOL-Analysis: theory Inner_Product

02:04:38 HOL-Analysis: theory Liminf_Limsup

02:04:38 HOL-Analysis: theory Nonpos_Ints

02:04:38 HOL-Analysis: theory Cardinality

02:04:38 HOL-Analysis: theory Operator_Norm

02:04:39 HOL-Analysis: theory Periodic_Fun

02:04:39 HOL-Analysis: theory Poly_Roots

02:04:39 HOL-Analysis: theory Sum_of_Squares

02:04:39 HOL-Analysis: theory Countable

02:04:40 HOL-Analysis: theory Numeral_Type

02:04:40 HOL-Analysis: theory Product_Vector

02:04:41 HOL-Analysis: theory Euclidean_Space

02:04:41 HOL-Analysis: theory Countable_Set

02:04:42 HOL-Analysis: theory Countable_Complete_Lattices

02:04:42 HOL-Analysis: theory Continuum_Not_Denumerable

02:04:43 HOL-Analysis: theory Norm_Arith

02:04:43 HOL-Analysis: theory Finite_Cartesian_Product

02:04:43 HOL-Analysis: theory Linear_Algebra

02:04:45 HOL-Analysis: theory Permutations

02:04:45 HOL-Analysis: theory Factorial_Ring

02:04:46 HOL-Analysis: theory Order_Continuity

02:04:47 HOL-Analysis: theory Extended_Nat

02:04:48 HOL-Analysis: theory Topology_Euclidean_Space

02:04:49 HOL-Analysis: theory Extended_Real

02:04:55 HOL-Analysis: theory Extended_Nonnegative_Real

02:04:55 HOL-Analysis: theory Summation_Tests

02:04:57 HOL-Analysis: theory Euclidean_Algorithm

02:04:58 HOL-Analysis: theory Sigma_Algebra

02:05:02 HOL-Analysis: theory Convex_Euclidean_Space

02:05:02 HOL-Analysis: theory Bounded_Linear_Function

02:05:02 HOL-Analysis: theory Extended_Real_Limits

02:05:02 HOL-Analysis: theory Tagged_Division

02:05:02 HOL-Analysis: theory Uniform_Limit

02:05:03 HOL-Analysis: theory Measurable

02:05:04 HOL-Analysis: theory Measure_Space

02:05:08 HOL-Analysis: theory Caratheodory

02:05:09 HOL-Analysis: theory Primes

02:05:10 HOL-Analysis: theory Continuous_Extension

02:05:11 HOL-Analysis: theory Path_Connected

02:05:17 HOL-Analysis: theory Homeomorphism

02:05:18 HOL-Analysis: theory Brouwer_Fixpoint

02:05:21 HOL-Analysis: theory Derivative

02:05:25 HOL-Analysis: theory Cartesian_Euclidean_Space

02:05:25 HOL-Analysis: theory Weierstrass_Theorems

02:05:29 HOL-Analysis: theory Determinants

02:05:29 HOL-Analysis: theory Fashoda_Theorem

02:05:29 HOL-Analysis: theory Ordered_Euclidean_Space

02:05:29 HOL-Analysis: theory Polytope

02:05:37 HOL-Analysis: theory Arcwise_Connected

02:05:37 HOL-Analysis: theory Borel_Space

02:05:41 HOL-Analysis: theory Nonnegative_Lebesgue_Integration

02:05:41 HOL-Analysis: theory Regularity

02:05:45 HOL-Analysis: theory Binary_Product_Measure

02:05:46 HOL-Analysis: theory Embed_Measure

02:05:46 HOL-Analysis: theory Finite_Product_Measure

02:05:48 HOL-Analysis: theory Bochner_Integration

02:05:48 HOL-Analysis: theory Function_Topology

02:05:52 HOL-Analysis: theory Complete_Measure

02:05:52 HOL-Analysis: theory Radon_Nikodym

02:05:53 HOL-Analysis: theory Set_Integral

02:05:53 HOL-Analysis: theory Lebesgue_Measure

02:05:56 HOL-Analysis: theory Henstock_Kurzweil_Integration

02:06:02 HOL-Analysis: theory Bounded_Continuous_Function

02:06:02 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration

02:06:02 HOL-Analysis: theory Integral_Test

02:06:04 HOL-Analysis: theory Complex_Analysis_Basics

02:06:04 HOL-Analysis: theory Interval_Integral

02:06:06 HOL-Analysis: theory Lebesgue_Integral_Substitution

02:06:07 HOL-Analysis: theory Complex_Transcendental

02:06:11 HOL-Analysis: theory Generalised_Binomial_Theorem

02:06:11 HOL-Analysis: theory Harmonic_Numbers

02:06:11 HOL-Analysis: theory Cauchy_Integral_Theorem

02:06:12 HOL-Analysis: theory Further_Topology

02:06:17 HOL-Analysis: theory Jordan_Curve

02:06:18 HOL-Analysis: theory Conformal_Mappings

02:06:18 HOL-Analysis: theory Winding_Numbers

02:06:18 HOL-Analysis: theory Gamma_Function

02:06:21 HOL-Analysis: theory Great_Picard

02:06:26 HOL-Analysis: theory Analysis

02:14:11 Timing HOL-Analysis (8 threads, 458.087s elapsed time, 2185.388s cpu time, 182.352s GC time, factor 4.77)

02:14:11 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis

02:14:11 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/document.pdf

02:14:11 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/outline.pdf

02:14:11 Finished HOL-Analysis (0:09:42 elapsed time, 0:39:57 cpu time, factor 4.12)

02:14:13 Building Ordinary_Differential_Equations ...

02:14:20 Ordinary_Differential_Equations: theory Code_Abstract_Nat

02:14:20 Ordinary_Differential_Equations: theory Code_Target_Int

02:14:20 Ordinary_Differential_Equations: theory Dense_Linear_Order

02:14:20 Ordinary_Differential_Equations: theory Diagonal_Subsequence

02:14:20 Ordinary_Differential_Equations: theory Lattice_Algebras

02:14:20 Ordinary_Differential_Equations: theory Log_Nat

02:14:20 Ordinary_Differential_Equations: theory Code_Target_Nat

02:14:21 Ordinary_Differential_Equations: theory Code_Target_Numeral

02:14:29 Ordinary_Differential_Equations: theory Float

02:14:32 Ordinary_Differential_Equations: theory Approximation

02:15:35 Ordinary_Differential_Equations: theory Bounded_Linear_Operator

02:15:35 Ordinary_Differential_Equations: theory ODE_Auxiliarities

02:15:41 Ordinary_Differential_Equations: theory Initial_Value_Problem

02:15:41 Ordinary_Differential_Equations: theory MVT_Ex

02:15:41 Ordinary_Differential_Equations: theory Multivariate_Taylor

02:15:52 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations

02:15:52 Ordinary_Differential_Equations FAILED

02:15:52 (see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.6_x86_64-linux/log/Ordinary_Differential_Equations)

02:15:52 *** ist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/f

02:15:52 *** onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/t

02:15:52 *** ype1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/p

02:15:52 *** ublic/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/

02:15:52 *** amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon

02:15:52 *** ts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c

02:15:52 *** mmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pf

02:15:52 *** b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr

02:15:52 *** /share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/

02:15:52 *** texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/

02:15:52 *** texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-di

02:15:52 *** st/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fon

02:15:52 *** ts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type

02:15:52 *** 1/public/amsfonts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi

02:15:52 *** c/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsf

02:15:52 *** onts/cm/cmti12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/c

02:15:52 *** m/cmtt10.pfb>

02:15:52 *** Output written on root.pdf (44 pages, 279865 bytes).

02:15:52 *** Transcript written on root.log.

02:15:52 *** This is BibTeX, Version 0.99d (TeX Live 2015/dev/Debian)

02:15:52 *** The top-level auxiliary file: root.aux

02:15:52 *** The style file: abbrv.bst

02:15:52 *** I found no \citation commands---while reading file root.aux

02:15:52 *** Database file #1: root.bib

02:15:52 *** (There was 1 error message)

02:15:52 *** Document preparation failure in directory '/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/outline'

02:15:52 ***

02:15:52 *** Failed to build document "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/outline.pdf"

02:15:52 *** Type unification failed: Clash of types "_ \<Rightarrow> _" and "_ \<Rightarrow>\<^sub>C _"

02:15:52 ***

02:15:52 *** Type error in application: incompatible operand type

02:15:52 ***

02:15:52 *** Operator: op = (P x) :: real \<Rightarrow>\<^sub>C 'a \<Rightarrow> bool

02:15:52 *** Operand: ext_cont (P_inner x) tmin tmax :: real \<Rightarrow> 'a

02:15:52 ***

02:15:52 *** Coercion Inference:

02:15:52 ***

02:15:52 *** Local coercion insertion on the operand failed:

02:15:52 *** No coercion known for type constructors: "fun" and "bcontfun"

02:15:52 *** At command "definition" (line 1383 of "~~/afp/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy")

02:15:52 HOL-ODE CANCELLED

02:15:52 HOL-ODE-Refinement CANCELLED

02:15:52 HOL-ODE-Numerics CANCELLED

02:15:52 Running Flyspeck-Tame ...

02:16:01 Flyspeck-Tame: theory Trie

02:16:04 Flyspeck-Tame: theory Tries

02:16:25 Flyspeck-Tame: theory ListAux

02:16:25 Flyspeck-Tame: theory IArray_Syntax

02:16:25 Flyspeck-Tame: theory Quasi_Order

02:16:25 Flyspeck-Tame: theory RTranCl

02:16:25 Flyspeck-Tame: theory Arch

02:16:25 Flyspeck-Tame: theory PlaneGraphIso

02:16:25 Flyspeck-Tame: theory Worklist

02:16:26 Flyspeck-Tame: theory ListSum

02:16:26 Flyspeck-Tame: theory Maps

02:16:26 Flyspeck-Tame: theory Rotation

02:16:26 Flyspeck-Tame: theory Graph

02:16:30 Flyspeck-Tame: theory Enumerator

02:16:30 Flyspeck-Tame: theory FaceDivision

02:16:30 Flyspeck-Tame: theory GraphProps

02:16:30 Flyspeck-Tame: theory Tame

02:16:30 Flyspeck-Tame: theory Plane

02:16:30 Flyspeck-Tame: theory EnumeratorProps

02:16:31 Flyspeck-Tame: theory TameProps

02:16:31 Flyspeck-Tame: theory Plane1

02:16:31 Flyspeck-Tame: theory FaceDivisionProps

02:16:31 Flyspeck-Tame: theory Generator

02:16:32 Flyspeck-Tame: theory TameEnum

02:16:34 Flyspeck-Tame: theory Invariants

02:16:37 Flyspeck-Tame: theory PlaneProps

02:16:39 Flyspeck-Tame: theory Plane1Props

02:16:40 Flyspeck-Tame: theory ScoreProps

02:16:42 Flyspeck-Tame: theory LowerBound

02:16:43 Flyspeck-Tame: theory GeneratorProps

02:16:44 Flyspeck-Tame: theory TameEnumProps

02:16:47 Flyspeck-Tame: theory ArchCompAux

02:16:48 Flyspeck-Tame: theory ArchCompProps

02:16:49 Flyspeck-Tame: theory ArchComp

02:16:49 Flyspeck-Tame: theory Completeness

09:51:58 Timing Flyspeck-Tame (8 threads, 27347.558s elapsed time, 40298.568s cpu time, 654.220s GC time, factor 1.47)

09:51:58 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame

09:51:58 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf

09:51:58 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf

09:51:58 Finished Flyspeck-Tame (7:36:05 elapsed time, 11:12:00 cpu time, factor 1.47)

09:51:59 Running Iptables_Semantics_Examples ...

09:52:14 Iptables_Semantics_Examples: theory Analyze_Ringofsaturn_com

09:52:14 Iptables_Semantics_Examples: theory Analyze_SQRL_Shorewall

09:52:14 Iptables_Semantics_Examples: theory Contrived_Example

09:52:14 Iptables_Semantics_Examples: theory Analyze_TUM_Net_Firewall

09:52:14 Iptables_Semantics_Examples: theory IP_Address_Space_Examples_All_Small

09:52:14 Iptables_Semantics_Examples: theory Parser_Test

09:52:14 Iptables_Semantics_Examples: theory Analyze_medium_sized_company

09:52:14 Iptables_Semantics_Examples: theory Analyze_topos_generated

09:52:24 Iptables_Semantics_Examples: theory SNS_IAS_Eduroam_Spoofing

09:52:24 Iptables_Semantics_Examples: theory SQRL_2015_nospoof

09:52:24 Iptables_Semantics_Examples: theory TUM_Spoofing_new3

09:52:24 Iptables_Semantics_Examples: theory Parser6

09:52:25 Iptables_Semantics_Examples: theory Parser6_Test

09:52:33 Iptables_Semantics_Examples: theory Ports_Fail

09:52:34 Iptables_Semantics_Examples: theory Small_Examples

09:52:34 Iptables_Semantics_Examples: theory iptables_Ln_tuned_parsed

09:52:35 Iptables_Semantics_Examples: theory Analyze_Synology_Diskstation

09:56:19 Iptables_Semantics_Examples: theory IP_Address_Space_Examples_All_Large

11:16:54 Iptables_Semantics_Examples: theory TUM_Simple_FW

12:48:40 Timing Iptables_Semantics_Examples (8 threads, 10581.773s elapsed time, 66303.436s cpu time, 9430.176s GC time, factor 6.27)

12:48:40 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples

12:48:40 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf

12:48:40 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf

12:48:40 Finished Iptables_Semantics_Examples (2:56:40 elapsed time, 18:25:32 cpu time, factor 6.26)

12:48:41 Running AODV ...

12:48:46 AODV: theory Aodv_Basic

12:48:48 AODV: theory A_Norreqid

12:48:48 AODV: theory Aodv_Message

12:48:48 AODV: theory B_Fwdrreps

12:48:48 AODV: theory E_All_ABCD

12:48:48 AODV: theory C_Gtobcast

12:48:48 AODV: theory D_Fwdrreqs

12:48:48 AODV: theory Aodv_Data

12:48:48 AODV: theory A_Aodv_Data

12:48:48 AODV: theory A_Aodv_Message

12:48:48 AODV: theory B_Aodv_Data

12:48:48 AODV: theory B_Aodv_Message

12:48:48 AODV: theory C_Aodv_Data

12:48:48 AODV: theory C_Aodv_Message

12:48:50 AODV: theory C_Fresher

12:48:50 AODV: theory Fresher

12:48:50 AODV: theory A_Fresher

12:48:50 AODV: theory D_Aodv_Data

12:48:50 AODV: theory B_Fresher

12:48:50 AODV: theory D_Aodv_Message

12:48:50 AODV: theory E_Aodv_Data

12:48:50 AODV: theory E_Aodv_Message

12:48:51 AODV: theory A_Aodv

12:48:51 AODV: theory Aodv

12:48:51 AODV: theory B_Aodv

12:48:51 AODV: theory C_Aodv

12:48:52 AODV: theory E_Fresher

12:48:52 AODV: theory D_Fresher

12:48:52 AODV: theory D_Aodv

12:48:52 AODV: theory E_Aodv

12:50:04 AODV: theory A_Aodv_Predicates

12:50:05 AODV: theory A_Loop_Freedom

12:50:05 AODV: theory A_Quality_Increases

12:50:06 AODV: theory A_Seq_Invariants

12:50:07 AODV: theory A_OAodv

12:50:07 AODV: theory A_Global_Invariants

12:50:09 AODV: theory A_Aodv_Loop_Freedom

12:50:11 AODV: theory C_Aodv_Predicates

12:50:11 AODV: theory C_Loop_Freedom

12:50:12 AODV: theory C_Quality_Increases

12:50:12 AODV: theory C_Seq_Invariants

12:50:13 AODV: theory C_OAodv

12:50:13 AODV: theory C_Global_Invariants

12:50:14 AODV: theory C_Aodv_Loop_Freedom

12:50:26 AODV: theory Aodv_Predicates

12:50:26 AODV: theory Loop_Freedom

12:50:27 AODV: theory Quality_Increases

12:50:27 AODV: theory Seq_Invariants

12:50:28 AODV: theory OAodv

12:50:28 AODV: theory Global_Invariants

12:50:29 AODV: theory Aodv_Loop_Freedom

12:50:32 AODV: theory E_Aodv_Predicates

12:50:32 AODV: theory E_OAodv

12:50:32 AODV: theory E_Loop_Freedom

12:50:32 AODV: theory E_Quality_Increases

12:50:32 AODV: theory E_Seq_Invariants

12:50:33 AODV: theory B_Aodv_Predicates

12:50:33 AODV: theory B_OAodv

12:50:33 AODV: theory E_Global_Invariants

12:50:33 AODV: theory B_Loop_Freedom

12:50:34 AODV: theory B_Quality_Increases

12:50:34 AODV: theory B_Seq_Invariants

12:50:34 AODV: theory E_Aodv_Loop_Freedom

12:50:35 AODV: theory B_Global_Invariants

12:50:36 AODV: theory B_Aodv_Loop_Freedom

12:50:42 AODV: theory D_Aodv_Predicates

12:50:42 AODV: theory D_OAodv

12:50:43 AODV: theory D_Loop_Freedom

12:50:43 AODV: theory D_Quality_Increases

12:50:43 AODV: theory D_Seq_Invariants

12:50:44 AODV: theory D_Global_Invariants

12:50:45 AODV: theory D_Aodv_Loop_Freedom

12:50:51 AODV: theory All

15:36:54 Timing AODV (8 threads, 10076.447s elapsed time, 51886.352s cpu time, 4377.372s GC time, factor 5.15)

15:36:54 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV

15:36:54 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/document.pdf

15:36:54 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/outline.pdf

15:36:54 Finished AODV (2:48:12 elapsed time, 14:25:08 cpu time, factor 5.14)

15:36:54 Running ConcurrentGC ...

15:37:04 ConcurrentGC: theory Model

15:37:23 ConcurrentGC: theory Tactics

15:37:31 ConcurrentGC: theory Proofs_basis

15:37:35 ConcurrentGC: theory TSO

15:37:51 ConcurrentGC: theory Handshakes

15:40:29 ConcurrentGC: theory MarkObject

15:43:15 ConcurrentGC: theory StrongTricolour

15:44:21 ConcurrentGC: theory Proofs

15:44:23 ConcurrentGC: theory Concrete_heap

15:44:24 ConcurrentGC: theory Concrete

17:53:48 Timing ConcurrentGC (8 threads, 8197.317s elapsed time, 27043.712s cpu time, 2387.428s GC time, factor 3.30)

17:53:48 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC

17:53:48 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf

17:53:48 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf

17:53:48 Finished ConcurrentGC (2:16:52 elapsed time, 7:30:58 cpu time, factor 3.29)

17:53:48 Running JinjaThreads ...

17:53:57 JinjaThreads: theory Adhoc_Overloading

17:53:57 JinjaThreads: theory Lattice_Syntax

17:53:57 JinjaThreads: theory AList

17:53:57 JinjaThreads: theory Char_ord

17:53:57 JinjaThreads: theory Cancellation

17:53:57 JinjaThreads: theory Code_Abstract_Nat

17:53:57 JinjaThreads: theory Dlist

17:53:57 JinjaThreads: theory FingerTree

17:53:57 JinjaThreads: theory Complete_Partial_Order2

17:53:57 JinjaThreads: theory Foldi

17:53:57 JinjaThreads: theory Code_Target_Nat

17:53:58 JinjaThreads: theory Code_Char

17:53:58 JinjaThreads: theory Code_Target_Int

17:53:58 JinjaThreads: theory ICF_Tools

17:53:58 JinjaThreads: theory Infinite_Set

17:53:58 JinjaThreads: theory Code_Target_Numeral

17:53:58 JinjaThreads: theory More_Bits_Int

17:53:58 JinjaThreads: theory Multiset

17:53:58 JinjaThreads: theory Monad_Syntax

17:53:59 JinjaThreads: theory Omega_Words_Fun

17:53:59 JinjaThreads: theory Nat_Bijection

17:54:00 JinjaThreads: theory Old_Datatype

17:54:00 JinjaThreads: theory Option_ord

17:54:00 JinjaThreads: theory Ord_Code_Preproc

17:54:00 JinjaThreads: theory Trie

17:54:00 JinjaThreads: theory Locale_Code

17:54:01 JinjaThreads: theory FinFun

17:54:01 JinjaThreads: theory Predicate_Compile_Alternative_Defs

17:54:01 JinjaThreads: theory Prio_List

17:54:01 JinjaThreads: theory RBT_Impl

17:54:02 JinjaThreads: theory Bits_Integer

17:54:02 JinjaThreads: theory Countable

17:54:03 JinjaThreads: theory Record_Intf

17:54:03 JinjaThreads: theory Refine_Chapter

17:54:03 JinjaThreads: theory Refine_Util

17:54:04 JinjaThreads: theory Set_Monad

17:54:04 JinjaThreads: theory Set_without_equal

17:54:05 JinjaThreads: theory Simps_Case_Conv

17:54:05 JinjaThreads: theory Anti_Unification

17:54:05 JinjaThreads: theory Attr_Comb

17:54:05 JinjaThreads: theory Autoref_Data

17:54:05 JinjaThreads: theory Mk_Term_Antiquot

17:54:05 JinjaThreads: theory Mpat_Antiquot

17:54:05 JinjaThreads: theory Named_Sorted_Thms

17:54:05 JinjaThreads: theory Countable_Set

17:54:05 JinjaThreads: theory Tagged_Solver

17:54:05 JinjaThreads: theory Select_Solve

17:54:05 JinjaThreads: theory Indep_Vars

17:54:05 JinjaThreads: theory Mk_Record_Simp

17:54:05 JinjaThreads: theory Sublist

17:54:05 JinjaThreads: theory Transitive_Closure_Table

17:54:05 JinjaThreads: theory While_Combinator

17:54:06 JinjaThreads: theory Countable_Complete_Lattices

17:54:07 JinjaThreads: theory Auxiliary

17:54:07 JinjaThreads: theory DatRef

17:54:07 JinjaThreads: theory BinomialHeap

17:54:07 JinjaThreads: theory Quicksort

17:54:08 JinjaThreads: theory List_More

17:54:09 JinjaThreads: theory Misc

17:54:09 JinjaThreads: theory SkewBinomialHeap

17:54:11 JinjaThreads: theory Order_Continuity

17:54:11 JinjaThreads: theory Word_Misc

17:54:12 JinjaThreads: theory Extended_Nat

17:54:15 JinjaThreads: theory Coinductive_Nat

17:54:17 JinjaThreads: theory Coinductive_List

17:54:19 JinjaThreads: theory SetIterator

17:54:19 JinjaThreads: theory Digraph_Basic

17:54:19 JinjaThreads: theory Sorted_List_Operations

17:54:20 JinjaThreads: theory Code_Target_Bits_Int

17:54:20 JinjaThreads: theory Code_Target_ICF

17:54:21 JinjaThreads: theory Refine_Lib

17:54:21 JinjaThreads: theory Uint32

17:54:22 JinjaThreads: theory SetIteratorOperations

17:54:22 JinjaThreads: theory Autoref_Phases

17:54:22 JinjaThreads: theory Autoref_Tagging

17:54:22 JinjaThreads: theory Refine_Mono_Prover

17:54:22 JinjaThreads: theory Relators

17:54:23 JinjaThreads: theory Param_Tool

17:54:23 JinjaThreads: theory HashCode

17:54:23 JinjaThreads: theory Param_HOL

17:54:25 JinjaThreads: theory Parametricity

17:54:25 JinjaThreads: theory Assoc_List

17:54:25 JinjaThreads: theory Autoref_Id_Ops

17:54:25 JinjaThreads: theory Dlist_add

17:54:25 JinjaThreads: theory Proper_Iterator

17:54:25 JinjaThreads: theory SetIteratorGA

17:54:26 JinjaThreads: theory Diff_Array

17:54:26 JinjaThreads: theory Trie_Impl

17:54:26 JinjaThreads: theory It_to_It

17:54:27 JinjaThreads: theory Autoref_Fix_Rel

17:54:27 JinjaThreads: theory Trie2

17:54:27 JinjaThreads: theory Autoref_Translate

17:54:27 JinjaThreads: theory Autoref_Relator_Interface

17:54:28 JinjaThreads: theory Autoref_Gen_Algo

17:54:28 JinjaThreads: theory Autoref_Tool

17:54:29 JinjaThreads: theory Lazy_LList

17:54:29 JinjaThreads: theory Autoref_Bindings_HOL

17:54:29 JinjaThreads: theory TLList

17:54:34 JinjaThreads: theory Lazy_TLList

17:54:35 JinjaThreads: theory Automatic_Refinement

17:54:35 JinjaThreads: theory Idx_Iterator

17:54:35 JinjaThreads: theory Refine_Misc

17:54:36 JinjaThreads: theory RefineG_Domain

17:54:36 JinjaThreads: theory RefineG_Transfer

17:54:37 JinjaThreads: theory RefineG_Assert

17:54:37 JinjaThreads: theory RefineG_Recursion

17:54:38 JinjaThreads: theory Refine_Basic

17:54:38 JinjaThreads: theory RefineG_While

17:54:39 JinjaThreads: theory Refine_Det

17:54:43 JinjaThreads: theory Refine_Heuristics

17:54:43 JinjaThreads: theory Refine_Leof

17:54:43 JinjaThreads: theory Refine_Pfun

17:54:43 JinjaThreads: theory Refine_While

17:54:46 JinjaThreads: theory Refine_Transfer

17:54:46 JinjaThreads: theory Autoref_Monadic

17:54:46 JinjaThreads: theory Refine_Automation

17:54:46 JinjaThreads: theory Refine_Foreach

17:54:50 JinjaThreads: theory Refine_Monadic

17:54:51 JinjaThreads: theory Gen_Iterator

17:54:51 JinjaThreads: theory Intf_Map

17:54:51 JinjaThreads: theory Intf_Set

17:54:52 JinjaThreads: theory Iterator

17:54:53 JinjaThreads: theory Array_Iterator

17:54:53 JinjaThreads: theory ICF_Spec_Base

17:54:53 JinjaThreads: theory AnnotatedListSpec

17:54:53 JinjaThreads: theory ListSpec

17:54:53 JinjaThreads: theory MapSpec

17:54:55 JinjaThreads: theory PrioSpec

17:54:56 JinjaThreads: theory PrioUniqueSpec

17:54:57 JinjaThreads: theory ListGA

17:54:57 JinjaThreads: theory FTAnnotatedListImpl

17:54:57 JinjaThreads: theory BinoPrioImpl

17:54:58 JinjaThreads: theory Fifo

17:54:58 JinjaThreads: theory PrioByAnnotatedList

17:54:59 JinjaThreads: theory SkewPrioImpl

17:54:59 JinjaThreads: theory PrioUniqueByAnnotatedList

17:54:59 JinjaThreads: theory RBT

17:54:59 JinjaThreads: theory SetSpec

17:55:00 JinjaThreads: theory RBT_add

17:55:02 JinjaThreads: theory FTPrioImpl

17:55:02 JinjaThreads: theory FTPrioUniqueImpl

17:55:05 JinjaThreads: theory Algos

17:55:05 JinjaThreads: theory SetIndex

17:55:05 JinjaThreads: theory SetIteratorCollectionsGA

17:55:06 JinjaThreads: theory MapGA

17:55:06 JinjaThreads: theory SetGA

17:55:10 JinjaThreads: theory ArrayMapImpl

17:55:10 JinjaThreads: theory ListMapImpl

17:55:10 JinjaThreads: theory ListMapImpl_Invar

17:55:10 JinjaThreads: theory TrieMapImpl

17:55:10 JinjaThreads: theory RBTMapImpl

17:55:12 JinjaThreads: theory ArrayHashMap_Impl

17:55:14 JinjaThreads: theory ListSetImpl

17:55:14 JinjaThreads: theory ListSetImpl_Invar

17:55:14 JinjaThreads: theory ListSetImpl_NotDist

17:55:14 JinjaThreads: theory ListSetImpl_Sorted

17:55:15 JinjaThreads: theory SetByMap

17:55:16 JinjaThreads: theory HashMap_Impl

17:55:17 JinjaThreads: theory ArrayHashMap

17:55:18 JinjaThreads: theory ArraySetImpl

17:55:18 JinjaThreads: theory TrieSetImpl

17:55:18 JinjaThreads: theory RBTSetImpl

17:55:18 JinjaThreads: theory HashMap

17:55:21 JinjaThreads: theory ArrayHashSet

17:55:22 JinjaThreads: theory HashSet

17:55:22 JinjaThreads: theory MapStdImpl

17:55:27 JinjaThreads: theory SetStdImpl

17:55:32 JinjaThreads: theory ICF_Impl

17:55:39 JinjaThreads: theory ICF_Refine_Monadic

17:55:40 JinjaThreads: theory ICF_Autoref

17:55:46 JinjaThreads: theory Collections

17:55:46 JinjaThreads: theory CollectionsV1

17:55:58 JinjaThreads: theory JT_ICF

17:55:58 JinjaThreads: theory Basic_Main

17:56:41 JinjaThreads: theory ListIndex

17:56:41 JinjaThreads: theory Prefix_Order

17:56:41 JinjaThreads: theory FWState

17:56:41 JinjaThreads: theory Orders

17:56:41 JinjaThreads: theory Mapping

17:56:41 JinjaThreads: theory LTS

17:56:41 JinjaThreads: theory Type

17:56:41 JinjaThreads: theory Semilat

17:56:41 JinjaThreads: theory Err

17:56:43 JinjaThreads: theory AList_Mapping

17:56:43 JinjaThreads: theory Listn

17:56:43 JinjaThreads: theory Opt

17:56:44 JinjaThreads: theory Product

17:56:44 JinjaThreads: theory Semilattices

17:56:45 JinjaThreads: theory Typing_Framework

17:56:45 JinjaThreads: theory SemilatAlg

17:56:45 JinjaThreads: theory Decl

17:56:45 JinjaThreads: theory Kildall

17:56:45 JinjaThreads: theory LBVSpec

17:56:46 JinjaThreads: theory LBVComplete

17:56:46 JinjaThreads: theory Bisimulation

17:56:47 JinjaThreads: theory LBVCorrect

17:56:47 JinjaThreads: theory Typing_Framework_err

17:56:48 JinjaThreads: theory Abstract_BV

17:56:49 JinjaThreads: theory TypeRel

17:56:56 JinjaThreads: theory TypeRelRefine

17:56:56 JinjaThreads: theory Value

17:57:02 JinjaThreads: theory Exceptions

17:57:02 JinjaThreads: theory Heap

17:57:03 JinjaThreads: theory SystemClasses

17:57:05 JinjaThreads: theory MM

17:57:05 JinjaThreads: theory State

17:57:17 JinjaThreads: theory FWCondAction

17:57:17 JinjaThreads: theory FWInterrupt

17:57:17 JinjaThreads: theory FWLock

17:57:17 JinjaThreads: theory FWThread

17:57:17 JinjaThreads: theory FWWait

17:57:17 JinjaThreads: theory Observable_Events

17:57:26 JinjaThreads: theory FWLocking

17:57:33 JinjaThreads: theory FWLockingThread

17:57:33 JinjaThreads: theory FWWellform

17:57:35 JinjaThreads: theory FWLifting

17:57:35 JinjaThreads: theory FWSemantics

17:57:38 JinjaThreads: theory JMM_Spec

17:57:38 JinjaThreads: theory JVMState

17:57:38 JinjaThreads: theory StartConfig

17:57:39 JinjaThreads: theory FWLiftingSem

17:57:39 JinjaThreads: theory FWProgressAux

17:57:40 JinjaThreads: theory Conform

17:57:40 JinjaThreads: theory State_Refinement

17:57:41 JinjaThreads: theory FWDeadlock

17:57:41 JinjaThreads: theory FWLTS

17:57:44 JinjaThreads: theory ConformThreaded

17:57:44 JinjaThreads: theory FWProgress

17:57:44 JinjaThreads: theory ExternalCall

17:57:45 JinjaThreads: theory SC

17:57:45 JinjaThreads: theory SC_Collections

17:57:51 JinjaThreads: theory JMM_DRF

17:57:51 JinjaThreads: theory SC_Legal

17:57:52 JinjaThreads: theory FWBisimulation

17:57:52 JinjaThreads: theory FWInitFinLift

17:57:52 JinjaThreads: theory Non_Speculative

17:57:54 JinjaThreads: theory Scheduler

17:57:56 JinjaThreads: theory HB_Completion

17:57:56 JinjaThreads: theory SC_Completion

17:58:23 JinjaThreads: theory ExternalCall_Execute

17:58:23 JinjaThreads: theory WellForm

17:58:26 JinjaThreads: theory BinOp

17:58:27 JinjaThreads: theory ExternalCallWF

17:58:27 JinjaThreads: theory JMM_Heap

17:58:30 JinjaThreads: theory SemiType

17:58:32 JinjaThreads: theory Random_Scheduler

17:58:33 JinjaThreads: theory JMM_Type

17:58:34 JinjaThreads: theory JMM_Type2

17:58:38 JinjaThreads: theory JVM_SemiType

17:58:39 JinjaThreads: theory Round_Robin

17:58:41 JinjaThreads: theory JMM_Framework

17:58:55 JinjaThreads: theory SC_Schedulers

17:58:55 JinjaThreads: theory Expr

17:58:58 JinjaThreads: theory JVMInstructions

17:58:59 JinjaThreads: theory PCompiler

17:59:02 JinjaThreads: theory PCompilerRefine

17:59:23 JinjaThreads: theory JVMExceptions

17:59:24 JinjaThreads: theory Effect

17:59:26 JinjaThreads: theory JVMHeap

17:59:29 JinjaThreads: theory CallExpr

17:59:30 JinjaThreads: theory DefAss

17:59:31 JinjaThreads: theory WWellForm

17:59:31 JinjaThreads: theory JHeap

17:59:31 JinjaThreads: theory WellType

17:59:36 JinjaThreads: theory JVMExecInstr

17:59:36 JinjaThreads: theory ToString

17:59:37 JinjaThreads: theory J1State

17:59:39 JinjaThreads: theory Annotate

17:59:41 JinjaThreads: theory Compiler1

17:59:41 JinjaThreads: theory JVMExec

17:59:43 JinjaThreads: theory Compiler2

17:59:46 JinjaThreads: theory JVMDefensive

17:59:47 JinjaThreads: theory JVMExec_Execute

17:59:49 JinjaThreads: theory J1Heap

17:59:54 JinjaThreads: theory JVMThreaded

17:59:56 JinjaThreads: theory J1WellType

17:59:58 JinjaThreads: theory SmallStep

18:00:01 JinjaThreads: theory Compiler

18:00:03 JinjaThreads: theory Exception_Tables

18:00:03 JinjaThreads: theory J1WellForm

18:00:05 JinjaThreads: theory JWellForm

18:00:06 JinjaThreads: theory JMM_Typesafe

18:00:06 JinjaThreads: theory WellTypeRT

18:00:08 JinjaThreads: theory JJ1WellForm

18:00:08 JinjaThreads: theory Preprocessor

18:00:25 JinjaThreads: theory JMM_JVM

18:00:29 JinjaThreads: theory JVM_Main

18:03:52 JinjaThreads: theory JMM_Common

18:03:57 JinjaThreads: theory BVSpec

18:03:58 JinjaThreads: theory EffectMono

18:03:58 JinjaThreads: theory TF_JVM

18:03:58 JinjaThreads: theory BVConform

18:03:59 JinjaThreads: theory TypeComp

18:03:59 JinjaThreads: theory JMM_Typesafe2

18:04:02 JinjaThreads: theory BVExec

18:04:03 JinjaThreads: theory LBVJVM

18:04:04 JinjaThreads: theory BVSpecTypeSafe

18:04:12 JinjaThreads: theory BVNoTypeError

18:04:14 JinjaThreads: theory BCVExec

18:04:15 JinjaThreads: theory JVMExec_Execute2

18:04:16 JinjaThreads: theory BVProgressThreaded

18:04:16 JinjaThreads: theory JVMTau

18:04:32 JinjaThreads: theory FWBisimDeadlock

18:04:32 JinjaThreads: theory FWBisimLift

18:04:32 JinjaThreads: theory J1

18:04:39 JinjaThreads: theory Execs

18:04:51 JinjaThreads: theory DefAssPreservation

18:04:51 JinjaThreads: theory Threaded

18:04:52 JinjaThreads: theory Progress

18:04:54 JinjaThreads: theory Common_Main

18:04:56 JinjaThreads: theory TypeSafe

18:05:03 JinjaThreads: theory J1Deadlock

18:05:10 JinjaThreads: theory J0

18:05:10 JinjaThreads: theory JMM_J

18:05:11 JinjaThreads: theory ProgressThreaded

18:05:11 JinjaThreads: theory J_Execute

18:05:25 JinjaThreads: theory J1JVMBisim

18:05:32 JinjaThreads: theory JVMDeadlocked

18:05:32 JinjaThreads: theory DRF_JVM

18:05:32 JinjaThreads: theory JVM_Execute

18:05:32 JinjaThreads: theory JVM_Execute2

18:05:35 JinjaThreads: theory DRF_J

18:05:37 JinjaThreads: theory Deadlocked

18:05:44 JinjaThreads: theory J_Main

18:05:57 JinjaThreads: theory J0Bisim

18:05:57 JinjaThreads: theory J0J1Bisim

18:06:02 JinjaThreads: theory BV_Main

18:06:15 JinjaThreads: theory Code_Generation

18:06:40 JinjaThreads: theory ApprenticeChallenge

18:06:40 JinjaThreads: theory BufferExample

18:06:49 JinjaThreads: theory Correctness1

18:06:49 JinjaThreads: theory Correctness1Threaded

18:06:57 JinjaThreads: theory Java2Jinja

18:11:50 JinjaThreads: theory Examples_Main

18:13:04 JinjaThreads: theory JMM_J_Typesafe

18:13:04 JinjaThreads: theory JMM_JVM_Typesafe

18:13:56 JinjaThreads: theory Execute_Main

18:14:55 JinjaThreads: theory J1JVM

18:14:55 JinjaThreads: theory JVMJ1

18:16:27 JinjaThreads: theory Correctness2

18:19:21 JinjaThreads: theory Correctness

18:30:29 JinjaThreads: theory Compiler_Main

18:30:30 JinjaThreads: theory JMM_Compiler

18:30:31 JinjaThreads: theory SC_Interp

18:35:09 JinjaThreads: theory JMM_Interp

18:35:13 JinjaThreads: theory JMM_Compiler_Type2

18:35:16 JinjaThreads: theory JMM

18:35:18 JinjaThreads: theory MM_Main

18:35:28 JinjaThreads: theory JinjaThreads

18:39:25 Timing JinjaThreads (8 threads, 2675.114s elapsed time, 12520.316s cpu time, 3616.192s GC time, factor 4.68)

18:39:25 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads

18:39:25 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf

18:39:25 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf

18:39:25 Finished JinjaThreads (0:45:31 elapsed time, 3:30:47 cpu time, factor 4.63)

18:39:26 HOL-ODE-Examples CANCELLED

18:39:26 Unfinished session(s): HOL-ODE, HOL-ODE-Examples, HOL-ODE-Numerics, HOL-ODE-Refinement, Ordinary_Differential_Equations

18:39:26

18:39:26 === TIMING ===

18:39:26

18:39:26 Group slow: 16:23:22 elapsed time, 55:04:26 cpu time, factor 3.36

18:39:26 Group AFP: 16:42:10 elapsed time, 56:01:30 cpu time, factor 3.35

18:39:26 Group main: 0:19:23 elapsed time, 1:13:10 cpu time, factor 3.77

18:39:26 Group timing: 0:14:14 elapsed time, 0:58:40 cpu time, factor 4.12

18:39:26 Group very_slow: 10:32:46 elapsed time, 29:37:32 cpu time, factor 2.81

18:39:26 Overall: 17:03:03 elapsed time, 57:14:59 cpu time, factor 3.36

18:39:26

18:39:26 === FAILED SESSIONS ===

18:39:26

18:39:26 Session HOL-ODE-Refinement: CANCELLED

18:39:26 Session Ordinary_Differential_Equations: FAILED 2

18:39:26 Session HOL-ODE-Examples: CANCELLED

18:39:26 Session HOL-ODE-Numerics: CANCELLED

18:39:26 Session HOL-ODE: CANCELLED

18:39:26 Build step 'Execute shell' marked build as failure

18:39:27 Archiving artifacts

18:39:32 Started calculate disk usage of build

18:39:32 Finished Calculation of disk usage of build in 0 seconds

18:39:40 Started calculate disk usage of workspace

18:39:55 Finished Calculation of disk usage of workspace in 15 second

18:39:55 No emails were triggered.

18:39:55 Finished: FAILURE