Console Output

01:33:13 Started by an SCM change
01:33:13 Running as SYSTEM
01:33:13 [EnvInject] - Loading node environment variables.
01:33:13 Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow
01:33:13 [isabelle-nightly-slow] $ hg showconfig paths.default
01:33:13 [isabelle-nightly-slow] $ hg pull --rev default
01:33:13 pulling from http://isabelle.in.tum.de/repos/isabelle/
01:33:13 no changes found
01:33:14 [isabelle-nightly-slow] $ hg update --clean --rev default
01:33:14 22 files updated, 0 files merged, 0 files removed, 0 files unresolved
01:33:14 [isabelle-nightly-slow] $ hg --config extensions.purge= clean --all
01:33:14 [isabelle-nightly-slow] $ hg log --rev . --template {node}
01:33:14 [isabelle-nightly-slow] $ hg log --rev . --template {rev}
01:33:15 [isabelle-nightly-slow] $ hg log --rev fabd29c73098bbd91870ca15883fcdf7c9f12858 --template exists\n
01:33:15 exists
01:33:15 [isabelle-nightly-slow] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(fabd29c73098bbd91870ca15883fcdf7c9f12858)" --encoding UTF-8 --encodingmode replace
01:33:15 [afp] $ hg showconfig paths.default
01:33:15 [afp] $ hg pull --rev default
01:33:16 pulling from https://foss.heptapod.net/isa-afp/afp-devel/
01:33:16 no changes found
01:33:16 [afp] $ hg update --clean --rev default
01:33:16 1 files updated, 0 files merged, 0 files removed, 0 files unresolved
01:33:16 [afp] $ hg --config extensions.purge= clean --all
01:33:17 [afp] $ hg log --rev . --template {node}
01:33:17 [afp] $ hg log --rev . --template {rev}
01:33:17 [afp] $ hg log --rev a9526e233fe2a54f2789ad44470f81ae2d6f577a --template exists\n
01:33:17 exists
01:33:17 [afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(a9526e233fe2a54f2789ad44470f81ae2d6f577a)" --encoding UTF-8 --encodingmode replace
01:33:17 No emails were triggered.
01:33:17 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins2435887966356704687.sh
01:33:17 + Admin/jenkins/run_build slow
01:33:17 + set -e
01:33:17 + PROFILE=slow
01:33:17 + shift
01:33:17 + bin/isabelle components -a
01:33:17 + bin/isabelle jedit -bf
01:33:17 ### Building graph browser ...
01:33:18 warning: [options] bootstrap class path not set in conjunction with -source 6
01:33:18 warning: [options] source value 6 is obsolete and will be removed in a future release
01:33:18 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
01:33:19 Note: Some input files use or override a deprecated API.
01:33:19 Note: Recompile with -Xlint:deprecation for details.
01:33:19 Note: Some input files use unchecked or unsafe operations.
01:33:19 Note: Recompile with -Xlint:unchecked for details.
01:33:19 3 warnings
01:33:19 ### Building Isabelle/Scala ...
01:33:51 ### Building Isabelle/jEdit ...
01:34:09 + bin/isabelle ocaml_setup
01:34:09 # Run eval $(opam env) to update the current shell environment
01:34:10 [NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
01:34:10        opam update
01:34:10 
01:34:10 [NOTE] Package zarith is already installed (current version is 1.7).
01:34:10 + bin/isabelle ghc_setup
01:34:11 stack will use a sandboxed GHC it installed
01:34:11 For more information on paths, see 'stack path' and 'stack exec env'
01:34:11 To use this GHC and packages outside of a project, consider using:
01:34:11 stack ghc, stack ghci, stack runghc, or stack exec
01:34:12 The Glorious Glasgow Haskell Compilation System, version 8.6.4
01:34:12 + bin/isabelle ci_build_slow
01:34:16 
01:34:16 === CONFIGURATION ===
01:34:16 
01:34:16 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
01:34:16 ISABELLE_BUILD_OPTIONS=""
01:34:16 
01:34:16 ML_PLATFORM="x86_64-linux"
01:34:16 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686/x86_64-linux"
01:34:16 ML_SYSTEM="polyml-5.8.2"
01:34:16 ML_OPTIONS="-H 4000 --maxheap 20G"
01:34:17 jobs = 1, threads = 8, numa = false
01:34:17 
01:34:17 === BUILD ===
01:34:17 
01:34:17 Build started at Fri, 27 Nov 2020 00:34:16 GMT
01:34:17 Isabelle id a4d7da18ac5c
01:34:17 Build for AFP id 938eda70c082
01:34:17 
01:34:17 === LOG ===
01:34:17 
01:34:18 Session Pure/Pure
01:34:19 Session FOL/FOL
01:34:19 Session Tools/Tools
01:34:19 Session HOL/HOL (main)
01:34:20 Session AFP/AWN (AFP)
01:34:20 Session AFP/AODV (AFP slow)
01:34:20 Session HOL/HOL-Cardinals (timing)
01:34:20 Session HOL/HOL-Library (main timing)
01:34:21 Session AFP/Binomial-Heaps (AFP)
01:34:21 Session AFP/ConcurrentIMP (AFP)
01:34:21 Session AFP/ConcurrentGC (AFP slow)
01:34:21 Session AFP/FinFun (AFP)
01:34:21 Session AFP/Finger-Trees (AFP)
01:34:21 Session HOL/HOL-Computational_Algebra (main timing)
01:34:21 Session HOL/HOL-Algebra (main timing)
01:34:21 Session HOL/HOL-Analysis (main timing)
01:34:22 Session AFP/Coinductive (AFP)
01:34:22 Session HOL/HOL-Eisbach
01:34:22 Session HOL/HOL-Number_Theory (main timing)
01:34:22 Session HOL/HOL-ex (timing)
01:34:22 Session AFP/Automatic_Refinement (AFP)
01:34:22 Session AFP/Refine_Monadic (AFP)
01:34:23 Session HOL/HOL-Imperative_HOL (timing)
01:34:23 Session AFP/HereditarilyFinite (AFP)
01:34:23 Session AFP/Category3 (AFP)
01:34:23 Session AFP/MonoidalCategory (AFP)
01:34:23 Session AFP/Bicategory (AFP slow)
01:34:23 Session AFP/Trie (AFP)
01:34:23 Session AFP/Flyspeck-Tame (AFP)
01:34:23 Session AFP/Flyspeck-Tame-Computation (AFP slow very_slow)
01:34:23 Session AFP/Word_Lib (AFP)
01:34:24 Session AFP/IP_Addresses (AFP)
01:34:24 Session AFP/Simple_Firewall (AFP)
01:34:24 Session AFP/Routing (AFP)
01:34:24 Session AFP/Native_Word (AFP)
01:34:24 Session AFP/Collections (AFP)
01:34:24 Session AFP/Iptables_Semantics (AFP)
01:34:24 Session AFP/Iptables_Semantics_Examples (AFP)
01:34:24 Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow)
01:34:25 Session AFP/JinjaThreads (AFP slow)
01:34:26 Building Pure ...
01:34:49 Pure: theory Pure
01:34:50 Pure: theory ML_Bootstrap
01:34:51 Pure: theory Pure.Sessions
01:34:53 Timing Pure (1 threads, 1.344s elapsed time, 1.354s cpu time, 0.049s GC time, factor 1.01)
01:34:53 Finished Pure (0:00:26 elapsed time, 0:00:25 cpu time, factor 0.99)
01:34:53 Building HOL ...
01:34:56 HOL: theory Tools.Code_Generator
01:35:01 HOL: theory HOL.HOL
01:35:07 HOL: theory HOL.Orderings
01:35:07 HOL: theory HOL.Argo
01:35:07 HOL: theory HOL.Ctr_Sugar
01:35:08 HOL: theory HOL.Groups
01:35:10 HOL: theory HOL.SAT
01:35:12 HOL: theory HOL.Lattices
01:35:16 HOL: theory HOL.Set
01:35:17 HOL: theory HOL.Fun
01:35:17 HOL: theory HOL.Typedef
01:35:18 HOL: theory HOL.Complete_Lattices
01:35:18 HOL: theory HOL.Rings
01:35:21 HOL: theory HOL.Inductive
01:35:23 HOL: theory HOL.Product_Type
01:35:23 HOL: theory HOL.Sum_Type
01:35:25 HOL: theory HOL.Complete_Partial_Order
01:35:30 HOL: theory HOL.Nat
01:35:33 HOL: theory HOL.Fields
01:35:33 HOL: theory HOL.Meson
01:35:33 HOL: theory HOL.ATP
01:35:36 HOL: theory HOL.Metis
01:35:38 HOL: theory HOL.Finite_Set
01:35:41 HOL: theory HOL.Relation
01:35:42 HOL: theory HOL.Transitive_Closure
01:35:43 HOL: theory HOL.Wellfounded
01:35:45 HOL: theory HOL.Fun_Def_Base
01:35:45 HOL: theory HOL.Hilbert_Choice
01:35:45 HOL: theory HOL.Wfrec
01:35:45 HOL: theory HOL.Order_Relation
01:35:46 HOL: theory HOL.BNF_Wellorder_Relation
01:35:47 HOL: theory HOL.Zorn
01:35:47 HOL: theory HOL.BNF_Wellorder_Embedding
01:35:48 HOL: theory HOL.BNF_Wellorder_Constructions
01:35:48 HOL: theory HOL.BNF_Cardinal_Order_Relation
01:35:49 HOL: theory HOL.BNF_Cardinal_Arithmetic
01:35:50 HOL: theory HOL.BNF_Def
01:35:53 HOL: theory HOL.BNF_Composition
01:35:53 HOL: theory HOL.Basic_BNFs
01:35:55 HOL: theory HOL.BNF_Fixpoint_Base
01:36:00 HOL: theory HOL.BNF_Least_Fixpoint
01:36:05 HOL: theory HOL.Basic_BNF_LFPs
01:36:05 HOL: theory HOL.Transfer
01:36:06 HOL: theory HOL.Num
01:36:09 HOL: theory HOL.Power
01:36:13 HOL: theory HOL.Groups_Big
01:36:16 HOL: theory HOL.Equiv_Relations
01:36:16 HOL: theory HOL.Lifting
01:36:18 HOL: theory HOL.Lifting_Set
01:36:18 HOL: theory HOL.Quotient
01:36:18 HOL: theory HOL.Option
01:36:19 HOL: theory HOL.Extraction
01:36:19 HOL: theory HOL.Lattices_Big
01:36:19 HOL: theory HOL.Partial_Function
01:36:20 HOL: theory HOL.Fun_Def
01:36:26 HOL: theory HOL.Int
01:36:32 HOL: theory HOL.Euclidean_Division
01:36:46 HOL: theory HOL.Parity
01:36:54 HOL: theory HOL.Divides
01:36:57 HOL: theory HOL.Code_Numeral
01:36:57 HOL: theory HOL.Numeral_Simprocs
01:36:57 HOL: theory HOL.Set_Interval
01:36:59 HOL: theory HOL.Semiring_Normalization
01:36:59 HOL: theory HOL.SMT
01:37:02 HOL: theory HOL.Groebner_Basis
01:37:04 HOL: theory HOL.Conditionally_Complete_Lattices
01:37:04 HOL: theory HOL.Filter
01:37:04 HOL: theory HOL.Presburger
01:37:08 HOL: theory HOL.Sledgehammer
01:37:12 HOL: theory HOL.List
01:37:22 HOL: theory HOL.Groups_List
01:37:22 HOL: theory HOL.Map
01:37:24 HOL: theory HOL.Factorial
01:37:24 HOL: theory HOL.Enum
01:37:24 HOL: theory HOL.GCD
01:37:24 HOL: theory HOL.Random
01:37:26 HOL: theory HOL.Binomial
01:37:29 HOL: theory HOL.String
01:37:32 HOL: theory HOL.Predicate
01:37:32 HOL: theory HOL.BNF_Greatest_Fixpoint
01:37:32 HOL: theory HOL.Typerep
01:37:33 HOL: theory HOL.Lazy_Sequence
01:37:34 HOL: theory HOL.Limited_Sequence
01:37:34 HOL: theory HOL.Code_Evaluation
01:37:35 HOL: theory HOL.Quickcheck_Random
01:37:41 HOL: theory HOL.Quickcheck_Exhaustive
01:37:41 HOL: theory HOL.Quickcheck_Narrowing
01:37:41 HOL: theory HOL.Random_Pred
01:37:42 HOL: theory HOL.Random_Sequence
01:37:46 HOL: theory HOL.Record
01:37:46 HOL: theory HOL.Predicate_Compile
01:37:48 HOL: theory HOL.Nitpick
01:37:56 HOL: theory HOL.Nunchaku
01:37:57 HOL: theory Main
01:37:59 HOL: theory HOL.Archimedean_Field
01:37:59 HOL: theory HOL.Hull
01:37:59 HOL: theory HOL.Topological_Spaces
01:37:59 HOL: theory HOL.Modules
01:38:00 HOL: theory HOL.Vector_Spaces
01:38:09 HOL: theory HOL.Rat
01:38:12 HOL: theory HOL.Real
01:38:14 HOL: theory HOL.Real_Vector_Spaces
01:38:32 HOL: theory HOL.Inequalities
01:38:32 HOL: theory HOL.Limits
01:38:41 HOL: theory HOL.Deriv
01:38:41 HOL: theory HOL.Series
01:38:43 HOL: theory HOL.NthRoot
01:38:44 HOL: theory HOL.Transcendental
01:38:50 HOL: theory HOL.Complex
01:38:51 HOL: theory HOL.MacLaurin
01:38:51 HOL: theory Complex_Main
01:40:01 Preparing HOL/document ...
01:41:44 Finished HOL/document (0:01:42 elapsed time)
01:41:44 Preparing HOL/outline ...
01:42:42 Finished HOL/outline (0:00:58 elapsed time)
01:42:46 Timing HOL (8 threads, 247.117s elapsed time, 822.980s cpu time, 70.787s GC time, factor 3.33)
01:42:46 Finished HOL (0:05:07 elapsed time, 0:15:45 cpu time, factor 3.07)
01:42:46 Running JinjaThreads ...
01:42:48 JinjaThreads: theory HOL-Eisbach.Eisbach
01:42:48 JinjaThreads: theory Automatic_Refinement.Foldi
01:42:48 JinjaThreads: theory Automatic_Refinement.Prio_List
01:42:48 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1
01:42:48 JinjaThreads: theory Collections.ICF_Tools
01:42:48 JinjaThreads: theory HOL-Library.Adhoc_Overloading
01:42:48 JinjaThreads: theory Finger-Trees.FingerTree
01:42:48 JinjaThreads: theory HOL-Library.AList
01:42:48 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot
01:42:48 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot
01:42:48 JinjaThreads: theory HOL-Library.Monad_Syntax
01:42:48 JinjaThreads: theory Collections.Ord_Code_Preproc
01:42:48 JinjaThreads: theory HOL-Library.Boolean_Algebra
01:42:48 JinjaThreads: theory HOL-Library.Cancellation
01:42:48 JinjaThreads: theory HOL-Library.Case_Converter
01:42:48 JinjaThreads: theory Collections.Locale_Code
01:42:48 JinjaThreads: theory Automatic_Refinement.Refine_Util
01:42:48 JinjaThreads: theory Collections.Record_Intf
01:42:48 JinjaThreads: theory HOL-Library.Bit_Operations
01:42:48 JinjaThreads: theory HOL-Library.Simps_Case_Conv
01:42:48 JinjaThreads: theory HOL-Library.Code_Abstract_Nat
01:42:49 JinjaThreads: theory HOL-Library.Code_Target_Int
01:42:49 JinjaThreads: theory HOL-Library.Code_Target_Nat
01:42:49 JinjaThreads: theory HOL-Library.Confluence
01:42:49 JinjaThreads: theory HOL-Library.Multiset
01:42:49 JinjaThreads: theory HOL-Library.Code_Target_Numeral
01:42:49 JinjaThreads: theory HOL-Library.Confluent_Quotient
01:42:49 JinjaThreads: theory Automatic_Refinement.Anti_Unification
01:42:49 JinjaThreads: theory Automatic_Refinement.Attr_Comb
01:42:49 JinjaThreads: theory Automatic_Refinement.Autoref_Data
01:42:49 JinjaThreads: theory Automatic_Refinement.Indep_Vars
01:42:49 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp
01:42:49 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms
01:42:49 JinjaThreads: theory Automatic_Refinement.Tagged_Solver
01:42:49 JinjaThreads: theory Automatic_Refinement.Select_Solve
01:42:49 JinjaThreads: theory HOL-Library.Dlist
01:42:49 JinjaThreads: theory HOL-Library.Infinite_Set
01:42:50 JinjaThreads: theory HOL-Library.Lattice_Syntax
01:42:50 JinjaThreads: theory HOL-Library.Complete_Partial_Order2
01:42:50 JinjaThreads: theory HOL-Library.Nat_Bijection
01:42:50 JinjaThreads: theory HOL-Library.Old_Datatype
01:42:50 JinjaThreads: theory Trie.Trie
01:42:50 JinjaThreads: theory HOL-Library.Option_ord
01:42:50 JinjaThreads: theory HOL-Library.Phantom_Type
01:42:50 JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs
01:42:50 JinjaThreads: theory HOL-Library.RBT_Impl
01:42:51 JinjaThreads: theory HOL-Library.Signed_Division
01:42:51 JinjaThreads: theory HOL-Library.Sublist
01:42:51 JinjaThreads: theory HOL-Library.Cardinality
01:42:52 JinjaThreads: theory HOL-Library.Transitive_Closure_Table
01:42:53 JinjaThreads: theory FinFun.FinFun
01:42:53 JinjaThreads: theory HOL-Library.Numeral_Type
01:42:53 JinjaThreads: theory HOL-Library.While_Combinator
01:42:53 JinjaThreads: theory HOL-Library.Countable
01:42:54 JinjaThreads: theory Collections.DatRef
01:42:54 JinjaThreads: theory HOL-Library.Type_Length
01:42:55 JinjaThreads: theory JinjaThreads.Set_Monad
01:42:55 JinjaThreads: theory JinjaThreads.Set_without_equal
01:42:55 JinjaThreads: theory Refine_Monadic.Refine_Chapter
01:42:55 JinjaThreads: theory Word_Lib.More_Arithmetic
01:42:55 JinjaThreads: theory Binomial-Heaps.BinomialHeap
01:42:55 JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap
01:42:55 JinjaThreads: theory HOL-ex.Quicksort
01:42:55 JinjaThreads: theory HOL-Library.Countable_Set
01:42:55 JinjaThreads: theory Automatic_Refinement.Misc
01:42:55 JinjaThreads: theory JinjaThreads.Auxiliary
01:42:56 JinjaThreads: theory HOL-Library.Countable_Complete_Lattices
01:42:56 JinjaThreads: theory HOL-Library.Word
01:42:58 JinjaThreads: theory HOL-Library.Order_Continuity
01:42:59 JinjaThreads: theory HOL-Library.Extended_Nat
01:43:00 JinjaThreads: theory Coinductive.Coinductive_Nat
01:43:01 JinjaThreads: theory Automatic_Refinement.Refine_Lib
01:43:01 JinjaThreads: theory Collections.SetIterator
01:43:01 JinjaThreads: theory Collections.Sorted_List_Operations
01:43:01 JinjaThreads: theory Coinductive.Coinductive_List
01:43:02 JinjaThreads: theory Automatic_Refinement.Autoref_Phases
01:43:02 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging
01:43:02 JinjaThreads: theory Automatic_Refinement.Relators
01:43:02 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover
01:43:03 JinjaThreads: theory Collections.SetIteratorOperations
01:43:04 JinjaThreads: theory Automatic_Refinement.Param_Tool
01:43:04 JinjaThreads: theory Automatic_Refinement.Param_HOL
01:43:06 JinjaThreads: theory Word_Lib.Bit_Comprehension
01:43:06 JinjaThreads: theory Word_Lib.More_Divides
01:43:06 JinjaThreads: theory Word_Lib.Signed_Division_Word
01:43:07 JinjaThreads: theory Word_Lib.More_Word
01:43:07 JinjaThreads: theory Automatic_Refinement.Parametricity
01:43:07 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops
01:43:07 JinjaThreads: theory Collections.Assoc_List
01:43:07 JinjaThreads: theory Collections.Dlist_add
01:43:07 JinjaThreads: theory Collections.Proper_Iterator
01:43:07 JinjaThreads: theory Collections.SetIteratorGA
01:43:08 JinjaThreads: theory Collections.Diff_Array
01:43:08 JinjaThreads: theory Collections.Trie_Impl
01:43:08 JinjaThreads: theory Word_Lib.Traditional_Infix_Syntax
01:43:08 JinjaThreads: theory Collections.It_to_It
01:43:08 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel
01:43:10 JinjaThreads: theory Collections.Trie2
01:43:10 JinjaThreads: theory Automatic_Refinement.Autoref_Translate
01:43:11 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface
01:43:11 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo
01:43:11 JinjaThreads: theory Automatic_Refinement.Autoref_Tool
01:43:12 JinjaThreads: theory Word_Lib.Bits_Int
01:43:12 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL
01:43:12 JinjaThreads: theory Coinductive.Lazy_LList
01:43:12 JinjaThreads: theory Coinductive.TLList
01:43:14 JinjaThreads: theory Native_Word.More_Bits_Int
01:43:14 JinjaThreads: theory Word_Lib.Least_significant_bit
01:43:14 JinjaThreads: theory Word_Lib.Most_significant_bit
01:43:15 JinjaThreads: theory Word_Lib.Generic_set_bit
01:43:16 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement
01:43:16 JinjaThreads: theory Coinductive.Lazy_TLList
01:43:16 JinjaThreads: theory Collections.Idx_Iterator
01:43:16 JinjaThreads: theory Refine_Monadic.Refine_Misc
01:43:17 JinjaThreads: theory Refine_Monadic.RefineG_Domain
01:43:17 JinjaThreads: theory Refine_Monadic.RefineG_Transfer
01:43:17 JinjaThreads: theory Native_Word.Code_Symbolic_Bits_Int
01:43:17 JinjaThreads: theory Refine_Monadic.RefineG_Assert
01:43:17 JinjaThreads: theory Refine_Monadic.RefineG_Recursion
01:43:18 JinjaThreads: theory Native_Word.Bits_Integer
01:43:18 JinjaThreads: theory Refine_Monadic.RefineG_While
01:43:18 JinjaThreads: theory Refine_Monadic.Refine_Basic
01:43:19 JinjaThreads: theory Refine_Monadic.Refine_Det
01:43:23 JinjaThreads: theory Refine_Monadic.Refine_Heuristics
01:43:23 JinjaThreads: theory Refine_Monadic.Refine_Leof
01:43:23 JinjaThreads: theory Refine_Monadic.Refine_More_Comb
01:43:23 JinjaThreads: theory Refine_Monadic.Refine_Pfun
01:43:24 JinjaThreads: theory Refine_Monadic.Refine_While
01:43:25 JinjaThreads: theory Refine_Monadic.Refine_Transfer
01:43:26 JinjaThreads: theory Refine_Monadic.Autoref_Monadic
01:43:26 JinjaThreads: theory Refine_Monadic.Refine_Automation
01:43:26 JinjaThreads: theory Refine_Monadic.Refine_Foreach
01:43:29 JinjaThreads: theory Refine_Monadic.Refine_Monadic
01:43:31 JinjaThreads: theory Collections.Gen_Iterator
01:43:31 JinjaThreads: theory Collections.Intf_Map
01:43:31 JinjaThreads: theory Collections.Intf_Set
01:43:32 JinjaThreads: theory Collections.Iterator
01:43:33 JinjaThreads: theory HOL-Library.RBT
01:43:33 JinjaThreads: theory Collections.Array_Iterator
01:43:33 JinjaThreads: theory Collections.ICF_Spec_Base
01:43:33 JinjaThreads: theory Collections.RBT_add
01:43:34 JinjaThreads: theory Collections.AnnotatedListSpec
01:43:34 JinjaThreads: theory Collections.ListSpec
01:43:34 JinjaThreads: theory Collections.MapSpec
01:43:34 JinjaThreads: theory Collections.PrioSpec
01:43:34 JinjaThreads: theory Collections.PrioUniqueSpec
01:43:34 JinjaThreads: theory Collections.SetSpec
01:43:35 JinjaThreads: theory Native_Word.Code_Target_Bits_Int
01:43:35 JinjaThreads: theory Collections.Code_Target_ICF
01:43:35 JinjaThreads: theory Native_Word.Code_Target_Word_Base
01:43:35 JinjaThreads: theory Collections.BinoPrioImpl
01:43:35 JinjaThreads: theory Collections.SkewPrioImpl
01:43:36 JinjaThreads: theory Collections.ListGA
01:43:36 JinjaThreads: theory Native_Word.Uint32
01:43:36 JinjaThreads: theory Collections.FTAnnotatedListImpl
01:43:36 JinjaThreads: theory Collections.Fifo
01:43:38 JinjaThreads: theory Collections.PrioByAnnotatedList
01:43:38 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList
01:43:40 JinjaThreads: theory Collections.HashCode
01:43:41 JinjaThreads: theory Collections.Algos
01:43:41 JinjaThreads: theory Collections.SetIndex
01:43:41 JinjaThreads: theory Collections.SetIteratorCollectionsGA
01:43:42 JinjaThreads: theory Collections.MapGA
01:43:42 JinjaThreads: theory Collections.SetGA
01:43:43 JinjaThreads: theory Collections.FTPrioImpl
01:43:43 JinjaThreads: theory Collections.FTPrioUniqueImpl
01:43:45 JinjaThreads: theory Collections.ArrayMapImpl
01:43:45 JinjaThreads: theory Collections.ListMapImpl
01:43:45 JinjaThreads: theory Collections.ListMapImpl_Invar
01:43:45 JinjaThreads: theory Collections.TrieMapImpl
01:43:47 JinjaThreads: theory Collections.RBTMapImpl
01:43:48 JinjaThreads: theory Collections.ListSetImpl
01:43:48 JinjaThreads: theory Collections.ListSetImpl_Invar
01:43:48 JinjaThreads: theory Collections.ListSetImpl_NotDist
01:43:52 JinjaThreads: theory Collections.ListSetImpl_Sorted
01:43:52 JinjaThreads: theory Collections.SetByMap
01:43:53 JinjaThreads: theory Collections.ArrayHashMap_Impl
01:43:56 JinjaThreads: theory Collections.ArraySetImpl
01:43:56 JinjaThreads: theory Collections.TrieSetImpl
01:43:57 JinjaThreads: theory Collections.RBTSetImpl
01:43:57 JinjaThreads: theory Collections.HashMap_Impl
01:43:58 JinjaThreads: theory Collections.ArrayHashMap
01:43:59 JinjaThreads: theory Collections.HashMap
01:44:06 JinjaThreads: theory Collections.ArrayHashSet
01:44:07 JinjaThreads: theory Collections.HashSet
01:44:08 JinjaThreads: theory Collections.MapStdImpl
01:44:14 JinjaThreads: theory Collections.SetStdImpl
01:44:18 JinjaThreads: theory Collections.ICF_Impl
01:44:24 JinjaThreads: theory Collections.ICF_Refine_Monadic
01:44:25 JinjaThreads: theory Collections.ICF_Autoref
01:44:29 JinjaThreads: theory Collections.Collections
01:44:29 JinjaThreads: theory Collections.CollectionsV1
01:44:36 JinjaThreads: theory JinjaThreads.JT_ICF
01:44:37 JinjaThreads: theory JinjaThreads.Basic_Main
01:45:25 JinjaThreads: theory HOL-Library.Mapping
01:45:25 JinjaThreads: theory HOL-Library.Prefix_Order
01:45:25 JinjaThreads: theory JinjaThreads.FWState
01:45:25 JinjaThreads: theory JinjaThreads.LTS
01:45:25 JinjaThreads: theory JinjaThreads.ListIndex
01:45:25 JinjaThreads: theory JinjaThreads.Type
01:45:25 JinjaThreads: theory JinjaThreads.Orders
01:45:25 JinjaThreads: theory JinjaThreads.Semilat
01:45:29 JinjaThreads: theory JinjaThreads.Err
01:45:30 JinjaThreads: theory HOL-Library.AList_Mapping
01:45:31 JinjaThreads: theory JinjaThreads.Listn
01:45:31 JinjaThreads: theory JinjaThreads.Opt
01:45:31 JinjaThreads: theory JinjaThreads.Product
01:45:32 JinjaThreads: theory JinjaThreads.Semilattices
01:45:32 JinjaThreads: theory JinjaThreads.Decl
01:45:32 JinjaThreads: theory JinjaThreads.Typing_Framework
01:45:32 JinjaThreads: theory JinjaThreads.SemilatAlg
01:45:33 JinjaThreads: theory JinjaThreads.Kildall
01:45:33 JinjaThreads: theory JinjaThreads.LBVSpec
01:45:33 JinjaThreads: theory JinjaThreads.Bisimulation
01:45:33 JinjaThreads: theory JinjaThreads.Typing_Framework_err
01:45:33 JinjaThreads: theory JinjaThreads.LBVComplete
01:45:33 JinjaThreads: theory JinjaThreads.LBVCorrect
01:45:34 JinjaThreads: theory JinjaThreads.Abstract_BV
01:45:34 JinjaThreads: theory JinjaThreads.TypeRel
01:45:38 JinjaThreads: theory JinjaThreads.TypeRelRefine
01:45:38 JinjaThreads: theory JinjaThreads.Value
01:45:44 JinjaThreads: theory JinjaThreads.Exceptions
01:45:44 JinjaThreads: theory JinjaThreads.Heap
01:45:45 JinjaThreads: theory JinjaThreads.SystemClasses
01:45:46 JinjaThreads: theory JinjaThreads.MM
01:45:46 JinjaThreads: theory JinjaThreads.State
01:45:53 JinjaThreads: theory JinjaThreads.FWCondAction
01:45:53 JinjaThreads: theory JinjaThreads.FWInterrupt
01:45:53 JinjaThreads: theory JinjaThreads.FWLock
01:45:53 JinjaThreads: theory JinjaThreads.FWThread
01:45:53 JinjaThreads: theory JinjaThreads.FWWait
01:45:53 JinjaThreads: theory JinjaThreads.Observable_Events
01:45:55 JinjaThreads: theory JinjaThreads.FWLocking
01:45:55 JinjaThreads: theory JinjaThreads.FWWellform
01:45:55 JinjaThreads: theory JinjaThreads.FWLockingThread
01:45:56 JinjaThreads: theory JinjaThreads.FWLifting
01:45:56 JinjaThreads: theory JinjaThreads.FWSemantics
01:45:58 JinjaThreads: theory JinjaThreads.JVMState
01:45:58 JinjaThreads: theory JinjaThreads.StartConfig
01:45:58 JinjaThreads: theory JinjaThreads.JMM_Spec
01:45:59 JinjaThreads: theory JinjaThreads.FWLiftingSem
01:45:59 JinjaThreads: theory JinjaThreads.FWProgressAux
01:46:00 JinjaThreads: theory JinjaThreads.Conform
01:46:00 JinjaThreads: theory JinjaThreads.State_Refinement
01:46:00 JinjaThreads: theory JinjaThreads.FWDeadlock
01:46:01 JinjaThreads: theory JinjaThreads.FWLTS
01:46:01 JinjaThreads: theory JinjaThreads.ConformThreaded
01:46:02 JinjaThreads: theory JinjaThreads.ExternalCall
01:46:03 JinjaThreads: theory JinjaThreads.SC
01:46:03 JinjaThreads: theory JinjaThreads.FWProgress
01:46:03 JinjaThreads: theory JinjaThreads.SC_Collections
01:46:08 JinjaThreads: theory JinjaThreads.JMM_DRF
01:46:08 JinjaThreads: theory JinjaThreads.SC_Legal
01:46:11 JinjaThreads: theory JinjaThreads.FWBisimulation
01:46:11 JinjaThreads: theory JinjaThreads.FWInitFinLift
01:46:11 JinjaThreads: theory JinjaThreads.Non_Speculative
01:46:12 JinjaThreads: theory JinjaThreads.Scheduler
01:46:14 JinjaThreads: theory JinjaThreads.HB_Completion
01:46:14 JinjaThreads: theory JinjaThreads.SC_Completion
01:46:27 JinjaThreads: theory JinjaThreads.WellForm
01:46:27 JinjaThreads: theory JinjaThreads.ExternalCall_Execute
01:46:29 JinjaThreads: theory JinjaThreads.ExternalCallWF
01:46:29 JinjaThreads: theory JinjaThreads.JMM_Heap
01:46:30 JinjaThreads: theory JinjaThreads.SemiType
01:46:30 JinjaThreads: theory JinjaThreads.BinOp
01:46:32 JinjaThreads: theory JinjaThreads.JVM_SemiType
01:46:34 JinjaThreads: theory JinjaThreads.JMM_Type
01:46:34 JinjaThreads: theory JinjaThreads.JMM_Type2
01:46:42 JinjaThreads: theory JinjaThreads.Random_Scheduler
01:46:42 JinjaThreads: theory JinjaThreads.Round_Robin
01:46:45 JinjaThreads: theory JinjaThreads.JMM_Framework
01:46:53 JinjaThreads: theory JinjaThreads.SC_Schedulers
01:46:57 JinjaThreads: theory JinjaThreads.Expr
01:46:57 JinjaThreads: theory JinjaThreads.JVMInstructions
01:46:57 JinjaThreads: theory JinjaThreads.PCompiler
01:46:58 JinjaThreads: theory JinjaThreads.PCompilerRefine
01:47:28 JinjaThreads: theory JinjaThreads.JVMExceptions
01:47:28 JinjaThreads: theory JinjaThreads.JVMHeap
01:47:28 JinjaThreads: theory JinjaThreads.Effect
01:47:35 JinjaThreads: theory JinjaThreads.JVMExecInstr
01:47:48 JinjaThreads: theory JinjaThreads.CallExpr
01:47:49 JinjaThreads: theory JinjaThreads.DefAss
01:47:52 JinjaThreads: theory JinjaThreads.JHeap
01:47:53 JinjaThreads: theory JinjaThreads.WWellForm
01:47:53 JinjaThreads: theory JinjaThreads.WellType
01:47:54 JinjaThreads: theory JinjaThreads.JVMExec
01:48:01 JinjaThreads: theory JinjaThreads.JVMDefensive
01:48:02 JinjaThreads: theory JinjaThreads.J1State
01:48:03 JinjaThreads: theory JinjaThreads.SmallStep
01:48:03 JinjaThreads: theory JinjaThreads.Annotate
01:48:06 JinjaThreads: theory JinjaThreads.J1Heap
01:48:07 JinjaThreads: theory JinjaThreads.J1WellType
01:48:10 JinjaThreads: theory JinjaThreads.JWellForm
01:48:11 JinjaThreads: theory JinjaThreads.J1WellForm
01:48:11 JinjaThreads: theory JinjaThreads.WellTypeRT
01:48:13 JinjaThreads: theory JinjaThreads.JVMThreaded
01:48:13 JinjaThreads: theory JinjaThreads.JVMExec_Execute
01:48:15 JinjaThreads: theory JinjaThreads.JMM_Typesafe
01:48:18 JinjaThreads: theory JinjaThreads.Compiler1
01:48:21 JinjaThreads: theory JinjaThreads.Compiler2
01:48:23 JinjaThreads: theory JinjaThreads.Preprocessor
01:48:24 JinjaThreads: theory JinjaThreads.JJ1WellForm
01:48:26 JinjaThreads: theory JinjaThreads.ToString
01:48:30 JinjaThreads: theory JinjaThreads.JMM_JVM
01:48:32 JinjaThreads: theory JinjaThreads.JVM_Main
01:48:33 JinjaThreads: theory JinjaThreads.JMM_Common
01:48:34 JinjaThreads: theory JinjaThreads.Compiler
01:48:35 JinjaThreads: theory JinjaThreads.Exception_Tables
01:48:43 JinjaThreads: theory JinjaThreads.JMM_Typesafe2
01:48:43 JinjaThreads: theory JinjaThreads.BVSpec
01:48:44 JinjaThreads: theory JinjaThreads.EffectMono
01:48:44 JinjaThreads: theory JinjaThreads.TF_JVM
01:48:44 JinjaThreads: theory JinjaThreads.BVConform
01:48:44 JinjaThreads: theory JinjaThreads.TypeComp
01:48:50 JinjaThreads: theory JinjaThreads.BVExec
01:48:50 JinjaThreads: theory JinjaThreads.LBVJVM
01:48:54 JinjaThreads: theory JinjaThreads.FWBisimDeadlock
01:48:54 JinjaThreads: theory JinjaThreads.FWBisimLift
01:48:55 JinjaThreads: theory JinjaThreads.J1
01:48:56 JinjaThreads: theory JinjaThreads.BVSpecTypeSafe
01:49:32 JinjaThreads: theory JinjaThreads.BVNoTypeError
01:49:38 JinjaThreads: theory JinjaThreads.BCVExec
01:49:39 JinjaThreads: theory JinjaThreads.JVMExec_Execute2
01:49:39 JinjaThreads: theory JinjaThreads.BVProgressThreaded
01:49:41 JinjaThreads: theory JinjaThreads.JVMTau
01:49:56 JinjaThreads: theory JinjaThreads.Common_Main
01:50:23 JinjaThreads: theory JinjaThreads.J1Deadlock
01:50:43 JinjaThreads: theory JinjaThreads.Execs
01:51:06 JinjaThreads: theory JinjaThreads.DefAssPreservation
01:51:08 JinjaThreads: theory JinjaThreads.Threaded
01:51:09 JinjaThreads: theory JinjaThreads.Progress
01:51:17 JinjaThreads: theory JinjaThreads.TypeSafe
01:51:49 JinjaThreads: theory JinjaThreads.J0
01:51:50 JinjaThreads: theory JinjaThreads.JMM_J
01:51:51 JinjaThreads: theory JinjaThreads.ProgressThreaded
01:51:54 JinjaThreads: theory JinjaThreads.J_Execute
01:56:50 JinjaThreads: theory JinjaThreads.J1JVMBisim
01:57:04 JinjaThreads: theory JinjaThreads.Deadlocked
01:57:06 JinjaThreads: theory JinjaThreads.DRF_J
01:57:10 JinjaThreads: theory JinjaThreads.J_Main
01:57:11 JinjaThreads: theory JinjaThreads.JVMDeadlocked
01:57:11 JinjaThreads: theory JinjaThreads.DRF_JVM
01:57:11 JinjaThreads: theory JinjaThreads.JVM_Execute
01:57:11 JinjaThreads: theory JinjaThreads.JVM_Execute2
01:57:12 JinjaThreads: theory JinjaThreads.J0Bisim
01:57:12 JinjaThreads: theory JinjaThreads.J0J1Bisim
01:58:05 JinjaThreads: theory JinjaThreads.BV_Main
01:58:16 JinjaThreads: theory JinjaThreads.Correctness1
01:58:19 JinjaThreads: theory JinjaThreads.Correctness1Threaded
01:58:28 JinjaThreads: theory JinjaThreads.Code_Generation
01:58:37 JinjaThreads: theory JinjaThreads.ApprenticeChallenge
01:58:39 JinjaThreads: theory JinjaThreads.BufferExample
01:58:42 JinjaThreads: theory JinjaThreads.Java2Jinja
01:58:53 JinjaThreads: theory JinjaThreads.Examples_Main
02:01:22 JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe
02:01:27 JinjaThreads: theory JinjaThreads.JMM_J_Typesafe
02:02:07 JinjaThreads: theory JinjaThreads.Execute_Main
02:02:21 JinjaThreads: theory JinjaThreads.J1JVM
02:02:26 JinjaThreads: theory JinjaThreads.JVMJ1
02:04:20 JinjaThreads: theory JinjaThreads.Correctness2
02:14:13 JinjaThreads: theory JinjaThreads.Correctness
02:20:38 JinjaThreads: theory JinjaThreads.JMM_Compiler
02:20:39 JinjaThreads: theory JinjaThreads.SC_Interp
02:20:47 JinjaThreads: theory JinjaThreads.Compiler_Main
02:25:31 JinjaThreads: theory JinjaThreads.JMM_Interp
02:25:37 JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2
02:25:40 JinjaThreads: theory JinjaThreads.JMM
02:25:42 JinjaThreads: theory JinjaThreads.MM_Main
02:25:49 JinjaThreads: theory JinjaThreads.JinjaThreads
02:37:59 Preparing JinjaThreads/document ...
02:39:42 Finished JinjaThreads/document (0:01:42 elapsed time)
02:39:42 Preparing JinjaThreads/outline ...
02:40:24 Finished JinjaThreads/outline (0:00:42 elapsed time)
02:40:27 Timing JinjaThreads (8 threads, 3305.536s elapsed time, 15528.386s cpu time, 7362.832s GC time, factor 4.70)
02:40:27 Finished JinjaThreads (0:55:11 elapsed time, 4:23:28 cpu time, factor 4.77)
02:40:27 Building Flyspeck-Tame ...
02:40:29 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order
02:40:29 Flyspeck-Tame: theory Flyspeck-Tame.ListAux
02:40:29 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl
02:40:29 Flyspeck-Tame: theory HOL-Library.AList
02:40:29 Flyspeck-Tame: theory HOL-Library.Code_Target_Int
02:40:29 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat
02:40:29 Flyspeck-Tame: theory HOL-Library.IArray
02:40:29 Flyspeck-Tame: theory HOL-Library.While_Combinator
02:40:29 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso
02:40:29 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat
02:40:30 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral
02:40:30 Flyspeck-Tame: theory Flyspeck-Tame.Arch
02:40:30 Flyspeck-Tame: theory Flyspeck-Tame.Worklist
02:40:30 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax
02:40:31 Flyspeck-Tame: theory Flyspeck-Tame.ListSum
02:40:31 Flyspeck-Tame: theory Flyspeck-Tame.Rotation
02:40:31 Flyspeck-Tame: theory Flyspeck-Tame.Graph
02:40:31 Flyspeck-Tame: theory Flyspeck-Tame.Maps
02:40:32 Flyspeck-Tame: theory Trie.Trie
02:40:33 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision
02:40:33 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps
02:40:34 Flyspeck-Tame: theory Flyspeck-Tame.Tame
02:40:35 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator
02:40:35 Flyspeck-Tame: theory Trie.Tries
02:40:35 Flyspeck-Tame: theory Flyspeck-Tame.TameProps
02:40:35 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps
02:40:35 Flyspeck-Tame: theory Flyspeck-Tame.Plane
02:40:36 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps
02:40:36 Flyspeck-Tame: theory Flyspeck-Tame.Plane1
02:40:36 Flyspeck-Tame: theory Flyspeck-Tame.Generator
02:40:37 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum
02:40:40 Flyspeck-Tame: theory Flyspeck-Tame.Invariants
02:40:41 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux
02:40:41 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps
02:40:42 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps
02:40:42 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props
02:40:43 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound
02:40:43 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps
02:40:43 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps
02:40:43 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps
02:40:44 Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness
02:42:14 Preparing Flyspeck-Tame/document ...
02:42:31 Finished Flyspeck-Tame/document (0:00:17 elapsed time)
02:42:31 Preparing Flyspeck-Tame/outline ...
02:42:38 Finished Flyspeck-Tame/outline (0:00:07 elapsed time)
02:42:40 Timing Flyspeck-Tame (8 threads, 62.767s elapsed time, 343.208s cpu time, 32.296s GC time, factor 5.47)
02:42:40 Finished Flyspeck-Tame (0:01:46 elapsed time, 0:07:10 cpu time, factor 4.06)
02:42:40 Running Flyspeck-Tame-Computation ...
02:42:42 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.ArchComp
02:42:42 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.Completeness
07:17:04 Timing Flyspeck-Tame-Computation (8 threads, 16457.117s elapsed time, 24606.781s cpu time, 796.138s GC time, factor 1.50)
07:17:04 Finished Flyspeck-Tame-Computation (4:34:19 elapsed time, 6:50:08 cpu time, factor 1.50)
07:17:04 Building AWN ...
07:17:05 AWN: theory AWN.Lib
07:17:05 AWN: theory AWN.TransitionSystems
07:17:05 AWN: theory AWN.AWN
07:17:06 AWN: theory AWN.Invariants
07:17:07 AWN: theory AWN.OInvariants
07:17:17 AWN: theory AWN.AWN_Cterms
07:17:17 AWN: theory AWN.AWN_SOS
07:17:18 AWN: theory AWN.OAWN_SOS
07:17:20 AWN: theory AWN.AWN_Labels
07:17:21 AWN: theory AWN.Pnet
07:17:22 AWN: theory AWN.Inv_Cterms
07:17:22 AWN: theory AWN.AWN_Invariants
07:17:22 AWN: theory AWN.Closed
07:17:23 AWN: theory AWN.AWN_SOS_Labels
07:17:23 AWN: theory AWN.Qmsg
07:17:24 AWN: theory AWN.OAWN_Invariants
07:17:24 AWN: theory AWN.OAWN_SOS_Labels
07:17:24 AWN: theory AWN.ONode_Lifting
07:17:24 AWN: theory AWN.OPnet
07:17:25 AWN: theory AWN.OPnet_Lifting
07:17:25 AWN: theory AWN.OClosed_Lifting
07:17:25 AWN: theory AWN.OClosed_Transfer
07:17:26 AWN: theory AWN.OAWN_Convert
07:17:26 AWN: theory AWN.Qmsg_Lifting
07:17:26 AWN: theory AWN.AWN_Main
07:17:27 AWN: theory AWN.Toy
07:17:36 AWN: theory AWN.AWN_Term_Graph
07:18:09 Preparing AWN/document ...
07:18:18 Finished AWN/document (0:00:09 elapsed time)
07:18:18 Preparing AWN/outline ...
07:18:24 Finished AWN/outline (0:00:05 elapsed time)
07:18:25 Timing AWN (8 threads, 34.732s elapsed time, 164.667s cpu time, 8.741s GC time, factor 4.74)
07:18:25 Finished AWN (0:01:05 elapsed time, 0:03:45 cpu time, factor 3.47)
07:18:25 Running AODV ...
07:18:27 AODV: theory AODV.Aodv_Basic
07:18:29 AODV: theory AODV.A_Norreqid
07:18:29 AODV: theory AODV.Aodv_Data
07:18:29 AODV: theory AODV.Aodv_Message
07:18:29 AODV: theory AODV.B_Fwdrreps
07:18:29 AODV: theory AODV.C_Gtobcast
07:18:29 AODV: theory AODV.D_Fwdrreqs
07:18:29 AODV: theory AODV.E_All_ABCD
07:18:29 AODV: theory AODV.A_Aodv_Data
07:18:29 AODV: theory AODV.A_Aodv_Message
07:18:29 AODV: theory AODV.D_Aodv_Data
07:18:29 AODV: theory AODV.D_Aodv_Message
07:18:29 AODV: theory AODV.B_Aodv_Data
07:18:29 AODV: theory AODV.B_Aodv_Message
07:18:30 AODV: theory AODV.Fresher
07:18:30 AODV: theory AODV.C_Aodv_Data
07:18:30 AODV: theory AODV.C_Aodv_Message
07:18:30 AODV: theory AODV.A_Fresher
07:18:30 AODV: theory AODV.D_Fresher
07:18:30 AODV: theory AODV.B_Fresher
07:18:30 AODV: theory AODV.E_Aodv_Data
07:18:31 AODV: theory AODV.E_Aodv_Message
07:18:31 AODV: theory AODV.A_Aodv
07:18:31 AODV: theory AODV.Aodv
07:18:31 AODV: theory AODV.B_Aodv
07:18:31 AODV: theory AODV.D_Aodv
07:18:31 AODV: theory AODV.C_Fresher
07:18:31 AODV: theory AODV.E_Fresher
07:18:32 AODV: theory AODV.C_Aodv
07:18:32 AODV: theory AODV.E_Aodv
07:19:10 AODV: theory AODV.A_Aodv_Predicates
07:19:10 AODV: theory AODV.A_Loop_Freedom
07:19:10 AODV: theory AODV.A_Quality_Increases
07:19:11 AODV: theory AODV.A_Seq_Invariants
07:19:11 AODV: theory AODV.A_OAodv
07:19:11 AODV: theory AODV.A_Global_Invariants
07:19:12 AODV: theory AODV.A_Aodv_Loop_Freedom
07:19:18 AODV: theory AODV.Aodv_Predicates
07:19:18 AODV: theory AODV.OAodv
07:19:18 AODV: theory AODV.Loop_Freedom
07:19:18 AODV: theory AODV.Quality_Increases
07:19:18 AODV: theory AODV.Seq_Invariants
07:19:19 AODV: theory AODV.Global_Invariants
07:19:20 AODV: theory AODV.Aodv_Loop_Freedom
07:19:21 AODV: theory AODV.B_Aodv_Predicates
07:19:22 AODV: theory AODV.B_OAodv
07:19:22 AODV: theory AODV.B_Loop_Freedom
07:19:22 AODV: theory AODV.B_Quality_Increases
07:19:22 AODV: theory AODV.B_Seq_Invariants
07:19:22 AODV: theory AODV.B_Global_Invariants
07:19:23 AODV: theory AODV.C_Aodv_Predicates
07:19:23 AODV: theory AODV.C_Loop_Freedom
07:19:23 AODV: theory AODV.C_Quality_Increases
07:19:23 AODV: theory AODV.C_Seq_Invariants
07:19:23 AODV: theory AODV.C_OAodv
07:19:23 AODV: theory AODV.B_Aodv_Loop_Freedom
07:19:24 AODV: theory AODV.C_Global_Invariants
07:19:25 AODV: theory AODV.C_Aodv_Loop_Freedom
07:19:26 AODV: theory AODV.E_Aodv_Predicates
07:19:26 AODV: theory AODV.E_OAodv
07:19:26 AODV: theory AODV.E_Loop_Freedom
07:19:26 AODV: theory AODV.E_Quality_Increases
07:19:26 AODV: theory AODV.E_Seq_Invariants
07:19:27 AODV: theory AODV.E_Global_Invariants
07:19:28 AODV: theory AODV.E_Aodv_Loop_Freedom
07:19:29 AODV: theory AODV.D_Aodv_Predicates
07:19:29 AODV: theory AODV.D_OAodv
07:19:30 AODV: theory AODV.D_Loop_Freedom
07:19:30 AODV: theory AODV.D_Quality_Increases
07:19:30 AODV: theory AODV.D_Seq_Invariants
07:19:31 AODV: theory AODV.D_Global_Invariants
07:19:31 AODV: theory AODV.D_Aodv_Loop_Freedom
07:19:36 AODV: theory AODV.All
08:28:49 Preparing AODV/document ...
08:29:09 Finished AODV/document (0:00:19 elapsed time)
08:29:09 Preparing AODV/outline ...
08:29:20 Finished AODV/outline (0:00:11 elapsed time)
08:29:22 Timing AODV (8 threads, 4221.278s elapsed time, 26269.396s cpu time, 852.242s GC time, factor 6.22)
08:29:22 Finished AODV (1:10:23 elapsed time, 7:17:53 cpu time, factor 6.22)
08:29:22 Building Word_Lib ...
08:29:23 Word_Lib: theory HOL-Library.Boolean_Algebra
08:29:23 Word_Lib: theory HOL-Library.Phantom_Type
08:29:23 Word_Lib: theory HOL-Library.Signed_Division
08:29:23 Word_Lib: theory HOL-Library.Sublist
08:29:23 Word_Lib: theory Word_Lib.Enumeration
08:29:23 Word_Lib: theory Word_Lib.More_Arithmetic
08:29:23 Word_Lib: theory Word_Lib.Even_More_List
08:29:23 Word_Lib: theory HOL-Eisbach.Eisbach
08:29:24 Word_Lib: theory Word_Lib.More_Misc
08:29:24 Word_Lib: theory HOL-Library.Bit_Operations
08:29:25 Word_Lib: theory HOL-Eisbach.Eisbach_Tools
08:29:25 Word_Lib: theory HOL-Library.Cardinality
08:29:26 Word_Lib: theory Word_Lib.More_Sublist
08:29:26 Word_Lib: theory HOL-Library.Numeral_Type
08:29:27 Word_Lib: theory HOL-Library.Type_Length
08:29:30 Word_Lib: theory HOL-Library.Word
08:29:39 Word_Lib: theory Word_Lib.Bit_Comprehension
08:29:39 Word_Lib: theory Word_Lib.Hex_Words
08:29:39 Word_Lib: theory Word_Lib.Legacy_Aliasses
08:29:39 Word_Lib: theory Word_Lib.More_Divides
08:29:39 Word_Lib: theory Word_Lib.Signed_Words
08:29:39 Word_Lib: theory Word_Lib.Type_Syntax
08:29:39 Word_Lib: theory Word_Lib.Word_Syntax
08:29:39 Word_Lib: theory Word_Lib.Signed_Division_Word
08:29:39 Word_Lib: theory Word_Lib.More_Word
08:29:40 Word_Lib: theory Word_Lib.Enumeration_Word
08:29:40 Word_Lib: theory Word_Lib.Strict_part_mono
08:29:40 Word_Lib: theory Word_Lib.Traditional_Infix_Syntax
08:29:41 Word_Lib: theory Word_Lib.Bits_Int
08:29:41 Word_Lib: theory Word_Lib.Word_EqI
08:29:43 Word_Lib: theory Word_Lib.Least_significant_bit
08:29:43 Word_Lib: theory Word_Lib.Norm_Words
08:29:44 Word_Lib: theory Word_Lib.Rsplit
08:29:44 Word_Lib: theory Word_Lib.Most_significant_bit
08:29:44 Word_Lib: theory Word_Lib.Typedef_Morphisms
08:29:44 Word_Lib: theory Word_Lib.Generic_set_bit
08:29:44 Word_Lib: theory Word_Lib.Aligned
08:29:45 Word_Lib: theory Word_Lib.Next_and_Prev
08:29:45 Word_Lib: theory Word_Lib.Word_Lemmas
08:29:45 Word_Lib: theory Word_Lib.Reversed_Bit_Lists
08:29:47 Word_Lib: theory Word_Lib.Ancient_Numeral
08:29:47 Word_Lib: theory Word_Lib.Bitwise
08:29:47 Word_Lib: theory Word_Lib.More_Word_Operations
08:29:48 Word_Lib: theory Word_Lib.Bitwise_Signed
08:29:48 Word_Lib: theory Word_Lib.Examples
08:29:48 Word_Lib: theory Word_Lib.Word_16
08:29:48 Word_Lib: theory Word_Lib.Word_8
08:29:50 Word_Lib: theory Word_Lib.Word_32
08:29:50 Word_Lib: theory Word_Lib.Word_64
08:29:51 Word_Lib: theory Word_Lib.Word_Lib_Sumo
08:29:54 Word_Lib: theory Word_Lib.Guide
08:30:27 Preparing Word_Lib/document ...
08:30:36 Finished Word_Lib/document (0:00:09 elapsed time)
08:30:36 Preparing Word_Lib/outline ...
08:30:43 Finished Word_Lib/outline (0:00:06 elapsed time)
08:30:44 Timing Word_Lib (8 threads, 36.815s elapsed time, 227.215s cpu time, 17.426s GC time, factor 6.17)
08:30:44 Finished Word_Lib (0:01:04 elapsed time, 0:04:41 cpu time, factor 4.35)
08:30:44 Building IP_Addresses ...
08:30:46 IP_Addresses: theory HOL-Library.Cancellation
08:30:46 IP_Addresses: theory HOL-Library.Option_ord
08:30:46 IP_Addresses: theory HOL-Library.Infinite_Set
08:30:46 IP_Addresses: theory IP_Addresses.NumberWang_IPv4
08:30:46 IP_Addresses: theory IP_Addresses.NumberWang_IPv6
08:30:47 IP_Addresses: theory HOL-Library.Multiset
08:30:52 IP_Addresses: theory HOL-ex.Quicksort
08:30:52 IP_Addresses: theory Automatic_Refinement.Misc
08:30:58 IP_Addresses: theory HOL-Library.Code_Abstract_Nat
08:30:58 IP_Addresses: theory IP_Addresses.Hs_Compat
08:30:58 IP_Addresses: theory HOL-Library.Product_Lexorder
08:30:58 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
08:30:58 IP_Addresses: theory IP_Addresses.WordInterval
08:30:58 IP_Addresses: theory HOL-Library.Code_Target_Nat
08:30:58 IP_Addresses: theory IP_Addresses.Lib_List_toString
08:30:58 IP_Addresses: theory IP_Addresses.Lib_Word_toString
08:31:03 IP_Addresses: theory IP_Addresses.WordInterval_Sorted
08:31:03 IP_Addresses: theory IP_Addresses.IP_Address
08:31:09 IP_Addresses: theory IP_Addresses.IPv4
08:31:09 IP_Addresses: theory IP_Addresses.Prefix_Match
08:31:09 IP_Addresses: theory IP_Addresses.IPv6
08:31:10 IP_Addresses: theory IP_Addresses.CIDR_Split
08:32:17 IP_Addresses: theory IP_Addresses.IP_Address_Parser
08:32:17 IP_Addresses: theory IP_Addresses.IP_Address_toString
08:32:19 IP_Addresses: theory IP_Addresses.Prefix_Match_toString
08:34:50 Preparing IP_Addresses/document ...
08:34:56 Finished IP_Addresses/document (0:00:05 elapsed time)
08:34:56 Preparing IP_Addresses/outline ...
08:35:01 Finished IP_Addresses/outline (0:00:04 elapsed time)
08:35:02 Timing IP_Addresses (8 threads, 194.257s elapsed time, 664.870s cpu time, 52.578s GC time, factor 3.42)
08:35:02 Finished IP_Addresses (0:04:05 elapsed time, 0:12:55 cpu time, factor 3.15)
08:35:02 Building Simple_Firewall ...
08:35:04 Simple_Firewall: theory Simple_Firewall.List_Product_More
08:35:04 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
08:35:04 Simple_Firewall: theory Simple_Firewall.Option_Helpers
08:35:04 Simple_Firewall: theory Simple_Firewall.GroupF
08:35:04 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
08:35:04 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
08:35:04 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
08:35:04 Simple_Firewall: theory HOL-Library.Char_ord
08:35:04 Simple_Firewall: theory Simple_Firewall.Iface
08:35:04 Simple_Firewall: theory Simple_Firewall.L4_Protocol
08:35:07 Simple_Firewall: theory Simple_Firewall.Simple_Packet
08:35:07 Simple_Firewall: theory Simple_Firewall.Primitives_toString
08:35:10 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
08:35:13 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
08:35:13 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString
08:35:15 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
08:35:15 Simple_Firewall: theory Simple_Firewall.Shadowed
08:35:15 Simple_Firewall: theory Simple_Firewall.Service_Matrix
08:35:45 Preparing Simple_Firewall/document ...
08:35:53 Finished Simple_Firewall/document (0:00:07 elapsed time)
08:35:53 Preparing Simple_Firewall/outline ...
08:35:59 Finished Simple_Firewall/outline (0:00:05 elapsed time)
08:36:00 Timing Simple_Firewall (8 threads, 17.745s elapsed time, 87.220s cpu time, 4.921s GC time, factor 4.92)
08:36:00 Finished Simple_Firewall (0:00:43 elapsed time, 0:02:25 cpu time, factor 3.35)
08:36:00 Building Routing ...
08:36:02 Routing: theory Routing.Linorder_Helper
08:36:02 Routing: theory HOL-Library.Adhoc_Overloading
08:36:02 Routing: theory HOL-Library.Monad_Syntax
08:36:03 Routing: theory Routing.Routing_Table
08:36:06 Routing: theory Routing.IpRoute_Parser
08:36:06 Routing: theory Routing.Linux_Router
08:36:29 Preparing Routing/document ...
08:36:32 Finished Routing/document (0:00:03 elapsed time)
08:36:32 Preparing Routing/outline ...
08:36:35 Finished Routing/outline (0:00:02 elapsed time)
08:36:36 Timing Routing (8 threads, 11.720s elapsed time, 30.163s cpu time, 1.208s GC time, factor 2.57)
08:36:36 Finished Routing (0:00:28 elapsed time, 0:01:01 cpu time, factor 2.14)
08:36:36 Building Iptables_Semantics ...
08:36:38 Iptables_Semantics: theory Iptables_Semantics.Negation_Type
08:36:38 Iptables_Semantics: theory Iptables_Semantics.List_Misc
08:36:39 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
08:36:40 Iptables_Semantics: theory HOL-Library.Code_Target_Int
08:36:40 Iptables_Semantics: theory HOL-Library.LaTeXsugar
08:36:40 Iptables_Semantics: theory Iptables_Semantics.Ternary
08:36:40 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
08:36:40 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
08:36:40 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
08:36:40 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
08:36:40 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
08:36:40 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
08:36:40 Iptables_Semantics: theory Native_Word.More_Bits_Int
08:36:40 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
08:36:40 Iptables_Semantics: theory Iptables_Semantics.Word_Upto
08:36:40 Iptables_Semantics: theory Iptables_Semantics.IpAddresses
08:36:42 Iptables_Semantics: theory Iptables_Semantics.Ports
08:36:42 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
08:36:42 Iptables_Semantics: theory Native_Word.Code_Symbolic_Bits_Int
08:36:43 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
08:36:43 Iptables_Semantics: theory Native_Word.Bits_Integer
08:36:55 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
08:36:55 Iptables_Semantics: theory Iptables_Semantics.Semantics
08:36:55 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
08:36:56 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
08:36:56 Iptables_Semantics: theory Iptables_Semantics.Matching
08:36:57 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
08:36:57 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
08:36:57 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
08:36:58 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
08:36:58 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
08:36:58 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
08:36:59 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
08:36:59 Iptables_Semantics: theory Iptables_Semantics.Optimizing
08:36:59 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
08:37:00 Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int
08:37:00 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
08:37:00 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
08:37:03 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
08:37:06 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
08:37:07 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
08:37:07 Iptables_Semantics: theory Iptables_Semantics.Ipassmt
08:37:10 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
08:37:40 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
08:37:40 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
08:37:40 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
08:37:40 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
08:37:40 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
08:37:40 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
08:37:40 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
08:37:40 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
08:37:40 Iptables_Semantics: theory Iptables_Semantics.No_Spoof
08:37:44 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
08:37:45 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
08:37:48 Iptables_Semantics: theory Iptables_Semantics.Transform
08:37:51 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
08:37:53 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
08:37:57 Iptables_Semantics: theory Iptables_Semantics.Code_Interface
08:37:57 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
08:37:58 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
08:37:58 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
08:37:58 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
08:38:04 Iptables_Semantics: theory Iptables_Semantics.Parser
08:38:04 Iptables_Semantics: theory Iptables_Semantics.Parser6
08:38:04 Iptables_Semantics: theory Iptables_Semantics.Documentation
08:38:05 Iptables_Semantics: theory Iptables_Semantics.Code_haskell
08:39:27 Preparing Iptables_Semantics/document ...
08:39:51 Finished Iptables_Semantics/document (0:00:24 elapsed time)
08:39:51 Preparing Iptables_Semantics/outline ...
08:40:04 Finished Iptables_Semantics/outline (0:00:12 elapsed time)
08:40:06 Timing Iptables_Semantics (8 threads, 109.270s elapsed time, 524.517s cpu time, 44.378s GC time, factor 4.80)
08:40:06 Finished Iptables_Semantics (0:02:50 elapsed time, 0:11:36 cpu time, factor 4.07)
08:40:06 Building Iptables_Semantics_Examples ...
08:40:09 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com
08:40:09 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing
08:40:09 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example
08:40:09 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test
08:40:09 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company
08:40:09 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test
08:40:09 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof
08:40:09 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall
08:40:14 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail
08:40:14 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples
08:40:14 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed
08:40:15 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation
08:43:54 Preparing Iptables_Semantics_Examples/document ...
08:43:59 Finished Iptables_Semantics_Examples/document (0:00:04 elapsed time)
08:43:59 Preparing Iptables_Semantics_Examples/outline ...
08:44:04 Finished Iptables_Semantics_Examples/outline (0:00:04 elapsed time)
08:44:05 Timing Iptables_Semantics_Examples (8 threads, 199.858s elapsed time, 1437.707s cpu time, 152.875s GC time, factor 7.19)
08:44:05 Finished Iptables_Semantics_Examples (0:03:47 elapsed time, 0:24:50 cpu time, factor 6.55)
08:44:05 Running Iptables_Semantics_Examples_Big ...
08:44:08 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern
08:44:08 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall
08:44:08 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small
08:44:08 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3
08:44:08 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated
08:45:22 Run out of store - interrupting threads
08:45:22 Iptables_Semantics_Examples_Big FAILED
08:45:22 (see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.8.2_x86_64-linux/log/Iptables_Semantics_Examples_Big)
08:45:22 Defining constant `fw4_def'
08:45:22 "([(''0.0.0.0'',
08:45:22     ''{0.0.0.0 .. 9.255.255.255} u {11.0.0.0 .. 255.255.255.255}''),
08:45:22    (''10.0.0.1'', ''10.0.0.1 u 10.0.0.42''), (''10.0.0.4'', ''10.0.0.4''),
08:45:22    (''10.0.0.3'', ''10.0.0.3''), (''10.0.0.2'', ''10.0.0.2''),
08:45:22    (''10.0.0.0'',
08:45:22     ''10.0.0.0 u {10.0.0.5 .. 10.0.0.41} u {10.0.0.43 .. 10.255.255.255}'')],
08:45:22   [(''0.0.0.0'', ''0.0.0.0''), (''0.0.0.0'', ''10.0.0.1''),
08:45:22    (''0.0.0.0'', ''10.0.0.4''), (''10.0.0.1'', ''0.0.0.0''),
08:45:22    (''10.0.0.1'', ''10.0.0.1''), (''10.0.0.1'', ''10.0.0.4''),
08:45:22    (''10.0.0.1'', ''10.0.0.2''), (''10.0.0.4'', ''0.0.0.0''),
08:45:22    (''10.0.0.4'', ''10.0.0.1''), (''10.0.0.4'', ''10.0.0.4''),
08:45:22    (''10.0.0.4'', ''10.0.0.3''), (''10.0.0.4'', ''10.0.0.2''),
08:45:22    (''10.0.0.3'', ''10.0.0.4''), (''10.0.0.3'', ''10.0.0.3''),
08:45:22    (''10.0.0.3'', ''10.0.0.2''), (''10.0.0.2'', ''10.0.0.2'')])"
08:45:22   :: "(char list \<times> char list) list \<times> (char list \<times> char list) list"
08:45:22 "([(''0.0.0.0'',
08:45:22     ''{0.0.0.0 .. 9.255.255.255} u {11.0.0.0 .. 255.255.255.255}''),
08:45:22    (''10.0.0.1'', ''10.0.0.1 u 10.0.0.42''), (''10.0.0.4'', ''10.0.0.4''),
08:45:22    (''10.0.0.3'', ''10.0.0.3''), (''10.0.0.2'', ''10.0.0.2''),
08:45:22    (''10.0.0.0'',
08:45:22     ''10.0.0.0 u {10.0.0.5 .. 10.0.0.41} u {10.0.0.43 .. 10.255.255.255}'')],
08:45:22   [(''0.0.0.0'', ''0.0.0.0''), (''0.0.0.0'', ''10.0.0.1''),
08:45:22    (''10.0.0.1'', ''0.0.0.0''), (''10.0.0.1'', ''10.0.0.1''),
08:45:22    (''10.0.0.1'', ''10.0.0.4''), (''10.0.0.1'', ''10.0.0.2''),
08:45:22    (''10.0.0.4'', ''0.0.0.0''), (''10.0.0.4'', ''10.0.0.1''),
08:45:22    (''10.0.0.4'', ''10.0.0.4''), (''10.0.0.4'', ''10.0.0.3''),
08:45:22    (''10.0.0.4'', ''10.0.0.2''), (''10.0.0.3'', ''10.0.0.4''),
08:45:22    (''10.0.0.3'', ''10.0.0.3''), (''10.0.0.3'', ''10.0.0.2''),
08:45:22    (''10.0.0.2'', ''10.0.0.2'')])"
08:45:22   :: "(char list \<times> char list) list \<times> (char list \<times> char list) list"
08:45:22 Defining constant `fw4_INPUT_default_policy_def'
08:45:22 Defining constant `fw4_FORWARD_default_policy_def'
08:45:22 Defining constant `fw4_OUTPUT_default_policy_def'
08:45:22 loading file /media/data/jenkins/workspace/isabelle-nightly-slow/afp/thys/Iptables_Semantics/Examples/IPPartEval/worst_case/iptables-save
08:45:22 Loaded 4 lines of the filter table
08:45:22 Parsed 3 chain declarations
08:45:22 Parsed 1 rules
08:45:22 unfolding (this may take a while) ...
08:45:22 *** Interrupt
08:45:22 Building HOL-Library ...
08:45:24 HOL-Library: theory HOL-Library.Adhoc_Overloading
08:45:24 HOL-Library: theory HOL-Library.AList
08:45:24 HOL-Library: theory HOL-Library.BNF_Axiomatization
08:45:24 HOL-Library: theory HOL-Library.Boolean_Algebra
08:45:24 HOL-Library: theory HOL-Library.Case_Converter
08:45:24 HOL-Library: theory HOL-Library.Cancellation
08:45:24 HOL-Library: theory HOL-Library.Char_ord
08:45:24 HOL-Library: theory HOL-Library.BNF_Corec
08:45:24 HOL-Library: theory HOL-Library.Code_Abstract_Nat
08:45:24 HOL-Library: theory HOL-Library.Code_Prolog
08:45:25 HOL-Library: theory HOL-Library.Monad_Syntax
08:45:25 HOL-Library: theory HOL-Library.Code_Binary_Nat
08:45:25 HOL-Library: theory HOL-Library.State_Monad
08:45:25 HOL-Library: theory HOL-Library.Bit_Operations
08:45:25 HOL-Library: theory HOL-Library.Code_Target_Nat
08:45:25 HOL-Library: theory HOL-Library.Code_Lazy
08:45:25 HOL-Library: theory HOL-Library.Simps_Case_Conv
08:45:25 HOL-Library: theory HOL-Library.Multiset
08:45:25 HOL-Library: theory HOL-Library.Extended
08:45:26 HOL-Library: theory HOL-Library.Code_Target_Int
08:45:26 HOL-Library: theory HOL-Library.Code_Test
08:45:26 HOL-Library: theory HOL-Library.Code_Target_Numeral
08:45:26 HOL-Library: theory HOL-Library.Comparator
08:45:26 HOL-Library: theory HOL-Library.Conditional_Parametricity
08:45:26 HOL-Library: theory HOL-Library.DAList
08:45:27 HOL-Library: theory HOL-Library.Confluence
08:45:27 HOL-Library: theory HOL-Library.Datatype_Records
08:45:27 HOL-Library: theory HOL-Library.Confluent_Quotient
08:45:27 HOL-Library: theory HOL-Library.Dlist
08:45:27 HOL-Library: theory HOL-Library.Debug
08:45:27 HOL-Library: theory HOL-Library.Disjoint_Sets
08:45:27 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
08:45:27 HOL-Library: theory HOL-Library.Fun_Lexorder
08:45:27 HOL-Library: theory HOL-Library.FuncSet
08:45:27 HOL-Library: theory HOL-Library.Function_Algebras
08:45:27 HOL-Library: theory HOL-Library.Function_Division
08:45:27 HOL-Library: theory HOL-Library.Groups_Big_Fun
08:45:27 HOL-Library: theory HOL-Library.IArray
08:45:27 HOL-Library: theory HOL-Library.Infinite_Set
08:45:28 HOL-Library: theory HOL-Library.LaTeXsugar
08:45:28 HOL-Library: theory HOL-Library.Lattice_Constructions
08:45:28 HOL-Library: theory HOL-Library.Lattice_Syntax
08:45:28 HOL-Library: theory HOL-Library.Equipollence
08:45:28 HOL-Library: theory HOL-Library.Combine_PER
08:45:28 HOL-Library: theory HOL-Library.Omega_Words_Fun
08:45:28 HOL-Library: theory HOL-Library.Ramsey
08:45:29 HOL-Library: theory HOL-Library.Complete_Partial_Order2
08:45:29 HOL-Library: theory HOL-Library.ListVector
08:45:29 HOL-Library: theory HOL-Library.List_Lenlexorder
08:45:29 HOL-Library: theory HOL-Library.List_Lexorder
08:45:29 HOL-Library: theory HOL-Library.Mapping
08:45:29 HOL-Library: theory HOL-Library.More_List
08:45:29 HOL-Library: theory HOL-Library.Nat_Bijection
08:45:30 HOL-Library: theory HOL-Library.Poly_Mapping
08:45:30 HOL-Library: theory HOL-Library.Stream
08:45:30 HOL-Library: theory HOL-Library.AList_Mapping
08:45:31 HOL-Library: theory HOL-Library.Old_Datatype
08:45:31 HOL-Library: theory HOL-Library.DAList_Multiset
08:45:31 HOL-Library: theory HOL-Library.Multiset_Order
08:45:31 HOL-Library: theory HOL-Library.Permutation
08:45:31 HOL-Library: theory HOL-Library.Permutations
08:45:31 HOL-Library: theory HOL-Library.Old_Recdef
08:45:31 HOL-Library: theory HOL-Library.Open_State_Syntax
08:45:31 HOL-Library: theory HOL-Library.Option_ord
08:45:31 HOL-Library: theory HOL-Library.Parallel
08:45:32 HOL-Library: theory HOL-Library.Pattern_Aliases
08:45:32 HOL-Library: theory HOL-Library.Perm
08:45:32 HOL-Library: theory HOL-Library.Phantom_Type
08:45:32 HOL-Library: theory HOL-Library.Power_By_Squaring
08:45:32 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
08:45:32 HOL-Library: theory HOL-Library.Preorder
08:45:32 HOL-Library: theory HOL-Library.Product_Lexorder
08:45:33 HOL-Library: theory HOL-Library.Product_Plus
08:45:33 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
08:45:33 HOL-Library: theory HOL-Library.Product_Order
08:45:33 HOL-Library: theory HOL-Library.Quotient_Syntax
08:45:33 HOL-Library: theory HOL-Library.Quotient_Option
08:45:34 HOL-Library: theory HOL-Library.Quotient_Product
08:45:34 HOL-Library: theory HOL-Library.Cardinality
08:45:34 HOL-Library: theory HOL-Library.Quotient_Set
08:45:34 HOL-Library: theory HOL-Library.Quotient_Sum
08:45:34 HOL-Library: theory HOL-Library.Finite_Lattice
08:45:34 HOL-Library: theory HOL-Library.Quotient_Type
08:45:34 HOL-Library: theory HOL-Library.RBT_Impl
08:45:34 HOL-Library: theory HOL-Library.Quotient_List
08:45:34 HOL-Library: theory HOL-Library.Realizers
08:45:34 HOL-Library: theory HOL-Library.Reflection
08:45:34 HOL-Library: theory HOL-Library.Refute
08:45:34 HOL-Library: theory HOL-Library.Rewrite
08:45:34 HOL-Library: theory HOL-Library.Set_Algebras
08:45:35 HOL-Library: theory HOL-Library.Signed_Division
08:45:35 HOL-Library: theory HOL-Library.Sorting_Algorithms
08:45:35 HOL-Library: theory HOL-Library.Stirling
08:45:35 HOL-Library: theory HOL-Library.Sublist
08:45:35 HOL-Library: theory HOL-Library.Transitive_Closure_Table
08:45:35 HOL-Library: theory HOL-Library.Numeral_Type
08:45:35 HOL-Library: theory HOL-Library.Tree
08:45:35 HOL-Library: theory HOL-Library.Uprod
08:45:35 HOL-Library: theory HOL-Library.While_Combinator
08:45:35 HOL-Library: theory HOL-Library.Z2
08:45:36 HOL-Library: theory HOL-Library.Countable
08:45:36 HOL-Library: theory HOL-Library.Type_Length
08:45:36 HOL-Library: theory HOL-Library.BigO
08:45:36 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
08:45:36 HOL-Library: theory HOL-Library.Prefix_Order
08:45:36 HOL-Library: theory HOL-Library.Subseq_Order
08:45:36 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
08:45:36 HOL-Library: theory HOL-Library.Diagonal_Subsequence
08:45:36 HOL-Library: theory HOL-Library.Discrete
08:45:37 HOL-Library: theory HOL-Library.Going_To_Filter
08:45:37 HOL-Library: theory HOL-Library.Saturated
08:45:38 HOL-Library: theory HOL-Library.Word
08:45:38 HOL-Library: theory HOL-Library.Indicator_Function
08:45:38 HOL-Library: theory HOL-Library.Landau_Symbols
08:45:38 HOL-Library: theory HOL-Library.Lattice_Algebras
08:45:38 HOL-Library: theory HOL-Library.Liminf_Limsup
08:45:38 HOL-Library: theory HOL-Library.Countable_Set
08:45:39 HOL-Library: theory HOL-Library.FSet
08:45:39 HOL-Library: theory HOL-Library.Tree_Multiset
08:45:39 HOL-Library: theory HOL-Library.Countable_Complete_Lattices
08:45:39 HOL-Library: theory HOL-Library.Countable_Set_Type
08:45:39 HOL-Library: theory HOL-Library.Set_Idioms
08:45:40 HOL-Library: theory HOL-Library.Log_Nat
08:45:40 HOL-Library: theory HOL-Library.Lub_Glb
08:45:40 HOL-Library: theory HOL-Library.Multiset_Permutations
08:45:41 HOL-Library: theory HOL-Library.Nonpos_Ints
08:45:41 HOL-Library: theory HOL-Library.OptionalSugar
08:45:41 HOL-Library: theory HOL-Library.Periodic_Fun
08:45:41 HOL-Library: theory HOL-Library.Quadratic_Discriminant
08:45:41 HOL-Library: theory HOL-Library.Sum_of_Squares
08:45:41 HOL-Library: theory HOL-Library.Tree_Real
08:45:42 HOL-Library: theory HOL-Library.Order_Continuity
08:45:42 HOL-Library: theory HOL-Library.Finite_Map
08:45:43 HOL-Library: theory HOL-Library.Extended_Nat
08:45:44 HOL-Library: theory HOL-Library.Extended_Real
08:45:44 HOL-Library: theory HOL-Library.Interval
08:45:45 HOL-Library: theory HOL-Library.Float
08:45:47 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
08:45:47 HOL-Library: theory HOL-Library.Interval_Float
08:45:48 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
08:45:56 HOL-Library: theory HOL-Library.Library
08:46:09 HOL-Library: theory HOL-Library.RBT
08:46:09 HOL-Library: theory HOL-Library.RBT_Mapping
08:46:09 HOL-Library: theory HOL-Library.RBT_Set
08:48:06 Preparing HOL-Library/document ...
08:49:10 Finished HOL-Library/document (0:01:03 elapsed time)
08:49:10 Preparing HOL-Library/outline ...
08:49:47 Finished HOL-Library/outline (0:00:37 elapsed time)
08:49:49 Timing HOL-Library (8 threads, 96.916s elapsed time, 621.321s cpu time, 42.641s GC time, factor 6.41)
08:49:49 Finished HOL-Library (0:02:42 elapsed time, 0:12:57 cpu time, factor 4.78)
08:49:49 Building Category3 ...
08:49:52 Category3: theory HOL-Cardinals.Fun_More
08:49:52 Category3: theory Category3.Category
08:49:52 Category3: theory HOL-Cardinals.Order_Union
08:49:52 Category3: theory HereditarilyFinite.HF
08:49:52 Category3: theory HOL-Cardinals.Order_Relation_More
08:49:53 Category3: theory HOL-Cardinals.Wellorder_Extension
08:49:53 Category3: theory HOL-Cardinals.Wellfounded_More
08:49:53 Category3: theory HOL-Cardinals.Wellorder_Relation
08:49:53 Category3: theory Category3.ConcreteCategory
08:49:53 Category3: theory Category3.DiscreteCategory
08:49:53 Category3: theory Category3.DualCategory
08:49:53 Category3: theory Category3.EpiMonoIso
08:49:53 Category3: theory HOL-Cardinals.Wellorder_Embedding
08:49:54 Category3: theory HOL-Cardinals.Wellorder_Constructions
08:49:54 Category3: theory Category3.ProductCategory
08:49:54 Category3: theory Category3.InitialTerminal
08:49:55 Category3: theory HOL-Cardinals.Cardinal_Order_Relation
08:49:55 Category3: theory HOL-Cardinals.Ordinal_Arithmetic
08:49:55 Category3: theory Category3.FreeCategory
08:49:55 Category3: theory Category3.Functor
08:49:56 Category3: theory HOL-Cardinals.Cardinal_Arithmetic
08:49:56 Category3: theory HOL-Cardinals.Cardinals
08:50:01 Category3: theory Category3.NaturalTransformation
08:50:02 Category3: theory Category3.Subcategory
08:50:02 Category3: theory Category3.SetCategory
08:50:03 Category3: theory Category3.BinaryFunctor
08:50:06 Category3: theory Category3.SetCat
08:50:08 Category3: theory Category3.FunctorCategory
08:50:18 Category3: theory Category3.Yoneda
08:50:41 Category3: theory Category3.Adjunction
08:51:10 Category3: theory Category3.EquivalenceOfCategories
08:51:10 Category3: theory Category3.Limit
08:52:05 Category3: theory Category3.CartesianCategory
08:52:06 Category3: theory Category3.CategoryWithPullbacks
08:52:18 Category3: theory Category3.CartesianClosedCategory
08:52:19 Category3: theory Category3.CategoryWithFiniteLimits
08:52:20 Category3: theory Category3.HFSetCat
08:55:37 Preparing Category3/document ...
08:56:05 Finished Category3/document (0:00:28 elapsed time)
08:56:05 Preparing Category3/outline ...
08:56:16 Finished Category3/outline (0:00:10 elapsed time)
08:56:19 Timing Category3 (8 threads, 268.913s elapsed time, 1246.705s cpu time, 121.095s GC time, factor 4.64)
08:56:19 Finished Category3 (0:05:47 elapsed time, 0:23:22 cpu time, factor 4.04)
08:56:19 Building MonoidalCategory ...
08:56:22 MonoidalCategory: theory MonoidalCategory.MonoidalCategory
08:57:31 MonoidalCategory: theory MonoidalCategory.CartesianMonoidalCategory
08:57:31 MonoidalCategory: theory MonoidalCategory.MonoidalFunctor
08:58:00 MonoidalCategory: theory MonoidalCategory.FreeMonoidalCategory
09:03:18 Preparing MonoidalCategory/document ...
09:03:31 Finished MonoidalCategory/document (0:00:12 elapsed time)
09:03:31 Preparing MonoidalCategory/outline ...
09:03:37 Finished MonoidalCategory/outline (0:00:05 elapsed time)
09:03:40 Timing MonoidalCategory (8 threads, 350.550s elapsed time, 804.906s cpu time, 91.885s GC time, factor 2.30)
09:03:40 Finished MonoidalCategory (0:06:59 elapsed time, 0:15:40 cpu time, factor 2.24)
09:03:40 Running Bicategory ...
09:03:53 Bicategory: theory Bicategory.IsomorphismClass
09:03:53 Bicategory: theory Bicategory.Prebicategory
09:04:51 Bicategory: theory Bicategory.Bicategory
09:05:53 Bicategory: theory Bicategory.Coherence
09:05:56 Bicategory: theory Bicategory.InternalEquivalence
09:05:56 Bicategory: theory Bicategory.Subbicategory
09:08:30 Bicategory: theory Bicategory.CanonicalIsos
09:08:31 Bicategory: theory Bicategory.Pseudofunctor
09:12:20 Bicategory: theory Bicategory.Strictness
09:14:42 Bicategory: theory Bicategory.InternalAdjunction
09:18:17 Bicategory: theory Bicategory.PseudonaturalTransformation
09:18:17 Bicategory: theory Bicategory.Tabulation
09:18:18 Bicategory: theory Bicategory.SpanBicategory
09:25:48 Bicategory: theory Bicategory.EquivalenceOfBicategories
09:29:26 Bicategory: theory Bicategory.Modification
09:48:35 Bicategory: theory Bicategory.BicategoryOfSpans
10:11:00 Preparing Bicategory/document ...
10:12:38 Finished Bicategory/document (0:01:38 elapsed time)
10:12:38 Preparing Bicategory/outline ...
10:12:58 Finished Bicategory/outline (0:00:19 elapsed time)
10:13:00 Timing Bicategory (8 threads, 4033.923s elapsed time, 10613.761s cpu time, 1758.205s GC time, factor 2.63)
10:13:00 Finished Bicategory (1:07:19 elapsed time, 2:57:00 cpu time, factor 2.63)
10:13:00 Building ConcurrentIMP ...
10:13:02 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred
10:13:03 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang
10:13:13 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg
10:13:15 ConcurrentIMP: theory ConcurrentIMP.CIMP
10:13:15 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer_ex
10:13:15 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer_ex
10:13:45 Preparing ConcurrentIMP/document ...
10:13:49 Finished ConcurrentIMP/document (0:00:04 elapsed time)
10:13:49 Preparing ConcurrentIMP/outline ...
10:13:53 Finished ConcurrentIMP/outline (0:00:03 elapsed time)
10:13:54 Timing ConcurrentIMP (8 threads, 17.751s elapsed time, 46.424s cpu time, 2.950s GC time, factor 2.62)
10:13:54 Finished ConcurrentIMP (0:00:45 elapsed time, 0:01:38 cpu time, factor 2.18)
10:13:54 Running ConcurrentGC ...
10:13:56 ConcurrentGC: theory ConcurrentGC.Model
10:14:12 ConcurrentGC: theory ConcurrentGC.Tactics
10:14:19 ConcurrentGC: theory ConcurrentGC.Proofs_basis
10:14:23 ConcurrentGC: theory ConcurrentGC.TSO
10:14:32 ConcurrentGC: theory ConcurrentGC.Handshakes
10:16:19 ConcurrentGC: theory ConcurrentGC.MarkObject
10:17:56 ConcurrentGC: theory ConcurrentGC.StrongTricolour
10:18:21 ConcurrentGC: theory ConcurrentGC.Proofs
10:18:22 ConcurrentGC: theory ConcurrentGC.Concrete_heap
10:18:23 ConcurrentGC: theory ConcurrentGC.Concrete
10:41:56 Preparing ConcurrentGC/document ...
10:42:01 Finished ConcurrentGC/document (0:00:05 elapsed time)
10:42:01 Preparing ConcurrentGC/outline ...
10:42:06 Finished ConcurrentGC/outline (0:00:04 elapsed time)
10:42:07 Timing ConcurrentGC (8 threads, 1678.052s elapsed time, 11168.724s cpu time, 472.475s GC time, factor 6.66)
10:42:07 Finished ConcurrentGC (0:28:01 elapsed time, 3:06:13 cpu time, factor 6.64)
10:42:07 Unfinished session(s): Iptables_Semantics_Examples_Big
10:42:07 
10:42:07 === TIMING ===
10:42:07 
10:42:07 Group slow: 8:16:32 elapsed time, 24:43:04 cpu time, factor 2.99
10:42:07 Group AFP: 8:45:57 elapsed time, 26:32:14 cpu time, factor 3.03
10:42:07 Group main: 0:07:50 elapsed time, 0:28:43 cpu time, factor 3.66
10:42:07 Group timing: 0:02:42 elapsed time, 0:12:57 cpu time, factor 4.78
10:42:07 Group very_slow: 4:35:35 elapsed time, 6:58:29 cpu time, factor 1.52
10:42:07 Overall: 9:07:50 elapsed time, 27:01:23 cpu time, factor 2.96
10:42:07 
10:42:07 === FAILED SESSIONS ===
10:42:07 
10:42:07 Session Iptables_Semantics_Examples_Big: FAILED 1
10:42:07 Build step 'Execute shell' marked build as failure
10:42:07 Archiving artifacts
10:42:13 Started calculate disk usage of build
10:42:13 Finished Calculation of disk usage of build in 0 seconds
10:42:16 Started calculate disk usage of workspace
10:42:16 Finished Calculation of disk usage of workspace in 0 seconds
10:42:16 Email was triggered for: Failure - 1st
10:42:16 Trigger Failure - Any was overridden by another trigger and will not send an email.
10:42:16 Trigger Failure - Still was overridden by another trigger and will not send an email.
10:42:16 Sending email for trigger: Failure - 1st
10:42:16 Sending email to: isabelle-ci@mail46.informatik.tu-muenchen.de
10:42:16 Finished: FAILURE