Console Output

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