Skip to content
[Jenkins]Jenkins
log in
Success

Console Output

01:33:30 Started by an SCM change


01:33:30 Running as SYSTEM


01:33:30 [EnvInject] - Loading node environment variables.


01:33:30 Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow


01:33:30 [isabelle-nightly-slow] $ hg showconfig paths.default


01:33:30 [isabelle-nightly-slow] $ hg pull --rev default


01:33:30 pulling from http://isabelle.in.tum.de/repos/isabelle/


01:33:30 real URL is https://isabelle.in.tum.de/repos/isabelle/


01:33:30 no changes found


01:33:30 [isabelle-nightly-slow] $ hg update --clean --rev default


01:33:47 29 files updated, 0 files merged, 3 files removed, 0 files unresolved


01:33:47 [isabelle-nightly-slow] $ hg --config extensions.purge= clean --all


01:33:47 [isabelle-nightly-slow] $ hg log --rev . --template {node}


01:33:47 [isabelle-nightly-slow] $ hg log --rev . --template {rev}


01:33:47 [isabelle-nightly-slow] $ hg log --rev e52a9b2084813a18973a14d44894178d4a81a8b8 --template exists\n


01:33:48 exists


01:33:48 [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(e52a9b2084813a18973a14d44894178d4a81a8b8)" --encoding UTF-8 --encodingmode replace


01:33:48 [afp] $ hg showconfig paths.default


01:33:48 [afp] $ hg pull --rev default


01:33:54 pulling from https://foss.heptapod.net/isa-afp/afp-devel/


01:33:54 no changes found


01:33:54 [afp] $ hg update --clean --rev default


01:34:08 0 files updated, 0 files merged, 0 files removed, 0 files unresolved


01:34:08 [afp] $ hg --config extensions.purge= clean --all


01:34:08 [afp] $ hg log --rev . --template {node}


01:34:08 [afp] $ hg log --rev . --template {rev}


01:34:08 [afp] $ hg log --rev 34dff8ee061c1acd2210177c824a42b9b9efd22c --template exists\n


01:34:09 exists


01:34:09 [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:34:09 No emails were triggered.


01:34:09 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins13762284352310157561.sh


01:34:09 + Admin/jenkins/run_build slow


01:34:09 + set -e


01:34:09 + PROFILE=slow


01:34:09 + shift


01:34:09 + bin/isabelle components -a


01:34:09 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1"


01:34:09 Getting "https://isabelle.sketis.net/components/kodkodi-1.5.6-1.tar.gz"


01:34:09 Unpacking "/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6-1.tar.gz"


01:34:10 + bin/isabelle jedit -bf


01:34:10 ### Building graph browser ...


01:34:10 warning: [options] bootstrap class path not set in conjunction with -source 7


01:34:10 warning: [options] source value 7 is obsolete and will be removed in a future release


01:34:10 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.


01:34:11 Note: Some input files use or override a deprecated API.


01:34:11 Note: Recompile with -Xlint:deprecation for details.


01:34:11 Note: Some input files use unchecked or unsafe operations.


01:34:11 Note: Recompile with -Xlint:unchecked for details.


01:34:11 3 warnings


01:34:11 ### Building Isabelle/Scala ...


01:34:40 ### Building Isabelle/jEdit ...


01:34:55 + bin/isabelle ocaml_setup


01:34:56 # Run eval $(opam env) to update the current shell environment


01:34:57 [NOTE] Package zarith is already installed (current version is 1.12).


01:34:57 + bin/isabelle ghc_setup


01:34:58 stack will use a sandboxed GHC it installed


01:34:58 For more information on paths, see 'stack path' and 'stack exec env'


01:34:58 To use this GHC and packages outside of a project, consider using:


01:34:58 stack ghc, stack ghci, stack runghc, or stack exec


01:34:58 The Glorious Glasgow Haskell Compilation System, version 8.8.4


01:34:59 + bin/isabelle ci_build_slow


01:35:02 

01:35:02 === CONFIGURATION ===


01:35:02 

01:35:02 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"


01:35:02 ISABELLE_BUILD_OPTIONS=""


01:35:02 

01:35:02 ML_PLATFORM="x86_64-linux"


01:35:02 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686/x86_64-linux"


01:35:02 ML_SYSTEM="polyml-5.8.2"


01:35:02 ML_OPTIONS="-H 4000 --maxheap 20G"


01:35:03 jobs = 1, threads = 8, numa = false


01:35:03 

01:35:03 === BUILD ===


01:35:03 

01:35:03 Build started at Wed, 31 Mar 2021 23:35:02 GMT


01:35:03 Isabelle id 419edc7f3726


01:35:03 Build for AFP id 34dff8ee061c


01:35:03 

01:35:03 === LOG ===


01:35:03 

01:35:14 Session Pure/Pure


01:35:14 Session FOL/FOL


01:35:14 Session Tools/Tools


01:35:14 Session HOL/HOL (main)


01:35:15 Session AFP/AWN (AFP)


01:35:15 Session AFP/AODV (AFP slow)


01:35:16 Session HOL/HOL-Cardinals (timing)


01:35:16 Session HOL/HOL-Library (main timing)


01:35:17 Session AFP/Binomial-Heaps (AFP)


01:35:17 Session AFP/ConcurrentIMP (AFP)


01:35:17 Session AFP/ConcurrentGC (AFP slow)


01:35:17 Session AFP/FinFun (AFP)


01:35:17 Session AFP/Finger-Trees (AFP)


01:35:17 Session HOL/HOL-Combinatorics (main timing)


01:35:17 Session HOL/HOL-Computational_Algebra (main timing)


01:35:18 Session HOL/HOL-Algebra (main timing)


01:35:18 Session HOL/HOL-Analysis (main timing)


01:35:19 Session AFP/Coinductive (AFP)


01:35:20 Session HOL/HOL-Eisbach


01:35:20 Session HOL/HOL-Number_Theory (main timing)


01:35:20 Session HOL/HOL-ex (timing)


01:35:20 Session AFP/Automatic_Refinement (AFP)


01:35:21 Session AFP/Refine_Monadic (AFP)


01:35:21 Session HOL/HOL-Imperative_HOL (timing)


01:35:21 Session AFP/HereditarilyFinite (AFP)


01:35:22 Session AFP/Category3 (AFP)


01:35:22 Session AFP/MonoidalCategory (AFP)


01:35:22 Session AFP/Bicategory (AFP slow)


01:35:23 Session AFP/Trie (AFP)


01:35:23 Session AFP/Flyspeck-Tame (AFP)


01:35:23 Session AFP/Flyspeck-Tame-Computation (AFP slow very_slow)


01:35:23 Session AFP/Word_Lib (AFP)


01:35:23 Session AFP/IP_Addresses (AFP)


01:35:24 Session AFP/Simple_Firewall (AFP)


01:35:24 Session AFP/Routing (AFP)


01:35:24 Session AFP/Native_Word (AFP)


01:35:24 Session AFP/Collections (AFP)


01:35:25 Session AFP/Iptables_Semantics (AFP)


01:35:25 Session AFP/Iptables_Semantics_Examples (AFP)


01:35:25 Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow)


01:35:25 Session AFP/JinjaThreads (AFP slow)


01:35:26 Building Pure ...


01:35:48 Pure: theory Pure


01:35:49 Pure: theory ML_Bootstrap


01:35:50 Pure: theory Pure.Sessions


01:35:53 Timing Pure (1 threads, 1.423s elapsed time, 1.403s cpu time, 0.057s GC time, factor 0.99)


01:35:53 Finished Pure (0:00:24 elapsed time, 0:00:23 cpu time, factor 0.98)


01:35:53 Building HOL ...


01:35:56 HOL: theory Tools.Code_Generator


01:36:02 HOL: theory HOL.HOL


01:36:07 HOL: theory HOL.Ctr_Sugar


01:36:07 HOL: theory HOL.Orderings


01:36:07 HOL: theory HOL.Argo


01:36:11 HOL: theory HOL.Groups


01:36:12 HOL: theory HOL.SAT


01:36:13 HOL: theory HOL.Lattices


01:36:17 HOL: theory HOL.Set


01:36:18 HOL: theory HOL.Fun


01:36:18 HOL: theory HOL.Typedef


01:36:19 HOL: theory HOL.Complete_Lattices


01:36:19 HOL: theory HOL.Rings


01:36:22 HOL: theory HOL.Inductive


01:36:25 HOL: theory HOL.Product_Type


01:36:25 HOL: theory HOL.Sum_Type


01:36:27 HOL: theory HOL.Complete_Partial_Order


01:36:31 HOL: theory HOL.Nat


01:36:34 HOL: theory HOL.Fields


01:36:34 HOL: theory HOL.Meson


01:36:35 HOL: theory HOL.ATP


01:36:39 HOL: theory HOL.Metis


01:36:41 HOL: theory HOL.Finite_Set


01:36:42 HOL: theory HOL.Relation


01:36:43 HOL: theory HOL.Transitive_Closure


01:36:44 HOL: theory HOL.Wellfounded


01:36:45 HOL: theory HOL.Fun_Def_Base


01:36:45 HOL: theory HOL.Hilbert_Choice


01:36:45 HOL: theory HOL.Wfrec


01:36:45 HOL: theory HOL.Order_Relation


01:36:46 HOL: theory HOL.BNF_Wellorder_Relation


01:36:49 HOL: theory HOL.BNF_Wellorder_Embedding


01:36:49 HOL: theory HOL.Zorn


01:36:49 HOL: theory HOL.BNF_Wellorder_Constructions


01:36:51 HOL: theory HOL.BNF_Cardinal_Order_Relation


01:36:51 HOL: theory HOL.BNF_Cardinal_Arithmetic


01:36:52 HOL: theory HOL.BNF_Def


01:36:55 HOL: theory HOL.BNF_Composition


01:36:55 HOL: theory HOL.Basic_BNFs


01:36:56 HOL: theory HOL.BNF_Fixpoint_Base


01:37:01 HOL: theory HOL.BNF_Least_Fixpoint


01:37:08 HOL: theory HOL.Basic_BNF_LFPs


01:37:08 HOL: theory HOL.Transfer


01:37:09 HOL: theory HOL.Num


01:37:13 HOL: theory HOL.Power


01:37:16 HOL: theory HOL.Groups_Big


01:37:19 HOL: theory HOL.Equiv_Relations


01:37:20 HOL: theory HOL.Lifting


01:37:22 HOL: theory HOL.Lifting_Set


01:37:22 HOL: theory HOL.Option


01:37:22 HOL: theory HOL.Quotient


01:37:23 HOL: theory HOL.Extraction


01:37:23 HOL: theory HOL.Lattices_Big


01:37:23 HOL: theory HOL.Partial_Function


01:37:24 HOL: theory HOL.Fun_Def


01:37:28 HOL: theory HOL.Int


01:37:31 HOL: theory HOL.Euclidean_Division


01:37:40 HOL: theory HOL.Parity


01:37:48 HOL: theory HOL.Divides


01:37:51 HOL: theory HOL.Numeral_Simprocs


01:37:51 HOL: theory HOL.Code_Numeral


01:37:51 HOL: theory HOL.Set_Interval


01:37:52 HOL: theory HOL.Semiring_Normalization


01:37:52 HOL: theory HOL.SMT


01:37:56 HOL: theory HOL.Groebner_Basis


01:37:58 HOL: theory HOL.Conditionally_Complete_Lattices


01:37:58 HOL: theory HOL.Filter


01:37:58 HOL: theory HOL.Presburger


01:38:02 HOL: theory HOL.Sledgehammer


01:38:06 HOL: theory HOL.List


01:38:16 HOL: theory HOL.Groups_List


01:38:16 HOL: theory HOL.Map


01:38:19 HOL: theory HOL.Factorial


01:38:19 HOL: theory HOL.Random


01:38:19 HOL: theory HOL.GCD


01:38:19 HOL: theory HOL.Enum


01:38:20 HOL: theory HOL.Binomial


01:38:23 HOL: theory HOL.String


01:38:26 HOL: theory HOL.BNF_Greatest_Fixpoint


01:38:26 HOL: theory HOL.Typerep


01:38:26 HOL: theory HOL.Predicate


01:38:27 HOL: theory HOL.Lazy_Sequence


01:38:28 HOL: theory HOL.Limited_Sequence


01:38:28 HOL: theory HOL.Code_Evaluation


01:38:32 HOL: theory HOL.Quickcheck_Random


01:38:35 HOL: theory HOL.Quickcheck_Exhaustive


01:38:35 HOL: theory HOL.Quickcheck_Narrowing


01:38:35 HOL: theory HOL.Random_Pred


01:38:35 HOL: theory HOL.Random_Sequence


01:38:40 HOL: theory HOL.Record


01:38:40 HOL: theory HOL.Predicate_Compile


01:38:44 HOL: theory HOL.Nitpick


01:38:54 HOL: theory HOL.Nunchaku


01:38:56 HOL: theory Main


01:38:57 HOL: theory HOL.Archimedean_Field


01:38:57 HOL: theory HOL.Hull


01:38:57 HOL: theory HOL.Topological_Spaces


01:38:57 HOL: theory HOL.Modules


01:38:58 HOL: theory HOL.Vector_Spaces


01:39:07 HOL: theory HOL.Rat


01:39:10 HOL: theory HOL.Real


01:39:13 HOL: theory HOL.Real_Vector_Spaces


01:39:31 HOL: theory HOL.Inequalities


01:39:31 HOL: theory HOL.Limits


01:39:39 HOL: theory HOL.Deriv


01:39:39 HOL: theory HOL.Series


01:39:41 HOL: theory HOL.NthRoot


01:39:42 HOL: theory HOL.Transcendental


01:39:48 HOL: theory HOL.Complex


01:39:49 HOL: theory HOL.MacLaurin


01:39:50 HOL: theory Complex_Main


01:40:58 Preparing HOL/document ...


01:42:15 Finished HOL/document (0:01:17 elapsed time)


01:42:16 Preparing HOL/outline ...


01:43:02 Finished HOL/outline (0:00:46 elapsed time)


01:43:05 Timing HOL (8 threads, 244.575s elapsed time, 798.800s cpu time, 68.754s GC time, factor 3.27)


01:43:05 Finished HOL (0:04:53 elapsed time, 0:15:02 cpu time, factor 3.07)


01:43:05 Running JinjaThreads ...


01:43:07 JinjaThreads: theory HOL-Eisbach.Eisbach


01:43:07 JinjaThreads: theory Automatic_Refinement.Foldi


01:43:07 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1


01:43:07 JinjaThreads: theory Automatic_Refinement.Prio_List


01:43:07 JinjaThreads: theory Collections.ICF_Tools


01:43:07 JinjaThreads: theory Finger-Trees.FingerTree


01:43:07 JinjaThreads: theory HOL-Library.AList


01:43:07 JinjaThreads: theory HOL-Library.Adhoc_Overloading


01:43:07 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot


01:43:07 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot


01:43:07 JinjaThreads: theory HOL-Library.Monad_Syntax


01:43:07 JinjaThreads: theory Collections.Ord_Code_Preproc


01:43:07 JinjaThreads: theory HOL-Library.Boolean_Algebra


01:43:07 JinjaThreads: theory HOL-Library.Cancellation


01:43:07 JinjaThreads: theory HOL-Library.Case_Converter


01:43:07 JinjaThreads: theory Collections.Locale_Code


01:43:07 JinjaThreads: theory Automatic_Refinement.Refine_Util


01:43:08 JinjaThreads: theory Collections.Record_Intf


01:43:08 JinjaThreads: theory HOL-Library.Bit_Operations


01:43:08 JinjaThreads: theory HOL-Library.Code_Abstract_Nat


01:43:08 JinjaThreads: theory HOL-Library.Simps_Case_Conv


01:43:08 JinjaThreads: theory HOL-Library.Code_Target_Nat


01:43:08 JinjaThreads: theory HOL-Library.Code_Target_Int


01:43:08 JinjaThreads: theory HOL-Library.Confluence


01:43:09 JinjaThreads: theory HOL-Library.Multiset


01:43:09 JinjaThreads: theory HOL-Library.Confluent_Quotient


01:43:09 JinjaThreads: theory Automatic_Refinement.Anti_Unification


01:43:09 JinjaThreads: theory Automatic_Refinement.Autoref_Data


01:43:09 JinjaThreads: theory Automatic_Refinement.Attr_Comb


01:43:09 JinjaThreads: theory Automatic_Refinement.Indep_Vars


01:43:09 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp


01:43:09 JinjaThreads: theory Automatic_Refinement.Tagged_Solver


01:43:09 JinjaThreads: theory Automatic_Refinement.Select_Solve


01:43:09 JinjaThreads: theory HOL-Library.Code_Target_Numeral


01:43:09 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms


01:43:09 JinjaThreads: theory HOL-Library.Dlist


01:43:09 JinjaThreads: theory HOL-Library.Infinite_Set


01:43:10 JinjaThreads: theory HOL-Library.Lattice_Syntax


01:43:10 JinjaThreads: theory HOL-Library.Complete_Partial_Order2


01:43:10 JinjaThreads: theory HOL-Library.Nat_Bijection


01:43:10 JinjaThreads: theory Trie.Trie


01:43:10 JinjaThreads: theory HOL-Library.Old_Datatype


01:43:10 JinjaThreads: theory HOL-Library.Option_ord


01:43:10 JinjaThreads: theory HOL-Library.Phantom_Type


01:43:11 JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs


01:43:11 JinjaThreads: theory HOL-Library.RBT_Impl


01:43:11 JinjaThreads: theory HOL-Library.Signed_Division


01:43:11 JinjaThreads: theory HOL-Library.Cardinality


01:43:11 JinjaThreads: theory HOL-Library.Sublist


01:43:12 JinjaThreads: theory HOL-Library.Transitive_Closure_Table


01:43:12 JinjaThreads: theory FinFun.FinFun


01:43:12 JinjaThreads: theory HOL-Library.Numeral_Type


01:43:13 JinjaThreads: theory HOL-Library.While_Combinator


01:43:13 JinjaThreads: theory HOL-Library.Countable


01:43:14 JinjaThreads: theory HOL-Library.Type_Length


01:43:14 JinjaThreads: theory Collections.DatRef


01:43:14 JinjaThreads: theory JinjaThreads.Set_Monad


01:43:14 JinjaThreads: theory JinjaThreads.Set_without_equal


01:43:14 JinjaThreads: theory Refine_Monadic.Refine_Chapter


01:43:15 JinjaThreads: theory Binomial-Heaps.BinomialHeap


01:43:15 JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap


01:43:15 JinjaThreads: theory HOL-ex.Quicksort


01:43:15 JinjaThreads: theory HOL-Library.Countable_Set


01:43:15 JinjaThreads: theory Automatic_Refinement.Misc


01:43:15 JinjaThreads: theory JinjaThreads.Auxiliary


01:43:15 JinjaThreads: theory HOL-Library.Countable_Complete_Lattices


01:43:15 JinjaThreads: theory HOL-Library.Word


01:43:17 JinjaThreads: theory Word_Lib.More_Arithmetic


01:43:18 JinjaThreads: theory HOL-Library.Order_Continuity


01:43:18 JinjaThreads: theory HOL-Library.Extended_Nat


01:43:19 JinjaThreads: theory Coinductive.Coinductive_Nat


01:43:21 JinjaThreads: theory Automatic_Refinement.Refine_Lib


01:43:21 JinjaThreads: theory Collections.SetIterator


01:43:21 JinjaThreads: theory Collections.Sorted_List_Operations


01:43:21 JinjaThreads: theory Coinductive.Coinductive_List


01:43:22 JinjaThreads: theory Automatic_Refinement.Autoref_Phases


01:43:22 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging


01:43:22 JinjaThreads: theory Automatic_Refinement.Relators


01:43:22 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover


01:43:22 JinjaThreads: theory Collections.SetIteratorOperations


01:43:23 JinjaThreads: theory Automatic_Refinement.Param_Tool


01:43:24 JinjaThreads: theory Automatic_Refinement.Param_HOL


01:43:24 JinjaThreads: theory Word_Lib.Bit_Comprehension


01:43:24 JinjaThreads: theory Word_Lib.More_Divides


01:43:25 JinjaThreads: theory Word_Lib.Signed_Words


01:43:25 JinjaThreads: theory Word_Lib.Signed_Division_Word


01:43:25 JinjaThreads: theory Word_Lib.More_Word


01:43:25 JinjaThreads: theory Collections.Assoc_List


01:43:26 JinjaThreads: theory Automatic_Refinement.Parametricity


01:43:26 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops


01:43:26 JinjaThreads: theory Collections.Dlist_add


01:43:26 JinjaThreads: theory Collections.Proper_Iterator


01:43:26 JinjaThreads: theory Collections.Diff_Array


01:43:26 JinjaThreads: theory Collections.Trie_Impl


01:43:26 JinjaThreads: theory Collections.SetIteratorGA


01:43:26 JinjaThreads: theory Word_Lib.Traditional_Infix_Syntax


01:43:27 JinjaThreads: theory Collections.Trie2


01:43:27 JinjaThreads: theory Collections.It_to_It


01:43:27 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel


01:43:28 JinjaThreads: theory Automatic_Refinement.Autoref_Translate


01:43:28 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface


01:43:28 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo


01:43:28 JinjaThreads: theory Automatic_Refinement.Autoref_Tool


01:43:29 JinjaThreads: theory Word_Lib.Bits_Int


01:43:29 JinjaThreads: theory Coinductive.Lazy_LList


01:43:29 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL


01:43:29 JinjaThreads: theory Coinductive.TLList


01:43:30 JinjaThreads: theory Native_Word.More_Bits_Int


01:43:30 JinjaThreads: theory Word_Lib.Least_significant_bit


01:43:30 JinjaThreads: theory Word_Lib.Most_significant_bit


01:43:31 JinjaThreads: theory Word_Lib.Generic_set_bit


01:43:31 JinjaThreads: theory Coinductive.Lazy_TLList


01:43:32 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement


01:43:32 JinjaThreads: theory Collections.Idx_Iterator


01:43:32 JinjaThreads: theory Refine_Monadic.Refine_Misc


01:43:32 JinjaThreads: theory Native_Word.Code_Symbolic_Bits_Int


01:43:33 JinjaThreads: theory Native_Word.Bits_Integer


01:43:33 JinjaThreads: theory Refine_Monadic.RefineG_Domain


01:43:33 JinjaThreads: theory Refine_Monadic.RefineG_Transfer


01:43:34 JinjaThreads: theory Refine_Monadic.RefineG_Assert


01:43:34 JinjaThreads: theory Refine_Monadic.RefineG_Recursion


01:43:35 JinjaThreads: theory Refine_Monadic.RefineG_While


01:43:35 JinjaThreads: theory Refine_Monadic.Refine_Basic


01:43:36 JinjaThreads: theory Refine_Monadic.Refine_Det


01:43:40 JinjaThreads: theory Refine_Monadic.Refine_Heuristics


01:43:40 JinjaThreads: theory Refine_Monadic.Refine_Leof


01:43:40 JinjaThreads: theory Refine_Monadic.Refine_Pfun


01:43:40 JinjaThreads: theory Refine_Monadic.Refine_More_Comb


01:43:42 JinjaThreads: theory Refine_Monadic.Refine_While


01:43:44 JinjaThreads: theory Refine_Monadic.Refine_Transfer


01:43:44 JinjaThreads: theory Refine_Monadic.Autoref_Monadic


01:43:44 JinjaThreads: theory Refine_Monadic.Refine_Automation


01:43:45 JinjaThreads: theory Refine_Monadic.Refine_Foreach


01:43:50 JinjaThreads: theory Refine_Monadic.Refine_Monadic


01:43:50 JinjaThreads: theory Native_Word.Code_Target_Bits_Int


01:43:50 JinjaThreads: theory Native_Word.Code_Target_Word_Base


01:43:50 JinjaThreads: theory Collections.Code_Target_ICF


01:43:51 JinjaThreads: theory Native_Word.Uint32


01:43:51 JinjaThreads: theory Collections.Gen_Iterator


01:43:51 JinjaThreads: theory Collections.Intf_Map


01:43:51 JinjaThreads: theory Collections.Intf_Set


01:43:52 JinjaThreads: theory Collections.Iterator


01:43:53 JinjaThreads: theory Collections.HashCode


01:43:53 JinjaThreads: theory Collections.Array_Iterator


01:43:53 JinjaThreads: theory Collections.ICF_Spec_Base


01:43:53 JinjaThreads: theory Collections.AnnotatedListSpec


01:43:53 JinjaThreads: theory Collections.ListSpec


01:43:53 JinjaThreads: theory Collections.MapSpec


01:43:53 JinjaThreads: theory Collections.PrioSpec


01:43:53 JinjaThreads: theory Collections.PrioUniqueSpec


01:43:53 JinjaThreads: theory Collections.SetSpec


01:43:55 JinjaThreads: theory Collections.BinoPrioImpl


01:43:55 JinjaThreads: theory Collections.SkewPrioImpl


01:43:55 JinjaThreads: theory Collections.ListGA


01:43:56 JinjaThreads: theory Collections.FTAnnotatedListImpl


01:43:56 JinjaThreads: theory Collections.PrioByAnnotatedList


01:43:56 JinjaThreads: theory Collections.Fifo


01:43:58 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList


01:43:58 JinjaThreads: theory Collections.Algos


01:43:59 JinjaThreads: theory Collections.SetIndex


01:43:59 JinjaThreads: theory Collections.SetIteratorCollectionsGA


01:44:00 JinjaThreads: theory Collections.MapGA


01:44:00 JinjaThreads: theory Collections.SetGA


01:44:02 JinjaThreads: theory Collections.FTPrioImpl


01:44:02 JinjaThreads: theory Collections.FTPrioUniqueImpl


01:44:03 JinjaThreads: theory Collections.ArrayMapImpl


01:44:03 JinjaThreads: theory Collections.ListMapImpl


01:44:03 JinjaThreads: theory Collections.ListMapImpl_Invar


01:44:04 JinjaThreads: theory Collections.TrieMapImpl


01:44:06 JinjaThreads: theory Collections.ListSetImpl


01:44:07 JinjaThreads: theory Collections.ListSetImpl_Invar


01:44:08 JinjaThreads: theory Collections.ListSetImpl_NotDist


01:44:09 JinjaThreads: theory Collections.ListSetImpl_Sorted


01:44:10 JinjaThreads: theory Collections.SetByMap


01:44:11 JinjaThreads: theory Collections.ArrayHashMap_Impl


01:44:13 JinjaThreads: theory Collections.ArraySetImpl


01:44:13 JinjaThreads: theory Collections.TrieSetImpl


01:44:13 JinjaThreads: theory Collections.RBT_add


01:44:13 JinjaThreads: theory HOL-Library.RBT


01:44:16 JinjaThreads: theory Collections.ArrayHashMap


01:44:16 JinjaThreads: theory Collections.RBTMapImpl


01:44:22 JinjaThreads: theory Collections.ArrayHashSet


01:44:24 JinjaThreads: theory Collections.RBTSetImpl


01:44:24 JinjaThreads: theory Collections.HashMap_Impl


01:44:26 JinjaThreads: theory Collections.HashMap


01:44:33 JinjaThreads: theory Collections.HashSet


01:44:33 JinjaThreads: theory Collections.MapStdImpl


01:44:39 JinjaThreads: theory Collections.SetStdImpl


01:44:43 JinjaThreads: theory Collections.ICF_Impl


01:44:49 JinjaThreads: theory Collections.ICF_Refine_Monadic


01:44:50 JinjaThreads: theory Collections.ICF_Autoref


01:44:54 JinjaThreads: theory Collections.Collections


01:44:54 JinjaThreads: theory Collections.CollectionsV1


01:45:00 JinjaThreads: theory JinjaThreads.JT_ICF


01:45:00 JinjaThreads: theory JinjaThreads.Basic_Main


01:46:05 JinjaThreads: theory HOL-Library.Mapping


01:46:05 JinjaThreads: theory HOL-Library.Prefix_Order


01:46:05 JinjaThreads: theory JinjaThreads.FWState


01:46:05 JinjaThreads: theory JinjaThreads.LTS


01:46:05 JinjaThreads: theory JinjaThreads.Type


01:46:05 JinjaThreads: theory JinjaThreads.ListIndex


01:46:05 JinjaThreads: theory JinjaThreads.Orders


01:46:05 JinjaThreads: theory JinjaThreads.Semilat


01:46:06 JinjaThreads: theory JinjaThreads.Err


01:46:07 JinjaThreads: theory HOL-Library.AList_Mapping


01:46:07 JinjaThreads: theory JinjaThreads.Listn


01:46:07 JinjaThreads: theory JinjaThreads.Opt


01:46:07 JinjaThreads: theory JinjaThreads.Product


01:46:08 JinjaThreads: theory JinjaThreads.Semilattices


01:46:08 JinjaThreads: theory JinjaThreads.Decl


01:46:08 JinjaThreads: theory JinjaThreads.Typing_Framework


01:46:08 JinjaThreads: theory JinjaThreads.SemilatAlg


01:46:09 JinjaThreads: theory JinjaThreads.Kildall


01:46:09 JinjaThreads: theory JinjaThreads.LBVSpec


01:46:09 JinjaThreads: theory JinjaThreads.Typing_Framework_err


01:46:10 JinjaThreads: theory JinjaThreads.Bisimulation


01:46:10 JinjaThreads: theory JinjaThreads.LBVComplete


01:46:10 JinjaThreads: theory JinjaThreads.LBVCorrect


01:46:11 JinjaThreads: theory JinjaThreads.Abstract_BV


01:46:11 JinjaThreads: theory JinjaThreads.TypeRel


01:46:16 JinjaThreads: theory JinjaThreads.TypeRelRefine


01:46:16 JinjaThreads: theory JinjaThreads.Value


01:46:20 JinjaThreads: theory JinjaThreads.Exceptions


01:46:20 JinjaThreads: theory JinjaThreads.Heap


01:46:21 JinjaThreads: theory JinjaThreads.SystemClasses


01:46:23 JinjaThreads: theory JinjaThreads.MM


01:46:23 JinjaThreads: theory JinjaThreads.State


01:46:31 JinjaThreads: theory JinjaThreads.FWCondAction


01:46:31 JinjaThreads: theory JinjaThreads.FWInterrupt


01:46:31 JinjaThreads: theory JinjaThreads.FWLock


01:46:31 JinjaThreads: theory JinjaThreads.FWThread


01:46:31 JinjaThreads: theory JinjaThreads.FWWait


01:46:31 JinjaThreads: theory JinjaThreads.Observable_Events


01:46:35 JinjaThreads: theory JinjaThreads.FWLocking


01:46:37 JinjaThreads: theory JinjaThreads.FWLockingThread


01:46:37 JinjaThreads: theory JinjaThreads.FWWellform


01:46:38 JinjaThreads: theory JinjaThreads.FWLifting


01:46:38 JinjaThreads: theory JinjaThreads.FWSemantics


01:46:40 JinjaThreads: theory JinjaThreads.JVMState


01:46:40 JinjaThreads: theory JinjaThreads.JMM_Spec


01:46:40 JinjaThreads: theory JinjaThreads.StartConfig


01:46:45 JinjaThreads: theory JinjaThreads.FWLiftingSem


01:46:45 JinjaThreads: theory JinjaThreads.FWProgressAux


01:46:45 JinjaThreads: theory JinjaThreads.Conform


01:46:47 JinjaThreads: theory JinjaThreads.State_Refinement


01:46:47 JinjaThreads: theory JinjaThreads.FWDeadlock


01:46:47 JinjaThreads: theory JinjaThreads.FWLTS


01:46:48 JinjaThreads: theory JinjaThreads.ConformThreaded


01:46:48 JinjaThreads: theory JinjaThreads.ExternalCall


01:46:48 JinjaThreads: theory JinjaThreads.SC


01:46:49 JinjaThreads: theory JinjaThreads.SC_Collections


01:46:50 JinjaThreads: theory JinjaThreads.FWProgress


01:46:59 JinjaThreads: theory JinjaThreads.JMM_DRF


01:46:59 JinjaThreads: theory JinjaThreads.SC_Legal


01:47:02 JinjaThreads: theory JinjaThreads.FWBisimulation


01:47:02 JinjaThreads: theory JinjaThreads.FWInitFinLift


01:47:02 JinjaThreads: theory JinjaThreads.Non_Speculative


01:47:03 JinjaThreads: theory JinjaThreads.Scheduler


01:47:05 JinjaThreads: theory JinjaThreads.HB_Completion


01:47:05 JinjaThreads: theory JinjaThreads.SC_Completion


01:47:19 JinjaThreads: theory JinjaThreads.WellForm


01:47:19 JinjaThreads: theory JinjaThreads.ExternalCall_Execute


01:47:21 JinjaThreads: theory JinjaThreads.ExternalCallWF


01:47:21 JinjaThreads: theory JinjaThreads.JMM_Heap


01:47:21 JinjaThreads: theory JinjaThreads.SemiType


01:47:24 JinjaThreads: theory JinjaThreads.BinOp


01:47:24 JinjaThreads: theory JinjaThreads.JVM_SemiType


01:47:27 JinjaThreads: theory JinjaThreads.JMM_Type


01:47:27 JinjaThreads: theory JinjaThreads.JMM_Type2


01:47:36 JinjaThreads: theory JinjaThreads.Random_Scheduler


01:47:38 JinjaThreads: theory JinjaThreads.Round_Robin


01:47:39 JinjaThreads: theory JinjaThreads.JMM_Framework


01:47:48 JinjaThreads: theory JinjaThreads.SC_Schedulers


01:47:51 JinjaThreads: theory JinjaThreads.Expr


01:47:51 JinjaThreads: theory JinjaThreads.JVMInstructions


01:47:51 JinjaThreads: theory JinjaThreads.PCompiler


01:47:52 JinjaThreads: theory JinjaThreads.PCompilerRefine


01:48:01 JinjaThreads: theory JinjaThreads.JVMExceptions


01:48:01 JinjaThreads: theory JinjaThreads.Effect


01:48:02 JinjaThreads: theory JinjaThreads.JVMHeap


01:48:18 JinjaThreads: theory JinjaThreads.JVMExecInstr


01:48:26 JinjaThreads: theory JinjaThreads.CallExpr


01:48:27 JinjaThreads: theory JinjaThreads.DefAss


01:48:27 JinjaThreads: theory JinjaThreads.JHeap


01:48:27 JinjaThreads: theory JinjaThreads.WWellForm


01:48:27 JinjaThreads: theory JinjaThreads.WellType


01:48:28 JinjaThreads: theory JinjaThreads.JVMExec


01:48:31 JinjaThreads: theory JinjaThreads.JVMDefensive


01:48:32 JinjaThreads: theory JinjaThreads.J1State


01:48:33 JinjaThreads: theory JinjaThreads.SmallStep


01:48:33 JinjaThreads: theory JinjaThreads.Annotate


01:48:36 JinjaThreads: theory JinjaThreads.J1Heap


01:48:37 JinjaThreads: theory JinjaThreads.J1WellType


01:48:40 JinjaThreads: theory JinjaThreads.JWellForm


01:48:40 JinjaThreads: theory JinjaThreads.WellTypeRT


01:48:41 JinjaThreads: theory JinjaThreads.J1WellForm


01:48:47 JinjaThreads: theory JinjaThreads.JVMThreaded


01:48:49 JinjaThreads: theory JinjaThreads.JVMExec_Execute


01:48:52 JinjaThreads: theory JinjaThreads.JMM_Typesafe


01:49:00 JinjaThreads: theory JinjaThreads.Compiler1


01:49:02 JinjaThreads: theory JinjaThreads.Compiler2


01:49:06 JinjaThreads: theory JinjaThreads.JJ1WellForm


01:49:08 JinjaThreads: theory JinjaThreads.Preprocessor


01:49:08 JinjaThreads: theory JinjaThreads.ToString


01:49:08 JinjaThreads: theory JinjaThreads.JMM_JVM


01:49:09 JinjaThreads: theory JinjaThreads.JVM_Main


01:49:11 JinjaThreads: theory JinjaThreads.JMM_Common


01:49:13 JinjaThreads: theory JinjaThreads.Compiler


01:49:13 JinjaThreads: theory JinjaThreads.Exception_Tables


01:49:19 JinjaThreads: theory JinjaThreads.BVSpec


01:49:19 JinjaThreads: theory JinjaThreads.EffectMono


01:49:19 JinjaThreads: theory JinjaThreads.JMM_Typesafe2


01:49:19 JinjaThreads: theory JinjaThreads.TF_JVM


01:49:19 JinjaThreads: theory JinjaThreads.BVConform


01:49:20 JinjaThreads: theory JinjaThreads.TypeComp


01:49:24 JinjaThreads: theory JinjaThreads.BVExec


01:49:24 JinjaThreads: theory JinjaThreads.LBVJVM


01:49:28 JinjaThreads: theory JinjaThreads.FWBisimLift


01:49:28 JinjaThreads: theory JinjaThreads.FWBisimDeadlock


01:49:28 JinjaThreads: theory JinjaThreads.J1


01:49:30 JinjaThreads: theory JinjaThreads.BVSpecTypeSafe


01:49:44 JinjaThreads: theory JinjaThreads.BVNoTypeError


01:49:47 JinjaThreads: theory JinjaThreads.BCVExec


01:49:47 JinjaThreads: theory JinjaThreads.JVMExec_Execute2


01:49:47 JinjaThreads: theory JinjaThreads.BVProgressThreaded


01:49:48 JinjaThreads: theory JinjaThreads.JVMTau


01:50:01 JinjaThreads: theory JinjaThreads.Common_Main


01:50:26 JinjaThreads: theory JinjaThreads.J1Deadlock


01:50:37 JinjaThreads: theory JinjaThreads.Execs


01:50:55 JinjaThreads: theory JinjaThreads.DefAssPreservation


01:50:55 JinjaThreads: theory JinjaThreads.Threaded


01:50:55 JinjaThreads: theory JinjaThreads.Progress


01:51:02 JinjaThreads: theory JinjaThreads.TypeSafe


01:51:29 JinjaThreads: theory JinjaThreads.J0


01:51:29 JinjaThreads: theory JinjaThreads.JMM_J


01:51:35 JinjaThreads: theory JinjaThreads.ProgressThreaded


01:51:38 JinjaThreads: theory JinjaThreads.J_Execute


01:55:35 JinjaThreads: theory JinjaThreads.J1JVMBisim


01:55:54 JinjaThreads: theory JinjaThreads.JVMDeadlocked


01:55:55 JinjaThreads: theory JinjaThreads.Deadlocked


01:55:55 JinjaThreads: theory JinjaThreads.DRF_J


01:55:55 JinjaThreads: theory JinjaThreads.DRF_JVM


01:55:58 JinjaThreads: theory JinjaThreads.JVM_Execute


01:56:02 JinjaThreads: theory JinjaThreads.J_Main


01:56:02 JinjaThreads: theory JinjaThreads.J0Bisim


01:56:11 JinjaThreads: theory JinjaThreads.J0J1Bisim


01:56:19 JinjaThreads: theory JinjaThreads.JVM_Execute2


01:56:38 JinjaThreads: theory JinjaThreads.BV_Main


01:56:59 JinjaThreads: theory JinjaThreads.Correctness1


01:57:01 JinjaThreads: theory JinjaThreads.Correctness1Threaded


01:57:12 JinjaThreads: theory JinjaThreads.Code_Generation


01:57:22 JinjaThreads: theory JinjaThreads.ApprenticeChallenge


01:57:24 JinjaThreads: theory JinjaThreads.BufferExample


01:57:38 JinjaThreads: theory JinjaThreads.Java2Jinja


01:57:50 JinjaThreads: theory JinjaThreads.Examples_Main


01:59:33 JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe


01:59:42 JinjaThreads: theory JinjaThreads.JMM_J_Typesafe


02:00:09 JinjaThreads: theory JinjaThreads.J1JVM


02:00:10 JinjaThreads: theory JinjaThreads.JVMJ1


02:00:25 JinjaThreads: theory JinjaThreads.Execute_Main


02:02:05 JinjaThreads: theory JinjaThreads.Correctness2


02:10:06 JinjaThreads: theory JinjaThreads.Correctness


02:16:08 JinjaThreads: theory JinjaThreads.JMM_Compiler


02:16:08 JinjaThreads: theory JinjaThreads.SC_Interp


02:16:13 JinjaThreads: theory JinjaThreads.Compiler_Main


02:26:23 JinjaThreads: theory JinjaThreads.JMM_Interp


02:26:26 JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2


02:26:27 JinjaThreads: theory JinjaThreads.JMM


02:26:29 JinjaThreads: theory JinjaThreads.MM_Main


02:26:35 JinjaThreads: theory JinjaThreads.JinjaThreads


02:29:53 Preparing JinjaThreads/document ...


02:31:10 Finished JinjaThreads/document (0:01:16 elapsed time)


02:31:10 Preparing JinjaThreads/outline ...


02:31:44 Finished JinjaThreads/outline (0:00:33 elapsed time)


02:31:45 Timing JinjaThreads (8 threads, 2781.657s elapsed time, 13099.566s cpu time, 5527.932s GC time, factor 4.71)


02:31:45 Finished JinjaThreads (0:46:35 elapsed time, 3:39:27 cpu time, factor 4.71)


02:31:45 Building Flyspeck-Tame ...


02:31:47 Flyspeck-Tame: theory Flyspeck-Tame.ListAux


02:31:47 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order


02:31:47 Flyspeck-Tame: theory HOL-Library.AList


02:31:47 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl


02:31:47 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat


02:31:47 Flyspeck-Tame: theory HOL-Library.Code_Target_Int


02:31:47 Flyspeck-Tame: theory HOL-Library.IArray


02:31:47 Flyspeck-Tame: theory HOL-Library.While_Combinator


02:31:47 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat


02:31:47 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso


02:31:48 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral


02:31:48 Flyspeck-Tame: theory Flyspeck-Tame.Arch


02:31:48 Flyspeck-Tame: theory Flyspeck-Tame.Worklist


02:31:48 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax


02:31:48 Flyspeck-Tame: theory Flyspeck-Tame.ListSum


02:31:48 Flyspeck-Tame: theory Flyspeck-Tame.Rotation


02:31:49 Flyspeck-Tame: theory Flyspeck-Tame.Graph


02:31:49 Flyspeck-Tame: theory Flyspeck-Tame.Maps


02:31:49 Flyspeck-Tame: theory Trie.Trie


02:31:51 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision


02:31:51 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps


02:31:51 Flyspeck-Tame: theory Flyspeck-Tame.Tame


02:31:52 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator


02:31:52 Flyspeck-Tame: theory Trie.Tries


02:31:52 Flyspeck-Tame: theory Flyspeck-Tame.TameProps


02:31:52 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps


02:31:52 Flyspeck-Tame: theory Flyspeck-Tame.Plane


02:31:53 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps


02:31:53 Flyspeck-Tame: theory Flyspeck-Tame.Plane1


02:31:53 Flyspeck-Tame: theory Flyspeck-Tame.Generator


02:31:53 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum


02:31:57 Flyspeck-Tame: theory Flyspeck-Tame.Invariants


02:31:58 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux


02:31:58 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps


02:31:58 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps


02:31:58 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props


02:31:59 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound


02:31:59 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps


02:32:00 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps


02:32:00 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps


02:32:00 Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness


02:33:22 Preparing Flyspeck-Tame/document ...


02:33:35 Finished Flyspeck-Tame/document (0:00:12 elapsed time)


02:33:35 Preparing Flyspeck-Tame/outline ...


02:33:41 Finished Flyspeck-Tame/outline (0:00:06 elapsed time)


02:33:43 Timing Flyspeck-Tame (8 threads, 58.601s elapsed time, 317.769s cpu time, 26.190s GC time, factor 5.42)


02:33:43 Finished Flyspeck-Tame (0:01:35 elapsed time, 0:06:33 cpu time, factor 4.13)


02:33:43 Running Flyspeck-Tame-Computation ...


02:33:45 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.ArchComp


02:33:45 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.Completeness


06:49:48 Timing Flyspeck-Tame-Computation (8 threads, 15359.619s elapsed time, 23024.214s cpu time, 815.711s GC time, factor 1.50)


06:49:48 Finished Flyspeck-Tame-Computation (4:16:01 elapsed time, 6:23:46 cpu time, factor 1.50)


06:49:48 Building AWN ...


06:49:50 AWN: theory AWN.Lib


06:49:50 AWN: theory AWN.TransitionSystems


06:49:50 AWN: theory AWN.AWN


06:49:51 AWN: theory AWN.Invariants


06:49:51 AWN: theory AWN.OInvariants


06:50:01 AWN: theory AWN.AWN_Cterms


06:50:01 AWN: theory AWN.AWN_SOS


06:50:02 AWN: theory AWN.OAWN_SOS


06:50:04 AWN: theory AWN.AWN_Labels


06:50:05 AWN: theory AWN.Pnet


06:50:05 AWN: theory AWN.Inv_Cterms


06:50:05 AWN: theory AWN.AWN_Invariants


06:50:06 AWN: theory AWN.Closed


06:50:06 AWN: theory AWN.AWN_SOS_Labels


06:50:07 AWN: theory AWN.Qmsg


06:50:08 AWN: theory AWN.OAWN_Invariants


06:50:08 AWN: theory AWN.OAWN_SOS_Labels


06:50:08 AWN: theory AWN.ONode_Lifting


06:50:08 AWN: theory AWN.OPnet


06:50:08 AWN: theory AWN.OPnet_Lifting


06:50:09 AWN: theory AWN.OClosed_Lifting


06:50:09 AWN: theory AWN.OClosed_Transfer


06:50:09 AWN: theory AWN.OAWN_Convert


06:50:09 AWN: theory AWN.Qmsg_Lifting


06:50:10 AWN: theory AWN.AWN_Main


06:50:10 AWN: theory AWN.Toy


06:50:20 AWN: theory AWN.AWN_Term_Graph


06:50:50 Preparing AWN/document ...


06:50:58 Finished AWN/document (0:00:08 elapsed time)


06:50:58 Preparing AWN/outline ...


06:51:03 Finished AWN/outline (0:00:05 elapsed time)


06:51:04 Timing AWN (8 threads, 33.554s elapsed time, 159.774s cpu time, 6.929s GC time, factor 4.76)


06:51:04 Finished AWN (0:00:59 elapsed time, 0:03:33 cpu time, factor 3.57)


06:51:04 Running AODV ...


06:51:06 AODV: theory AODV.Aodv_Basic


06:51:07 AODV: theory AODV.A_Norreqid


06:51:07 AODV: theory AODV.Aodv_Data


06:51:07 AODV: theory AODV.B_Fwdrreps


06:51:07 AODV: theory AODV.Aodv_Message


06:51:07 AODV: theory AODV.C_Gtobcast


06:51:07 AODV: theory AODV.D_Fwdrreqs


06:51:07 AODV: theory AODV.E_All_ABCD


06:51:07 AODV: theory AODV.C_Aodv_Data


06:51:07 AODV: theory AODV.C_Aodv_Message


06:51:07 AODV: theory AODV.D_Aodv_Data


06:51:07 AODV: theory AODV.D_Aodv_Message


06:51:07 AODV: theory AODV.A_Aodv_Data


06:51:07 AODV: theory AODV.A_Aodv_Message


06:51:10 AODV: theory AODV.B_Aodv_Data


06:51:10 AODV: theory AODV.B_Aodv_Message


06:51:10 AODV: theory AODV.C_Fresher


06:51:10 AODV: theory AODV.D_Fresher


06:51:10 AODV: theory AODV.A_Fresher


06:51:10 AODV: theory AODV.Fresher


06:51:10 AODV: theory AODV.E_Aodv_Data


06:51:10 AODV: theory AODV.E_Aodv_Message


06:51:12 AODV: theory AODV.A_Aodv


06:51:12 AODV: theory AODV.Aodv


06:51:12 AODV: theory AODV.C_Aodv


06:51:12 AODV: theory AODV.D_Aodv


06:51:12 AODV: theory AODV.E_Fresher


06:51:12 AODV: theory AODV.B_Fresher


06:51:13 AODV: theory AODV.B_Aodv


06:51:13 AODV: theory AODV.E_Aodv


06:51:46 AODV: theory AODV.A_Aodv_Predicates


06:51:46 AODV: theory AODV.A_Loop_Freedom


06:51:47 AODV: theory AODV.A_Quality_Increases


06:51:47 AODV: theory AODV.A_Seq_Invariants


06:51:48 AODV: theory AODV.A_OAodv


06:51:48 AODV: theory AODV.A_Global_Invariants


06:51:49 AODV: theory AODV.A_Aodv_Loop_Freedom


06:51:50 AODV: theory AODV.C_Aodv_Predicates


06:51:50 AODV: theory AODV.C_Loop_Freedom


06:51:50 AODV: theory AODV.C_Quality_Increases


06:51:51 AODV: theory AODV.C_Seq_Invariants


06:51:52 AODV: theory AODV.C_OAodv


06:51:52 AODV: theory AODV.C_Global_Invariants


06:51:53 AODV: theory AODV.C_Aodv_Loop_Freedom


06:51:58 AODV: theory AODV.Aodv_Predicates


06:51:58 AODV: theory AODV.Loop_Freedom


06:51:58 AODV: theory AODV.Quality_Increases


06:51:59 AODV: theory AODV.Seq_Invariants


06:51:59 AODV: theory AODV.OAodv


06:51:59 AODV: theory AODV.Global_Invariants


06:52:00 AODV: theory AODV.Aodv_Loop_Freedom


06:52:01 AODV: theory AODV.E_Aodv_Predicates


06:52:01 AODV: theory AODV.E_OAodv


06:52:01 AODV: theory AODV.E_Loop_Freedom


06:52:02 AODV: theory AODV.E_Quality_Increases


06:52:02 AODV: theory AODV.E_Seq_Invariants


06:52:02 AODV: theory AODV.E_Global_Invariants


06:52:03 AODV: theory AODV.E_Aodv_Loop_Freedom


06:52:04 AODV: theory AODV.D_Aodv_Predicates


06:52:04 AODV: theory AODV.D_OAodv


06:52:04 AODV: theory AODV.D_Loop_Freedom


06:52:04 AODV: theory AODV.D_Quality_Increases


06:52:04 AODV: theory AODV.D_Seq_Invariants


06:52:05 AODV: theory AODV.B_Aodv_Predicates


06:52:05 AODV: theory AODV.B_OAodv


06:52:05 AODV: theory AODV.D_Global_Invariants


06:52:05 AODV: theory AODV.B_Loop_Freedom


06:52:05 AODV: theory AODV.B_Quality_Increases


06:52:05 AODV: theory AODV.B_Seq_Invariants


06:52:06 AODV: theory AODV.D_Aodv_Loop_Freedom


06:52:06 AODV: theory AODV.B_Global_Invariants


06:52:07 AODV: theory AODV.B_Aodv_Loop_Freedom


06:52:10 AODV: theory AODV.All


08:00:59 Preparing AODV/document ...


08:01:16 Finished AODV/document (0:00:16 elapsed time)


08:01:16 Preparing AODV/outline ...


08:01:26 Finished AODV/outline (0:00:10 elapsed time)


08:01:29 Timing AODV (8 threads, 4188.597s elapsed time, 25408.089s cpu time, 993.239s GC time, factor 6.07)


08:01:29 Finished AODV (1:09:50 elapsed time, 7:03:31 cpu time, factor 6.06)


08:01:29 Building Word_Lib ...


08:01:30 Word_Lib: theory HOL-Library.Phantom_Type


08:01:30 Word_Lib: theory HOL-Library.Boolean_Algebra


08:01:30 Word_Lib: theory HOL-Library.Sublist


08:01:30 Word_Lib: theory HOL-Eisbach.Eisbach


08:01:30 Word_Lib: theory HOL-Library.Signed_Division


08:01:30 Word_Lib: theory Word_Lib.Even_More_List


08:01:30 Word_Lib: theory Word_Lib.Enumeration


08:01:30 Word_Lib: theory Word_Lib.More_Misc


08:01:31 Word_Lib: theory HOL-Library.Bit_Operations


08:01:31 Word_Lib: theory HOL-Library.Cardinality


08:01:32 Word_Lib: theory HOL-Eisbach.Eisbach_Tools


08:01:33 Word_Lib: theory Word_Lib.More_Sublist


08:01:33 Word_Lib: theory HOL-Library.Numeral_Type


08:01:34 Word_Lib: theory HOL-Library.Type_Length


08:01:36 Word_Lib: theory HOL-Library.Word


08:01:38 Word_Lib: theory Word_Lib.More_Arithmetic


08:01:44 Word_Lib: theory Word_Lib.Bit_Comprehension


08:01:44 Word_Lib: theory Word_Lib.Hex_Words


08:01:44 Word_Lib: theory Word_Lib.Legacy_Aliases


08:01:44 Word_Lib: theory Word_Lib.More_Divides


08:01:44 Word_Lib: theory Word_Lib.Signed_Words


08:01:44 Word_Lib: theory Word_Lib.Type_Syntax


08:01:44 Word_Lib: theory Word_Lib.Word_Syntax


08:01:44 Word_Lib: theory Word_Lib.Signed_Division_Word


08:01:44 Word_Lib: theory Word_Lib.Word_Names


08:01:44 Word_Lib: theory Word_Lib.More_Word


08:01:45 Word_Lib: theory Word_Lib.Enumeration_Word


08:01:45 Word_Lib: theory Word_Lib.Many_More


08:01:45 Word_Lib: theory Word_Lib.Strict_part_mono


08:01:45 Word_Lib: theory Word_Lib.Traditional_Infix_Syntax


08:01:45 Word_Lib: theory Word_Lib.Word_16


08:01:47 Word_Lib: theory Word_Lib.Bits_Int


08:01:47 Word_Lib: theory Word_Lib.Word_EqI


08:01:49 Word_Lib: theory Word_Lib.Least_significant_bit


08:01:49 Word_Lib: theory Word_Lib.Norm_Words


08:01:49 Word_Lib: theory Word_Lib.Rsplit


08:01:49 Word_Lib: theory Word_Lib.Most_significant_bit


08:01:49 Word_Lib: theory Word_Lib.Typedef_Morphisms


08:01:49 Word_Lib: theory Word_Lib.Generic_set_bit


08:01:50 Word_Lib: theory Word_Lib.Aligned


08:01:50 Word_Lib: theory Word_Lib.Next_and_Prev


08:01:50 Word_Lib: theory Word_Lib.Word_Lemmas


08:01:50 Word_Lib: theory Word_Lib.Reversed_Bit_Lists


08:01:53 Word_Lib: theory Word_Lib.Word_8


08:01:53 Word_Lib: theory Word_Lib.Ancient_Numeral


08:01:53 Word_Lib: theory Word_Lib.Bitwise


08:01:53 Word_Lib: theory Word_Lib.More_Word_Operations


08:01:53 Word_Lib: theory Word_Lib.Bitwise_Signed


08:01:53 Word_Lib: theory Word_Lib.Examples


08:01:54 Word_Lib: theory Word_Lib.Word_32


08:01:54 Word_Lib: theory Word_Lib.Word_64


08:01:55 Word_Lib: theory Word_Lib.Word_Lib_Sumo


08:01:58 Word_Lib: theory Word_Lib.Guide


08:02:42 Preparing Word_Lib/document ...


08:02:51 Finished Word_Lib/document (0:00:08 elapsed time)


08:02:51 Preparing Word_Lib/outline ...


08:02:57 Finished Word_Lib/outline (0:00:06 elapsed time)


08:02:58 Timing Word_Lib (8 threads, 48.145s elapsed time, 236.731s cpu time, 18.236s GC time, factor 4.92)


08:02:58 Finished Word_Lib (0:01:12 elapsed time, 0:04:45 cpu time, factor 3.96)


08:02:58 Building IP_Addresses ...


08:03:00 IP_Addresses: theory HOL-Library.Cancellation


08:03:00 IP_Addresses: theory HOL-Library.Infinite_Set


08:03:00 IP_Addresses: theory HOL-Library.Option_ord


08:03:00 IP_Addresses: theory IP_Addresses.NumberWang_IPv4


08:03:00 IP_Addresses: theory IP_Addresses.NumberWang_IPv6


08:03:01 IP_Addresses: theory HOL-Library.Multiset


08:03:06 IP_Addresses: theory HOL-ex.Quicksort


08:03:06 IP_Addresses: theory Automatic_Refinement.Misc


08:03:13 IP_Addresses: theory HOL-Library.Code_Abstract_Nat


08:03:13 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString


08:03:13 IP_Addresses: theory IP_Addresses.Hs_Compat


08:03:13 IP_Addresses: theory IP_Addresses.WordInterval


08:03:13 IP_Addresses: theory HOL-Library.Product_Lexorder


08:03:13 IP_Addresses: theory HOL-Library.Code_Target_Nat


08:03:13 IP_Addresses: theory IP_Addresses.Lib_List_toString


08:03:13 IP_Addresses: theory IP_Addresses.Lib_Word_toString


08:03:16 IP_Addresses: theory IP_Addresses.WordInterval_Sorted


08:03:17 IP_Addresses: theory IP_Addresses.IP_Address


08:03:22 IP_Addresses: theory IP_Addresses.Prefix_Match


08:03:22 IP_Addresses: theory IP_Addresses.IPv4


08:03:22 IP_Addresses: theory IP_Addresses.IPv6


08:03:23 IP_Addresses: theory IP_Addresses.CIDR_Split


08:04:22 IP_Addresses: theory IP_Addresses.IP_Address_Parser


08:04:22 IP_Addresses: theory IP_Addresses.IP_Address_toString


08:04:24 IP_Addresses: theory IP_Addresses.Prefix_Match_toString


08:06:51 Preparing IP_Addresses/document ...


08:06:56 Finished IP_Addresses/document (0:00:04 elapsed time)


08:06:56 Preparing IP_Addresses/outline ...


08:07:00 Finished IP_Addresses/outline (0:00:03 elapsed time)


08:07:01 Timing IP_Addresses (8 threads, 186.158s elapsed time, 626.276s cpu time, 46.065s GC time, factor 3.36)


08:07:01 Finished IP_Addresses (0:03:52 elapsed time, 0:11:57 cpu time, factor 3.09)


08:07:01 Building Simple_Firewall ...


08:07:03 Simple_Firewall: theory HOL-Library.Char_ord


08:07:03 Simple_Firewall: theory Simple_Firewall.GroupF


08:07:03 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString


08:07:03 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries


08:07:03 Simple_Firewall: theory Simple_Firewall.List_Product_More


08:07:03 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State


08:07:03 Simple_Firewall: theory Simple_Firewall.Option_Helpers


08:07:03 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString


08:07:03 Simple_Firewall: theory Simple_Firewall.Iface


08:07:03 Simple_Firewall: theory Simple_Firewall.L4_Protocol


08:07:06 Simple_Firewall: theory Simple_Firewall.Simple_Packet


08:07:06 Simple_Firewall: theory Simple_Firewall.Primitives_toString


08:07:09 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax


08:07:12 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics


08:07:12 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString


08:07:14 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw


08:07:14 Simple_Firewall: theory Simple_Firewall.Shadowed


08:07:14 Simple_Firewall: theory Simple_Firewall.Service_Matrix


08:07:42 Preparing Simple_Firewall/document ...


08:07:48 Finished Simple_Firewall/document (0:00:06 elapsed time)


08:07:48 Preparing Simple_Firewall/outline ...


08:07:54 Finished Simple_Firewall/outline (0:00:05 elapsed time)


08:07:55 Timing Simple_Firewall (8 threads, 17.156s elapsed time, 84.530s cpu time, 4.374s GC time, factor 4.93)


08:07:55 Finished Simple_Firewall (0:00:40 elapsed time, 0:02:10 cpu time, factor 3.22)


08:07:55 Building Routing ...


08:07:57 Routing: theory HOL-Library.Adhoc_Overloading


08:07:57 Routing: theory Routing.Linorder_Helper


08:07:57 Routing: theory HOL-Library.Monad_Syntax


08:07:58 Routing: theory Routing.Routing_Table


08:08:01 Routing: theory Routing.IpRoute_Parser


08:08:01 Routing: theory Routing.Linux_Router


08:08:23 Preparing Routing/document ...


08:08:26 Finished Routing/document (0:00:02 elapsed time)


08:08:26 Preparing Routing/outline ...


08:08:28 Finished Routing/outline (0:00:02 elapsed time)


08:08:29 Timing Routing (8 threads, 11.451s elapsed time, 29.354s cpu time, 1.156s GC time, factor 2.56)


08:08:29 Finished Routing (0:00:28 elapsed time, 0:00:59 cpu time, factor 2.13)


08:08:29 Building Iptables_Semantics ...


08:08:31 Iptables_Semantics: theory Iptables_Semantics.Negation_Type


08:08:31 Iptables_Semantics: theory Iptables_Semantics.List_Misc


08:08:32 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists


08:08:33 Iptables_Semantics: theory HOL-Library.Code_Target_Int


08:08:33 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF


08:08:33 Iptables_Semantics: theory HOL-Library.LaTeXsugar


08:08:33 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors


08:08:33 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev


08:08:33 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize


08:08:33 Iptables_Semantics: theory Iptables_Semantics.Ternary


08:08:33 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State


08:08:33 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags


08:08:33 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common


08:08:33 Iptables_Semantics: theory Native_Word.More_Bits_Int


08:08:33 Iptables_Semantics: theory Iptables_Semantics.Word_Upto


08:08:33 Iptables_Semantics: theory Iptables_Semantics.IpAddresses


08:08:34 Iptables_Semantics: theory Iptables_Semantics.Ports


08:08:35 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet


08:08:35 Iptables_Semantics: theory Native_Word.Code_Symbolic_Bits_Int


08:08:36 Iptables_Semantics: theory Native_Word.Bits_Integer


08:08:36 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax


08:08:47 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary


08:08:47 Iptables_Semantics: theory Iptables_Semantics.Semantics


08:08:47 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto


08:08:49 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics


08:08:49 Iptables_Semantics: theory Iptables_Semantics.Matching


08:08:49 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful


08:08:49 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update


08:08:50 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding


08:08:50 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary


08:08:50 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs


08:08:51 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings


08:08:52 Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int


08:08:52 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action


08:08:52 Iptables_Semantics: theory Iptables_Semantics.Optimizing


08:08:52 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic


08:08:53 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches


08:08:53 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching


08:08:55 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization


08:08:56 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher


08:08:58 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold


08:08:58 Iptables_Semantics: theory Iptables_Semantics.Ipassmt


08:09:00 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt


08:09:31 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas


08:09:31 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform


08:09:31 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics


08:09:31 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString


08:09:32 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize


08:09:32 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize


08:09:32 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize


08:09:32 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize


08:09:32 Iptables_Semantics: theory Iptables_Semantics.No_Spoof


08:09:37 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace


08:09:38 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace


08:09:40 Iptables_Semantics: theory Iptables_Semantics.Transform


08:09:44 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract


08:09:45 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance


08:09:49 Iptables_Semantics: theory Iptables_Semantics.Code_Interface


08:09:49 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings


08:09:49 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings


08:09:50 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics


08:09:50 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings


08:09:55 Iptables_Semantics: theory Iptables_Semantics.Parser


08:09:55 Iptables_Semantics: theory Iptables_Semantics.Parser6


08:09:55 Iptables_Semantics: theory Iptables_Semantics.Documentation


08:09:55 Iptables_Semantics: theory Iptables_Semantics.Code_haskell


08:11:06 Preparing Iptables_Semantics/document ...


08:11:23 Finished Iptables_Semantics/document (0:00:17 elapsed time)


08:11:23 Preparing Iptables_Semantics/outline ...


08:11:33 Finished Iptables_Semantics/outline (0:00:09 elapsed time)


08:11:35 Timing Iptables_Semantics (8 threads, 104.237s elapsed time, 518.077s cpu time, 47.953s GC time, factor 4.97)


08:11:35 Finished Iptables_Semantics (0:02:35 elapsed time, 0:10:22 cpu time, factor 4.01)


08:11:35 Building Iptables_Semantics_Examples ...


08:11:38 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall


08:11:38 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company


08:11:38 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example


08:11:38 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test


08:11:38 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing


08:11:38 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof


08:11:38 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test


08:11:38 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com


08:11:42 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail


08:11:42 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples


08:11:42 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed


08:11:43 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation


08:15:02 Preparing Iptables_Semantics_Examples/document ...


08:15:06 Finished Iptables_Semantics_Examples/document (0:00:04 elapsed time)


08:15:06 Preparing Iptables_Semantics_Examples/outline ...


08:15:10 Finished Iptables_Semantics_Examples/outline (0:00:04 elapsed time)


08:15:11 Timing Iptables_Semantics_Examples (8 threads, 182.374s elapsed time, 1333.049s cpu time, 126.106s GC time, factor 7.31)


08:15:11 Finished Iptables_Semantics_Examples (0:03:25 elapsed time, 0:22:59 cpu time, factor 6.70)


08:15:11 Running Iptables_Semantics_Examples_Big ...


08:15:14 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated


08:15:14 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern


08:15:14 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small


08:15:14 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3


08:15:14 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall


08:17:31 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large


08:49:54 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW


10:08:17 Preparing Iptables_Semantics_Examples_Big/document ...


10:08:21 Finished Iptables_Semantics_Examples_Big/document (0:00:03 elapsed time)


10:08:21 Preparing Iptables_Semantics_Examples_Big/outline ...


10:08:24 Finished Iptables_Semantics_Examples_Big/outline (0:00:03 elapsed time)


10:08:26 Timing Iptables_Semantics_Examples_Big (8 threads, 6778.219s elapsed time, 32246.149s cpu time, 14490.804s GC time, factor 4.76)


10:08:26 Finished Iptables_Semantics_Examples_Big (1:53:05 elapsed time, 8:57:37 cpu time, factor 4.75)


10:08:26 Building HOL-Library ...


10:08:28 HOL-Library: theory HOL-Library.AList


10:08:28 HOL-Library: theory HOL-Library.Adhoc_Overloading


10:08:28 HOL-Library: theory HOL-Library.BNF_Axiomatization


10:08:28 HOL-Library: theory HOL-Library.BNF_Corec


10:08:28 HOL-Library: theory HOL-Library.Boolean_Algebra


10:08:28 HOL-Library: theory HOL-Library.Case_Converter


10:08:28 HOL-Library: theory HOL-Library.Cancellation


10:08:28 HOL-Library: theory HOL-Library.Char_ord


10:08:28 HOL-Library: theory HOL-Library.Code_Abstract_Nat


10:08:28 HOL-Library: theory HOL-Library.Monad_Syntax


10:08:28 HOL-Library: theory HOL-Library.Code_Prolog


10:08:28 HOL-Library: theory HOL-Library.State_Monad


10:08:28 HOL-Library: theory HOL-Library.Code_Binary_Nat


10:08:28 HOL-Library: theory HOL-Library.Bit_Operations


10:08:29 HOL-Library: theory HOL-Library.Code_Target_Nat


10:08:29 HOL-Library: theory HOL-Library.Code_Lazy


10:08:29 HOL-Library: theory HOL-Library.Multiset


10:08:29 HOL-Library: theory HOL-Library.Simps_Case_Conv


10:08:29 HOL-Library: theory HOL-Library.Extended


10:08:30 HOL-Library: theory HOL-Library.Code_Target_Int


10:08:30 HOL-Library: theory HOL-Library.Code_Test


10:08:30 HOL-Library: theory HOL-Library.Code_Target_Numeral


10:08:31 HOL-Library: theory HOL-Library.Comparator


10:08:31 HOL-Library: theory HOL-Library.Conditional_Parametricity


10:08:31 HOL-Library: theory HOL-Library.DAList


10:08:31 HOL-Library: theory HOL-Library.Confluence


10:08:31 HOL-Library: theory HOL-Library.Datatype_Records


10:08:31 HOL-Library: theory HOL-Library.Confluent_Quotient


10:08:32 HOL-Library: theory HOL-Library.Dlist


10:08:32 HOL-Library: theory HOL-Library.Debug


10:08:32 HOL-Library: theory HOL-Library.Disjoint_Sets


10:08:32 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice


10:08:32 HOL-Library: theory HOL-Library.Fun_Lexorder


10:08:32 HOL-Library: theory HOL-Library.FuncSet


10:08:32 HOL-Library: theory HOL-Library.Function_Algebras


10:08:32 HOL-Library: theory HOL-Library.Groups_Big_Fun


10:08:32 HOL-Library: theory HOL-Library.IArray


10:08:32 HOL-Library: theory HOL-Library.Infinite_Set


10:08:32 HOL-Library: theory HOL-Library.Function_Division


10:08:33 HOL-Library: theory HOL-Library.LaTeXsugar


10:08:33 HOL-Library: theory HOL-Library.Lattice_Constructions


10:08:33 HOL-Library: theory HOL-Library.Lattice_Syntax


10:08:33 HOL-Library: theory HOL-Library.Combine_PER


10:08:33 HOL-Library: theory HOL-Library.Equipollence


10:08:33 HOL-Library: theory HOL-Library.Complete_Partial_Order2


10:08:33 HOL-Library: theory HOL-Library.Omega_Words_Fun


10:08:33 HOL-Library: theory HOL-Library.Ramsey


10:08:33 HOL-Library: theory HOL-Library.ListVector


10:08:34 HOL-Library: theory HOL-Library.List_Lenlexorder


10:08:34 HOL-Library: theory HOL-Library.List_Lexorder


10:08:34 HOL-Library: theory HOL-Library.Mapping


10:08:34 HOL-Library: theory HOL-Library.More_List


10:08:34 HOL-Library: theory HOL-Library.Nat_Bijection


10:08:34 HOL-Library: theory HOL-Library.Poly_Mapping


10:08:34 HOL-Library: theory HOL-Library.Stream


10:08:35 HOL-Library: theory HOL-Library.AList_Mapping


10:08:36 HOL-Library: theory HOL-Library.Old_Datatype


10:08:36 HOL-Library: theory HOL-Library.Old_Recdef


10:08:37 HOL-Library: theory HOL-Library.DAList_Multiset


10:08:40 HOL-Library: theory HOL-Library.Multiset_Order


10:08:40 HOL-Library: theory HOL-Library.Open_State_Syntax


10:08:40 HOL-Library: theory HOL-Library.Option_ord


10:08:40 HOL-Library: theory HOL-Library.Parallel


10:08:40 HOL-Library: theory HOL-Library.Pattern_Aliases


10:08:40 HOL-Library: theory HOL-Library.Perm


10:08:40 HOL-Library: theory HOL-Library.Phantom_Type


10:08:40 HOL-Library: theory HOL-Library.Power_By_Squaring


10:08:41 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs


10:08:41 HOL-Library: theory HOL-Library.Preorder


10:08:41 HOL-Library: theory HOL-Library.Product_Lexorder


10:08:41 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck


10:08:42 HOL-Library: theory HOL-Library.Product_Plus


10:08:42 HOL-Library: theory HOL-Library.Quotient_Syntax


10:08:42 HOL-Library: theory HOL-Library.Quotient_Option


10:08:42 HOL-Library: theory HOL-Library.Product_Order


10:08:42 HOL-Library: theory HOL-Library.Quotient_Product


10:08:42 HOL-Library: theory HOL-Library.Quotient_Set


10:08:42 HOL-Library: theory HOL-Library.Quotient_Sum


10:08:42 HOL-Library: theory HOL-Library.Cardinality


10:08:42 HOL-Library: theory HOL-Library.Quotient_Type


10:08:42 HOL-Library: theory HOL-Library.Quotient_List


10:08:42 HOL-Library: theory HOL-Library.RBT_Impl


10:08:42 HOL-Library: theory HOL-Library.Finite_Lattice


10:08:42 HOL-Library: theory HOL-Library.Realizers


10:08:42 HOL-Library: theory HOL-Library.Reflection


10:08:43 HOL-Library: theory HOL-Library.Refute


10:08:43 HOL-Library: theory HOL-Library.Rewrite


10:08:43 HOL-Library: theory HOL-Library.Set_Algebras


10:08:43 HOL-Library: theory HOL-Library.Signed_Division


10:08:43 HOL-Library: theory HOL-Library.Sorting_Algorithms


10:08:43 HOL-Library: theory HOL-Library.Sublist


10:08:43 HOL-Library: theory HOL-Library.Transitive_Closure_Table


10:08:44 HOL-Library: theory HOL-Library.Numeral_Type


10:08:45 HOL-Library: theory HOL-Library.Tree


10:08:45 HOL-Library: theory HOL-Library.Uprod


10:08:46 HOL-Library: theory HOL-Library.While_Combinator


10:08:46 HOL-Library: theory HOL-Library.Z2


10:08:46 HOL-Library: theory HOL-Library.Countable


10:08:47 HOL-Library: theory HOL-Library.BigO


10:08:47 HOL-Library: theory HOL-Library.Type_Length


10:08:47 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint


10:08:47 HOL-Library: theory HOL-Library.Prefix_Order


10:08:47 HOL-Library: theory HOL-Library.Subseq_Order


10:08:47 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float


10:08:47 HOL-Library: theory HOL-Library.Diagonal_Subsequence


10:08:47 HOL-Library: theory HOL-Library.Discrete


10:08:47 HOL-Library: theory HOL-Library.Saturated


10:08:47 HOL-Library: theory HOL-Library.Word


10:08:48 HOL-Library: theory HOL-Library.Going_To_Filter


10:08:48 HOL-Library: theory HOL-Library.Indicator_Function


10:08:48 HOL-Library: theory HOL-Library.Landau_Symbols


10:08:48 HOL-Library: theory HOL-Library.Lattice_Algebras


10:08:48 HOL-Library: theory HOL-Library.Countable_Set


10:08:48 HOL-Library: theory HOL-Library.FSet


10:08:48 HOL-Library: theory HOL-Library.Liminf_Limsup


10:08:48 HOL-Library: theory HOL-Library.Tree_Multiset


10:08:48 HOL-Library: theory HOL-Library.Countable_Complete_Lattices


10:08:49 HOL-Library: theory HOL-Library.Countable_Set_Type


10:08:49 HOL-Library: theory HOL-Library.Set_Idioms


10:08:49 HOL-Library: theory HOL-Library.Log_Nat


10:08:49 HOL-Library: theory HOL-Library.Lub_Glb


10:08:49 HOL-Library: theory HOL-Library.Nonpos_Ints


10:08:50 HOL-Library: theory HOL-Library.OptionalSugar


10:08:50 HOL-Library: theory HOL-Library.Periodic_Fun


10:08:50 HOL-Library: theory HOL-Library.Quadratic_Discriminant


10:08:50 HOL-Library: theory HOL-Library.Sum_of_Squares


10:08:50 HOL-Library: theory HOL-Library.Tree_Real


10:08:51 HOL-Library: theory HOL-Library.Order_Continuity


10:08:51 HOL-Library: theory HOL-Library.Finite_Map


10:08:51 HOL-Library: theory HOL-Library.Extended_Nat


10:08:51 HOL-Library: theory HOL-Library.Extended_Real


10:08:52 HOL-Library: theory HOL-Library.Interval


10:08:53 HOL-Library: theory HOL-Library.Float


10:08:55 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams


10:08:55 HOL-Library: theory HOL-Library.Interval_Float


10:08:56 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real


10:09:06 HOL-Library: theory HOL-Library.Disjoint_FSets


10:09:07 HOL-Library: theory HOL-Library.Library


10:09:29 HOL-Library: theory HOL-Library.RBT


10:09:29 HOL-Library: theory HOL-Library.RBT_Mapping


10:09:29 HOL-Library: theory HOL-Library.RBT_Set


10:11:30 Preparing HOL-Library/document ...


10:12:17 Finished HOL-Library/document (0:00:46 elapsed time)


10:12:17 Preparing HOL-Library/outline ...


10:12:46 Finished HOL-Library/outline (0:00:29 elapsed time)


10:12:48 Timing HOL-Library (8 threads, 118.159s elapsed time, 736.617s cpu time, 45.635s GC time, factor 6.23)


10:12:48 Finished HOL-Library (0:02:59 elapsed time, 0:14:24 cpu time, factor 4.81)


10:12:48 Building Category3 ...


10:12:51 Category3: theory HOL-Cardinals.Fun_More


10:12:51 Category3: theory HereditarilyFinite.HF


10:12:51 Category3: theory HOL-Cardinals.Order_Union


10:12:51 Category3: theory Category3.Category


10:12:51 Category3: theory HOL-Cardinals.Order_Relation_More


10:12:51 Category3: theory HOL-Cardinals.Wellorder_Extension


10:12:52 Category3: theory HOL-Cardinals.Wellfounded_More


10:12:52 Category3: theory HOL-Cardinals.Wellorder_Relation


10:12:52 Category3: theory Category3.ConcreteCategory


10:12:52 Category3: theory Category3.DiscreteCategory


10:12:52 Category3: theory Category3.DualCategory


10:12:52 Category3: theory Category3.EpiMonoIso


10:12:52 Category3: theory HOL-Cardinals.Wellorder_Embedding


10:12:52 Category3: theory HOL-Cardinals.Wellorder_Constructions


10:12:52 Category3: theory Category3.InitialTerminal


10:12:52 Category3: theory Category3.ProductCategory


10:12:53 Category3: theory HOL-Cardinals.Cardinal_Order_Relation


10:12:53 Category3: theory HOL-Cardinals.Ordinal_Arithmetic


10:12:54 Category3: theory Category3.FreeCategory


10:12:54 Category3: theory Category3.Functor


10:12:55 Category3: theory HOL-Cardinals.Cardinal_Arithmetic


10:12:55 Category3: theory HOL-Cardinals.Cardinals


10:12:58 Category3: theory Category3.NaturalTransformation


10:13:00 Category3: theory Category3.Subcategory


10:13:00 Category3: theory Category3.SetCategory


10:13:00 Category3: theory Category3.BinaryFunctor


10:13:03 Category3: theory Category3.SetCat


10:13:05 Category3: theory Category3.FunctorCategory


10:13:14 Category3: theory Category3.Yoneda


10:13:36 Category3: theory Category3.Adjunction


10:14:07 Category3: theory Category3.EquivalenceOfCategories


10:14:07 Category3: theory Category3.Limit


10:15:03 Category3: theory Category3.CartesianCategory


10:15:05 Category3: theory Category3.CategoryWithPullbacks


10:15:17 Category3: theory Category3.CartesianClosedCategory


10:15:17 Category3: theory Category3.CategoryWithFiniteLimits


10:15:18 Category3: theory Category3.HFSetCat


10:18:19 Preparing Category3/document ...


10:18:40 Finished Category3/document (0:00:20 elapsed time)


10:18:40 Preparing Category3/outline ...


10:18:48 Finished Category3/outline (0:00:08 elapsed time)


10:18:51 Timing Category3 (8 threads, 262.953s elapsed time, 1205.204s cpu time, 119.999s GC time, factor 4.58)


10:18:51 Finished Category3 (0:05:28 elapsed time, 0:22:19 cpu time, factor 4.08)


10:18:51 Building MonoidalCategory ...


10:18:54 MonoidalCategory: theory MonoidalCategory.MonoidalCategory


10:19:59 MonoidalCategory: theory MonoidalCategory.MonoidalFunctor


10:20:01 MonoidalCategory: theory MonoidalCategory.CartesianMonoidalCategory


10:20:24 MonoidalCategory: theory MonoidalCategory.FreeMonoidalCategory


10:25:13 Preparing MonoidalCategory/document ...


10:25:24 Finished MonoidalCategory/document (0:00:10 elapsed time)


10:25:24 Preparing MonoidalCategory/outline ...


10:25:29 Finished MonoidalCategory/outline (0:00:05 elapsed time)


10:25:31 Timing MonoidalCategory (8 threads, 318.636s elapsed time, 737.536s cpu time, 73.700s GC time, factor 2.31)


10:25:31 Finished MonoidalCategory (0:06:21 elapsed time, 0:14:21 cpu time, factor 2.26)


10:25:31 Running Bicategory ...


10:25:43 Bicategory: theory Bicategory.IsomorphismClass


10:25:44 Bicategory: theory Bicategory.Prebicategory


10:26:37 Bicategory: theory Bicategory.Bicategory


10:27:35 Bicategory: theory Bicategory.Coherence


10:27:38 Bicategory: theory Bicategory.InternalEquivalence


10:27:38 Bicategory: theory Bicategory.Subbicategory


10:30:00 Bicategory: theory Bicategory.CanonicalIsos


10:30:00 Bicategory: theory Bicategory.Pseudofunctor


10:33:51 Bicategory: theory Bicategory.Strictness


10:35:48 Bicategory: theory Bicategory.InternalAdjunction


10:39:07 Bicategory: theory Bicategory.PseudonaturalTransformation


10:39:07 Bicategory: theory Bicategory.Tabulation


10:39:07 Bicategory: theory Bicategory.SpanBicategory


10:46:12 Bicategory: theory Bicategory.EquivalenceOfBicategories


10:49:30 Bicategory: theory Bicategory.Modification


11:07:13 Bicategory: theory Bicategory.BicategoryOfSpans


11:28:25 Preparing Bicategory/document ...


11:29:47 Finished Bicategory/document (0:01:22 elapsed time)


11:29:47 Preparing Bicategory/outline ...


11:30:03 Finished Bicategory/outline (0:00:16 elapsed time)


11:30:05 Timing Bicategory (8 threads, 3763.266s elapsed time, 9886.358s cpu time, 1672.709s GC time, factor 2.63)


11:30:05 Finished Bicategory (1:02:48 elapsed time, 2:44:52 cpu time, factor 2.62)


11:30:05 Building ConcurrentIMP ...


11:30:07 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred


11:30:07 ConcurrentIMP: theory ConcurrentIMP.Infinite_Sequences


11:30:08 ConcurrentIMP: theory ConcurrentIMP.LTL


11:30:09 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang


11:30:14 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg


11:30:21 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg_rules


11:30:21 ConcurrentIMP: theory ConcurrentIMP.CIMP


11:30:22 ConcurrentIMP: theory ConcurrentIMP.CIMP_locales


11:30:22 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer


11:30:22 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer


11:30:49 Preparing ConcurrentIMP/document ...


11:30:53 Finished ConcurrentIMP/document (0:00:04 elapsed time)


11:30:53 Preparing ConcurrentIMP/outline ...


11:30:57 Finished ConcurrentIMP/outline (0:00:03 elapsed time)


11:30:58 Timing ConcurrentIMP (8 threads, 19.259s elapsed time, 65.613s cpu time, 5.411s GC time, factor 3.41)


11:30:58 Finished ConcurrentIMP (0:00:43 elapsed time, 0:01:53 cpu time, factor 2.60)


11:30:58 Running ConcurrentGC ...


11:31:00 ConcurrentGC: theory ConcurrentGC.Model


11:31:17 ConcurrentGC: theory ConcurrentGC.Proofs_Basis


11:31:27 ConcurrentGC: theory ConcurrentGC.Global_Invariants


11:31:27 ConcurrentGC: theory ConcurrentGC.Local_Invariants


11:31:27 ConcurrentGC: theory ConcurrentGC.Tactics


11:31:28 ConcurrentGC: theory ConcurrentGC.Concrete_heap


11:31:28 ConcurrentGC: theory ConcurrentGC.Global_Invariants_Lemmas


11:31:29 ConcurrentGC: theory ConcurrentGC.Concrete


11:31:31 ConcurrentGC: theory ConcurrentGC.Global_Noninterference


11:32:56 ConcurrentGC: theory ConcurrentGC.Local_Invariants_Lemmas


11:32:56 ConcurrentGC: theory ConcurrentGC.Initial_Conditions


11:32:56 ConcurrentGC: theory ConcurrentGC.MarkObject


11:32:57 ConcurrentGC: theory ConcurrentGC.Noninterference


11:32:57 ConcurrentGC: theory ConcurrentGC.Phases


11:32:57 ConcurrentGC: theory ConcurrentGC.StrongTricolour


11:32:57 ConcurrentGC: theory ConcurrentGC.TSO


11:32:57 ConcurrentGC: theory ConcurrentGC.Valid_Refs


11:32:58 ConcurrentGC: theory ConcurrentGC.Worklists


11:32:59 ConcurrentGC: theory ConcurrentGC.Proofs


11:46:41 Preparing ConcurrentGC/document ...


11:46:49 Finished ConcurrentGC/document (0:00:08 elapsed time)


11:46:49 Preparing ConcurrentGC/outline ...


11:46:55 Finished ConcurrentGC/outline (0:00:06 elapsed time)


11:46:56 Timing ConcurrentGC (8 threads, 938.877s elapsed time, 5263.263s cpu time, 284.500s GC time, factor 5.61)


11:46:56 Finished ConcurrentGC (0:15:41 elapsed time, 1:27:46 cpu time, factor 5.59)


11:46:56 Presentation in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info"


11:46:56 Presenting AODV ...


11:46:56 Presenting document AODV/document


11:46:56 Presenting document AODV/outline


11:46:56 Presenting theory AODV.Aodv_Basic


11:46:56 Presenting theory AODV.Aodv_Data


11:46:56 Presenting theory AODV.Aodv


11:46:56 Presenting theory AODV.Aodv_Message


11:46:56 Presenting theory AODV.Aodv_Predicates


11:46:56 Presenting theory AODV.Seq_Invariants


11:46:56 Presenting theory AODV.Quality_Increases


11:46:56 Presenting theory AODV.Fresher


11:46:56 Presenting theory AODV.OAodv


11:46:56 Presenting theory AODV.Global_Invariants


11:46:56 Presenting theory AODV.Loop_Freedom


11:46:56 Presenting theory AODV.Aodv_Loop_Freedom


11:46:56 Presenting theory AODV.A_Norreqid


11:46:56 Presenting theory AODV.A_Aodv_Data


11:46:57 Presenting theory AODV.A_Aodv_Message


11:46:57 Presenting theory AODV.A_Aodv


11:46:58 Presenting theory AODV.A_Aodv_Predicates


11:46:58 Presenting theory AODV.A_Fresher


11:46:58 Presenting theory AODV.A_Seq_Invariants


11:46:58 Presenting theory AODV.A_Quality_Increases


11:47:00 Presenting theory AODV.A_OAodv


11:47:00 Presenting theory AODV.A_Global_Invariants


11:47:00 Presenting theory AODV.A_Loop_Freedom


11:47:00 Presenting theory AODV.A_Aodv_Loop_Freedom


11:47:01 Presenting theory AODV.B_Fwdrreps


11:47:01 Presenting theory AODV.B_Aodv_Data


11:47:01 Presenting theory AODV.B_Aodv_Message


11:47:01 Presenting theory AODV.B_Aodv


11:47:01 Presenting theory AODV.B_Aodv_Predicates


11:47:02 Presenting theory AODV.B_Fresher


11:47:02 Presenting theory AODV.B_Seq_Invariants


11:47:02 Presenting theory AODV.B_Quality_Increases


11:47:03 Presenting theory AODV.B_OAodv


11:47:03 Presenting theory AODV.B_Global_Invariants


11:47:03 Presenting theory AODV.B_Loop_Freedom


11:47:03 Presenting theory AODV.B_Aodv_Loop_Freedom


11:47:03 Presenting theory AODV.C_Gtobcast


11:47:03 Presenting theory AODV.C_Aodv_Data


11:47:04 Presenting theory AODV.C_Aodv_Message


11:47:04 Presenting theory AODV.C_Aodv


11:47:05 Presenting theory AODV.C_Aodv_Predicates


11:47:05 Presenting theory AODV.C_Fresher


11:47:05 Presenting theory AODV.C_Seq_Invariants


11:47:05 Presenting theory AODV.C_Quality_Increases


11:47:05 Presenting theory AODV.C_OAodv


11:47:05 Presenting theory AODV.C_Global_Invariants


11:47:05 Presenting theory AODV.C_Loop_Freedom


11:47:06 Presenting theory AODV.C_Aodv_Loop_Freedom


11:47:06 Presenting theory AODV.D_Fwdrreqs


11:47:06 Presenting theory AODV.D_Aodv_Data


11:47:07 Presenting theory AODV.D_Aodv_Message


11:47:07 Presenting theory AODV.D_Aodv


11:47:07 Presenting theory AODV.D_Aodv_Predicates


11:47:07 Presenting theory AODV.D_Fresher


11:47:07 Presenting theory AODV.D_Seq_Invariants


11:47:08 Presenting theory AODV.D_Quality_Increases


11:47:08 Presenting theory AODV.D_OAodv


11:47:08 Presenting theory AODV.D_Global_Invariants


11:47:08 Presenting theory AODV.D_Loop_Freedom


11:47:08 Presenting theory AODV.D_Aodv_Loop_Freedom


11:47:08 Presenting theory AODV.E_All_ABCD


11:47:08 Presenting theory AODV.E_Aodv_Data


11:47:09 Presenting theory AODV.E_Aodv_Message


11:47:09 Presenting theory AODV.E_Aodv


11:47:09 Presenting theory AODV.E_Aodv_Predicates


11:47:09 Presenting theory AODV.E_Fresher


11:47:10 Presenting theory AODV.E_Seq_Invariants


11:47:10 Presenting theory AODV.E_Quality_Increases


11:47:10 Presenting theory AODV.E_OAodv


11:47:10 Presenting theory AODV.E_Global_Invariants


11:47:10 Presenting theory AODV.E_Loop_Freedom


11:47:10 Presenting theory AODV.E_Aodv_Loop_Freedom


11:47:11 Presenting theory AODV.All


11:47:12 Presenting Flyspeck-Tame-Computation ...


11:47:12 Presenting theory Flyspeck-Tame-Computation.ArchComp


11:47:12 Presenting theory Flyspeck-Tame-Computation.Completeness


11:47:12 Presenting Bicategory ...


11:47:12 Presenting document Bicategory/document


11:47:12 Presenting document Bicategory/outline


11:47:12 Presenting theory Bicategory.IsomorphismClass


11:47:12 Presenting theory Bicategory.Bicategory


11:47:12 Presenting theory Bicategory.Prebicategory


11:47:12 Presenting theory Bicategory.Coherence


11:47:12 Presenting theory Bicategory.CanonicalIsos


11:47:12 Presenting theory Bicategory.Subbicategory


11:47:12 Presenting theory Bicategory.InternalEquivalence


11:47:12 Presenting theory Bicategory.Pseudofunctor


11:47:12 Presenting theory Bicategory.Strictness


11:47:13 Presenting theory Bicategory.InternalAdjunction


11:47:14 Presenting theory Bicategory.PseudonaturalTransformation


11:47:14 Presenting theory Bicategory.EquivalenceOfBicategories


11:47:17 Presenting theory Bicategory.SpanBicategory


11:47:19 Presenting theory Bicategory.Tabulation


11:47:22 Presenting theory Bicategory.BicategoryOfSpans


11:47:24 Presenting theory Bicategory.Modification


11:47:38 Presenting ConcurrentGC ...


11:47:38 Presenting document ConcurrentGC/document


11:47:38 Presenting document ConcurrentGC/outline


11:47:38 Presenting theory ConcurrentGC.Model


11:47:38 Presenting theory ConcurrentGC.Proofs_Basis


11:47:38 Presenting theory ConcurrentGC.Local_Invariants


11:47:38 Presenting theory ConcurrentGC.Global_Invariants


11:47:38 Presenting theory ConcurrentGC.Tactics


11:47:38 Presenting theory ConcurrentGC.Global_Invariants_Lemmas


11:47:38 Presenting theory ConcurrentGC.Local_Invariants_Lemmas


11:47:38 Presenting theory ConcurrentGC.Initial_Conditions


11:47:38 Presenting theory ConcurrentGC.Noninterference


11:47:38 Presenting theory ConcurrentGC.Global_Noninterference


11:47:38 Presenting theory ConcurrentGC.MarkObject


11:47:38 Presenting theory ConcurrentGC.Phases


11:47:39 Presenting theory ConcurrentGC.StrongTricolour


11:47:39 Presenting theory ConcurrentGC.TSO


11:47:39 Presenting theory ConcurrentGC.Valid_Refs


11:47:39 Presenting theory ConcurrentGC.Worklists


11:47:40 Presenting theory ConcurrentGC.Proofs


11:47:40 Presenting theory ConcurrentGC.Concrete_heap


11:47:40 Presenting theory ConcurrentGC.Concrete


11:47:40 Presenting JinjaThreads ...


11:47:41 Presenting document JinjaThreads/document


11:47:41 Presenting document JinjaThreads/outline


11:47:41 Presenting theory JinjaThreads.Set_without_equal


11:47:41 Presenting theory JinjaThreads.JT_ICF


11:47:41 Presenting theory JinjaThreads.Set_Monad


11:47:41 Presenting theory JinjaThreads.Auxiliary


11:47:41 Presenting theory JinjaThreads.Basic_Main


11:47:41 Presenting theory JinjaThreads.FWState


11:47:41 Presenting theory JinjaThreads.FWLock


11:47:41 Presenting theory JinjaThreads.FWLocking


11:47:41 Presenting theory JinjaThreads.FWThread


11:47:41 Presenting theory JinjaThreads.FWWait


11:47:41 Presenting theory JinjaThreads.FWCondAction


11:47:41 Presenting theory JinjaThreads.FWWellform


11:47:41 Presenting theory JinjaThreads.FWLockingThread


11:47:41 Presenting theory JinjaThreads.FWInterrupt


11:47:41 Presenting theory JinjaThreads.FWSemantics


11:47:41 Presenting theory JinjaThreads.FWProgressAux


11:47:41 Presenting theory JinjaThreads.FWDeadlock


11:47:41 Presenting theory JinjaThreads.FWProgress


11:47:41 Presenting theory JinjaThreads.FWLifting


11:47:42 Presenting theory JinjaThreads.LTS


11:47:42 Presenting theory JinjaThreads.FWLTS


11:47:43 Presenting theory JinjaThreads.Bisimulation


11:47:43 Presenting theory JinjaThreads.FWBisimulation


11:47:43 Presenting theory JinjaThreads.FWBisimDeadlock


11:47:43 Presenting theory JinjaThreads.FWLiftingSem


11:47:43 Presenting theory JinjaThreads.FWInitFinLift


11:47:44 Presenting theory JinjaThreads.FWBisimLift


11:47:45 Presenting theory JinjaThreads.Semilat


11:47:46 Presenting theory JinjaThreads.Err


11:47:46 Presenting theory JinjaThreads.Opt


11:47:46 Presenting theory JinjaThreads.Product


11:47:46 Presenting theory JinjaThreads.Listn


11:47:46 Presenting theory JinjaThreads.Semilattices


11:47:46 Presenting theory JinjaThreads.Typing_Framework


11:47:47 Presenting theory JinjaThreads.SemilatAlg


11:47:47 Presenting theory JinjaThreads.Typing_Framework_err


11:47:47 Presenting theory JinjaThreads.Kildall


11:47:47 Presenting theory JinjaThreads.LBVSpec


11:47:47 Presenting theory JinjaThreads.LBVCorrect


11:47:47 Presenting theory JinjaThreads.LBVComplete


11:47:47 Presenting theory JinjaThreads.Abstract_BV


11:47:47 Presenting theory JinjaThreads.Type


11:47:47 Presenting theory JinjaThreads.Decl


11:47:47 Presenting theory JinjaThreads.TypeRel


11:47:48 Presenting theory JinjaThreads.Value


11:47:48 Presenting theory JinjaThreads.Exceptions


11:47:48 Presenting theory JinjaThreads.SystemClasses


11:47:48 Presenting theory JinjaThreads.Heap


11:47:48 Presenting theory JinjaThreads.Observable_Events


11:47:48 Presenting theory JinjaThreads.StartConfig


11:47:48 Presenting theory JinjaThreads.Conform


11:47:48 Presenting theory JinjaThreads.ExternalCall


11:47:48 Presenting theory JinjaThreads.WellForm


11:47:49 Presenting theory JinjaThreads.ExternalCallWF


11:47:49 Presenting theory JinjaThreads.ConformThreaded


11:47:49 Presenting theory JinjaThreads.BinOp


11:47:49 Presenting theory JinjaThreads.SemiType


11:47:49 Presenting theory JinjaThreads.Common_Main


11:47:49 Presenting theory JinjaThreads.State


11:47:49 Presenting theory JinjaThreads.Expr


11:47:49 Presenting theory JinjaThreads.JHeap


11:47:49 Presenting theory JinjaThreads.SmallStep


11:47:49 Presenting theory JinjaThreads.WWellForm


11:47:49 Presenting theory JinjaThreads.WellType


11:47:50 Presenting theory JinjaThreads.DefAss


11:47:50 Presenting theory JinjaThreads.JWellForm


11:47:50 Presenting theory JinjaThreads.Threaded


11:47:51 Presenting theory JinjaThreads.WellTypeRT


11:47:51 Presenting theory JinjaThreads.Progress


11:47:51 Presenting theory JinjaThreads.DefAssPreservation


11:47:51 Presenting theory JinjaThreads.TypeSafe


11:47:51 Presenting theory JinjaThreads.ProgressThreaded


11:47:51 Presenting theory JinjaThreads.Deadlocked


11:47:52 Presenting theory JinjaThreads.Annotate


11:47:52 Presenting theory JinjaThreads.J_Main


11:47:52 Presenting theory JinjaThreads.JVMState


11:47:52 Presenting theory JinjaThreads.JVMInstructions


11:47:52 Presenting theory JinjaThreads.JVMHeap


11:47:53 Presenting theory JinjaThreads.JVMExecInstr


11:47:53 Presenting theory JinjaThreads.JVMExceptions


11:47:53 Presenting theory JinjaThreads.JVMExec


11:47:53 Presenting theory JinjaThreads.JVMDefensive


11:47:53 Presenting theory JinjaThreads.JVMThreaded


11:47:54 Presenting theory JinjaThreads.JVM_Main


11:47:54 Presenting theory JinjaThreads.JVM_SemiType


11:47:54 Presenting theory JinjaThreads.Effect


11:47:54 Presenting theory JinjaThreads.BVSpec


11:47:54 Presenting theory JinjaThreads.BVConform


11:47:54 Presenting theory JinjaThreads.BVSpecTypeSafe


11:47:55 Presenting theory JinjaThreads.BVNoTypeError


11:47:55 Presenting theory JinjaThreads.BVProgressThreaded


11:47:55 Presenting theory JinjaThreads.JVMDeadlocked


11:47:55 Presenting theory JinjaThreads.EffectMono


11:47:55 Presenting theory JinjaThreads.TF_JVM


11:47:55 Presenting theory JinjaThreads.LBVJVM


11:47:55 Presenting theory JinjaThreads.BVExec


11:47:56 Presenting theory JinjaThreads.BCVExec


11:47:56 Presenting theory JinjaThreads.BV_Main


11:47:56 Presenting theory JinjaThreads.CallExpr


11:47:56 Presenting theory JinjaThreads.J0


11:47:56 Presenting theory JinjaThreads.J0Bisim


11:47:56 Presenting theory JinjaThreads.J1State


11:47:57 Presenting theory JinjaThreads.J1Heap


11:47:57 Presenting theory JinjaThreads.J1


11:47:57 Presenting theory JinjaThreads.J1Deadlock


11:47:57 Presenting theory JinjaThreads.PCompiler


11:47:58 Presenting theory JinjaThreads.Compiler2


11:47:58 Presenting theory JinjaThreads.Exception_Tables


11:47:59 Presenting theory JinjaThreads.J1WellType


11:47:59 Presenting theory JinjaThreads.J1WellForm


11:47:59 Presenting theory JinjaThreads.TypeComp


11:47:59 Presenting theory JinjaThreads.JVMTau


11:47:59 Presenting theory JinjaThreads.Execs


11:48:00 Presenting theory JinjaThreads.J1JVMBisim


11:48:00 Presenting theory JinjaThreads.J1JVM


11:48:02 Presenting theory JinjaThreads.JVMJ1


11:48:02 Presenting theory JinjaThreads.Correctness2


11:48:02 Presenting theory JinjaThreads.ListIndex


11:48:03 Presenting theory JinjaThreads.Compiler1


11:48:03 Presenting theory JinjaThreads.J0J1Bisim


11:48:03 Presenting theory JinjaThreads.Correctness1Threaded


11:48:03 Presenting theory JinjaThreads.Correctness1


11:48:06 Presenting theory JinjaThreads.JJ1WellForm


11:48:06 Presenting theory JinjaThreads.Compiler


11:48:06 Presenting theory JinjaThreads.Correctness


11:48:07 Presenting theory JinjaThreads.Preprocessor


11:48:07 Presenting theory JinjaThreads.Compiler_Main


11:48:07 Presenting theory JinjaThreads.MM


11:48:07 Presenting theory JinjaThreads.SC


11:48:08 Presenting theory JinjaThreads.SC_Interp


11:48:08 Presenting theory JinjaThreads.SC_Collections


11:48:09 Presenting theory JinjaThreads.Orders


11:48:09 Presenting theory JinjaThreads.JMM_Spec


11:48:11 Presenting theory JinjaThreads.JMM_DRF


11:48:11 Presenting theory JinjaThreads.SC_Legal


11:48:13 Presenting theory JinjaThreads.Non_Speculative


11:48:13 Presenting theory JinjaThreads.SC_Completion


11:48:15 Presenting theory JinjaThreads.HB_Completion


11:48:17 Presenting theory JinjaThreads.JMM_Heap


11:48:18 Presenting theory JinjaThreads.JMM_Framework


11:48:18 Presenting theory JinjaThreads.JMM_Typesafe


11:48:23 Presenting theory JinjaThreads.JMM_Common


11:48:24 Presenting theory JinjaThreads.JMM_J


11:48:24 Presenting theory JinjaThreads.DRF_J


11:48:25 Presenting theory JinjaThreads.JMM_JVM


11:48:26 Presenting theory JinjaThreads.DRF_JVM


11:48:26 Presenting theory JinjaThreads.JMM_Type


11:48:27 Presenting theory JinjaThreads.JMM_Compiler


11:48:27 Presenting theory JinjaThreads.JMM_Type2


11:48:28 Presenting theory JinjaThreads.JMM_Interp


11:48:29 Presenting theory JinjaThreads.JMM_Typesafe2


11:48:29 Presenting theory JinjaThreads.JMM_J_Typesafe


11:48:30 Presenting theory JinjaThreads.JMM_JVM_Typesafe


11:48:30 Presenting theory JinjaThreads.JMM_Compiler_Type2


11:48:31 Presenting theory JinjaThreads.JMM


11:48:31 Presenting theory JinjaThreads.MM_Main


11:48:31 Presenting theory JinjaThreads.State_Refinement


11:48:31 Presenting theory JinjaThreads.Scheduler


11:48:31 Presenting theory JinjaThreads.Random_Scheduler


11:48:31 Presenting theory JinjaThreads.Round_Robin


11:48:32 Presenting theory JinjaThreads.SC_Schedulers


11:48:33 Presenting theory JinjaThreads.TypeRelRefine


11:48:33 Presenting theory JinjaThreads.PCompilerRefine


11:48:33 Presenting theory JinjaThreads.J_Execute


11:48:34 Presenting theory JinjaThreads.ExternalCall_Execute


11:48:34 Presenting theory JinjaThreads.JVMExec_Execute2


11:48:34 Presenting theory JinjaThreads.JVM_Execute2


11:48:35 Presenting theory JinjaThreads.Code_Generation


11:48:36 Presenting theory JinjaThreads.JVMExec_Execute


11:48:37 Presenting theory JinjaThreads.JVM_Execute


11:48:37 Presenting theory JinjaThreads.ToString


11:48:38 Presenting theory JinjaThreads.Java2Jinja


11:48:38 Presenting theory JinjaThreads.Execute_Main


11:48:38 Presenting theory JinjaThreads.ApprenticeChallenge


11:48:38 Presenting theory JinjaThreads.BufferExample


11:48:38 Presenting theory JinjaThreads.Examples_Main


11:48:38 Presenting theory JinjaThreads.JinjaThreads


11:48:42 Presenting Iptables_Semantics_Examples_Big ...


11:48:42 Presenting document Iptables_Semantics_Examples_Big/document


11:48:42 Presenting document Iptables_Semantics_Examples_Big/outline


11:48:42 Presenting theory Iptables_Semantics_Examples_Big.Analyze_topos_generated


11:48:42 Presenting theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small


11:48:42 Presenting theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall


11:48:42 Presenting theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3


11:48:42 Presenting theory Iptables_Semantics_Examples_Big.TUM_Simple_FW


11:48:42 Presenting theory Iptables_Semantics_Examples_Big.Analyze_Containern


11:48:42 Presenting theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large


11:48:44 

11:48:44 === TIMING ===


11:48:44 

11:48:44 Group slow: 9:24:04 elapsed time, 30:17:01 cpu time, factor 3.22


11:48:44 Group AFP: 9:51:27 elapsed time, 31:58:59 cpu time, factor 3.24


11:48:44 Group main: 0:07:53 elapsed time, 0:29:26 cpu time, factor 3.73


11:48:44 Group timing: 0:02:59 elapsed time, 0:14:24 cpu time, factor 4.81


11:48:44 Group very_slow: 6:09:07 elapsed time, 15:21:23 cpu time, factor 2.50


11:48:44 Overall: 10:13:41 elapsed time, 32:28:50 cpu time, factor 3.18


11:48:46 Archiving artifacts


11:48:55 Started calculate disk usage of build


11:48:55 Finished Calculation of disk usage of build in 0 seconds


11:48:55 Started calculate disk usage of workspace


11:48:56 Finished Calculation of disk usage of workspace in 0 seconds


11:48:56 No emails were triggered.


11:48:56 Finished: SUCCESS