Console Output

01:33:09 Started by an SCM change
01:33:09 [EnvInject] - Loading node environment variables.
01:33:09 Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow
01:33:09 [isabelle-nightly-slow] $ hg showconfig paths.default
01:33:09 [isabelle-nightly-slow] $ hg pull --rev default
01:33:10 pulling from http://isabelle.in.tum.de/repos/isabelle/
01:33:10 no changes found
01:33:10 [isabelle-nightly-slow] $ hg update --clean --rev default
01:33:10 5 files updated, 0 files merged, 0 files removed, 0 files unresolved
01:33:10 [isabelle-nightly-slow] $ hg --config extensions.purge= clean --all
01:33:11 [isabelle-nightly-slow] $ hg log --rev . --template {node}
01:33:11 [isabelle-nightly-slow] $ hg log --rev . --template {rev}
01:33:11 [isabelle-nightly-slow] $ hg log --rev a7aba6db79a143c5a47e0cfadc01c50e155f6403 --template exists\n
01:33:11 exists
01:33:11 [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:11 [afp] $ hg showconfig paths.default
01:33:11 [afp] $ hg pull --rev default
01:33:12 pulling from https://bitbucket.org/isa-afp/afp-devel/
01:33:12 no changes found
01:33:12 [afp] $ hg update --clean --rev default
01:33:13 38 files updated, 0 files merged, 1 files removed, 0 files unresolved
01:33:13 [afp] $ hg --config extensions.purge= clean --all
01:33:13 [afp] $ hg log --rev . --template {node}
01:33:13 [afp] $ hg log --rev . --template {rev}
01:33:13 [afp] $ hg log --rev 69945e1330db22c0bfcf00d214e8dbbe3def71a9 --template exists\n
01:33:13 exists
01:33:13 [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(69945e1330db22c0bfcf00d214e8dbbe3def71a9)" --encoding UTF-8 --encodingmode replace
01:33:13 No emails were triggered.
01:33:13 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins7213610976666075591.sh
01:33:13 + Admin/jenkins/run_build slow
01:33:13 + set -e
01:33:13 + PROFILE=slow
01:33:13 + shift
01:33:13 + bin/isabelle components -a
01:33:13 + bin/isabelle jedit -bf
01:33:13 ### Building graph browser ...
01:33:14 warning: [options] bootstrap class path not set in conjunction with -source 6
01:33:14 warning: [options] source value 6 is obsolete and will be removed in a future release
01:33:14 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
01:33:15 Note: Some input files use or override a deprecated API.
01:33:15 Note: Recompile with -Xlint:deprecation for details.
01:33:15 Note: Some input files use unchecked or unsafe operations.
01:33:15 Note: Recompile with -Xlint:unchecked for details.
01:33:15 3 warnings
01:33:16 ### Building Isabelle/Scala ...
01:34:22 ### 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 Sun, 21 Apr 2019 01:35:12 +0200
01:35:13 Isabelle id ac1706cdde25
01:35:13 Build for AFP id 91971ca6ad5e
01:35:13 
01:35:13 === LOG ===
01:35:13 
01:35:16 Session Pure/Pure
01:35:17 Session FOL/FOL
01:35:17 Session HOL/HOL (main)
01:35:19 Session AFP/AWN (AFP)
01:35:19 Session AFP/AODV (AFP slow)
01:35:20 Session HOL/HOL-Eisbach
01:35:20 Session HOL/HOL-Library (main timing)
01:35:21 Session AFP/Binomial-Heaps (AFP)
01:35:21 Session AFP/ConcurrentIMP (AFP)
01:35:21 Session AFP/ConcurrentGC (AFP slow)
01:35:21 Session AFP/FinFun (AFP)
01:35:21 Session AFP/Finger-Trees (AFP)
01:35:21 Session HOL/HOL-Computational_Algebra (main timing)
01:35:21 Session HOL/HOL-Algebra (main timing)
01:35:22 Session HOL/HOL-Analysis (main timing)
01:35:23 Session AFP/Coinductive (AFP)
01:35:23 Session HOL/HOL-Number_Theory (main timing)
01:35:24 Session HOL/HOL-ex (timing)
01:35:24 Session AFP/Automatic_Refinement (AFP)
01:35:24 Session HOL/HOL-Imperative_HOL (timing)
01:35:25 Session AFP/Trie (AFP)
01:35:25 Session AFP/Flyspeck-Tame (AFP)
01:35:25 Session AFP/Flyspeck-Tame-Computation (AFP slow very_slow)
01:35:25 Session HOL/HOL-Word (main timing)
01:35:26 Session AFP/Native_Word (AFP)
01:35:26 Session AFP/Refine_Monadic (AFP)
01:35:26 Session AFP/Collections (AFP)
01:35:27 Session AFP/Word_Lib (AFP)
01:35:27 Session AFP/IP_Addresses (AFP)
01:35:28 Session AFP/Simple_Firewall (AFP)
01:35:28 Session AFP/Routing (AFP)
01:35:28 Session AFP/Iptables_Semantics (AFP)
01:35:29 Session AFP/Iptables_Semantics_Examples (AFP)
01:35:29 Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow)
01:35:29 Session AFP/JinjaThreads (AFP slow)
01:35:32 Building Pure ...
01:36:03 Pure: theory Pure
01:36:04 Pure: theory ML_Bootstrap
01:36:04 Pure: theory Pure.Sessions
01:36:07 Timing Pure (1 threads, 1.574s elapsed time, 1.576s cpu time, 0.000s GC time, factor 1.00)
01:36:07 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure
01:36:07 Finished Pure (0:00:33 elapsed time, 0:00:33 cpu time, factor 1.00)
01:36:07 Building HOL ...
01:36:12 HOL: theory HOL.Code_Generator
01:36:18 HOL: theory HOL.HOL
01:36:24 HOL: theory HOL.Argo
01:36:24 HOL: theory HOL.Ctr_Sugar
01:36:24 HOL: theory HOL.Orderings
01:36:26 HOL: theory HOL.Groups
01:36:27 HOL: theory HOL.SAT
01:36:30 HOL: theory HOL.Lattices
01:36:32 HOL: theory HOL.Set
01:36:34 HOL: theory HOL.Fun
01:36:34 HOL: theory HOL.Typedef
01:36:35 HOL: theory HOL.Complete_Lattices
01:36:35 HOL: theory HOL.Rings
01:36:39 HOL: theory HOL.Inductive
01:36:42 HOL: theory HOL.Product_Type
01:36:42 HOL: theory HOL.Sum_Type
01:36:44 HOL: theory HOL.Complete_Partial_Order
01:36:50 HOL: theory HOL.Nat
01:36:53 HOL: theory HOL.Fields
01:36:53 HOL: theory HOL.Meson
01:36:54 HOL: theory HOL.ATP
01:36:59 HOL: theory HOL.Metis
01:37:00 HOL: theory HOL.Finite_Set
01:37:03 HOL: theory HOL.Relation
01:37:05 HOL: theory HOL.Transitive_Closure
01:37:07 HOL: theory HOL.Wellfounded
01:37:08 HOL: theory HOL.Fun_Def_Base
01:37:08 HOL: theory HOL.Hilbert_Choice
01:37:08 HOL: theory HOL.Wfrec
01:37:08 HOL: theory HOL.Order_Relation
01:37:09 HOL: theory HOL.BNF_Wellorder_Relation
01:37:10 HOL: theory HOL.Zorn
01:37:10 HOL: theory HOL.BNF_Wellorder_Embedding
01:37:11 HOL: theory HOL.BNF_Wellorder_Constructions
01:37:12 HOL: theory HOL.BNF_Cardinal_Order_Relation
01:37:14 HOL: theory HOL.BNF_Cardinal_Arithmetic
01:37:15 HOL: theory HOL.BNF_Def
01:37:19 HOL: theory HOL.BNF_Composition
01:37:19 HOL: theory HOL.Basic_BNFs
01:37:21 HOL: theory HOL.BNF_Fixpoint_Base
01:37:26 HOL: theory HOL.BNF_Least_Fixpoint
01:37:31 HOL: theory HOL.Basic_BNF_LFPs
01:37:31 HOL: theory HOL.Transfer
01:37:33 HOL: theory HOL.Num
01:37:37 HOL: theory HOL.Power
01:37:41 HOL: theory HOL.Groups_Big
01:37:45 HOL: theory HOL.Equiv_Relations
01:37:46 HOL: theory HOL.Lifting
01:37:49 HOL: theory HOL.Lifting_Set
01:37:49 HOL: theory HOL.Option
01:37:49 HOL: theory HOL.Quotient
01:37:50 HOL: theory HOL.Extraction
01:37:50 HOL: theory HOL.Lattices_Big
01:37:50 HOL: theory HOL.Partial_Function
01:37:51 HOL: theory HOL.Fun_Def
01:37:55 HOL: theory HOL.Int
01:38:00 HOL: theory HOL.Euclidean_Division
01:38:08 HOL: theory HOL.Parity
01:38:14 HOL: theory HOL.Divides
01:38:18 HOL: theory HOL.Code_Numeral
01:38:18 HOL: theory HOL.Set_Interval
01:38:18 HOL: theory HOL.Numeral_Simprocs
01:38:18 HOL: theory HOL.SMT
01:38:21 HOL: theory HOL.Semiring_Normalization
01:38:26 HOL: theory HOL.Groebner_Basis
01:38:27 HOL: theory HOL.Conditionally_Complete_Lattices
01:38:27 HOL: theory HOL.Filter
01:38:28 HOL: theory HOL.Presburger
01:38:36 HOL: theory HOL.Sledgehammer
01:38:40 HOL: theory HOL.List
01:38:57 HOL: theory HOL.Groups_List
01:38:57 HOL: theory HOL.Map
01:38:59 HOL: theory HOL.Factorial
01:38:59 HOL: theory HOL.GCD
01:38:59 HOL: theory HOL.Enum
01:38:59 HOL: theory HOL.Random
01:39:02 HOL: theory HOL.Binomial
01:39:08 HOL: theory HOL.String
01:39:12 HOL: theory HOL.BNF_Greatest_Fixpoint
01:39:12 HOL: theory HOL.Predicate
01:39:12 HOL: theory HOL.Typerep
01:39:15 HOL: theory HOL.Lazy_Sequence
01:39:17 HOL: theory HOL.Limited_Sequence
01:39:18 HOL: theory HOL.Code_Evaluation
01:39:22 HOL: theory HOL.Quickcheck_Random
01:39:30 HOL: theory HOL.Random_Pred
01:39:30 HOL: theory HOL.Quickcheck_Exhaustive
01:39:30 HOL: theory HOL.Quickcheck_Narrowing
01:39:31 HOL: theory HOL.Random_Sequence
01:39:40 HOL: theory HOL.Record
01:39:40 HOL: theory HOL.Predicate_Compile
01:39:43 HOL: theory HOL.Nitpick
01:39:53 HOL: theory HOL.Nunchaku
01:39:54 HOL: theory Main
01:39:57 HOL: theory HOL.Archimedean_Field
01:39:57 HOL: theory HOL.Topological_Spaces
01:39:57 HOL: theory HOL.Hull
01:39:57 HOL: theory HOL.Modules
01:39:59 HOL: theory HOL.Vector_Spaces
01:40:12 HOL: theory HOL.Rat
01:40:18 HOL: theory HOL.Real
01:40:21 HOL: theory HOL.Real_Vector_Spaces
01:40:40 HOL: theory HOL.Inequalities
01:40:40 HOL: theory HOL.Limits
01:40:49 HOL: theory HOL.Deriv
01:40:49 HOL: theory HOL.Series
01:40:53 HOL: theory HOL.NthRoot
01:40:54 HOL: theory HOL.Transcendental
01:41:03 HOL: theory HOL.Complex
01:41:05 HOL: theory HOL.MacLaurin
01:41:05 HOL: theory Complex_Main
01:42:57 Timing HOL (8 threads, 308.904s elapsed time, 1133.400s cpu time, 111.496s GC time, factor 3.67)
01:42:57 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL
01:42:57 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf
01:42:57 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf
01:42:57 Finished HOL (0:06:45 elapsed time, 0:22:11 cpu time, factor 3.28)
01:42:57 Running JinjaThreads ...
01:43:00 JinjaThreads: theory HOL-Eisbach.Eisbach
01:43:00 JinjaThreads: theory Automatic_Refinement.Prio_List
01:43:00 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1
01:43:00 JinjaThreads: theory Collections.ICF_Tools
01:43:00 JinjaThreads: theory Automatic_Refinement.Foldi
01:43:00 JinjaThreads: theory HOL-Library.AList
01:43:00 JinjaThreads: theory Finger-Trees.FingerTree
01:43:00 JinjaThreads: theory HOL-Library.Adhoc_Overloading
01:43:00 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot
01:43:00 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot
01:43:00 JinjaThreads: theory HOL-Library.Monad_Syntax
01:43:00 JinjaThreads: theory Collections.Ord_Code_Preproc
01:43:00 JinjaThreads: theory HOL-Library.Bit
01:43:00 JinjaThreads: theory HOL-Library.Boolean_Algebra
01:43:01 JinjaThreads: theory HOL-Library.Cancellation
01:43:01 JinjaThreads: theory Collections.Locale_Code
01:43:01 JinjaThreads: theory Automatic_Refinement.Refine_Util
01:43:01 JinjaThreads: theory Collections.Record_Intf
01:43:01 JinjaThreads: theory HOL-Library.Case_Converter
01:43:01 JinjaThreads: theory HOL-Library.Code_Abstract_Nat
01:43:01 JinjaThreads: theory HOL-Library.Code_Target_Nat
01:43:02 JinjaThreads: theory HOL-Library.Simps_Case_Conv
01:43:02 JinjaThreads: theory HOL-Library.Code_Target_Int
01:43:02 JinjaThreads: theory HOL-Library.Dlist
01:43:02 JinjaThreads: theory Automatic_Refinement.Anti_Unification
01:43:02 JinjaThreads: theory Automatic_Refinement.Attr_Comb
01:43:02 JinjaThreads: theory Automatic_Refinement.Autoref_Data
01:43:02 JinjaThreads: theory Automatic_Refinement.Indep_Vars
01:43:02 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp
01:43:02 JinjaThreads: theory Automatic_Refinement.Tagged_Solver
01:43:02 JinjaThreads: theory Automatic_Refinement.Select_Solve
01:43:02 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms
01:43:02 JinjaThreads: theory HOL-Library.Multiset
01:43:02 JinjaThreads: theory HOL-Library.Code_Target_Numeral
01:43:02 JinjaThreads: theory HOL-Library.Infinite_Set
01:43:02 JinjaThreads: theory HOL-Library.Lattice_Syntax
01:43:02 JinjaThreads: theory HOL-Library.Complete_Partial_Order2
01:43:03 JinjaThreads: theory HOL-Library.Nat_Bijection
01:43:03 JinjaThreads: theory HOL-Library.Old_Datatype
01:43:03 JinjaThreads: theory HOL-Library.Option_ord
01:43:03 JinjaThreads: theory HOL-Library.Phantom_Type
01:43:04 JinjaThreads: theory Trie.Trie
01:43:04 JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs
01:43:04 JinjaThreads: theory HOL-Library.RBT_Impl
01:43:04 JinjaThreads: theory HOL-Library.Sublist
01:43:04 JinjaThreads: theory HOL-Library.Transitive_Closure_Table
01:43:05 JinjaThreads: theory HOL-Library.Cardinality
01:43:05 JinjaThreads: theory HOL-Library.While_Combinator
01:43:06 JinjaThreads: theory Collections.DatRef
01:43:07 JinjaThreads: theory HOL-Word.Bit_Representation
01:43:07 JinjaThreads: theory HOL-Word.Bits
01:43:08 JinjaThreads: theory HOL-Word.Bits_Bit
01:43:09 JinjaThreads: theory FinFun.FinFun
01:43:09 JinjaThreads: theory HOL-Library.Numeral_Type
01:43:09 JinjaThreads: theory HOL-Word.Misc_Typedef
01:43:10 JinjaThreads: theory HOL-Library.Countable
01:43:10 JinjaThreads: theory JinjaThreads.Set_Monad
01:43:10 JinjaThreads: theory JinjaThreads.Set_without_equal
01:43:10 JinjaThreads: theory Refine_Monadic.Refine_Chapter
01:43:11 JinjaThreads: theory HOL-Word.Bool_List_Representation
01:43:11 JinjaThreads: theory HOL-Word.Misc_Arithmetic
01:43:12 JinjaThreads: theory HOL-Library.Type_Length
01:43:12 JinjaThreads: theory HOL-Word.Bits_Int
01:43:13 JinjaThreads: theory HOL-Library.Countable_Set
01:43:13 JinjaThreads: theory Binomial-Heaps.BinomialHeap
01:43:14 JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap
01:43:14 JinjaThreads: theory HOL-ex.Quicksort
01:43:15 JinjaThreads: theory Native_Word.More_Bits_Int
01:43:15 JinjaThreads: theory HOL-Word.Word
01:43:15 JinjaThreads: theory Automatic_Refinement.Misc
01:43:15 JinjaThreads: theory HOL-Library.Countable_Complete_Lattices
01:43:17 JinjaThreads: theory Native_Word.Code_Symbolic_Bits_Int
01:43:18 JinjaThreads: theory Native_Word.Bits_Integer
01:43:19 JinjaThreads: theory HOL-Library.Order_Continuity
01:43:20 JinjaThreads: theory JinjaThreads.Auxiliary
01:43:20 JinjaThreads: theory HOL-Library.Extended_Nat
01:43:22 JinjaThreads: theory Coinductive.Coinductive_Nat
01:43:27 JinjaThreads: theory Coinductive.Coinductive_List
01:43:29 JinjaThreads: theory Automatic_Refinement.Refine_Lib
01:43:30 JinjaThreads: theory Collections.SetIterator
01:43:30 JinjaThreads: theory Collections.Sorted_List_Operations
01:43:32 JinjaThreads: theory Automatic_Refinement.Autoref_Phases
01:43:32 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging
01:43:32 JinjaThreads: theory Automatic_Refinement.Relators
01:43:32 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover
01:43:33 JinjaThreads: theory Collections.SetIteratorOperations
01:43:35 JinjaThreads: theory Automatic_Refinement.Param_Tool
01:43:36 JinjaThreads: theory Automatic_Refinement.Param_HOL
01:43:38 JinjaThreads: theory Collections.Assoc_List
01:43:38 JinjaThreads: theory Collections.Dlist_add
01:43:38 JinjaThreads: theory Collections.Proper_Iterator
01:43:39 JinjaThreads: theory Collections.SetIteratorGA
01:43:40 JinjaThreads: theory Automatic_Refinement.Parametricity
01:43:40 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops
01:43:40 JinjaThreads: theory Collections.Diff_Array
01:43:40 JinjaThreads: theory Collections.Trie_Impl
01:43:41 JinjaThreads: theory Collections.It_to_It
01:43:43 JinjaThreads: theory Collections.Trie2
01:43:43 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel
01:43:45 JinjaThreads: theory Automatic_Refinement.Autoref_Translate
01:43:45 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface
01:43:45 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo
01:43:45 JinjaThreads: theory Automatic_Refinement.Autoref_Tool
01:43:46 JinjaThreads: theory Coinductive.Lazy_LList
01:43:47 JinjaThreads: theory Coinductive.TLList
01:43:47 JinjaThreads: theory Native_Word.Code_Target_Bits_Int
01:43:47 JinjaThreads: theory Native_Word.Code_Target_Word_Base
01:43:47 JinjaThreads: theory Collections.Code_Target_ICF
01:43:48 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL
01:43:50 JinjaThreads: theory Native_Word.Uint32
01:43:54 JinjaThreads: theory Coinductive.Lazy_TLList
01:43:55 JinjaThreads: theory Collections.HashCode
01:43:57 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement
01:43:57 JinjaThreads: theory Collections.Idx_Iterator
01:43:57 JinjaThreads: theory Refine_Monadic.Refine_Misc
01:43:59 JinjaThreads: theory Refine_Monadic.RefineG_Domain
01:43:59 JinjaThreads: theory Refine_Monadic.RefineG_Transfer
01:43:59 JinjaThreads: theory Refine_Monadic.RefineG_Assert
01:44:00 JinjaThreads: theory Refine_Monadic.RefineG_Recursion
01:44:01 JinjaThreads: theory Refine_Monadic.RefineG_While
01:44:01 JinjaThreads: theory Refine_Monadic.Refine_Basic
01:44:02 JinjaThreads: theory Refine_Monadic.Refine_Det
01:44:08 JinjaThreads: theory Refine_Monadic.Refine_Heuristics
01:44:08 JinjaThreads: theory Refine_Monadic.Refine_Leof
01:44:08 JinjaThreads: theory Refine_Monadic.Refine_Pfun
01:44:09 JinjaThreads: theory Refine_Monadic.Refine_More_Comb
01:44:09 JinjaThreads: theory Refine_Monadic.Refine_While
01:44:12 JinjaThreads: theory Refine_Monadic.Refine_Transfer
01:44:13 JinjaThreads: theory Refine_Monadic.Autoref_Monadic
01:44:13 JinjaThreads: theory Refine_Monadic.Refine_Automation
01:44:13 JinjaThreads: theory Refine_Monadic.Refine_Foreach
01:44:18 JinjaThreads: theory Refine_Monadic.Refine_Monadic
01:44:20 JinjaThreads: theory Collections.Gen_Iterator
01:44:20 JinjaThreads: theory Collections.Intf_Map
01:44:20 JinjaThreads: theory Collections.Intf_Set
01:44:21 JinjaThreads: theory Collections.Iterator
01:44:22 JinjaThreads: theory Collections.Array_Iterator
01:44:22 JinjaThreads: theory Collections.ICF_Spec_Base
01:44:23 JinjaThreads: theory Collections.AnnotatedListSpec
01:44:23 JinjaThreads: theory Collections.ListSpec
01:44:23 JinjaThreads: theory Collections.PrioSpec
01:44:23 JinjaThreads: theory Collections.MapSpec
01:44:23 JinjaThreads: theory Collections.PrioUniqueSpec
01:44:24 JinjaThreads: theory Collections.SetSpec
01:44:25 JinjaThreads: theory Collections.BinoPrioImpl
01:44:25 JinjaThreads: theory Collections.SkewPrioImpl
01:44:27 JinjaThreads: theory Collections.ListGA
01:44:27 JinjaThreads: theory Collections.FTAnnotatedListImpl
01:44:28 JinjaThreads: theory Collections.PrioByAnnotatedList
01:44:28 JinjaThreads: theory Collections.Fifo
01:44:33 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList
01:44:34 JinjaThreads: theory HOL-Library.RBT
01:44:34 JinjaThreads: theory Collections.RBT_add
01:44:34 JinjaThreads: theory Collections.Algos
01:44:35 JinjaThreads: theory Collections.SetIndex
01:44:37 JinjaThreads: theory Collections.SetIteratorCollectionsGA
01:44:38 JinjaThreads: theory Collections.MapGA
01:44:38 JinjaThreads: theory Collections.SetGA
01:44:39 JinjaThreads: theory Collections.FTPrioImpl
01:44:40 JinjaThreads: theory Collections.FTPrioUniqueImpl
01:44:43 JinjaThreads: theory Collections.ArrayMapImpl
01:44:43 JinjaThreads: theory Collections.ListMapImpl
01:44:44 JinjaThreads: theory Collections.ListMapImpl_Invar
01:44:44 JinjaThreads: theory Collections.TrieMapImpl
01:44:44 JinjaThreads: theory Collections.RBTMapImpl
01:44:50 JinjaThreads: theory Collections.ListSetImpl
01:44:50 JinjaThreads: theory Collections.ListSetImpl_Invar
01:44:51 JinjaThreads: theory Collections.ListSetImpl_NotDist
01:44:54 JinjaThreads: theory Collections.ArrayHashMap_Impl
01:44:55 JinjaThreads: theory Collections.ListSetImpl_Sorted
01:44:58 JinjaThreads: theory Collections.SetByMap
01:45:01 JinjaThreads: theory Collections.HashMap_Impl
01:45:04 JinjaThreads: theory Collections.ArraySetImpl
01:45:04 JinjaThreads: theory Collections.TrieSetImpl
01:45:05 JinjaThreads: theory Collections.RBTSetImpl
01:45:05 JinjaThreads: theory Collections.ArrayHashMap
01:45:06 JinjaThreads: theory Collections.HashMap
01:45:19 JinjaThreads: theory Collections.ArrayHashSet
01:45:20 JinjaThreads: theory Collections.HashSet
01:45:20 JinjaThreads: theory Collections.MapStdImpl
01:45:32 JinjaThreads: theory Collections.SetStdImpl
01:45:38 JinjaThreads: theory Collections.ICF_Impl
01:45:47 JinjaThreads: theory Collections.ICF_Refine_Monadic
01:45:48 JinjaThreads: theory Collections.ICF_Autoref
01:45:54 JinjaThreads: theory Collections.Collections
01:45:55 JinjaThreads: theory Collections.CollectionsV1
01:46:07 JinjaThreads: theory JinjaThreads.JT_ICF
01:46:07 JinjaThreads: theory JinjaThreads.Basic_Main
01:46:59 JinjaThreads: theory HOL-Library.Mapping
01:46:59 JinjaThreads: theory HOL-Library.Prefix_Order
01:46:59 JinjaThreads: theory JinjaThreads.FWState
01:46:59 JinjaThreads: theory JinjaThreads.LTS
01:46:59 JinjaThreads: theory JinjaThreads.Type
01:46:59 JinjaThreads: theory JinjaThreads.ListIndex
01:46:59 JinjaThreads: theory JinjaThreads.Orders
01:46:59 JinjaThreads: theory JinjaThreads.Semilat
01:47:00 JinjaThreads: theory JinjaThreads.Err
01:47:01 JinjaThreads: theory HOL-Library.AList_Mapping
01:47:02 JinjaThreads: theory JinjaThreads.Listn
01:47:02 JinjaThreads: theory JinjaThreads.Opt
01:47:02 JinjaThreads: theory JinjaThreads.Product
01:47:03 JinjaThreads: theory JinjaThreads.Semilattices
01:47:03 JinjaThreads: theory JinjaThreads.Typing_Framework
01:47:04 JinjaThreads: theory JinjaThreads.SemilatAlg
01:47:04 JinjaThreads: theory JinjaThreads.Decl
01:47:04 JinjaThreads: theory JinjaThreads.Kildall
01:47:04 JinjaThreads: theory JinjaThreads.LBVSpec
01:47:05 JinjaThreads: theory JinjaThreads.Bisimulation
01:47:05 JinjaThreads: theory JinjaThreads.Typing_Framework_err
01:47:05 JinjaThreads: theory JinjaThreads.LBVComplete
01:47:05 JinjaThreads: theory JinjaThreads.LBVCorrect
01:47:07 JinjaThreads: theory JinjaThreads.Abstract_BV
01:47:08 JinjaThreads: theory JinjaThreads.TypeRel
01:47:14 JinjaThreads: theory JinjaThreads.TypeRelRefine
01:47:14 JinjaThreads: theory JinjaThreads.Value
01:47:20 JinjaThreads: theory JinjaThreads.Exceptions
01:47:20 JinjaThreads: theory JinjaThreads.Heap
01:47:21 JinjaThreads: theory JinjaThreads.SystemClasses
01:47:23 JinjaThreads: theory JinjaThreads.MM
01:47:23 JinjaThreads: theory JinjaThreads.State
01:47:33 JinjaThreads: theory JinjaThreads.FWCondAction
01:47:33 JinjaThreads: theory JinjaThreads.FWInterrupt
01:47:33 JinjaThreads: theory JinjaThreads.FWLock
01:47:33 JinjaThreads: theory JinjaThreads.FWThread
01:47:33 JinjaThreads: theory JinjaThreads.Observable_Events
01:47:33 JinjaThreads: theory JinjaThreads.FWWait
01:47:36 JinjaThreads: theory JinjaThreads.FWLocking
01:47:37 JinjaThreads: theory JinjaThreads.FWLockingThread
01:47:37 JinjaThreads: theory JinjaThreads.FWWellform
01:47:39 JinjaThreads: theory JinjaThreads.FWLifting
01:47:39 JinjaThreads: theory JinjaThreads.FWSemantics
01:47:42 JinjaThreads: theory JinjaThreads.JVMState
01:47:42 JinjaThreads: theory JinjaThreads.JMM_Spec
01:47:42 JinjaThreads: theory JinjaThreads.StartConfig
01:47:42 JinjaThreads: theory JinjaThreads.FWLiftingSem
01:47:42 JinjaThreads: theory JinjaThreads.FWProgressAux
01:47:44 JinjaThreads: theory JinjaThreads.Conform
01:47:44 JinjaThreads: theory JinjaThreads.FWDeadlock
01:47:44 JinjaThreads: theory JinjaThreads.FWLTS
01:47:44 JinjaThreads: theory JinjaThreads.State_Refinement
01:47:47 JinjaThreads: theory JinjaThreads.ConformThreaded
01:47:49 JinjaThreads: theory JinjaThreads.FWProgress
01:47:49 JinjaThreads: theory JinjaThreads.ExternalCall
01:47:50 JinjaThreads: theory JinjaThreads.SC
01:47:50 JinjaThreads: theory JinjaThreads.SC_Collections
01:47:59 JinjaThreads: theory JinjaThreads.FWBisimulation
01:47:59 JinjaThreads: theory JinjaThreads.FWInitFinLift
01:48:00 JinjaThreads: theory JinjaThreads.Scheduler
01:48:00 JinjaThreads: theory JinjaThreads.JMM_DRF
01:48:01 JinjaThreads: theory JinjaThreads.Non_Speculative
01:48:01 JinjaThreads: theory JinjaThreads.SC_Legal
01:48:05 JinjaThreads: theory JinjaThreads.HB_Completion
01:48:05 JinjaThreads: theory JinjaThreads.SC_Completion
01:48:43 JinjaThreads: theory JinjaThreads.WellForm
01:48:43 JinjaThreads: theory JinjaThreads.ExternalCall_Execute
01:48:48 JinjaThreads: theory JinjaThreads.BinOp
01:48:48 JinjaThreads: theory JinjaThreads.ExternalCallWF
01:48:48 JinjaThreads: theory JinjaThreads.JMM_Heap
01:48:48 JinjaThreads: theory JinjaThreads.SemiType
01:48:53 JinjaThreads: theory JinjaThreads.JVM_SemiType
01:48:55 JinjaThreads: theory JinjaThreads.Random_Scheduler
01:48:55 JinjaThreads: theory JinjaThreads.Round_Robin
01:48:57 JinjaThreads: theory JinjaThreads.JMM_Framework
01:48:59 JinjaThreads: theory JinjaThreads.JMM_Type
01:49:05 JinjaThreads: theory JinjaThreads.JMM_Type2
01:49:19 JinjaThreads: theory JinjaThreads.SC_Schedulers
01:49:49 JinjaThreads: theory JinjaThreads.Expr
01:49:50 JinjaThreads: theory JinjaThreads.JVMInstructions
01:49:50 JinjaThreads: theory JinjaThreads.PCompiler
01:49:53 JinjaThreads: theory JinjaThreads.PCompilerRefine
01:50:09 JinjaThreads: theory JinjaThreads.JVMExceptions
01:50:09 JinjaThreads: theory JinjaThreads.JVMHeap
01:50:09 JinjaThreads: theory JinjaThreads.Effect
01:50:19 JinjaThreads: theory JinjaThreads.JVMExecInstr
01:50:24 JinjaThreads: theory JinjaThreads.CallExpr
01:50:24 JinjaThreads: theory JinjaThreads.DefAss
01:50:26 JinjaThreads: theory JinjaThreads.WWellForm
01:50:26 JinjaThreads: theory JinjaThreads.JHeap
01:50:26 JinjaThreads: theory JinjaThreads.WellType
01:50:26 JinjaThreads: theory JinjaThreads.JVMExec
01:50:30 JinjaThreads: theory JinjaThreads.ToString
01:50:31 JinjaThreads: theory JinjaThreads.JVMDefensive
01:50:35 JinjaThreads: theory JinjaThreads.J1State
01:50:36 JinjaThreads: theory JinjaThreads.JMM_Typesafe
01:50:36 JinjaThreads: theory JinjaThreads.Annotate
01:50:36 JinjaThreads: theory JinjaThreads.SmallStep
01:50:40 JinjaThreads: theory JinjaThreads.Compiler2
01:50:40 JinjaThreads: theory JinjaThreads.JVMThreaded
01:50:45 JinjaThreads: theory JinjaThreads.J1Heap
01:50:54 JinjaThreads: theory JinjaThreads.Compiler1
01:50:56 JinjaThreads: theory JinjaThreads.JMM_Common
01:50:59 JinjaThreads: theory JinjaThreads.Exception_Tables
01:51:00 JinjaThreads: theory JinjaThreads.JVM_Main
01:51:00 JinjaThreads: theory JinjaThreads.JMM_JVM
01:51:01 JinjaThreads: theory JinjaThreads.J1WellType
01:51:03 JinjaThreads: theory JinjaThreads.Compiler
01:51:04 JinjaThreads: theory JinjaThreads.JWellForm
01:51:04 JinjaThreads: theory JinjaThreads.WellTypeRT
01:51:07 JinjaThreads: theory JinjaThreads.Preprocessor
01:51:08 JinjaThreads: theory JinjaThreads.J1WellForm
01:51:08 JinjaThreads: theory JinjaThreads.JMM_Typesafe2
01:51:10 JinjaThreads: theory JinjaThreads.JVMExec_Execute
01:51:10 JinjaThreads: theory JinjaThreads.JJ1WellForm
01:51:11 JinjaThreads: theory JinjaThreads.FWBisimDeadlock
01:51:12 JinjaThreads: theory JinjaThreads.FWBisimLift
01:51:13 JinjaThreads: theory JinjaThreads.J1
01:51:54 JinjaThreads: theory JinjaThreads.BVSpec
01:51:54 JinjaThreads: theory JinjaThreads.BVConform
01:51:55 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:06 JinjaThreads: theory JinjaThreads.Common_Main
01:52:06 JinjaThreads: theory JinjaThreads.LBVJVM
01:52:09 JinjaThreads: theory JinjaThreads.BVSpecTypeSafe
01:52:22 JinjaThreads: theory JinjaThreads.J1Deadlock
01:52:24 JinjaThreads: theory JinjaThreads.BVNoTypeError
01:52:28 JinjaThreads: theory JinjaThreads.BVProgressThreaded
01:52:29 JinjaThreads: theory JinjaThreads.BCVExec
01:52:31 JinjaThreads: theory JinjaThreads.JVMExec_Execute2
01:52:33 JinjaThreads: theory JinjaThreads.JVMTau
01:53:16 JinjaThreads: theory JinjaThreads.Execs
01:54:12 JinjaThreads: theory JinjaThreads.DefAssPreservation
01:54:12 JinjaThreads: theory JinjaThreads.Threaded
01:54:12 JinjaThreads: theory JinjaThreads.Progress
01:54:21 JinjaThreads: theory JinjaThreads.TypeSafe
01:54:35 JinjaThreads: theory JinjaThreads.J1JVMBisim
01:54:50 JinjaThreads: theory JinjaThreads.J0
01:54:50 JinjaThreads: theory JinjaThreads.DRF_JVM
01:54:52 JinjaThreads: theory JinjaThreads.JVMDeadlocked
01:54:52 JinjaThreads: theory JinjaThreads.JMM_J
01:54:52 JinjaThreads: theory JinjaThreads.ProgressThreaded
01:54:52 JinjaThreads: theory JinjaThreads.JVM_Execute
01:54:58 JinjaThreads: theory JinjaThreads.JVM_Execute2
01:55:16 JinjaThreads: theory JinjaThreads.J_Execute
01:56:04 JinjaThreads: theory JinjaThreads.Code_Generation
01:56:07 JinjaThreads: theory JinjaThreads.BV_Main
01:56:37 JinjaThreads: theory JinjaThreads.DRF_J
01:56:38 JinjaThreads: theory JinjaThreads.Deadlocked
01:56:45 JinjaThreads: theory JinjaThreads.ApprenticeChallenge
01:56:48 JinjaThreads: theory JinjaThreads.BufferExample
01:56:53 JinjaThreads: theory JinjaThreads.J_Main
01:56:54 JinjaThreads: theory JinjaThreads.J0Bisim
01:56:54 JinjaThreads: theory JinjaThreads.J0J1Bisim
01:56:54 JinjaThreads: theory JinjaThreads.Java2Jinja
01:57:07 JinjaThreads: theory JinjaThreads.Examples_Main
01:57:45 JinjaThreads: theory JinjaThreads.Correctness1
01:57:50 JinjaThreads: theory JinjaThreads.Correctness1Threaded
02:01:02 JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe
02:07:59 JinjaThreads: theory JinjaThreads.Execute_Main
02:08:43 JinjaThreads: theory JinjaThreads.JMM_J_Typesafe
02:09:01 JinjaThreads: theory JinjaThreads.J1JVM
02:09:02 JinjaThreads: theory JinjaThreads.JVMJ1
02:10:59 JinjaThreads: theory JinjaThreads.Correctness2
02:13:43 JinjaThreads: theory JinjaThreads.Correctness
02:24:36 JinjaThreads: theory JinjaThreads.Compiler_Main
02:24:37 JinjaThreads: theory JinjaThreads.JMM_Compiler
02:24:37 JinjaThreads: theory JinjaThreads.SC_Interp
02:33:09 JinjaThreads: theory JinjaThreads.JMM_Interp
02:33:19 JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2
02:33:24 JinjaThreads: theory JinjaThreads.JMM
02:33:31 JinjaThreads: theory JinjaThreads.MM_Main
02:33:54 JinjaThreads: theory JinjaThreads.JinjaThreads
02:48:26 Timing JinjaThreads (8 threads, 3863.513s elapsed time, 18311.164s cpu time, 6141.516s GC time, factor 4.74)
02:48:26 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads
02:48:26 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf
02:48:26 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf
02:48:26 Finished JinjaThreads (1:05:25 elapsed time, 5:12:57 cpu time, factor 4.78)
02:48:26 Building Flyspeck-Tame ...
02:48:27 Flyspeck-Tame: theory Flyspeck-Tame.ListAux
02:48:27 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order
02:48:27 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl
02:48:27 Flyspeck-Tame: theory HOL-Library.AList
02:48:27 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat
02:48:27 Flyspeck-Tame: theory HOL-Library.Code_Target_Int
02:48:27 Flyspeck-Tame: theory HOL-Library.IArray
02:48:27 Flyspeck-Tame: theory HOL-Library.While_Combinator
02:48:27 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso
02:48:27 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat
02:48:28 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral
02:48:28 Flyspeck-Tame: theory Flyspeck-Tame.Arch
02:48:28 Flyspeck-Tame: theory Flyspeck-Tame.Worklist
02:48:29 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax
02:48:29 Flyspeck-Tame: theory Flyspeck-Tame.ListSum
02:48:29 Flyspeck-Tame: theory Flyspeck-Tame.Rotation
02:48:30 Flyspeck-Tame: theory Flyspeck-Tame.Graph
02:48:30 Flyspeck-Tame: theory Flyspeck-Tame.Maps
02:48:31 Flyspeck-Tame: theory Trie.Trie
02:48:34 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision
02:48:34 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps
02:48:34 Flyspeck-Tame: theory Flyspeck-Tame.Tame
02:48:34 Flyspeck-Tame: theory Trie.Tries
02:48:36 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator
02:48:36 Flyspeck-Tame: theory Flyspeck-Tame.TameProps
02:48:37 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps
02:48:37 Flyspeck-Tame: theory Flyspeck-Tame.Plane
02:48:38 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps
02:48:38 Flyspeck-Tame: theory Flyspeck-Tame.Plane1
02:48:38 Flyspeck-Tame: theory Flyspeck-Tame.Generator
02:48:39 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum
02:48:47 Flyspeck-Tame: theory Flyspeck-Tame.Invariants
02:48:50 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps
02:48:50 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux
02:48:50 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps
02:48:51 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props
02:48:52 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound
02:48:52 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps
02:48:53 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps
02:48:53 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps
02:48:54 Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness
02:51:10 Timing Flyspeck-Tame (8 threads, 110.391s elapsed time, 623.584s cpu time, 48.964s GC time, factor 5.65)
02:51:10 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame
02:51:10 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf
02:51:10 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf
02:51:10 Finished Flyspeck-Tame (0:02:42 elapsed time, 0:12:24 cpu time, factor 4.57)
02:51:10 Running Flyspeck-Tame-Computation ...
02:51:12 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.ArchComp
02:51:12 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.Completeness
10:35:38 Timing Flyspeck-Tame-Computation (8 threads, 27856.223s elapsed time, 41379.708s cpu time, 3164.520s GC time, factor 1.49)
10:35:38 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame-Computation
10:35:38 Finished Flyspeck-Tame-Computation (7:44:17 elapsed time, 11:29:41 cpu time, factor 1.49)
10:35:38 Building AWN ...
10:35:39 AWN: theory AWN.Lib
10:35:39 AWN: theory AWN.TransitionSystems
10:35:39 AWN: theory AWN.AWN
10:35:40 AWN: theory AWN.Invariants
10:35:41 AWN: theory AWN.OInvariants
10:35:54 AWN: theory AWN.AWN_Cterms
10:35:54 AWN: theory AWN.AWN_SOS
10:35:54 AWN: theory AWN.OAWN_SOS
10:36:00 AWN: theory AWN.AWN_Labels
10:36:02 AWN: theory AWN.Pnet
10:36:02 AWN: theory AWN.Inv_Cterms
10:36:02 AWN: theory AWN.AWN_Invariants
10:36:03 AWN: theory AWN.Closed
10:36:04 AWN: theory AWN.AWN_SOS_Labels
10:36:05 AWN: theory AWN.Qmsg
10:36:06 AWN: theory AWN.OAWN_Invariants
10:36:06 AWN: theory AWN.OAWN_SOS_Labels
10:36:06 AWN: theory AWN.ONode_Lifting
10:36:06 AWN: theory AWN.OPnet
10:36:07 AWN: theory AWN.OPnet_Lifting
10:36:08 AWN: theory AWN.OClosed_Lifting
10:36:08 AWN: theory AWN.OClosed_Transfer
10:36:09 AWN: theory AWN.OAWN_Convert
10:36:09 AWN: theory AWN.Qmsg_Lifting
10:36:10 AWN: theory AWN.AWN_Main
10:36:11 AWN: theory AWN.Toy
10:36:30 AWN: theory AWN.AWN_Term_Graph
10:37:06 Timing AWN (8 threads, 56.144s elapsed time, 296.608s cpu time, 9.272s GC time, factor 5.28)
10:37:06 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN
10:37:06 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf
10:37:06 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf
10:37:06 Finished AWN (0:01:27 elapsed time, 0:06:07 cpu time, factor 4.20)
10:37:06 Running AODV ...
10:37:07 AODV: theory AODV.Aodv_Basic
10:37:09 AODV: theory AODV.A_Norreqid
10:37:09 AODV: theory AODV.Aodv_Data
10:37:09 AODV: theory AODV.Aodv_Message
10:37:09 AODV: theory AODV.B_Fwdrreps
10:37:09 AODV: theory AODV.C_Gtobcast
10:37:09 AODV: theory AODV.D_Fwdrreqs
10:37:09 AODV: theory AODV.E_All_ABCD
10:37:10 AODV: theory AODV.A_Aodv_Data
10:37:10 AODV: theory AODV.A_Aodv_Message
10:37:10 AODV: theory AODV.D_Aodv_Data
10:37:10 AODV: theory AODV.D_Aodv_Message
10:37:10 AODV: theory AODV.B_Aodv_Data
10:37:10 AODV: theory AODV.B_Aodv_Message
10:37:12 AODV: theory AODV.A_Fresher
10:37:12 AODV: theory AODV.C_Aodv_Data
10:37:12 AODV: theory AODV.Fresher
10:37:12 AODV: theory AODV.B_Fresher
10:37:12 AODV: theory AODV.C_Aodv_Message
10:37:12 AODV: theory AODV.D_Fresher
10:37:13 AODV: theory AODV.E_Aodv_Data
10:37:13 AODV: theory AODV.E_Aodv_Message
10:37:13 AODV: theory AODV.A_Aodv
10:37:14 AODV: theory AODV.Aodv
10:37:14 AODV: theory AODV.B_Aodv
10:37:14 AODV: theory AODV.D_Aodv
10:37:14 AODV: theory AODV.C_Fresher
10:37:14 AODV: theory AODV.E_Fresher
10:37:15 AODV: theory AODV.C_Aodv
10:37:15 AODV: theory AODV.E_Aodv
10:38:49 AODV: theory AODV.Aodv_Predicates
10:38:50 AODV: theory AODV.Loop_Freedom
10:38:50 AODV: theory AODV.Quality_Increases
10:38:51 AODV: theory AODV.Seq_Invariants
10:38:51 AODV: theory AODV.OAodv
10:38:52 AODV: theory AODV.Global_Invariants
10:38:53 AODV: theory AODV.Aodv_Loop_Freedom
10:39:09 AODV: theory AODV.A_Aodv_Predicates
10:39:09 AODV: theory AODV.A_OAodv
10:39:09 AODV: theory AODV.A_Loop_Freedom
10:39:10 AODV: theory AODV.A_Quality_Increases
10:39:10 AODV: theory AODV.A_Seq_Invariants
10:39:11 AODV: theory AODV.A_Global_Invariants
10:39:12 AODV: theory AODV.A_Aodv_Loop_Freedom
10:39:26 AODV: theory AODV.D_Aodv_Predicates
10:39:26 AODV: theory AODV.D_OAodv
10:39:27 AODV: theory AODV.D_Loop_Freedom
10:39:27 AODV: theory AODV.C_Aodv_Predicates
10:39:27 AODV: theory AODV.D_Quality_Increases
10:39:27 AODV: theory AODV.C_Loop_Freedom
10:39:27 AODV: theory AODV.C_Quality_Increases
10:39:27 AODV: theory AODV.B_Aodv_Predicates
10:39:28 AODV: theory AODV.C_Seq_Invariants
10:39:28 AODV: theory AODV.D_Seq_Invariants
10:39:28 AODV: theory AODV.B_Loop_Freedom
10:39:28 AODV: theory AODV.B_Quality_Increases
10:39:28 AODV: theory AODV.B_Seq_Invariants
10:39:28 AODV: theory AODV.B_OAodv
10:39:28 AODV: theory AODV.C_OAodv
10:39:28 AODV: theory AODV.E_Aodv_Predicates
10:39:28 AODV: theory AODV.E_OAodv
10:39:29 AODV: theory AODV.E_Loop_Freedom
10:39:29 AODV: theory AODV.E_Quality_Increases
10:39:29 AODV: theory AODV.E_Seq_Invariants
10:39:29 AODV: theory AODV.D_Global_Invariants
10:39:29 AODV: theory AODV.B_Global_Invariants
10:39:29 AODV: theory AODV.C_Global_Invariants
10:39:30 AODV: theory AODV.E_Global_Invariants
10:39:30 AODV: theory AODV.B_Aodv_Loop_Freedom
10:39:31 AODV: theory AODV.D_Aodv_Loop_Freedom
10:39:31 AODV: theory AODV.C_Aodv_Loop_Freedom
10:39:31 AODV: theory AODV.E_Aodv_Loop_Freedom
10:39:40 AODV: theory AODV.All
13:28:22 Timing AODV (8 threads, 10256.541s elapsed time, 61925.684s cpu time, 5450.092s GC time, factor 6.04)
13:28:22 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV
13:28:22 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/document.pdf
13:28:22 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/outline.pdf
13:28:22 Finished AODV (2:51:12 elapsed time, 17:12:34 cpu time, factor 6.03)
13:28:22 Building HOL-Library ...
13:28:25 HOL-Library: theory HOL-Library.AList
13:28:25 HOL-Library: theory HOL-Library.Adhoc_Overloading
13:28:25 HOL-Library: theory HOL-Library.BNF_Axiomatization
13:28:25 HOL-Library: theory HOL-Library.BNF_Corec
13:28:25 HOL-Library: theory HOL-Library.Case_Converter
13:28:25 HOL-Library: theory HOL-Library.Bit
13:28:25 HOL-Library: theory HOL-Library.Cancellation
13:28:25 HOL-Library: theory HOL-Library.Boolean_Algebra
13:28:25 HOL-Library: theory HOL-Library.Monad_Syntax
13:28:25 HOL-Library: theory HOL-Library.Char_ord
13:28:25 HOL-Library: theory HOL-Library.State_Monad
13:28:25 HOL-Library: theory HOL-Library.Code_Abstract_Nat
13:28:25 HOL-Library: theory HOL-Library.Code_Prolog
13:28:25 HOL-Library: theory HOL-Library.Code_Lazy
13:28:26 HOL-Library: theory HOL-Library.Simps_Case_Conv
13:28:26 HOL-Library: theory HOL-Library.Extended
13:28:26 HOL-Library: theory HOL-Library.Code_Binary_Nat
13:28:26 HOL-Library: theory HOL-Library.Multiset
13:28:26 HOL-Library: theory HOL-Library.Code_Target_Nat
13:28:27 HOL-Library: theory HOL-Library.Code_Target_Int
13:28:27 HOL-Library: theory HOL-Library.Code_Test
13:28:27 HOL-Library: theory HOL-Library.Comparator
13:28:27 HOL-Library: theory HOL-Library.Code_Target_Numeral
13:28:28 HOL-Library: theory HOL-Library.Conditional_Parametricity
13:28:28 HOL-Library: theory HOL-Library.Datatype_Records
13:28:28 HOL-Library: theory HOL-Library.DAList
13:28:28 HOL-Library: theory HOL-Library.Debug
13:28:28 HOL-Library: theory HOL-Library.Disjoint_Sets
13:28:29 HOL-Library: theory HOL-Library.Dlist
13:28:29 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
13:28:29 HOL-Library: theory HOL-Library.Fun_Lexorder
13:28:29 HOL-Library: theory HOL-Library.FuncSet
13:28:29 HOL-Library: theory HOL-Library.Function_Algebras
13:28:29 HOL-Library: theory HOL-Library.Function_Division
13:28:29 HOL-Library: theory HOL-Library.Groups_Big_Fun
13:28:30 HOL-Library: theory HOL-Library.IArray
13:28:30 HOL-Library: theory HOL-Library.Infinite_Set
13:28:30 HOL-Library: theory HOL-Library.Equipollence
13:28:30 HOL-Library: theory HOL-Library.LaTeXsugar
13:28:30 HOL-Library: theory HOL-Library.Lattice_Constructions
13:28:30 HOL-Library: theory HOL-Library.Omega_Words_Fun
13:28:30 HOL-Library: theory HOL-Library.Ramsey
13:28:30 HOL-Library: theory HOL-Library.Lattice_Syntax
13:28:30 HOL-Library: theory HOL-Library.Combine_PER
13:28:31 HOL-Library: theory HOL-Library.Complete_Partial_Order2
13:28:31 HOL-Library: theory HOL-Library.ListVector
13:28:31 HOL-Library: theory HOL-Library.List_Lexorder
13:28:31 HOL-Library: theory HOL-Library.Mapping
13:28:31 HOL-Library: theory HOL-Library.More_List
13:28:31 HOL-Library: theory HOL-Library.Nat_Bijection
13:28:32 HOL-Library: theory HOL-Library.Poly_Mapping
13:28:32 HOL-Library: theory HOL-Library.Stream
13:28:32 HOL-Library: theory HOL-Library.Old_Datatype
13:28:34 HOL-Library: theory HOL-Library.AList_Mapping
13:28:34 HOL-Library: theory HOL-Library.Old_Recdef
13:28:35 HOL-Library: theory HOL-Library.Open_State_Syntax
13:28:35 HOL-Library: theory HOL-Library.Option_ord
13:28:36 HOL-Library: theory HOL-Library.Parallel
13:28:36 HOL-Library: theory HOL-Library.Pattern_Aliases
13:28:36 HOL-Library: theory HOL-Library.Perm
13:28:37 HOL-Library: theory HOL-Library.Phantom_Type
13:28:37 HOL-Library: theory HOL-Library.Power_By_Squaring
13:28:37 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
13:28:37 HOL-Library: theory HOL-Library.Preorder
13:28:37 HOL-Library: theory HOL-Library.Product_Lexorder
13:28:37 HOL-Library: theory HOL-Library.DAList_Multiset
13:28:37 HOL-Library: theory HOL-Library.Multiset_Order
13:28:37 HOL-Library: theory HOL-Library.Permutation
13:28:37 HOL-Library: theory HOL-Library.Permutations
13:28:38 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
13:28:38 HOL-Library: theory HOL-Library.Product_Plus
13:28:38 HOL-Library: theory HOL-Library.Cardinality
13:28:38 HOL-Library: theory HOL-Library.Quotient_Syntax
13:28:38 HOL-Library: theory HOL-Library.Product_Order
13:28:38 HOL-Library: theory HOL-Library.Quotient_Option
13:28:38 HOL-Library: theory HOL-Library.Quotient_Product
13:28:38 HOL-Library: theory HOL-Library.Quotient_Set
13:28:38 HOL-Library: theory HOL-Library.Quotient_Sum
13:28:38 HOL-Library: theory HOL-Library.Quotient_List
13:28:39 HOL-Library: theory HOL-Library.Quotient_Type
13:28:39 HOL-Library: theory HOL-Library.Finite_Lattice
13:28:39 HOL-Library: theory HOL-Library.RBT_Impl
13:28:39 HOL-Library: theory HOL-Library.Realizers
13:28:39 HOL-Library: theory HOL-Library.Reflection
13:28:39 HOL-Library: theory HOL-Library.Refute
13:28:40 HOL-Library: theory HOL-Library.Rewrite
13:28:40 HOL-Library: theory HOL-Library.Set_Algebras
13:28:42 HOL-Library: theory HOL-Library.Sorting_Algorithms
13:28:42 HOL-Library: theory HOL-Library.Stirling
13:28:42 HOL-Library: theory HOL-Library.Sublist
13:28:42 HOL-Library: theory HOL-Library.Numeral_Type
13:28:43 HOL-Library: theory HOL-Library.Transitive_Closure_Table
13:28:43 HOL-Library: theory HOL-Library.Tree
13:28:43 HOL-Library: theory HOL-Library.Uprod
13:28:44 HOL-Library: theory HOL-Library.While_Combinator
13:28:44 HOL-Library: theory HOL-Library.Countable
13:28:45 HOL-Library: theory HOL-Library.Type_Length
13:28:45 HOL-Library: theory HOL-Library.BigO
13:28:45 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
13:28:45 HOL-Library: theory HOL-Library.Prefix_Order
13:28:45 HOL-Library: theory HOL-Library.Saturated
13:28:45 HOL-Library: theory HOL-Library.Subseq_Order
13:28:45 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
13:28:46 HOL-Library: theory HOL-Library.Diagonal_Subsequence
13:28:46 HOL-Library: theory HOL-Library.Discrete
13:28:46 HOL-Library: theory HOL-Library.Going_To_Filter
13:28:46 HOL-Library: theory HOL-Library.Indicator_Function
13:28:46 HOL-Library: theory HOL-Library.Landau_Symbols
13:28:46 HOL-Library: theory HOL-Library.Lattice_Algebras
13:28:46 HOL-Library: theory HOL-Library.Countable_Set
13:28:46 HOL-Library: theory HOL-Library.FSet
13:28:47 HOL-Library: theory HOL-Library.Liminf_Limsup
13:28:47 HOL-Library: theory HOL-Library.Log_Nat
13:28:47 HOL-Library: theory HOL-Library.Lub_Glb
13:28:48 HOL-Library: theory HOL-Library.Countable_Complete_Lattices
13:28:48 HOL-Library: theory HOL-Library.Countable_Set_Type
13:28:48 HOL-Library: theory HOL-Library.Set_Idioms
13:28:49 HOL-Library: theory HOL-Library.Tree_Multiset
13:28:49 HOL-Library: theory HOL-Library.Multiset_Permutations
13:28:50 HOL-Library: theory HOL-Library.Nonpos_Ints
13:28:50 HOL-Library: theory HOL-Library.OptionalSugar
13:28:51 HOL-Library: theory HOL-Library.Periodic_Fun
13:28:51 HOL-Library: theory HOL-Library.Quadratic_Discriminant
13:28:51 HOL-Library: theory HOL-Library.Sum_of_Squares
13:28:51 HOL-Library: theory HOL-Library.Tree_Real
13:28:52 HOL-Library: theory HOL-Library.Order_Continuity
13:28:53 HOL-Library: theory HOL-Library.Extended_Nat
13:28:54 HOL-Library: theory HOL-Library.Finite_Map
13:28:55 HOL-Library: theory HOL-Library.Float
13:28:55 HOL-Library: theory HOL-Library.Extended_Real
13:28:55 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
13:29:04 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
13:29:24 HOL-Library: theory HOL-Library.Library
13:29:50 HOL-Library: theory HOL-Library.RBT
13:29:51 HOL-Library: theory HOL-Library.RBT_Mapping
13:29:51 HOL-Library: theory HOL-Library.RBT_Set
13:31:53 Timing HOL-Library (8 threads, 132.550s elapsed time, 853.040s cpu time, 47.836s GC time, factor 6.44)
13:31:53 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library
13:31:53 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf
13:31:53 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf
13:31:53 Finished HOL-Library (0:03:26 elapsed time, 0:17:49 cpu time, factor 5.17)
13:31:53 Building ConcurrentIMP ...
13:31:54 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred
13:31:55 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang
13:32:08 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg
13:32:11 ConcurrentIMP: theory ConcurrentIMP.CIMP
13:32:11 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer_ex
13:32:11 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer_ex
13:32:43 Timing ConcurrentIMP (8 threads, 22.467s elapsed time, 58.656s cpu time, 3.084s GC time, factor 2.61)
13:32:43 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP
13:32:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf
13:32:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf
13:32:43 Finished ConcurrentIMP (0:00:49 elapsed time, 0:01:56 cpu time, factor 2.36)
13:32:43 Running ConcurrentGC ...
13:32:44 ConcurrentGC: theory ConcurrentGC.Model
13:33:04 ConcurrentGC: theory ConcurrentGC.Tactics
13:33:13 ConcurrentGC: theory ConcurrentGC.Proofs_basis
13:33:17 ConcurrentGC: theory ConcurrentGC.TSO
13:33:43 ConcurrentGC: theory ConcurrentGC.Handshakes
13:38:43 ConcurrentGC: theory ConcurrentGC.MarkObject
13:42:15 ConcurrentGC: theory ConcurrentGC.StrongTricolour
13:43:46 ConcurrentGC: theory ConcurrentGC.Proofs
13:43:48 ConcurrentGC: theory ConcurrentGC.Concrete_heap
13:43:50 ConcurrentGC: theory ConcurrentGC.Concrete
16:10:57 Timing ConcurrentGC (8 threads, 9484.261s elapsed time, 36652.904s cpu time, 2347.416s GC time, factor 3.86)
16:10:57 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC
16:10:57 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf
16:10:57 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf
16:10:57 Finished ConcurrentGC (2:38:11 elapsed time, 10:11:06 cpu time, factor 3.86)
16:10:57 Building HOL-Word ...
16:10:58 HOL-Word: theory HOL-Library.Bit
16:10:58 HOL-Word: theory HOL-Library.Boolean_Algebra
16:10:58 HOL-Word: theory HOL-Library.Phantom_Type
16:10:58 HOL-Word: theory HOL-Word.Bit_Representation
16:10:58 HOL-Word: theory HOL-Word.Bits
16:10:58 HOL-Word: theory HOL-Word.Misc_Typedef
16:11:00 HOL-Word: theory HOL-Word.Bits_Bit
16:11:00 HOL-Word: theory HOL-Library.Cardinality
16:11:02 HOL-Word: theory HOL-Word.Bool_List_Representation
16:11:02 HOL-Word: theory HOL-Word.Misc_Arithmetic
16:11:03 HOL-Word: theory HOL-Library.Numeral_Type
16:11:03 HOL-Word: theory HOL-Word.Bits_Int
16:11:05 HOL-Word: theory HOL-Library.Type_Length
16:11:05 HOL-Word: theory HOL-Word.Word
16:11:12 HOL-Word: theory HOL-Word.Word_Bitwise
16:11:13 HOL-Word: theory HOL-Word.More_Word
16:11:13 HOL-Word: theory HOL-Word.Word_Examples
16:11:33 Timing HOL-Word (8 threads, 15.712s elapsed time, 84.356s cpu time, 2.884s GC time, factor 5.37)
16:11:33 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word
16:11:33 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf
16:11:33 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf
16:11:33 Finished HOL-Word (0:00:35 elapsed time, 0:02:04 cpu time, factor 3.53)
16:11:33 Building Word_Lib ...
16:11:34 Word_Lib: theory Word_Lib.Hex_Words
16:11:34 Word_Lib: theory HOL-Library.Sublist
16:11:34 Word_Lib: theory Word_Lib.Word_Type_Syntax
16:11:34 Word_Lib: theory Word_Lib.Signed_Words
16:11:34 Word_Lib: theory Word_Lib.Enumeration
16:11:34 Word_Lib: theory Word_Lib.HOL_Lemmas
16:11:34 Word_Lib: theory Word_Lib.More_Divides
16:11:35 Word_Lib: theory Word_Lib.Norm_Words
16:11:35 Word_Lib: theory Word_Lib.WordBitwise_Signed
16:11:35 Word_Lib: theory Word_Lib.Word_Syntax
16:11:37 Word_Lib: theory Word_Lib.Word_Lib
16:11:38 Word_Lib: theory Word_Lib.Word_Enum
16:11:38 Word_Lib: theory Word_Lib.Aligned
16:11:39 Word_Lib: theory Word_Lib.Word_Setup_32
16:11:39 Word_Lib: theory Word_Lib.Word_Setup_64
16:11:39 Word_Lib: theory Word_Lib.Word_Next
16:11:39 Word_Lib: theory Word_Lib.Word_Lemmas
16:11:47 Word_Lib: theory Word_Lib.Word_Lemmas_32
16:11:48 Word_Lib: theory Word_Lib.Word_Lemmas_64
16:13:05 Timing Word_Lib (8 threads, 72.769s elapsed time, 211.672s cpu time, 6.112s GC time, factor 2.91)
16:13:05 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib
16:13:05 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf
16:13:05 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf
16:13:05 Finished Word_Lib (0:01:30 elapsed time, 0:04:08 cpu time, factor 2.74)
16:13:05 Building IP_Addresses ...
16:13:06 IP_Addresses: theory HOL-Eisbach.Eisbach
16:13:06 IP_Addresses: theory HOL-Library.Cancellation
16:13:06 IP_Addresses: theory HOL-Library.Infinite_Set
16:13:06 IP_Addresses: theory HOL-Library.Option_ord
16:13:06 IP_Addresses: theory IP_Addresses.NumberWang_IPv4
16:13:06 IP_Addresses: theory IP_Addresses.NumberWang_IPv6
16:13:08 IP_Addresses: theory HOL-Library.Multiset
16:13:15 IP_Addresses: theory HOL-ex.Quicksort
16:13:15 IP_Addresses: theory Automatic_Refinement.Misc
16:13:24 IP_Addresses: theory HOL-Library.Code_Abstract_Nat
16:13:24 IP_Addresses: theory HOL-Library.Product_Lexorder
16:13:24 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
16:13:24 IP_Addresses: theory IP_Addresses.Hs_Compat
16:13:24 IP_Addresses: theory IP_Addresses.WordInterval
16:13:24 IP_Addresses: theory HOL-Library.Code_Target_Nat
16:13:24 IP_Addresses: theory IP_Addresses.Lib_List_toString
16:13:24 IP_Addresses: theory IP_Addresses.Lib_Word_toString
16:13:31 IP_Addresses: theory IP_Addresses.IP_Address
16:13:31 IP_Addresses: theory IP_Addresses.WordInterval_Sorted
16:13:37 IP_Addresses: theory IP_Addresses.IPv4
16:13:37 IP_Addresses: theory IP_Addresses.IPv6
16:13:37 IP_Addresses: theory IP_Addresses.Prefix_Match
16:13:39 IP_Addresses: theory IP_Addresses.CIDR_Split
16:15:23 IP_Addresses: theory IP_Addresses.IP_Address_Parser
16:15:23 IP_Addresses: theory IP_Addresses.IP_Address_toString
16:15:26 IP_Addresses: theory IP_Addresses.Prefix_Match_toString
16:19:31 Timing IP_Addresses (8 threads, 344.225s elapsed time, 1127.668s cpu time, 59.208s GC time, factor 3.28)
16:19:31 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses
16:19:31 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf
16:19:31 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf
16:19:31 Finished IP_Addresses (0:06:25 elapsed time, 0:20:33 cpu time, factor 3.20)
16:19:31 Building Simple_Firewall ...
16:19:33 Simple_Firewall: theory HOL-Library.Char_ord
16:19:33 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
16:19:33 Simple_Firewall: theory Simple_Firewall.GroupF
16:19:33 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
16:19:33 Simple_Firewall: theory Simple_Firewall.List_Product_More
16:19:33 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
16:19:33 Simple_Firewall: theory Simple_Firewall.Option_Helpers
16:19:33 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
16:19:33 Simple_Firewall: theory Simple_Firewall.Iface
16:19:34 Simple_Firewall: theory Simple_Firewall.L4_Protocol
16:19:40 Simple_Firewall: theory Simple_Firewall.Simple_Packet
16:19:40 Simple_Firewall: theory Simple_Firewall.Primitives_toString
16:19:43 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
16:19:46 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString
16:19:46 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
16:19:49 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
16:19:49 Simple_Firewall: theory Simple_Firewall.Shadowed
16:19:50 Simple_Firewall: theory Simple_Firewall.Service_Matrix
16:20:28 Timing Simple_Firewall (8 threads, 27.984s elapsed time, 120.644s cpu time, 4.792s GC time, factor 4.31)
16:20:28 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall
16:20:28 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf
16:20:28 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf
16:20:28 Finished Simple_Firewall (0:00:56 elapsed time, 0:03:11 cpu time, factor 3.41)
16:20:28 Building Routing ...
16:20:30 Routing: theory Routing.Linorder_Helper
16:20:30 Routing: theory HOL-Library.Adhoc_Overloading
16:20:30 Routing: theory HOL-Library.Monad_Syntax
16:20:31 Routing: theory Routing.Routing_Table
16:20:36 Routing: theory Routing.IpRoute_Parser
16:20:36 Routing: theory Routing.Linux_Router
16:21:02 Timing Routing (8 threads, 13.656s elapsed time, 43.044s cpu time, 1.136s GC time, factor 3.15)
16:21:02 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing
16:21:02 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf
16:21:02 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf
16:21:02 Finished Routing (0:00:33 elapsed time, 0:01:22 cpu time, factor 2.49)
16:21:02 Building Iptables_Semantics ...
16:21:03 Iptables_Semantics: theory Iptables_Semantics.List_Misc
16:21:03 Iptables_Semantics: theory Iptables_Semantics.Negation_Type
16:21:06 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
16:21:07 Iptables_Semantics: theory HOL-Library.Code_Target_Int
16:21:07 Iptables_Semantics: theory HOL-Library.LaTeXsugar
16:21:07 Iptables_Semantics: theory Native_Word.More_Bits_Int
16:21:07 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
16:21:07 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
16:21:07 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
16:21:07 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
16:21:07 Iptables_Semantics: theory Iptables_Semantics.Ternary
16:21:07 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
16:21:07 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
16:21:07 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
16:21:07 Iptables_Semantics: theory Iptables_Semantics.IpAddresses
16:21:07 Iptables_Semantics: theory Iptables_Semantics.Word_Upto
16:21:10 Iptables_Semantics: theory Iptables_Semantics.Ports
16:21:10 Iptables_Semantics: theory Native_Word.Code_Symbolic_Bits_Int
16:21:10 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
16:21:10 Iptables_Semantics: theory Native_Word.Bits_Integer
16:21:13 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
16:21:34 Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int
16:21:36 Iptables_Semantics: theory Iptables_Semantics.Semantics
16:21:36 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
16:21:36 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
16:21:38 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
16:21:38 Iptables_Semantics: theory Iptables_Semantics.Matching
16:21:38 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
16:21:39 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
16:21:39 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
16:21:40 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
16:21:40 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
16:21:41 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
16:21:42 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
16:21:43 Iptables_Semantics: theory Iptables_Semantics.Optimizing
16:21:43 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
16:21:43 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
16:21:45 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
16:21:48 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
16:21:51 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
16:21:53 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
16:21:53 Iptables_Semantics: theory Iptables_Semantics.Ipassmt
16:21:59 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
16:22:59 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
16:22:59 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
16:22:59 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
16:22:59 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
16:23:00 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
16:23:00 Iptables_Semantics: theory Iptables_Semantics.No_Spoof
16:23:00 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
16:23:00 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
16:23:00 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
16:23:11 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
16:23:16 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
16:23:24 Iptables_Semantics: theory Iptables_Semantics.Transform
16:23:32 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
16:23:34 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
16:23:43 Iptables_Semantics: theory Iptables_Semantics.Code_Interface
16:23:43 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
16:23:45 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
16:23:45 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
16:23:45 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
16:23:57 Iptables_Semantics: theory Iptables_Semantics.Documentation
16:23:57 Iptables_Semantics: theory Iptables_Semantics.Parser
16:23:58 Iptables_Semantics: theory Iptables_Semantics.Code_haskell
16:25:26 Timing Iptables_Semantics (8 threads, 203.111s elapsed time, 967.200s cpu time, 67.832s GC time, factor 4.76)
16:25:26 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics
16:25:26 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf
16:25:26 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf
16:25:26 Finished Iptables_Semantics (0:04:22 elapsed time, 0:19:37 cpu time, factor 4.49)
16:25:26 Building Iptables_Semantics_Examples ...
16:25:28 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com
16:25:28 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall
16:25:28 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company
16:25:28 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example
16:25:28 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing
16:25:28 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test
16:25:28 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof
16:25:28 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6
16:25:30 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test
16:25:38 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail
16:25:39 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples
16:25:39 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed
16:25:40 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation
16:32:40 Timing Iptables_Semantics_Examples (8 threads, 404.569s elapsed time, 2875.544s cpu time, 251.972s GC time, factor 7.11)
16:32:40 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples
16:32:40 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf
16:32:40 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf
16:32:40 Finished Iptables_Semantics_Examples (0:07:12 elapsed time, 0:48:56 cpu time, factor 6.79)
16:32:40 Running Iptables_Semantics_Examples_Big ...
16:32:42 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern
16:32:42 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated
16:32:42 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small
16:32:42 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3
16:32:42 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall
16:38:06 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large
18:20:10 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW
20:11:52 Timing Iptables_Semantics_Examples_Big (8 threads, 13141.456s elapsed time, 68058.876s cpu time, 23910.952s GC time, factor 5.18)
20:11:52 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big
20:11:52 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/document.pdf
20:11:52 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/outline.pdf
20:11:52 Finished Iptables_Semantics_Examples_Big (3:39:09 elapsed time, 18:54:48 cpu time, factor 5.18)
20:11:52 
20:11:52 === TIMING ===
20:11:52 
20:11:52 Group slow: 17:58:15 elapsed time, 63:01:08 cpu time, factor 3.51
20:11:52 Group AFP: 18:24:16 elapsed time, 64:59:27 cpu time, factor 3.53
20:11:52 Group main: 0:10:47 elapsed time, 0:42:05 cpu time, factor 3.90
20:11:52 Group timing: 0:04:02 elapsed time, 0:19:54 cpu time, factor 4.93
20:11:52 Group very_slow: 11:23:27 elapsed time, 30:24:30 cpu time, factor 2.67
20:11:52 Overall: 18:36:38 elapsed time, 65:42:06 cpu time, factor 3.53
20:11:52 Archiving artifacts
20:11:53 Started calculate disk usage of build
20:11:53 Finished Calculation of disk usage of build in 0 seconds
20:12:09 Started calculate disk usage of workspace
20:12:10 Finished Calculation of disk usage of workspace in  1 second
20:12:10 No emails were triggered.
20:12:10 Finished: SUCCESS