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:11 Started by an SCM change

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

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

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

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

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

01:33:11 searching for changes

01:33:11 no changes found

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

01:33:12 26 files updated, 0 files merged, 0 files removed, 0 files unresolved

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

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

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

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

01:33:13 exists

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

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

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

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

01:33:14 no changes found

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

01:33:14 67 files updated, 0 files merged, 0 files removed, 0 files unresolved

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

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

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

01:33:15 [afp] $ hg log --rev c3cfeceda7a0e693ab13f1482e86d26a62780ead --template exists\n

01:33:15 exists

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

01:33:15 No emails were triggered.

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

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

01:33:15 + set -e

01:33:15 + PROFILE=slow

01:33:15 + shift

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

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

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

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

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

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

01:33:18 Note: Some input files use unchecked or unsafe operations.

01:33:18 Note: Recompile with -Xlint:unchecked for details.

01:33:18 1 warning

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

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

01:34:46 + bin/isabelle ci_build_slow

01:34:54

01:34:54 === CONFIGURATION ===

01:34:54

01:34:54 ISABELLE_BUILD_OPTIONS=""

01:34:54

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

01:34:54 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7.1-5/x86_64-linux"

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

01:34:54 ML_OPTIONS="-H 4000 --maxheap 20G"

01:34:54

01:34:54 === BUILD ===

01:34:54

01:34:54 Build started at Thu, 10 May 2018 01:34:54 +0200

01:34:54 Isabelle id 763f5a8f3f7f

01:34:55 Build for AFP id 2d77f99edaa7

01:34:55

01:34:55 === LOG ===

01:34:55

01:34:56 Session Pure/Pure

01:34:57 Session FOL/FOL

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

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

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

01:34:59 Session HOL/HOL-Eisbach

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

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

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

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

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

01:35:00 Session AFP/Finger-Trees (AFP)

01:35:00 Session HOL/HOL-Computational_Algebra (main timing)

01:35:00 Session HOL/HOL-Algebra (main timing)

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

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

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

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

01:35:02 Session HOL/HOL-Number_Theory (main timing)

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

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

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

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

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

01:35:04 Session HOL/HOL-Types_To_Sets

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

01:35:17 Building Pure ...

01:35:41 Pure: theory Pure

01:35:42 Pure: theory ML_Bootstrap

01:35:42 Pure: theory Pure.Sessions

01:35:46 Timing Pure (1 threads, 0.923s elapsed time, 0.924s cpu time, 0.000s GC time, factor 1.00)

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

01:35:46 Finished Pure (0:00:27 elapsed time, 0:00:26 cpu time, factor 0.98)

01:35:46 Building HOL ...

01:35:51 HOL: theory HOL.Code_Generator

01:35:55 HOL: theory HOL.HOL

01:36:00 HOL: theory HOL.Argo

01:36:00 HOL: theory HOL.Orderings

01:36:00 HOL: theory HOL.Ctr_Sugar

01:36:02 HOL: theory HOL.Groups

01:36:02 HOL: theory HOL.SAT

01:36:05 HOL: theory HOL.Lattices

01:36:07 HOL: theory HOL.Set

01:36:08 HOL: theory HOL.Fun

01:36:08 HOL: theory HOL.Typedef

01:36:08 HOL: theory HOL.Rings

01:36:09 HOL: theory HOL.Complete_Lattices

01:36:12 HOL: theory HOL.Inductive

01:36:15 HOL: theory HOL.Product_Type

01:36:15 HOL: theory HOL.Sum_Type

01:36:16 HOL: theory HOL.Complete_Partial_Order

01:36:20 HOL: theory HOL.Nat

01:36:23 HOL: theory HOL.Fields

01:36:23 HOL: theory HOL.Meson

01:36:24 HOL: theory HOL.ATP

01:36:27 HOL: theory HOL.Metis

01:36:29 HOL: theory HOL.Finite_Set

01:36:30 HOL: theory HOL.Relation

01:36:32 HOL: theory HOL.Transitive_Closure

01:36:34 HOL: theory HOL.Wellfounded

01:36:35 HOL: theory HOL.Fun_Def_Base

01:36:35 HOL: theory HOL.Hilbert_Choice

01:36:35 HOL: theory HOL.Wfrec

01:36:35 HOL: theory HOL.Order_Relation

01:36:35 HOL: theory HOL.BNF_Wellorder_Relation

01:36:36 HOL: theory HOL.BNF_Wellorder_Embedding

01:36:36 HOL: theory HOL.Zorn

01:36:37 HOL: theory HOL.BNF_Wellorder_Constructions

01:36:37 HOL: theory HOL.BNF_Cardinal_Order_Relation

01:36:39 HOL: theory HOL.BNF_Cardinal_Arithmetic

01:36:39 HOL: theory HOL.BNF_Def

01:36:43 HOL: theory HOL.BNF_Composition

01:36:43 HOL: theory HOL.Basic_BNFs

01:36:44 HOL: theory HOL.BNF_Fixpoint_Base

01:36:49 HOL: theory HOL.BNF_Least_Fixpoint

01:36:53 HOL: theory HOL.Basic_BNF_LFPs

01:36:54 HOL: theory HOL.Transfer

01:36:55 HOL: theory HOL.Num

01:36:59 HOL: theory HOL.Power

01:37:02 HOL: theory HOL.Groups_Big

01:37:04 HOL: theory HOL.Equiv_Relations

01:37:05 HOL: theory HOL.Lifting

01:37:07 HOL: theory HOL.Lifting_Set

01:37:07 HOL: theory HOL.Option

01:37:07 HOL: theory HOL.Quotient

01:37:08 HOL: theory HOL.Extraction

01:37:08 HOL: theory HOL.Lattices_Big

01:37:08 HOL: theory HOL.Partial_Function

01:37:09 HOL: theory HOL.Fun_Def

01:37:11 HOL: theory HOL.Int

01:37:14 HOL: theory HOL.Euclidean_Division

01:37:20 HOL: theory HOL.Parity

01:37:23 HOL: theory HOL.Divides

01:37:26 HOL: theory HOL.Code_Numeral

01:37:26 HOL: theory HOL.Numeral_Simprocs

01:37:26 HOL: theory HOL.SMT

01:37:26 HOL: theory HOL.Set_Interval

01:37:28 HOL: theory HOL.Semiring_Normalization

01:37:30 HOL: theory HOL.Groebner_Basis

01:37:31 HOL: theory HOL.Conditionally_Complete_Lattices

01:37:31 HOL: theory HOL.Filter

01:37:32 HOL: theory HOL.Presburger

01:37:35 HOL: theory HOL.Sledgehammer

01:37:39 HOL: theory HOL.List

01:37:52 HOL: theory HOL.Groups_List

01:37:52 HOL: theory HOL.Map

01:37:53 HOL: theory HOL.GCD

01:37:53 HOL: theory HOL.Random

01:37:53 HOL: theory HOL.Factorial

01:37:53 HOL: theory HOL.Enum

01:37:54 HOL: theory HOL.Binomial

01:37:59 HOL: theory HOL.String

01:38:02 HOL: theory HOL.BNF_Greatest_Fixpoint

01:38:02 HOL: theory HOL.Predicate

01:38:02 HOL: theory HOL.Typerep

01:38:04 HOL: theory HOL.Lazy_Sequence

01:38:05 HOL: theory HOL.Limited_Sequence

01:38:05 HOL: theory HOL.Code_Evaluation

01:38:08 HOL: theory HOL.Quickcheck_Random

01:38:11 HOL: theory HOL.Quickcheck_Exhaustive

01:38:11 HOL: theory HOL.Quickcheck_Narrowing

01:38:11 HOL: theory HOL.Random_Pred

01:38:12 HOL: theory HOL.Random_Sequence

01:38:17 HOL: theory HOL.Record

01:38:17 HOL: theory HOL.Predicate_Compile

01:38:19 HOL: theory HOL.Nitpick

01:38:28 HOL: theory HOL.Nunchaku

01:38:29 HOL: theory Main

01:38:31 HOL: theory HOL.Archimedean_Field

01:38:31 HOL: theory HOL.FuncSet

01:38:31 HOL: theory HOL.Hull

01:38:31 HOL: theory HOL.Topological_Spaces

01:38:31 HOL: theory HOL.Modules

01:38:33 HOL: theory HOL.Vector_Spaces

01:38:40 HOL: theory HOL.Rat

01:38:45 HOL: theory HOL.Real

01:38:49 HOL: theory HOL.Real_Vector_Spaces

01:39:03 HOL: theory HOL.Inequalities

01:39:03 HOL: theory HOL.Limits

01:39:09 HOL: theory HOL.Deriv

01:39:09 HOL: theory HOL.Series

01:39:16 HOL: theory HOL.NthRoot

01:39:17 HOL: theory HOL.Transcendental

01:39:25 HOL: theory HOL.Complex

01:39:27 HOL: theory HOL.MacLaurin

01:39:28 HOL: theory Complex_Main

01:41:31 Timing HOL (8 threads, 233.059s elapsed time, 843.460s cpu time, 87.316s GC time, factor 3.62)

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

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

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

01:41:31 Finished HOL (0:05:40 elapsed time, 0:17:18 cpu time, factor 3.05)

01:41:31 Building AWN ...

01:41:32 AWN: theory AWN.Lib

01:41:32 AWN: theory AWN.TransitionSystems

01:41:32 AWN: theory AWN.AWN

01:41:33 AWN: theory AWN.Invariants

01:41:34 AWN: theory AWN.OInvariants

01:41:47 AWN: theory AWN.AWN_Cterms

01:41:47 AWN: theory AWN.AWN_SOS

01:41:47 AWN: theory AWN.OAWN_SOS

01:41:51 AWN: theory AWN.AWN_Labels

01:41:54 AWN: theory AWN.Inv_Cterms

01:41:54 AWN: theory AWN.AWN_Invariants

01:41:54 AWN: theory AWN.Pnet

01:41:55 AWN: theory AWN.AWN_SOS_Labels

01:41:55 AWN: theory AWN.Closed

01:41:56 AWN: theory AWN.Qmsg

01:41:57 AWN: theory AWN.OAWN_Invariants

01:41:57 AWN: theory AWN.OAWN_SOS_Labels

01:41:57 AWN: theory AWN.OPnet

01:41:57 AWN: theory AWN.ONode_Lifting

01:41:58 AWN: theory AWN.OPnet_Lifting

01:41:58 AWN: theory AWN.OClosed_Lifting

01:41:59 AWN: theory AWN.OClosed_Transfer

01:41:59 AWN: theory AWN.OAWN_Convert

01:41:59 AWN: theory AWN.Qmsg_Lifting

01:42:00 AWN: theory AWN.AWN_Main

01:42:01 AWN: theory AWN.Toy

01:42:17 AWN: theory AWN.AWN_Term_Graph

01:43:16 Timing AWN (8 threads, 49.049s elapsed time, 240.428s cpu time, 10.176s GC time, factor 4.90)

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

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

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

01:43:16 Finished AWN (0:01:44 elapsed time, 0:05:29 cpu time, factor 3.15)

01:43:16 Building HOL-Analysis ...

01:43:18 HOL-Analysis: theory HOL-Library.Cancellation

01:43:18 HOL-Analysis: theory HOL-Library.Disjoint_Sets

01:43:18 HOL-Analysis: theory HOL-Library.Infinite_Set

01:43:18 HOL-Analysis: theory HOL-Library.Nat_Bijection

01:43:18 HOL-Analysis: theory HOL-Library.Old_Datatype

01:43:18 HOL-Analysis: theory HOL-Library.Phantom_Type

01:43:18 HOL-Analysis: theory HOL-Library.Product_Plus

01:43:18 HOL-Analysis: theory HOL-Library.Set_Algebras

01:43:18 HOL-Analysis: theory HOL-Library.Product_Order

01:43:19 HOL-Analysis: theory HOL-Analysis.Infinite_Products

01:43:19 HOL-Analysis: theory HOL-Analysis.Inner_Product

01:43:19 HOL-Analysis: theory HOL-Analysis.L2_Norm

01:43:19 HOL-Analysis: theory HOL-Analysis.Operator_Norm

01:43:19 HOL-Analysis: theory HOL-Library.Multiset

01:43:19 HOL-Analysis: theory HOL-Analysis.Poly_Roots

01:43:19 HOL-Analysis: theory HOL-Library.Discrete

01:43:19 HOL-Analysis: theory HOL-Library.Indicator_Function

01:43:19 HOL-Analysis: theory HOL-Library.Liminf_Limsup

01:43:20 HOL-Analysis: theory HOL-Library.Nonpos_Ints

01:43:20 HOL-Analysis: theory HOL-Library.Countable

01:43:20 HOL-Analysis: theory HOL-Library.Cardinality

01:43:20 HOL-Analysis: theory HOL-Library.Periodic_Fun

01:43:20 HOL-Analysis: theory HOL-Library.Sum_of_Squares

01:43:21 HOL-Analysis: theory HOL-Analysis.Product_Vector

01:43:22 HOL-Analysis: theory HOL-Library.Numeral_Type

01:43:22 HOL-Analysis: theory HOL-Library.Countable_Set

01:43:22 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices

01:43:22 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable

01:43:23 HOL-Analysis: theory HOL-Analysis.Euclidean_Space

01:43:24 HOL-Analysis: theory HOL-Analysis.Norm_Arith

01:43:25 HOL-Analysis: theory HOL-Analysis.Linear_Algebra

01:43:25 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product

01:43:25 HOL-Analysis: theory HOL-Library.Order_Continuity

01:43:26 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space

01:43:26 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring

01:43:26 HOL-Analysis: theory HOL-Library.Permutations

01:43:27 HOL-Analysis: theory HOL-Library.Extended_Nat

01:43:28 HOL-Analysis: theory HOL-Analysis.Cartesian_Space

01:43:28 HOL-Analysis: theory HOL-Library.Extended_Real

01:43:35 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real

01:43:35 HOL-Analysis: theory HOL-Analysis.Connected

01:43:35 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm

01:43:38 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra

01:43:38 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits

01:43:40 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space

01:43:40 HOL-Analysis: theory HOL-Analysis.Tagged_Division

01:43:40 HOL-Analysis: theory HOL-Analysis.Summation_Tests

01:43:42 HOL-Analysis: theory HOL-Analysis.Uniform_Limit

01:43:42 HOL-Analysis: theory HOL-Analysis.Measurable

01:43:43 HOL-Analysis: theory HOL-Analysis.Measure_Space

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

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

01:43:45 HOL-Analysis: theory HOL-Computational_Algebra.Primes

01:43:45 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series

01:43:48 HOL-Analysis: theory HOL-Analysis.Caratheodory

01:43:49 HOL-Analysis: theory HOL-Analysis.Continuous_Extension

01:43:50 HOL-Analysis: theory HOL-Analysis.Path_Connected

01:43:57 HOL-Analysis: theory HOL-Analysis.Homeomorphism

01:43:59 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint

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

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

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

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

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

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

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

01:44:15 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected

01:44:15 HOL-Analysis: theory HOL-Analysis.Borel_Space

01:44:20 HOL-Analysis: theory HOL-Analysis.Lipschitz

01:44:20 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration

01:44:20 HOL-Analysis: theory HOL-Analysis.Regularity

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

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

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

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

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

01:44:31 HOL-Analysis: theory HOL-Analysis.Complete_Measure

01:44:31 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym

01:44:32 HOL-Analysis: theory HOL-Analysis.Set_Integral

01:44:32 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure

01:44:33 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum

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

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

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

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

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

01:44:46 HOL-Analysis: theory HOL-Analysis.Improper_Integral

01:44:46 HOL-Analysis: theory HOL-Analysis.Interval_Integral

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

01:44:48 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental

01:44:53 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem

01:44:53 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers

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

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

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

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

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

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

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

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

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

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

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

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

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

01:53:08 Timing HOL-Analysis (8 threads, 464.045s elapsed time, 2479.996s cpu time, 224.868s GC time, factor 5.34)

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

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

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

01:53:08 Finished HOL-Analysis (0:09:49 elapsed time, 0:44:24 cpu time, factor 4.52)

01:53:08 Building Ordinary_Differential_Equations ...

01:53:10 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order

01:53:10 Ordinary_Differential_Equations: theory HOL-Word.Misc_Numeric

01:53:10 Ordinary_Differential_Equations: theory HOL-Word.Bits

01:53:10 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int

01:53:10 Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat

01:53:10 Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence

01:53:10 Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras

01:53:10 Ordinary_Differential_Equations: theory HOL-Library.Log_Nat

01:53:10 Ordinary_Differential_Equations: theory HOL-Word.Bit_Representation

01:53:10 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat

01:53:10 Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities

01:53:11 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator

01:53:11 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Vector_Derivative_On

01:53:11 Ordinary_Differential_Equations: theory Triangle.Angles

01:53:11 Ordinary_Differential_Equations: theory List-Index.List_Index

01:53:11 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral

01:53:11 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Gronwall

01:53:11 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Interval_Integral_HK

01:53:11 Ordinary_Differential_Equations: theory Triangle.Triangle

01:53:11 Ordinary_Differential_Equations: theory HOL-Word.Bits_Int

01:53:14 Ordinary_Differential_Equations: theory HOL-Word.Bool_List_Representation

01:53:17 Ordinary_Differential_Equations: theory HOL-Library.Float

01:53:20 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds

01:53:20 Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space

01:53:26 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation

01:53:28 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities

01:53:29 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones

01:53:29 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem

01:53:29 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor

01:53:33 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative

01:53:34 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow

01:53:39 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map

01:53:39 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution

01:53:40 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE

01:53:42 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis

01:54:30 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex

01:54:32 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis

01:55:44 Timing Ordinary_Differential_Equations (8 threads, 113.474s elapsed time, 573.764s cpu time, 21.696s GC time, factor 5.06)

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

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

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

01:55:44 Finished Ordinary_Differential_Equations (0:02:34 elapsed time, 0:10:51 cpu time, factor 4.22)

01:55:44 Building HOL-ODE ...

01:55:48 Timing HOL-ODE (8 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

01:55:48 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE

01:55:48 Finished HOL-ODE (0:00:02 elapsed time)

01:55:48 Building HOL-ODE-Refinement ...

01:55:50 HOL-ODE-Refinement: theory HOL-Eisbach.Eisbach

01:55:50 HOL-ODE-Refinement: theory Automatic_Refinement.Foldi

01:55:50 HOL-ODE-Refinement: theory Automatic_Refinement.Prio_List

01:55:50 HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1

01:55:50 HOL-ODE-Refinement: theory Deriving.Derive_Manager

01:55:50 HOL-ODE-Refinement: theory Deriving.Generator_Aux

01:55:50 HOL-ODE-Refinement: theory Deriving.Comparator

01:55:50 HOL-ODE-Refinement: theory HOL-Library.AList

01:55:50 HOL-ODE-Refinement: theory HOL-Library.Adhoc_Overloading

01:55:50 HOL-ODE-Refinement: theory Automatic_Refinement.Mk_Term_Antiquot

01:55:50 HOL-ODE-Refinement: theory Automatic_Refinement.Mpat_Antiquot

01:55:50 HOL-ODE-Refinement: theory HOL-Library.Monad_Syntax

01:55:50 HOL-ODE-Refinement: theory HOL-Library.Bit

01:55:50 HOL-ODE-Refinement: theory HOL-Library.Boolean_Algebra

01:55:50 HOL-ODE-Refinement: theory HOL-Library.Permutation

01:55:50 HOL-ODE-Refinement: theory Deriving.Equality_Generator

01:55:50 HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Util

01:55:51 HOL-ODE-Refinement: theory HOL-ex.Quicksort

01:55:51 HOL-ODE-Refinement: theory HOL-Library.Char_ord

01:55:51 HOL-ODE-Refinement: theory HOL-Library.Mapping

01:55:51 HOL-ODE-Refinement: theory Deriving.Equality_Instances

01:55:51 HOL-ODE-Refinement: theory Automatic_Refinement.Anti_Unification

01:55:51 HOL-ODE-Refinement: theory Automatic_Refinement.Attr_Comb

01:55:51 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Data

01:55:51 HOL-ODE-Refinement: theory Automatic_Refinement.Indep_Vars

01:55:51 HOL-ODE-Refinement: theory Automatic_Refinement.Mk_Record_Simp

01:55:51 HOL-ODE-Refinement: theory Automatic_Refinement.Tagged_Solver

01:55:51 HOL-ODE-Refinement: theory Automatic_Refinement.Select_Solve

01:55:51 HOL-ODE-Refinement: theory Automatic_Refinement.Named_Sorted_Thms

01:55:51 HOL-ODE-Refinement: theory HOL-Library.Option_ord

01:55:51 HOL-ODE-Refinement: theory HOL-Library.Type_Length

01:55:51 HOL-ODE-Refinement: theory HOL-Library.RBT_Impl

01:55:52 HOL-ODE-Refinement: theory HOL-Library.While_Combinator

01:55:52 HOL-ODE-Refinement: theory HOL-Word.Bits_Bit

01:55:52 HOL-ODE-Refinement: theory Deriving.Compare

01:55:52 HOL-ODE-Refinement: theory Deriving.Comparator_Generator

01:55:52 HOL-ODE-Refinement: theory Native_Word.More_Bits_Int

01:55:52 HOL-ODE-Refinement: theory Automatic_Refinement.Misc

01:55:53 HOL-ODE-Refinement: theory HOL-Word.Word_Miscellaneous

01:55:53 HOL-ODE-Refinement: theory HOL-Word.Misc_Typedef

01:55:53 HOL-ODE-Refinement: theory Deriving.Countable_Generator

01:55:53 HOL-ODE-Refinement: theory Affine_Arithmetic.Optimize_Integer

01:55:53 HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise

01:55:53 HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Form

01:55:53 HOL-ODE-Refinement: theory Deriving.Compare_Generator

01:55:53 HOL-ODE-Refinement: theory HOL-Word.Word

01:55:53 HOL-ODE-Refinement: theory Affine_Arithmetic.Optimize_Float

01:55:54 HOL-ODE-Refinement: theory Deriving.Compare_Instances

01:55:54 HOL-ODE-Refinement: theory Affine_Arithmetic.Float_Real

01:55:54 HOL-ODE-Refinement: theory Affine_Arithmetic.Floatarith_Expression

01:55:54 HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_Vector

01:55:55 HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_2D_Strict

01:55:55 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Chapter

01:55:55 HOL-ODE-Refinement: theory Show.Show

01:55:55 HOL-ODE-Refinement: theory Native_Word.Bits_Integer

01:55:56 HOL-ODE-Refinement: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary

01:55:56 HOL-ODE-Refinement: theory Affine_Arithmetic.Polygon

01:55:58 HOL-ODE-Refinement: theory Show.Show_Instances

01:56:02 HOL-ODE-Refinement: theory Affine_Arithmetic.Intersection

01:56:03 HOL-ODE-Refinement: theory Automatic_Refinement.Refine_Lib

01:56:03 HOL-ODE-Refinement: theory Collections.SetIterator

01:56:03 HOL-ODE-Refinement: theory Native_Word.Word_Misc

01:56:04 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Phases

01:56:04 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Tagging

01:56:04 HOL-ODE-Refinement: theory Automatic_Refinement.Relators

01:56:04 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Mono_Prover

01:56:05 HOL-ODE-Refinement: theory Collections.SetIteratorOperations

01:56:07 HOL-ODE-Refinement: theory Automatic_Refinement.Param_Tool

01:56:07 HOL-ODE-Refinement: theory Automatic_Refinement.Param_HOL

01:56:08 HOL-ODE-Refinement: theory Collections.Assoc_List

01:56:09 HOL-ODE-Refinement: theory Collections.Proper_Iterator

01:56:09 HOL-ODE-Refinement: theory Automatic_Refinement.Parametricity

01:56:09 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Id_Ops

01:56:10 HOL-ODE-Refinement: theory Collections.Diff_Array

01:56:10 HOL-ODE-Refinement: theory Collections.It_to_It

01:56:10 HOL-ODE-Refinement: theory Collections.SetIteratorGA

01:56:11 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Fix_Rel

01:56:12 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Translate

01:56:12 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Relator_Interface

01:56:13 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Gen_Algo

01:56:13 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Tool

01:56:15 HOL-ODE-Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL

01:56:19 HOL-ODE-Refinement: theory Native_Word.Code_Target_Bits_Int

01:56:19 HOL-ODE-Refinement: theory Native_Word.Uint

01:56:20 HOL-ODE-Refinement: theory Collections.Code_Target_ICF

01:56:20 HOL-ODE-Refinement: theory Native_Word.Uint32

01:56:22 HOL-ODE-Refinement: theory Automatic_Refinement.Automatic_Refinement

01:56:22 HOL-ODE-Refinement: theory Collections.Intf_Comp

01:56:22 HOL-ODE-Refinement: theory Collections.Idx_Iterator

01:56:23 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Misc

01:56:24 HOL-ODE-Refinement: theory Collections.HashCode

01:56:25 HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Domain

01:56:25 HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Transfer

01:56:25 HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Assert

01:56:25 HOL-ODE-Refinement: theory Collections.Intf_Hash

01:56:25 HOL-ODE-Refinement: theory Deriving.Hash_Generator

01:56:25 HOL-ODE-Refinement: theory Refine_Monadic.RefineG_Recursion

01:56:26 HOL-ODE-Refinement: theory Refine_Monadic.RefineG_While

01:56:26 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Basic

01:56:26 HOL-ODE-Refinement: theory Collections.Gen_Hash

01:56:27 HOL-ODE-Refinement: theory Deriving.Hash_Instances

01:56:27 HOL-ODE-Refinement: theory Deriving.Derive

01:56:27 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Det

01:56:30 HOL-ODE-Refinement: theory Collections.Impl_Array_Stack

01:56:32 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Heuristics

01:56:32 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Leof

01:56:32 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Pfun

01:56:32 HOL-ODE-Refinement: theory Refine_Monadic.Refine_More_Comb

01:56:32 HOL-ODE-Refinement: theory Refine_Monadic.Refine_While

01:56:34 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Transfer

01:56:35 HOL-ODE-Refinement: theory Refine_Monadic.Autoref_Monadic

01:56:35 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Automation

01:56:35 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Foreach

01:56:39 HOL-ODE-Refinement: theory Refine_Monadic.Refine_Monadic

01:56:41 HOL-ODE-Refinement: theory Collections.Gen_Iterator

01:56:41 HOL-ODE-Refinement: theory Collections.Intf_Map

01:56:41 HOL-ODE-Refinement: theory Collections.Intf_Set

01:56:42 HOL-ODE-Refinement: theory Collections.Impl_Cfun_Set

01:56:42 HOL-ODE-Refinement: theory Collections.Iterator

01:56:43 HOL-ODE-Refinement: theory Collections.Array_Iterator

01:56:43 HOL-ODE-Refinement: theory Collections.Gen_Map

01:56:43 HOL-ODE-Refinement: theory Collections.Gen_Map2Set

01:56:43 HOL-ODE-Refinement: theory Collections.Gen_Set

01:56:43 HOL-ODE-Refinement: theory Collections.Impl_Bit_Set

01:56:43 HOL-ODE-Refinement: theory Collections.Impl_List_Set

01:56:44 HOL-ODE-Refinement: theory Collections.Impl_Array_Map

01:56:44 HOL-ODE-Refinement: theory Collections.Impl_List_Map

01:56:45 HOL-ODE-Refinement: theory Collections.Impl_Uv_Set

01:56:46 HOL-ODE-Refinement: theory Collections.Impl_Array_Hash_Map

01:56:50 HOL-ODE-Refinement: theory HOL-Library.RBT

01:56:50 HOL-ODE-Refinement: theory Collections.RBT_add

01:56:51 HOL-ODE-Refinement: theory HOL-Library.RBT_Mapping

01:56:52 HOL-ODE-Refinement: theory Affine_Arithmetic.Straight_Line_Program

01:56:53 HOL-ODE-Refinement: theory Collections.Impl_RBT_Map

01:57:04 HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Approximation

01:57:12 HOL-ODE-Refinement: theory HOL-ODE-Refinement.GenCF_No_Comp

01:57:20 HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Code

01:57:21 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Dflt_No_Comp

01:57:21 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Autoref_Misc

01:57:24 HOL-ODE-Refinement: theory Affine_Arithmetic.Print

01:57:29 HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Affine_Approximation

01:57:29 HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Ineqs

01:57:30 HOL-ODE-Refinement: theory Affine_Arithmetic.Ex_Inter

01:57:32 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_Folds

01:57:32 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Refine_String

01:57:33 HOL-ODE-Refinement: theory HOL-ODE-Refinement.Weak_Set

01:58:47 HOL-ODE-Refinement: theory Affine_Arithmetic.Affine_Arithmetic

02:01:21 Timing HOL-ODE-Refinement (8 threads, 264.294s elapsed time, 1554.068s cpu time, 158.068s GC time, factor 5.88)

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

02:01:21 Finished HOL-ODE-Refinement (0:05:31 elapsed time, 0:30:19 cpu time, factor 5.49)

02:01:21 Building HOL-ODE-Numerics ...

02:01:24 HOL-ODE-Numerics: theory Collections.ICF_Tools

02:01:24 HOL-ODE-Numerics: theory HOL-Library.Parallel

02:01:24 HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets

02:01:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method

02:01:25 HOL-ODE-Numerics: theory Collections.Ord_Code_Preproc

02:01:25 HOL-ODE-Numerics: theory Collections.Locale_Code

02:01:26 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta

02:01:32 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List

02:01:45 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector

02:01:49 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics

02:05:40 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis

02:29:39 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform

02:32:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities

02:34:09 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics

04:01:25 *** Timeout

04:01:25 HOL-ODE-Numerics FAILED

04:01:25 (see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.7.1_x86_64-linux/log/HOL-ODE-Numerics)

04:01:25 int ->

04:01:25 (int * int * string) list ->

04:01:25 string -> Proof.context -> int -> tactic

04:01:25 val ode'_bnds_tac = fn:

04:01:25 thm ->

04:01:25 int ->

04:01:25 (int * int * string * int list) list ->

04:01:25 string list -> string -> Proof.context -> int -> tactic

04:01:25 val poincare_bnds_tac = fn:

04:01:25 thm ->

04:01:25 int ->

04:01:25 (int * int * string) list ->

04:01:25 string -> Proof.context -> int -> tactic

04:01:25 val poincare'_bnds_tac = fn:

04:01:25 thm ->

04:01:25 int ->

04:01:25 (int * int * string) list ->

04:01:25 string -> Proof.context -> int -> tactic

04:01:25 ### Introduced fixed type variable(s): 'b in "X__"

04:01:25 ### Rule already declared as elimination (elim)

04:01:25 ### \<lbrakk>(?f has_derivative ?f') ?F;

04:01:25 ### bounded_linear ?f' \<Longrightarrow> PROP ?W\<rbrakk>

04:01:25 ### \<Longrightarrow> PROP ?W

04:01:25 ### theory "HOL-ODE-Numerics.Example_Utilities"

04:01:25 ### 104.447s elapsed time, 322.388s cpu time, 81.996s GC time

04:01:25 Loading theory "HOL-ODE-Numerics.ODE_Numerics"

04:01:25 ### theory "HOL-ODE-Numerics.ODE_Numerics"

04:01:25 ### 0.074s elapsed time, 0.296s cpu time, 0.000s GC time

04:01:25 *** Interrupt

04:01:25 Lorenz_Approximation CANCELLED

04:01:25 Building HOL-Library ...

04:01:27 HOL-Library: theory HOL-Library.Lattice_Syntax

04:01:27 HOL-Library: theory HOL-Library.AList

04:01:27 HOL-Library: theory HOL-Library.Adhoc_Overloading

04:01:27 HOL-Library: theory HOL-Library.Boolean_Algebra

04:01:27 HOL-Library: theory HOL-Library.Cancellation

04:01:27 HOL-Library: theory HOL-Library.BNF_Axiomatization

04:01:27 HOL-Library: theory HOL-Library.BNF_Corec

04:01:27 HOL-Library: theory HOL-Library.Bit

04:01:27 HOL-Library: theory HOL-Library.Cardinal_Notations

04:01:27 HOL-Library: theory HOL-Library.Char_ord

04:01:27 HOL-Library: theory HOL-Library.Monad_Syntax

04:01:27 HOL-Library: theory HOL-Library.Code_Abstract_Nat

04:01:27 HOL-Library: theory HOL-Library.Code_Prolog

04:01:28 HOL-Library: theory HOL-Library.State_Monad

04:01:28 HOL-Library: theory HOL-Library.Code_Binary_Nat

04:01:28 HOL-Library: theory HOL-Library.Code_Target_Nat

04:01:28 HOL-Library: theory HOL-Library.Code_Target_Int

04:01:28 HOL-Library: theory HOL-Library.Code_Test

04:01:28 HOL-Library: theory HOL-Library.Combine_PER

04:01:28 HOL-Library: theory HOL-Library.Multiset

04:01:28 HOL-Library: theory HOL-Library.Code_Target_Numeral

04:01:28 HOL-Library: theory HOL-Library.Complete_Partial_Order2

04:01:28 HOL-Library: theory HOL-Library.Conditional_Parametricity

04:01:28 HOL-Library: theory HOL-Library.Datatype_Records

04:01:29 HOL-Library: theory HOL-Library.Debug

04:01:29 HOL-Library: theory HOL-Library.Disjoint_Sets

04:01:29 HOL-Library: theory HOL-Library.Dlist

04:01:30 HOL-Library: theory HOL-Library.Fun_Lexorder

04:01:30 HOL-Library: theory HOL-Library.Function_Algebras

04:01:30 HOL-Library: theory HOL-Library.Groups_Big_Fun

04:01:30 HOL-Library: theory HOL-Library.IArray

04:01:30 HOL-Library: theory HOL-Library.Function_Division

04:01:30 HOL-Library: theory HOL-Library.DAList

04:01:30 HOL-Library: theory HOL-Library.Infinite_Set

04:01:30 HOL-Library: theory HOL-Library.LaTeXsugar

04:01:30 HOL-Library: theory HOL-Library.Lattice_Constructions

04:01:31 HOL-Library: theory HOL-Library.Omega_Words_Fun

04:01:31 HOL-Library: theory HOL-Library.Ramsey

04:01:31 HOL-Library: theory HOL-Library.ListVector

04:01:31 HOL-Library: theory HOL-Library.List_lexord

04:01:31 HOL-Library: theory HOL-Library.Mapping

04:01:31 HOL-Library: theory HOL-Library.More_List

04:01:32 HOL-Library: theory HOL-Library.Nat_Bijection

04:01:32 HOL-Library: theory HOL-Library.Old_Datatype

04:01:32 HOL-Library: theory HOL-Library.Old_Recdef

04:01:32 HOL-Library: theory HOL-Library.Stream

04:01:33 HOL-Library: theory HOL-Library.Open_State_Syntax

04:01:33 HOL-Library: theory HOL-Library.Option_ord

04:01:33 HOL-Library: theory HOL-Library.AList_Mapping

04:01:33 HOL-Library: theory HOL-Library.Parallel

04:01:33 HOL-Library: theory HOL-Library.Pattern_Aliases

04:01:33 HOL-Library: theory HOL-Library.Perm

04:01:34 HOL-Library: theory HOL-Library.Phantom_Type

04:01:35 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs

04:01:35 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck

04:01:35 HOL-Library: theory HOL-Library.Preorder

04:01:35 HOL-Library: theory HOL-Library.Product_Lexorder

04:01:36 HOL-Library: theory HOL-Library.Product_Plus

04:01:36 HOL-Library: theory HOL-Library.Quotient_Syntax

04:01:36 HOL-Library: theory HOL-Library.Quotient_Option

04:01:36 HOL-Library: theory HOL-Library.Quotient_Product

04:01:36 HOL-Library: theory HOL-Library.Quotient_Set

04:01:36 HOL-Library: theory HOL-Library.Quotient_Sum

04:01:36 HOL-Library: theory HOL-Library.Product_Order

04:01:36 HOL-Library: theory HOL-Library.Quotient_Type

04:01:36 HOL-Library: theory HOL-Library.RBT_Impl

04:01:36 HOL-Library: theory HOL-Library.Cardinality

04:01:36 HOL-Library: theory HOL-Library.Quotient_List

04:01:36 HOL-Library: theory HOL-Library.Realizers

04:01:36 HOL-Library: theory HOL-Library.Finite_Lattice

04:01:37 HOL-Library: theory HOL-Library.Reflection

04:01:37 HOL-Library: theory HOL-Library.Refute

04:01:37 HOL-Library: theory HOL-Library.Rewrite

04:01:37 HOL-Library: theory HOL-Library.Set_Algebras

04:01:37 HOL-Library: theory HOL-Library.Simps_Case_Conv

04:01:38 HOL-Library: theory HOL-Library.Extended

04:01:38 HOL-Library: theory HOL-Library.Stirling

04:01:38 HOL-Library: theory HOL-Library.DAList_Multiset

04:01:38 HOL-Library: theory HOL-Library.Multiset_Order

04:01:38 HOL-Library: theory HOL-Library.Permutation

04:01:38 HOL-Library: theory HOL-Library.Permutations

04:01:38 HOL-Library: theory HOL-Library.Numeral_Type

04:01:38 HOL-Library: theory HOL-Library.Sublist

04:01:39 HOL-Library: theory HOL-Library.Transitive_Closure_Table

04:01:40 HOL-Library: theory HOL-Library.Tree

04:01:40 HOL-Library: theory HOL-Library.Uprod

04:01:40 HOL-Library: theory HOL-Library.While_Combinator

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

04:01:42 HOL-Library: theory HOL-Library.Countable

04:01:42 HOL-Library: theory HOL-Library.Saturated

04:01:42 HOL-Library: theory HOL-Library.Prefix_Order

04:01:42 HOL-Library: theory HOL-Library.Subseq_Order

04:01:42 HOL-Library: theory HOL-Library.BigO

04:01:42 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float

04:01:42 HOL-Library: theory HOL-Library.Diagonal_Subsequence

04:01:42 HOL-Library: theory HOL-Library.Discrete

04:01:43 HOL-Library: theory HOL-Library.Going_To_Filter

04:01:43 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint

04:01:43 HOL-Library: theory HOL-Library.Indicator_Function

04:01:43 HOL-Library: theory HOL-Library.Lattice_Algebras

04:01:43 HOL-Library: theory HOL-Library.Liminf_Limsup

04:01:43 HOL-Library: theory HOL-Library.Log_Nat

04:01:44 HOL-Library: theory HOL-Library.Lub_Glb

04:01:44 HOL-Library: theory HOL-Library.Multiset_Permutations

04:01:44 HOL-Library: theory HOL-Library.Countable_Set

04:01:44 HOL-Library: theory HOL-Library.FSet

04:01:44 HOL-Library: theory HOL-Library.Nonpos_Ints

04:01:44 HOL-Library: theory HOL-Library.OptionalSugar

04:01:44 HOL-Library: theory HOL-Library.Periodic_Fun

04:01:45 HOL-Library: theory HOL-Library.Countable_Complete_Lattices

04:01:45 HOL-Library: theory HOL-Library.Countable_Set_Type

04:01:45 HOL-Library: theory HOL-Library.Quadratic_Discriminant

04:01:45 HOL-Library: theory HOL-Library.Sum_of_Squares

04:01:45 HOL-Library: theory HOL-Library.Tree_Multiset

04:01:45 HOL-Library: theory HOL-Library.Tree_Real

04:01:48 HOL-Library: theory HOL-Library.Order_Continuity

04:01:49 HOL-Library: theory HOL-Library.Extended_Nat

04:01:49 HOL-Library: theory HOL-Library.Float

04:01:50 HOL-Library: theory HOL-Library.Finite_Map

04:01:50 HOL-Library: theory HOL-Library.Extended_Real

04:01:50 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams

04:01:58 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real

04:02:01 HOL-Library: theory HOL-Library.Library

04:02:26 HOL-Library: theory HOL-Library.RBT

04:02:27 HOL-Library: theory HOL-Library.RBT_Mapping

04:02:27 HOL-Library: theory HOL-Library.RBT_Set

04:04:04 Timing HOL-Library (8 threads, 87.058s elapsed time, 574.428s cpu time, 39.384s GC time, factor 6.60)

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

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

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

04:04:04 Finished HOL-Library (0:02:36 elapsed time, 0:11:51 cpu time, factor 4.55)

04:04:04 Building ConcurrentIMP ...

04:04:06 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred

04:04:06 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang

04:04:19 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg

04:04:21 ConcurrentIMP: theory ConcurrentIMP.CIMP

04:04:21 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer_ex

04:04:21 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer_ex

04:04:51 Timing ConcurrentIMP (8 threads, 20.590s elapsed time, 50.304s cpu time, 2.888s GC time, factor 2.44)

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

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

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

04:04:51 Finished ConcurrentIMP (0:00:46 elapsed time, 0:01:40 cpu time, factor 2.19)

04:04:51 Building HOL-Word ...

04:04:52 HOL-Word: theory HOL-Library.Bit

04:04:52 HOL-Word: theory HOL-Word.Bits

04:04:52 HOL-Word: theory HOL-Library.Boolean_Algebra

04:04:52 HOL-Word: theory HOL-Word.Misc_Typedef

04:04:52 HOL-Word: theory HOL-Library.Phantom_Type

04:04:52 HOL-Word: theory HOL-Word.Misc_Numeric

04:04:52 HOL-Word: theory HOL-Word.Bit_Representation

04:04:53 HOL-Word: theory HOL-Word.Bits_Bit

04:04:53 HOL-Word: theory HOL-Word.Word_Miscellaneous

04:04:54 HOL-Word: theory HOL-Word.Bits_Int

04:04:54 HOL-Word: theory HOL-Library.Cardinality

04:04:55 HOL-Word: theory HOL-Library.Numeral_Type

04:04:56 HOL-Word: theory HOL-Word.Bit_Comparison

04:04:56 HOL-Word: theory HOL-Word.Bool_List_Representation

04:04:57 HOL-Word: theory HOL-Library.Type_Length

04:04:57 HOL-Word: theory HOL-Word.Word

04:05:04 HOL-Word: theory HOL-Word.WordBitwise

04:05:04 HOL-Word: theory HOL-Word.WordExamples

04:05:25 Timing HOL-Word (8 threads, 13.425s elapsed time, 65.016s cpu time, 2.672s GC time, factor 4.84)

04:05:25 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word

04:05:25 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf

04:05:25 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf

04:05:25 Finished HOL-Word (0:00:33 elapsed time, 0:01:43 cpu time, factor 3.10)

04:05:25 Building Word_Lib ...

04:05:26 Word_Lib: theory Word_Lib.Hex_Words

04:05:26 Word_Lib: theory Word_Lib.Signed_Words

04:05:26 Word_Lib: theory Word_Lib.Enumeration

04:05:26 Word_Lib: theory HOL-Library.Sublist

04:05:26 Word_Lib: theory Word_Lib.More_Divides

04:05:26 Word_Lib: theory Word_Lib.HOL_Lemmas

04:05:27 Word_Lib: theory Word_Lib.Norm_Words

04:05:27 Word_Lib: theory Word_Lib.WordBitwise_Signed

04:05:27 Word_Lib: theory Word_Lib.Word_Syntax

04:05:28 Word_Lib: theory Word_Lib.Word_Lib

04:05:29 Word_Lib: theory Word_Lib.Word_Enum

04:05:29 Word_Lib: theory Word_Lib.Aligned

04:05:29 Word_Lib: theory Word_Lib.Word_Setup_32

04:05:29 Word_Lib: theory Word_Lib.Word_Setup_64

04:05:30 Word_Lib: theory Word_Lib.Word_Lemmas

04:05:36 Word_Lib: theory Word_Lib.Word_Lemmas_32

04:05:37 Word_Lib: theory Word_Lib.Word_Lemmas_64

04:06:56 Timing Word_Lib (8 threads, 70.799s elapsed time, 179.976s cpu time, 5.264s GC time, factor 2.54)

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

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

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

04:06:56 Finished Word_Lib (0:01:30 elapsed time, 0:03:36 cpu time, factor 2.40)

04:06:56 Building IP_Addresses ...

04:06:57 IP_Addresses: theory HOL-Eisbach.Eisbach

04:06:57 IP_Addresses: theory HOL-Library.Cancellation

04:06:57 IP_Addresses: theory HOL-Library.Infinite_Set

04:06:57 IP_Addresses: theory HOL-Library.Option_ord

04:06:57 IP_Addresses: theory IP_Addresses.NumberWang_IPv4

04:06:57 IP_Addresses: theory IP_Addresses.NumberWang_IPv6

04:06:57 IP_Addresses: theory IP_Addresses.Word_More

04:06:59 IP_Addresses: theory HOL-Library.Multiset

04:07:05 IP_Addresses: theory HOL-ex.Quicksort

04:07:05 IP_Addresses: theory Automatic_Refinement.Misc

04:07:15 IP_Addresses: theory HOL-Library.Product_Lexorder

04:07:15 IP_Addresses: theory IP_Addresses.Hs_Compat

04:07:15 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString

04:07:15 IP_Addresses: theory HOL-Library.Code_Abstract_Nat

04:07:15 IP_Addresses: theory IP_Addresses.Word_Next

04:07:15 IP_Addresses: theory IP_Addresses.WordInterval

04:07:15 IP_Addresses: theory HOL-Library.Code_Target_Nat

04:07:15 IP_Addresses: theory IP_Addresses.Lib_List_toString

04:07:15 IP_Addresses: theory IP_Addresses.Lib_Word_toString

04:07:27 IP_Addresses: theory IP_Addresses.IP_Address

04:07:27 IP_Addresses: theory IP_Addresses.WordInterval_Sorted

04:07:32 IP_Addresses: theory IP_Addresses.IPv4

04:07:32 IP_Addresses: theory IP_Addresses.Prefix_Match

04:07:32 IP_Addresses: theory IP_Addresses.IPv6

04:07:33 IP_Addresses: theory IP_Addresses.CIDR_Split

04:09:16 IP_Addresses: theory IP_Addresses.IP_Address_Parser

04:09:16 IP_Addresses: theory IP_Addresses.IP_Address_toString

04:09:18 IP_Addresses: theory IP_Addresses.Prefix_Match_toString

04:13:02 Timing IP_Addresses (8 threads, 322.014s elapsed time, 926.900s cpu time, 59.428s GC time, factor 2.88)

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

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

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

04:13:02 Finished IP_Addresses (0:06:04 elapsed time, 0:17:04 cpu time, factor 2.81)

04:13:02 Building Simple_Firewall ...

04:13:04 Simple_Firewall: theory HOL-Library.Char_ord

04:13:04 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State

04:13:04 Simple_Firewall: theory Simple_Firewall.GroupF

04:13:04 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries

04:13:04 Simple_Firewall: theory Simple_Firewall.List_Product_More

04:13:04 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString

04:13:04 Simple_Firewall: theory Simple_Firewall.Option_Helpers

04:13:04 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString

04:13:04 Simple_Firewall: theory Simple_Firewall.Iface

04:13:05 Simple_Firewall: theory Simple_Firewall.L4_Protocol

04:13:10 Simple_Firewall: theory Simple_Firewall.Simple_Packet

04:13:10 Simple_Firewall: theory Simple_Firewall.Primitives_toString

04:13:12 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax

04:13:15 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString

04:13:15 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics

04:13:19 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw

04:13:19 Simple_Firewall: theory Simple_Firewall.Shadowed

04:13:19 Simple_Firewall: theory Simple_Firewall.Service_Matrix

04:14:01 Timing Simple_Firewall (8 threads, 24.835s elapsed time, 96.028s cpu time, 5.040s GC time, factor 3.87)

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

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

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

04:14:01 Finished Simple_Firewall (0:00:58 elapsed time, 0:02:43 cpu time, factor 2.80)

04:14:01 Building Routing ...

04:14:03 Routing: theory Routing.Linorder_Helper

04:14:03 Routing: theory HOL-Library.Adhoc_Overloading

04:14:03 Routing: theory HOL-Library.Monad_Syntax

04:14:04 Routing: theory Routing.Routing_Table

04:14:09 Routing: theory Routing.IpRoute_Parser

04:14:09 Routing: theory Routing.Linux_Router

04:14:34 Timing Routing (8 threads, 11.899s elapsed time, 34.568s cpu time, 1.028s GC time, factor 2.91)

04:14:34 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing

04:14:34 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf

04:14:34 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf

04:14:34 Finished Routing (0:00:32 elapsed time, 0:01:12 cpu time, factor 2.27)

04:14:34 Building Iptables_Semantics ...

04:14:36 Iptables_Semantics: theory HOL-Library.Code_Target_Int

04:14:36 Iptables_Semantics: theory HOL-Library.LaTeXsugar

04:14:36 Iptables_Semantics: theory Native_Word.More_Bits_Int

04:14:36 Iptables_Semantics: theory Iptables_Semantics.List_Misc

04:14:36 Iptables_Semantics: theory Iptables_Semantics.Negation_Type

04:14:38 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists

04:14:39 Iptables_Semantics: theory Native_Word.Bits_Integer

04:14:55 Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int

04:14:58 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev

04:14:58 Iptables_Semantics: theory Iptables_Semantics.Ternary

04:14:58 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize

04:14:58 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State

04:14:58 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags

04:14:58 Iptables_Semantics: theory Iptables_Semantics.IpAddresses

04:14:58 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF

04:14:58 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors

04:14:58 Iptables_Semantics: theory Iptables_Semantics.Word_Upto

04:14:59 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common

04:15:00 Iptables_Semantics: theory Iptables_Semantics.Ports

04:15:00 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet

04:15:02 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax

04:15:16 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary

04:15:16 Iptables_Semantics: theory Iptables_Semantics.Semantics

04:15:16 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto

04:15:18 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics

04:15:19 Iptables_Semantics: theory Iptables_Semantics.Matching

04:15:19 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful

04:15:19 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update

04:15:19 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding

04:15:20 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary

04:15:21 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs

04:15:21 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings

04:15:22 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action

04:15:22 Iptables_Semantics: theory Iptables_Semantics.Optimizing

04:15:22 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic

04:15:23 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches

04:15:24 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching

04:15:26 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization

04:15:29 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher

04:15:31 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold

04:15:31 Iptables_Semantics: theory Iptables_Semantics.Ipassmt

04:15:36 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt

04:16:30 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas

04:16:30 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform

04:16:30 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString

04:16:30 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics

04:16:31 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize

04:16:31 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize

04:16:31 Iptables_Semantics: theory Iptables_Semantics.No_Spoof

04:16:31 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize

04:16:31 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize

04:16:42 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace

04:16:46 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace

04:16:55 Iptables_Semantics: theory Iptables_Semantics.Transform

04:17:01 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract

04:17:03 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance

04:17:09 Iptables_Semantics: theory Iptables_Semantics.Code_Interface

04:17:09 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings

04:17:11 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings

04:17:11 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics

04:17:11 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings

04:17:19 Iptables_Semantics: theory Iptables_Semantics.Parser

04:17:19 Iptables_Semantics: theory Iptables_Semantics.Documentation

04:17:20 Iptables_Semantics: theory Iptables_Semantics.Code_haskell

04:18:45 Timing Iptables_Semantics (8 threads, 187.099s elapsed time, 722.256s cpu time, 66.160s GC time, factor 3.86)

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

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

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

04:18:45 Finished Iptables_Semantics (0:04:08 elapsed time, 0:15:00 cpu time, factor 3.62)

04:18:45 Building Iptables_Semantics_Examples ...

04:18:48 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall

04:18:48 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing

04:18:48 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company

04:18:48 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof

04:18:48 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example

04:18:48 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com

04:18:48 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6

04:18:48 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test

04:18:49 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test

04:18:55 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail

04:18:55 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples

04:18:56 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed

04:18:57 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation

04:24:38 Timing Iptables_Semantics_Examples (8 threads, 324.020s elapsed time, 2011.604s cpu time, 195.944s GC time, factor 6.21)

04:24:38 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples

04:24:38 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf

04:24:38 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf

04:24:38 Finished Iptables_Semantics_Examples (0:05:53 elapsed time, 0:34:28 cpu time, factor 5.86)

04:24:38 Running Iptables_Semantics_Examples_Big ...

04:24:41 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern

04:24:41 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated

04:24:41 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small

04:24:41 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3

04:24:41 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall

04:29:42 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large

05:50:15 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW

06:45:51 Timing Iptables_Semantics_Examples_Big (8 threads, 8456.043s elapsed time, 44313.864s cpu time, 15730.388s GC time, factor 5.24)

06:45:51 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big

06:45:51 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/document.pdf

06:45:51 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/outline.pdf

06:45:51 Finished Iptables_Semantics_Examples_Big (2:21:10 elapsed time, 12:18:57 cpu time, factor 5.23)

06:45:51 Running Flyspeck-Tame ...

06:45:53 Flyspeck-Tame: theory Flyspeck-Tame.ListAux

06:45:53 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order

06:45:53 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl

06:45:53 Flyspeck-Tame: theory HOL-Library.AList

06:45:53 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat

06:45:53 Flyspeck-Tame: theory HOL-Library.Code_Target_Int

06:45:53 Flyspeck-Tame: theory HOL-Library.IArray

06:45:53 Flyspeck-Tame: theory HOL-Library.While_Combinator

06:45:53 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat

06:45:53 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso

06:45:53 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral

06:45:54 Flyspeck-Tame: theory Flyspeck-Tame.Arch

06:45:54 Flyspeck-Tame: theory Flyspeck-Tame.Worklist

06:45:55 Flyspeck-Tame: theory Flyspeck-Tame.ListSum

06:45:55 Flyspeck-Tame: theory Flyspeck-Tame.Rotation

06:45:55 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax

06:45:55 Flyspeck-Tame: theory Flyspeck-Tame.Graph

06:45:55 Flyspeck-Tame: theory Flyspeck-Tame.Maps

06:45:56 Flyspeck-Tame: theory Trie.Trie

06:45:58 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision

06:45:58 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps

06:45:59 Flyspeck-Tame: theory Flyspeck-Tame.Tame

06:46:00 Flyspeck-Tame: theory Trie.Tries

06:46:00 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator

06:46:01 Flyspeck-Tame: theory Flyspeck-Tame.TameProps

06:46:01 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps

06:46:01 Flyspeck-Tame: theory Flyspeck-Tame.Plane

06:46:02 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps

06:46:02 Flyspeck-Tame: theory Flyspeck-Tame.Plane1

06:46:02 Flyspeck-Tame: theory Flyspeck-Tame.Generator

06:46:03 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum

06:46:08 Flyspeck-Tame: theory Flyspeck-Tame.Invariants

06:46:10 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux

06:46:11 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps

06:46:11 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps

06:46:11 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props

06:46:13 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound

06:46:13 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps

06:46:14 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps

06:46:14 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps

06:46:14 Flyspeck-Tame: theory Flyspeck-Tame.ArchComp

06:46:15 Flyspeck-Tame: theory Flyspeck-Tame.Completeness

16:04:55 Timing Flyspeck-Tame (8 threads, 33523.651s elapsed time, 50107.868s cpu time, 4744.012s GC time, factor 1.49)

16:04:55 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame

16:04:55 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf

16:04:55 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf

16:04:55 Finished Flyspeck-Tame (9:18:56 elapsed time, 13:55:28 cpu time, factor 1.49)

16:04:55 Running AODV ...

16:04:57 AODV: theory AODV.Aodv_Basic

16:05:00 AODV: theory AODV.A_Norreqid

16:05:00 AODV: theory AODV.Aodv_Data

16:05:00 AODV: theory AODV.Aodv_Message

16:05:00 AODV: theory AODV.B_Fwdrreps

16:05:00 AODV: theory AODV.D_Fwdrreqs

16:05:00 AODV: theory AODV.C_Gtobcast

16:05:00 AODV: theory AODV.E_All_ABCD

16:05:00 AODV: theory AODV.A_Aodv_Data

16:05:00 AODV: theory AODV.A_Aodv_Message

16:05:00 AODV: theory AODV.D_Aodv_Data

16:05:00 AODV: theory AODV.C_Aodv_Data

16:05:00 AODV: theory AODV.C_Aodv_Message

16:05:00 AODV: theory AODV.B_Aodv_Data

16:05:02 AODV: theory AODV.B_Aodv_Message

16:05:02 AODV: theory AODV.C_Fresher

16:05:02 AODV: theory AODV.A_Fresher

16:05:02 AODV: theory AODV.Fresher

16:05:02 AODV: theory AODV.D_Aodv_Message

16:05:02 AODV: theory AODV.E_Aodv_Data

16:05:02 AODV: theory AODV.B_Fresher

16:05:02 AODV: theory AODV.D_Fresher

16:05:03 AODV: theory AODV.E_Aodv_Message

16:05:03 AODV: theory AODV.A_Aodv

16:05:03 AODV: theory AODV.Aodv

16:05:03 AODV: theory AODV.C_Aodv

16:05:04 AODV: theory AODV.B_Aodv

16:05:04 AODV: theory AODV.E_Fresher

16:05:04 AODV: theory AODV.D_Aodv

16:05:05 AODV: theory AODV.E_Aodv

16:06:12 AODV: theory AODV.A_Aodv_Predicates

16:06:12 AODV: theory AODV.A_OAodv

16:06:13 AODV: theory AODV.A_Loop_Freedom

16:06:13 AODV: theory AODV.A_Quality_Increases

16:06:13 AODV: theory AODV.A_Seq_Invariants

16:06:14 AODV: theory AODV.A_Global_Invariants

16:06:15 AODV: theory AODV.A_Aodv_Loop_Freedom

16:06:19 AODV: theory AODV.C_Aodv_Predicates

16:06:19 AODV: theory AODV.C_Loop_Freedom

16:06:19 AODV: theory AODV.C_Quality_Increases

16:06:20 AODV: theory AODV.C_Seq_Invariants

16:06:21 AODV: theory AODV.C_OAodv

16:06:22 AODV: theory AODV.C_Global_Invariants

16:06:23 AODV: theory AODV.C_Aodv_Loop_Freedom

16:06:34 AODV: theory AODV.Aodv_Predicates

16:06:34 AODV: theory AODV.OAodv

16:06:34 AODV: theory AODV.Loop_Freedom

16:06:34 AODV: theory AODV.Quality_Increases

16:06:35 AODV: theory AODV.Seq_Invariants

16:06:35 AODV: theory AODV.Global_Invariants

16:06:37 AODV: theory AODV.Aodv_Loop_Freedom

16:06:38 AODV: theory AODV.E_Aodv_Predicates

16:06:38 AODV: theory AODV.E_OAodv

16:06:38 AODV: theory AODV.E_Loop_Freedom

16:06:39 AODV: theory AODV.E_Quality_Increases

16:06:39 AODV: theory AODV.E_Seq_Invariants

16:06:39 AODV: theory AODV.B_Aodv_Predicates

16:06:40 AODV: theory AODV.B_OAodv

16:06:40 AODV: theory AODV.E_Global_Invariants

16:06:40 AODV: theory AODV.B_Loop_Freedom

16:06:40 AODV: theory AODV.B_Quality_Increases

16:06:40 AODV: theory AODV.B_Seq_Invariants

16:06:41 AODV: theory AODV.E_Aodv_Loop_Freedom

16:06:41 AODV: theory AODV.B_Global_Invariants

16:06:43 AODV: theory AODV.B_Aodv_Loop_Freedom

16:06:48 AODV: theory AODV.D_Aodv_Predicates

16:06:49 AODV: theory AODV.D_Loop_Freedom

16:06:49 AODV: theory AODV.D_Quality_Increases

16:06:49 AODV: theory AODV.D_Seq_Invariants

16:06:49 AODV: theory AODV.D_OAodv

16:06:50 AODV: theory AODV.D_Global_Invariants

16:06:51 AODV: theory AODV.D_Aodv_Loop_Freedom

16:06:57 AODV: theory AODV.All

18:25:18 Timing AODV (8 threads, 8404.545s elapsed time, 47030.832s cpu time, 2354.192s GC time, factor 5.60)

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

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

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

18:25:18 Finished AODV (2:20:21 elapsed time, 13:04:18 cpu time, factor 5.59)

18:25:18 Running ConcurrentGC ...

18:25:20 ConcurrentGC: theory ConcurrentGC.Model

18:25:40 ConcurrentGC: theory ConcurrentGC.Tactics

18:25:50 ConcurrentGC: theory ConcurrentGC.Proofs_basis

18:25:54 ConcurrentGC: theory ConcurrentGC.TSO

18:26:13 ConcurrentGC: theory ConcurrentGC.Handshakes

18:30:27 ConcurrentGC: theory ConcurrentGC.MarkObject

18:34:57 ConcurrentGC: theory ConcurrentGC.StrongTricolour

18:36:27 ConcurrentGC: theory ConcurrentGC.Proofs

18:36:31 ConcurrentGC: theory ConcurrentGC.Concrete_heap

18:36:35 ConcurrentGC: theory ConcurrentGC.Concrete

20:55:36 Timing ConcurrentGC (8 threads, 9007.545s elapsed time, 32389.276s cpu time, 2218.652s GC time, factor 3.60)

20:55:36 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC

20:55:36 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf

20:55:36 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf

20:55:36 Finished ConcurrentGC (2:30:15 elapsed time, 9:00:01 cpu time, factor 3.59)

20:55:36 Running JinjaThreads ...

20:55:39 JinjaThreads: theory HOL-Eisbach.Eisbach

20:55:39 JinjaThreads: theory HOL-Library.Lattice_Syntax

20:55:39 JinjaThreads: theory Automatic_Refinement.Prio_List

20:55:39 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1

20:55:39 JinjaThreads: theory Automatic_Refinement.Foldi

20:55:39 JinjaThreads: theory Collections.ICF_Tools

20:55:39 JinjaThreads: theory Finger-Trees.FingerTree

20:55:39 JinjaThreads: theory HOL-Library.AList

20:55:39 JinjaThreads: theory HOL-Library.Adhoc_Overloading

20:55:39 JinjaThreads: theory HOL-Library.Bit

20:55:39 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot

20:55:39 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot

20:55:39 JinjaThreads: theory Collections.Ord_Code_Preproc

20:55:39 JinjaThreads: theory HOL-Library.Monad_Syntax

20:55:40 JinjaThreads: theory Collections.Locale_Code

20:55:40 JinjaThreads: theory Collections.Record_Intf

20:55:40 JinjaThreads: theory HOL-Library.Boolean_Algebra

20:55:40 JinjaThreads: theory HOL-Library.Cancellation

20:55:40 JinjaThreads: theory Automatic_Refinement.Refine_Util

20:55:40 JinjaThreads: theory HOL-Library.Code_Abstract_Nat

20:55:40 JinjaThreads: theory HOL-Library.Code_Target_Nat

20:55:40 JinjaThreads: theory HOL-Library.Code_Target_Int

20:55:40 JinjaThreads: theory HOL-Library.Complete_Partial_Order2

20:55:40 JinjaThreads: theory HOL-Library.Dlist

20:55:40 JinjaThreads: theory HOL-Library.Infinite_Set

20:55:41 JinjaThreads: theory HOL-Library.Code_Target_Numeral

20:55:41 JinjaThreads: theory Automatic_Refinement.Anti_Unification

20:55:41 JinjaThreads: theory Automatic_Refinement.Attr_Comb

20:55:41 JinjaThreads: theory Automatic_Refinement.Autoref_Data

20:55:41 JinjaThreads: theory Automatic_Refinement.Indep_Vars

20:55:41 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp

20:55:41 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms

20:55:41 JinjaThreads: theory Automatic_Refinement.Tagged_Solver

20:55:41 JinjaThreads: theory Automatic_Refinement.Select_Solve

20:55:41 JinjaThreads: theory HOL-Library.Multiset

20:55:41 JinjaThreads: theory HOL-Library.Nat_Bijection

20:55:41 JinjaThreads: theory HOL-Library.Old_Datatype

20:55:41 JinjaThreads: theory HOL-Library.Option_ord

20:55:42 JinjaThreads: theory HOL-Library.Phantom_Type

20:55:42 JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs

20:55:42 JinjaThreads: theory HOL-Library.RBT_Impl

20:55:42 JinjaThreads: theory Trie.Trie

20:55:42 JinjaThreads: theory HOL-Library.Simps_Case_Conv

20:55:43 JinjaThreads: theory HOL-Library.Sublist

20:55:43 JinjaThreads: theory HOL-Library.Transitive_Closure_Table

20:55:43 JinjaThreads: theory HOL-Library.Cardinality

20:55:43 JinjaThreads: theory HOL-Library.While_Combinator

20:55:44 JinjaThreads: theory Collections.DatRef

20:55:45 JinjaThreads: theory FinFun.FinFun

20:55:45 JinjaThreads: theory HOL-Library.Numeral_Type

20:55:45 JinjaThreads: theory HOL-Word.Bits

20:55:45 JinjaThreads: theory HOL-Word.Bits_Bit

20:55:45 JinjaThreads: theory HOL-Word.Misc_Numeric

20:55:46 JinjaThreads: theory HOL-Word.Bit_Representation

20:55:46 JinjaThreads: theory HOL-Word.Word_Miscellaneous

20:55:47 JinjaThreads: theory HOL-Word.Misc_Typedef

20:55:47 JinjaThreads: theory HOL-Library.Countable

20:55:47 JinjaThreads: theory HOL-Word.Bits_Int

20:55:47 JinjaThreads: theory JinjaThreads.Set_Monad

20:55:47 JinjaThreads: theory JinjaThreads.Set_without_equal

20:55:47 JinjaThreads: theory Refine_Monadic.Refine_Chapter

20:55:48 JinjaThreads: theory HOL-Library.Type_Length

20:55:49 JinjaThreads: theory HOL-Library.Countable_Set

20:55:50 JinjaThreads: theory HOL-Word.Bool_List_Representation

20:55:50 JinjaThreads: theory HOL-Library.Countable_Complete_Lattices

20:55:50 JinjaThreads: theory Binomial-Heaps.BinomialHeap

20:55:50 JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap

20:55:50 JinjaThreads: theory HOL-ex.Quicksort

20:55:51 JinjaThreads: theory Native_Word.More_Bits_Int

20:55:51 JinjaThreads: theory HOL-Word.Word

20:55:51 JinjaThreads: theory Automatic_Refinement.Misc

20:55:54 JinjaThreads: theory HOL-Library.Order_Continuity

20:55:55 JinjaThreads: theory HOL-Library.Extended_Nat

20:55:56 JinjaThreads: theory Native_Word.Bits_Integer

20:55:57 JinjaThreads: theory JinjaThreads.Auxiliary

20:55:57 JinjaThreads: theory Coinductive.Coinductive_Nat

20:55:59 JinjaThreads: theory Coinductive.Coinductive_List

20:56:01 JinjaThreads: theory Native_Word.Word_Misc

20:56:02 JinjaThreads: theory Automatic_Refinement.Refine_Lib

20:56:02 JinjaThreads: theory Collections.SetIterator

20:56:02 JinjaThreads: theory Collections.Sorted_List_Operations

20:56:04 JinjaThreads: theory Automatic_Refinement.Autoref_Phases

20:56:04 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging

20:56:04 JinjaThreads: theory Automatic_Refinement.Relators

20:56:04 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover

20:56:05 JinjaThreads: theory Collections.SetIteratorOperations

20:56:06 JinjaThreads: theory Automatic_Refinement.Param_Tool

20:56:06 JinjaThreads: theory Automatic_Refinement.Param_HOL

20:56:08 JinjaThreads: theory Collections.Assoc_List

20:56:08 JinjaThreads: theory Automatic_Refinement.Parametricity

20:56:08 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops

20:56:09 JinjaThreads: theory Collections.Dlist_add

20:56:09 JinjaThreads: theory Collections.Proper_Iterator

20:56:09 JinjaThreads: theory Collections.SetIteratorGA

20:56:09 JinjaThreads: theory Collections.Diff_Array

20:56:09 JinjaThreads: theory Collections.Trie_Impl

20:56:10 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel

20:56:10 JinjaThreads: theory Collections.It_to_It

20:56:11 JinjaThreads: theory Collections.Trie2

20:56:11 JinjaThreads: theory Automatic_Refinement.Autoref_Translate

20:56:11 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface

20:56:11 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo

20:56:11 JinjaThreads: theory Coinductive.Lazy_LList

20:56:11 JinjaThreads: theory Coinductive.TLList

20:56:11 JinjaThreads: theory Automatic_Refinement.Autoref_Tool

20:56:13 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL

20:56:19 JinjaThreads: theory Coinductive.Lazy_TLList

20:56:20 JinjaThreads: theory Native_Word.Code_Target_Bits_Int

20:56:20 JinjaThreads: theory Native_Word.Uint32

20:56:21 JinjaThreads: theory Collections.Code_Target_ICF

20:56:21 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement

20:56:21 JinjaThreads: theory Collections.Idx_Iterator

20:56:21 JinjaThreads: theory Refine_Monadic.Refine_Misc

20:56:23 JinjaThreads: theory Refine_Monadic.RefineG_Domain

20:56:23 JinjaThreads: theory Refine_Monadic.RefineG_Transfer

20:56:24 JinjaThreads: theory Refine_Monadic.RefineG_Assert

20:56:24 JinjaThreads: theory Refine_Monadic.RefineG_Recursion

20:56:24 JinjaThreads: theory Collections.HashCode

20:56:25 JinjaThreads: theory Refine_Monadic.RefineG_While

20:56:25 JinjaThreads: theory Refine_Monadic.Refine_Basic

20:56:26 JinjaThreads: theory Refine_Monadic.Refine_Det

20:56:31 JinjaThreads: theory Refine_Monadic.Refine_Heuristics

20:56:31 JinjaThreads: theory Refine_Monadic.Refine_Leof

20:56:31 JinjaThreads: theory Refine_Monadic.Refine_Pfun

20:56:32 JinjaThreads: theory Refine_Monadic.Refine_More_Comb

20:56:32 JinjaThreads: theory Refine_Monadic.Refine_While

20:56:34 JinjaThreads: theory Refine_Monadic.Refine_Transfer

20:56:35 JinjaThreads: theory Refine_Monadic.Autoref_Monadic

20:56:35 JinjaThreads: theory Refine_Monadic.Refine_Automation

20:56:35 JinjaThreads: theory Refine_Monadic.Refine_Foreach

20:56:39 JinjaThreads: theory Refine_Monadic.Refine_Monadic

20:56:40 JinjaThreads: theory Collections.Gen_Iterator

20:56:40 JinjaThreads: theory Collections.Intf_Map

20:56:40 JinjaThreads: theory Collections.Intf_Set

20:56:41 JinjaThreads: theory Collections.Iterator

20:56:42 JinjaThreads: theory Collections.Array_Iterator

20:56:42 JinjaThreads: theory Collections.ICF_Spec_Base

20:56:43 JinjaThreads: theory Collections.AnnotatedListSpec

20:56:43 JinjaThreads: theory Collections.ListSpec

20:56:43 JinjaThreads: theory Collections.MapSpec

20:56:43 JinjaThreads: theory Collections.PrioSpec

20:56:44 JinjaThreads: theory Collections.PrioUniqueSpec

20:56:44 JinjaThreads: theory Collections.SetSpec

20:56:45 JinjaThreads: theory Collections.BinoPrioImpl

20:56:45 JinjaThreads: theory Collections.SkewPrioImpl

20:56:46 JinjaThreads: theory Collections.ListGA

20:56:46 JinjaThreads: theory HOL-Library.RBT

20:56:46 JinjaThreads: theory Collections.RBT_add

20:56:47 JinjaThreads: theory Collections.FTAnnotatedListImpl

20:56:47 JinjaThreads: theory Collections.PrioByAnnotatedList

20:56:47 JinjaThreads: theory Collections.Fifo

20:56:47 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList

20:56:50 JinjaThreads: theory Collections.Algos

20:56:50 JinjaThreads: theory Collections.SetIndex

20:56:50 JinjaThreads: theory Collections.SetIteratorCollectionsGA

20:56:50 JinjaThreads: theory Collections.FTPrioImpl

20:56:51 JinjaThreads: theory Collections.MapGA

20:56:51 JinjaThreads: theory Collections.SetGA

20:56:51 JinjaThreads: theory Collections.FTPrioUniqueImpl

20:56:55 JinjaThreads: theory Collections.ArrayMapImpl

20:56:55 JinjaThreads: theory Collections.ListMapImpl

20:56:55 JinjaThreads: theory Collections.ListMapImpl_Invar

20:56:55 JinjaThreads: theory Collections.TrieMapImpl

20:56:55 JinjaThreads: theory Collections.RBTMapImpl

20:56:57 JinjaThreads: theory Collections.ArrayHashMap_Impl

20:56:58 JinjaThreads: theory Collections.ListSetImpl

20:56:58 JinjaThreads: theory Collections.ListSetImpl_Invar

20:56:58 JinjaThreads: theory Collections.ListSetImpl_NotDist

20:56:58 JinjaThreads: theory Collections.ListSetImpl_Sorted

20:56:58 JinjaThreads: theory Collections.SetByMap

20:57:00 JinjaThreads: theory Collections.HashMap_Impl

20:57:01 JinjaThreads: theory Collections.ArraySetImpl

20:57:01 JinjaThreads: theory Collections.TrieSetImpl

20:57:01 JinjaThreads: theory Collections.RBTSetImpl

20:57:02 JinjaThreads: theory Collections.ArrayHashMap

20:57:03 JinjaThreads: theory Collections.HashMap

20:57:06 JinjaThreads: theory Collections.ArrayHashSet

20:57:06 JinjaThreads: theory Collections.HashSet

20:57:06 JinjaThreads: theory Collections.MapStdImpl

20:57:10 JinjaThreads: theory Collections.SetStdImpl

20:57:15 JinjaThreads: theory Collections.ICF_Impl

20:57:23 JinjaThreads: theory Collections.ICF_Refine_Monadic

20:57:24 JinjaThreads: theory Collections.ICF_Autoref

20:57:28 JinjaThreads: theory Collections.Collections

20:57:29 JinjaThreads: theory Collections.CollectionsV1

20:57:40 JinjaThreads: theory JinjaThreads.JT_ICF

20:57:40 JinjaThreads: theory JinjaThreads.Basic_Main

20:58:21 JinjaThreads: theory HOL-Library.Mapping

20:58:21 JinjaThreads: theory JinjaThreads.FWState

20:58:21 JinjaThreads: theory JinjaThreads.LTS

20:58:21 JinjaThreads: theory JinjaThreads.Type

20:58:21 JinjaThreads: theory HOL-Library.Prefix_Order

20:58:21 JinjaThreads: theory JinjaThreads.ListIndex

20:58:21 JinjaThreads: theory JinjaThreads.Orders

20:58:21 JinjaThreads: theory JinjaThreads.Semilat

20:58:22 JinjaThreads: theory JinjaThreads.Err

20:58:23 JinjaThreads: theory HOL-Library.AList_Mapping

20:58:23 JinjaThreads: theory JinjaThreads.Listn

20:58:23 JinjaThreads: theory JinjaThreads.Opt

20:58:23 JinjaThreads: theory JinjaThreads.Product

20:58:24 JinjaThreads: theory JinjaThreads.Semilattices

20:58:25 JinjaThreads: theory JinjaThreads.Decl

20:58:25 JinjaThreads: theory JinjaThreads.Typing_Framework

20:58:25 JinjaThreads: theory JinjaThreads.SemilatAlg

20:58:25 JinjaThreads: theory JinjaThreads.Kildall

20:58:25 JinjaThreads: theory JinjaThreads.LBVSpec

20:58:27 JinjaThreads: theory JinjaThreads.Typing_Framework_err

20:58:27 JinjaThreads: theory JinjaThreads.LBVComplete

20:58:27 JinjaThreads: theory JinjaThreads.Bisimulation

20:58:27 JinjaThreads: theory JinjaThreads.LBVCorrect

20:58:28 JinjaThreads: theory JinjaThreads.Abstract_BV

20:58:29 JinjaThreads: theory JinjaThreads.TypeRel

20:58:34 JinjaThreads: theory JinjaThreads.TypeRelRefine

20:58:34 JinjaThreads: theory JinjaThreads.Value

20:58:39 JinjaThreads: theory JinjaThreads.Exceptions

20:58:39 JinjaThreads: theory JinjaThreads.Heap

20:58:40 JinjaThreads: theory JinjaThreads.SystemClasses

20:58:42 JinjaThreads: theory JinjaThreads.MM

20:58:42 JinjaThreads: theory JinjaThreads.State

20:58:49 JinjaThreads: theory JinjaThreads.FWCondAction

20:58:50 JinjaThreads: theory JinjaThreads.FWInterrupt

20:58:50 JinjaThreads: theory JinjaThreads.FWLock

20:58:50 JinjaThreads: theory JinjaThreads.FWThread

20:58:50 JinjaThreads: theory JinjaThreads.FWWait

20:58:50 JinjaThreads: theory JinjaThreads.Observable_Events

20:58:53 JinjaThreads: theory JinjaThreads.FWLocking

20:58:54 JinjaThreads: theory JinjaThreads.FWLockingThread

20:58:54 JinjaThreads: theory JinjaThreads.FWWellform

20:58:55 JinjaThreads: theory JinjaThreads.FWLifting

20:58:55 JinjaThreads: theory JinjaThreads.FWSemantics

20:58:59 JinjaThreads: theory JinjaThreads.FWLiftingSem

20:58:59 JinjaThreads: theory JinjaThreads.FWProgressAux

20:58:59 JinjaThreads: theory JinjaThreads.JVMState

20:58:59 JinjaThreads: theory JinjaThreads.StartConfig

20:58:59 JinjaThreads: theory JinjaThreads.JMM_Spec

20:59:01 JinjaThreads: theory JinjaThreads.FWDeadlock

20:59:01 JinjaThreads: theory JinjaThreads.FWLTS

20:59:01 JinjaThreads: theory JinjaThreads.Conform

20:59:02 JinjaThreads: theory JinjaThreads.State_Refinement

20:59:04 JinjaThreads: theory JinjaThreads.ConformThreaded

20:59:05 JinjaThreads: theory JinjaThreads.ExternalCall

20:59:05 JinjaThreads: theory JinjaThreads.FWProgress

20:59:05 JinjaThreads: theory JinjaThreads.SC

20:59:06 JinjaThreads: theory JinjaThreads.SC_Collections

20:59:17 JinjaThreads: theory JinjaThreads.FWBisimulation

20:59:17 JinjaThreads: theory JinjaThreads.FWInitFinLift

20:59:18 JinjaThreads: theory JinjaThreads.Scheduler

20:59:18 JinjaThreads: theory JinjaThreads.JMM_DRF

20:59:19 JinjaThreads: theory JinjaThreads.Non_Speculative

20:59:20 JinjaThreads: theory JinjaThreads.SC_Legal

20:59:35 JinjaThreads: theory JinjaThreads.HB_Completion

20:59:35 JinjaThreads: theory JinjaThreads.SC_Completion

21:00:34 JinjaThreads: theory JinjaThreads.Random_Scheduler

21:00:35 JinjaThreads: theory JinjaThreads.Round_Robin

21:00:55 JinjaThreads: theory JinjaThreads.SC_Schedulers

21:02:07 JinjaThreads: theory JinjaThreads.FWBisimDeadlock

21:02:07 JinjaThreads: theory JinjaThreads.FWBisimLift

21:15:24 JinjaThreads: theory JinjaThreads.WellForm

21:15:24 JinjaThreads: theory JinjaThreads.ExternalCall_Execute

21:15:26 JinjaThreads: theory JinjaThreads.BinOp

21:15:26 JinjaThreads: theory JinjaThreads.ExternalCallWF

21:15:27 JinjaThreads: theory JinjaThreads.JMM_Heap

21:15:27 JinjaThreads: theory JinjaThreads.SemiType

21:15:29 JinjaThreads: theory JinjaThreads.JVM_SemiType

21:15:34 JinjaThreads: theory JinjaThreads.JMM_Framework

21:15:34 JinjaThreads: theory JinjaThreads.JMM_Type

21:15:35 JinjaThreads: theory JinjaThreads.JMM_Type2

21:15:58 JinjaThreads: theory JinjaThreads.Expr

21:15:58 JinjaThreads: theory JinjaThreads.JVMInstructions

21:15:58 JinjaThreads: theory JinjaThreads.PCompiler

21:15:58 JinjaThreads: theory JinjaThreads.Common_Main

21:16:00 JinjaThreads: theory JinjaThreads.PCompilerRefine

21:16:19 JinjaThreads: theory JinjaThreads.JVMExceptions

21:16:19 JinjaThreads: theory JinjaThreads.JVMHeap

21:16:19 JinjaThreads: theory JinjaThreads.Effect

21:16:28 JinjaThreads: theory JinjaThreads.JVMExecInstr

21:16:32 JinjaThreads: theory JinjaThreads.CallExpr

21:16:33 JinjaThreads: theory JinjaThreads.DefAss

21:16:35 JinjaThreads: theory JinjaThreads.WWellForm

21:16:35 JinjaThreads: theory JinjaThreads.JHeap

21:16:35 JinjaThreads: theory JinjaThreads.JVMExec

21:16:36 JinjaThreads: theory JinjaThreads.WellType

21:16:40 JinjaThreads: theory JinjaThreads.JVMDefensive

21:16:42 JinjaThreads: theory JinjaThreads.J1State

21:16:44 JinjaThreads: theory JinjaThreads.SmallStep

21:16:46 JinjaThreads: theory JinjaThreads.ToString

21:16:46 JinjaThreads: theory JinjaThreads.Annotate

21:16:48 JinjaThreads: theory JinjaThreads.Compiler2

21:16:48 JinjaThreads: theory JinjaThreads.J1Heap

21:16:49 JinjaThreads: theory JinjaThreads.JVMThreaded

21:16:54 JinjaThreads: theory JinjaThreads.J1

21:16:55 JinjaThreads: theory JinjaThreads.Compiler1

21:17:03 JinjaThreads: theory JinjaThreads.JMM_Typesafe

21:17:05 JinjaThreads: theory JinjaThreads.Exception_Tables

21:17:07 JinjaThreads: theory JinjaThreads.Compiler

21:17:08 JinjaThreads: theory JinjaThreads.JVM_Main

21:17:08 JinjaThreads: theory JinjaThreads.JMM_JVM

21:17:08 JinjaThreads: theory JinjaThreads.J1WellType

21:17:14 JinjaThreads: theory JinjaThreads.J1WellForm

21:17:16 JinjaThreads: theory JinjaThreads.JWellForm

21:17:16 JinjaThreads: theory JinjaThreads.WellTypeRT

21:17:19 JinjaThreads: theory JinjaThreads.JJ1WellForm

21:17:22 JinjaThreads: theory JinjaThreads.Preprocessor

21:17:24 JinjaThreads: theory JinjaThreads.JMM_Common

21:17:35 JinjaThreads: theory JinjaThreads.JMM_Typesafe2

21:17:42 JinjaThreads: theory JinjaThreads.BVSpec

21:17:42 JinjaThreads: theory JinjaThreads.EffectMono

21:17:43 JinjaThreads: theory JinjaThreads.BVConform

21:17:44 JinjaThreads: theory JinjaThreads.TypeComp

21:17:47 JinjaThreads: theory JinjaThreads.TF_JVM

21:17:51 JinjaThreads: theory JinjaThreads.J1Deadlock

21:17:54 JinjaThreads: theory JinjaThreads.BVExec

21:17:54 JinjaThreads: theory JinjaThreads.LBVJVM

21:17:59 JinjaThreads: theory JinjaThreads.BVSpecTypeSafe

21:18:15 JinjaThreads: theory JinjaThreads.BVNoTypeError

21:18:20 JinjaThreads: theory JinjaThreads.BVProgressThreaded

21:18:20 JinjaThreads: theory JinjaThreads.BCVExec

21:18:29 JinjaThreads: theory JinjaThreads.JVMTau

21:19:14 JinjaThreads: theory JinjaThreads.Execs

21:20:23 JinjaThreads: theory JinjaThreads.DefAssPreservation

21:20:26 JinjaThreads: theory JinjaThreads.Threaded

21:20:29 JinjaThreads: theory JinjaThreads.Progress

21:20:45 JinjaThreads: theory JinjaThreads.TypeSafe

21:21:41 JinjaThreads: theory JinjaThreads.J1JVMBisim

21:21:47 JinjaThreads: theory JinjaThreads.J0

21:21:47 JinjaThreads: theory JinjaThreads.JMM_J

21:21:47 JinjaThreads: theory JinjaThreads.ProgressThreaded

21:21:48 JinjaThreads: theory JinjaThreads.J_Execute

21:21:58 JinjaThreads: theory JinjaThreads.DRF_JVM

21:22:05 JinjaThreads: theory JinjaThreads.JVMDeadlocked

21:22:38 JinjaThreads: theory JinjaThreads.DRF_J

21:22:38 JinjaThreads: theory JinjaThreads.Deadlocked

21:22:52 JinjaThreads: theory JinjaThreads.J_Main

21:22:52 JinjaThreads: theory JinjaThreads.BV_Main

21:22:57 JinjaThreads: theory JinjaThreads.J0Bisim

21:22:57 JinjaThreads: theory JinjaThreads.J0J1Bisim

21:23:55 JinjaThreads: theory JinjaThreads.Correctness1

21:23:57 JinjaThreads: theory JinjaThreads.Correctness1Threaded

21:27:46 JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe

21:35:48 JinjaThreads: theory JinjaThreads.JMM_J_Typesafe

21:36:06 JinjaThreads: theory JinjaThreads.J1JVM

21:36:11 JinjaThreads: theory JinjaThreads.JVMJ1

21:37:48 JinjaThreads: theory JinjaThreads.Correctness2

21:41:05 JinjaThreads: theory JinjaThreads.JVMExec_Execute

21:41:05 JinjaThreads: theory JinjaThreads.JVMExec_Execute2

21:41:07 JinjaThreads: theory JinjaThreads.Correctness

21:41:14 JinjaThreads: theory JinjaThreads.JVM_Execute

21:41:35 JinjaThreads: theory JinjaThreads.JVM_Execute2

21:42:11 JinjaThreads: theory JinjaThreads.Code_Generation

21:42:22 JinjaThreads: theory JinjaThreads.ApprenticeChallenge

21:42:22 JinjaThreads: theory JinjaThreads.BufferExample

21:42:22 JinjaThreads: theory JinjaThreads.Java2Jinja

21:42:40 JinjaThreads: theory JinjaThreads.Examples_Main

21:45:33 JinjaThreads: theory JinjaThreads.Execute_Main

21:47:11 JinjaThreads: theory JinjaThreads.Compiler_Main

21:47:12 JinjaThreads: theory JinjaThreads.JMM_Compiler

21:47:18 JinjaThreads: theory JinjaThreads.SC_Interp

21:51:18 JinjaThreads: theory JinjaThreads.JMM_Interp

21:51:23 JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2

21:51:26 JinjaThreads: theory JinjaThreads.JMM

21:51:29 JinjaThreads: theory JinjaThreads.MM_Main

21:51:41 JinjaThreads: theory JinjaThreads.JinjaThreads

21:57:29 Timing JinjaThreads (8 threads, 3649.088s elapsed time, 16389.916s cpu time, 4438.120s GC time, factor 4.49)

21:57:29 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads

21:57:29 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf

21:57:29 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf

21:57:29 Finished JinjaThreads (1:01:49 elapsed time, 4:36:14 cpu time, factor 4.47)

21:57:29 Lorenz_C0 CANCELLED

21:57:29 Unfinished session(s): HOL-ODE-Numerics, Lorenz_Approximation, Lorenz_C0

21:57:29

21:57:29 === TIMING ===

21:57:29

21:57:29 Group slow: 17:32:33 elapsed time, 52:54:59 cpu time, factor 3.02

21:57:29 Group AFP: 20:02:20 elapsed time, 57:53:03 cpu time, factor 2.89

21:57:29 Group main: 0:18:39 elapsed time, 1:15:17 cpu time, factor 4.04

21:57:29 Group timing: 0:12:58 elapsed time, 0:57:59 cpu time, factor 4.47

21:57:29 Group very_slow: 11:40:07 elapsed time, 26:14:25 cpu time, factor 2.25

21:57:29 Overall: 20:22:34 elapsed time, 59:08:47 cpu time, factor 2.90

21:57:29

21:57:29 === FAILED SESSIONS ===

21:57:29

21:57:29 Session Lorenz_C0: CANCELLED

21:57:29 Session HOL-ODE-Numerics: FAILED 1

21:57:29 Session Lorenz_Approximation: CANCELLED

21:57:29 Build step 'Execute shell' marked build as failure

21:57:29 Archiving artifacts

21:57:30 Started calculate disk usage of build

21:57:30 Finished Calculation of disk usage of build in 0 seconds

21:57:38 Started calculate disk usage of workspace

21:57:39 Finished Calculation of disk usage of workspace in 1 second

21:57:39 No emails were triggered.

21:57:39 Finished: FAILURE