Console Output

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