Started by an SCM change
[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/
searching for changes
no changes found
[isabelle-nightly-slow] $ hg update --clean --rev default
2 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 6be69d6881cd829a29f9c68a89acc9342970e61d --template exists\n
exists
[isabelle-nightly-slow] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(6be69d6881cd829a29f9c68a89acc9342970e61d)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
[afp] $ hg pull --rev default
pulling from https://bitbucket.org/isa-afp/afp-devel/
no changes found
[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 df890a63c1faa44510471cf646c051209c831456 --template exists\n
exists
[afp] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(df890a63c1faa44510471cf646c051209c831456)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-nightly-slow] $ /bin/sh -xe /tmp/hudson6333705301140598468.sh
+ Admin/jenkins/run_build slow
+ set -e
+ PROFILE=slow
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### 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.
4 warnings
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
+ bin/isabelle ci_build_slow
=== CONFIGURATION ===
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7-20170217/x86_64-linux"
ML_SYSTEM="polyml-5.7"
ML_OPTIONS="-H 4000 --maxheap 10G"
=== BUILD ===
Build started at Mon, 20 Feb 2017 01:35:01 +0100
Isabelle id b46fe5138cb0
Build for AFP id 901f6bfc8084
=== LOG ===
Session Pure/Pure
Session HOL/HOL (main)
Session AFP/AWN (AFP)
Session AFP/AODV (AFP slow)
Session HOL/HOL-Analysis (main timing)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/HOL-ODE (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/Word_Lib (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Routing (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP slow very_slow)
Building Pure ...
Pure: theory Pure
Pure: theory ML_Bootstrap
Warning: missing document directory
Timing Pure (1 threads, 0.817s elapsed time, 0.816s 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:20 elapsed time, 0:00:20 cpu time, factor 0.99)
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Argo
HOL: theory Ctr_Sugar
HOL: theory Orderings
HOL: theory SAT
HOL: theory Groups
HOL: theory Lattices
HOL: theory Set
HOL: theory Fun
HOL: theory Typedef
HOL: theory Rings
HOL: theory Complete_Lattices
HOL: theory Inductive
HOL: theory Sum_Type
HOL: theory Product_Type
HOL: theory Complete_Partial_Order
HOL: theory Nat
HOL: theory Fields
HOL: theory Meson
HOL: theory ATP
HOL: theory Metis
HOL: theory Finite_Set
HOL: theory Relation
HOL: theory Transitive_Closure
HOL: theory Wellfounded
HOL: theory Fun_Def_Base
HOL: theory Hilbert_Choice
HOL: theory Wfrec
HOL: theory Order_Relation
HOL: theory BNF_Wellorder_Relation
HOL: theory Zorn
HOL: theory BNF_Wellorder_Embedding
HOL: theory BNF_Wellorder_Constructions
HOL: theory BNF_Cardinal_Order_Relation
HOL: theory BNF_Cardinal_Arithmetic
HOL: theory BNF_Def
HOL: theory BNF_Composition
HOL: theory Basic_BNFs
HOL: theory BNF_Fixpoint_Base
HOL: theory BNF_Least_Fixpoint
HOL: theory Basic_BNF_LFPs
HOL: theory Transfer
HOL: theory Num
HOL: theory Power
HOL: theory Groups_Big
HOL: theory Equiv_Relations
HOL: theory Lifting
HOL: theory Lifting_Set
HOL: theory Quotient
HOL: theory Option
HOL: theory Extraction
HOL: theory Lattices_Big
HOL: theory Partial_Function
HOL: theory Fun_Def
HOL: theory Int
HOL: theory Nat_Transfer
HOL: theory Euclidean_Division
HOL: theory Parity
HOL: theory Divides
HOL: theory Code_Numeral
HOL: theory Numeral_Simprocs
HOL: theory SMT
HOL: theory Set_Interval
HOL: theory Semiring_Normalization
HOL: theory Conditionally_Complete_Lattices
HOL: theory Filter
HOL: theory Groebner_Basis
HOL: theory Presburger
HOL: theory Sledgehammer
HOL: theory List
HOL: theory Groups_List
HOL: theory Map
HOL: theory Enum
HOL: theory Random
HOL: theory String
HOL: theory BNF_Greatest_Fixpoint
HOL: theory Predicate
HOL: theory Typerep
HOL: theory Lazy_Sequence
HOL: theory Limited_Sequence
HOL: theory Code_Evaluation
HOL: theory Quickcheck_Random
HOL: theory Quickcheck_Exhaustive
HOL: theory Random_Pred
HOL: theory Quickcheck_Narrowing
HOL: theory Random_Sequence
HOL: theory Record
HOL: theory Predicate_Compile
HOL: theory Nitpick
HOL: theory Main
HOL: theory Archimedean_Field
HOL: theory Binomial
HOL: theory GCD
HOL: theory Topological_Spaces
HOL: theory Rat
HOL: theory Real
HOL: theory Real_Vector_Spaces
HOL: theory Inequalities
HOL: theory Limits
HOL: theory Deriv
HOL: theory Series
HOL: theory NthRoot
HOL: theory Transcendental
HOL: theory Complex
HOL: theory MacLaurin
HOL: theory Complex_Main
Timing HOL (8 threads, 247.945s elapsed time, 807.480s cpu time, 82.484s 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:15 cpu time, factor 2.92)
Building HOL-Library ...
HOL-Library: theory Adhoc_Overloading
HOL-Library: theory Lattice_Syntax
HOL-Library: theory AList
HOL-Library: theory BNF_Corec
HOL-Library: theory Bits
HOL-Library: theory Bit
HOL-Library: theory Stirling
HOL-Library: theory BNF_Axiomatization
HOL-Library: theory Boolean_Algebra
HOL-Library: theory Cancellation
HOL-Library: theory Cardinal_Notations
HOL-Library: theory Char_ord
HOL-Library: theory Code_Abstract_Nat
HOL-Library: theory Code_Binary_Nat
HOL-Library: theory Code_Target_Nat
HOL-Library: theory Code_Char
HOL-Library: theory Code_Prolog
HOL-Library: theory Code_Test
HOL-Library: theory Combine_PER
HOL-Library: theory Complete_Partial_Order2
HOL-Library: theory Multiset
HOL-Library: theory Bits_Bit
HOL-Library: theory Debug
HOL-Library: theory Disjoint_Sets
HOL-Library: theory Dlist
HOL-Library: theory FSet
HOL-Library: theory Fraction_Field
HOL-Library: theory Fun_Lexorder
HOL-Library: theory FuncSet
HOL-Library: theory DAList
HOL-Library: theory Function_Algebras
HOL-Library: theory Function_Division
HOL-Library: theory Code_Target_Int
HOL-Library: theory Groups_Big_Fun
HOL-Library: theory Code_Target_Numeral
HOL-Library: theory IArray
HOL-Library: theory Infinite_Set
HOL-Library: theory LaTeXsugar
HOL-Library: theory Lattice_Constructions
HOL-Library: theory ListVector
HOL-Library: theory Omega_Words_Fun
HOL-Library: theory List_lexord
HOL-Library: theory Mapping
HOL-Library: theory Misc_Numeric
HOL-Library: theory Misc_Typedef
HOL-Library: theory Bit_Representation
HOL-Library: theory Monad_Syntax
HOL-Library: theory More_List
HOL-Library: theory Nat_Bijection
HOL-Library: theory Old_Datatype
HOL-Library: theory Bits_Int
HOL-Library: theory Finite_Map
HOL-Library: theory AList_Mapping
HOL-Library: theory Stream
HOL-Library: theory Old_Recdef
HOL-Library: theory Countable
HOL-Library: theory Bool_List_Representation
HOL-Library: theory Option_ord
HOL-Library: theory Parallel
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 Perm
HOL-Library: theory Phantom_Type
HOL-Library: theory Predicate_Compile_Alternative_Defs
HOL-Library: theory Product_Lexorder
HOL-Library: theory Product_Plus
HOL-Library: theory Quotient_Syntax
HOL-Library: theory Quotient_Option
HOL-Library: theory Product_Order
HOL-Library: theory Quotient_Product
HOL-Library: theory Countable_Set
HOL-Library: theory Predicate_Compile_Quickcheck
HOL-Library: theory Quotient_Set
HOL-Library: theory Quotient_List
HOL-Library: theory Finite_Lattice
HOL-Library: theory Cardinality
HOL-Library: theory Quotient_Sum
HOL-Library: theory Quotient_Type
HOL-Library: theory RBT_Impl
HOL-Library: theory Countable_Complete_Lattices
HOL-Library: theory Countable_Set_Type
HOL-Library: theory Ramsey
HOL-Library: theory Reflection
HOL-Library: theory Refute
HOL-Library: theory Rewrite
HOL-Library: theory Set_Algebras
HOL-Library: theory FinFun
HOL-Library: theory Numeral_Type
HOL-Library: theory Simps_Case_Conv
HOL-Library: theory Extended
HOL-Library: theory Type_Length
HOL-Library: theory Saturated
HOL-Library: theory State_Monad
HOL-Library: theory Sublist
HOL-Library: theory Polynomial
HOL-Library: theory BigO
HOL-Library: theory Code_Real_Approx_By_Float
HOL-Library: theory Diagonal_Subsequence
HOL-Library: theory Discrete
HOL-Library: theory Indicator_Function
HOL-Library: theory Prefix_Order
HOL-Library: theory Sublist_Order
HOL-Library: theory Lattice_Algebras
HOL-Library: theory Liminf_Limsup
HOL-Library: theory Log_Nat
HOL-Library: theory Lub_Glb
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 Tree
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 Word
HOL-Library: theory Preorder
HOL-Library: theory Function_Growth
HOL-Library: theory Tree_Multiset
HOL-Library: theory Float
HOL-Library: theory Fundamental_Theorem_Algebra
HOL-Library: theory Extended_Nonnegative_Real
HOL-Library: theory Old_SMT
HOL-Library: theory Normalized_Fraction
HOL-Library: theory Formal_Power_Series
HOL-Library: theory Field_as_Ring
HOL-Library: theory Polynomial_Factorial
HOL-Library: theory Polynomial_FPS
HOL-Library: theory Library
HOL-Library: theory RBT
HOL-Library: theory RBT_Mapping
HOL-Library: theory RBT_Set
Timing HOL-Library (8 threads, 163.222s elapsed time, 917.944s cpu time, 75.672s 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:12 elapsed time, 0:18:18 cpu time, factor 4.36)
Building HOL-Word ...
HOL-Word: theory Bits
HOL-Word: theory Bit
HOL-Word: theory Boolean_Algebra
HOL-Word: theory Misc_Numeric
HOL-Word: theory Phantom_Type
HOL-Word: theory Misc_Typedef
HOL-Word: theory Bit_Representation
HOL-Word: theory Bits_Bit
HOL-Word: theory Word_Miscellaneous
HOL-Word: theory Bits_Int
HOL-Word: theory Cardinality
HOL-Word: theory Numeral_Type
HOL-Word: theory Bool_List_Representation
HOL-Word: theory Type_Length
HOL-Word: theory Word
Timing HOL-Word (8 threads, 13.818s elapsed time, 62.860s cpu time, 2.084s GC time, factor 4.55)
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:34 elapsed time, 0:01:40 cpu time, factor 2.94)
Building AWN ...
AWN: theory Lib
AWN: theory TransitionSystems
AWN: theory AWN
AWN: theory Invariants
AWN: theory OInvariants
AWN: theory AWN_Cterms
AWN: theory AWN_SOS
AWN: theory OAWN_SOS
AWN: theory AWN_Labels
AWN: theory Inv_Cterms
AWN: theory Pnet
AWN: theory AWN_Invariants
AWN: theory AWN_SOS_Labels
AWN: theory Closed
AWN: theory Qmsg
AWN: theory OAWN_Invariants
AWN: theory OAWN_SOS_Labels
AWN: theory ONode_Lifting
AWN: theory OPnet
AWN: theory OPnet_Lifting
AWN: theory OClosed_Lifting
AWN: theory OClosed_Transfer
AWN: theory OAWN_Convert
AWN: theory Qmsg_Lifting
AWN: theory AWN_Main
AWN: theory Toy
Timing AWN (8 threads, 53.605s elapsed time, 270.156s cpu time, 9.920s GC time, factor 5.04)
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:07 cpu time, factor 3.13)
Building ConcurrentIMP ...
ConcurrentIMP: theory CIMP_pred
ConcurrentIMP: theory CIMP_lang
ConcurrentIMP: theory CIMP_vcg
ConcurrentIMP: theory CIMP
ConcurrentIMP: theory CIMP_one_place_buffer_ex
ConcurrentIMP: theory CIMP_unbounded_buffer_ex
Timing ConcurrentIMP (8 threads, 22.506s elapsed time, 54.424s cpu time, 2.692s GC time, factor 2.42)
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:58 elapsed time, 0:02:00 cpu time, factor 2.05)
Building Word_Lib ...
Word_Lib: theory Sublist
Word_Lib: theory WordBitwise
Word_Lib: theory Prefix_Order
Word_Lib: theory HOL_Lemmas
Word_Lib: theory More_Divides
Word_Lib: theory Hex_Words
Word_Lib: theory Signed_Words
Word_Lib: theory Enumeration
Word_Lib: theory Norm_Words
Word_Lib: theory WordBitwise_Signed
Word_Lib: theory Word_Syntax
Word_Lib: theory Word_Lib
Word_Lib: theory Aligned
Word_Lib: theory Word_Enum
Word_Lib: theory Word_Setup_32
Word_Lib: theory Word_Setup_64
Word_Lib: theory Word_Lemmas
Word_Lib: theory Word_Lemmas_32
Word_Lib: theory Word_Lemmas_64
Timing Word_Lib (8 threads, 77.659s elapsed time, 192.848s cpu time, 4.708s GC time, factor 2.48)
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:36 elapsed time, 0:03:45 cpu time, factor 2.34)
Building IP_Addresses ...
IP_Addresses: theory Cancellation
IP_Addresses: theory NumberWang_IPv4
IP_Addresses: theory NumberWang_IPv6
IP_Addresses: theory Option_ord
IP_Addresses: theory Char_ord
IP_Addresses: theory Infinite_Set
IP_Addresses: theory Code_Abstract_Nat
IP_Addresses: theory Code_Target_Int
IP_Addresses: theory Word_More
IP_Addresses: theory Code_Target_Nat
IP_Addresses: theory Code_Char
IP_Addresses: theory Multiset
IP_Addresses: theory Quicksort
IP_Addresses: theory List_More
IP_Addresses: theory Misc
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 IPv4
IP_Addresses: theory IPv6
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.388s elapsed time, 1028.280s cpu time, 61.668s GC time, factor 3.08)
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:53 cpu time, factor 2.99)
Building Simple_Firewall ...
Simple_Firewall: theory Firewall_Common_Decision_State
Simple_Firewall: theory Iface
Simple_Firewall: theory Lib_Enum_toString
Simple_Firewall: theory GroupF
Simple_Firewall: theory Option_Helpers
Simple_Firewall: theory IP_Partition_Preliminaries
Simple_Firewall: theory List_Product_More
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 Shadowed
Simple_Firewall: theory Generic_SimpleFw
Simple_Firewall: theory Service_Matrix
Timing Simple_Firewall (8 threads, 27.162s elapsed time, 106.832s cpu time, 4.376s GC time, factor 3.93)
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:00 elapsed time, 0:02:53 cpu time, factor 2.90)
Building Routing ...
Routing: theory Adhoc_Overloading
Routing: theory Monad_Syntax
Routing: theory Linorder_Helper
Routing: theory Prefix_Match_toString
Routing: theory Routing_Table
Routing: theory IpRoute_Parser
Routing: theory Linux_Router
Timing Routing (8 threads, 13.317s elapsed time, 49.164s cpu time, 1.052s GC time, factor 3.69)
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:35 cpu time, factor 2.35)
Building Iptables_Semantics ...
Iptables_Semantics: theory LaTeXsugar
Iptables_Semantics: theory List_Misc
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 Conntrack_State
Iptables_Semantics: theory Negation_Type_DNF
Iptables_Semantics: theory Remdups_Rev
Iptables_Semantics: theory L4_Protocol_Flags
Iptables_Semantics: theory SimpleFw_toString
Iptables_Semantics: theory Ternary
Iptables_Semantics: theory Repeat_Stabilize
Iptables_Semantics: theory Datatype_Selectors
Iptables_Semantics: theory IpAddresses
Iptables_Semantics: theory Firewall_Common
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 Normalized_Matches
Iptables_Semantics: theory Common_Primitive_Matcher_Generic
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_toString
Iptables_Semantics: theory Common_Primitive_Lemmas
Iptables_Semantics: theory Conntrack_State_Transform
Iptables_Semantics: theory Example_Semantics
Iptables_Semantics: theory Interfaces_Normalize
Iptables_Semantics: theory No_Spoof
Iptables_Semantics: theory IpAddresses_Normalize
Iptables_Semantics: theory Ports_Normalize
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, 196.601s elapsed time, 821.944s cpu time, 62.444s GC time, factor 4.18)
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:28 elapsed time, 0:16:53 cpu time, factor 3.77)
Building HOL-Analysis ...
HOL-Analysis: theory Old_Datatype
HOL-Analysis: theory FuncSet
HOL-Analysis: theory Cancellation
HOL-Analysis: theory Product_Plus
HOL-Analysis: theory Infinite_Set
HOL-Analysis: theory Nat_Bijection
HOL-Analysis: theory Phantom_Type
HOL-Analysis: theory Disjoint_Sets
HOL-Analysis: theory Product_Order
HOL-Analysis: theory Set_Algebras
HOL-Analysis: theory L2_Norm
HOL-Analysis: theory Discrete
HOL-Analysis: theory Indicator_Function
HOL-Analysis: theory Inner_Product
HOL-Analysis: theory Multiset
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 Primes
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 Polytope
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
HOL-Analysis: theory Analysis
Timing HOL-Analysis (8 threads, 481.536s elapsed time, 2266.668s cpu time, 185.416s GC time, factor 4.71)
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:10 elapsed time, 0:41:31 cpu time, factor 4.08)
Building Ordinary_Differential_Equations ...
Ordinary_Differential_Equations: theory Code_Target_Int
Ordinary_Differential_Equations: theory Dense_Linear_Order
Ordinary_Differential_Equations: theory Code_Abstract_Nat
Ordinary_Differential_Equations: theory Lattice_Algebras
Ordinary_Differential_Equations: theory Diagonal_Subsequence
Ordinary_Differential_Equations: theory Log_Nat
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 ODE_Auxiliarities
Ordinary_Differential_Equations: theory Bounded_Linear_Operator
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, 171.157s elapsed time, 520.512s cpu time, 14.308s GC time, factor 3.04)
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:37 elapsed time, 0:10:03 cpu time, factor 2.77)
Building HOL-ODE ...
Timing HOL-ODE (8 threads, 0.173s elapsed time, 0.180s cpu time, 0.000s GC time, factor 1.04)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE
Finished HOL-ODE (0:00:32 elapsed time, 0:00:48 cpu time, factor 1.50)
Building HOL-ODE-Refinement ...
HOL-ODE-Refinement: theory Adhoc_Overloading
HOL-ODE-Refinement: theory AList
HOL-ODE-Refinement: theory Bits
HOL-ODE-Refinement: theory Omega_Words_Fun
HOL-ODE-Refinement: theory Quicksort
HOL-ODE-Refinement: theory Foldi
HOL-ODE-Refinement: theory Boolean_Algebra
HOL-ODE-Refinement: theory Bit
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 Refine_Util
HOL-ODE-Refinement: theory While_Combinator
HOL-ODE-Refinement: theory Bits_Bit
HOL-ODE-Refinement: theory Word_Miscellaneous
HOL-ODE-Refinement: theory Misc
HOL-ODE-Refinement: theory Anti_Unification
HOL-ODE-Refinement: theory Attr_Comb
HOL-ODE-Refinement: theory Bits_Int
HOL-ODE-Refinement: theory Autoref_Data
HOL-ODE-Refinement: theory Named_Sorted_Thms
HOL-ODE-Refinement: theory Mk_Term_Antiquot
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 Autoref_Phases
HOL-ODE-Refinement: theory Autoref_Tagging
HOL-ODE-Refinement: theory Refine_Mono_Prover
HOL-ODE-Refinement: theory Relators
HOL-ODE-Refinement: theory SetIteratorOperations
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 Autoref_Fix_Rel
HOL-ODE-Refinement: theory Diff_Array
HOL-ODE-Refinement: theory It_to_It
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 Code_Target_Bits_Int
HOL-ODE-Refinement: theory Uint
HOL-ODE-Refinement: theory Uint32
HOL-ODE-Refinement: theory Code_Target_ICF
HOL-ODE-Refinement: theory Automatic_Refinement
HOL-ODE-Refinement: theory Idx_Iterator
HOL-ODE-Refinement: theory Intf_Comp
HOL-ODE-Refinement: theory Refine_Misc
HOL-ODE-Refinement: theory Impl_Array_Stack
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 HashCode
HOL-ODE-Refinement: theory Refine_Basic
HOL-ODE-Refinement: theory RefineG_While
HOL-ODE-Refinement: theory Intf_Hash
HOL-ODE-Refinement: theory Refine_Det
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.105s elapsed time, 645.868s cpu time, 32.872s GC time, factor 5.04)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Refinement
Finished HOL-ODE-Refinement (0:03:10 elapsed time, 0:14:04 cpu time, factor 4.43)
Building HOL-ODE-Numerics ...
HOL-ODE-Numerics: theory Permutation
HOL-ODE-Numerics: theory Float_Real
HOL-ODE-Numerics: theory Counterclockwise
HOL-ODE-Numerics: theory Quotient_Syntax
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 ICF_Tools
HOL-ODE-Numerics: theory Generator_Aux
HOL-ODE-Numerics: theory Optimize_Integer
HOL-ODE-Numerics: theory Derive_Manager
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 Show
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 Plot
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, 801.088s elapsed time, 1981.316s cpu time, 110.880s GC time, factor 2.47)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Numerics
Finished HOL-ODE-Numerics (0:14:43 elapsed time, 0:35:36 cpu time, factor 2.42)
Running Flyspeck-Tame ...
Flyspeck-Tame: theory Trie
Flyspeck-Tame: theory Tries
Flyspeck-Tame: theory Arch
Flyspeck-Tame: theory Quasi_Order
Flyspeck-Tame: theory ListAux
Flyspeck-Tame: theory IArray_Syntax
Flyspeck-Tame: theory RTranCl
Flyspeck-Tame: theory PlaneGraphIso
Flyspeck-Tame: theory Worklist
Flyspeck-Tame: theory Maps
Flyspeck-Tame: theory ListSum
Flyspeck-Tame: theory Rotation
Flyspeck-Tame: theory Graph
Flyspeck-Tame: theory Enumerator
Flyspeck-Tame: theory FaceDivision
Flyspeck-Tame: theory GraphProps
Flyspeck-Tame: theory Tame
Flyspeck-Tame: theory Plane
Flyspeck-Tame: theory EnumeratorProps
Flyspeck-Tame: theory TameProps
Flyspeck-Tame: theory Plane1
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, 36236.825s elapsed time, 54160.820s cpu time, 899.476s GC time, factor 1.49)
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:04:18 elapsed time, 15:03:05 cpu time, factor 1.49)
Running Iptables_Semantics_Examples ...
Iptables_Semantics_Examples: theory Analyze_Ringofsaturn_com
Iptables_Semantics_Examples: theory Analyze_medium_sized_company
Iptables_Semantics_Examples: theory Analyze_SQRL_Shorewall
Iptables_Semantics_Examples: theory Analyze_topos_generated
Iptables_Semantics_Examples: theory Analyze_TUM_Net_Firewall
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
Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Failed to recover - exiting
Iptables_Semantics_Examples FAILED
(see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.7_x86_64-linux/log/Iptables_Semantics_Examples)
Rule
(MatchAnd (Match (Extra ''-d ::ffff:127.0.0.1/128''))
(MatchAnd (Match (IIface (Iface ''eth0'')))
(Match (OIface (Iface ''foobar'')))))
(Call ''gh32_-2qns''),
Rule
(MatchAnd (Match (Src (IpAddrNetmask 1 128)))
(MatchAnd (Match (IIface (Iface ''lo'')))
(Match (OIface (Iface ''lo'')))))
action.Accept,
Rule
(Match
(Extra
[CHR ''-'', CHR ''-'', CHR ''l'', CHR ''o'', CHR ''g'', CHR ''-'',
CHR ''p'', CHR ''r'', CHR ''e'', CHR ''f'', CHR ''i'', CHR ''x'',
CHR '' '', CHR 0x22, CHR ''~'', CHR ''%'', CHR ''&'', CHR ''/'',
CHR ''('', CHR '')'', CHR ''='', CHR ''?'', CHR 0x22, CHR '' '',
CHR ''-'', CHR ''-'', CHR ''l'', CHR ''o'', CHR ''g'', CHR ''-'',
CHR ''l'', CHR ''e'', CHR ''v'', CHR ''e'', CHR ''l'', CHR '' '',
CHR ''6'']))
Log,
Rule (Match (Src (IpAddrNetmask 0 128))) action.Drop]),
(''INPUT'', []), (''OUTPUT'', []),
(''gh32_-2qns'',
[Rule
(Match (Src (IpAddrNetmask 0x20010DB885A308D313198A2E03707344 128)))
Reject,
Rule MatchAny Empty, Rule MatchAny action.Accept])]"
:: "(char list \ 128 common_primitive rule list) list"
Simplified term (23462.961 seconds)
checked sanity with sanity_wf_ruleset (46.781 seconds)
Defining constant `fw11_def'
Defining constant `fw11_INPUT_default_policy_def'
Defining constant `fw11_FORWARD_default_policy_def'
Defining constant `fw11_OUTPUT_default_policy_def'
loading file /media/data/jenkins/workspace/isabelle-nightly-slow/afp/thys/Iptables_Semantics/Examples/IPPartEval/medium-sized-company/iptables-save
Loaded 602 lines of the filter table
Parsed 7 chain declarations
Parsed 595 rules
unfolding (this may take a while) ...
Running AODV ...
AODV: theory Aodv_Basic
AODV: theory A_Norreqid
AODV: theory Aodv_Data
AODV: theory B_Fwdrreps
AODV: theory C_Gtobcast
AODV: theory D_Fwdrreqs
AODV: theory E_All_ABCD
AODV: theory Aodv_Message
AODV: theory A_Aodv_Data
AODV: theory A_Aodv_Message
AODV: theory D_Aodv_Data
AODV: theory D_Aodv_Message
AODV: theory B_Aodv_Data
AODV: theory B_Aodv_Message
AODV: theory Fresher
AODV: theory C_Aodv_Data
AODV: theory A_Fresher
AODV: theory C_Aodv_Message
AODV: theory B_Fresher
AODV: theory E_Aodv_Data
AODV: theory D_Fresher
AODV: theory E_Aodv_Message
AODV: theory A_Aodv
AODV: theory Aodv
AODV: theory B_Aodv
AODV: theory D_Aodv
AODV: theory C_Fresher
AODV: theory E_Fresher
AODV: theory C_Aodv
AODV: theory E_Aodv
AODV: theory Aodv_Predicates
AODV: theory Loop_Freedom
AODV: theory Quality_Increases
AODV: theory Seq_Invariants
AODV: theory OAodv
AODV: theory Global_Invariants
AODV: theory Aodv_Loop_Freedom
AODV: theory A_Aodv_Predicates
AODV: theory A_OAodv
AODV: theory A_Loop_Freedom
AODV: theory A_Quality_Increases
AODV: theory A_Seq_Invariants
AODV: theory A_Global_Invariants
AODV: theory A_Aodv_Loop_Freedom
AODV: theory B_Aodv_Predicates
AODV: theory B_OAodv
AODV: theory B_Loop_Freedom
AODV: theory B_Quality_Increases
AODV: theory B_Seq_Invariants
AODV: theory B_Global_Invariants
AODV: theory B_Aodv_Loop_Freedom
AODV: theory C_Aodv_Predicates
AODV: theory C_Loop_Freedom
AODV: theory C_Quality_Increases
AODV: theory C_Seq_Invariants
AODV: theory E_Aodv_Predicates
AODV: theory C_OAodv
AODV: theory E_Loop_Freedom
AODV: theory E_Quality_Increases
AODV: theory E_Seq_Invariants
AODV: theory C_Global_Invariants
AODV: theory E_OAodv
AODV: theory E_Global_Invariants
AODV: theory C_Aodv_Loop_Freedom
AODV: theory E_Aodv_Loop_Freedom
AODV: theory D_Aodv_Predicates
AODV: theory D_OAodv
AODV: theory D_Loop_Freedom
AODV: theory D_Quality_Increases
AODV: theory D_Seq_Invariants
AODV: theory D_Global_Invariants
AODV: theory D_Aodv_Loop_Freedom
AODV: theory All
Build timed out (after 1,200 minutes). Marking the build as aborted.
Build was aborted
Archiving artifacts
Terminated
Started calculate disk usage of build
Finished Calculation of disk usage of build in 0 seconds
Started calculate disk usage of workspace
Finished Calculation of disk usage of workspace in 0 seconds
No emails were triggered.
Finished: ABORTED