Skip to content
Aborted

Console Output

01:33:10 Started by an SCM change

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

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

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

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

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

01:33:11 searching for changes

01:33:11 no changes found

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

01:33:11 15 files updated, 0 files merged, 0 files removed, 0 files unresolved

01:33:11 [isabelle-nightly-slow] $ hg --config extensions.purge= clean --all

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

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

01:33:12 [isabelle-nightly-slow] $ hg log --rev b46fe5138cb008e16ffd03e1d59d34dc45968365 --template exists\n

01:33:12 exists

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

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

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

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

01:33:13 no changes found

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

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

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

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

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

01:33:13 [afp] $ hg log --rev 901f6bfc80844443e3f48a912fb1ed7ff7cd6d31 --template exists\n

01:33:13 exists

01:33:13 [afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg><added>{file_adds|stringify|xmlescape}</added><deleted>{file_dels|stringify|xmlescape}</deleted><files>{files|stringify|xmlescape}</files><parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(901f6bfc80844443e3f48a912fb1ed7ff7cd6d31)" --encoding UTF-8 --encodingmode replace

01:33:13 No emails were triggered.

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

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

01:33:13 + set -e

01:33:13 + PROFILE=slow

01:33:13 + shift

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

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

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

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

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

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

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

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

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

01:33:15 4 warnings

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

01:34:25 ### Building Isabelle/jEdit ...

01:34:54 + bin/isabelle ci_build_slow

01:35:00

01:35:00 === CONFIGURATION ===

01:35:00

01:35:00 ISABELLE_BUILD_OPTIONS=""

01:35:00

01:35:00 ML_PLATFORM="x86_64-linux"

01:35:00 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7-20170217/x86_64-linux"

01:35:00 ML_SYSTEM="polyml-5.7"

01:35:00 ML_OPTIONS="-H 4000 --maxheap 10G"

01:35:00

01:35:00 === BUILD ===

01:35:00

01:35:00 Build started at Wed, 22 Feb 2017 01:35:00 +0100

01:35:00 Isabelle id 2cf841ff23be

01:35:00 Build for AFP id f9dd72c30e1c

01:35:00

01:35:00 === LOG ===

01:35:00

01:35:01 Session Pure/Pure

01:35:02 Session HOL/HOL (main)

01:35:03 Session AFP/AWN (AFP)

01:35:03 Session AFP/AODV (AFP slow)

01:35:03 Session HOL/HOL-Analysis (main timing)

01:35:03 Session AFP/Ordinary_Differential_Equations (AFP)

01:35:04 Session AFP/HOL-ODE (AFP)

01:35:04 Session AFP/HOL-ODE-Refinement (AFP)

01:35:04 Session AFP/HOL-ODE-Numerics (AFP)

01:35:04 Session AFP/HOL-ODE-Examples (AFP slow)

01:35:04 Session HOL/HOL-Library (main timing)

01:35:05 Session AFP/ConcurrentIMP (AFP)

01:35:05 Session AFP/ConcurrentGC (AFP slow)

01:35:05 Session AFP/Flyspeck-Tame (AFP slow very_slow)

01:35:05 Session HOL/HOL-Word (main timing)

01:35:05 Session AFP/JinjaThreads (AFP slow)

01:35:06 Session AFP/Word_Lib (AFP)

01:35:06 Session AFP/IP_Addresses (AFP)

01:35:06 Session AFP/Simple_Firewall (AFP)

01:35:06 Session AFP/Routing (AFP)

01:35:06 Session AFP/Iptables_Semantics (AFP)

01:35:07 Session AFP/Iptables_Semantics_Examples (AFP slow very_slow)

01:35:07 Building Pure ...

01:35:24 Pure: theory Pure

01:35:25 Pure: theory ML_Bootstrap

01:35:28 Warning: missing document directory

01:35:28 Timing Pure (1 threads, 0.807s elapsed time, 0.808s cpu time, 0.000s GC time, factor 1.00)

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

01:35:28 Finished Pure (0:00:20 elapsed time, 0:00:19 cpu time, factor 0.99)

01:35:28 Building HOL ...

01:35:29 HOL: theory Code_Generator

01:35:33 HOL: theory HOL

01:35:37 HOL: theory Argo

01:35:37 HOL: theory Ctr_Sugar

01:35:37 HOL: theory Orderings

01:35:39 HOL: theory SAT

01:35:40 HOL: theory Groups

01:35:43 HOL: theory Lattices

01:35:46 HOL: theory Set

01:35:47 HOL: theory Fun

01:35:47 HOL: theory Typedef

01:35:47 HOL: theory Rings

01:35:48 HOL: theory Complete_Lattices

01:35:52 HOL: theory Inductive

01:35:54 HOL: theory Product_Type

01:35:54 HOL: theory Sum_Type

01:35:56 HOL: theory Complete_Partial_Order

01:36:01 HOL: theory Nat

01:36:03 HOL: theory Fields

01:36:03 HOL: theory Meson

01:36:04 HOL: theory ATP

01:36:07 HOL: theory Metis

01:36:10 HOL: theory Finite_Set

01:36:12 HOL: theory Relation

01:36:14 HOL: theory Transitive_Closure

01:36:16 HOL: theory Wellfounded

01:36:17 HOL: theory Fun_Def_Base

01:36:17 HOL: theory Hilbert_Choice

01:36:17 HOL: theory Wfrec

01:36:17 HOL: theory Order_Relation

01:36:17 HOL: theory BNF_Wellorder_Relation

01:36:18 HOL: theory Zorn

01:36:18 HOL: theory BNF_Wellorder_Embedding

01:36:18 HOL: theory BNF_Wellorder_Constructions

01:36:19 HOL: theory BNF_Cardinal_Order_Relation

01:36:21 HOL: theory BNF_Cardinal_Arithmetic

01:36:22 HOL: theory BNF_Def

01:36:24 HOL: theory BNF_Composition

01:36:24 HOL: theory Basic_BNFs

01:36:25 HOL: theory BNF_Fixpoint_Base

01:36:29 HOL: theory BNF_Least_Fixpoint

01:36:32 HOL: theory Basic_BNF_LFPs

01:36:32 HOL: theory Transfer

01:36:34 HOL: theory Num

01:36:38 HOL: theory Power

01:36:41 HOL: theory Groups_Big

01:36:45 HOL: theory Equiv_Relations

01:36:46 HOL: theory Lifting

01:36:47 HOL: theory Lifting_Set

01:36:47 HOL: theory Option

01:36:47 HOL: theory Quotient

01:36:49 HOL: theory Extraction

01:36:49 HOL: theory Partial_Function

01:36:49 HOL: theory Lattices_Big

01:36:50 HOL: theory Fun_Def

01:36:52 HOL: theory Int

01:36:56 HOL: theory Nat_Transfer

01:36:57 HOL: theory Euclidean_Division

01:37:03 HOL: theory Parity

01:37:06 HOL: theory Divides

01:37:17 HOL: theory Code_Numeral

01:37:17 HOL: theory SMT

01:37:17 HOL: theory Numeral_Simprocs

01:37:17 HOL: theory Set_Interval

01:37:19 HOL: theory Semiring_Normalization

01:37:22 HOL: theory Conditionally_Complete_Lattices

01:37:22 HOL: theory Filter

01:37:22 HOL: theory Groebner_Basis

01:37:23 HOL: theory Presburger

01:37:28 HOL: theory Sledgehammer

01:37:31 HOL: theory List

01:37:43 HOL: theory Groups_List

01:37:43 HOL: theory Map

01:37:44 HOL: theory Enum

01:37:44 HOL: theory Random

01:37:48 HOL: theory String

01:37:50 HOL: theory BNF_Greatest_Fixpoint

01:37:50 HOL: theory Predicate

01:37:50 HOL: theory Typerep

01:37:52 HOL: theory Lazy_Sequence

01:37:53 HOL: theory Limited_Sequence

01:37:54 HOL: theory Code_Evaluation

01:37:56 HOL: theory Quickcheck_Random

01:37:58 HOL: theory Quickcheck_Exhaustive

01:37:58 HOL: theory Quickcheck_Narrowing

01:37:58 HOL: theory Random_Pred

01:37:59 HOL: theory Random_Sequence

01:38:04 HOL: theory Record

01:38:04 HOL: theory Predicate_Compile

01:38:07 HOL: theory Nitpick

01:38:14 HOL: theory Main

01:38:16 HOL: theory Archimedean_Field

01:38:16 HOL: theory Topological_Spaces

01:38:16 HOL: theory Binomial

01:38:16 HOL: theory GCD

01:38:31 HOL: theory Rat

01:38:34 HOL: theory Real

01:38:37 HOL: theory Real_Vector_Spaces

01:38:54 HOL: theory Inequalities

01:38:54 HOL: theory Limits

01:38:59 HOL: theory Deriv

01:38:59 HOL: theory Series

01:39:02 HOL: theory NthRoot

01:39:04 HOL: theory Transcendental

01:39:15 HOL: theory Complex

01:39:18 HOL: theory MacLaurin

01:39:23 HOL: theory Complex_Main

01:41:02 Timing HOL (8 threads, 246.241s elapsed time, 800.684s cpu time, 80.976s GC time, factor 3.25)

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

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

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

01:41:02 Finished HOL (0:05:33 elapsed time, 0:16:10 cpu time, factor 2.91)

01:41:05 Building HOL-Library ...

01:41:11 HOL-Library: theory Adhoc_Overloading

01:41:11 HOL-Library: theory Lattice_Syntax

01:41:11 HOL-Library: theory AList

01:41:11 HOL-Library: theory BNF_Corec

01:41:11 HOL-Library: theory Bits

01:41:11 HOL-Library: theory Bit

01:41:11 HOL-Library: theory BNF_Axiomatization

01:41:11 HOL-Library: theory Stirling

01:41:11 HOL-Library: theory Boolean_Algebra

01:41:11 HOL-Library: theory Cancellation

01:41:11 HOL-Library: theory Cardinal_Notations

01:41:11 HOL-Library: theory Char_ord

01:41:11 HOL-Library: theory Code_Abstract_Nat

01:41:12 HOL-Library: theory Code_Binary_Nat

01:41:12 HOL-Library: theory Code_Target_Nat

01:41:12 HOL-Library: theory Code_Char

01:41:12 HOL-Library: theory Code_Prolog

01:41:12 HOL-Library: theory Code_Test

01:41:12 HOL-Library: theory Bits_Bit

01:41:12 HOL-Library: theory Combine_PER

01:41:12 HOL-Library: theory Complete_Partial_Order2

01:41:12 HOL-Library: theory Multiset

01:41:12 HOL-Library: theory Debug

01:41:12 HOL-Library: theory Disjoint_Sets

01:41:13 HOL-Library: theory Dlist

01:41:13 HOL-Library: theory FSet

01:41:13 HOL-Library: theory Fraction_Field

01:41:14 HOL-Library: theory Fun_Lexorder

01:41:14 HOL-Library: theory FuncSet

01:41:14 HOL-Library: theory DAList

01:41:14 HOL-Library: theory Function_Algebras

01:41:15 HOL-Library: theory Function_Division

01:41:15 HOL-Library: theory Code_Target_Int

01:41:15 HOL-Library: theory Groups_Big_Fun

01:41:15 HOL-Library: theory Code_Target_Numeral

01:41:15 HOL-Library: theory IArray

01:41:15 HOL-Library: theory Infinite_Set

01:41:15 HOL-Library: theory LaTeXsugar

01:41:16 HOL-Library: theory Lattice_Constructions

01:41:16 HOL-Library: theory Omega_Words_Fun

01:41:16 HOL-Library: theory ListVector

01:41:17 HOL-Library: theory List_lexord

01:41:17 HOL-Library: theory Mapping

01:41:17 HOL-Library: theory Misc_Numeric

01:41:17 HOL-Library: theory Misc_Typedef

01:41:17 HOL-Library: theory Bit_Representation

01:41:17 HOL-Library: theory Monad_Syntax

01:41:17 HOL-Library: theory More_List

01:41:18 HOL-Library: theory Finite_Map

01:41:18 HOL-Library: theory Nat_Bijection

01:41:18 HOL-Library: theory Bits_Int

01:41:18 HOL-Library: theory Old_Datatype

01:41:18 HOL-Library: theory AList_Mapping

01:41:19 HOL-Library: theory Old_Recdef

01:41:19 HOL-Library: theory Stream

01:41:20 HOL-Library: theory Countable

01:41:20 HOL-Library: theory Option_ord

01:41:20 HOL-Library: theory Parallel

01:41:20 HOL-Library: theory DAList_Multiset

01:41:20 HOL-Library: theory Multiset_Order

01:41:20 HOL-Library: theory Permutation

01:41:21 HOL-Library: theory Permutations

01:41:21 HOL-Library: theory Factorial_Ring

01:41:21 HOL-Library: theory Bool_List_Representation

01:41:21 HOL-Library: theory Perm

01:41:21 HOL-Library: theory Phantom_Type

01:41:21 HOL-Library: theory Predicate_Compile_Alternative_Defs

01:41:22 HOL-Library: theory Predicate_Compile_Quickcheck

01:41:22 HOL-Library: theory Product_Lexorder

01:41:22 HOL-Library: theory Product_Plus

01:41:22 HOL-Library: theory Countable_Set

01:41:22 HOL-Library: theory Quotient_Syntax

01:41:22 HOL-Library: theory Quotient_Type

01:41:22 HOL-Library: theory Quotient_Option

01:41:22 HOL-Library: theory Product_Order

01:41:22 HOL-Library: theory Cardinality

01:41:22 HOL-Library: theory Quotient_Product

01:41:23 HOL-Library: theory Quotient_Set

01:41:23 HOL-Library: theory Quotient_Sum

01:41:23 HOL-Library: theory RBT_Impl

01:41:23 HOL-Library: theory Ramsey

01:41:23 HOL-Library: theory Quotient_List

01:41:23 HOL-Library: theory Reflection

01:41:23 HOL-Library: theory Finite_Lattice

01:41:23 HOL-Library: theory Refute

01:41:23 HOL-Library: theory Countable_Complete_Lattices

01:41:23 HOL-Library: theory Countable_Set_Type

01:41:23 HOL-Library: theory Rewrite

01:41:24 HOL-Library: theory Set_Algebras

01:41:24 HOL-Library: theory Simps_Case_Conv

01:41:24 HOL-Library: theory FinFun

01:41:24 HOL-Library: theory Numeral_Type

01:41:24 HOL-Library: theory Extended

01:41:26 HOL-Library: theory Type_Length

01:41:26 HOL-Library: theory Saturated

01:41:26 HOL-Library: theory State_Monad

01:41:27 HOL-Library: theory Sublist

01:41:27 HOL-Library: theory Polynomial

01:41:27 HOL-Library: theory BigO

01:41:27 HOL-Library: theory Code_Real_Approx_By_Float

01:41:27 HOL-Library: theory Diagonal_Subsequence

01:41:28 HOL-Library: theory Discrete

01:41:28 HOL-Library: theory Indicator_Function

01:41:28 HOL-Library: theory Lattice_Algebras

01:41:28 HOL-Library: theory Prefix_Order

01:41:28 HOL-Library: theory Sublist_Order

01:41:28 HOL-Library: theory Liminf_Limsup

01:41:28 HOL-Library: theory Log_Nat

01:41:28 HOL-Library: theory Lub_Glb

01:41:29 HOL-Library: theory Multiset_Permutations

01:41:29 HOL-Library: theory Nonpos_Ints

01:41:29 HOL-Library: theory OptionalSugar

01:41:29 HOL-Library: theory Order_Continuity

01:41:29 HOL-Library: theory Periodic_Fun

01:41:30 HOL-Library: theory Quadratic_Discriminant

01:41:30 HOL-Library: theory Sum_of_Squares

01:41:30 HOL-Library: theory Transitive_Closure_Table

01:41:30 HOL-Library: theory Tree

01:41:30 HOL-Library: theory Extended_Nat

01:41:31 HOL-Library: theory While_Combinator

01:41:32 HOL-Library: theory Bourbaki_Witt_Fixpoint

01:41:32 HOL-Library: theory Extended_Real

01:41:32 HOL-Library: theory Linear_Temporal_Logic_on_Streams

01:41:34 HOL-Library: theory Word_Miscellaneous

01:41:35 HOL-Library: theory Euclidean_Algorithm

01:41:35 HOL-Library: theory Word

01:41:35 HOL-Library: theory Preorder

01:41:35 HOL-Library: theory Function_Growth

01:41:36 HOL-Library: theory Tree_Multiset

01:41:37 HOL-Library: theory Float

01:41:38 HOL-Library: theory Fundamental_Theorem_Algebra

01:41:39 HOL-Library: theory Extended_Nonnegative_Real

01:41:44 HOL-Library: theory Old_SMT

01:41:48 HOL-Library: theory Normalized_Fraction

01:41:48 HOL-Library: theory Field_as_Ring

01:41:48 HOL-Library: theory Formal_Power_Series

01:41:51 HOL-Library: theory Polynomial_Factorial

01:41:56 HOL-Library: theory Polynomial_FPS

01:41:57 HOL-Library: theory Library

01:42:44 HOL-Library: theory RBT

01:42:45 HOL-Library: theory RBT_Mapping

01:42:45 HOL-Library: theory RBT_Set

01:45:18 Timing HOL-Library (8 threads, 163.087s elapsed time, 908.136s cpu time, 75.440s GC time, factor 5.57)

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

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

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

01:45:18 Finished HOL-Library (0:04:11 elapsed time, 0:18:05 cpu time, factor 4.32)

01:45:21 Building HOL-Word ...

01:45:25 HOL-Word: theory Bit

01:45:25 HOL-Word: theory Phantom_Type

01:45:25 HOL-Word: theory Boolean_Algebra

01:45:25 HOL-Word: theory Misc_Typedef

01:45:25 HOL-Word: theory Misc_Numeric

01:45:25 HOL-Word: theory Bits

01:45:25 HOL-Word: theory Bit_Representation

01:45:26 HOL-Word: theory Bits_Bit

01:45:26 HOL-Word: theory Word_Miscellaneous

01:45:26 HOL-Word: theory Bits_Int

01:45:27 HOL-Word: theory Cardinality

01:45:29 HOL-Word: theory Numeral_Type

01:45:29 HOL-Word: theory Bool_List_Representation

01:45:30 HOL-Word: theory Type_Length

01:45:30 HOL-Word: theory Word

01:45:55 Timing HOL-Word (8 threads, 13.609s elapsed time, 62.628s cpu time, 1.992s GC time, factor 4.60)

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

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

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

01:45:55 Finished HOL-Word (0:00:34 elapsed time, 0:01:41 cpu time, factor 2.95)

01:45:56 Building AWN ...

01:45:59 AWN: theory Lib

01:45:59 AWN: theory TransitionSystems

01:45:59 AWN: theory AWN

01:46:00 AWN: theory Invariants

01:46:01 AWN: theory OInvariants

01:46:16 AWN: theory AWN_Cterms

01:46:17 AWN: theory AWN_SOS

01:46:17 AWN: theory OAWN_SOS

01:46:20 AWN: theory AWN_Labels

01:46:23 AWN: theory Inv_Cterms

01:46:23 AWN: theory AWN_Invariants

01:46:23 AWN: theory Pnet

01:46:24 AWN: theory AWN_SOS_Labels

01:46:25 AWN: theory Closed

01:46:25 AWN: theory Qmsg

01:46:28 AWN: theory OAWN_Invariants

01:46:28 AWN: theory ONode_Lifting

01:46:28 AWN: theory OPnet

01:46:28 AWN: theory OAWN_SOS_Labels

01:46:28 AWN: theory OPnet_Lifting

01:46:29 AWN: theory OClosed_Lifting

01:46:29 AWN: theory OClosed_Transfer

01:46:30 AWN: theory OAWN_Convert

01:46:30 AWN: theory Qmsg_Lifting

01:46:31 AWN: theory AWN_Main

01:46:31 AWN: theory Toy

01:48:00 Timing AWN (8 threads, 54.871s elapsed time, 270.076s cpu time, 9.524s GC time, factor 4.92)

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

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

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

01:48:00 Finished AWN (0:02:03 elapsed time, 0:06:07 cpu time, factor 2.96)

01:48:00 Building ConcurrentIMP ...

01:48:13 ConcurrentIMP: theory CIMP_pred

01:48:13 ConcurrentIMP: theory CIMP_lang

01:48:26 ConcurrentIMP: theory CIMP_vcg

01:48:29 ConcurrentIMP: theory CIMP

01:48:29 ConcurrentIMP: theory CIMP_one_place_buffer_ex

01:48:29 ConcurrentIMP: theory CIMP_unbounded_buffer_ex

01:49:00 Timing ConcurrentIMP (8 threads, 22.715s elapsed time, 54.476s cpu time, 2.848s GC time, factor 2.40)

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

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

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

01:49:00 Finished ConcurrentIMP (0:00:59 elapsed time, 0:01:59 cpu time, factor 2.01)

01:49:00 Building Word_Lib ...

01:49:05 Word_Lib: theory Sublist

01:49:05 Word_Lib: theory WordBitwise

01:49:07 Word_Lib: theory Prefix_Order

01:49:07 Word_Lib: theory HOL_Lemmas

01:49:07 Word_Lib: theory Enumeration

01:49:07 Word_Lib: theory More_Divides

01:49:07 Word_Lib: theory Hex_Words

01:49:07 Word_Lib: theory Signed_Words

01:49:07 Word_Lib: theory Norm_Words

01:49:07 Word_Lib: theory WordBitwise_Signed

01:49:08 Word_Lib: theory Word_Syntax

01:49:08 Word_Lib: theory Word_Lib

01:49:09 Word_Lib: theory Aligned

01:49:09 Word_Lib: theory Word_Enum

01:49:10 Word_Lib: theory Word_Setup_32

01:49:10 Word_Lib: theory Word_Setup_64

01:49:10 Word_Lib: theory Word_Lemmas

01:49:18 Word_Lib: theory Word_Lemmas_32

01:49:18 Word_Lib: theory Word_Lemmas_64

01:50:38 Timing Word_Lib (8 threads, 78.549s elapsed time, 192.104s cpu time, 4.840s GC time, factor 2.45)

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

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

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

01:50:38 Finished Word_Lib (0:01:37 elapsed time, 0:03:45 cpu time, factor 2.32)

01:50:38 Building IP_Addresses ...

01:50:43 IP_Addresses: theory Cancellation

01:50:43 IP_Addresses: theory NumberWang_IPv6

01:50:43 IP_Addresses: theory Code_Target_Int

01:50:43 IP_Addresses: theory NumberWang_IPv4

01:50:43 IP_Addresses: theory Option_ord

01:50:43 IP_Addresses: theory Char_ord

01:50:43 IP_Addresses: theory Infinite_Set

01:50:43 IP_Addresses: theory Code_Abstract_Nat

01:50:43 IP_Addresses: theory Word_More

01:50:43 IP_Addresses: theory Code_Target_Nat

01:50:43 IP_Addresses: theory Code_Char

01:50:44 IP_Addresses: theory Multiset

01:50:51 IP_Addresses: theory Quicksort

01:50:51 IP_Addresses: theory List_More

01:50:52 IP_Addresses: theory Misc

01:51:20 IP_Addresses: theory Lib_Numbers_toString

01:51:20 IP_Addresses: theory Hs_Compat

01:51:20 IP_Addresses: theory Product_Lexorder

01:51:20 IP_Addresses: theory Word_Next

01:51:20 IP_Addresses: theory WordInterval

01:51:20 IP_Addresses: theory Lib_List_toString

01:51:20 IP_Addresses: theory Lib_Word_toString

01:51:26 IP_Addresses: theory IP_Address

01:51:26 IP_Addresses: theory WordInterval_Sorted

01:51:33 IP_Addresses: theory IPv4

01:51:33 IP_Addresses: theory IPv6

01:51:33 IP_Addresses: theory Prefix_Match

01:51:34 IP_Addresses: theory CIDR_Split

01:53:03 IP_Addresses: theory IP_Address_Parser

01:53:03 IP_Addresses: theory IP_Address_toString

01:56:55 Timing IP_Addresses (8 threads, 331.079s elapsed time, 1020.096s cpu time, 60.660s GC time, factor 3.08)

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

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

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

01:56:55 Finished IP_Addresses (0:06:16 elapsed time, 0:18:47 cpu time, factor 2.99)

01:56:56 Building Simple_Firewall ...

01:57:04 Simple_Firewall: theory GroupF

01:57:04 Simple_Firewall: theory Firewall_Common_Decision_State

01:57:04 Simple_Firewall: theory Option_Helpers

01:57:04 Simple_Firewall: theory List_Product_More

01:57:04 Simple_Firewall: theory IP_Partition_Preliminaries

01:57:04 Simple_Firewall: theory IP_Addr_WordInterval_toString

01:57:04 Simple_Firewall: theory Lib_Enum_toString

01:57:04 Simple_Firewall: theory Iface

01:57:05 Simple_Firewall: theory L4_Protocol

01:57:10 Simple_Firewall: theory Simple_Packet

01:57:10 Simple_Firewall: theory Primitives_toString

01:57:13 Simple_Firewall: theory SimpleFw_Syntax

01:57:17 Simple_Firewall: theory SimpleFw_Semantics

01:57:21 Simple_Firewall: theory Generic_SimpleFw

01:57:21 Simple_Firewall: theory Shadowed

01:57:21 Simple_Firewall: theory Service_Matrix

01:57:57 Timing Simple_Firewall (8 threads, 27.422s elapsed time, 106.184s cpu time, 4.232s GC time, factor 3.87)

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

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

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

01:57:57 Finished Simple_Firewall (0:01:00 elapsed time, 0:02:53 cpu time, factor 2.86)

01:57:57 Building Routing ...

01:58:06 Routing: theory Adhoc_Overloading

01:58:07 Routing: theory Monad_Syntax

01:58:07 Routing: theory Linorder_Helper

01:58:07 Routing: theory Prefix_Match_toString

01:58:08 Routing: theory Routing_Table

01:58:13 Routing: theory IpRoute_Parser

01:58:13 Routing: theory Linux_Router

01:58:38 Timing Routing (8 threads, 13.597s elapsed time, 49.724s cpu time, 1.076s GC time, factor 3.66)

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

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

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

01:58:38 Finished Routing (0:00:40 elapsed time, 0:01:35 cpu time, factor 2.34)

01:58:38 Building Iptables_Semantics ...

01:58:48 Iptables_Semantics: theory LaTeXsugar

01:58:48 Iptables_Semantics: theory List_Misc

01:58:48 Iptables_Semantics: theory More_Bits_Int

01:58:48 Iptables_Semantics: theory Negation_Type

01:58:51 Iptables_Semantics: theory WordInterval_Lists

01:58:51 Iptables_Semantics: theory Bits_Integer

01:59:04 Iptables_Semantics: theory Code_Target_Bits_Int

01:59:07 Iptables_Semantics: theory Conntrack_State

01:59:07 Iptables_Semantics: theory Negation_Type_DNF

01:59:07 Iptables_Semantics: theory Datatype_Selectors

01:59:07 Iptables_Semantics: theory Remdups_Rev

01:59:07 Iptables_Semantics: theory Repeat_Stabilize

01:59:07 Iptables_Semantics: theory L4_Protocol_Flags

01:59:07 Iptables_Semantics: theory SimpleFw_toString

01:59:07 Iptables_Semantics: theory Ternary

01:59:08 Iptables_Semantics: theory IpAddresses

01:59:08 Iptables_Semantics: theory Firewall_Common

01:59:08 Iptables_Semantics: theory Word_Upto

01:59:09 Iptables_Semantics: theory Ports

01:59:10 Iptables_Semantics: theory Tagged_Packet

01:59:12 Iptables_Semantics: theory Common_Primitive_Syntax

01:59:31 Iptables_Semantics: theory Semantics

01:59:31 Iptables_Semantics: theory Matching_Ternary

01:59:31 Iptables_Semantics: theory Semantics_Goto

01:59:33 Iptables_Semantics: theory Matching

01:59:33 Iptables_Semantics: theory Semantics_Stateful

01:59:33 Iptables_Semantics: theory Ruleset_Update

01:59:34 Iptables_Semantics: theory Call_Return_Unfolding

01:59:35 Iptables_Semantics: theory Semantics_Ternary

01:59:36 Iptables_Semantics: theory Unknown_Match_Tacs

01:59:37 Iptables_Semantics: theory Matching_Embeddings

01:59:37 Iptables_Semantics: theory Fixed_Action

01:59:37 Iptables_Semantics: theory Optimizing

01:59:37 Iptables_Semantics: theory Common_Primitive_Matcher_Generic

01:59:38 Iptables_Semantics: theory Normalized_Matches

01:59:39 Iptables_Semantics: theory Negation_Type_Matching

01:59:41 Iptables_Semantics: theory Primitive_Normalization

01:59:44 Iptables_Semantics: theory Common_Primitive_Matcher

01:59:47 Iptables_Semantics: theory MatchExpr_Fold

01:59:47 Iptables_Semantics: theory Ipassmt

01:59:52 Iptables_Semantics: theory Routing_IpAssmt

02:00:51 Iptables_Semantics: theory Common_Primitive_toString

02:00:51 Iptables_Semantics: theory Common_Primitive_Lemmas

02:00:51 Iptables_Semantics: theory Conntrack_State_Transform

02:00:51 Iptables_Semantics: theory Example_Semantics

02:00:52 Iptables_Semantics: theory Interfaces_Normalize

02:00:52 Iptables_Semantics: theory No_Spoof

02:00:52 Iptables_Semantics: theory Ports_Normalize

02:00:52 Iptables_Semantics: theory IpAddresses_Normalize

02:00:52 Iptables_Semantics: theory Protocols_Normalize

02:01:08 Iptables_Semantics: theory Output_Interface_Replace

02:01:10 Iptables_Semantics: theory Interface_Replace

02:01:14 Iptables_Semantics: theory Transform

02:01:20 Iptables_Semantics: theory Primitive_Abstract

02:01:22 Iptables_Semantics: theory SimpleFw_Compliance

02:01:29 Iptables_Semantics: theory Code_Interface

02:01:29 Iptables_Semantics: theory Semantics_Embeddings

02:01:31 Iptables_Semantics: theory Iptables_Semantics

02:01:31 Iptables_Semantics: theory No_Spoof_Embeddings

02:01:41 Iptables_Semantics: theory Parser

02:01:41 Iptables_Semantics: theory Documentation

02:01:42 Iptables_Semantics: theory Code_haskell

02:03:10 Timing Iptables_Semantics (8 threads, 198.328s elapsed time, 833.600s cpu time, 63.020s GC time, factor 4.20)

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

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

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

02:03:10 Finished Iptables_Semantics (0:04:30 elapsed time, 0:17:08 cpu time, factor 3.80)

02:03:11 Building HOL-Analysis ...

02:03:17 HOL-Analysis: theory Cancellation

02:03:17 HOL-Analysis: theory Disjoint_Sets

02:03:17 HOL-Analysis: theory FuncSet

02:03:17 HOL-Analysis: theory Old_Datatype

02:03:17 HOL-Analysis: theory Infinite_Set

02:03:17 HOL-Analysis: theory Nat_Bijection

02:03:17 HOL-Analysis: theory Product_Plus

02:03:17 HOL-Analysis: theory Phantom_Type

02:03:17 HOL-Analysis: theory Product_Order

02:03:18 HOL-Analysis: theory Set_Algebras

02:03:18 HOL-Analysis: theory L2_Norm

02:03:18 HOL-Analysis: theory Discrete

02:03:18 HOL-Analysis: theory Indicator_Function

02:03:18 HOL-Analysis: theory Multiset

02:03:18 HOL-Analysis: theory Inner_Product

02:03:18 HOL-Analysis: theory Liminf_Limsup

02:03:18 HOL-Analysis: theory Nonpos_Ints

02:03:18 HOL-Analysis: theory Operator_Norm

02:03:19 HOL-Analysis: theory Cardinality

02:03:19 HOL-Analysis: theory Periodic_Fun

02:03:19 HOL-Analysis: theory Poly_Roots

02:03:19 HOL-Analysis: theory Sum_of_Squares

02:03:19 HOL-Analysis: theory Countable

02:03:20 HOL-Analysis: theory Product_Vector

02:03:20 HOL-Analysis: theory Numeral_Type

02:03:21 HOL-Analysis: theory Euclidean_Space

02:03:21 HOL-Analysis: theory Countable_Set

02:03:22 HOL-Analysis: theory Countable_Complete_Lattices

02:03:22 HOL-Analysis: theory Continuum_Not_Denumerable

02:03:23 HOL-Analysis: theory Norm_Arith

02:03:24 HOL-Analysis: theory Finite_Cartesian_Product

02:03:24 HOL-Analysis: theory Linear_Algebra

02:03:26 HOL-Analysis: theory Permutations

02:03:26 HOL-Analysis: theory Factorial_Ring

02:03:26 HOL-Analysis: theory Order_Continuity

02:03:27 HOL-Analysis: theory Extended_Nat

02:03:28 HOL-Analysis: theory Topology_Euclidean_Space

02:03:29 HOL-Analysis: theory Extended_Real

02:03:35 HOL-Analysis: theory Extended_Nonnegative_Real

02:03:35 HOL-Analysis: theory Summation_Tests

02:03:38 HOL-Analysis: theory Euclidean_Algorithm

02:03:39 HOL-Analysis: theory Sigma_Algebra

02:03:42 HOL-Analysis: theory Bounded_Linear_Function

02:03:42 HOL-Analysis: theory Convex_Euclidean_Space

02:03:42 HOL-Analysis: theory Extended_Real_Limits

02:03:42 HOL-Analysis: theory Tagged_Division

02:03:42 HOL-Analysis: theory Uniform_Limit

02:03:44 HOL-Analysis: theory Measurable

02:03:45 HOL-Analysis: theory Measure_Space

02:03:50 HOL-Analysis: theory Caratheodory

02:03:51 HOL-Analysis: theory Primes

02:03:52 HOL-Analysis: theory Continuous_Extension

02:03:52 HOL-Analysis: theory Path_Connected

02:04:00 HOL-Analysis: theory Homeomorphism

02:04:01 HOL-Analysis: theory Brouwer_Fixpoint

02:04:05 HOL-Analysis: theory Derivative

02:04:08 HOL-Analysis: theory Cartesian_Euclidean_Space

02:04:09 HOL-Analysis: theory Weierstrass_Theorems

02:04:13 HOL-Analysis: theory Determinants

02:04:13 HOL-Analysis: theory Fashoda_Theorem

02:04:13 HOL-Analysis: theory Ordered_Euclidean_Space

02:04:13 HOL-Analysis: theory Polytope

02:04:20 HOL-Analysis: theory Arcwise_Connected

02:04:20 HOL-Analysis: theory Borel_Space

02:04:25 HOL-Analysis: theory Nonnegative_Lebesgue_Integration

02:04:25 HOL-Analysis: theory Regularity

02:04:29 HOL-Analysis: theory Binary_Product_Measure

02:04:31 HOL-Analysis: theory Embed_Measure

02:04:31 HOL-Analysis: theory Finite_Product_Measure

02:04:33 HOL-Analysis: theory Bochner_Integration

02:04:33 HOL-Analysis: theory Function_Topology

02:04:37 HOL-Analysis: theory Complete_Measure

02:04:37 HOL-Analysis: theory Radon_Nikodym

02:04:38 HOL-Analysis: theory Set_Integral

02:04:38 HOL-Analysis: theory Lebesgue_Measure

02:04:41 HOL-Analysis: theory Henstock_Kurzweil_Integration

02:04:48 HOL-Analysis: theory Bounded_Continuous_Function

02:04:49 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration

02:04:49 HOL-Analysis: theory Integral_Test

02:04:51 HOL-Analysis: theory Complex_Analysis_Basics

02:04:51 HOL-Analysis: theory Interval_Integral

02:04:53 HOL-Analysis: theory Lebesgue_Integral_Substitution

02:04:54 HOL-Analysis: theory Complex_Transcendental

02:04:59 HOL-Analysis: theory Generalised_Binomial_Theorem

02:04:59 HOL-Analysis: theory Harmonic_Numbers

02:05:00 HOL-Analysis: theory Cauchy_Integral_Theorem

02:05:00 HOL-Analysis: theory Further_Topology

02:05:07 HOL-Analysis: theory Jordan_Curve

02:05:10 HOL-Analysis: theory Conformal_Mappings

02:05:11 HOL-Analysis: theory Gamma_Function

02:05:33 HOL-Analysis: theory Analysis

02:13:30 Timing HOL-Analysis (8 threads, 488.388s elapsed time, 2264.484s cpu time, 187.812s GC time, factor 4.64)

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

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

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

02:13:30 Finished HOL-Analysis (0:10:18 elapsed time, 0:41:29 cpu time, factor 4.03)

02:13:32 Building Ordinary_Differential_Equations ...

02:13:43 Ordinary_Differential_Equations: theory Code_Abstract_Nat

02:13:43 Ordinary_Differential_Equations: theory Code_Target_Int

02:13:43 Ordinary_Differential_Equations: theory Lattice_Algebras

02:13:43 Ordinary_Differential_Equations: theory Log_Nat

02:13:43 Ordinary_Differential_Equations: theory Dense_Linear_Order

02:13:43 Ordinary_Differential_Equations: theory Diagonal_Subsequence

02:13:43 Ordinary_Differential_Equations: theory Code_Target_Nat

02:13:43 Ordinary_Differential_Equations: theory Code_Target_Numeral

02:13:51 Ordinary_Differential_Equations: theory Float

02:13:54 Ordinary_Differential_Equations: theory Approximation

02:14:59 Ordinary_Differential_Equations: theory ODE_Auxiliarities

02:14:59 Ordinary_Differential_Equations: theory Bounded_Linear_Operator

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

02:15:07 Ordinary_Differential_Equations FAILED

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

02:15:07 *** unded[]uniform[]limit$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF Bounded[]Linear[]Fu

02:15:07 *** nction$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 blinfun$\OML/cmm/m/it/10 :$\OT1/cmr/

02:15:07 *** m/it/10 flip$\OT1/cmr/m/n/10 ]$[]

02:15:07 *** ))

02:15:07 *** No file root.bbl.

02:15:07 *** [3] (./root.aux)

02:15:07 ***

02:15:07 *** Package rerunfilecheck Warning: File `root.out' has changed.

02:15:07 *** (rerunfilecheck) Rerun to get outlines right

02:15:07 *** (rerunfilecheck) or use package `bookmark'.

02:15:07 ***

02:15:07 *** )

02:15:07 *** (see the transcript file for additional information)</usr/share/texlive/texmf-d

02:15:07 *** ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo

02:15:07 *** nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty

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

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

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

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

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

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

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

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

02:15:07 *** /texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb>

02:15:07 *** Output written on root.pdf (3 pages, 138469 bytes).

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

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

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

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

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

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

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

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

02:15:07 ***

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

02:15:07 *** Undefined fact: "uniform_limit_on_union" (line 2913 of "~~/afp/thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy")

02:15:07 *** At command "lemmas" (line 2913 of "~~/afp/thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy")

02:15:07 *** At command "by" (line 1892 of "~~/afp/thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy")

02:15:07 *** Undefined fact: "uniform_limit_on_union" (line 2913 of "~~/afp/thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy")

02:15:07 *** At command "lemmas" (line 2913 of "~~/afp/thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy")

02:15:07 HOL-ODE CANCELLED

02:15:07 HOL-ODE-Refinement CANCELLED

02:15:07 HOL-ODE-Numerics CANCELLED

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

02:15:19 Flyspeck-Tame: theory Trie

02:15:22 Flyspeck-Tame: theory Tries

02:15:45 Flyspeck-Tame: theory Arch

02:15:45 Flyspeck-Tame: theory Quasi_Order

02:15:45 Flyspeck-Tame: theory IArray_Syntax

02:15:45 Flyspeck-Tame: theory RTranCl

02:15:45 Flyspeck-Tame: theory ListAux

02:15:46 Flyspeck-Tame: theory PlaneGraphIso

02:15:46 Flyspeck-Tame: theory Worklist

02:15:47 Flyspeck-Tame: theory Maps

02:15:47 Flyspeck-Tame: theory ListSum

02:15:47 Flyspeck-Tame: theory Rotation

02:15:48 Flyspeck-Tame: theory Graph

02:15:51 Flyspeck-Tame: theory Enumerator

02:15:51 Flyspeck-Tame: theory FaceDivision

02:15:52 Flyspeck-Tame: theory GraphProps

02:15:52 Flyspeck-Tame: theory Tame

02:15:52 Flyspeck-Tame: theory Plane

02:15:52 Flyspeck-Tame: theory EnumeratorProps

02:15:52 Flyspeck-Tame: theory TameProps

02:15:53 Flyspeck-Tame: theory Plane1

02:15:53 Flyspeck-Tame: theory Generator

02:15:54 Flyspeck-Tame: theory FaceDivisionProps

02:15:55 Flyspeck-Tame: theory TameEnum

02:16:02 Flyspeck-Tame: theory Invariants

02:16:03 Flyspeck-Tame: theory ArchCompAux

02:16:05 Flyspeck-Tame: theory PlaneProps

02:16:06 Flyspeck-Tame: theory Plane1Props

02:16:06 Flyspeck-Tame: theory ScoreProps

02:16:07 Flyspeck-Tame: theory LowerBound

02:16:07 Flyspeck-Tame: theory GeneratorProps

02:16:08 Flyspeck-Tame: theory TameEnumProps

02:16:08 Flyspeck-Tame: theory ArchCompProps

02:16:09 Flyspeck-Tame: theory ArchComp

02:16:09 Flyspeck-Tame: theory Completeness

12:25:02 Timing Flyspeck-Tame (8 threads, 36573.660s elapsed time, 54724.452s cpu time, 863.592s GC time, factor 1.50)

12:25:02 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame

12:25:02 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf

12:25:02 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf

12:25:02 Finished Flyspeck-Tame (10:09:54 elapsed time, 15:12:29 cpu time, factor 1.50)

12:25:03 Running Iptables_Semantics_Examples ...

12:25:24 Iptables_Semantics_Examples: theory Analyze_SQRL_Shorewall

12:25:24 Iptables_Semantics_Examples: theory Analyze_TUM_Net_Firewall

12:25:24 Iptables_Semantics_Examples: theory Analyze_medium_sized_company

12:25:24 Iptables_Semantics_Examples: theory Analyze_topos_generated

12:25:24 Iptables_Semantics_Examples: theory Contrived_Example

12:25:24 Iptables_Semantics_Examples: theory Analyze_Ringofsaturn_com

12:25:24 Iptables_Semantics_Examples: theory Parser_Test

12:25:24 Iptables_Semantics_Examples: theory IP_Address_Space_Examples_All_Small

12:25:32 Iptables_Semantics_Examples: theory SNS_IAS_Eduroam_Spoofing

12:25:36 Iptables_Semantics_Examples: theory SQRL_2015_nospoof

12:25:36 Iptables_Semantics_Examples: theory TUM_Spoofing_new3

12:25:36 Iptables_Semantics_Examples: theory Parser6

12:25:37 Iptables_Semantics_Examples: theory Parser6_Test

12:25:44 Iptables_Semantics_Examples: theory Ports_Fail

12:25:45 Iptables_Semantics_Examples: theory Small_Examples

12:25:45 Iptables_Semantics_Examples: theory iptables_Ln_tuned_parsed

12:25:47 Iptables_Semantics_Examples: theory Analyze_Synology_Diskstation

21:33:13 Build timed out (after 1,200 minutes). Marking the build as aborted.

21:33:14 Build was aborted

21:33:14 Archiving artifacts

21:33:14 Started calculate disk usage of build

21:33:14 Finished Calculation of disk usage of build in 0 seconds

21:33:23 Started calculate disk usage of workspace

21:33:23 Finished Calculation of disk usage of workspace in 0 seconds

21:33:23 No emails were triggered.

21:33:23 Finished: ABORTED