Skip to content
[Jenkins]Jenkins
log in
Success

Console Output

01:33:11 Started by an SCM change


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 no changes found


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


01:33:11 0 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 a7aba6db79a143c5a47e0cfadc01c50e155f6403 --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><added>{file_adds|stringify|xmlescape}</added><deleted>{file_dels|stringify|xmlescape}</deleted><files>{files|stringify|xmlescape}</files><parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(a7aba6db79a143c5a47e0cfadc01c50e155f6403)" --encoding UTF-8 --encodingmode replace


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


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


01:33:14 pulling from https://bitbucket.org/isa-afp/afp-devel/


01:33:14 no changes found


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


01:33:14 1 files updated, 0 files merged, 0 files removed, 0 files unresolved


01:33:14 [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 e9a7b2a763bc9a025c90ece24b2ddbb96432bd31 --template exists\n


01:33:15 exists


01:33:15 [afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg><added>{file_adds|stringify|xmlescape}</added><deleted>{file_dels|stringify|xmlescape}</deleted><files>{files|stringify|xmlescape}</files><parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(e9a7b2a763bc9a025c90ece24b2ddbb96432bd31)" --encoding UTF-8 --encodingmode replace


01:33:15 No emails were triggered.


01:33:15 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins4368952908787063127.sh


01:33:15 + Admin/jenkins/run_build slow


01:33:15 + set -e


01:33:15 + PROFILE=slow


01:33:15 + shift


01:33:15 + bin/isabelle components -a


01:33:15 + bin/isabelle jedit -bf


01:33:15 ### Building graph browser ...


01:33:15 warning: [options] bootstrap class path not set in conjunction with -source 6


01:33:15 warning: [options] source value 6 is obsolete and will be removed in a future release


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


01:33:17 Note: Some input files use or override a deprecated API.


01:33:17 Note: Recompile with -Xlint:deprecation for details.


01:33:17 Note: Some input files use unchecked or unsafe operations.


01:33:17 Note: Recompile with -Xlint:unchecked for details.


01:33:17 3 warnings


01:33:17 ### Building Isabelle/Scala ...


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


01:35:02 + bin/isabelle ocaml_setup


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


01:35:03 [NOTE] It seems you have not updated your repositories for a while. Consider updating them with:


01:35:03        opam update


01:35:03 

01:35:03 [NOTE] Package zarith is already installed (current version is 1.7).


01:35:04 + bin/isabelle ghc_setup


01:35:04 stack will use a sandboxed GHC it installed


01:35:04 For more information on paths, see 'stack path' and 'stack exec env'


01:35:04 To use this GHC and packages outside of a project, consider using:


01:35:04 stack ghc, stack ghci, stack runghc, or stack exec


01:35:05 The Glorious Glasgow Haskell Compilation System, version 8.4.4


01:35:05 + bin/isabelle ci_build_slow


01:35:12 

01:35:12 === CONFIGURATION ===


01:35:12 

01:35:12 ISABELLE_BUILD_OPTIONS=""


01:35:12 

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


01:35:12 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64-linux"


01:35:12 ML_SYSTEM="polyml-5.8"


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


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


01:35:13 

01:35:13 === BUILD ===


01:35:13 

01:35:13 Build started at Sat, 20 Apr 2019 01:35:12 +0200


01:35:13 Isabelle id a7aba6db79a1


01:35:13 Build for AFP id 69945e1330db


01:35:13 

01:35:13 === LOG ===


01:35:13 

01:35:15 Session Pure/Pure


01:35:16 Session FOL/FOL


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


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


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


01:35:19 Session HOL/HOL-Eisbach


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


01:35:24 Session HOL/HOL-Word (main timing)


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


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


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


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


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


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


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


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


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


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


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


01:35:31 Building Pure ...


01:36:01 Pure: theory Pure


01:36:02 Pure: theory ML_Bootstrap


01:36:03 Pure: theory Pure.Sessions


01:36:06 Timing Pure (1 threads, 1.665s elapsed time, 1.664s cpu time, 0.000s GC time, factor 1.00)


01:36:06 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure


01:36:06 Finished Pure (0:00:33 elapsed time, 0:00:32 cpu time, factor 1.00)


01:36:06 Building HOL ...


01:36:10 HOL: theory HOL.Code_Generator


01:36:16 HOL: theory HOL.HOL


01:36:22 HOL: theory HOL.Argo


01:36:22 HOL: theory HOL.Ctr_Sugar


01:36:22 HOL: theory HOL.Orderings


01:36:25 HOL: theory HOL.Groups


01:36:25 HOL: theory HOL.SAT


01:36:28 HOL: theory HOL.Lattices


01:36:31 HOL: theory HOL.Set


01:36:33 HOL: theory HOL.Fun


01:36:33 HOL: theory HOL.Typedef


01:36:34 HOL: theory HOL.Complete_Lattices


01:36:34 HOL: theory HOL.Rings


01:36:37 HOL: theory HOL.Inductive


01:36:40 HOL: theory HOL.Product_Type


01:36:40 HOL: theory HOL.Sum_Type


01:36:43 HOL: theory HOL.Complete_Partial_Order


01:36:48 HOL: theory HOL.Nat


01:36:51 HOL: theory HOL.Fields


01:36:51 HOL: theory HOL.Meson


01:36:52 HOL: theory HOL.ATP


01:36:57 HOL: theory HOL.Metis


01:36:58 HOL: theory HOL.Finite_Set


01:37:01 HOL: theory HOL.Relation


01:37:03 HOL: theory HOL.Transitive_Closure


01:37:05 HOL: theory HOL.Wellfounded


01:37:06 HOL: theory HOL.Fun_Def_Base


01:37:06 HOL: theory HOL.Hilbert_Choice


01:37:06 HOL: theory HOL.Wfrec


01:37:07 HOL: theory HOL.Order_Relation


01:37:07 HOL: theory HOL.BNF_Wellorder_Relation


01:37:09 HOL: theory HOL.BNF_Wellorder_Embedding


01:37:09 HOL: theory HOL.Zorn


01:37:09 HOL: theory HOL.BNF_Wellorder_Constructions


01:37:10 HOL: theory HOL.BNF_Cardinal_Order_Relation


01:37:12 HOL: theory HOL.BNF_Cardinal_Arithmetic


01:37:13 HOL: theory HOL.BNF_Def


01:37:17 HOL: theory HOL.Basic_BNFs


01:37:17 HOL: theory HOL.BNF_Composition


01:37:19 HOL: theory HOL.BNF_Fixpoint_Base


01:37:24 HOL: theory HOL.BNF_Least_Fixpoint


01:37:29 HOL: theory HOL.Basic_BNF_LFPs


01:37:30 HOL: theory HOL.Transfer


01:37:31 HOL: theory HOL.Num


01:37:35 HOL: theory HOL.Power


01:37:39 HOL: theory HOL.Groups_Big


01:37:43 HOL: theory HOL.Equiv_Relations


01:37:43 HOL: theory HOL.Lifting


01:37:46 HOL: theory HOL.Lifting_Set


01:37:46 HOL: theory HOL.Option


01:37:46 HOL: theory HOL.Quotient


01:37:47 HOL: theory HOL.Extraction


01:37:47 HOL: theory HOL.Partial_Function


01:37:47 HOL: theory HOL.Lattices_Big


01:37:49 HOL: theory HOL.Fun_Def


01:37:52 HOL: theory HOL.Int


01:37:57 HOL: theory HOL.Euclidean_Division


01:38:06 HOL: theory HOL.Parity


01:38:11 HOL: theory HOL.Divides


01:38:14 HOL: theory HOL.Code_Numeral


01:38:14 HOL: theory HOL.Set_Interval


01:38:14 HOL: theory HOL.SMT


01:38:14 HOL: theory HOL.Numeral_Simprocs


01:38:18 HOL: theory HOL.Semiring_Normalization


01:38:23 HOL: theory HOL.Groebner_Basis


01:38:24 HOL: theory HOL.Conditionally_Complete_Lattices


01:38:24 HOL: theory HOL.Filter


01:38:25 HOL: theory HOL.Presburger


01:38:33 HOL: theory HOL.Sledgehammer


01:38:38 HOL: theory HOL.List


01:38:54 HOL: theory HOL.Groups_List


01:38:54 HOL: theory HOL.Map


01:38:56 HOL: theory HOL.Factorial


01:38:56 HOL: theory HOL.GCD


01:38:56 HOL: theory HOL.Enum


01:38:56 HOL: theory HOL.Random


01:38:58 HOL: theory HOL.Binomial


01:39:05 HOL: theory HOL.String


01:39:08 HOL: theory HOL.BNF_Greatest_Fixpoint


01:39:09 HOL: theory HOL.Predicate


01:39:09 HOL: theory HOL.Typerep


01:39:12 HOL: theory HOL.Lazy_Sequence


01:39:14 HOL: theory HOL.Limited_Sequence


01:39:15 HOL: theory HOL.Code_Evaluation


01:39:19 HOL: theory HOL.Quickcheck_Random


01:39:27 HOL: theory HOL.Quickcheck_Exhaustive


01:39:27 HOL: theory HOL.Quickcheck_Narrowing


01:39:27 HOL: theory HOL.Random_Pred


01:39:28 HOL: theory HOL.Random_Sequence


01:39:36 HOL: theory HOL.Record


01:39:36 HOL: theory HOL.Predicate_Compile


01:39:40 HOL: theory HOL.Nitpick


01:39:50 HOL: theory HOL.Nunchaku


01:39:51 HOL: theory Main


01:39:53 HOL: theory HOL.Archimedean_Field


01:39:53 HOL: theory HOL.Hull


01:39:53 HOL: theory HOL.Topological_Spaces


01:39:54 HOL: theory HOL.Modules


01:39:56 HOL: theory HOL.Vector_Spaces


01:40:09 HOL: theory HOL.Rat


01:40:15 HOL: theory HOL.Real


01:40:18 HOL: theory HOL.Real_Vector_Spaces


01:40:36 HOL: theory HOL.Inequalities


01:40:36 HOL: theory HOL.Limits


01:40:45 HOL: theory HOL.Deriv


01:40:45 HOL: theory HOL.Series


01:40:49 HOL: theory HOL.NthRoot


01:40:50 HOL: theory HOL.Transcendental


01:40:59 HOL: theory HOL.Complex


01:41:01 HOL: theory HOL.MacLaurin


01:41:02 HOL: theory Complex_Main


01:42:51 Timing HOL (8 threads, 305.645s elapsed time, 1128.920s cpu time, 111.400s GC time, factor 3.69)


01:42:51 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL


01:42:51 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf


01:42:51 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf


01:42:51 Finished HOL (0:06:41 elapsed time, 0:22:05 cpu time, factor 3.31)


01:42:51 Running JinjaThreads ...


01:42:54 JinjaThreads: theory HOL-Eisbach.Eisbach


01:42:54 JinjaThreads: theory Automatic_Refinement.Foldi


01:42:54 JinjaThreads: theory Automatic_Refinement.Prio_List


01:42:54 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1


01:42:54 JinjaThreads: theory HOL-Library.Adhoc_Overloading


01:42:54 JinjaThreads: theory Collections.ICF_Tools


01:42:54 JinjaThreads: theory HOL-Library.AList


01:42:54 JinjaThreads: theory Finger-Trees.FingerTree


01:42:54 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot


01:42:54 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot


01:42:55 JinjaThreads: theory HOL-Library.Monad_Syntax


01:42:55 JinjaThreads: theory Collections.Ord_Code_Preproc


01:42:55 JinjaThreads: theory HOL-Library.Bit


01:42:55 JinjaThreads: theory HOL-Library.Boolean_Algebra


01:42:55 JinjaThreads: theory Collections.Locale_Code


01:42:55 JinjaThreads: theory Collections.Record_Intf


01:42:55 JinjaThreads: theory Automatic_Refinement.Refine_Util


01:42:55 JinjaThreads: theory HOL-Library.Cancellation


01:42:55 JinjaThreads: theory HOL-Library.Case_Converter


01:42:55 JinjaThreads: theory HOL-Library.Code_Abstract_Nat


01:42:55 JinjaThreads: theory HOL-Library.Code_Target_Nat


01:42:56 JinjaThreads: theory HOL-Library.Simps_Case_Conv


01:42:56 JinjaThreads: theory HOL-Library.Code_Target_Int


01:42:56 JinjaThreads: theory HOL-Library.Dlist


01:42:56 JinjaThreads: theory HOL-Library.Infinite_Set


01:42:56 JinjaThreads: theory HOL-Library.Lattice_Syntax


01:42:56 JinjaThreads: theory Automatic_Refinement.Anti_Unification


01:42:56 JinjaThreads: theory Automatic_Refinement.Attr_Comb


01:42:56 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms


01:42:56 JinjaThreads: theory Automatic_Refinement.Autoref_Data


01:42:56 JinjaThreads: theory Automatic_Refinement.Indep_Vars


01:42:56 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp


01:42:56 JinjaThreads: theory Automatic_Refinement.Tagged_Solver


01:42:57 JinjaThreads: theory Automatic_Refinement.Select_Solve


01:42:57 JinjaThreads: theory HOL-Library.Code_Target_Numeral


01:42:57 JinjaThreads: theory HOL-Library.Complete_Partial_Order2


01:42:57 JinjaThreads: theory HOL-Library.Multiset


01:42:57 JinjaThreads: theory HOL-Library.Nat_Bijection


01:42:57 JinjaThreads: theory HOL-Library.Old_Datatype


01:42:57 JinjaThreads: theory HOL-Library.Option_ord


01:42:58 JinjaThreads: theory HOL-Library.Phantom_Type


01:42:58 JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs


01:42:58 JinjaThreads: theory Trie.Trie


01:42:58 JinjaThreads: theory HOL-Library.RBT_Impl


01:42:58 JinjaThreads: theory HOL-Library.Sublist


01:42:58 JinjaThreads: theory HOL-Library.Transitive_Closure_Table


01:42:59 JinjaThreads: theory HOL-Library.Cardinality


01:42:59 JinjaThreads: theory HOL-Library.While_Combinator


01:43:01 JinjaThreads: theory Collections.DatRef


01:43:01 JinjaThreads: theory HOL-Word.Bit_Representation


01:43:01 JinjaThreads: theory HOL-Word.Bits


01:43:03 JinjaThreads: theory HOL-Word.Bits_Bit


01:43:03 JinjaThreads: theory FinFun.FinFun


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


01:43:04 JinjaThreads: theory HOL-Word.Misc_Typedef


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


01:43:04 JinjaThreads: theory JinjaThreads.Set_Monad


01:43:04 JinjaThreads: theory JinjaThreads.Set_without_equal


01:43:04 JinjaThreads: theory Refine_Monadic.Refine_Chapter


01:43:05 JinjaThreads: theory HOL-Word.Bool_List_Representation


01:43:05 JinjaThreads: theory HOL-Word.Misc_Arithmetic


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


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


01:43:07 JinjaThreads: theory HOL-Word.Bits_Int


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


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


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


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


01:43:09 JinjaThreads: theory Native_Word.More_Bits_Int


01:43:09 JinjaThreads: theory HOL-Word.Word


01:43:10 JinjaThreads: theory Automatic_Refinement.Misc


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


01:43:12 JinjaThreads: theory Native_Word.Bits_Integer


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


01:43:14 JinjaThreads: theory JinjaThreads.Auxiliary


01:43:15 JinjaThreads: theory Coinductive.Coinductive_Nat


01:43:17 JinjaThreads: theory Coinductive.Coinductive_List


01:43:23 JinjaThreads: theory Native_Word.Word_Misc


01:43:25 JinjaThreads: theory Automatic_Refinement.Refine_Lib


01:43:25 JinjaThreads: theory Collections.SetIterator


01:43:25 JinjaThreads: theory Collections.Sorted_List_Operations


01:43:28 JinjaThreads: theory Automatic_Refinement.Autoref_Phases


01:43:28 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging


01:43:28 JinjaThreads: theory Automatic_Refinement.Relators


01:43:28 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover


01:43:28 JinjaThreads: theory Collections.SetIteratorOperations


01:43:32 JinjaThreads: theory Automatic_Refinement.Param_Tool


01:43:32 JinjaThreads: theory Automatic_Refinement.Param_HOL


01:43:35 JinjaThreads: theory Collections.Assoc_List


01:43:35 JinjaThreads: theory Collections.Dlist_add


01:43:35 JinjaThreads: theory Collections.Proper_Iterator


01:43:36 JinjaThreads: theory Collections.SetIteratorGA


01:43:36 JinjaThreads: theory Automatic_Refinement.Parametricity


01:43:36 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops


01:43:37 JinjaThreads: theory Collections.Diff_Array


01:43:37 JinjaThreads: theory Collections.Trie_Impl


01:43:38 JinjaThreads: theory Collections.Trie2


01:43:39 JinjaThreads: theory Collections.It_to_It


01:43:39 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel


01:43:40 JinjaThreads: theory Coinductive.Lazy_LList


01:43:40 JinjaThreads: theory Coinductive.TLList


01:43:40 JinjaThreads: theory Automatic_Refinement.Autoref_Translate


01:43:40 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface


01:43:41 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo


01:43:41 JinjaThreads: theory Automatic_Refinement.Autoref_Tool


01:43:42 JinjaThreads: theory Native_Word.Code_Target_Bits_Int


01:43:42 JinjaThreads: theory Native_Word.Uint32


01:43:42 JinjaThreads: theory Collections.Code_Target_ICF


01:43:43 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL


01:43:46 JinjaThreads: theory Coinductive.Lazy_TLList


01:43:46 JinjaThreads: theory Collections.HashCode


01:43:52 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement


01:43:52 JinjaThreads: theory Collections.Idx_Iterator


01:43:52 JinjaThreads: theory Refine_Monadic.Refine_Misc


01:43:54 JinjaThreads: theory Refine_Monadic.RefineG_Domain


01:43:54 JinjaThreads: theory Refine_Monadic.RefineG_Transfer


01:43:55 JinjaThreads: theory Refine_Monadic.RefineG_Assert


01:43:55 JinjaThreads: theory Refine_Monadic.RefineG_Recursion


01:43:56 JinjaThreads: theory Refine_Monadic.RefineG_While


01:43:56 JinjaThreads: theory Refine_Monadic.Refine_Basic


01:43:57 JinjaThreads: theory Refine_Monadic.Refine_Det


01:44:04 JinjaThreads: theory Refine_Monadic.Refine_Heuristics


01:44:04 JinjaThreads: theory Refine_Monadic.Refine_Leof


01:44:04 JinjaThreads: theory Refine_Monadic.Refine_Pfun


01:44:04 JinjaThreads: theory Refine_Monadic.Refine_More_Comb


01:44:04 JinjaThreads: theory Refine_Monadic.Refine_While


01:44:07 JinjaThreads: theory Refine_Monadic.Refine_Transfer


01:44:08 JinjaThreads: theory Refine_Monadic.Refine_Automation


01:44:08 JinjaThreads: theory Refine_Monadic.Autoref_Monadic


01:44:08 JinjaThreads: theory Refine_Monadic.Refine_Foreach


01:44:13 JinjaThreads: theory Refine_Monadic.Refine_Monadic


01:44:15 JinjaThreads: theory Collections.Gen_Iterator


01:44:15 JinjaThreads: theory Collections.Intf_Map


01:44:15 JinjaThreads: theory Collections.Intf_Set


01:44:17 JinjaThreads: theory Collections.Iterator


01:44:18 JinjaThreads: theory Collections.Array_Iterator


01:44:18 JinjaThreads: theory Collections.ICF_Spec_Base


01:44:19 JinjaThreads: theory Collections.AnnotatedListSpec


01:44:19 JinjaThreads: theory Collections.ListSpec


01:44:19 JinjaThreads: theory Collections.MapSpec


01:44:19 JinjaThreads: theory Collections.PrioSpec


01:44:20 JinjaThreads: theory Collections.PrioUniqueSpec


01:44:21 JinjaThreads: theory Collections.SetSpec


01:44:21 JinjaThreads: theory Collections.BinoPrioImpl


01:44:22 JinjaThreads: theory Collections.SkewPrioImpl


01:44:22 JinjaThreads: theory Collections.ListGA


01:44:23 JinjaThreads: theory Collections.FTAnnotatedListImpl


01:44:23 JinjaThreads: theory Collections.PrioByAnnotatedList


01:44:24 JinjaThreads: theory Collections.Fifo


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


01:44:26 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList


01:44:27 JinjaThreads: theory Collections.RBT_add


01:44:32 JinjaThreads: theory Collections.Algos


01:44:32 JinjaThreads: theory Collections.SetIndex


01:44:32 JinjaThreads: theory Collections.SetIteratorCollectionsGA


01:44:34 JinjaThreads: theory Collections.MapGA


01:44:34 JinjaThreads: theory Collections.SetGA


01:44:35 JinjaThreads: theory Collections.FTPrioImpl


01:44:35 JinjaThreads: theory Collections.FTPrioUniqueImpl


01:44:39 JinjaThreads: theory Collections.ArrayMapImpl


01:44:39 JinjaThreads: theory Collections.ListMapImpl


01:44:39 JinjaThreads: theory Collections.ListMapImpl_Invar


01:44:39 JinjaThreads: theory Collections.TrieMapImpl


01:44:40 JinjaThreads: theory Collections.RBTMapImpl


01:44:45 JinjaThreads: theory Collections.ListSetImpl


01:44:46 JinjaThreads: theory Collections.ListSetImpl_Invar


01:44:46 JinjaThreads: theory Collections.ListSetImpl_NotDist


01:44:49 JinjaThreads: theory Collections.ListSetImpl_Sorted


01:44:50 JinjaThreads: theory Collections.ArrayHashMap_Impl


01:44:52 JinjaThreads: theory Collections.SetByMap


01:44:57 JinjaThreads: theory Collections.HashMap_Impl


01:44:58 JinjaThreads: theory Collections.ArraySetImpl


01:44:59 JinjaThreads: theory Collections.TrieSetImpl


01:44:59 JinjaThreads: theory Collections.RBTSetImpl


01:45:01 JinjaThreads: theory Collections.ArrayHashMap


01:45:03 JinjaThreads: theory Collections.HashMap


01:45:15 JinjaThreads: theory Collections.ArrayHashSet


01:45:16 JinjaThreads: theory Collections.HashSet


01:45:16 JinjaThreads: theory Collections.MapStdImpl


01:45:28 JinjaThreads: theory Collections.SetStdImpl


01:45:34 JinjaThreads: theory Collections.ICF_Impl


01:45:44 JinjaThreads: theory Collections.ICF_Refine_Monadic


01:45:45 JinjaThreads: theory Collections.ICF_Autoref


01:45:50 JinjaThreads: theory Collections.Collections


01:45:51 JinjaThreads: theory Collections.CollectionsV1


01:46:03 JinjaThreads: theory JinjaThreads.JT_ICF


01:46:03 JinjaThreads: theory JinjaThreads.Basic_Main


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


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


01:46:52 JinjaThreads: theory JinjaThreads.FWState


01:46:52 JinjaThreads: theory JinjaThreads.LTS


01:46:52 JinjaThreads: theory JinjaThreads.Type


01:46:52 JinjaThreads: theory JinjaThreads.Orders


01:46:52 JinjaThreads: theory JinjaThreads.ListIndex


01:46:52 JinjaThreads: theory JinjaThreads.Semilat


01:46:53 JinjaThreads: theory JinjaThreads.Err


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


01:46:55 JinjaThreads: theory JinjaThreads.Listn


01:46:55 JinjaThreads: theory JinjaThreads.Opt


01:46:55 JinjaThreads: theory JinjaThreads.Product


01:46:56 JinjaThreads: theory JinjaThreads.Semilattices


01:46:56 JinjaThreads: theory JinjaThreads.Typing_Framework


01:46:57 JinjaThreads: theory JinjaThreads.SemilatAlg


01:46:57 JinjaThreads: theory JinjaThreads.Decl


01:46:57 JinjaThreads: theory JinjaThreads.Kildall


01:46:57 JinjaThreads: theory JinjaThreads.LBVSpec


01:46:58 JinjaThreads: theory JinjaThreads.Bisimulation


01:46:58 JinjaThreads: theory JinjaThreads.Typing_Framework_err


01:46:58 JinjaThreads: theory JinjaThreads.LBVComplete


01:46:58 JinjaThreads: theory JinjaThreads.LBVCorrect


01:46:59 JinjaThreads: theory JinjaThreads.Abstract_BV


01:47:00 JinjaThreads: theory JinjaThreads.TypeRel


01:47:07 JinjaThreads: theory JinjaThreads.TypeRelRefine


01:47:07 JinjaThreads: theory JinjaThreads.Value


01:47:12 JinjaThreads: theory JinjaThreads.Exceptions


01:47:12 JinjaThreads: theory JinjaThreads.Heap


01:47:13 JinjaThreads: theory JinjaThreads.SystemClasses


01:47:15 JinjaThreads: theory JinjaThreads.MM


01:47:15 JinjaThreads: theory JinjaThreads.State


01:47:25 JinjaThreads: theory JinjaThreads.FWCondAction


01:47:25 JinjaThreads: theory JinjaThreads.FWLock


01:47:25 JinjaThreads: theory JinjaThreads.FWInterrupt


01:47:25 JinjaThreads: theory JinjaThreads.FWThread


01:47:25 JinjaThreads: theory JinjaThreads.FWWait


01:47:25 JinjaThreads: theory JinjaThreads.Observable_Events


01:47:28 JinjaThreads: theory JinjaThreads.FWLocking


01:47:29 JinjaThreads: theory JinjaThreads.FWLockingThread


01:47:29 JinjaThreads: theory JinjaThreads.FWWellform


01:47:31 JinjaThreads: theory JinjaThreads.FWLifting


01:47:31 JinjaThreads: theory JinjaThreads.FWSemantics


01:47:34 JinjaThreads: theory JinjaThreads.JVMState


01:47:34 JinjaThreads: theory JinjaThreads.StartConfig


01:47:34 JinjaThreads: theory JinjaThreads.JMM_Spec


01:47:34 JinjaThreads: theory JinjaThreads.FWLiftingSem


01:47:34 JinjaThreads: theory JinjaThreads.FWProgressAux


01:47:36 JinjaThreads: theory JinjaThreads.Conform


01:47:37 JinjaThreads: theory JinjaThreads.FWDeadlock


01:47:37 JinjaThreads: theory JinjaThreads.FWLTS


01:47:38 JinjaThreads: theory JinjaThreads.State_Refinement


01:47:39 JinjaThreads: theory JinjaThreads.ConformThreaded


01:47:41 JinjaThreads: theory JinjaThreads.ExternalCall


01:47:41 JinjaThreads: theory JinjaThreads.FWProgress


01:47:41 JinjaThreads: theory JinjaThreads.SC


01:47:42 JinjaThreads: theory JinjaThreads.SC_Collections


01:47:51 JinjaThreads: theory JinjaThreads.FWBisimulation


01:47:51 JinjaThreads: theory JinjaThreads.FWInitFinLift


01:47:51 JinjaThreads: theory JinjaThreads.Scheduler


01:47:51 JinjaThreads: theory JinjaThreads.JMM_DRF


01:47:52 JinjaThreads: theory JinjaThreads.Non_Speculative


01:47:52 JinjaThreads: theory JinjaThreads.SC_Legal


01:47:56 JinjaThreads: theory JinjaThreads.HB_Completion


01:47:57 JinjaThreads: theory JinjaThreads.SC_Completion


01:48:34 JinjaThreads: theory JinjaThreads.WellForm


01:48:35 JinjaThreads: theory JinjaThreads.ExternalCall_Execute


01:48:39 JinjaThreads: theory JinjaThreads.BinOp


01:48:39 JinjaThreads: theory JinjaThreads.ExternalCallWF


01:48:41 JinjaThreads: theory JinjaThreads.JMM_Heap


01:48:44 JinjaThreads: theory JinjaThreads.SemiType


01:48:45 JinjaThreads: theory JinjaThreads.Random_Scheduler


01:48:46 JinjaThreads: theory JinjaThreads.Round_Robin


01:48:49 JinjaThreads: theory JinjaThreads.JVM_SemiType


01:48:49 JinjaThreads: theory JinjaThreads.JMM_Framework


01:48:50 JinjaThreads: theory JinjaThreads.JMM_Type


01:48:56 JinjaThreads: theory JinjaThreads.JMM_Type2


01:49:06 JinjaThreads: theory JinjaThreads.SC_Schedulers


01:49:21 JinjaThreads: theory JinjaThreads.Expr


01:49:21 JinjaThreads: theory JinjaThreads.JVMInstructions


01:49:45 JinjaThreads: theory JinjaThreads.PCompiler


01:49:47 JinjaThreads: theory JinjaThreads.PCompilerRefine


01:49:58 JinjaThreads: theory JinjaThreads.JVMExceptions


01:49:58 JinjaThreads: theory JinjaThreads.JVMHeap


01:49:59 JinjaThreads: theory JinjaThreads.Effect


01:50:09 JinjaThreads: theory JinjaThreads.JVMExecInstr


01:50:12 JinjaThreads: theory JinjaThreads.CallExpr


01:50:12 JinjaThreads: theory JinjaThreads.DefAss


01:50:12 JinjaThreads: theory JinjaThreads.WWellForm


01:50:12 JinjaThreads: theory JinjaThreads.JHeap


01:50:14 JinjaThreads: theory JinjaThreads.WellType


01:50:14 JinjaThreads: theory JinjaThreads.ToString


01:50:14 JinjaThreads: theory JinjaThreads.JVMExec


01:50:20 JinjaThreads: theory JinjaThreads.JVMDefensive


01:50:23 JinjaThreads: theory JinjaThreads.J1State


01:50:24 JinjaThreads: theory JinjaThreads.SmallStep


01:50:24 JinjaThreads: theory JinjaThreads.Annotate


01:50:27 JinjaThreads: theory JinjaThreads.JMM_Typesafe


01:50:28 JinjaThreads: theory JinjaThreads.Compiler2


01:50:30 JinjaThreads: theory JinjaThreads.JVMThreaded


01:50:35 JinjaThreads: theory JinjaThreads.J1Heap


01:50:42 JinjaThreads: theory JinjaThreads.Compiler1


01:50:47 JinjaThreads: theory JinjaThreads.JMM_Common


01:50:47 JinjaThreads: theory JinjaThreads.Exception_Tables


01:50:48 JinjaThreads: theory JinjaThreads.J1WellType


01:50:50 JinjaThreads: theory JinjaThreads.JVM_Main


01:50:50 JinjaThreads: theory JinjaThreads.JMM_JVM


01:50:50 JinjaThreads: theory JinjaThreads.JWellForm


01:50:51 JinjaThreads: theory JinjaThreads.Compiler


01:50:52 JinjaThreads: theory JinjaThreads.WellTypeRT


01:50:52 JinjaThreads: theory JinjaThreads.Preprocessor


01:50:54 JinjaThreads: theory JinjaThreads.J1WellForm


01:50:55 JinjaThreads: theory JinjaThreads.JVMExec_Execute


01:50:55 JinjaThreads: theory JinjaThreads.JJ1WellForm


01:50:59 JinjaThreads: theory JinjaThreads.JMM_Typesafe2


01:51:00 JinjaThreads: theory JinjaThreads.FWBisimDeadlock


01:51:00 JinjaThreads: theory JinjaThreads.FWBisimLift


01:51:06 JinjaThreads: theory JinjaThreads.J1


01:51:56 JinjaThreads: theory JinjaThreads.BVSpec


01:51:57 JinjaThreads: theory JinjaThreads.BVConform


01:51:57 JinjaThreads: theory JinjaThreads.TypeComp


01:51:57 JinjaThreads: theory JinjaThreads.EffectMono


01:51:57 JinjaThreads: theory JinjaThreads.TF_JVM


01:52:05 JinjaThreads: theory JinjaThreads.BVExec


01:52:05 JinjaThreads: theory JinjaThreads.Common_Main


01:52:05 JinjaThreads: theory JinjaThreads.LBVJVM


01:52:11 JinjaThreads: theory JinjaThreads.BVSpecTypeSafe


01:52:27 JinjaThreads: theory JinjaThreads.BVNoTypeError


01:52:28 JinjaThreads: theory JinjaThreads.J1Deadlock


01:52:31 JinjaThreads: theory JinjaThreads.BVProgressThreaded


01:52:32 JinjaThreads: theory JinjaThreads.BCVExec


01:52:33 JinjaThreads: theory JinjaThreads.JVMExec_Execute2


01:52:36 JinjaThreads: theory JinjaThreads.JVMTau


01:53:17 JinjaThreads: theory JinjaThreads.Execs


01:54:00 JinjaThreads: theory JinjaThreads.DefAssPreservation


01:54:00 JinjaThreads: theory JinjaThreads.Threaded


01:54:00 JinjaThreads: theory JinjaThreads.Progress


01:54:10 JinjaThreads: theory JinjaThreads.TypeSafe


01:54:29 JinjaThreads: theory JinjaThreads.J1JVMBisim


01:54:37 JinjaThreads: theory JinjaThreads.J0


01:54:38 JinjaThreads: theory JinjaThreads.JMM_J


01:54:45 JinjaThreads: theory JinjaThreads.DRF_JVM


01:54:46 JinjaThreads: theory JinjaThreads.JVMDeadlocked


01:54:46 JinjaThreads: theory JinjaThreads.JVM_Execute


01:54:46 JinjaThreads: theory JinjaThreads.ProgressThreaded


01:54:48 JinjaThreads: theory JinjaThreads.JVM_Execute2


01:54:52 JinjaThreads: theory JinjaThreads.J_Execute


01:55:35 JinjaThreads: theory JinjaThreads.Code_Generation


01:55:38 JinjaThreads: theory JinjaThreads.BV_Main


01:55:45 JinjaThreads: theory JinjaThreads.DRF_J


01:55:45 JinjaThreads: theory JinjaThreads.Deadlocked


01:55:51 JinjaThreads: theory JinjaThreads.J0Bisim


01:55:51 JinjaThreads: theory JinjaThreads.J0J1Bisim


01:55:53 JinjaThreads: theory JinjaThreads.ApprenticeChallenge


01:56:02 JinjaThreads: theory JinjaThreads.BufferExample


01:56:02 JinjaThreads: theory JinjaThreads.J_Main


01:56:04 JinjaThreads: theory JinjaThreads.Java2Jinja


01:56:27 JinjaThreads: theory JinjaThreads.Examples_Main


01:57:03 JinjaThreads: theory JinjaThreads.Correctness1


01:57:15 JinjaThreads: theory JinjaThreads.Correctness1Threaded


02:06:11 JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe


02:06:40 JinjaThreads: theory JinjaThreads.Execute_Main


02:07:23 JinjaThreads: theory JinjaThreads.JMM_J_Typesafe


02:07:37 JinjaThreads: theory JinjaThreads.J1JVM


02:07:42 JinjaThreads: theory JinjaThreads.JVMJ1


02:09:37 JinjaThreads: theory JinjaThreads.Correctness2


02:12:33 JinjaThreads: theory JinjaThreads.Correctness


02:23:40 JinjaThreads: theory JinjaThreads.Compiler_Main


02:24:05 JinjaThreads: theory JinjaThreads.JMM_Compiler


02:24:05 JinjaThreads: theory JinjaThreads.SC_Interp


02:40:27 JinjaThreads: theory JinjaThreads.JMM_Interp


02:40:35 JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2


02:40:39 JinjaThreads: theory JinjaThreads.JMM


02:40:44 JinjaThreads: theory JinjaThreads.MM_Main


02:41:01 JinjaThreads: theory JinjaThreads.JinjaThreads


02:47:07 Timing JinjaThreads (8 threads, 3788.247s elapsed time, 18056.228s cpu time, 5967.260s GC time, factor 4.77)


02:47:07 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads


02:47:07 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf


02:47:07 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf


02:47:07 Finished JinjaThreads (1:04:11 elapsed time, 5:08:48 cpu time, factor 4.81)


02:47:07 Building Flyspeck-Tame ...


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


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


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


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


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


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


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


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


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


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


02:47:09 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral


02:47:09 Flyspeck-Tame: theory Flyspeck-Tame.Arch


02:47:09 Flyspeck-Tame: theory Flyspeck-Tame.Worklist


02:47:10 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax


02:47:10 Flyspeck-Tame: theory Flyspeck-Tame.ListSum


02:47:10 Flyspeck-Tame: theory Flyspeck-Tame.Rotation


02:47:11 Flyspeck-Tame: theory Flyspeck-Tame.Graph


02:47:11 Flyspeck-Tame: theory Flyspeck-Tame.Maps


02:47:12 Flyspeck-Tame: theory Trie.Trie


02:47:14 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision


02:47:15 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps


02:47:15 Flyspeck-Tame: theory Flyspeck-Tame.Tame


02:47:15 Flyspeck-Tame: theory Trie.Tries


02:47:15 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator


02:47:16 Flyspeck-Tame: theory Flyspeck-Tame.TameProps


02:47:17 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps


02:47:18 Flyspeck-Tame: theory Flyspeck-Tame.Plane


02:47:19 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps


02:47:19 Flyspeck-Tame: theory Flyspeck-Tame.Plane1


02:47:19 Flyspeck-Tame: theory Flyspeck-Tame.Generator


02:47:20 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum


02:47:25 Flyspeck-Tame: theory Flyspeck-Tame.Invariants


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


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


02:47:32 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props


02:47:32 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux


02:47:33 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound


02:47:33 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps


02:47:34 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps


02:47:34 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps


02:47:35 Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness


02:49:52 Timing Flyspeck-Tame (8 threads, 111.637s elapsed time, 640.936s cpu time, 49.708s GC time, factor 5.74)


02:49:52 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame


02:49:52 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf


02:49:52 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf


02:49:52 Finished Flyspeck-Tame (0:02:43 elapsed time, 0:12:42 cpu time, factor 4.65)


02:49:52 Running Flyspeck-Tame-Computation ...


02:49:54 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.ArchComp


02:49:54 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.Completeness


10:28:21 Timing Flyspeck-Tame-Computation (8 threads, 27497.729s elapsed time, 41087.712s cpu time, 3185.380s GC time, factor 1.49)


10:28:21 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame-Computation


10:28:21 Finished Flyspeck-Tame-Computation (7:38:19 elapsed time, 11:24:49 cpu time, factor 1.49)


10:28:21 Building AWN ...


10:28:22 AWN: theory AWN.Lib


10:28:22 AWN: theory AWN.TransitionSystems


10:28:22 AWN: theory AWN.AWN


10:28:22 AWN: theory AWN.Invariants


10:28:24 AWN: theory AWN.OInvariants


10:28:37 AWN: theory AWN.AWN_Cterms


10:28:37 AWN: theory AWN.AWN_SOS


10:28:37 AWN: theory AWN.OAWN_SOS


10:28:43 AWN: theory AWN.AWN_Labels


10:28:45 AWN: theory AWN.Pnet


10:28:45 AWN: theory AWN.Inv_Cterms


10:28:45 AWN: theory AWN.AWN_Invariants


10:28:47 AWN: theory AWN.Closed


10:28:47 AWN: theory AWN.AWN_SOS_Labels


10:28:48 AWN: theory AWN.Qmsg


10:28:49 AWN: theory AWN.OAWN_Invariants


10:28:49 AWN: theory AWN.OAWN_SOS_Labels


10:28:49 AWN: theory AWN.ONode_Lifting


10:28:49 AWN: theory AWN.OPnet


10:28:50 AWN: theory AWN.OPnet_Lifting


10:28:51 AWN: theory AWN.OClosed_Lifting


10:28:51 AWN: theory AWN.OClosed_Transfer


10:28:51 AWN: theory AWN.OAWN_Convert


10:28:52 AWN: theory AWN.Qmsg_Lifting


10:28:53 AWN: theory AWN.AWN_Main


10:28:54 AWN: theory AWN.Toy


10:29:13 AWN: theory AWN.AWN_Term_Graph


10:29:49 Timing AWN (8 threads, 55.904s elapsed time, 297.364s cpu time, 9.112s GC time, factor 5.32)


10:29:49 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN


10:29:49 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf


10:29:49 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf


10:29:49 Finished AWN (0:01:27 elapsed time, 0:06:07 cpu time, factor 4.20)


10:29:49 Running AODV ...


10:29:50 AODV: theory AODV.Aodv_Basic


10:29:52 AODV: theory AODV.A_Norreqid


10:29:52 AODV: theory AODV.Aodv_Data


10:29:52 AODV: theory AODV.Aodv_Message


10:29:52 AODV: theory AODV.B_Fwdrreps


10:29:52 AODV: theory AODV.E_All_ABCD


10:29:52 AODV: theory AODV.D_Fwdrreqs


10:29:52 AODV: theory AODV.C_Gtobcast


10:29:53 AODV: theory AODV.D_Aodv_Data


10:29:53 AODV: theory AODV.D_Aodv_Message


10:29:53 AODV: theory AODV.B_Aodv_Data


10:29:53 AODV: theory AODV.B_Aodv_Message


10:29:53 AODV: theory AODV.A_Aodv_Data


10:29:53 AODV: theory AODV.A_Aodv_Message


10:29:55 AODV: theory AODV.Fresher


10:29:55 AODV: theory AODV.C_Aodv_Data


10:29:55 AODV: theory AODV.B_Fresher


10:29:55 AODV: theory AODV.C_Aodv_Message


10:29:56 AODV: theory AODV.D_Fresher


10:29:56 AODV: theory AODV.A_Fresher


10:29:56 AODV: theory AODV.E_Aodv_Data


10:29:56 AODV: theory AODV.E_Aodv_Message


10:29:57 AODV: theory AODV.A_Aodv


10:29:57 AODV: theory AODV.Aodv


10:29:57 AODV: theory AODV.B_Aodv


10:29:57 AODV: theory AODV.D_Aodv


10:29:57 AODV: theory AODV.C_Fresher


10:29:57 AODV: theory AODV.E_Fresher


10:29:58 AODV: theory AODV.C_Aodv


10:29:58 AODV: theory AODV.E_Aodv


10:31:32 AODV: theory AODV.A_Aodv_Predicates


10:31:33 AODV: theory AODV.A_Loop_Freedom


10:31:33 AODV: theory AODV.A_Quality_Increases


10:31:33 AODV: theory AODV.A_Seq_Invariants


10:31:33 AODV: theory AODV.A_OAodv


10:31:34 AODV: theory AODV.A_Global_Invariants


10:31:36 AODV: theory AODV.A_Aodv_Loop_Freedom


10:31:51 AODV: theory AODV.Aodv_Predicates


10:31:51 AODV: theory AODV.OAodv


10:31:51 AODV: theory AODV.Loop_Freedom


10:31:51 AODV: theory AODV.Quality_Increases


10:31:51 AODV: theory AODV.Seq_Invariants


10:31:53 AODV: theory AODV.Global_Invariants


10:31:54 AODV: theory AODV.Aodv_Loop_Freedom


10:32:00 AODV: theory AODV.B_Aodv_Predicates


10:32:00 AODV: theory AODV.B_OAodv


10:32:00 AODV: theory AODV.B_Loop_Freedom


10:32:01 AODV: theory AODV.B_Quality_Increases


10:32:01 AODV: theory AODV.B_Seq_Invariants


10:32:02 AODV: theory AODV.B_Global_Invariants


10:32:04 AODV: theory AODV.B_Aodv_Loop_Freedom


10:32:11 AODV: theory AODV.C_Aodv_Predicates


10:32:12 AODV: theory AODV.C_Loop_Freedom


10:32:12 AODV: theory AODV.C_Quality_Increases


10:32:12 AODV: theory AODV.C_Seq_Invariants


10:32:12 AODV: theory AODV.E_Aodv_Predicates


10:32:12 AODV: theory AODV.C_OAodv


10:32:13 AODV: theory AODV.E_Loop_Freedom


10:32:13 AODV: theory AODV.E_Quality_Increases


10:32:13 AODV: theory AODV.E_Seq_Invariants


10:32:13 AODV: theory AODV.E_OAodv


10:32:13 AODV: theory AODV.C_Global_Invariants


10:32:14 AODV: theory AODV.E_Global_Invariants


10:32:15 AODV: theory AODV.C_Aodv_Loop_Freedom


10:32:16 AODV: theory AODV.E_Aodv_Loop_Freedom


10:32:19 AODV: theory AODV.D_Aodv_Predicates


10:32:19 AODV: theory AODV.D_OAodv


10:32:19 AODV: theory AODV.D_Loop_Freedom


10:32:20 AODV: theory AODV.D_Quality_Increases


10:32:20 AODV: theory AODV.D_Seq_Invariants


10:32:21 AODV: theory AODV.D_Global_Invariants


10:32:22 AODV: theory AODV.D_Aodv_Loop_Freedom


10:32:31 AODV: theory AODV.All


13:23:08 Timing AODV (8 threads, 10380.016s elapsed time, 57796.464s cpu time, 4641.456s GC time, factor 5.57)


13:23:08 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV


13:23:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/document.pdf


13:23:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/outline.pdf


13:23:08 Finished AODV (2:53:15 elapsed time, 16:03:45 cpu time, factor 5.56)


13:23:08 Building HOL-Library ...


13:23:11 HOL-Library: theory HOL-Library.AList


13:23:11 HOL-Library: theory HOL-Library.Adhoc_Overloading


13:23:11 HOL-Library: theory HOL-Library.BNF_Axiomatization


13:23:11 HOL-Library: theory HOL-Library.BNF_Corec


13:23:11 HOL-Library: theory HOL-Library.Bit


13:23:11 HOL-Library: theory HOL-Library.Cancellation


13:23:11 HOL-Library: theory HOL-Library.Boolean_Algebra


13:23:11 HOL-Library: theory HOL-Library.Case_Converter


13:23:11 HOL-Library: theory HOL-Library.Char_ord


13:23:11 HOL-Library: theory HOL-Library.Monad_Syntax


13:23:11 HOL-Library: theory HOL-Library.State_Monad


13:23:11 HOL-Library: theory HOL-Library.Code_Abstract_Nat


13:23:11 HOL-Library: theory HOL-Library.Code_Prolog


13:23:12 HOL-Library: theory HOL-Library.Code_Binary_Nat


13:23:12 HOL-Library: theory HOL-Library.Code_Lazy


13:23:12 HOL-Library: theory HOL-Library.Simps_Case_Conv


13:23:12 HOL-Library: theory HOL-Library.Extended


13:23:12 HOL-Library: theory HOL-Library.Code_Target_Nat


13:23:12 HOL-Library: theory HOL-Library.Multiset


13:23:12 HOL-Library: theory HOL-Library.Code_Target_Int


13:23:13 HOL-Library: theory HOL-Library.Code_Test


13:23:13 HOL-Library: theory HOL-Library.Code_Target_Numeral


13:23:13 HOL-Library: theory HOL-Library.Comparator


13:23:14 HOL-Library: theory HOL-Library.Conditional_Parametricity


13:23:14 HOL-Library: theory HOL-Library.Datatype_Records


13:23:14 HOL-Library: theory HOL-Library.Debug


13:23:14 HOL-Library: theory HOL-Library.Disjoint_Sets


13:23:14 HOL-Library: theory HOL-Library.Dlist


13:23:14 HOL-Library: theory HOL-Library.DAList


13:23:15 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice


13:23:15 HOL-Library: theory HOL-Library.Fun_Lexorder


13:23:15 HOL-Library: theory HOL-Library.FuncSet


13:23:15 HOL-Library: theory HOL-Library.Function_Algebras


13:23:15 HOL-Library: theory HOL-Library.Function_Division


13:23:15 HOL-Library: theory HOL-Library.Groups_Big_Fun


13:23:16 HOL-Library: theory HOL-Library.IArray


13:23:16 HOL-Library: theory HOL-Library.Infinite_Set


13:23:16 HOL-Library: theory HOL-Library.Equipollence


13:23:16 HOL-Library: theory HOL-Library.LaTeXsugar


13:23:16 HOL-Library: theory HOL-Library.Lattice_Constructions


13:23:16 HOL-Library: theory HOL-Library.Lattice_Syntax


13:23:16 HOL-Library: theory HOL-Library.Combine_PER


13:23:16 HOL-Library: theory HOL-Library.Complete_Partial_Order2


13:23:16 HOL-Library: theory HOL-Library.ListVector


13:23:17 HOL-Library: theory HOL-Library.Omega_Words_Fun


13:23:17 HOL-Library: theory HOL-Library.Ramsey


13:23:17 HOL-Library: theory HOL-Library.List_Lexorder


13:23:17 HOL-Library: theory HOL-Library.Mapping


13:23:17 HOL-Library: theory HOL-Library.More_List


13:23:17 HOL-Library: theory HOL-Library.Nat_Bijection


13:23:17 HOL-Library: theory HOL-Library.Old_Datatype


13:23:18 HOL-Library: theory HOL-Library.Poly_Mapping


13:23:19 HOL-Library: theory HOL-Library.Stream


13:23:20 HOL-Library: theory HOL-Library.Old_Recdef


13:23:20 HOL-Library: theory HOL-Library.AList_Mapping


13:23:21 HOL-Library: theory HOL-Library.Open_State_Syntax


13:23:21 HOL-Library: theory HOL-Library.Option_ord


13:23:22 HOL-Library: theory HOL-Library.Parallel


13:23:22 HOL-Library: theory HOL-Library.Pattern_Aliases


13:23:22 HOL-Library: theory HOL-Library.Perm


13:23:22 HOL-Library: theory HOL-Library.Phantom_Type


13:23:23 HOL-Library: theory HOL-Library.Power_By_Squaring


13:23:23 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs


13:23:23 HOL-Library: theory HOL-Library.Preorder


13:23:23 HOL-Library: theory HOL-Library.Product_Lexorder


13:23:23 HOL-Library: theory HOL-Library.Product_Plus


13:23:23 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck


13:23:23 HOL-Library: theory HOL-Library.Quotient_Syntax


13:23:23 HOL-Library: theory HOL-Library.Quotient_Option


13:23:24 HOL-Library: theory HOL-Library.Product_Order


13:23:24 HOL-Library: theory HOL-Library.Quotient_Product


13:23:24 HOL-Library: theory HOL-Library.Quotient_Set


13:23:24 HOL-Library: theory HOL-Library.DAList_Multiset


13:23:24 HOL-Library: theory HOL-Library.Multiset_Order


13:23:24 HOL-Library: theory HOL-Library.Permutation


13:23:24 HOL-Library: theory HOL-Library.Permutations


13:23:24 HOL-Library: theory HOL-Library.Cardinality


13:23:24 HOL-Library: theory HOL-Library.Finite_Lattice


13:23:24 HOL-Library: theory HOL-Library.Quotient_List


13:23:24 HOL-Library: theory HOL-Library.Quotient_Sum


13:23:25 HOL-Library: theory HOL-Library.Quotient_Type


13:23:25 HOL-Library: theory HOL-Library.RBT_Impl


13:23:25 HOL-Library: theory HOL-Library.Realizers


13:23:25 HOL-Library: theory HOL-Library.Reflection


13:23:25 HOL-Library: theory HOL-Library.Refute


13:23:25 HOL-Library: theory HOL-Library.Rewrite


13:23:26 HOL-Library: theory HOL-Library.Set_Algebras


13:23:26 HOL-Library: theory HOL-Library.Sorting_Algorithms


13:23:28 HOL-Library: theory HOL-Library.Stirling


13:23:28 HOL-Library: theory HOL-Library.Sublist


13:23:28 HOL-Library: theory HOL-Library.Numeral_Type


13:23:29 HOL-Library: theory HOL-Library.Transitive_Closure_Table


13:23:29 HOL-Library: theory HOL-Library.Tree


13:23:29 HOL-Library: theory HOL-Library.Uprod


13:23:29 HOL-Library: theory HOL-Library.While_Combinator


13:23:30 HOL-Library: theory HOL-Library.Countable


13:23:31 HOL-Library: theory HOL-Library.Type_Length


13:23:31 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint


13:23:31 HOL-Library: theory HOL-Library.BigO


13:23:31 HOL-Library: theory HOL-Library.Saturated


13:23:31 HOL-Library: theory HOL-Library.Prefix_Order


13:23:32 HOL-Library: theory HOL-Library.Subseq_Order


13:23:32 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float


13:23:32 HOL-Library: theory HOL-Library.Diagonal_Subsequence


13:23:32 HOL-Library: theory HOL-Library.Discrete


13:23:32 HOL-Library: theory HOL-Library.Going_To_Filter


13:23:32 HOL-Library: theory HOL-Library.Indicator_Function


13:23:32 HOL-Library: theory HOL-Library.Landau_Symbols


13:23:32 HOL-Library: theory HOL-Library.Lattice_Algebras


13:23:33 HOL-Library: theory HOL-Library.Countable_Set


13:23:33 HOL-Library: theory HOL-Library.FSet


13:23:33 HOL-Library: theory HOL-Library.Liminf_Limsup


13:23:33 HOL-Library: theory HOL-Library.Log_Nat


13:23:33 HOL-Library: theory HOL-Library.Lub_Glb


13:23:34 HOL-Library: theory HOL-Library.Countable_Complete_Lattices


13:23:34 HOL-Library: theory HOL-Library.Countable_Set_Type


13:23:34 HOL-Library: theory HOL-Library.Set_Idioms


13:23:35 HOL-Library: theory HOL-Library.Multiset_Permutations


13:23:35 HOL-Library: theory HOL-Library.Tree_Multiset


13:23:36 HOL-Library: theory HOL-Library.Nonpos_Ints


13:23:36 HOL-Library: theory HOL-Library.OptionalSugar


13:23:37 HOL-Library: theory HOL-Library.Periodic_Fun


13:23:37 HOL-Library: theory HOL-Library.Quadratic_Discriminant


13:23:37 HOL-Library: theory HOL-Library.Sum_of_Squares


13:23:37 HOL-Library: theory HOL-Library.Tree_Real


13:23:38 HOL-Library: theory HOL-Library.Order_Continuity


13:23:39 HOL-Library: theory HOL-Library.Extended_Nat


13:23:40 HOL-Library: theory HOL-Library.Finite_Map


13:23:41 HOL-Library: theory HOL-Library.Extended_Real


13:23:41 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams


13:23:41 HOL-Library: theory HOL-Library.Float


13:23:49 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real


13:24:10 HOL-Library: theory HOL-Library.Library


13:24:36 HOL-Library: theory HOL-Library.RBT


13:24:37 HOL-Library: theory HOL-Library.RBT_Mapping


13:24:37 HOL-Library: theory HOL-Library.RBT_Set


13:26:37 Timing HOL-Library (8 threads, 131.972s elapsed time, 850.152s cpu time, 46.672s GC time, factor 6.44)


13:26:37 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library


13:26:37 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf


13:26:37 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf


13:26:37 Finished HOL-Library (0:03:25 elapsed time, 0:17:48 cpu time, factor 5.19)


13:26:37 Building ConcurrentIMP ...


13:26:39 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred


13:26:39 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang


13:26:53 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg


13:26:55 ConcurrentIMP: theory ConcurrentIMP.CIMP


13:26:55 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer_ex


13:26:55 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer_ex


13:27:26 Timing ConcurrentIMP (8 threads, 21.987s elapsed time, 58.064s cpu time, 2.940s GC time, factor 2.64)


13:27:26 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP


13:27:26 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf


13:27:26 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf


13:27:26 Finished ConcurrentIMP (0:00:48 elapsed time, 0:01:54 cpu time, factor 2.37)


13:27:26 Running ConcurrentGC ...


13:27:28 ConcurrentGC: theory ConcurrentGC.Model


13:27:49 ConcurrentGC: theory ConcurrentGC.Tactics


13:27:58 ConcurrentGC: theory ConcurrentGC.Proofs_basis


13:28:02 ConcurrentGC: theory ConcurrentGC.TSO


13:28:28 ConcurrentGC: theory ConcurrentGC.Handshakes


13:33:26 ConcurrentGC: theory ConcurrentGC.MarkObject


13:37:20 ConcurrentGC: theory ConcurrentGC.StrongTricolour


13:38:50 ConcurrentGC: theory ConcurrentGC.Proofs


13:38:51 ConcurrentGC: theory ConcurrentGC.Concrete_heap


13:38:53 ConcurrentGC: theory ConcurrentGC.Concrete


16:06:04 Timing ConcurrentGC (8 threads, 9507.864s elapsed time, 36807.152s cpu time, 2214.672s GC time, factor 3.87)


16:06:04 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC


16:06:04 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf


16:06:04 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf


16:06:04 Finished ConcurrentGC (2:38:34 elapsed time, 10:13:41 cpu time, factor 3.87)


16:06:04 Building HOL-Word ...


16:06:06 HOL-Word: theory HOL-Library.Bit


16:06:06 HOL-Word: theory HOL-Library.Phantom_Type


16:06:06 HOL-Word: theory HOL-Library.Boolean_Algebra


16:06:06 HOL-Word: theory HOL-Word.Bit_Representation


16:06:06 HOL-Word: theory HOL-Word.Bits


16:06:06 HOL-Word: theory HOL-Word.Misc_Typedef


16:06:07 HOL-Word: theory HOL-Word.Bits_Bit


16:06:07 HOL-Word: theory HOL-Library.Cardinality


16:06:09 HOL-Word: theory HOL-Word.Bool_List_Representation


16:06:09 HOL-Word: theory HOL-Word.Misc_Arithmetic


16:06:10 HOL-Word: theory HOL-Library.Numeral_Type


16:06:10 HOL-Word: theory HOL-Word.Bits_Int


16:06:12 HOL-Word: theory HOL-Library.Type_Length


16:06:12 HOL-Word: theory HOL-Word.Word


16:06:19 HOL-Word: theory HOL-Word.Word_Bitwise


16:06:20 HOL-Word: theory HOL-Word.More_Word


16:06:20 HOL-Word: theory HOL-Word.Word_Examples


16:06:41 Timing HOL-Word (8 threads, 15.390s elapsed time, 84.416s cpu time, 2.892s GC time, factor 5.49)


16:06:41 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word


16:06:41 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf


16:06:41 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf


16:06:41 Finished HOL-Word (0:00:35 elapsed time, 0:02:05 cpu time, factor 3.51)


16:06:41 Building Word_Lib ...


16:06:42 Word_Lib: theory Word_Lib.Hex_Words


16:06:42 Word_Lib: theory Word_Lib.Signed_Words


16:06:42 Word_Lib: theory Word_Lib.Word_Type_Syntax


16:06:42 Word_Lib: theory HOL-Library.Sublist


16:06:42 Word_Lib: theory Word_Lib.Enumeration


16:06:42 Word_Lib: theory Word_Lib.HOL_Lemmas


16:06:42 Word_Lib: theory Word_Lib.More_Divides


16:06:42 Word_Lib: theory Word_Lib.Norm_Words


16:06:42 Word_Lib: theory Word_Lib.WordBitwise_Signed


16:06:43 Word_Lib: theory Word_Lib.Word_Syntax


16:06:44 Word_Lib: theory Word_Lib.Word_Lib


16:06:45 Word_Lib: theory Word_Lib.Word_Enum


16:06:45 Word_Lib: theory Word_Lib.Aligned


16:06:46 Word_Lib: theory Word_Lib.Word_Setup_32


16:06:46 Word_Lib: theory Word_Lib.Word_Setup_64


16:06:46 Word_Lib: theory Word_Lib.Word_Next


16:06:46 Word_Lib: theory Word_Lib.Word_Lemmas


16:06:55 Word_Lib: theory Word_Lib.Word_Lemmas_32


16:06:55 Word_Lib: theory Word_Lib.Word_Lemmas_64


16:08:13 Timing Word_Lib (8 threads, 73.061s elapsed time, 213.444s cpu time, 6.188s GC time, factor 2.92)


16:08:13 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib


16:08:13 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf


16:08:13 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf


16:08:13 Finished Word_Lib (0:01:31 elapsed time, 0:04:10 cpu time, factor 2.75)


16:08:13 Building IP_Addresses ...


16:08:14 IP_Addresses: theory HOL-Eisbach.Eisbach


16:08:14 IP_Addresses: theory HOL-Library.Cancellation


16:08:14 IP_Addresses: theory HOL-Library.Infinite_Set


16:08:14 IP_Addresses: theory HOL-Library.Option_ord


16:08:14 IP_Addresses: theory IP_Addresses.NumberWang_IPv4


16:08:14 IP_Addresses: theory IP_Addresses.NumberWang_IPv6


16:08:15 IP_Addresses: theory HOL-Library.Multiset


16:08:23 IP_Addresses: theory HOL-ex.Quicksort


16:08:23 IP_Addresses: theory Automatic_Refinement.Misc


16:08:32 IP_Addresses: theory HOL-Library.Code_Abstract_Nat


16:08:32 IP_Addresses: theory HOL-Library.Product_Lexorder


16:08:32 IP_Addresses: theory IP_Addresses.Hs_Compat


16:08:32 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString


16:08:32 IP_Addresses: theory IP_Addresses.WordInterval


16:08:32 IP_Addresses: theory HOL-Library.Code_Target_Nat


16:08:32 IP_Addresses: theory IP_Addresses.Lib_List_toString


16:08:32 IP_Addresses: theory IP_Addresses.Lib_Word_toString


16:08:39 IP_Addresses: theory IP_Addresses.IP_Address


16:08:39 IP_Addresses: theory IP_Addresses.WordInterval_Sorted


16:08:45 IP_Addresses: theory IP_Addresses.Prefix_Match


16:08:45 IP_Addresses: theory IP_Addresses.IPv6


16:08:45 IP_Addresses: theory IP_Addresses.IPv4


16:08:47 IP_Addresses: theory IP_Addresses.CIDR_Split


16:10:34 IP_Addresses: theory IP_Addresses.IP_Address_Parser


16:10:34 IP_Addresses: theory IP_Addresses.IP_Address_toString


16:10:37 IP_Addresses: theory IP_Addresses.Prefix_Match_toString


16:14:43 Timing IP_Addresses (8 threads, 347.974s elapsed time, 1153.528s cpu time, 66.004s GC time, factor 3.31)


16:14:43 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses


16:14:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf


16:14:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf


16:14:43 Finished IP_Addresses (0:06:29 elapsed time, 0:21:01 cpu time, factor 3.24)


16:14:43 Building Simple_Firewall ...


16:14:45 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State


16:14:45 Simple_Firewall: theory HOL-Library.Char_ord


16:14:45 Simple_Firewall: theory Simple_Firewall.GroupF


16:14:45 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries


16:14:45 Simple_Firewall: theory Simple_Firewall.Option_Helpers


16:14:45 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString


16:14:45 Simple_Firewall: theory Simple_Firewall.List_Product_More


16:14:45 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString


16:14:45 Simple_Firewall: theory Simple_Firewall.Iface


16:14:46 Simple_Firewall: theory Simple_Firewall.L4_Protocol


16:14:53 Simple_Firewall: theory Simple_Firewall.Simple_Packet


16:14:53 Simple_Firewall: theory Simple_Firewall.Primitives_toString


16:14:56 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax


16:14:59 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString


16:14:59 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics


16:15:02 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw


16:15:02 Simple_Firewall: theory Simple_Firewall.Shadowed


16:15:02 Simple_Firewall: theory Simple_Firewall.Service_Matrix


16:15:40 Timing Simple_Firewall (8 threads, 28.145s elapsed time, 122.040s cpu time, 4.540s GC time, factor 4.34)


16:15:40 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall


16:15:40 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf


16:15:40 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf


16:15:40 Finished Simple_Firewall (0:00:56 elapsed time, 0:03:13 cpu time, factor 3.42)


16:15:40 Building Routing ...


16:15:42 Routing: theory Routing.Linorder_Helper


16:15:42 Routing: theory HOL-Library.Adhoc_Overloading


16:15:42 Routing: theory HOL-Library.Monad_Syntax


16:15:43 Routing: theory Routing.Routing_Table


16:15:49 Routing: theory Routing.IpRoute_Parser


16:15:49 Routing: theory Routing.Linux_Router


16:16:14 Timing Routing (8 threads, 13.867s elapsed time, 43.920s cpu time, 1.192s GC time, factor 3.17)


16:16:14 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing


16:16:14 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf


16:16:14 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf


16:16:14 Finished Routing (0:00:33 elapsed time, 0:01:23 cpu time, factor 2.50)


16:16:14 Building Iptables_Semantics ...


16:16:16 Iptables_Semantics: theory Iptables_Semantics.List_Misc


16:16:16 Iptables_Semantics: theory Iptables_Semantics.Negation_Type


16:16:18 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists


16:16:20 Iptables_Semantics: theory HOL-Library.Code_Target_Int


16:16:20 Iptables_Semantics: theory HOL-Library.LaTeXsugar


16:16:20 Iptables_Semantics: theory Iptables_Semantics.Ternary


16:16:20 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize


16:16:20 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev


16:16:20 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors


16:16:20 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF


16:16:20 Iptables_Semantics: theory Native_Word.More_Bits_Int


16:16:20 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State


16:16:20 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags


16:16:20 Iptables_Semantics: theory Iptables_Semantics.IpAddresses


16:16:20 Iptables_Semantics: theory Iptables_Semantics.Word_Upto


16:16:20 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common


16:16:22 Iptables_Semantics: theory Iptables_Semantics.Ports


16:16:23 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet


16:16:23 Iptables_Semantics: theory Native_Word.Bits_Integer


16:16:25 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax


16:16:45 Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int


16:16:47 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary


16:16:47 Iptables_Semantics: theory Iptables_Semantics.Semantics


16:16:47 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto


16:16:49 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics


16:16:50 Iptables_Semantics: theory Iptables_Semantics.Matching


16:16:50 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful


16:16:50 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update


16:16:50 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding


16:16:52 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary


16:16:52 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs


16:16:53 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings


16:16:54 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action


16:16:54 Iptables_Semantics: theory Iptables_Semantics.Optimizing


16:16:54 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic


16:16:55 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches


16:16:56 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching


16:16:59 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization


16:17:03 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher


16:17:05 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold


16:17:05 Iptables_Semantics: theory Iptables_Semantics.Ipassmt


16:17:11 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt


16:18:12 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas


16:18:12 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString


16:18:12 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform


16:18:12 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics


16:18:12 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize


16:18:12 Iptables_Semantics: theory Iptables_Semantics.No_Spoof


16:18:12 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize


16:18:12 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize


16:18:13 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize


16:18:24 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace


16:18:27 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace


16:18:36 Iptables_Semantics: theory Iptables_Semantics.Transform


16:18:44 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract


16:18:47 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance


16:18:56 Iptables_Semantics: theory Iptables_Semantics.Code_Interface


16:18:56 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings


16:18:57 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings


16:18:58 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics


16:18:58 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings


16:19:09 Iptables_Semantics: theory Iptables_Semantics.Parser


16:19:09 Iptables_Semantics: theory Iptables_Semantics.Documentation


16:19:10 Iptables_Semantics: theory Iptables_Semantics.Code_haskell


16:20:38 Timing Iptables_Semantics (8 threads, 203.454s elapsed time, 975.336s cpu time, 67.008s GC time, factor 4.79)


16:20:38 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics


16:20:38 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf


16:20:38 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf


16:20:38 Finished Iptables_Semantics (0:04:22 elapsed time, 0:19:42 cpu time, factor 4.51)


16:20:38 Building Iptables_Semantics_Examples ...


16:20:40 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com


16:20:40 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall


16:20:40 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing


16:20:40 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example


16:20:40 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company


16:20:40 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof


16:20:40 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test


16:20:40 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6


16:20:42 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test


16:20:49 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail


16:20:51 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples


16:20:51 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed


16:20:52 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation


16:28:08 Timing Iptables_Semantics_Examples (8 threads, 421.080s elapsed time, 2980.424s cpu time, 307.760s GC time, factor 7.08)


16:28:08 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples


16:28:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf


16:28:08 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf


16:28:08 Finished Iptables_Semantics_Examples (0:07:28 elapsed time, 0:50:37 cpu time, factor 6.77)


16:28:08 Running Iptables_Semantics_Examples_Big ...


16:28:10 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern


16:28:10 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small


16:28:10 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall


16:28:10 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3


16:28:10 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated


16:33:22 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large


18:29:16 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW


20:04:14 Timing Iptables_Semantics_Examples_Big (8 threads, 12956.588s elapsed time, 65398.088s cpu time, 21942.672s GC time, factor 5.05)


20:04:14 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big


20:04:14 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/document.pdf


20:04:14 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/outline.pdf


20:04:14 Finished Iptables_Semantics_Examples_Big (3:36:04 elapsed time, 18:10:26 cpu time, factor 5.05)


20:04:14 

20:04:14 === TIMING ===


20:04:14 

20:04:14 Group slow: 17:50:25 elapsed time, 61:01:30 cpu time, factor 3.42


20:04:14 Group AFP: 18:16:46 elapsed time, 63:02:22 cpu time, factor 3.45


20:04:14 Group main: 0:10:42 elapsed time, 0:42:00 cpu time, factor 3.92


20:04:14 Group timing: 0:04:01 elapsed time, 0:19:54 cpu time, factor 4.94


20:04:14 Group very_slow: 11:14:23 elapsed time, 29:35:16 cpu time, factor 2.63


20:04:14 Overall: 18:29:01 elapsed time, 63:44:55 cpu time, factor 3.45


20:04:14 Archiving artifacts


20:04:15 Started calculate disk usage of build


20:04:15 Finished Calculation of disk usage of build in 0 seconds


20:04:15 Started calculate disk usage of workspace


20:04:17 Finished Calculation of disk usage of workspace in  1 second


20:04:17 No emails were triggered.


20:04:17 Finished: SUCCESS