Status

Changes

Console Output

View Build Information

Polling Log

Timings

Environment Variables

Mercurial Build Data

Embeddable Build Status

Previous Build

Next Build

Console Output

01:33:12 Started by an SCM change

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

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

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

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

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

01:33:13 searching for changes

01:33:13 no changes found

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

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

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

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

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

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

01:33:14 exists

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

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

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

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

01:33:15 no changes found

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

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

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

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

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

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

01:33:16 exists

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

01:33:16 No emails were triggered.

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

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

01:33:16 + set -e

01:33:16 + PROFILE=slow

01:33:16 + shift

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

01:33:16 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/polyml-test-79534495ee94"

01:33:16 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/scala-2.12.4"

01:33:16 Getting "https://isabelle.in.tum.de/components/polyml-test-79534495ee94.tar.gz"

01:33:17 Unpacking "/media/data/jenkins/.isabelle/contrib/polyml-test-79534495ee94.tar.gz"

01:33:18 Getting "https://isabelle.in.tum.de/components/scala-2.12.4.tar.gz"

01:33:18 Unpacking "/media/data/jenkins/.isabelle/contrib/scala-2.12.4.tar.gz"

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

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

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

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

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

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

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

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

01:33:20 4 warnings

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

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

01:34:43 + bin/isabelle ci_build_slow

01:34:51

01:34:51 === CONFIGURATION ===

01:34:51

01:34:51 ISABELLE_BUILD_OPTIONS=""

01:34:51

01:34:51 ML_PLATFORM="x86_64-linux"

01:34:51 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-79534495ee94/x86_64-linux"

01:34:51 ML_SYSTEM="polyml-5.7.1"

01:34:51 ML_OPTIONS="-H 4000 --maxheap 10G"

01:34:52

01:34:52 === BUILD ===

01:34:52

01:34:52 Build started at Mon, 6 Nov 2017 01:34:51 +0100

01:34:52 Isabelle id 335a7dce7cb3

01:34:52 Build for AFP id fee069c9805b

01:34:52

01:34:52 === LOG ===

01:34:52

01:34:53 Session Pure/Pure

01:34:54 Session FOL/FOL

01:34:54 Session HOL/HOL (main)

01:34:55 Session AFP/AWN (AFP)

01:34:55 Session AFP/AODV (AFP slow)

01:34:55 Session HOL/HOL-Eisbach

01:34:55 Session HOL/HOL-Library (main timing)

01:34:56 Session AFP/Binomial-Heaps (AFP)

01:34:57 Session AFP/ConcurrentIMP (AFP)

01:34:57 Session AFP/ConcurrentGC (AFP slow)

01:34:58 Session AFP/FinFun (AFP)

01:34:58 Session AFP/Finger-Trees (AFP)

01:34:58 Session HOL/HOL-Computational_Algebra (timing)

01:34:58 Session HOL/HOL-Algebra (main timing)

01:34:58 Session HOL/HOL-Decision_Procs (timing)

01:34:58 Session HOL/HOL-Analysis (main timing)

01:34:59 Session AFP/Coinductive (AFP)

01:35:00 Session AFP/Triangle (AFP)

01:35:00 Session HOL/HOL-Number_Theory (timing)

01:35:00 Session HOL/HOL-ex (timing)

01:35:00 Session AFP/Automatic_Refinement (AFP)

01:35:00 Session HOL/HOL-Imperative_HOL (timing)

01:35:00 Session AFP/Trie (AFP)

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

01:35:01 Session HOL/HOL-Types_To_Sets

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

01:35:01 Session AFP/Native_Word (AFP)

01:35:01 Session AFP/Refine_Monadic (AFP)

01:35:01 Session AFP/Collections (AFP)

01:35:02 Session AFP/Deriving (AFP)

01:35:02 Session AFP/Show (AFP)

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

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

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

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

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

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

01:35:03 Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow)

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

01:35:05 Session AFP/List-Index (AFP)

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

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

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

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

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

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

01:35:07 Session AFP/Lorenz_Approximation (AFP)

01:35:07 Session AFP/Lorenz_C0 (AFP slow)

01:35:08 Building Pure ...

01:35:31 Pure: theory Pure

01:35:32 Pure: theory ML_Bootstrap

01:35:35 Timing Pure (1 threads, 0.918s elapsed time, 0.920s cpu time, 0.000s GC time, factor 1.00)

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

01:35:35 Finished Pure (0:00:25 elapsed time, 0:00:25 cpu time, factor 0.98)

01:35:35 Building HOL ...

01:35:37 HOL: theory HOL.Code_Generator

01:35:40 HOL: theory HOL.HOL

01:35:46 HOL: theory HOL.Argo

01:35:46 HOL: theory HOL.Orderings

01:35:46 HOL: theory HOL.Ctr_Sugar

01:35:48 HOL: theory HOL.SAT

01:35:48 HOL: theory HOL.Groups

01:35:51 HOL: theory HOL.Lattices

01:35:54 HOL: theory HOL.Set

01:35:55 HOL: theory HOL.Fun

01:35:55 HOL: theory HOL.Typedef

01:35:55 HOL: theory HOL.Rings

01:35:56 HOL: theory HOL.Complete_Lattices

01:36:00 HOL: theory HOL.Inductive

01:36:02 HOL: theory HOL.Product_Type

01:36:02 HOL: theory HOL.Sum_Type

01:36:04 HOL: theory HOL.Complete_Partial_Order

01:36:09 HOL: theory HOL.Nat

01:36:11 HOL: theory HOL.Fields

01:36:11 HOL: theory HOL.Meson

01:36:12 HOL: theory HOL.ATP

01:36:16 HOL: theory HOL.Metis

01:36:18 HOL: theory HOL.Finite_Set

01:36:19 HOL: theory HOL.Relation

01:36:21 HOL: theory HOL.Transitive_Closure

01:36:23 HOL: theory HOL.Wellfounded

01:36:24 HOL: theory HOL.Fun_Def_Base

01:36:24 HOL: theory HOL.Hilbert_Choice

01:36:24 HOL: theory HOL.Wfrec

01:36:24 HOL: theory HOL.Order_Relation

01:36:25 HOL: theory HOL.BNF_Wellorder_Relation

01:36:25 HOL: theory HOL.Zorn

01:36:25 HOL: theory HOL.BNF_Wellorder_Embedding

01:36:26 HOL: theory HOL.BNF_Wellorder_Constructions

01:36:27 HOL: theory HOL.BNF_Cardinal_Order_Relation

01:36:28 HOL: theory HOL.BNF_Cardinal_Arithmetic

01:36:29 HOL: theory HOL.BNF_Def

01:36:33 HOL: theory HOL.BNF_Composition

01:36:33 HOL: theory HOL.Basic_BNFs

01:36:34 HOL: theory HOL.BNF_Fixpoint_Base

01:36:39 HOL: theory HOL.BNF_Least_Fixpoint

01:36:43 HOL: theory HOL.Basic_BNF_LFPs

01:36:44 HOL: theory HOL.Transfer

01:36:45 HOL: theory HOL.Num

01:36:49 HOL: theory HOL.Power

01:36:53 HOL: theory HOL.Groups_Big

01:36:56 HOL: theory HOL.Equiv_Relations

01:36:57 HOL: theory HOL.Lifting

01:36:59 HOL: theory HOL.Lifting_Set

01:36:59 HOL: theory HOL.Option

01:36:59 HOL: theory HOL.Quotient

01:37:00 HOL: theory HOL.Extraction

01:37:00 HOL: theory HOL.Lattices_Big

01:37:00 HOL: theory HOL.Partial_Function

01:37:01 HOL: theory HOL.Fun_Def

01:37:03 HOL: theory HOL.Int

01:37:07 HOL: theory HOL.Euclidean_Division

01:37:15 HOL: theory HOL.Parity

01:37:20 HOL: theory HOL.Divides

01:37:24 HOL: theory HOL.Code_Numeral

01:37:24 HOL: theory HOL.Numeral_Simprocs

01:37:24 HOL: theory HOL.Set_Interval

01:37:24 HOL: theory HOL.SMT

01:37:26 HOL: theory HOL.Semiring_Normalization

01:37:29 HOL: theory HOL.Groebner_Basis

01:37:30 HOL: theory HOL.Conditionally_Complete_Lattices

01:37:30 HOL: theory HOL.Filter

01:37:31 HOL: theory HOL.Presburger

01:37:35 HOL: theory HOL.Sledgehammer

01:37:38 HOL: theory HOL.List

01:37:51 HOL: theory HOL.Groups_List

01:37:51 HOL: theory HOL.Map

01:37:53 HOL: theory HOL.Factorial

01:37:53 HOL: theory HOL.GCD

01:37:53 HOL: theory HOL.Enum

01:37:53 HOL: theory HOL.Random

01:37:53 HOL: theory HOL.Binomial

01:37:57 HOL: theory HOL.String

01:37:58 HOL: theory HOL.BNF_Greatest_Fixpoint

01:37:58 HOL: theory HOL.Predicate

01:37:58 HOL: theory HOL.Typerep

01:37:59 HOL: theory HOL.Lazy_Sequence

01:38:01 HOL: theory HOL.Limited_Sequence

01:38:01 HOL: theory HOL.Code_Evaluation

01:38:03 HOL: theory HOL.Quickcheck_Random

01:38:07 HOL: theory HOL.Quickcheck_Exhaustive

01:38:07 HOL: theory HOL.Quickcheck_Narrowing

01:38:07 HOL: theory HOL.Random_Pred

01:38:08 HOL: theory HOL.Random_Sequence

01:38:12 HOL: theory HOL.Record

01:38:12 HOL: theory HOL.Predicate_Compile

01:38:15 HOL: theory HOL.Nitpick

01:38:23 HOL: theory HOL.Nunchaku

01:38:24 HOL: theory Main

01:38:26 HOL: theory HOL.Archimedean_Field

01:38:26 HOL: theory HOL.Topological_Spaces

01:38:35 HOL: theory HOL.Rat

01:38:39 HOL: theory HOL.Real

01:38:41 HOL: theory HOL.Real_Vector_Spaces

01:38:57 HOL: theory HOL.Inequalities

01:38:57 HOL: theory HOL.Limits

01:39:02 HOL: theory HOL.Deriv

01:39:02 HOL: theory HOL.Series

01:39:05 HOL: theory HOL.NthRoot

01:39:06 HOL: theory HOL.Transcendental

01:39:16 HOL: theory HOL.Complex

01:39:18 HOL: theory HOL.MacLaurin

01:39:19 HOL: theory Complex_Main

01:41:22 Timing HOL (8 threads, 244.305s elapsed time, 767.732s cpu time, 97.804s GC time, factor 3.14)

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

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

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

01:41:22 Finished HOL (0:05:40 elapsed time, 0:15:36 cpu time, factor 2.76)

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

01:41:25 HOL-Library: theory HOL-Library.Adhoc_Overloading

01:41:25 HOL-Library: theory HOL-Library.BNF_Corec

01:41:25 HOL-Library: theory HOL-Library.Bit

01:41:25 HOL-Library: theory HOL-Library.BNF_Axiomatization

01:41:25 HOL-Library: theory HOL-Library.AList

01:41:25 HOL-Library: theory HOL-Library.Cancellation

01:41:25 HOL-Library: theory HOL-Library.Lattice_Syntax

01:41:25 HOL-Library: theory HOL-Library.Boolean_Algebra

01:41:25 HOL-Library: theory HOL-Library.Cardinal_Notations

01:41:25 HOL-Library: theory HOL-Library.Char_ord

01:41:25 HOL-Library: theory HOL-Library.Code_Abstract_Nat

01:41:25 HOL-Library: theory HOL-Library.Code_Prolog

01:41:25 HOL-Library: theory HOL-Library.Code_Char

01:41:25 HOL-Library: theory HOL-Library.Code_Target_Int

01:41:25 HOL-Library: theory HOL-Library.Code_Binary_Nat

01:41:25 HOL-Library: theory HOL-Library.Code_Target_Nat

01:41:25 HOL-Library: theory HOL-Library.Code_Test

01:41:26 HOL-Library: theory HOL-Library.Combine_PER

01:41:26 HOL-Library: theory HOL-Library.Code_Target_Numeral

01:41:26 HOL-Library: theory HOL-Library.Complete_Partial_Order2

01:41:26 HOL-Library: theory HOL-Library.Multiset

01:41:26 HOL-Library: theory HOL-Library.Debug

01:41:26 HOL-Library: theory HOL-Library.Disjoint_Sets

01:41:26 HOL-Library: theory HOL-Library.Dlist

01:41:26 HOL-Library: theory HOL-Library.Fun_Lexorder

01:41:26 HOL-Library: theory HOL-Library.FuncSet

01:41:27 HOL-Library: theory HOL-Library.Function_Algebras

01:41:27 HOL-Library: theory HOL-Library.Function_Division

01:41:27 HOL-Library: theory HOL-Library.Groups_Big_Fun

01:41:27 HOL-Library: theory HOL-Library.IArray

01:41:27 HOL-Library: theory HOL-Library.Infinite_Set

01:41:28 HOL-Library: theory HOL-Library.DAList

01:41:28 HOL-Library: theory HOL-Library.LaTeXsugar

01:41:28 HOL-Library: theory HOL-Library.Lattice_Constructions

01:41:28 HOL-Library: theory HOL-Library.Omega_Words_Fun

01:41:28 HOL-Library: theory HOL-Library.Ramsey

01:41:28 HOL-Library: theory HOL-Library.ListVector

01:41:28 HOL-Library: theory HOL-Library.List_lexord

01:41:28 HOL-Library: theory HOL-Library.Mapping

01:41:28 HOL-Library: theory HOL-Library.Monad_Syntax

01:41:29 HOL-Library: theory HOL-Library.More_List

01:41:29 HOL-Library: theory HOL-Library.State_Monad

01:41:29 HOL-Library: theory HOL-Library.Nat_Bijection

01:41:29 HOL-Library: theory HOL-Library.Old_Datatype

01:41:30 HOL-Library: theory HOL-Library.Stream

01:41:30 HOL-Library: theory HOL-Library.AList_Mapping

01:41:31 HOL-Library: theory HOL-Library.Old_Recdef

01:41:31 HOL-Library: theory HOL-Library.Open_State_Syntax

01:41:31 HOL-Library: theory HOL-Library.Option_ord

01:41:32 HOL-Library: theory HOL-Library.Parallel

01:41:32 HOL-Library: theory HOL-Library.Pattern_Aliases

01:41:32 HOL-Library: theory HOL-Library.Perm

01:41:32 HOL-Library: theory HOL-Library.Phantom_Type

01:41:33 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs

01:41:33 HOL-Library: theory HOL-Library.Preorder

01:41:33 HOL-Library: theory HOL-Library.Product_Lexorder

01:41:33 HOL-Library: theory HOL-Library.Product_Plus

01:41:33 HOL-Library: theory HOL-Library.Quotient_Syntax

01:41:33 HOL-Library: theory HOL-Library.Quotient_Option

01:41:33 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck

01:41:33 HOL-Library: theory HOL-Library.Quotient_Product

01:41:33 HOL-Library: theory HOL-Library.Quotient_Set

01:41:33 HOL-Library: theory HOL-Library.Product_Order

01:41:33 HOL-Library: theory HOL-Library.Quotient_Sum

01:41:33 HOL-Library: theory HOL-Library.Quotient_List

01:41:34 HOL-Library: theory HOL-Library.Quotient_Type

01:41:34 HOL-Library: theory HOL-Library.RBT_Impl

01:41:34 HOL-Library: theory HOL-Library.Cardinality

01:41:34 HOL-Library: theory HOL-Library.Finite_Lattice

01:41:34 HOL-Library: theory HOL-Library.Reflection

01:41:34 HOL-Library: theory HOL-Library.Refute

01:41:34 HOL-Library: theory HOL-Library.Rewrite

01:41:34 HOL-Library: theory HOL-Library.Set_Algebras

01:41:34 HOL-Library: theory HOL-Library.Simps_Case_Conv

01:41:35 HOL-Library: theory HOL-Library.Extended

01:41:35 HOL-Library: theory HOL-Library.Stirling

01:41:35 HOL-Library: theory HOL-Library.Sublist

01:41:35 HOL-Library: theory HOL-Library.Numeral_Type

01:41:35 HOL-Library: theory HOL-Library.Transitive_Closure_Table

01:41:35 HOL-Library: theory HOL-Library.DAList_Multiset

01:41:36 HOL-Library: theory HOL-Library.Multiset_Order

01:41:36 HOL-Library: theory HOL-Library.Permutation

01:41:36 HOL-Library: theory HOL-Library.Permutations

01:41:36 HOL-Library: theory HOL-Library.Tree

01:41:38 HOL-Library: theory HOL-Library.Uprod

01:41:38 HOL-Library: theory HOL-Library.Type_Length

01:41:38 HOL-Library: theory HOL-Library.Saturated

01:41:39 HOL-Library: theory HOL-Library.Prefix_Order

01:41:39 HOL-Library: theory HOL-Library.Subseq_Order

01:41:39 HOL-Library: theory HOL-Library.While_Combinator

01:41:39 HOL-Library: theory HOL-Library.Countable

01:41:39 HOL-Library: theory HOL-Library.BigO

01:41:39 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float

01:41:39 HOL-Library: theory HOL-Library.Diagonal_Subsequence

01:41:40 HOL-Library: theory HOL-Library.Discrete

01:41:40 HOL-Library: theory HOL-Library.Going_To_Filter

01:41:40 HOL-Library: theory HOL-Library.Indicator_Function

01:41:40 HOL-Library: theory HOL-Library.Lattice_Algebras

01:41:40 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint

01:41:40 HOL-Library: theory HOL-Library.Liminf_Limsup

01:41:40 HOL-Library: theory HOL-Library.Log_Nat

01:41:40 HOL-Library: theory HOL-Library.Lub_Glb

01:41:40 HOL-Library: theory HOL-Library.Multiset_Permutations

01:41:41 HOL-Library: theory HOL-Library.Nonpos_Ints

01:41:41 HOL-Library: theory HOL-Library.OptionalSugar

01:41:41 HOL-Library: theory HOL-Library.Countable_Set

01:41:41 HOL-Library: theory HOL-Library.FSet

01:41:41 HOL-Library: theory HOL-Library.Periodic_Fun

01:41:41 HOL-Library: theory HOL-Library.Quadratic_Discriminant

01:41:41 HOL-Library: theory HOL-Library.Sum_of_Squares

01:41:42 HOL-Library: theory HOL-Library.Countable_Complete_Lattices

01:41:42 HOL-Library: theory HOL-Library.Countable_Set_Type

01:41:42 HOL-Library: theory HOL-Library.Tree_Multiset

01:41:42 HOL-Library: theory HOL-Library.Tree_Real

01:41:45 HOL-Library: theory HOL-Library.Order_Continuity

01:41:46 HOL-Library: theory HOL-Library.Extended_Nat

01:41:46 HOL-Library: theory HOL-Library.Finite_Map

01:41:47 HOL-Library: theory HOL-Library.Float

01:41:47 HOL-Library: theory HOL-Library.Extended_Real

01:41:47 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams

01:41:53 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real

01:41:58 HOL-Library: theory HOL-Library.Library

01:42:24 HOL-Library: theory HOL-Library.RBT

01:42:25 HOL-Library: theory HOL-Library.RBT_Mapping

01:42:25 HOL-Library: theory HOL-Library.RBT_Set

01:44:00 Timing HOL-Library (8 threads, 83.709s elapsed time, 541.872s cpu time, 32.780s GC time, factor 6.47)

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

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

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

01:44:00 Finished HOL-Library (0:02:34 elapsed time, 0:11:11 cpu time, factor 4.34)

01:44:00 Building HOL-Analysis ...

01:44:03 HOL-Analysis: theory HOL-Library.Disjoint_Sets

01:44:03 HOL-Analysis: theory HOL-Library.FuncSet

01:44:03 HOL-Analysis: theory HOL-Library.Infinite_Set

01:44:03 HOL-Analysis: theory HOL-Library.Nat_Bijection

01:44:03 HOL-Analysis: theory HOL-Library.Old_Datatype

01:44:03 HOL-Analysis: theory HOL-Library.Phantom_Type

01:44:03 HOL-Analysis: theory HOL-Library.Product_Plus

01:44:03 HOL-Analysis: theory HOL-Library.Cancellation

01:44:04 HOL-Analysis: theory HOL-Library.Product_Order

01:44:04 HOL-Analysis: theory HOL-Library.Set_Algebras

01:44:04 HOL-Analysis: theory HOL-Analysis.Infinite_Products

01:44:04 HOL-Analysis: theory HOL-Analysis.Inner_Product

01:44:04 HOL-Analysis: theory HOL-Analysis.L2_Norm

01:44:04 HOL-Analysis: theory HOL-Analysis.Operator_Norm

01:44:05 HOL-Analysis: theory HOL-Analysis.Poly_Roots

01:44:05 HOL-Analysis: theory HOL-Library.Discrete

01:44:05 HOL-Analysis: theory HOL-Library.Multiset

01:44:05 HOL-Analysis: theory HOL-Library.Indicator_Function

01:44:05 HOL-Analysis: theory HOL-Library.Liminf_Limsup

01:44:05 HOL-Analysis: theory HOL-Library.Nonpos_Ints

01:44:05 HOL-Analysis: theory HOL-Library.Cardinality

01:44:05 HOL-Analysis: theory HOL-Library.Periodic_Fun

01:44:06 HOL-Analysis: theory HOL-Library.Sum_of_Squares

01:44:06 HOL-Analysis: theory HOL-Library.Countable

01:44:06 HOL-Analysis: theory HOL-Analysis.Product_Vector

01:44:07 HOL-Analysis: theory HOL-Library.Numeral_Type

01:44:07 HOL-Analysis: theory HOL-Analysis.Euclidean_Space

01:44:08 HOL-Analysis: theory HOL-Library.Countable_Set

01:44:09 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices

01:44:09 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable

01:44:09 HOL-Analysis: theory HOL-Analysis.Linear_Algebra

01:44:09 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product

01:44:10 HOL-Analysis: theory HOL-Analysis.Norm_Arith

01:44:12 HOL-Analysis: theory HOL-Library.Order_Continuity

01:44:13 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring

01:44:13 HOL-Analysis: theory HOL-Library.Permutations

01:44:13 HOL-Analysis: theory HOL-Library.Extended_Nat

01:44:14 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space

01:44:15 HOL-Analysis: theory HOL-Library.Extended_Real

01:44:20 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real

01:44:22 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function

01:44:22 HOL-Analysis: theory HOL-Analysis.Connected

01:44:24 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra

01:44:24 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits

01:44:24 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm

01:44:26 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space

01:44:26 HOL-Analysis: theory HOL-Analysis.Tagged_Division

01:44:26 HOL-Analysis: theory HOL-Analysis.Summation_Tests

01:44:27 HOL-Analysis: theory HOL-Analysis.Uniform_Limit

01:44:28 HOL-Analysis: theory HOL-Analysis.Measurable

01:44:30 HOL-Analysis: theory HOL-Analysis.Measure_Space

01:44:30 HOL-Analysis: theory HOL-Analysis.Starlike

01:44:34 HOL-Analysis: theory HOL-Analysis.Caratheodory

01:44:35 HOL-Analysis: theory HOL-Analysis.Continuous_Extension

01:44:36 HOL-Analysis: theory HOL-Analysis.Path_Connected

01:44:37 HOL-Analysis: theory HOL-Computational_Algebra.Primes

01:44:37 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series

01:44:42 HOL-Analysis: theory HOL-Analysis.Homeomorphism

01:44:44 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint

01:44:47 HOL-Analysis: theory HOL-Analysis.Derivative

01:44:50 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space

01:44:51 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems

01:44:54 HOL-Analysis: theory HOL-Analysis.Determinants

01:44:54 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem

01:44:54 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space

01:44:54 HOL-Analysis: theory HOL-Analysis.Polytope

01:45:00 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected

01:45:00 HOL-Analysis: theory HOL-Analysis.Borel_Space

01:45:04 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration

01:45:04 HOL-Analysis: theory HOL-Analysis.Regularity

01:45:08 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure

01:45:09 HOL-Analysis: theory HOL-Analysis.Embed_Measure

01:45:09 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure

01:45:11 HOL-Analysis: theory HOL-Analysis.Bochner_Integration

01:45:11 HOL-Analysis: theory HOL-Analysis.Function_Topology

01:45:15 HOL-Analysis: theory HOL-Analysis.Complete_Measure

01:45:15 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym

01:45:15 HOL-Analysis: theory HOL-Analysis.Set_Integral

01:45:16 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure

01:45:16 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum

01:45:18 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration

01:45:24 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function

01:45:24 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration

01:45:24 HOL-Analysis: theory HOL-Analysis.Integral_Test

01:45:27 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics

01:45:27 HOL-Analysis: theory HOL-Analysis.Improper_Integral

01:45:27 HOL-Analysis: theory HOL-Analysis.Interval_Integral

01:45:29 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution

01:45:29 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental

01:45:33 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem

01:45:33 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers

01:45:33 HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem

01:45:33 HOL-Analysis: theory HOL-Analysis.Further_Topology

01:45:39 HOL-Analysis: theory HOL-Analysis.Jordan_Curve

01:45:41 HOL-Analysis: theory HOL-Analysis.Conformal_Mappings

01:45:45 HOL-Analysis: theory HOL-Analysis.FPS_Convergence

01:45:45 HOL-Analysis: theory HOL-Analysis.Gamma_Function

01:45:45 HOL-Analysis: theory HOL-Analysis.Great_Picard

01:45:47 HOL-Analysis: theory HOL-Analysis.Riemann_Mapping

01:45:49 HOL-Analysis: theory HOL-Analysis.Winding_Numbers

01:45:54 HOL-Analysis: theory HOL-Analysis.Analysis

01:53:49 Timing HOL-Analysis (8 threads, 388.254s elapsed time, 2070.296s cpu time, 145.280s GC time, factor 5.33)

01:53:49 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis

01:53:49 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/document.pdf

01:53:49 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/outline.pdf

01:53:49 Finished HOL-Analysis (0:09:46 elapsed time, 0:37:29 cpu time, factor 3.84)

01:53:49 Building HOL-Computational_Algebra ...

01:53:51 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field

01:53:51 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring

01:54:02 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm

01:54:02 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial

01:54:11 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra

01:54:12 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction

01:54:12 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes

01:54:13 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring

01:54:13 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series

01:54:13 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers

01:54:13 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree

01:54:13 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial

01:54:18 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS

01:54:30 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra

01:55:10 Timing HOL-Computational_Algebra (8 threads, 50.715s elapsed time, 150.824s cpu time, 5.808s GC time, factor 2.97)

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

01:55:10 Finished HOL-Computational_Algebra (0:01:19 elapsed time, 0:03:17 cpu time, factor 2.48)

01:55:10 Building HOL-Word ...

01:55:11 HOL-Word: theory HOL-Library.Phantom_Type

01:55:11 HOL-Word: theory HOL-Library.Boolean_Algebra

01:55:11 HOL-Word: theory HOL-Word.Bits

01:55:11 HOL-Word: theory HOL-Library.Bit

01:55:11 HOL-Word: theory HOL-Word.Misc_Numeric

01:55:11 HOL-Word: theory HOL-Word.Misc_Typedef

01:55:11 HOL-Word: theory HOL-Word.Bit_Representation

01:55:12 HOL-Word: theory HOL-Word.Bits_Bit

01:55:12 HOL-Word: theory HOL-Word.Word_Miscellaneous

01:55:12 HOL-Word: theory HOL-Word.Bits_Int

01:55:12 HOL-Word: theory HOL-Library.Cardinality

01:55:14 HOL-Word: theory HOL-Library.Numeral_Type

01:55:15 HOL-Word: theory HOL-Word.Bit_Comparison

01:55:15 HOL-Word: theory HOL-Word.Bool_List_Representation

01:55:16 HOL-Word: theory HOL-Library.Type_Length

01:55:16 HOL-Word: theory HOL-Word.Word

01:55:22 HOL-Word: theory HOL-Word.WordBitwise

01:55:41 Timing HOL-Word (8 threads, 12.932s elapsed time, 62.324s cpu time, 2.296s GC time, factor 4.82)

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

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

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

01:55:41 Finished HOL-Word (0:00:30 elapsed time, 0:01:33 cpu time, factor 3.01)

01:55:41 Building Ordinary_Differential_Equations ...

01:55:43 Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras

01:55:43 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order

01:55:43 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int

01:55:43 Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat

01:55:43 Ordinary_Differential_Equations: theory HOL-Word.Misc_Numeric

01:55:43 Ordinary_Differential_Equations: theory HOL-Library.Log_Nat

01:55:43 Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence

01:55:43 Ordinary_Differential_Equations: theory HOL-Word.Bits

01:55:44 Ordinary_Differential_Equations: theory HOL-Word.Bit_Representation

01:55:44 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat

01:55:44 Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities

01:55:44 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator

01:55:44 Ordinary_Differential_Equations: theory Triangle.Angles

01:55:44 Ordinary_Differential_Equations: theory List-Index.List_Index

01:55:44 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral

01:55:44 Ordinary_Differential_Equations: theory Triangle.Triangle

01:55:45 Ordinary_Differential_Equations: theory HOL-Word.Bits_Int

01:55:47 Ordinary_Differential_Equations: theory HOL-Word.Bool_List_Representation

01:55:51 Ordinary_Differential_Equations: theory HOL-Library.Float

01:55:55 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds

01:55:55 Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space

01:56:00 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation

01:56:02 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities

01:56:07 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones

01:56:07 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem

01:56:07 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor

01:56:10 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative

01:56:11 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow

01:56:16 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map

01:56:16 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution

01:56:17 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE

01:56:21 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis

01:57:08 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex

01:57:10 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis

01:58:33 Timing Ordinary_Differential_Equations (8 threads, 130.589s elapsed time, 589.276s cpu time, 20.092s GC time, factor 4.51)

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

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

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

01:58:33 Finished Ordinary_Differential_Equations (0:02:50 elapsed time, 0:11:02 cpu time, factor 3.88)

01:58:33 Building Automatic_Refinement ...

01:58:34 Automatic_Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1

01:58:34 Automatic_Refinement: theory HOL-Library.Infinite_Set

01:58:34 Automatic_Refinement: theory HOL-Library.Option_ord

01:58:34 Automatic_Refinement: theory Automatic_Refinement.Foldi

01:58:34 Automatic_Refinement: theory Automatic_Refinement.Prio_List

01:58:34 Automatic_Refinement: theory HOL-Library.Cancellation

01:58:34 Automatic_Refinement: theory HOL-Eisbach.Eisbach

01:58:34 Automatic_Refinement: theory Automatic_Refinement.Mk_Term_Antiquot

01:58:34 Automatic_Refinement: theory Automatic_Refinement.Mpat_Antiquot

01:58:35 Automatic_Refinement: theory Automatic_Refinement.Refine_Util

01:58:35 Automatic_Refinement: theory HOL-Library.Omega_Words_Fun

01:58:35 Automatic_Refinement: theory HOL-Library.Multiset

01:58:36 Automatic_Refinement: theory Automatic_Refinement.Anti_Unification

01:58:36 Automatic_Refinement: theory Automatic_Refinement.Attr_Comb

01:58:36 Automatic_Refinement: theory Automatic_Refinement.Indep_Vars

01:58:36 Automatic_Refinement: theory Automatic_Refinement.Mk_Record_Simp

01:58:36 Automatic_Refinement: theory Automatic_Refinement.Named_Sorted_Thms

01:58:36 Automatic_Refinement: theory Automatic_Refinement.Tagged_Solver

01:58:36 Automatic_Refinement: theory Automatic_Refinement.Select_Solve

01:58:42 Automatic_Refinement: theory HOL-ex.Quicksort

01:58:43 Automatic_Refinement: theory Automatic_Refinement.Misc

01:58:50 Automatic_Refinement: theory Automatic_Refinement.Digraph_Basic

01:58:51 Automatic_Refinement: theory Automatic_Refinement.Refine_Lib

01:58:56 Automatic_Refinement: theory Automatic_Refinement.Param_Chapter

01:58:56 Automatic_Refinement: theory Automatic_Refinement.Relators

01:58:57 Automatic_Refinement: theory Automatic_Refinement.Param_Tool

01:58:58 Automatic_Refinement: theory Automatic_Refinement.Param_HOL

01:58:59 Automatic_Refinement: theory Automatic_Refinement.Parametricity

01:58:59 Automatic_Refinement: theory Automatic_Refinement.Autoref_Data

01:58:59 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tagging

01:58:59 Automatic_Refinement: theory Automatic_Refinement.Autoref_Phases

01:58:59 Automatic_Refinement: theory Automatic_Refinement.Autoref_Id_Ops

01:59:00 Automatic_Refinement: theory Automatic_Refinement.Autoref_Fix_Rel

01:59:01 Automatic_Refinement: theory Automatic_Refinement.Autoref_Translate

01:59:01 Automatic_Refinement: theory Automatic_Refinement.Autoref_Relator_Interface

01:59:01 Automatic_Refinement: theory Automatic_Refinement.Autoref_Gen_Algo

01:59:01 Automatic_Refinement: theory Automatic_Refinement.Autoref_Chapter

01:59:01 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tool

01:59:02 Automatic_Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL

01:59:06 Automatic_Refinement: theory Automatic_Refinement.Automatic_Refinement

01:59:23 Timing Automatic_Refinement (8 threads, 32.045s elapsed time, 108.936s cpu time, 4.384s GC time, factor 3.40)

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

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

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

01:59:23 Finished Automatic_Refinement (0:00:49 elapsed time, 0:02:20 cpu time, factor 2.82)

01:59:23 Building Refine_Monadic ...

01:59:25 Refine_Monadic: theory HOL-Library.Adhoc_Overloading

01:59:25 Refine_Monadic: theory HOL-Library.Bit

01:59:25 Refine_Monadic: theory HOL-Library.Phantom_Type

01:59:25 Refine_Monadic: theory HOL-Library.Boolean_Algebra

01:59:25 Refine_Monadic: theory HOL-Word.Bits

01:59:25 Refine_Monadic: theory HOL-Library.While_Combinator

01:59:25 Refine_Monadic: theory HOL-Word.Misc_Numeric

01:59:25 Refine_Monadic: theory HOL-Word.Misc_Typedef

01:59:25 Refine_Monadic: theory HOL-Word.Bit_Representation

01:59:25 Refine_Monadic: theory HOL-Library.Monad_Syntax

01:59:25 Refine_Monadic: theory Refine_Monadic.Example_Chapter

01:59:25 Refine_Monadic: theory Refine_Monadic.Refine_Chapter

01:59:25 Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover

01:59:26 Refine_Monadic: theory Refine_Monadic.Refine_Misc

01:59:26 Refine_Monadic: theory HOL-Word.Bits_Bit

01:59:26 Refine_Monadic: theory HOL-Word.Word_Miscellaneous

01:59:26 Refine_Monadic: theory HOL-Word.Bits_Int

01:59:27 Refine_Monadic: theory HOL-Library.Cardinality

01:59:27 Refine_Monadic: theory Refine_Monadic.RefineG_Domain

01:59:27 Refine_Monadic: theory Refine_Monadic.RefineG_Transfer

01:59:28 Refine_Monadic: theory Refine_Monadic.RefineG_Assert

01:59:28 Refine_Monadic: theory Refine_Monadic.RefineG_Recursion

01:59:28 Refine_Monadic: theory HOL-Library.Numeral_Type

01:59:29 Refine_Monadic: theory HOL-Word.Bool_List_Representation

01:59:29 Refine_Monadic: theory Refine_Monadic.RefineG_While

01:59:29 Refine_Monadic: theory Refine_Monadic.Refine_Basic

01:59:30 Refine_Monadic: theory Refine_Monadic.Refine_Det

01:59:30 Refine_Monadic: theory HOL-Library.Type_Length

01:59:30 Refine_Monadic: theory HOL-Word.Word

01:59:33 Refine_Monadic: theory Refine_Monadic.Refine_Heuristics

01:59:33 Refine_Monadic: theory Refine_Monadic.Refine_Leof

01:59:33 Refine_Monadic: theory Refine_Monadic.Refine_Pfun

01:59:34 Refine_Monadic: theory Refine_Monadic.Refine_More_Comb

01:59:34 Refine_Monadic: theory Refine_Monadic.Refine_While

01:59:36 Refine_Monadic: theory Refine_Monadic.Refine_Transfer

01:59:36 Refine_Monadic: theory Refine_Monadic.Autoref_Monadic

01:59:36 Refine_Monadic: theory Refine_Monadic.Refine_Automation

01:59:37 Refine_Monadic: theory Refine_Monadic.Refine_Foreach

01:59:40 Refine_Monadic: theory Refine_Monadic.Refine_Monadic

01:59:41 Refine_Monadic: theory Refine_Monadic.Breadth_First_Search

01:59:42 Refine_Monadic: theory Refine_Monadic.WordRefine

01:59:43 Refine_Monadic: theory Refine_Monadic.Examples

02:00:20 Timing Refine_Monadic (8 threads, 30.034s elapsed time, 148.144s cpu time, 7.116s GC time, factor 4.93)

02:00:20 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Refine_Monadic

02:00:20 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Refine_Monadic/document.pdf

02:00:20 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Refine_Monadic/outline.pdf

02:00:20 Finished Refine_Monadic (0:00:55 elapsed time, 0:03:13 cpu time, factor 3.50)

02:00:20 Building AWN ...

02:00:21 AWN: theory AWN.Lib

02:00:21 AWN: theory AWN.TransitionSystems

02:00:21 AWN: theory AWN.AWN

02:00:21 AWN: theory AWN.Invariants

02:00:22 AWN: theory AWN.OInvariants

02:00:36 AWN: theory AWN.AWN_SOS

02:00:36 AWN: theory AWN.AWN_Cterms

02:00:36 AWN: theory AWN.OAWN_SOS

02:00:40 AWN: theory AWN.AWN_Labels

02:00:42 AWN: theory AWN.Pnet

02:00:42 AWN: theory AWN.Inv_Cterms

02:00:42 AWN: theory AWN.AWN_Invariants

02:00:43 AWN: theory AWN.Closed

02:00:43 AWN: theory AWN.AWN_SOS_Labels

02:00:44 AWN: theory AWN.Qmsg

02:00:45 AWN: theory AWN.OAWN_Invariants

02:00:45 AWN: theory AWN.OAWN_SOS_Labels

02:00:45 AWN: theory AWN.ONode_Lifting

02:00:45 AWN: theory AWN.OPnet

02:00:46 AWN: theory AWN.OPnet_Lifting

02:00:46 AWN: theory AWN.OClosed_Lifting

02:00:47 AWN: theory AWN.OClosed_Transfer

02:00:47 AWN: theory AWN.OAWN_Convert

02:00:47 AWN: theory AWN.Qmsg_Lifting

02:00:48 AWN: theory AWN.AWN_Main

02:00:48 AWN: theory AWN.Toy

02:01:03 AWN: theory AWN.AWN_Term_Graph

02:02:02 Timing AWN (8 threads, 47.037s elapsed time, 223.520s cpu time, 8.004s GC time, factor 4.75)

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

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

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

02:02:02 Finished AWN (0:01:41 elapsed time, 0:05:05 cpu time, factor 3.01)

02:02:02 Building Deriving ...

02:02:04 Deriving: theory Deriving.Comparator

02:02:04 Deriving: theory Deriving.Derive_Manager

02:02:04 Deriving: theory HOL-Word.Misc_Numeric

02:02:04 Deriving: theory HOL-Word.Bits

02:02:04 Deriving: theory Deriving.Generator_Aux

02:02:04 Deriving: theory HOL-Word.Misc_Typedef

02:02:04 Deriving: theory HOL-Word.Bit_Representation

02:02:04 Deriving: theory HOL-Word.Word_Miscellaneous

02:02:04 Deriving: theory Deriving.Countable_Generator

02:02:04 Deriving: theory HOL-Word.Bits_Bit

02:02:04 Deriving: theory Deriving.Equality_Generator

02:02:05 Deriving: theory Deriving.Equality_Instances

02:02:05 Deriving: theory HOL-Word.Bits_Int

02:02:05 Deriving: theory Deriving.Compare

02:02:05 Deriving: theory Deriving.Comparator_Generator

02:02:06 Deriving: theory Deriving.RBT_Comparator_Impl

02:02:06 Deriving: theory Deriving.RBT_Compare_Order_Impl

02:02:07 Deriving: theory Deriving.Compare_Generator

02:02:07 Deriving: theory Deriving.Compare_Instances

02:02:07 Deriving: theory Deriving.Compare_Rat

02:02:07 Deriving: theory Deriving.Compare_Real

02:02:07 Deriving: theory HOL-Word.Bool_List_Representation

02:02:08 Deriving: theory Deriving.Compare_Order_Instances

02:02:08 Deriving: theory Native_Word.More_Bits_Int

02:02:08 Deriving: theory HOL-Word.Word

02:02:11 Deriving: theory Native_Word.Bits_Integer

02:02:16 Deriving: theory Native_Word.Word_Misc

02:02:26 Deriving: theory Native_Word.Uint32

02:02:28 Deriving: theory Collections.HashCode

02:02:29 Deriving: theory Deriving.Hash_Generator

02:02:30 Deriving: theory Deriving.Hash_Instances

02:02:30 Deriving: theory Deriving.Derive

02:02:31 Deriving: theory Deriving.Derive_Examples

02:03:16 Timing Deriving (8 threads, 42.766s elapsed time, 120.460s cpu time, 5.516s GC time, factor 2.82)

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

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

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

02:03:16 Finished Deriving (0:01:13 elapsed time, 0:03:31 cpu time, factor 2.88)

02:03:16 Building ConcurrentIMP ...

02:03:18 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred

02:03:18 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang

02:03:30 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg

02:03:32 ConcurrentIMP: theory ConcurrentIMP.CIMP

02:03:33 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer_ex

02:03:33 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer_ex

02:04:03 Timing ConcurrentIMP (8 threads, 20.613s elapsed time, 49.796s cpu time, 3.000s GC time, factor 2.42)

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

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

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

02:04:03 Finished ConcurrentIMP (0:00:45 elapsed time, 0:01:35 cpu time, factor 2.08)

02:04:03 Building HOL-ODE ...

02:04:05 Timing HOL-ODE (8 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

02:04:05 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE

02:04:05 Finished HOL-ODE (0:00:02 elapsed time)

02:04:05 Building HOL-ODE-Refinement ...

02:04:08 HOL-ODE-Refinement: theory HOL-Eisbach.Eisbach

02:04:08 HOL-ODE-Refinement: theory HOL-Library.Adhoc_Overloading

02:04:08 HOL-ODE-Refinement: theory Automatic_Refinement.Foldi

02:04:08 HOL-ODE-Refinement: theory Automatic_Refinement.Prio_List

02:04:08 HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1

02:04:08 HOL-ODE-Refinement: theory Deriving.Comparator

02:04:08 HOL-ODE-Refinement: theory Deriving.Derive_Manager

02:04:08 HOL-ODE-Refinement: theory Deriving.Generator_Aux

02:04:08 HOL-ODE-Refinement: theory Automatic_Refinement.Mk_Term_Antiquot

02:04:08 HOL-ODE-Refinement: theory Automatic_Refinement.Mpat_Antiquot

02:04:08 HOL-ODE-Refinement: theory HOL-Library.AList

02:04:08 HOL-ODE-Refinement: theory HOL-Library.Bit

02:04:08 HOL-ODE-Refinement: theory HOL-Library.Boolean_Algebra

02:04:08 HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Util

02:04:08 HOL-ODE-Refinement: theory HOL-Library.Permutation

02:04:08 HOL-ODE-Refinement: theory Deriving.Equality_Generator

02:04:09 HOL-ODE-Refinement: theory HOL-ex.Quicksort

02:04:09 HOL-ODE-Refinement: theory HOL-Library.Char_ord

02:04:09 HOL-ODE-Refinement: theory HOL-Library.Omega_Words_Fun

02:04:09 HOL-ODE-Refinement: theory HOL-Library.Code_Char

02:04:09 HOL-ODE-Refinement: theory Deriving.Equality_Instances

02:04:09 HOL-ODE-Refinement: theory HOL-Library.Mapping

02:04:09 HOL-ODE-Refinement: theory HOL-Library.Monad_Syntax

02:04:09 HOL-ODE-Refinement: theory Automatic_Refinement.Anti_Unification

02:04:09 HOL-ODE-Refinement: theory Automatic_Refinement.Attr_Comb

02:04:09 HOL-ODE-Refinement: theory Automatic_Refinement.Named_Sorted_Thms

02:04:09 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Data

02:04:10 HOL-ODE-Refinement: theory Automatic_Refinement.Indep_Vars

02:04:10 HOL-ODE-Refinement: theory Automatic_Refinement.Mk_Record_Simp

02:04:10 HOL-ODE-Refinement: theory Automatic_Refinement.Tagged_Solver

02:04:10 HOL-ODE-Refinement: theory Automatic_Refinement.Select_Solve

02:04:10 HOL-ODE-Refinement: theory HOL-Library.Option_ord

02:04:10 HOL-ODE-Refinement: theory Deriving.Compare

02:04:10 HOL-ODE-Refinement: theory Deriving.Comparator_Generator

02:04:10 HOL-ODE-Refinement: theory HOL-Library.Type_Length

02:04:10 HOL-ODE-Refinement: theory HOL-Library.RBT_Impl

02:04:10 HOL-ODE-Refinement: theory HOL-Library.While_Combinator

02:04:10 HOL-ODE-Refinement: theory HOL-Word.Bits_Bit

02:04:10 HOL-ODE-Refinement: theory Automatic_Refinement.Misc

02:04:10 HOL-ODE-Refinement: theory Native_Word.More_Bits_Int

02:04:11 HOL-ODE-Refinement: theory HOL-Word.Word_Miscellaneous

02:04:11 HOL-ODE-Refinement: theory HOL-Word.Misc_Typedef

02:04:11 HOL-ODE-Refinement: theory Deriving.Countable_Generator

02:04:11 HOL-ODE-Refinement: theory Affine_Arithmetic.Optimize_Integer

02:04:11 HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise

02:04:11 HOL-ODE-Refinement: theory Deriving.Compare_Generator

02:04:11 HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Form

02:04:11 HOL-ODE-Refinement: theory HOL-Word.Word

02:04:11 HOL-ODE-Refinement: theory Affine_Arithmetic.Optimize_Float

02:04:11 HOL-ODE-Refinement: theory Deriving.Compare_Instances

02:04:12 HOL-ODE-Refinement: theory Affine_Arithmetic.Float_Real

02:04:12 HOL-ODE-Refinement: theory Affine_Arithmetic.Floatarith_Expression

02:04:12 HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_Vector

02:04:12 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Chapter

02:04:12 HOL-ODE-Refinement: theory Show.Show

02:04:12 HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_2D_Strict

02:04:13 HOL-ODE-Refinement: theory Native_Word.Bits_Integer

02:04:14 HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary

02:04:14 HOL-ODE-Refinement: theory Affine_Arithmetic.Polygon

02:04:15 HOL-ODE-Refinement: theory Show.Show_Instances

02:04:17 HOL-ODE-Refinement: theory Affine_Arithmetic.Intersection

02:04:19 HOL-ODE-Refinement: theory Native_Word.Word_Misc

02:04:19 HOL-ODE-Refinement: theory Automatic_Refinement.Digraph_Basic

02:04:19 HOL-ODE-Refinement: theory Collections.SetIterator

02:04:20 HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Lib

02:04:21 HOL-ODE-Refinement: theory Collections.SetIteratorOperations

02:04:22 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Phases

02:04:22 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Tagging

02:04:22 HOL-ODE-Refinement: theory Automatic_Refinement.Relators

02:04:22 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Mono_Prover

02:04:24 HOL-ODE-Refinement: theory Automatic_Refinement.Param_Tool

02:04:24 HOL-ODE-Refinement: theory Automatic_Refinement.Param_HOL

02:04:26 HOL-ODE-Refinement: theory Automatic_Refinement.Parametricity

02:04:26 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Id_Ops

02:04:26 HOL-ODE-Refinement: theory Collections.Assoc_List

02:04:26 HOL-ODE-Refinement: theory Collections.Proper_Iterator

02:04:26 HOL-ODE-Refinement: theory Collections.SetIteratorGA

02:04:27 HOL-ODE-Refinement: theory Collections.Diff_Array

02:04:27 HOL-ODE-Refinement: theory Collections.It_to_It

02:04:28 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Fix_Rel

02:04:29 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Translate

02:04:29 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Relator_Interface

02:04:29 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Gen_Algo

02:04:29 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Tool

02:04:30 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL

02:04:34 HOL-ODE-Refinement: theory Native_Word.Code_Target_Bits_Int

02:04:34 HOL-ODE-Refinement: theory Native_Word.Uint

02:04:34 HOL-ODE-Refinement: theory Collections.Code_Target_ICF

02:04:34 HOL-ODE-Refinement: theory Native_Word.Uint32

02:04:36 HOL-ODE-Refinement: theory Automatic_Refinement.Automatic_Refinement

02:04:36 HOL-ODE-Refinement: theory Collections.Intf_Comp

02:04:36 HOL-ODE-Refinement: theory Collections.Idx_Iterator

02:04:36 HOL-ODE-Refinement: theory Collections.Impl_Array_Stack

02:04:36 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Misc

02:04:37 HOL-ODE-Refinement: theory Collections.HashCode

02:04:37 HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Domain

02:04:37 HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Transfer

02:04:37 HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Assert

02:04:38 HOL-ODE-Refinement: theory Collections.Intf_Hash

02:04:38 HOL-ODE-Refinement: theory Deriving.Hash_Generator

02:04:38 HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Recursion

02:04:39 HOL-ODE-Refinement: theory Refine_Monadic.RefineG_While

02:04:39 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Basic

02:04:39 HOL-ODE-Refinement: theory Collections.Gen_Hash

02:04:39 HOL-ODE-Refinement: theory Deriving.Hash_Instances

02:04:39 HOL-ODE-Refinement: theory Deriving.Derive

02:04:40 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Det

02:04:44 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Heuristics

02:04:44 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Leof

02:04:44 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Pfun

02:04:44 HOL-ODE-Refinement: theory Refine_Monadic.Refine_More_Comb

02:04:45 HOL-ODE-Refinement: theory Refine_Monadic.Refine_While

02:04:47 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Transfer

02:04:48 HOL-ODE-Refinement: theory Refine_Monadic.Autoref_Monadic

02:04:48 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Automation

02:04:48 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Foreach

02:04:52 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Monadic

02:04:54 HOL-ODE-Refinement: theory Collections.Gen_Iterator

02:04:54 HOL-ODE-Refinement: theory Collections.Intf_Map

02:04:54 HOL-ODE-Refinement: theory Collections.Intf_Set

02:04:55 HOL-ODE-Refinement: theory Collections.Impl_Cfun_Set

02:04:55 HOL-ODE-Refinement: theory Collections.Iterator

02:04:56 HOL-ODE-Refinement: theory Collections.Array_Iterator

02:04:56 HOL-ODE-Refinement: theory Collections.Gen_Map

02:04:57 HOL-ODE-Refinement: theory Collections.Gen_Map2Set

02:04:57 HOL-ODE-Refinement: theory Collections.Gen_Set

02:04:57 HOL-ODE-Refinement: theory Collections.Impl_Bit_Set

02:04:57 HOL-ODE-Refinement: theory Collections.Impl_List_Set

02:04:58 HOL-ODE-Refinement: theory Collections.Impl_Array_Map

02:04:58 HOL-ODE-Refinement: theory Collections.Impl_List_Map

02:04:58 HOL-ODE-Refinement: theory Collections.Impl_Uv_Set

02:05:00 HOL-ODE-Refinement: theory Collections.Impl_Array_Hash_Map

02:05:06 HOL-ODE-Refinement: theory HOL-Library.RBT

02:05:06 HOL-ODE-Refinement: theory Collections.RBT_add

02:05:07 HOL-ODE-Refinement: theory HOL-Library.RBT_Mapping

02:05:08 HOL-ODE-Refinement: theory Affine_Arithmetic.Straight_Line_Program

02:05:09 HOL-ODE-Refinement: theory Collections.Impl_RBT_Map

02:05:23 HOL-ODE-Refinement: theory HOL-ODE-Refinement.GenCF_No_Comp

02:05:24 HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Approximation

02:05:33 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Dflt_No_Comp

02:05:33 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Misc

02:05:42 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Folds

02:05:42 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_String

02:05:42 HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Code

02:05:42 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Weak_Set

02:05:48 HOL-ODE-Refinement: theory Affine_Arithmetic.Print

02:05:56 HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Affine_Approximation

02:05:56 HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Ineqs

02:05:56 HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Inter

02:07:22 HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Arithmetic

02:10:13 Timing HOL-ODE-Refinement (8 threads, 296.234s elapsed time, 1643.644s cpu time, 210.544s GC time, factor 5.55)

02:10:13 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Refinement

02:10:13 Finished HOL-ODE-Refinement (0:06:05 elapsed time, 0:31:06 cpu time, factor 5.11)

02:10:13 Building HOL-ODE-Numerics ...

02:10:16 HOL-ODE-Numerics: theory Collections.ICF_Tools

02:10:16 HOL-ODE-Numerics: theory HOL-Library.Parallel

02:10:16 HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets

02:10:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method

02:10:16 HOL-ODE-Numerics: theory Collections.Ord_Code_Preproc

02:10:17 HOL-ODE-Numerics: theory Collections.Locale_Code

02:10:18 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta

02:10:23 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List

02:10:32 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector

02:10:36 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics

02:13:10 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis

02:31:09 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform

02:33:07 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities

02:35:12 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics

02:37:07 Timing HOL-ODE-Numerics (8 threads, 1501.528s elapsed time, 3263.356s cpu time, 316.956s GC time, factor 2.17)

02:37:07 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Numerics

02:37:07 Finished HOL-ODE-Numerics (0:26:51 elapsed time, 0:58:15 cpu time, factor 2.17)

02:37:07 Building Lorenz_Approximation ...

02:37:10 Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements

02:37:15 Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse

02:37:53 Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation

02:43:13 Timing Lorenz_Approximation (8 threads, 317.836s elapsed time, 662.952s cpu time, 60.672s GC time, factor 2.09)

02:43:13 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Lorenz_Approximation

02:43:13 Finished Lorenz_Approximation (0:06:04 elapsed time, 0:12:34 cpu time, factor 2.07)

02:43:13 Building Word_Lib ...

02:43:14 Word_Lib: theory HOL-Library.Sublist

02:43:14 Word_Lib: theory Word_Lib.Signed_Words

02:43:14 Word_Lib: theory Word_Lib.Hex_Words

02:43:14 Word_Lib: theory Word_Lib.HOL_Lemmas

02:43:14 Word_Lib: theory Word_Lib.Enumeration

02:43:14 Word_Lib: theory Word_Lib.More_Divides

02:43:14 Word_Lib: theory Word_Lib.Norm_Words

02:43:14 Word_Lib: theory Word_Lib.WordBitwise_Signed

02:43:15 Word_Lib: theory Word_Lib.Word_Syntax

02:43:15 Word_Lib: theory Word_Lib.Word_Lib

02:43:17 Word_Lib: theory Word_Lib.Word_Enum

02:43:17 Word_Lib: theory Word_Lib.Aligned

02:43:17 Word_Lib: theory HOL-Library.Prefix_Order

02:43:17 Word_Lib: theory Word_Lib.Word_Setup_32

02:43:17 Word_Lib: theory Word_Lib.Word_Setup_64

02:43:18 Word_Lib: theory Word_Lib.Word_Lemmas

02:43:24 Word_Lib: theory Word_Lib.Word_Lemmas_32

02:43:24 Word_Lib: theory Word_Lib.Word_Lemmas_64

02:44:43 Timing Word_Lib (8 threads, 71.834s elapsed time, 179.172s cpu time, 4.700s GC time, factor 2.49)

02:44:43 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib

02:44:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf

02:44:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf

02:44:43 Finished Word_Lib (0:01:29 elapsed time, 0:03:27 cpu time, factor 2.32)

02:44:43 Building IP_Addresses ...

02:44:44 IP_Addresses: theory HOL-Eisbach.Eisbach

02:44:44 IP_Addresses: theory HOL-Library.Cancellation

02:44:44 IP_Addresses: theory HOL-Library.Infinite_Set

02:44:44 IP_Addresses: theory HOL-Library.Option_ord

02:44:44 IP_Addresses: theory IP_Addresses.NumberWang_IPv6

02:44:44 IP_Addresses: theory IP_Addresses.Word_More

02:44:44 IP_Addresses: theory IP_Addresses.NumberWang_IPv4

02:44:45 IP_Addresses: theory HOL-Library.Multiset

02:44:52 IP_Addresses: theory HOL-ex.Quicksort

02:44:53 IP_Addresses: theory Automatic_Refinement.Misc

02:45:01 IP_Addresses: theory HOL-Library.Code_Abstract_Nat

02:45:01 IP_Addresses: theory HOL-Library.Product_Lexorder

02:45:01 IP_Addresses: theory IP_Addresses.Hs_Compat

02:45:01 IP_Addresses: theory IP_Addresses.Word_Next

02:45:01 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString

02:45:01 IP_Addresses: theory HOL-Library.Code_Target_Nat

02:45:01 IP_Addresses: theory IP_Addresses.WordInterval

02:45:01 IP_Addresses: theory IP_Addresses.Lib_List_toString

02:45:01 IP_Addresses: theory IP_Addresses.Lib_Word_toString

02:45:06 IP_Addresses: theory IP_Addresses.IP_Address

02:45:07 IP_Addresses: theory IP_Addresses.WordInterval_Sorted

02:45:12 IP_Addresses: theory IP_Addresses.IPv4

02:45:12 IP_Addresses: theory IP_Addresses.IPv6

02:45:12 IP_Addresses: theory IP_Addresses.Prefix_Match

02:45:13 IP_Addresses: theory IP_Addresses.CIDR_Split

02:47:03 IP_Addresses: theory IP_Addresses.IP_Address_Parser

02:47:03 IP_Addresses: theory IP_Addresses.IP_Address_toString

02:47:05 IP_Addresses: theory IP_Addresses.Prefix_Match_toString

02:50:38 Timing IP_Addresses (8 threads, 312.089s elapsed time, 903.964s cpu time, 57.728s GC time, factor 2.90)

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

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

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

02:50:38 Finished IP_Addresses (0:05:54 elapsed time, 0:16:36 cpu time, factor 2.81)

02:50:38 Building Simple_Firewall ...

02:50:40 Simple_Firewall: theory HOL-Library.Char_ord

02:50:40 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State

02:50:40 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString

02:50:40 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries

02:50:40 Simple_Firewall: theory Simple_Firewall.GroupF

02:50:40 Simple_Firewall: theory Simple_Firewall.List_Product_More

02:50:40 Simple_Firewall: theory Simple_Firewall.Option_Helpers

02:50:40 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString

02:50:40 Simple_Firewall: theory Simple_Firewall.Iface

02:50:41 Simple_Firewall: theory Simple_Firewall.L4_Protocol

02:50:46 Simple_Firewall: theory Simple_Firewall.Simple_Packet

02:50:46 Simple_Firewall: theory Simple_Firewall.Primitives_toString

02:50:49 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax

02:50:52 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString

02:50:52 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics

02:50:55 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw

02:50:55 Simple_Firewall: theory Simple_Firewall.Shadowed

02:50:55 Simple_Firewall: theory Simple_Firewall.Service_Matrix

02:51:32 Timing Simple_Firewall (8 threads, 24.885s elapsed time, 95.264s cpu time, 4.772s GC time, factor 3.83)

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

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

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

02:51:32 Finished Simple_Firewall (0:00:52 elapsed time, 0:02:31 cpu time, factor 2.88)

02:51:32 Building Routing ...

02:51:33 Routing: theory HOL-Library.Adhoc_Overloading

02:51:33 Routing: theory Routing.Linorder_Helper

02:51:34 Routing: theory HOL-Library.Monad_Syntax

02:51:35 Routing: theory Routing.Routing_Table

02:51:39 Routing: theory Routing.IpRoute_Parser

02:51:39 Routing: theory Routing.Linux_Router

02:52:03 Timing Routing (8 threads, 11.020s elapsed time, 33.572s cpu time, 1.120s GC time, factor 3.05)

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

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

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

02:52:03 Finished Routing (0:00:29 elapsed time, 0:01:04 cpu time, factor 2.18)

02:52:03 Building Iptables_Semantics ...

02:52:05 Iptables_Semantics: theory HOL-Library.Code_Target_Int

02:52:05 Iptables_Semantics: theory HOL-Library.LaTeXsugar

02:52:05 Iptables_Semantics: theory Native_Word.More_Bits_Int

02:52:05 Iptables_Semantics: theory HOL-Library.Code_Char

02:52:05 Iptables_Semantics: theory Iptables_Semantics.List_Misc

02:52:05 Iptables_Semantics: theory Iptables_Semantics.Negation_Type

02:52:07 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists

02:52:08 Iptables_Semantics: theory Native_Word.Bits_Integer

02:52:22 Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int

02:52:26 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors

02:52:26 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF

02:52:26 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev

02:52:26 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize

02:52:26 Iptables_Semantics: theory Iptables_Semantics.Ternary

02:52:26 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags

02:52:26 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State

02:52:26 Iptables_Semantics: theory Iptables_Semantics.IpAddresses

02:52:26 Iptables_Semantics: theory Iptables_Semantics.Word_Upto

02:52:26 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common

02:52:27 Iptables_Semantics: theory Iptables_Semantics.Ports

02:52:28 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet

02:52:30 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax

02:52:44 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary

02:52:44 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto

02:52:44 Iptables_Semantics: theory Iptables_Semantics.Semantics

02:52:47 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics

02:52:47 Iptables_Semantics: theory Iptables_Semantics.Matching

02:52:47 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful

02:52:47 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update

02:52:47 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding

02:52:48 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary

02:52:49 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs

02:52:50 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings

02:52:50 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action

02:52:50 Iptables_Semantics: theory Iptables_Semantics.Optimizing

02:52:51 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic

02:52:51 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches

02:52:52 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching

02:52:54 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization

02:52:57 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher

02:52:59 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold

02:52:59 Iptables_Semantics: theory Iptables_Semantics.Ipassmt

02:53:03 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt

02:53:56 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString

02:53:56 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas

02:53:56 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform

02:53:56 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics

02:53:57 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize

02:53:57 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize

02:53:57 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize

02:53:57 Iptables_Semantics: theory Iptables_Semantics.No_Spoof

02:53:57 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize

02:54:06 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace

02:54:11 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace

02:54:19 Iptables_Semantics: theory Iptables_Semantics.Transform

02:54:24 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract

02:54:26 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance

02:54:33 Iptables_Semantics: theory Iptables_Semantics.Code_Interface

02:54:34 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings

02:54:35 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings

02:54:36 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics

02:54:36 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings

02:54:43 Iptables_Semantics: theory Iptables_Semantics.Parser

02:54:43 Iptables_Semantics: theory Iptables_Semantics.Documentation

02:54:44 Iptables_Semantics: theory Iptables_Semantics.Code_haskell

02:56:12 Timing Iptables_Semantics (8 threads, 180.093s elapsed time, 708.020s cpu time, 62.368s GC time, factor 3.93)

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

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

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

02:56:12 Finished Iptables_Semantics (0:04:06 elapsed time, 0:14:49 cpu time, factor 3.60)

02:56:12 Building Iptables_Semantics_Examples ...

02:56:15 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall

02:56:15 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test

02:56:15 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example

02:56:15 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company

02:56:15 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com

02:56:15 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing

02:56:15 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof

02:56:15 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6

02:56:16 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test

02:56:22 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail

02:56:22 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples

02:56:23 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed

02:56:24 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation

03:01:19 Timing Iptables_Semantics_Examples (8 threads, 270.073s elapsed time, 1835.796s cpu time, 189.256s GC time, factor 6.80)

03:01:19 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples

03:01:19 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf

03:01:19 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf

03:01:19 Finished Iptables_Semantics_Examples (0:05:06 elapsed time, 0:31:45 cpu time, factor 6.23)

03:01:19 Building HOL-Algebra ...

03:01:21 HOL-Algebra: theory HOL-Algebra.Exponent

03:01:21 HOL-Algebra: theory HOL-Algebra.Congruence

03:01:22 HOL-Algebra: theory HOL-Algebra.Order

03:01:25 HOL-Algebra: theory HOL-Algebra.Lattice

03:01:26 HOL-Algebra: theory HOL-Algebra.Complete_Lattice

03:01:28 HOL-Algebra: theory HOL-Algebra.Galois_Connection

03:01:28 HOL-Algebra: theory HOL-Algebra.Group

03:01:30 HOL-Algebra: theory HOL-Algebra.Bij

03:01:30 HOL-Algebra: theory HOL-Algebra.Coset

03:01:30 HOL-Algebra: theory HOL-Algebra.FiniteProduct

03:01:31 HOL-Algebra: theory HOL-Algebra.Ring

03:01:32 HOL-Algebra: theory HOL-Algebra.Sylow

03:01:32 HOL-Algebra: theory HOL-Algebra.Divisibility

03:01:38 HOL-Algebra: theory HOL-Algebra.AbelCoset

03:01:38 HOL-Algebra: theory HOL-Algebra.Module

03:01:38 HOL-Algebra: theory HOL-Algebra.More_Group

03:01:38 HOL-Algebra: theory HOL-Algebra.More_Ring

03:01:38 HOL-Algebra: theory HOL-Algebra.More_Finite_Product

03:01:47 HOL-Algebra: theory HOL-Algebra.Ideal

03:01:54 HOL-Algebra: theory HOL-Algebra.RingHom

03:01:57 HOL-Algebra: theory HOL-Algebra.QuotRing

03:01:57 HOL-Algebra: theory HOL-Algebra.UnivPoly

03:01:58 HOL-Algebra: theory HOL-Algebra.IntRing

03:02:28 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group

03:03:42 Timing HOL-Algebra (8 threads, 75.686s elapsed time, 235.208s cpu time, 12.576s GC time, factor 3.11)

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

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

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

03:03:42 Finished HOL-Algebra (0:02:21 elapsed time, 0:05:29 cpu time, factor 2.32)

03:03:42 Building HOL-Number_Theory ...

03:03:44 HOL-Number_Theory: theory HOL-Number_Theory.Cong

03:03:44 HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers

03:03:44 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes

03:03:44 HOL-Number_Theory: theory HOL-Number_Theory.Fib

03:03:44 HOL-Number_Theory: theory HOL-Algebra.Congruence

03:03:46 HOL-Number_Theory: theory HOL-Algebra.Order

03:03:47 HOL-Number_Theory: theory HOL-Number_Theory.Totient

03:03:48 HOL-Number_Theory: theory HOL-Algebra.Lattice

03:03:50 HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice

03:03:52 HOL-Number_Theory: theory HOL-Algebra.Group

03:03:54 HOL-Number_Theory: theory HOL-Algebra.Coset

03:03:54 HOL-Number_Theory: theory HOL-Algebra.FiniteProduct

03:03:55 HOL-Number_Theory: theory HOL-Algebra.Ring

03:04:01 HOL-Number_Theory: theory HOL-Algebra.AbelCoset

03:04:02 HOL-Number_Theory: theory HOL-Algebra.Module

03:04:02 HOL-Number_Theory: theory HOL-Algebra.More_Group

03:04:02 HOL-Number_Theory: theory HOL-Algebra.More_Ring

03:04:03 HOL-Number_Theory: theory HOL-Algebra.More_Finite_Product

03:04:10 HOL-Number_Theory: theory HOL-Algebra.Ideal

03:04:17 HOL-Number_Theory: theory HOL-Algebra.RingHom

03:04:20 HOL-Number_Theory: theory HOL-Algebra.UnivPoly

03:04:51 HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group

03:04:58 HOL-Number_Theory: theory HOL-Number_Theory.Residues

03:05:03 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion

03:05:03 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington

03:05:03 HOL-Number_Theory: theory HOL-Number_Theory.Gauss

03:05:04 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity

03:05:04 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory

03:06:08 Timing HOL-Number_Theory (8 threads, 91.074s elapsed time, 297.168s cpu time, 13.088s GC time, factor 3.26)

03:06:08 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Number_Theory

03:06:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Number_Theory/document.pdf

03:06:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Number_Theory/outline.pdf

03:06:08 Finished HOL-Number_Theory (0:02:25 elapsed time, 0:06:17 cpu time, factor 2.59)

03:06:08 Running Iptables_Semantics_Examples_Big ...

03:06:11 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated

03:06:11 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small

03:06:11 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3

03:06:11 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall

03:06:11 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern

03:13:44 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large

06:28:09 Run out of store - interrupting threads

06:28:09 Failed to recover - exiting

06:28:09 Iptables_Semantics_Examples_Big FAILED

06:28:09 (see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.7.1_x86_64-linux/log/Iptables_Semantics_Examples_Big)

06:28:09 ((char list \<times> char list) list \<times>

06:28:09 (char list \<times> char list) list) \<times>

06:28:09 (char list \<times> char list) list \<times>

06:28:09 (char list \<times> char list) list"

06:28:09 "[''distinct: passed'', ''ipassmt_sanity_nowildcards: passed'',

06:28:09 ''ipassmt_sanity_defined (interfaces defined in the ruleset are also in ipassmt): passed'',

06:28:09 ''ipassmt_sanity_disjoint (no zone-spanning interfaces): fail: [(eth1.110,eth1.1024), (eth1.1024,eth1.110)]'',

06:28:09 ''ipassmt_sanity_disjoint excluding UNIV interfaces: fail: [(eth1.110,eth1.1024), (eth1.1024,eth1.110)]'',

06:28:09 ''ipassmt_sanity_complete: the following is not covered: {188.95.232.192 .. 188.95.232.223}'',

06:28:09 ''ipassmt_sanity_complete excluding UNIV interfaces: the following is not covered: {188.95.232.192 .. 188.95.232.223}'']"

06:28:09 :: "char list list"

06:28:09 "[''{0.0.0.0 .. 255.255.255.255}'']"

06:28:09 :: "char list list"

06:28:09 "[''{192.168.16.0 .. 192.168.16.255} u {192.168.134.0 .. 192.168.134.255}'',

06:28:09 ''{0.0.0.0 .. 127.0.0.0} u {127.0.0.2 .. 192.168.15.255} u {192.168.17.0 .. 192.168.133.255} u {192.168.135.0 .. 255.255.255.255}'',

06:28:09 ''127.0.0.1'']"

06:28:09 :: "char list list"

06:28:09 "()"

06:28:09 :: "unit"

06:28:09 Simplified term (3077.478 seconds)

06:28:09 checked sanity with sanity_wf_ruleset (2145.255 seconds)

06:28:09 Defining constant `net_fw_1_def'

06:28:09 Defining constant `net_fw_1_INPUT_default_policy_def'

06:28:09 Defining constant `net_fw_1_FORWARD_default_policy_def'

06:28:09 Defining constant `net_fw_1_OUTPUT_default_policy_def'

06:28:09 loading file /media/data/jenkins/workspace/isabelle-nightly-slow/afp/thys/Iptables_Semantics/Examples/TUM_Net_Firewall/iptables-save-2015-05-15_14-14-46_cheating

06:28:09 Loaded 4903 lines of the filter table

06:28:09 Parsed 90 chain declarations

06:28:09 Parsed 4813 rules

06:28:09 unfolding (this may take a while) ...

06:28:09 checked sanity with sanity_wf_ruleset (642.498 seconds)

06:28:09 Defining constant `net_fw_def'

06:28:09 Defining constant `net_fw_INPUT_default_policy_def'

06:28:09 Defining constant `net_fw_FORWARD_default_policy_def'

06:28:09 Defining constant `net_fw_OUTPUT_default_policy_def'

06:28:09 loading file /media/data/jenkins/workspace/isabelle-nightly-slow/afp/thys/Iptables_Semantics/Examples/IPPartEval/TUM_Net/iptables-save-2015-09-03_15-56-50

06:28:09 Loaded 5038 lines of the filter table

06:28:09 Parsed 92 chain declarations

06:28:09 Parsed 4946 rules

06:28:09 unfolding (this may take a while) ...

06:28:09 Running Flyspeck-Tame ...

06:28:10 Flyspeck-Tame: theory Flyspeck-Tame.ListAux

06:28:10 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order

06:28:10 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl

06:28:10 Flyspeck-Tame: theory HOL-Library.AList

06:28:10 Flyspeck-Tame: theory HOL-Library.While_Combinator

06:28:10 Flyspeck-Tame: theory HOL-Library.Code_Target_Int

06:28:10 Flyspeck-Tame: theory HOL-Library.IArray

06:28:10 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat

06:28:11 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso

06:28:11 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat

06:28:11 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral

06:28:12 Flyspeck-Tame: theory Flyspeck-Tame.Arch

06:28:12 Flyspeck-Tame: theory Flyspeck-Tame.Worklist

06:28:13 Flyspeck-Tame: theory Flyspeck-Tame.ListSum

06:28:13 Flyspeck-Tame: theory Flyspeck-Tame.Rotation

06:28:13 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax

06:28:13 Flyspeck-Tame: theory Flyspeck-Tame.Graph

06:28:13 Flyspeck-Tame: theory Flyspeck-Tame.Maps

06:28:14 Flyspeck-Tame: theory Trie.Trie

06:28:16 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision

06:28:17 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps

06:28:18 Flyspeck-Tame: theory Flyspeck-Tame.Tame

06:28:18 Flyspeck-Tame: theory Trie.Tries

06:28:18 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator

06:28:18 Flyspeck-Tame: theory Flyspeck-Tame.TameProps

06:28:19 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps

06:28:19 Flyspeck-Tame: theory Flyspeck-Tame.Plane

06:28:20 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps

06:28:20 Flyspeck-Tame: theory Flyspeck-Tame.Plane1

06:28:20 Flyspeck-Tame: theory Flyspeck-Tame.Generator

06:28:21 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum

06:28:28 Flyspeck-Tame: theory Flyspeck-Tame.Invariants

06:28:29 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux

06:28:30 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps

06:28:30 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps

06:28:30 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props

06:28:32 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound

06:28:32 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps

06:28:33 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps

06:28:33 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps

06:28:33 Flyspeck-Tame: theory Flyspeck-Tame.ArchComp

06:28:33 Flyspeck-Tame: theory Flyspeck-Tame.Completeness

14:46:47 Timing Flyspeck-Tame (8 threads, 29901.064s elapsed time, 46026.416s cpu time, 1647.824s GC time, factor 1.54)

14:46:47 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame

14:46:47 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf

14:46:47 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf

14:46:47 Finished Flyspeck-Tame (8:18:31 elapsed time, 12:47:20 cpu time, factor 1.54)

14:46:47 Running AODV ...

14:46:49 AODV: theory AODV.Aodv_Basic

14:46:51 AODV: theory AODV.A_Norreqid

14:46:51 AODV: theory AODV.Aodv_Data

14:46:51 AODV: theory AODV.Aodv_Message

14:46:51 AODV: theory AODV.B_Fwdrreps

14:46:51 AODV: theory AODV.E_All_ABCD

14:46:51 AODV: theory AODV.D_Fwdrreqs

14:46:51 AODV: theory AODV.C_Gtobcast

14:46:51 AODV: theory AODV.A_Aodv_Data

14:46:51 AODV: theory AODV.A_Aodv_Message

14:46:51 AODV: theory AODV.B_Aodv_Data

14:46:51 AODV: theory AODV.B_Aodv_Message

14:46:51 AODV: theory AODV.D_Aodv_Data

14:46:51 AODV: theory AODV.C_Aodv_Data

14:46:53 AODV: theory AODV.C_Fresher

14:46:53 AODV: theory AODV.C_Aodv_Message

14:46:53 AODV: theory AODV.Fresher

14:46:54 AODV: theory AODV.A_Fresher

14:46:54 AODV: theory AODV.B_Fresher

14:46:54 AODV: theory AODV.D_Fresher

14:46:54 AODV: theory AODV.D_Aodv_Message

14:46:54 AODV: theory AODV.E_Aodv_Data

14:46:54 AODV: theory AODV.E_Aodv_Message

14:46:54 AODV: theory AODV.A_Aodv

14:46:55 AODV: theory AODV.Aodv

14:46:55 AODV: theory AODV.B_Aodv

14:46:55 AODV: theory AODV.E_Fresher

14:46:55 AODV: theory AODV.C_Aodv

14:46:56 AODV: theory AODV.D_Aodv

14:46:56 AODV: theory AODV.E_Aodv

14:47:58 AODV: theory AODV.Aodv_Predicates

14:47:58 AODV: theory AODV.OAodv

14:47:58 AODV: theory AODV.Loop_Freedom

14:47:59 AODV: theory AODV.Quality_Increases

14:47:59 AODV: theory AODV.Seq_Invariants

14:47:59 AODV: theory AODV.Global_Invariants

14:48:00 AODV: theory AODV.Aodv_Loop_Freedom

14:48:07 AODV: theory AODV.B_Aodv_Predicates

14:48:07 AODV: theory AODV.B_Loop_Freedom

14:48:08 AODV: theory AODV.B_Quality_Increases

14:48:08 AODV: theory AODV.B_Seq_Invariants

14:48:08 AODV: theory AODV.B_OAodv

14:48:09 AODV: theory AODV.B_Global_Invariants

14:48:10 AODV: theory AODV.B_Aodv_Loop_Freedom

14:48:18 AODV: theory AODV.C_Aodv_Predicates

14:48:18 AODV: theory AODV.C_OAodv

14:48:18 AODV: theory AODV.C_Loop_Freedom

14:48:18 AODV: theory AODV.C_Quality_Increases

14:48:18 AODV: theory AODV.C_Seq_Invariants

14:48:19 AODV: theory AODV.A_Aodv_Predicates

14:48:19 AODV: theory AODV.A_OAodv

14:48:19 AODV: theory AODV.C_Global_Invariants

14:48:19 AODV: theory AODV.A_Loop_Freedom

14:48:19 AODV: theory AODV.A_Quality_Increases

14:48:19 AODV: theory AODV.A_Seq_Invariants

14:48:20 AODV: theory AODV.E_Aodv_Predicates

14:48:20 AODV: theory AODV.E_OAodv

14:48:20 AODV: theory AODV.E_Loop_Freedom

14:48:20 AODV: theory AODV.E_Quality_Increases

14:48:20 AODV: theory AODV.E_Seq_Invariants

14:48:20 AODV: theory AODV.A_Global_Invariants

14:48:20 AODV: theory AODV.C_Aodv_Loop_Freedom

14:48:21 AODV: theory AODV.E_Global_Invariants

14:48:22 AODV: theory AODV.A_Aodv_Loop_Freedom

14:48:22 AODV: theory AODV.E_Aodv_Loop_Freedom

14:48:32 AODV: theory AODV.D_Aodv_Predicates

14:48:32 AODV: theory AODV.D_OAodv

14:48:32 AODV: theory AODV.D_Loop_Freedom

14:48:33 AODV: theory AODV.D_Quality_Increases

14:48:33 AODV: theory AODV.D_Seq_Invariants

14:48:34 AODV: theory AODV.D_Global_Invariants

14:48:35 AODV: theory AODV.D_Aodv_Loop_Freedom

14:48:41 AODV: theory AODV.All

17:15:47 Timing AODV (8 threads, 8923.910s elapsed time, 44752.256s cpu time, 4116.604s GC time, factor 5.01)

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

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

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

17:15:47 Finished AODV (2:28:57 elapsed time, 12:26:11 cpu time, factor 5.01)

17:15:47 Running ConcurrentGC ...

17:15:49 ConcurrentGC: theory ConcurrentGC.Model

17:16:08 ConcurrentGC: theory ConcurrentGC.Tactics

17:16:16 ConcurrentGC: theory ConcurrentGC.Proofs_basis

17:16:19 ConcurrentGC: theory ConcurrentGC.TSO

17:16:33 ConcurrentGC: theory ConcurrentGC.Handshakes

17:19:09 ConcurrentGC: theory ConcurrentGC.MarkObject

17:21:53 ConcurrentGC: theory ConcurrentGC.StrongTricolour

17:22:59 ConcurrentGC: theory ConcurrentGC.Proofs

17:23:00 ConcurrentGC: theory ConcurrentGC.Concrete_heap

17:23:01 ConcurrentGC: theory ConcurrentGC.Concrete

19:23:33 Timing ConcurrentGC (8 threads, 7658.812s elapsed time, 26003.264s cpu time, 1775.076s GC time, factor 3.40)

19:23:33 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC

19:23:33 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf

19:23:33 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf

19:23:33 Finished ConcurrentGC (2:07:43 elapsed time, 7:13:29 cpu time, factor 3.39)

19:23:33 Running JinjaThreads ...

19:23:36 JinjaThreads: theory HOL-Library.Adhoc_Overloading

19:23:36 JinjaThreads: theory HOL-Eisbach.Eisbach

19:23:36 JinjaThreads: theory HOL-Library.Lattice_Syntax

19:23:37 JinjaThreads: theory Automatic_Refinement.Foldi

19:23:37 JinjaThreads: theory Automatic_Refinement.Prio_List

19:23:37 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1

19:23:37 JinjaThreads: theory Collections.ICF_Tools

19:23:37 JinjaThreads: theory Finger-Trees.FingerTree

19:23:37 JinjaThreads: theory HOL-Library.AList

19:23:37 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot

19:23:37 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot

19:23:37 JinjaThreads: theory HOL-Library.Bit

19:23:37 JinjaThreads: theory HOL-Library.Boolean_Algebra

19:23:37 JinjaThreads: theory Collections.Ord_Code_Preproc

19:23:37 JinjaThreads: theory Automatic_Refinement.Refine_Util

19:23:37 JinjaThreads: theory Collections.Locale_Code

19:23:37 JinjaThreads: theory Collections.Record_Intf

19:23:37 JinjaThreads: theory HOL-Library.Cancellation

19:23:37 JinjaThreads: theory HOL-Library.Char_ord

19:23:37 JinjaThreads: theory HOL-Library.Code_Abstract_Nat

19:23:37 JinjaThreads: theory HOL-Library.Code_Target_Nat

19:23:37 JinjaThreads: theory HOL-Library.Code_Target_Int

19:23:38 JinjaThreads: theory HOL-Library.Code_Char

19:23:38 JinjaThreads: theory HOL-Library.Complete_Partial_Order2

19:23:38 JinjaThreads: theory HOL-Library.Dlist

19:23:38 JinjaThreads: theory Automatic_Refinement.Anti_Unification

19:23:38 JinjaThreads: theory Automatic_Refinement.Attr_Comb

19:23:38 JinjaThreads: theory Automatic_Refinement.Autoref_Data

19:23:38 JinjaThreads: theory Automatic_Refinement.Indep_Vars

19:23:38 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp

19:23:38 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms

19:23:38 JinjaThreads: theory Automatic_Refinement.Tagged_Solver

19:23:38 JinjaThreads: theory Automatic_Refinement.Select_Solve

19:23:38 JinjaThreads: theory HOL-Library.Code_Target_Numeral

19:23:38 JinjaThreads: theory HOL-Library.Infinite_Set

19:23:38 JinjaThreads: theory HOL-Library.Multiset

19:23:38 JinjaThreads: theory HOL-Library.Monad_Syntax

19:23:39 JinjaThreads: theory HOL-Library.Nat_Bijection

19:23:39 JinjaThreads: theory HOL-Library.Old_Datatype

19:23:39 JinjaThreads: theory HOL-Library.Omega_Words_Fun

19:23:39 JinjaThreads: theory HOL-Library.Option_ord

19:23:40 JinjaThreads: theory Trie.Trie

19:23:40 JinjaThreads: theory HOL-Library.Phantom_Type

19:23:40 JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs

19:23:40 JinjaThreads: theory HOL-Library.RBT_Impl

19:23:40 JinjaThreads: theory HOL-Library.Simps_Case_Conv

19:23:40 JinjaThreads: theory HOL-Library.Sublist

19:23:41 JinjaThreads: theory HOL-Library.Transitive_Closure_Table

19:23:41 JinjaThreads: theory HOL-Library.Cardinality

19:23:41 JinjaThreads: theory HOL-Library.While_Combinator

19:23:42 JinjaThreads: theory HOL-Word.Bits

19:23:43 JinjaThreads: theory FinFun.FinFun

19:23:43 JinjaThreads: theory HOL-Library.Numeral_Type

19:23:43 JinjaThreads: theory Collections.DatRef

19:23:44 JinjaThreads: theory HOL-Word.Bits_Bit

19:23:44 JinjaThreads: theory HOL-Word.Misc_Numeric

19:23:44 JinjaThreads: theory HOL-Word.Misc_Typedef

19:23:44 JinjaThreads: theory HOL-Word.Bit_Representation

19:23:44 JinjaThreads: theory HOL-Word.Word_Miscellaneous

19:23:45 JinjaThreads: theory HOL-Library.Countable

19:23:45 JinjaThreads: theory HOL-Library.Type_Length

19:23:45 JinjaThreads: theory JinjaThreads.Set_Monad

19:23:45 JinjaThreads: theory JinjaThreads.Set_without_equal

19:23:45 JinjaThreads: theory Refine_Monadic.Refine_Chapter

19:23:45 JinjaThreads: theory HOL-Word.Bits_Int

19:23:46 JinjaThreads: theory JinjaThreads.Auxiliary

19:23:47 JinjaThreads: theory HOL-Library.Countable_Set

19:23:47 JinjaThreads: theory HOL-Word.Bool_List_Representation

19:23:47 JinjaThreads: theory HOL-Library.Countable_Complete_Lattices

19:23:48 JinjaThreads: theory Binomial-Heaps.BinomialHeap

19:23:48 JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap

19:23:48 JinjaThreads: theory HOL-ex.Quicksort

19:23:48 JinjaThreads: theory Native_Word.More_Bits_Int

19:23:49 JinjaThreads: theory Automatic_Refinement.Misc

19:23:49 JinjaThreads: theory HOL-Word.Word

19:23:51 JinjaThreads: theory HOL-Library.Order_Continuity

19:23:51 JinjaThreads: theory Native_Word.Bits_Integer

19:23:52 JinjaThreads: theory HOL-Library.Extended_Nat

19:23:53 JinjaThreads: theory Coinductive.Coinductive_Nat

19:23:55 JinjaThreads: theory Coinductive.Coinductive_List

19:24:00 JinjaThreads: theory Native_Word.Word_Misc

19:24:01 JinjaThreads: theory Automatic_Refinement.Digraph_Basic

19:24:01 JinjaThreads: theory Collections.SetIterator

19:24:02 JinjaThreads: theory Collections.Sorted_List_Operations

19:24:03 JinjaThreads: theory Automatic_Refinement.Refine_Lib

19:24:04 JinjaThreads: theory Automatic_Refinement.Autoref_Phases

19:24:04 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging

19:24:04 JinjaThreads: theory Automatic_Refinement.Relators

19:24:04 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover

19:24:05 JinjaThreads: theory Collections.SetIteratorOperations

19:24:07 JinjaThreads: theory Automatic_Refinement.Param_Tool

19:24:08 JinjaThreads: theory Automatic_Refinement.Param_HOL

19:24:11 JinjaThreads: theory Collections.Assoc_List

19:24:11 JinjaThreads: theory Collections.Dlist_add

19:24:11 JinjaThreads: theory Collections.Proper_Iterator

19:24:11 JinjaThreads: theory Collections.SetIteratorGA

19:24:11 JinjaThreads: theory Automatic_Refinement.Parametricity

19:24:11 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops

19:24:12 JinjaThreads: theory Collections.It_to_It

19:24:12 JinjaThreads: theory Collections.Diff_Array

19:24:12 JinjaThreads: theory Collections.Trie_Impl

19:24:12 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel

19:24:12 JinjaThreads: theory Native_Word.Code_Target_Bits_Int

19:24:12 JinjaThreads: theory Native_Word.Uint32

19:24:12 JinjaThreads: theory Collections.Trie2

19:24:13 JinjaThreads: theory Collections.Code_Target_ICF

19:24:13 JinjaThreads: theory Coinductive.Lazy_LList

19:24:13 JinjaThreads: theory Coinductive.TLList

19:24:13 JinjaThreads: theory Automatic_Refinement.Autoref_Translate

19:24:13 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface

19:24:13 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo

19:24:13 JinjaThreads: theory Automatic_Refinement.Autoref_Tool

19:24:14 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL

19:24:15 JinjaThreads: theory Collections.HashCode

19:24:17 JinjaThreads: theory Coinductive.Lazy_TLList

19:24:19 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement

19:24:19 JinjaThreads: theory Collections.Idx_Iterator

19:24:20 JinjaThreads: theory Refine_Monadic.Refine_Misc

19:24:21 JinjaThreads: theory Refine_Monadic.RefineG_Domain

19:24:21 JinjaThreads: theory Refine_Monadic.RefineG_Transfer

19:24:21 JinjaThreads: theory Refine_Monadic.RefineG_Assert

19:24:22 JinjaThreads: theory Refine_Monadic.RefineG_Recursion

19:24:23 JinjaThreads: theory Refine_Monadic.RefineG_While

19:24:23 JinjaThreads: theory Refine_Monadic.Refine_Basic

19:24:24 JinjaThreads: theory Refine_Monadic.Refine_Det

19:24:28 JinjaThreads: theory Refine_Monadic.Refine_Heuristics

19:24:28 JinjaThreads: theory Refine_Monadic.Refine_Leof

19:24:28 JinjaThreads: theory Refine_Monadic.Refine_Pfun

19:24:28 JinjaThreads: theory Refine_Monadic.Refine_More_Comb

19:24:28 JinjaThreads: theory Refine_Monadic.Refine_While

19:24:31 JinjaThreads: theory Refine_Monadic.Refine_Transfer

19:24:32 JinjaThreads: theory Refine_Monadic.Autoref_Monadic

19:24:32 JinjaThreads: theory Refine_Monadic.Refine_Automation

19:24:32 JinjaThreads: theory Refine_Monadic.Refine_Foreach

19:24:36 JinjaThreads: theory Refine_Monadic.Refine_Monadic

19:24:38 JinjaThreads: theory Collections.Gen_Iterator

19:24:38 JinjaThreads: theory Collections.Intf_Map

19:24:38 JinjaThreads: theory Collections.Intf_Set

19:24:39 JinjaThreads: theory Collections.Iterator

19:24:40 JinjaThreads: theory Collections.Array_Iterator

19:24:40 JinjaThreads: theory Collections.ICF_Spec_Base

19:24:40 JinjaThreads: theory Collections.AnnotatedListSpec

19:24:40 JinjaThreads: theory Collections.ListSpec

19:24:40 JinjaThreads: theory Collections.MapSpec

19:24:40 JinjaThreads: theory Collections.PrioSpec

19:24:40 JinjaThreads: theory Collections.PrioUniqueSpec

19:24:40 JinjaThreads: theory Collections.SetSpec

19:24:42 JinjaThreads: theory Collections.BinoPrioImpl

19:24:42 JinjaThreads: theory Collections.SkewPrioImpl

19:24:43 JinjaThreads: theory HOL-Library.RBT

19:24:43 JinjaThreads: theory Collections.RBT_add

19:24:43 JinjaThreads: theory Collections.ListGA

19:24:44 JinjaThreads: theory Collections.FTAnnotatedListImpl

19:24:44 JinjaThreads: theory Collections.PrioByAnnotatedList

19:24:44 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList

19:24:44 JinjaThreads: theory Collections.Fifo

19:24:47 JinjaThreads: theory Collections.Algos

19:24:47 JinjaThreads: theory Collections.SetIndex

19:24:47 JinjaThreads: theory Collections.SetIteratorCollectionsGA

19:24:47 JinjaThreads: theory Collections.FTPrioImpl

19:24:47 JinjaThreads: theory Collections.MapGA

19:24:47 JinjaThreads: theory Collections.SetGA

19:24:48 JinjaThreads: theory Collections.FTPrioUniqueImpl

19:24:52 JinjaThreads: theory Collections.ArrayMapImpl

19:24:52 JinjaThreads: theory Collections.ListMapImpl

19:24:52 JinjaThreads: theory Collections.ListMapImpl_Invar

19:24:52 JinjaThreads: theory Collections.TrieMapImpl

19:24:52 JinjaThreads: theory Collections.RBTMapImpl

19:24:54 JinjaThreads: theory Collections.ArrayHashMap_Impl

19:24:57 JinjaThreads: theory Collections.ListSetImpl

19:24:57 JinjaThreads: theory Collections.ListSetImpl_Invar

19:24:57 JinjaThreads: theory Collections.ListSetImpl_NotDist

19:24:57 JinjaThreads: theory Collections.ListSetImpl_Sorted

19:24:57 JinjaThreads: theory Collections.SetByMap

19:24:59 JinjaThreads: theory Collections.HashMap_Impl

19:24:59 JinjaThreads: theory Collections.ArrayHashMap

19:25:00 JinjaThreads: theory Collections.ArraySetImpl

19:25:00 JinjaThreads: theory Collections.TrieSetImpl

19:25:00 JinjaThreads: theory Collections.RBTSetImpl

19:25:01 JinjaThreads: theory Collections.HashMap

19:25:03 JinjaThreads: theory Collections.ArrayHashSet

19:25:05 JinjaThreads: theory Collections.HashSet

19:25:05 JinjaThreads: theory Collections.MapStdImpl

19:25:09 JinjaThreads: theory Collections.SetStdImpl

19:25:14 JinjaThreads: theory Collections.ICF_Impl

19:25:21 JinjaThreads: theory Collections.ICF_Refine_Monadic

19:25:22 JinjaThreads: theory Collections.ICF_Autoref

19:25:27 JinjaThreads: theory Collections.Collections

19:25:28 JinjaThreads: theory Collections.CollectionsV1

19:25:38 JinjaThreads: theory JinjaThreads.JT_ICF

19:25:38 JinjaThreads: theory JinjaThreads.Basic_Main

19:26:06 JinjaThreads: theory HOL-Library.Prefix_Order

19:26:06 JinjaThreads: theory JinjaThreads.FWState

19:26:06 JinjaThreads: theory JinjaThreads.LTS

19:26:06 JinjaThreads: theory JinjaThreads.Type

19:26:06 JinjaThreads: theory JinjaThreads.ListIndex

19:26:06 JinjaThreads: theory JinjaThreads.Orders

19:26:06 JinjaThreads: theory JinjaThreads.Semilat

19:26:06 JinjaThreads: theory HOL-Library.Mapping

19:26:07 JinjaThreads: theory JinjaThreads.Err

19:26:09 JinjaThreads: theory HOL-Library.AList_Mapping

19:26:09 JinjaThreads: theory JinjaThreads.Listn

19:26:09 JinjaThreads: theory JinjaThreads.Opt

19:26:09 JinjaThreads: theory JinjaThreads.Product

19:26:10 JinjaThreads: theory JinjaThreads.Semilattices

19:26:10 JinjaThreads: theory JinjaThreads.Typing_Framework

19:26:10 JinjaThreads: theory JinjaThreads.SemilatAlg

19:26:10 JinjaThreads: theory JinjaThreads.Decl

19:26:11 JinjaThreads: theory JinjaThreads.Kildall

19:26:11 JinjaThreads: theory JinjaThreads.LBVSpec

19:26:11 JinjaThreads: theory JinjaThreads.Bisimulation

19:26:11 JinjaThreads: theory JinjaThreads.Typing_Framework_err

19:26:12 JinjaThreads: theory JinjaThreads.LBVComplete

19:26:12 JinjaThreads: theory JinjaThreads.LBVCorrect

19:26:13 JinjaThreads: theory JinjaThreads.Abstract_BV

19:26:14 JinjaThreads: theory JinjaThreads.TypeRel

19:26:20 JinjaThreads: theory JinjaThreads.TypeRelRefine

19:26:20 JinjaThreads: theory JinjaThreads.Value

19:26:24 JinjaThreads: theory JinjaThreads.Exceptions

19:26:24 JinjaThreads: theory JinjaThreads.Heap

19:26:25 JinjaThreads: theory JinjaThreads.SystemClasses

19:26:27 JinjaThreads: theory JinjaThreads.MM

19:26:27 JinjaThreads: theory JinjaThreads.State

19:26:36 JinjaThreads: theory JinjaThreads.FWCondAction

19:26:36 JinjaThreads: theory JinjaThreads.FWInterrupt

19:26:36 JinjaThreads: theory JinjaThreads.FWLock

19:26:36 JinjaThreads: theory JinjaThreads.FWThread

19:26:36 JinjaThreads: theory JinjaThreads.FWWait

19:26:36 JinjaThreads: theory JinjaThreads.Observable_Events

19:26:39 JinjaThreads: theory JinjaThreads.FWLocking

19:26:40 JinjaThreads: theory JinjaThreads.FWLockingThread

19:26:40 JinjaThreads: theory JinjaThreads.FWWellform

19:26:42 JinjaThreads: theory JinjaThreads.FWLifting

19:26:42 JinjaThreads: theory JinjaThreads.FWSemantics

19:26:45 JinjaThreads: theory JinjaThreads.JVMState

19:26:45 JinjaThreads: theory JinjaThreads.StartConfig

19:26:45 JinjaThreads: theory JinjaThreads.JMM_Spec

19:26:46 JinjaThreads: theory JinjaThreads.FWLiftingSem

19:26:46 JinjaThreads: theory JinjaThreads.FWProgressAux

19:26:47 JinjaThreads: theory JinjaThreads.Conform

19:26:47 JinjaThreads: theory JinjaThreads.State_Refinement

19:26:48 JinjaThreads: theory JinjaThreads.FWDeadlock

19:26:50 JinjaThreads: theory JinjaThreads.FWLTS

19:26:52 JinjaThreads: theory JinjaThreads.ConformThreaded

19:26:52 JinjaThreads: theory JinjaThreads.ExternalCall

19:26:53 JinjaThreads: theory JinjaThreads.FWProgress

19:26:53 JinjaThreads: theory JinjaThreads.SC

19:26:54 JinjaThreads: theory JinjaThreads.SC_Collections

19:27:01 JinjaThreads: theory JinjaThreads.JMM_DRF

19:27:01 JinjaThreads: theory JinjaThreads.SC_Legal

19:27:08 JinjaThreads: theory JinjaThreads.FWBisimulation

19:27:09 JinjaThreads: theory JinjaThreads.FWInitFinLift

19:27:09 JinjaThreads: theory JinjaThreads.Non_Speculative

19:27:10 JinjaThreads: theory JinjaThreads.Scheduler

19:27:14 JinjaThreads: theory JinjaThreads.HB_Completion

19:27:15 JinjaThreads: theory JinjaThreads.SC_Completion

19:27:42 JinjaThreads: theory JinjaThreads.WellForm

19:27:42 JinjaThreads: theory JinjaThreads.ExternalCall_Execute

19:27:47 JinjaThreads: theory JinjaThreads.BinOp

19:27:47 JinjaThreads: theory JinjaThreads.ExternalCallWF

19:27:48 JinjaThreads: theory JinjaThreads.JMM_Heap

19:27:57 JinjaThreads: theory JinjaThreads.SemiType

19:28:02 JinjaThreads: theory JinjaThreads.JMM_Type

19:28:04 JinjaThreads: theory JinjaThreads.JMM_Type2

19:28:21 JinjaThreads: theory JinjaThreads.JVM_SemiType

19:28:36 JinjaThreads: theory JinjaThreads.Expr

19:28:37 JinjaThreads: theory JinjaThreads.JVMInstructions

19:28:38 JinjaThreads: theory JinjaThreads.PCompiler

19:28:39 JinjaThreads: theory JinjaThreads.Random_Scheduler

19:28:40 JinjaThreads: theory JinjaThreads.PCompilerRefine

19:28:40 JinjaThreads: theory JinjaThreads.Round_Robin

19:28:51 JinjaThreads: theory JinjaThreads.JMM_Framework

19:28:53 JinjaThreads: theory JinjaThreads.JVMExceptions

19:28:53 JinjaThreads: theory JinjaThreads.JVMHeap

19:28:53 JinjaThreads: theory JinjaThreads.Effect

19:29:02 JinjaThreads: theory JinjaThreads.SC_Schedulers

19:29:03 JinjaThreads: theory JinjaThreads.CallExpr

19:29:03 JinjaThreads: theory JinjaThreads.DefAss

19:29:05 JinjaThreads: theory JinjaThreads.WWellForm

19:29:05 JinjaThreads: theory JinjaThreads.JHeap

19:29:08 JinjaThreads: theory JinjaThreads.JVMExecInstr

19:29:12 JinjaThreads: theory JinjaThreads.J1State

19:29:13 JinjaThreads: theory JinjaThreads.WellType

19:29:14 JinjaThreads: theory JinjaThreads.JVMExec

19:29:17 JinjaThreads: theory JinjaThreads.Compiler2

19:29:19 JinjaThreads: theory JinjaThreads.JVMDefensive

19:29:22 JinjaThreads: theory JinjaThreads.J1Heap

19:29:23 JinjaThreads: theory JinjaThreads.SmallStep

19:29:31 JinjaThreads: theory JinjaThreads.JVMThreaded

19:29:36 JinjaThreads: theory JinjaThreads.Compiler1

19:29:39 JinjaThreads: theory JinjaThreads.Exception_Tables

19:29:53 JinjaThreads: theory JinjaThreads.J1WellType

19:29:57 JinjaThreads: theory JinjaThreads.Compiler

19:29:58 JinjaThreads: theory JinjaThreads.Annotate

19:29:59 JinjaThreads: theory JinjaThreads.J1WellForm

19:30:00 JinjaThreads: theory JinjaThreads.JWellForm

19:30:03 JinjaThreads: theory JinjaThreads.JJ1WellForm

19:30:05 JinjaThreads: theory JinjaThreads.WellTypeRT

19:30:08 JinjaThreads: theory JinjaThreads.JVMExec_Execute

19:30:09 JinjaThreads: theory JinjaThreads.Preprocessor

19:30:12 JinjaThreads: theory JinjaThreads.ToString

19:30:21 JinjaThreads: theory JinjaThreads.JVM_Main

19:33:27 JinjaThreads: theory JinjaThreads.BVSpec

19:33:28 JinjaThreads: theory JinjaThreads.BVConform

19:33:28 JinjaThreads: theory JinjaThreads.TypeComp

19:33:32 JinjaThreads: theory JinjaThreads.EffectMono

19:33:32 JinjaThreads: theory JinjaThreads.TF_JVM

19:33:37 JinjaThreads: theory JinjaThreads.BVExec

19:33:38 JinjaThreads: theory JinjaThreads.LBVJVM

19:33:42 JinjaThreads: theory JinjaThreads.BVSpecTypeSafe

19:33:57 JinjaThreads: theory JinjaThreads.JMM_JVM

19:33:57 JinjaThreads: theory JinjaThreads.JMM_Typesafe

19:33:57 JinjaThreads: theory JinjaThreads.BVNoTypeError

19:33:59 JinjaThreads: theory JinjaThreads.JVMTau

19:34:02 JinjaThreads: theory JinjaThreads.BVProgressThreaded

19:34:03 JinjaThreads: theory JinjaThreads.BCVExec

19:34:03 JinjaThreads: theory JinjaThreads.JVMExec_Execute2

19:34:25 JinjaThreads: theory JinjaThreads.JMM_Common

19:34:36 JinjaThreads: theory JinjaThreads.JMM_Typesafe2

19:34:44 JinjaThreads: theory JinjaThreads.Execs

19:34:53 JinjaThreads: theory JinjaThreads.DefAssPreservation

19:34:53 JinjaThreads: theory JinjaThreads.Threaded

19:34:54 JinjaThreads: theory JinjaThreads.Progress

19:35:02 JinjaThreads: theory JinjaThreads.TypeSafe

19:35:31 JinjaThreads: theory JinjaThreads.JMM_J

19:35:39 JinjaThreads: theory JinjaThreads.ProgressThreaded

19:35:39 JinjaThreads: theory JinjaThreads.J_Execute

19:36:28 JinjaThreads: theory JinjaThreads.FWBisimDeadlock

19:36:30 JinjaThreads: theory JinjaThreads.FWBisimLift

19:36:31 JinjaThreads: theory JinjaThreads.J1

19:36:34 JinjaThreads: theory JinjaThreads.J0

19:37:01 JinjaThreads: theory JinjaThreads.DRF_J

19:37:01 JinjaThreads: theory JinjaThreads.Deadlocked

19:37:18 JinjaThreads: theory JinjaThreads.J_Main

19:37:24 JinjaThreads: theory JinjaThreads.J1Deadlock

19:37:24 JinjaThreads: theory JinjaThreads.J1JVMBisim

19:37:41 JinjaThreads: theory JinjaThreads.Common_Main

19:38:12 JinjaThreads: theory JinjaThreads.J0Bisim

19:38:12 JinjaThreads: theory JinjaThreads.J0J1Bisim

19:38:24 JinjaThreads: theory JinjaThreads.DRF_JVM

19:38:24 JinjaThreads: theory JinjaThreads.JVMDeadlocked

19:38:25 JinjaThreads: theory JinjaThreads.JVM_Execute

19:38:38 JinjaThreads: theory JinjaThreads.JVM_Execute2

19:44:11 JinjaThreads: theory JinjaThreads.Correctness1

19:44:16 JinjaThreads: theory JinjaThreads.Correctness1Threaded

19:44:21 JinjaThreads: theory JinjaThreads.Code_Generation

19:44:29 JinjaThreads: theory JinjaThreads.ApprenticeChallenge

19:44:30 JinjaThreads: theory JinjaThreads.BufferExample

19:44:33 JinjaThreads: theory JinjaThreads.BV_Main

19:44:34 JinjaThreads: theory JinjaThreads.Java2Jinja

19:44:49 JinjaThreads: theory JinjaThreads.Examples_Main

19:46:50 JinjaThreads: theory JinjaThreads.Execute_Main

19:47:04 JinjaThreads: theory JinjaThreads.JMM_J_Typesafe

19:48:13 JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe

19:49:35 JinjaThreads: theory JinjaThreads.J1JVM

19:49:36 JinjaThreads: theory JinjaThreads.JVMJ1

19:58:02 JinjaThreads: theory JinjaThreads.Correctness2

20:03:04 JinjaThreads: theory JinjaThreads.Correctness

20:09:53 JinjaThreads: theory JinjaThreads.JMM_Compiler

20:09:53 JinjaThreads: theory JinjaThreads.SC_Interp

20:09:53 JinjaThreads: theory JinjaThreads.Compiler_Main

20:15:02 JinjaThreads: theory JinjaThreads.JMM_Interp

20:15:08 JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2

20:19:40 JinjaThreads: theory JinjaThreads.JMM

20:19:42 JinjaThreads: theory JinjaThreads.MM_Main

20:19:51 JinjaThreads: theory JinjaThreads.JinjaThreads

20:21:17 Timing JinjaThreads (8 threads, 3389.547s elapsed time, 15394.792s cpu time, 5012.512s GC time, factor 4.54)

20:21:17 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads

20:21:17 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf

20:21:17 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf

20:21:17 Finished JinjaThreads (0:57:41 elapsed time, 4:18:50 cpu time, factor 4.49)

20:21:17 Running Lorenz_C0 ...

20:21:20 Lorenz_C0: theory Lorenz_C0.Lorenz_C0

20:35:20 Timing Lorenz_C0 (8 threads, 820.864s elapsed time, 6215.024s cpu time, 56.976s GC time, factor 7.57)

20:35:20 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Lorenz_C0

20:35:20 Finished Lorenz_C0 (0:13:44 elapsed time, 1:43:38 cpu time, factor 7.54)

20:35:20 Running HOL-ODE-Examples ...

20:35:23 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral

20:35:23 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method

20:35:23 HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map

20:38:39 HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples

20:43:50 Timing HOL-ODE-Examples (8 threads, 505.132s elapsed time, 1966.372s cpu time, 74.088s GC time, factor 3.89)

20:43:50 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Examples

20:43:50 Finished HOL-ODE-Examples (0:08:29 elapsed time, 0:32:49 cpu time, factor 3.87)

20:43:50 Running Affine_Arithmetic ...

20:43:51 Affine_Arithmetic: theory Deriving.Comparator

20:43:51 Affine_Arithmetic: theory Deriving.Derive_Manager

20:43:51 Affine_Arithmetic: theory HOL-Library.Bit

20:43:51 Affine_Arithmetic: theory HOL-Decision_Procs.Dense_Linear_Order

20:43:51 Affine_Arithmetic: theory Deriving.Generator_Aux

20:43:51 Affine_Arithmetic: theory HOL-Library.Permutation

20:43:51 Affine_Arithmetic: theory HOL-Library.Boolean_Algebra

20:43:51 Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading

20:43:52 Affine_Arithmetic: theory HOL-Library.Char_ord

20:43:52 Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat

20:43:52 Affine_Arithmetic: theory HOL-Library.Code_Target_Nat

20:43:52 Affine_Arithmetic: theory HOL-Library.Code_Target_Int

20:43:52 Affine_Arithmetic: theory Deriving.Equality_Generator

20:43:52 Affine_Arithmetic: theory HOL-Library.Code_Char

20:43:52 Affine_Arithmetic: theory HOL-Library.Mapping

20:43:52 Affine_Arithmetic: theory HOL-Library.Monad_Syntax

20:43:52 Affine_Arithmetic: theory HOL-Library.Type_Length

20:43:53 Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral

20:43:53 Affine_Arithmetic: theory HOL-Library.RBT_Impl

20:43:53 Affine_Arithmetic: theory HOL-Word.Bits

20:43:53 Affine_Arithmetic: theory HOL-Word.Misc_Numeric

20:43:53 Affine_Arithmetic: theory HOL-Word.Bit_Representation

20:43:53 Affine_Arithmetic: theory Deriving.Equality_Instances

20:43:53 Affine_Arithmetic: theory HOL-Word.Word_Miscellaneous

20:43:53 Affine_Arithmetic: theory HOL-Word.Bits_Bit

20:43:53 Affine_Arithmetic: theory HOL-Word.Misc_Typedef

20:43:53 Affine_Arithmetic: theory Deriving.Countable_Generator

20:43:53 Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer

20:43:54 Affine_Arithmetic: theory Deriving.Compare

20:43:54 Affine_Arithmetic: theory Deriving.Comparator_Generator

20:43:54 Affine_Arithmetic: theory HOL-Library.Lattice_Algebras

20:43:54 Affine_Arithmetic: theory HOL-Word.Bits_Int

20:43:54 Affine_Arithmetic: theory HOL-Library.Log_Nat

20:43:54 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities

20:43:54 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise

20:43:55 Affine_Arithmetic: theory List-Index.List_Index

20:43:55 Affine_Arithmetic: theory Show.Show

20:43:55 Affine_Arithmetic: theory Deriving.Compare_Generator

20:43:55 Affine_Arithmetic: theory Deriving.Compare_Instances

20:43:55 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector

20:43:56 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict

20:43:56 Affine_Arithmetic: theory HOL-Word.Bool_List_Representation

20:43:56 Affine_Arithmetic: theory Show.Show_Instances

20:43:57 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary

20:43:57 Affine_Arithmetic: theory Affine_Arithmetic.Polygon

20:43:57 Affine_Arithmetic: theory Native_Word.More_Bits_Int

20:43:57 Affine_Arithmetic: theory HOL-Word.Word

20:44:00 Affine_Arithmetic: theory Native_Word.Bits_Integer

20:44:01 Affine_Arithmetic: theory HOL-Library.Float

20:44:04 Affine_Arithmetic: theory Native_Word.Word_Misc

20:44:05 Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float

20:44:05 Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds

20:44:05 Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space

20:44:05 Affine_Arithmetic: theory Affine_Arithmetic.Float_Real

20:44:11 Affine_Arithmetic: theory HOL-Decision_Procs.Approximation

20:44:13 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form

20:44:20 Affine_Arithmetic: theory Affine_Arithmetic.Intersection

20:44:21 Affine_Arithmetic: theory Native_Word.Uint32

20:44:24 Affine_Arithmetic: theory Collections.HashCode

20:44:24 Affine_Arithmetic: theory Deriving.Hash_Generator

20:44:26 Affine_Arithmetic: theory Deriving.Hash_Instances

20:44:26 Affine_Arithmetic: theory Deriving.Derive

20:44:46 Affine_Arithmetic: theory HOL-Library.RBT

20:44:47 Affine_Arithmetic: theory HOL-Library.RBT_Mapping

20:45:22 Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression

20:45:38 Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program

20:45:52 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation

20:46:19 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code

20:46:24 Affine_Arithmetic: theory Affine_Arithmetic.Print

20:46:29 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation

20:46:29 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs

20:46:30 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter

20:47:47 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic

20:48:00 Timing Affine_Arithmetic (8 threads, 237.536s elapsed time, 1309.224s cpu time, 114.876s GC time, factor 5.51)

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

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

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

20:48:00 Finished Affine_Arithmetic (0:04:09 elapsed time, 0:22:45 cpu time, factor 5.48)

20:48:00 Running Collections ...

20:48:02 Collections: theory Collections.ICF_Tools

20:48:02 Collections: theory Collections.Partial_Equivalence_Relation

20:48:02 Collections: theory Finger-Trees.FingerTree

20:48:02 Collections: theory HOL-Library.AList

20:48:02 Collections: theory Binomial-Heaps.BinomialHeap

20:48:02 Collections: theory HOL-Library.Code_Abstract_Nat

20:48:02 Collections: theory HOL-Library.Code_Target_Int

20:48:02 Collections: theory Binomial-Heaps.SkewBinomialHeap

20:48:02 Collections: theory HOL-Library.Code_Target_Nat

20:48:02 Collections: theory Collections.Ord_Code_Preproc

20:48:02 Collections: theory HOL-Library.Dlist

20:48:02 Collections: theory Collections.Locale_Code

20:48:02 Collections: theory Collections.Record_Intf

20:48:02 Collections: theory HOL-Library.Code_Target_Numeral

20:48:03 Collections: theory Collections.SetIterator

20:48:03 Collections: theory Collections.Sorted_List_Operations

20:48:03 Collections: theory HOL-Library.RBT_Impl

20:48:04 Collections: theory Collections.DatRef

20:48:05 Collections: theory Native_Word.More_Bits_Int

20:48:06 Collections: theory Collections.Idx_Iterator

20:48:06 Collections: theory Collections.SetAbstractionIterator

20:48:06 Collections: theory Collections.SetIteratorOperations

20:48:09 Collections: theory Native_Word.Bits_Integer

20:48:09 Collections: theory Native_Word.Word_Misc

20:48:12 Collections: theory Collections.Assoc_List

20:48:12 Collections: theory Collections.Dlist_add

20:48:12 Collections: theory Collections.Proper_Iterator

20:48:12 Collections: theory Collections.SetIteratorGA

20:48:12 Collections: theory Collections.Diff_Array

20:48:13 Collections: theory Collections.It_to_It

20:48:13 Collections: theory Collections.Gen_Iterator

20:48:14 Collections: theory Collections.Iterator

20:48:15 Collections: theory Collections.ICF_Spec_Base

20:48:15 Collections: theory Collections.MapSpec

20:48:21 Collections: theory Collections.Robdd

20:48:30 Collections: theory Native_Word.Code_Target_Bits_Int

20:48:30 Collections: theory Native_Word.Uint32

20:48:30 Collections: theory Collections.Code_Target_ICF

20:48:30 Collections: theory Collections.Locale_Code_Ex

20:48:32 Collections: theory Collections.HashCode

20:48:57 Collections: theory Collections.RBT_add

20:49:08 Collections: theory Collections.GenCF_Gen_Chapter

20:49:08 Collections: theory Collections.GenCF_Chapter

20:49:08 Collections: theory Collections.Impl_Array_Stack

20:49:08 Collections: theory Collections.GenCF_Intf_Chapter

20:49:08 Collections: theory Collections.Intf_Comp

20:49:08 Collections: theory Collections.GenCF_Impl_Chapter

20:49:08 Collections: theory HOL-Library.Product_Lexorder

20:49:08 Collections: theory Collections.Intf_Hash

20:49:08 Collections: theory Collections.Array_Iterator

20:49:08 Collections: theory Collections.Intf_Map

20:49:08 Collections: theory Collections.Intf_Set

20:49:09 Collections: theory Collections.Gen_Map

20:49:09 Collections: theory Collections.Gen_Set

20:49:09 Collections: theory Collections.Impl_Cfun_Set

20:49:09 Collections: theory Collections.Impl_List_Set

20:49:11 Collections: theory Collections.Impl_Array_Map

20:49:11 Collections: theory Collections.Gen_Comp

20:49:11 Collections: theory Collections.Impl_List_Map

20:49:11 Collections: theory Collections.Impl_RBT_Map

20:49:11 Collections: theory Collections.Gen_Map2Set

20:49:12 Collections: theory Collections.Impl_Array_Hash_Map

20:49:22 Collections: theory Native_Word.Uint

20:49:22 Collections: theory Collections.Gen_Hash

20:49:22 Collections: theory Collections.Impl_Bit_Set

20:49:24 Collections: theory Collections.Impl_Uv_Set

20:49:40 Collections: theory Collections.GenCF

20:49:45 Collections: theory Collections.ICF_Spec_Chapter

20:49:45 Collections: theory Collections.ICF_Gen_Algo_Chapter

20:49:45 Collections: theory Collections.ICF_Chapter

20:49:45 Collections: theory Collections.ICF_Impl_Chapter

20:49:45 Collections: theory Trie.Trie

20:49:45 Collections: theory HOL-Library.RBT

20:49:45 Collections: theory Collections.AnnotatedListSpec

20:49:45 Collections: theory Collections.ListSpec

20:49:45 Collections: theory Collections.PrioSpec

20:49:45 Collections: theory Collections.PrioUniqueSpec

20:49:45 Collections: theory Collections.SetSpec

20:49:47 Collections: theory Collections.BinoPrioImpl

20:49:47 Collections: theory Collections.SkewPrioImpl

20:49:48 Collections: theory Collections.Trie_Impl

20:49:48 Collections: theory Collections.ListGA

20:49:48 Collections: theory Collections.Trie2

20:49:49 Collections: theory Collections.FTAnnotatedListImpl

20:49:49 Collections: theory Collections.PrioByAnnotatedList

20:49:49 Collections: theory Collections.PrioUniqueByAnnotatedList

20:49:49 Collections: theory Collections.Fifo

20:49:51 Collections: theory Collections.Algos

20:49:51 Collections: theory Collections.SetIndex

20:49:51 Collections: theory Collections.SetIteratorCollectionsGA

20:49:52 Collections: theory Collections.MapGA

20:49:52 Collections: theory Collections.SetGA

20:49:52 Collections: theory Collections.FTPrioImpl

20:49:52 Collections: theory Collections.FTPrioUniqueImpl

20:49:56 Collections: theory Collections.ArrayMapImpl

20:49:56 Collections: theory Collections.ListMapImpl

20:49:56 Collections: theory Collections.ListMapImpl_Invar

20:49:56 Collections: theory Collections.TrieMapImpl

20:49:56 Collections: theory Collections.RBTMapImpl

20:49:58 Collections: theory Collections.ArrayHashMap_Impl

20:50:00 Collections: theory Collections.HashMap_Impl

20:50:00 Collections: theory Collections.ListSetImpl

20:50:00 Collections: theory Collections.ListSetImpl_Invar

20:50:00 Collections: theory Collections.ListSetImpl_Sorted

20:50:00 Collections: theory Collections.SetByMap

20:50:00 Collections: theory Collections.ListSetImpl_NotDist

20:50:02 Collections: theory Collections.ArrayHashMap

20:50:03 Collections: theory Collections.HashMap

20:50:04 Collections: theory Collections.ArraySetImpl

20:50:04 Collections: theory Collections.TrieSetImpl

20:50:04 Collections: theory Collections.RBTSetImpl

20:50:05 Collections: theory Collections.ArrayHashSet

20:50:06 Collections: theory Collections.MapStdImpl

20:50:06 Collections: theory Collections.HashSet

20:50:09 Collections: theory Collections.SetStdImpl

20:50:13 Collections: theory Collections.ICF_Impl

20:50:18 Collections: theory Collections.ICF_Refine_Monadic

20:50:19 Collections: theory Collections.ICF_Autoref

20:50:23 Collections: theory Collections.Collections_Entrypoints_Chapter

20:50:23 Collections: theory Collections.ICF_Entrypoints_Chapter

20:50:23 Collections: theory Collections.Userguides_Chapter

20:50:23 Collections: theory Collections.Collections

20:50:23 Collections: theory Collections.Refine_Dflt

20:50:24 Collections: theory Collections.CollectionsV1

20:50:24 Collections: theory Collections.ICF_Userguide

20:50:24 Collections: theory Collections.Refine_Dflt_ICF

20:50:24 Collections: theory Collections.Refine_Dflt_Only_ICF

20:50:24 Collections: theory Collections.Refine_Monadic_Userguide

20:50:49 Timing Collections (8 threads, 151.853s elapsed time, 665.852s cpu time, 43.356s GC time, factor 4.38)

20:50:49 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Collections

20:50:49 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Collections/document.pdf

20:50:49 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Collections/outline.pdf

20:50:49 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Collections/userguide.pdf

20:50:49 Finished Collections (0:02:47 elapsed time, 0:12:39 cpu time, factor 4.54)

20:50:49 Running Native_Word ...

20:50:50 Native_Word: theory HOL-Library.Adhoc_Overloading

20:50:50 Native_Word: theory HOL-Library.Char_ord

20:50:50 Native_Word: theory HOL-Library.Code_Target_Int

20:50:50 Native_Word: theory Native_Word.More_Bits_Int

20:50:50 Native_Word: theory HOL-Library.Old_Datatype

20:50:50 Native_Word: theory HOL-Library.Code_Test

20:50:50 Native_Word: theory HOL-Library.Nat_Bijection

20:50:50 Native_Word: theory HOL-Library.Monad_Syntax

20:50:50 Native_Word: theory HOL-Library.Code_Char

20:50:53 Native_Word: theory HOL-Library.Countable

20:50:53 Native_Word: theory Native_Word.Bits_Integer

20:50:53 Native_Word: theory Native_Word.Word_Misc

20:50:55 Native_Word: theory HOL-Imperative_HOL.Heap

20:50:57 Native_Word: theory HOL-Imperative_HOL.Heap_Monad

20:50:59 Native_Word: theory Native_Word.Native_Word_Imperative_HOL

20:51:08 Native_Word: theory Native_Word.Code_Target_Bits_Int

20:51:08 Native_Word: theory Native_Word.Uint

20:51:08 Native_Word: theory Native_Word.Uint16

20:51:08 Native_Word: theory Native_Word.Uint32

20:51:08 Native_Word: theory Native_Word.Uint64

20:51:09 Native_Word: theory Native_Word.Uint8

20:51:11 Native_Word: theory Native_Word.Native_Cast

20:51:13 Native_Word: theory Native_Word.Native_Word_Test

20:54:08 Native_Word: theory Native_Word.Native_Word_Test_Emu

20:54:08 Native_Word: theory Native_Word.Native_Word_Test_PolyML

20:54:08 Native_Word: theory Native_Word.Native_Word_Test_Scala

20:54:32 Native_Word: theory Native_Word.Native_Word_Test_PolyML2

20:54:36 Native_Word: theory Native_Word.Native_Word_Test_PolyML64

20:54:38 Native_Word: theory Native_Word.Native_Word_Test_GHC

20:54:48 Native_Word: theory Native_Word.Native_Word_Test_MLton

20:54:48 Native_Word: theory Native_Word.Native_Word_Test_MLton2

20:55:02 Native_Word: theory Native_Word.Native_Word_Test_OCaml2

20:55:02 Native_Word: theory Native_Word.Native_Word_Test_OCaml

20:55:06 Native_Word: theory Native_Word.Native_Word_Test_SMLNJ2

20:55:06 Native_Word: theory Native_Word.Native_Word_Test_SMLNJ

20:55:15 Native_Word: theory Native_Word.Uint_Userguide

20:55:26 Timing Native_Word (8 threads, 269.917s elapsed time, 281.376s cpu time, 6.576s GC time, factor 1.04)

20:55:26 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Native_Word

20:55:26 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Native_Word/document.pdf

20:55:26 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Native_Word/outline.pdf

20:55:26 Finished Native_Word (0:04:36 elapsed time, 0:12:54 cpu time, factor 2.80)

20:55:26 Running Binomial-Heaps ...

20:55:28 Binomial-Heaps: theory Binomial-Heaps.BinomialHeap

20:55:28 Binomial-Heaps: theory Binomial-Heaps.SkewBinomialHeap

20:55:41 Binomial-Heaps: theory Binomial-Heaps.Test

20:55:47 Timing Binomial-Heaps (8 threads, 14.800s elapsed time, 46.360s cpu time, 3.624s GC time, factor 3.13)

20:55:47 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Binomial-Heaps

20:55:47 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Binomial-Heaps/document.pdf

20:55:47 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Binomial-Heaps/outline.pdf

20:55:47 Finished Binomial-Heaps (0:00:20 elapsed time, 0:00:52 cpu time, factor 2.61)

20:55:47 Running Coinductive ...

20:55:49 Coinductive: theory HOL-Analysis.Inner_Product

20:55:49 Coinductive: theory Coinductive.Resumption

20:55:49 Coinductive: theory HOL-Analysis.L2_Norm

20:55:49 Coinductive: theory Coinductive.Coinductive_Nat

20:55:49 Coinductive: theory HOL-Analysis.Norm_Arith

20:55:51 Coinductive: theory HOL-Analysis.Product_Vector

20:55:51 Coinductive: theory Coinductive.Coinductive_List

20:55:52 Coinductive: theory HOL-Analysis.Euclidean_Space

20:55:54 Coinductive: theory HOL-Analysis.Linear_Algebra

20:55:58 Coinductive: theory HOL-Analysis.Topology_Euclidean_Space

20:56:00 Coinductive: theory Coinductive.Coinductive_List_Prefix

20:56:00 Coinductive: theory Coinductive.Hamming_Stream

20:56:00 Coinductive: theory Coinductive.Koenigslemma

20:56:00 Coinductive: theory Coinductive.LMirror

20:56:00 Coinductive: theory Coinductive.Lazy_LList

20:56:00 Coinductive: theory Coinductive.Quotient_Coinductive_List

20:56:01 Coinductive: theory Coinductive.TLList

20:56:01 Coinductive: theory Coinductive.Coinductive_Stream

20:56:04 Coinductive: theory Coinductive.Lazy_TLList

20:56:04 Coinductive: theory Coinductive.Quotient_TLList

20:56:04 Coinductive: theory Coinductive.TLList_CCPO

20:56:05 Coinductive: theory Coinductive.TLList_CCPO_Examples

20:56:06 Coinductive: theory Coinductive.Coinductive

20:56:07 Coinductive: theory HOL-Analysis.Extended_Real_Limits

20:56:08 Coinductive: theory Coinductive.CCPO_Topology

20:56:10 Coinductive: theory Coinductive.LList_CCPO_Topology

20:56:13 Coinductive: theory Coinductive.Coinductive_Examples

20:56:31 Timing Coinductive (8 threads, 33.933s elapsed time, 202.916s cpu time, 8.092s GC time, factor 5.98)

20:56:31 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Coinductive

20:56:31 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Coinductive/document.pdf

20:56:31 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Coinductive/outline.pdf

20:56:31 Finished Coinductive (0:00:43 elapsed time, 0:03:49 cpu time, factor 5.26)

20:56:31 Running FinFun ...

20:56:32 FinFun: theory HOL-Library.Phantom_Type

20:56:33 FinFun: theory HOL-Library.Cardinality

20:56:34 FinFun: theory FinFun.FinFun

20:56:38 FinFun: theory FinFun.FinFunPred

20:56:42 Timing FinFun (8 threads, 6.790s elapsed time, 14.380s cpu time, 0.616s GC time, factor 2.12)

20:56:42 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/FinFun

20:56:42 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/FinFun/document.pdf

20:56:42 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/FinFun/outline.pdf

20:56:42 Finished FinFun (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.76)

20:56:42 Running Finger-Trees ...

20:56:44 Finger-Trees: theory Finger-Trees.FingerTree

20:56:58 Finger-Trees: theory Finger-Trees.Test

20:57:03 Timing Finger-Trees (8 threads, 15.498s elapsed time, 32.772s cpu time, 2.160s GC time, factor 2.11)

20:57:03 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Finger-Trees

20:57:03 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Finger-Trees/document.pdf

20:57:03 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Finger-Trees/outline.pdf

20:57:03 Finished Finger-Trees (0:00:20 elapsed time, 0:00:38 cpu time, factor 1.90)

20:57:03 Running List-Index ...

20:57:04 List-Index: theory List-Index.List_Index

20:57:08 Timing List-Index (8 threads, 1.954s elapsed time, 8.720s cpu time, 0.100s GC time, factor 4.46)

20:57:08 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/List-Index

20:57:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/List-Index/document.pdf

20:57:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/List-Index/outline.pdf

20:57:08 Finished List-Index (0:00:04 elapsed time, 0:00:11 cpu time, factor 2.40)

20:57:08 Running Show ...

20:57:10 Show: theory HOL-Computational_Algebra.Factorial_Ring

20:57:10 Show: theory Show.Show

20:57:12 Show: theory Show.Show_Instances

20:57:12 Show: theory Show.Show_Real

20:57:12 Show: theory Show.Show_Complex

20:57:14 Show: theory Show.Show_Real_Impl

20:57:21 Show: theory HOL-Computational_Algebra.Polynomial

20:57:31 Show: theory Show.Show_Poly

20:57:35 Timing Show (8 threads, 21.896s elapsed time, 50.996s cpu time, 2.108s GC time, factor 2.33)

20:57:35 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Show

20:57:35 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Show/document.pdf

20:57:35 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Show/outline.pdf

20:57:35 Finished Show (0:00:26 elapsed time, 0:00:55 cpu time, factor 2.13)

20:57:35 Running Triangle ...

20:57:36 Triangle: theory Triangle.Angles

20:57:37 Triangle: theory Triangle.Triangle

20:57:44 Timing Triangle (8 threads, 5.171s elapsed time, 8.740s cpu time, 0.120s GC time, factor 1.69)

20:57:44 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Triangle

20:57:44 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Triangle/document.pdf

20:57:44 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Triangle/outline.pdf

20:57:44 Finished Triangle (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.43)

20:57:44 Running Trie ...

20:57:46 Trie: theory Trie.Trie

20:57:48 Trie: theory Trie.Tries

20:58:12 Timing Trie (8 threads, 23.180s elapsed time, 27.612s cpu time, 0.860s GC time, factor 1.19)

20:58:12 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Trie

20:58:12 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Trie/document.pdf

20:58:12 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Trie/outline.pdf

20:58:12 Finished Trie (0:00:27 elapsed time, 0:00:31 cpu time, factor 1.17)

20:58:12 Running FOL ...

20:58:12 FOL: theory IFOL

20:58:13 FOL: theory FOL

20:58:18 Timing FOL (8 threads, 3.737s elapsed time, 3.984s cpu time, 0.144s GC time, factor 1.07)

20:58:18 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/FOL/FOL

20:58:18 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/FOL/FOL/document.pdf

20:58:18 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/FOL/FOL/outline.pdf

20:58:18 Finished FOL (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.14)

20:58:18 Running HOL-Decision_Procs ...

20:58:21 HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions

20:58:21 HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux

20:58:21 HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper

20:58:21 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order

20:58:21 HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library

20:58:21 HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair

20:58:21 HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List

20:58:24 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring

20:58:26 HOL-Decision_Procs: theory HOL-Decision_Procs.Ferrack

20:58:26 HOL-Decision_Procs: theory HOL-Decision_Procs.MIR

20:58:26 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Bounds

20:58:26 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order_Ex

20:58:32 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation

20:58:40 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Complete

20:58:40 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflective_Field

20:58:43 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial

20:59:03 HOL-Decision_Procs: theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff

20:59:04 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex

21:00:12 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Ex

21:00:13 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Quickcheck_Ex

21:04:22 HOL-Decision_Procs: theory HOL-Decision_Procs.Decision_Procs

21:06:35 Timing HOL-Decision_Procs (8 threads, 492.876s elapsed time, 2015.116s cpu time, 231.068s GC time, factor 4.09)

21:06:35 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Decision_Procs

21:06:35 Finished HOL-Decision_Procs (0:08:16 elapsed time, 0:33:38 cpu time, factor 4.07)

21:06:35 Running HOL-Eisbach ...

21:06:36 HOL-Eisbach: theory HOL-Eisbach.Eisbach

21:06:36 HOL-Eisbach: theory IFOL

21:06:37 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Old_Appl_Syntax

21:06:37 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Tools

21:06:37 HOL-Eisbach: theory HOL-Eisbach.Examples

21:06:37 HOL-Eisbach: theory HOL-Eisbach.Tests

21:06:38 HOL-Eisbach: theory FOL

21:06:40 HOL-Eisbach: theory HOL-Eisbach.Examples_FOL

21:06:41 Timing HOL-Eisbach (8 threads, 3.752s elapsed time, 8.444s cpu time, 0.188s GC time, factor 2.25)

21:06:41 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Eisbach

21:06:41 Finished HOL-Eisbach (0:00:05 elapsed time, 0:00:09 cpu time, factor 1.77)

21:06:41 Running HOL-Imperative_HOL ...

21:06:42 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Sorted_List

21:06:42 HOL-Imperative_HOL: theory HOL-Imperative_HOL.List_Sublist

21:06:42 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap

21:06:46 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad

21:06:48 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Array

21:06:49 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Ref

21:06:49 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Subarray

21:06:49 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL

21:06:49 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Linked_Lists

21:06:49 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Overview

21:06:49 HOL-Imperative_HOL: theory HOL-Imperative_HOL.SatChecker

21:06:49 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort

21:06:49 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse

21:07:26 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL_ex

21:07:50 Timing HOL-Imperative_HOL (8 threads, 65.274s elapsed time, 96.532s cpu time, 2.580s GC time, factor 1.48)

21:07:50 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Imperative_HOL

21:07:50 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Imperative_HOL/document.pdf

21:07:50 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Imperative_HOL/outline.pdf

21:07:50 Finished HOL-Imperative_HOL (0:01:09 elapsed time, 0:06:05 cpu time, factor 5.27)

21:07:50 Running HOL-Types_To_Sets ...

21:07:51 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Prerequisites

21:07:51 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Types_To_Sets

21:07:52 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Finite

21:07:52 HOL-Types_To_Sets: theory HOL-Types_To_Sets.T2_Spaces

21:07:54 Timing HOL-Types_To_Sets (8 threads, 1.092s elapsed time, 1.672s cpu time, 0.000s GC time, factor 1.53)

21:07:54 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Types_To_Sets

21:07:54 Finished HOL-Types_To_Sets (0:00:02 elapsed time)

21:07:54 Running HOL-ex ...

21:07:56 HOL-ex: theory HOL-ex.Computations

21:07:56 HOL-ex: theory HOL-ex.Bubblesort

21:07:56 HOL-ex: theory HOL-ex.MergeSort

21:07:56 HOL-ex: theory HOL-ex.IArray_Examples

21:07:56 HOL-ex: theory HOL-ex.Perm_Fragments

21:07:56 HOL-ex: theory HOL-ex.Quicksort

21:07:56 HOL-ex: theory HOL-ex.Refute_Examples

21:07:56 HOL-ex: theory HOL-ex.Simps_Case_Conv_Examples

21:07:57 HOL-ex: theory HOL-ex.Transitive_Closure_Table_Ex

21:07:57 HOL-ex: theory HOL-ex.While_Combinator_Example

21:07:57 HOL-ex: theory HOL-ex.Code_Timing

21:07:57 HOL-ex: theory HOL-ex.Adhoc_Overloading_Examples

21:07:58 HOL-ex: theory HOL-ex.Antiquote

21:07:58 HOL-ex: theory HOL-ex.Arith_Examples

21:07:58 HOL-ex: theory HOL-ex.Birthday_Paradox

21:07:58 HOL-ex: theory HOL-ex.CTL

21:07:58 HOL-ex: theory HOL-ex.Cartouche_Examples

21:07:58 HOL-ex: theory HOL-ex.Case_Product

21:07:58 HOL-ex: theory HOL-ex.Chinese

21:07:59 HOL-ex: theory HOL-ex.Classical

21:07:59 HOL-ex: theory HOL-ex.Coercion_Examples

21:07:59 HOL-ex: theory HOL-ex.Coherent

21:07:59 HOL-ex: theory HOL-ex.Commands

21:07:59 HOL-ex: theory HOL-ex.Erdoes_Szekeres

21:07:59 HOL-ex: theory HOL-ex.Executable_Relation

21:07:59 HOL-ex: theory HOL-ex.Execute_Choice

21:07:59 HOL-ex: theory HOL-ex.Functions

21:07:59 HOL-ex: theory HOL-ex.Groebner_Examples

21:08:00 HOL-ex: theory HOL-ex.Guess

21:08:00 HOL-ex: theory HOL-ex.Hebrew

21:08:00 HOL-ex: theory HOL-ex.Hex_Bin_Examples

21:08:00 HOL-ex: theory HOL-ex.Iff_Oracle

21:08:00 HOL-ex: theory HOL-ex.Induction_Schema

21:08:00 HOL-ex: theory HOL-ex.Intuitionistic

21:08:00 HOL-ex: theory HOL-ex.Lagrange

21:08:00 HOL-ex: theory HOL-ex.List_to_Set_Comprehension_Examples

21:08:00 HOL-ex: theory HOL-ex.LocaleTest2

21:08:00 HOL-ex: theory HOL-ex.ML

21:08:00 HOL-ex: theory HOL-ex.MonoidGroup

21:08:00 HOL-ex: theory HOL-ex.Multiquote

21:08:00 HOL-ex: theory HOL-ex.NatSum

21:08:00 HOL-ex: theory HOL-ex.PER

21:08:00 HOL-ex: theory HOL-ex.Peano_Axioms

21:08:01 HOL-ex: theory HOL-ex.PresburgerEx

21:08:01 HOL-ex: theory HOL-ex.Primrec

21:08:01 HOL-ex: theory HOL-ex.Records

21:08:01 HOL-ex: theory HOL-ex.Rewrite_Examples

21:08:01 HOL-ex: theory HOL-ex.SAT_Examples

21:08:01 HOL-ex: theory HOL-ex.Seq

21:08:01 HOL-ex: theory HOL-ex.Serbian

21:08:02 HOL-ex: theory HOL-ex.Set_Comprehension_Pointfree_Examples

21:08:02 HOL-ex: theory HOL-ex.Set_Theory

21:08:02 HOL-ex: theory HOL-ex.Simproc_Tests

21:08:02 HOL-ex: theory HOL-ex.Sudoku

21:08:02 HOL-ex: theory HOL-ex.Tarski

21:08:02 HOL-ex: theory HOL-ex.Termination

21:08:04 HOL-ex: theory HOL-ex.ThreeDivides

21:08:04 HOL-ex: theory HOL-ex.Transfer_Int_Nat

21:08:04 HOL-ex: theory HOL-ex.Tree23

21:08:04 HOL-ex: theory HOL-ex.Unification

21:08:04 HOL-ex: theory HOL-ex.Word_Type

21:08:07 HOL-ex: theory HOL-ex.veriT_Preprocessing

21:08:08 HOL-ex: theory HOL-ex.Transfer_Debug

21:08:08 HOL-ex: theory HOL-ex.Function_Growth

21:08:08 HOL-ex: theory HOL-ex.SOS

21:08:09 HOL-ex: theory HOL-ex.SOS_Cert

21:08:09 HOL-ex: theory HOL-ex.Argo_Examples

21:08:09 HOL-ex: theory HOL-ex.Ballot

21:08:09 HOL-ex: theory HOL-ex.BinEx

21:08:10 HOL-ex: theory HOL-ex.Code_Binary_Nat_examples

21:08:10 HOL-ex: theory HOL-ex.Cubic_Quartic

21:08:10 HOL-ex: theory HOL-ex.Dedekind_Real

21:08:10 HOL-ex: theory HOL-ex.Eval_Examples

21:08:10 HOL-ex: theory HOL-ex.Gauge_Integration

21:08:11 HOL-ex: theory HOL-ex.HarmonicSeries

21:08:11 HOL-ex: theory HOL-ex.Normalization_by_Evaluation

21:08:11 HOL-ex: theory HOL-ex.Parallel_Example

21:08:12 HOL-ex: theory HOL-ex.Pythagoras

21:08:12 HOL-ex: theory HOL-ex.Reflection_Examples

21:08:13 HOL-ex: theory HOL-ex.Sqrt

21:08:13 HOL-ex: theory HOL-ex.Sqrt_Script

21:08:13 HOL-ex: theory HOL-ex.Sum_of_Powers

21:11:49 HOL-ex: theory HOL-ex.Meson_Test

21:12:04 Timing HOL-ex (8 threads, 246.506s elapsed time, 1151.036s cpu time, 65.624s GC time, factor 4.67)

21:12:04 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-ex

21:12:04 Finished HOL-ex (0:04:09 elapsed time, 0:19:56 cpu time, factor 4.79)

21:12:04 Unfinished session(s): Iptables_Semantics_Examples_Big

21:12:04

21:12:04 === TIMING ===

21:12:04

21:12:04 Group slow: 17:37:08 elapsed time, 55:27:27 cpu time, factor 3.15

21:12:04 Group AFP: 18:56:42 elapsed time, 59:42:20 cpu time, factor 3.15

21:12:04 Group main: 0:20:53 elapsed time, 1:11:20 cpu time, factor 3.41

21:12:04 Group timing: 0:32:34 elapsed time, 2:04:58 cpu time, factor 3.84

21:12:04 Group very_slow: 11:40:32 elapsed time, 29:12:27 cpu time, factor 2.50

21:12:04 Overall: 19:37:11 elapsed time, 62:03:41 cpu time, factor 3.16

21:12:04

21:12:04 === FAILED SESSIONS ===

21:12:04

21:12:04 Session Iptables_Semantics_Examples_Big: FAILED 1

21:12:04 Build step 'Execute shell' marked build as failure

21:12:04 Archiving artifacts

21:12:05 Started calculate disk usage of build

21:12:05 Finished Calculation of disk usage of build in 0 seconds

21:12:05 Started calculate disk usage of workspace

21:12:06 Finished Calculation of disk usage of workspace in 0 seconds

21:12:06 Email was triggered for: Failure - 1st

21:12:06 Trigger Failure - Any was overridden by another trigger and will not send an email.

21:12:06 Trigger Failure - Still was overridden by another trigger and will not send an email.

21:12:06 Sending email for trigger: Failure - 1st

21:12:06 Sending email to: isabelle-ci@mail46.informatik.tu-muenchen.de

21:12:06 Finished: FAILURE