![[Jenkins]](/jenkins/static/e0654fc9/images/svgs/logo.svg){kind=logo}
[EnvInject] - Loading node environment variables.
Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow
[isabelle-nightly-slow] $ hg showconfig paths.default
[isabelle-nightly-slow] $ hg pull --rev default
pulling from http://isabelle.in.tum.de/repos/isabelle/
[isabelle-nightly-slow] $ hg update --clean --rev default
6 files updated, 0 files merged, 0 files removed, 0 files unresolved
[isabelle-nightly-slow] $ hg --config extensions.purge= clean --all
[isabelle-nightly-slow] $ hg log --rev . --template {node}
[isabelle-nightly-slow] $ hg log --rev . --template {rev}
[isabelle-nightly-slow] $ hg log --rev 52e2c99f37115936d2fbe9a5ad69ca965764fd30 --template exists\n
[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(52e2c99f37115936d2fbe9a5ad69ca965764fd30)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
pulling from https://bitbucket.org/isa-afp/afp-devel/
[afp] $ hg update --clean --rev default
6 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg --config extensions.purge= clean --all
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg log --rev 2ea64cb09ca690fb2afdc268739ba16d6a9845ba --template exists\n
[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(2ea64cb09ca690fb2afdc268739ba16d6a9845ba)" --encoding UTF-8 --encodingmode replace
[isabelle-nightly-slow] $ /bin/sh -xe /tmp/hudson2540253901185452872.sh
+ Admin/jenkins/run_build slow
### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/polyml-5.7-20170217"
Getting "https://isabelle.in.tum.de/components/polyml-5.7-20170217.tar.gz"
Unpacking "/media/data/jenkins/.isabelle/contrib/polyml-5.7-20170217.tar.gz"
### Building graph browser ...
warning: [options] bootstrap class path not set in conjunction with -source 1.4
warning: [options] source value 1.4 is obsolete and will be removed in a future release
warning: [options] target value 1.4 is obsolete and will be removed in a future release
warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.
Note: Recompile with -Xlint:deprecation for details.
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7-20170217/x86_64-linux"
Session HOL/HOL-Analysis (main timing)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/HOL-ODE-Refinement (AFP)
Session AFP/HOL-ODE-Numerics (AFP)
Session AFP/HOL-ODE-Examples (AFP slow)
Session HOL/HOL-Library (main timing)
Session AFP/ConcurrentIMP (AFP)
Session AFP/ConcurrentGC (AFP slow)
Session AFP/Flyspeck-Tame (AFP slow very_slow)
Session HOL/HOL-Word (main timing)
Session AFP/JinjaThreads (AFP slow)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP slow very_slow)
Warning: missing document directory
Timing Pure (1 threads, 0.803s elapsed time, 0.804s cpu time, 0.000s GC time, factor 1.00)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure
Finished Pure (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.99)
HOL: theory Complete_Partial_Order
HOL: theory Transitive_Closure
HOL: theory BNF_Wellorder_Relation
HOL: theory BNF_Wellorder_Embedding
HOL: theory BNF_Wellorder_Constructions
HOL: theory BNF_Cardinal_Order_Relation
HOL: theory BNF_Cardinal_Arithmetic
HOL: theory BNF_Least_Fixpoint
HOL: theory Euclidean_Division
HOL: theory Semiring_Normalization
HOL: theory Conditionally_Complete_Lattices
HOL: theory BNF_Greatest_Fixpoint
HOL: theory Quickcheck_Exhaustive
HOL: theory Quickcheck_Narrowing
HOL: theory Topological_Spaces
HOL: theory Real_Vector_Spaces
Timing HOL (8 threads, 249.295s elapsed time, 812.560s cpu time, 81.524s GC time, factor 3.26)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf
Finished HOL (0:05:34 elapsed time, 0:16:22 cpu time, factor 2.93)
HOL-Library: theory Lattice_Syntax
HOL-Library: theory BNF_Axiomatization
HOL-Library: theory Adhoc_Overloading
HOL-Library: theory Boolean_Algebra
HOL-Library: theory Cancellation
HOL-Library: theory Cardinal_Notations
HOL-Library: theory Code_Abstract_Nat
HOL-Library: theory Code_Prolog
HOL-Library: theory Code_Binary_Nat
HOL-Library: theory Code_Target_Nat
HOL-Library: theory Combine_PER
HOL-Library: theory Complete_Partial_Order2
HOL-Library: theory Disjoint_Sets
HOL-Library: theory Fraction_Field
HOL-Library: theory Fun_Lexorder
HOL-Library: theory Function_Algebras
HOL-Library: theory Code_Target_Int
HOL-Library: theory Function_Division
HOL-Library: theory Groups_Big_Fun
HOL-Library: theory Code_Target_Numeral
HOL-Library: theory Infinite_Set
HOL-Library: theory LaTeXsugar
HOL-Library: theory Lattice_Constructions
HOL-Library: theory Omega_Words_Fun
HOL-Library: theory ListVector
HOL-Library: theory List_lexord
HOL-Library: theory Misc_Numeric
HOL-Library: theory Bit_Representation
HOL-Library: theory Misc_Typedef
HOL-Library: theory Monad_Syntax
HOL-Library: theory Nat_Bijection
HOL-Library: theory Finite_Map
HOL-Library: theory Old_Datatype
HOL-Library: theory AList_Mapping
HOL-Library: theory Old_Recdef
HOL-Library: theory Option_ord
HOL-Library: theory DAList_Multiset
HOL-Library: theory Multiset_Order
HOL-Library: theory Permutation
HOL-Library: theory Permutations
HOL-Library: theory Factorial_Ring
HOL-Library: theory Bool_List_Representation
HOL-Library: theory Phantom_Type
HOL-Library: theory Predicate_Compile_Alternative_Defs
HOL-Library: theory Product_Lexorder
HOL-Library: theory Countable_Set
HOL-Library: theory Product_Plus
HOL-Library: theory Quotient_Syntax
HOL-Library: theory Quotient_Option
HOL-Library: theory Quotient_Product
HOL-Library: theory Predicate_Compile_Quickcheck
HOL-Library: theory Quotient_Set
HOL-Library: theory Product_Order
HOL-Library: theory Quotient_Sum
HOL-Library: theory Cardinality
HOL-Library: theory Quotient_Type
HOL-Library: theory Quotient_List
HOL-Library: theory Countable_Complete_Lattices
HOL-Library: theory Countable_Set_Type
HOL-Library: theory Finite_Lattice
HOL-Library: theory Reflection
HOL-Library: theory Set_Algebras
HOL-Library: theory Numeral_Type
HOL-Library: theory Simps_Case_Conv
HOL-Library: theory Type_Length
HOL-Library: theory State_Monad
HOL-Library: theory Polynomial
HOL-Library: theory Code_Real_Approx_By_Float
HOL-Library: theory Diagonal_Subsequence
HOL-Library: theory Prefix_Order
HOL-Library: theory Sublist_Order
HOL-Library: theory Indicator_Function
HOL-Library: theory Lattice_Algebras
HOL-Library: theory Liminf_Limsup
HOL-Library: theory Multiset_Permutations
HOL-Library: theory Nonpos_Ints
HOL-Library: theory OptionalSugar
HOL-Library: theory Order_Continuity
HOL-Library: theory Periodic_Fun
HOL-Library: theory Quadratic_Discriminant
HOL-Library: theory Sum_of_Squares
HOL-Library: theory Transitive_Closure_Table
HOL-Library: theory Extended_Nat
HOL-Library: theory While_Combinator
HOL-Library: theory Bourbaki_Witt_Fixpoint
HOL-Library: theory Extended_Real
HOL-Library: theory Linear_Temporal_Logic_on_Streams
HOL-Library: theory Word_Miscellaneous
HOL-Library: theory Euclidean_Algorithm
HOL-Library: theory Function_Growth
HOL-Library: theory Tree_Multiset
HOL-Library: theory Fundamental_Theorem_Algebra
HOL-Library: theory Extended_Nonnegative_Real
HOL-Library: theory Normalized_Fraction
HOL-Library: theory Field_as_Ring
HOL-Library: theory Formal_Power_Series
HOL-Library: theory Polynomial_Factorial
HOL-Library: theory Polynomial_FPS
HOL-Library: theory RBT_Mapping
Timing HOL-Library (8 threads, 160.752s elapsed time, 902.856s cpu time, 75.956s GC time, factor 5.62)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf
Finished HOL-Library (0:04:08 elapsed time, 0:18:00 cpu time, factor 4.35)
HOL-Word: theory Boolean_Algebra
HOL-Word: theory Bit_Representation
HOL-Word: theory Word_Miscellaneous
HOL-Word: theory Bool_List_Representation
Timing HOL-Word (8 threads, 15.758s elapsed time, 64.720s cpu time, 2.044s GC time, factor 4.11)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf
Finished HOL-Word (0:00:37 elapsed time, 0:01:43 cpu time, factor 2.74)
Timing AWN (8 threads, 53.246s elapsed time, 264.852s cpu time, 9.756s GC time, factor 4.97)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf
Finished AWN (0:01:57 elapsed time, 0:06:04 cpu time, factor 3.10)
ConcurrentIMP: theory CIMP_pred
ConcurrentIMP: theory CIMP_lang
ConcurrentIMP: theory CIMP_vcg
ConcurrentIMP: theory CIMP_one_place_buffer_ex
ConcurrentIMP: theory CIMP_unbounded_buffer_ex
Timing ConcurrentIMP (8 threads, 21.874s elapsed time, 53.700s cpu time, 2.864s GC time, factor 2.46)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf
Finished ConcurrentIMP (0:00:59 elapsed time, 0:02:01 cpu time, factor 2.04)
Word_Lib: theory WordBitwise_Signed
Word_Lib: theory Word_Setup_32
Word_Lib: theory Word_Setup_64
Word_Lib: theory Word_Lemmas_32
Word_Lib: theory Word_Lemmas_64
Timing Word_Lib (8 threads, 78.493s elapsed time, 192.388s cpu time, 4.652s GC time, factor 2.45)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf
Finished Word_Lib (0:01:37 elapsed time, 0:03:45 cpu time, factor 2.31)
IP_Addresses: theory Code_Abstract_Nat
IP_Addresses: theory Cancellation
IP_Addresses: theory Infinite_Set
IP_Addresses: theory Code_Target_Int
IP_Addresses: theory Option_ord
IP_Addresses: theory NumberWang_IPv4
IP_Addresses: theory NumberWang_IPv6
IP_Addresses: theory Word_More
IP_Addresses: theory Code_Target_Nat
IP_Addresses: theory Code_Char
IP_Addresses: theory Quicksort
IP_Addresses: theory List_More
IP_Addresses: theory Hs_Compat
IP_Addresses: theory Product_Lexorder
IP_Addresses: theory Lib_Numbers_toString
IP_Addresses: theory Word_Next
IP_Addresses: theory WordInterval
IP_Addresses: theory Lib_List_toString
IP_Addresses: theory Lib_Word_toString
IP_Addresses: theory IP_Address
IP_Addresses: theory WordInterval_Sorted
IP_Addresses: theory Prefix_Match
IP_Addresses: theory CIDR_Split
IP_Addresses: theory IP_Address_Parser
IP_Addresses: theory IP_Address_toString
Timing IP_Addresses (8 threads, 333.762s elapsed time, 1016.360s cpu time, 61.996s GC time, factor 3.05)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf
Finished IP_Addresses (0:06:18 elapsed time, 0:18:40 cpu time, factor 2.96)
Simple_Firewall: theory GroupF
Simple_Firewall: theory Lib_Enum_toString
Simple_Firewall: theory Option_Helpers
Simple_Firewall: theory Firewall_Common_Decision_State
Simple_Firewall: theory List_Product_More
Simple_Firewall: theory IP_Partition_Preliminaries
Simple_Firewall: theory IP_Addr_WordInterval_toString
Simple_Firewall: theory L4_Protocol
Simple_Firewall: theory Simple_Packet
Simple_Firewall: theory Primitives_toString
Simple_Firewall: theory SimpleFw_Syntax
Simple_Firewall: theory SimpleFw_Semantics
Simple_Firewall: theory Generic_SimpleFw
Simple_Firewall: theory Shadowed
Simple_Firewall: theory Service_Matrix
Timing Simple_Firewall (8 threads, 27.879s elapsed time, 108.368s cpu time, 4.264s GC time, factor 3.89)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf
Finished Simple_Firewall (0:01:04 elapsed time, 0:02:57 cpu time, factor 2.75)
Routing: theory Adhoc_Overloading
Routing: theory Linorder_Helper
Routing: theory Prefix_Match_toString
Routing: theory IpRoute_Parser
Timing Routing (8 threads, 13.537s elapsed time, 49.664s cpu time, 1.184s GC time, factor 3.67)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf
Finished Routing (0:00:40 elapsed time, 0:01:36 cpu time, factor 2.38)
Building Iptables_Semantics ...
Iptables_Semantics: theory List_Misc
Iptables_Semantics: theory LaTeXsugar
Iptables_Semantics: theory More_Bits_Int
Iptables_Semantics: theory Negation_Type
Iptables_Semantics: theory WordInterval_Lists
Iptables_Semantics: theory Bits_Integer
Iptables_Semantics: theory Code_Target_Bits_Int
Iptables_Semantics: theory Repeat_Stabilize
Iptables_Semantics: theory L4_Protocol_Flags
Iptables_Semantics: theory Ternary
Iptables_Semantics: theory Datatype_Selectors
Iptables_Semantics: theory Conntrack_State
Iptables_Semantics: theory Remdups_Rev
Iptables_Semantics: theory Negation_Type_DNF
Iptables_Semantics: theory SimpleFw_toString
Iptables_Semantics: theory Firewall_Common
Iptables_Semantics: theory IpAddresses
Iptables_Semantics: theory Word_Upto
Iptables_Semantics: theory Ports
Iptables_Semantics: theory Tagged_Packet
Iptables_Semantics: theory Common_Primitive_Syntax
Iptables_Semantics: theory Semantics
Iptables_Semantics: theory Semantics_Goto
Iptables_Semantics: theory Matching_Ternary
Iptables_Semantics: theory Matching
Iptables_Semantics: theory Semantics_Stateful
Iptables_Semantics: theory Ruleset_Update
Iptables_Semantics: theory Call_Return_Unfolding
Iptables_Semantics: theory Semantics_Ternary
Iptables_Semantics: theory Unknown_Match_Tacs
Iptables_Semantics: theory Matching_Embeddings
Iptables_Semantics: theory Fixed_Action
Iptables_Semantics: theory Optimizing
Iptables_Semantics: theory Common_Primitive_Matcher_Generic
Iptables_Semantics: theory Normalized_Matches
Iptables_Semantics: theory Negation_Type_Matching
Iptables_Semantics: theory Primitive_Normalization
Iptables_Semantics: theory Common_Primitive_Matcher
Iptables_Semantics: theory MatchExpr_Fold
Iptables_Semantics: theory Ipassmt
Iptables_Semantics: theory Routing_IpAssmt
Iptables_Semantics: theory Common_Primitive_Lemmas
Iptables_Semantics: theory Common_Primitive_toString
Iptables_Semantics: theory Conntrack_State_Transform
Iptables_Semantics: theory Example_Semantics
Iptables_Semantics: theory Interfaces_Normalize
Iptables_Semantics: theory IpAddresses_Normalize
Iptables_Semantics: theory Ports_Normalize
Iptables_Semantics: theory No_Spoof
Iptables_Semantics: theory Protocols_Normalize
Iptables_Semantics: theory Output_Interface_Replace
Iptables_Semantics: theory Interface_Replace
Iptables_Semantics: theory Transform
Iptables_Semantics: theory Primitive_Abstract
Iptables_Semantics: theory SimpleFw_Compliance
Iptables_Semantics: theory Code_Interface
Iptables_Semantics: theory Semantics_Embeddings
Iptables_Semantics: theory Iptables_Semantics
Iptables_Semantics: theory No_Spoof_Embeddings
Iptables_Semantics: theory Parser
Iptables_Semantics: theory Documentation
Iptables_Semantics: theory Code_haskell
Timing Iptables_Semantics (8 threads, 197.392s elapsed time, 831.252s cpu time, 62.596s GC time, factor 4.21)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf
Finished Iptables_Semantics (0:04:29 elapsed time, 0:17:08 cpu time, factor 3.81)
HOL-Analysis: theory Disjoint_Sets
HOL-Analysis: theory Infinite_Set
HOL-Analysis: theory Nat_Bijection
HOL-Analysis: theory Old_Datatype
HOL-Analysis: theory Cancellation
HOL-Analysis: theory Phantom_Type
HOL-Analysis: theory Product_Plus
HOL-Analysis: theory Product_Order
HOL-Analysis: theory Set_Algebras
HOL-Analysis: theory Indicator_Function
HOL-Analysis: theory Inner_Product
HOL-Analysis: theory Liminf_Limsup
HOL-Analysis: theory Nonpos_Ints
HOL-Analysis: theory Operator_Norm
HOL-Analysis: theory Cardinality
HOL-Analysis: theory Periodic_Fun
HOL-Analysis: theory Poly_Roots
HOL-Analysis: theory Sum_of_Squares
HOL-Analysis: theory Countable
HOL-Analysis: theory Product_Vector
HOL-Analysis: theory Numeral_Type
HOL-Analysis: theory Euclidean_Space
HOL-Analysis: theory Countable_Set
HOL-Analysis: theory Countable_Complete_Lattices
HOL-Analysis: theory Continuum_Not_Denumerable
HOL-Analysis: theory Norm_Arith
HOL-Analysis: theory Finite_Cartesian_Product
HOL-Analysis: theory Linear_Algebra
HOL-Analysis: theory Permutations
HOL-Analysis: theory Factorial_Ring
HOL-Analysis: theory Order_Continuity
HOL-Analysis: theory Extended_Nat
HOL-Analysis: theory Topology_Euclidean_Space
HOL-Analysis: theory Extended_Real
HOL-Analysis: theory Extended_Nonnegative_Real
HOL-Analysis: theory Summation_Tests
HOL-Analysis: theory Euclidean_Algorithm
HOL-Analysis: theory Sigma_Algebra
HOL-Analysis: theory Bounded_Linear_Function
HOL-Analysis: theory Convex_Euclidean_Space
HOL-Analysis: theory Extended_Real_Limits
HOL-Analysis: theory Tagged_Division
HOL-Analysis: theory Uniform_Limit
HOL-Analysis: theory Measurable
HOL-Analysis: theory Measure_Space
HOL-Analysis: theory Caratheodory
HOL-Analysis: theory Continuous_Extension
HOL-Analysis: theory Path_Connected
HOL-Analysis: theory Homeomorphism
HOL-Analysis: theory Brouwer_Fixpoint
HOL-Analysis: theory Derivative
HOL-Analysis: theory Cartesian_Euclidean_Space
HOL-Analysis: theory Weierstrass_Theorems
HOL-Analysis: theory Determinants
HOL-Analysis: theory Fashoda_Theorem
HOL-Analysis: theory Ordered_Euclidean_Space
HOL-Analysis: theory Arcwise_Connected
HOL-Analysis: theory Borel_Space
HOL-Analysis: theory Nonnegative_Lebesgue_Integration
HOL-Analysis: theory Regularity
HOL-Analysis: theory Binary_Product_Measure
HOL-Analysis: theory Embed_Measure
HOL-Analysis: theory Finite_Product_Measure
HOL-Analysis: theory Bochner_Integration
HOL-Analysis: theory Function_Topology
HOL-Analysis: theory Complete_Measure
HOL-Analysis: theory Radon_Nikodym
HOL-Analysis: theory Lebesgue_Measure
HOL-Analysis: theory Set_Integral
HOL-Analysis: theory Henstock_Kurzweil_Integration
HOL-Analysis: theory Bounded_Continuous_Function
HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration
HOL-Analysis: theory Integral_Test
HOL-Analysis: theory Complex_Analysis_Basics
HOL-Analysis: theory Interval_Integral
HOL-Analysis: theory Lebesgue_Integral_Substitution
HOL-Analysis: theory Complex_Transcendental
HOL-Analysis: theory Generalised_Binomial_Theorem
HOL-Analysis: theory Harmonic_Numbers
HOL-Analysis: theory Cauchy_Integral_Theorem
HOL-Analysis: theory Further_Topology
HOL-Analysis: theory Jordan_Curve
HOL-Analysis: theory Conformal_Mappings
HOL-Analysis: theory Gamma_Function
Timing HOL-Analysis (8 threads, 489.614s elapsed time, 2284.836s cpu time, 189.152s GC time, factor 4.67)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/outline.pdf
Finished HOL-Analysis (0:10:19 elapsed time, 0:41:51 cpu time, factor 4.05)
Building Ordinary_Differential_Equations ...
Ordinary_Differential_Equations: theory Code_Abstract_Nat
Ordinary_Differential_Equations: theory Code_Target_Int
Ordinary_Differential_Equations: theory Lattice_Algebras
Ordinary_Differential_Equations: theory Diagonal_Subsequence
Ordinary_Differential_Equations: theory Log_Nat
Ordinary_Differential_Equations: theory Dense_Linear_Order
Ordinary_Differential_Equations: theory Code_Target_Nat
Ordinary_Differential_Equations: theory Code_Target_Numeral
Ordinary_Differential_Equations: theory Float
Ordinary_Differential_Equations: theory Approximation
Ordinary_Differential_Equations: theory Bounded_Linear_Operator
Ordinary_Differential_Equations: theory ODE_Auxiliarities
Ordinary_Differential_Equations: theory Initial_Value_Problem
Ordinary_Differential_Equations: theory MVT_Ex
Ordinary_Differential_Equations: theory Multivariate_Taylor
Ordinary_Differential_Equations: theory Picard_Lindeloef_Qualitative
Ordinary_Differential_Equations: theory Flow
Ordinary_Differential_Equations: theory Reachability_Analysis
Ordinary_Differential_Equations: theory Upper_Lower_Solution
Ordinary_Differential_Equations: theory Linear_ODE
Ordinary_Differential_Equations: theory ODE_Analysis
Timing Ordinary_Differential_Equations (8 threads, 173.091s elapsed time, 529.324s cpu time, 14.952s GC time, factor 3.06)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/outline.pdf
Finished Ordinary_Differential_Equations (0:03:38 elapsed time, 0:10:13 cpu time, factor 2.80)
Timing HOL-ODE (8 threads, 0.188s elapsed time, 0.228s cpu time, 0.000s GC time, factor 1.21)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE
Finished HOL-ODE (0:00:31 elapsed time, 0:00:49 cpu time, factor 1.55)
Building HOL-ODE-Refinement ...
HOL-ODE-Refinement: theory AList
HOL-ODE-Refinement: theory Bit
HOL-ODE-Refinement: theory Adhoc_Overloading
HOL-ODE-Refinement: theory Bits
HOL-ODE-Refinement: theory Boolean_Algebra
HOL-ODE-Refinement: theory Quicksort
HOL-ODE-Refinement: theory Foldi
HOL-ODE-Refinement: theory Omega_Words_Fun
HOL-ODE-Refinement: theory List_More
HOL-ODE-Refinement: theory Misc_Numeric
HOL-ODE-Refinement: theory Misc_Typedef
HOL-ODE-Refinement: theory Bit_Representation
HOL-ODE-Refinement: theory Monad_Syntax
HOL-ODE-Refinement: theory Option_ord
HOL-ODE-Refinement: theory Type_Length
HOL-ODE-Refinement: theory Prio_List
HOL-ODE-Refinement: theory RBT_Impl
HOL-ODE-Refinement: theory Refine_Chapter
HOL-ODE-Refinement: theory Bits_Bit
HOL-ODE-Refinement: theory Refine_Util
HOL-ODE-Refinement: theory While_Combinator
HOL-ODE-Refinement: theory Word_Miscellaneous
HOL-ODE-Refinement: theory Misc
HOL-ODE-Refinement: theory Bits_Int
HOL-ODE-Refinement: theory Anti_Unification
HOL-ODE-Refinement: theory Attr_Comb
HOL-ODE-Refinement: theory Autoref_Data
HOL-ODE-Refinement: theory Mk_Term_Antiquot
HOL-ODE-Refinement: theory Named_Sorted_Thms
HOL-ODE-Refinement: theory Mpat_Antiquot
HOL-ODE-Refinement: theory Tagged_Solver
HOL-ODE-Refinement: theory Select_Solve
HOL-ODE-Refinement: theory Indep_Vars
HOL-ODE-Refinement: theory Mk_Record_Simp
HOL-ODE-Refinement: theory Bool_List_Representation
HOL-ODE-Refinement: theory More_Bits_Int
HOL-ODE-Refinement: theory Word
HOL-ODE-Refinement: theory Bits_Integer
HOL-ODE-Refinement: theory SetIterator
HOL-ODE-Refinement: theory Digraph_Basic
HOL-ODE-Refinement: theory Refine_Lib
HOL-ODE-Refinement: theory SetIteratorOperations
HOL-ODE-Refinement: theory Autoref_Phases
HOL-ODE-Refinement: theory Autoref_Tagging
HOL-ODE-Refinement: theory Refine_Mono_Prover
HOL-ODE-Refinement: theory Relators
HOL-ODE-Refinement: theory Word_Misc
HOL-ODE-Refinement: theory Param_Tool
HOL-ODE-Refinement: theory Param_HOL
HOL-ODE-Refinement: theory Parametricity
HOL-ODE-Refinement: theory Autoref_Id_Ops
HOL-ODE-Refinement: theory Assoc_List
HOL-ODE-Refinement: theory Proper_Iterator
HOL-ODE-Refinement: theory SetIteratorGA
HOL-ODE-Refinement: theory Diff_Array
HOL-ODE-Refinement: theory It_to_It
HOL-ODE-Refinement: theory Autoref_Fix_Rel
HOL-ODE-Refinement: theory Autoref_Translate
HOL-ODE-Refinement: theory Autoref_Relator_Interface
HOL-ODE-Refinement: theory Autoref_Gen_Algo
HOL-ODE-Refinement: theory Autoref_Tool
HOL-ODE-Refinement: theory Autoref_Bindings_HOL
HOL-ODE-Refinement: theory Automatic_Refinement
HOL-ODE-Refinement: theory Idx_Iterator
HOL-ODE-Refinement: theory Intf_Comp
HOL-ODE-Refinement: theory Code_Target_Bits_Int
HOL-ODE-Refinement: theory Refine_Misc
HOL-ODE-Refinement: theory Impl_Array_Stack
HOL-ODE-Refinement: theory Code_Target_ICF
HOL-ODE-Refinement: theory Uint
HOL-ODE-Refinement: theory Uint32
HOL-ODE-Refinement: theory RefineG_Domain
HOL-ODE-Refinement: theory RefineG_Transfer
HOL-ODE-Refinement: theory RefineG_Assert
HOL-ODE-Refinement: theory RefineG_Recursion
HOL-ODE-Refinement: theory Refine_Basic
HOL-ODE-Refinement: theory RefineG_While
HOL-ODE-Refinement: theory HashCode
HOL-ODE-Refinement: theory Refine_Det
HOL-ODE-Refinement: theory Intf_Hash
HOL-ODE-Refinement: theory Gen_Hash
HOL-ODE-Refinement: theory Refine_Heuristics
HOL-ODE-Refinement: theory Refine_Leof
HOL-ODE-Refinement: theory Refine_Pfun
HOL-ODE-Refinement: theory Refine_While
HOL-ODE-Refinement: theory Refine_Transfer
HOL-ODE-Refinement: theory Autoref_Monadic
HOL-ODE-Refinement: theory Refine_Automation
HOL-ODE-Refinement: theory Refine_Foreach
HOL-ODE-Refinement: theory Refine_Monadic
HOL-ODE-Refinement: theory Gen_Iterator
HOL-ODE-Refinement: theory Intf_Map
HOL-ODE-Refinement: theory Intf_Set
HOL-ODE-Refinement: theory Impl_Cfun_Set
HOL-ODE-Refinement: theory Iterator
HOL-ODE-Refinement: theory Array_Iterator
HOL-ODE-Refinement: theory Gen_Map
HOL-ODE-Refinement: theory Gen_Map2Set
HOL-ODE-Refinement: theory Gen_Set
HOL-ODE-Refinement: theory Impl_Bit_Set
HOL-ODE-Refinement: theory Impl_List_Set
HOL-ODE-Refinement: theory Impl_Uv_Set
HOL-ODE-Refinement: theory Impl_Array_Map
HOL-ODE-Refinement: theory Impl_List_Map
HOL-ODE-Refinement: theory Impl_Array_Hash_Map
HOL-ODE-Refinement: theory RBT_add
HOL-ODE-Refinement: theory Impl_RBT_Map
HOL-ODE-Refinement: theory GenCF_No_Comp
HOL-ODE-Refinement: theory Refine_Dflt_No_Comp
Timing HOL-ODE-Refinement (8 threads, 128.057s elapsed time, 652.880s cpu time, 32.820s GC time, factor 5.10)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Refinement
Finished HOL-ODE-Refinement (0:03:12 elapsed time, 0:14:16 cpu time, factor 4.45)
HOL-ODE-Numerics: theory Permutation
HOL-ODE-Numerics: theory Float_Real
HOL-ODE-Numerics: theory Quotient_Syntax
HOL-ODE-Numerics: theory Counterclockwise
HOL-ODE-Numerics: theory Euclidean_Space_Explicit
HOL-ODE-Numerics: theory Quotient_Set
HOL-ODE-Numerics: theory Executable_Euclidean_Space
HOL-ODE-Numerics: theory Affine_Form
HOL-ODE-Numerics: theory Counterclockwise_Vector
HOL-ODE-Numerics: theory Counterclockwise_2D_Strict
HOL-ODE-Numerics: theory Counterclockwise_2D_Arbitrary
HOL-ODE-Numerics: theory Polygon
HOL-ODE-Numerics: theory Affine_Approximation
HOL-ODE-Numerics: theory Affine_Code
HOL-ODE-Numerics: theory Straight_Line_Program
HOL-ODE-Numerics: theory Ex_Affine_Approximation
HOL-ODE-Numerics: theory Ex_Ineqs
HOL-ODE-Numerics: theory Intersection
HOL-ODE-Numerics: theory Ex_Inter
HOL-ODE-Numerics: theory Affine_Arithmetic
HOL-ODE-Numerics: theory Char_ord
HOL-ODE-Numerics: theory Derive_Manager
HOL-ODE-Numerics: theory Generator_Aux
HOL-ODE-Numerics: theory ICF_Tools
HOL-ODE-Numerics: theory Optimize_Integer
HOL-ODE-Numerics: theory One_Step_Method
HOL-ODE-Numerics: theory Autoref_Misc
HOL-ODE-Numerics: theory Ord_Code_Preproc
HOL-ODE-Numerics: theory Code_Char
HOL-ODE-Numerics: theory Locale_Code
HOL-ODE-Numerics: theory Optimize_Float
HOL-ODE-Numerics: theory Runge_Kutta
HOL-ODE-Numerics: theory Show_Instances
HOL-ODE-Numerics: theory Print
HOL-ODE-Numerics: theory Refine_Folds
HOL-ODE-Numerics: theory Refine_String
HOL-ODE-Numerics: theory Weak_Set
HOL-ODE-Numerics: theory Refine_Rigorous_Numerics
HOL-ODE-Numerics: theory Refine_Reachability_Analysis
HOL-ODE-Numerics: theory Refine_Rigorous_Numerics_Aform
HOL-ODE-Numerics: theory ODE_Numerics
Timing HOL-ODE-Numerics (8 threads, 807.152s elapsed time, 1987.356s cpu time, 108.644s GC time, factor 2.46)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Numerics
Finished HOL-ODE-Numerics (0:14:49 elapsed time, 0:35:41 cpu time, factor 2.41)
Flyspeck-Tame: theory IArray_Syntax
Flyspeck-Tame: theory Quasi_Order
Flyspeck-Tame: theory PlaneGraphIso
Flyspeck-Tame: theory Worklist
Flyspeck-Tame: theory Rotation
Flyspeck-Tame: theory Enumerator
Flyspeck-Tame: theory FaceDivision
Flyspeck-Tame: theory GraphProps
Flyspeck-Tame: theory EnumeratorProps
Flyspeck-Tame: theory TameProps
Flyspeck-Tame: theory Generator
Flyspeck-Tame: theory FaceDivisionProps
Flyspeck-Tame: theory TameEnum
Flyspeck-Tame: theory Invariants
Flyspeck-Tame: theory ArchCompAux
Flyspeck-Tame: theory PlaneProps
Flyspeck-Tame: theory Plane1Props
Flyspeck-Tame: theory ScoreProps
Flyspeck-Tame: theory LowerBound
Flyspeck-Tame: theory GeneratorProps
Flyspeck-Tame: theory TameEnumProps
Flyspeck-Tame: theory ArchCompProps
Flyspeck-Tame: theory ArchComp
Flyspeck-Tame: theory Completeness
Timing Flyspeck-Tame (8 threads, 36771.457s elapsed time, 57467.584s cpu time, 4003.580s GC time, factor 1.56)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf
Finished Flyspeck-Tame (10:13:14 elapsed time, 15:58:13 cpu time, factor 1.56)
Running Iptables_Semantics_Examples ...
Iptables_Semantics_Examples: theory Analyze_Ringofsaturn_com
Iptables_Semantics_Examples: theory Analyze_TUM_Net_Firewall
Iptables_Semantics_Examples: theory Analyze_SQRL_Shorewall
Iptables_Semantics_Examples: theory Analyze_medium_sized_company
Iptables_Semantics_Examples: theory Analyze_topos_generated
Iptables_Semantics_Examples: theory Contrived_Example
Iptables_Semantics_Examples: theory IP_Address_Space_Examples_All_Small
Iptables_Semantics_Examples: theory Parser_Test
Iptables_Semantics_Examples: theory SNS_IAS_Eduroam_Spoofing
Iptables_Semantics_Examples: theory SQRL_2015_nospoof
Iptables_Semantics_Examples: theory TUM_Spoofing_new3
Iptables_Semantics_Examples: theory Parser6
Iptables_Semantics_Examples: theory Parser6_Test
Iptables_Semantics_Examples: theory Ports_Fail
Iptables_Semantics_Examples: theory Small_Examples
Iptables_Semantics_Examples: theory iptables_Ln_tuned_parsed
Iptables_Semantics_Examples: theory Analyze_Synology_Diskstation
Build timed out (after 1,200 minutes). Marking the build as aborted.
Started calculate disk usage of build
Finished Calculation of disk usage of build in 0 seconds
Started calculate disk usage of workspace
Iptables_Semantics_Examples FAILED
(see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.7_x86_64-linux/log/Iptables_Semantics_Examples)
(MatchAnd (Match (IIface (Iface ''wlan0'')))
(MatchAnd (Match (Prot (Proto 6)))
(MatchAnd (Match (Src_Ports (L4Ports 6 [(0x14, 0x14)])))
(Match (CT_State {CT_Related, CT_Established})))))
(MatchAnd (Match (IIface (Iface ''wlan0'')))
(MatchAnd (Match (Prot (Proto 6)))
(MatchAnd (Match (Src_Ports (L4Ports 6 [(0x400, 0xFFFF)])))
(MatchAnd (Match (Dst_Ports (L4Ports 6 [(0x400, 0xFFFF)])))
(Match (CT_State {CT_Established}))))))
(MatchAnd (Match (IIface (Iface ''wlan0'')))
(MatchAnd (Match (Prot (Proto 6)))
(MatchAnd (Match (Src_Ports (L4Ports 6 [(0x19, 0x19)])))
(Match (CT_State {CT_Established})))))
(MatchAnd (Match (IIface (Iface ''wlan0'')))
(MatchAnd (Match (Prot (Proto 6)))
(Match (Dst_Ports (L4Ports 6 [(0x71, 0x71)])))))
(MatchAnd (Match (IIface (Iface ''wlan0'')))
(MatchAnd (Match (Prot (Proto 1)))
(Match (CT_State {CT_Related, CT_Established}))))
(MatchAnd (Match (IIface (Iface ''wlan0''))) (Match (Prot (Proto 0x11))))
(MatchAnd (Match (IIface (Iface ''wlan0''))) (Match (Prot (Proto 1))))
(MatchAnd (Match (IIface (Iface ''wlan0''))) (Match (Prot (Proto 6))))
Rule (Match (IIface (Iface ''wlan0''))) action.Drop,
:: "32 common_primitive rule list"
Finished Calculation of disk usage of workspace in 0 seconds