Console Output

01:33:10 Started by an SCM change
01:33:10 [EnvInject] - Loading node environment variables.
01:33:10 Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow
01:33:10 [isabelle-nightly-slow] $ hg showconfig paths.default
01:33:10 [isabelle-nightly-slow] $ hg pull --rev default
01:33:10 pulling from http://isabelle.in.tum.de/repos/isabelle/
01:33:10 searching for changes
01:33:10 no changes found
01:33:11 [isabelle-nightly-slow] $ hg update --clean --rev default
01:33:11 32 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:11 [isabelle-nightly-slow] $ hg log --rev . --template {node}
01:33:11 [isabelle-nightly-slow] $ hg log --rev . --template {rev}
01:33:12 [isabelle-nightly-slow] $ hg log --rev 24bbc4e30e5b2bc59c394f006ae06fdcd0e6dc69 --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(24bbc4e30e5b2bc59c394f006ae06fdcd0e6dc69)" --encoding UTF-8 --encodingmode replace
01:33:12 [afp] $ hg showconfig paths.default
01:33:12 [afp] $ hg pull --rev default
01:33:13 pulling from https://bitbucket.org/isa-afp/afp-devel/
01:33:13 no changes found
01:33:13 [afp] $ hg update --clean --rev default
01:33:13 36 files updated, 0 files merged, 5 files removed, 0 files unresolved
01:33:13 [afp] $ hg --config extensions.purge= clean --all
01:33:14 [afp] $ hg log --rev . --template {node}
01:33:14 [afp] $ hg log --rev . --template {rev}
01:33:14 [afp] $ hg log --rev c380272ea50c12a8f6e19eb6741ef19f45de8345 --template exists\n
01:33:14 exists
01:33:14 [afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg><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(c380272ea50c12a8f6e19eb6741ef19f45de8345)" --encoding UTF-8 --encodingmode replace
01:33:15 No emails were triggered.
01:33:15 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins2269687091325850339.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:16 ### Building graph browser ...
01:33:16 warning: [options] bootstrap class path not set in conjunction with -source 6
01:33:16 warning: [options] source value 6 is obsolete and will be removed in a future release
01:33:16 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
01:33:17 Note: Some input files use or override a deprecated API.
01:33:17 Note: Recompile with -Xlint:deprecation for details.
01:33:17 Note: Some input files use unchecked or unsafe operations.
01:33:17 Note: Recompile with -Xlint:unchecked for details.
01:33:17 3 warnings
01:33:18 ### Building Isabelle/Scala ...
01:34:18 ### Building Isabelle/jEdit ...
01:34:53 + bin/isabelle ocaml_setup
01:34:54 # To setup the new switch in the current shell, you need to run:
01:34:54 eval `opam config env`
01:34:54 + bin/isabelle ghc_setup
01:34:55 stack will use a sandboxed GHC it installed
01:34:55 For more information on paths, see 'stack path' and 'stack exec env'
01:34:55 To use this GHC and packages outside of a project, consider using:
01:34:55 stack ghc, stack ghci, stack runghc, or stack exec
01:34:55 The Glorious Glasgow Haskell Compilation System, version 8.4.4
01:34:56 + bin/isabelle ci_build_slow
01:35:03 
01:35:03 === CONFIGURATION ===
01:35:03 
01:35:03 ISABELLE_BUILD_OPTIONS=""
01:35:03 
01:35:03 ML_PLATFORM="x86_64-linux"
01:35:03 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7.1-8/x86_64-linux"
01:35:03 ML_SYSTEM="polyml-5.7.1"
01:35:03 ML_OPTIONS="-H 4000 --maxheap 20G"
01:35:04 jobs = 1, threads = 8, numa = false
01:35:04 
01:35:04 === BUILD ===
01:35:04 
01:35:04 Build started at Tue, 5 Feb 2019 01:35:03 +0100
01:35:04 Isabelle id d21789843f01
01:35:04 Build for AFP id 875c61096d3e
01:35:04 
01:35:04 === LOG ===
01:35:04 
01:35:06 Session Pure/Pure
01:35:07 Session FOL/FOL
01:35:07 Session HOL/HOL (main)
01:35:09 Session AFP/AWN (AFP)
01:35:09 Session AFP/AODV (AFP slow)
01:35:09 Session HOL/HOL-Eisbach
01:35:09 Session HOL/HOL-Library (main timing)
01:35:10 Session AFP/Binomial-Heaps (AFP)
01:35:10 Session AFP/ConcurrentIMP (AFP)
01:35:10 Session AFP/ConcurrentGC (AFP slow)
01:35:10 Session AFP/FinFun (AFP)
01:35:10 Session AFP/Finger-Trees (AFP)
01:35:10 Session HOL/HOL-Computational_Algebra (main timing)
01:35:11 Session HOL/HOL-Algebra (main timing)
01:35:11 Session HOL/HOL-Analysis (main timing)
01:35:12 Session AFP/Coinductive (AFP)
01:35:12 Session HOL/HOL-Number_Theory (main timing)
01:35:13 Session HOL/HOL-ex (timing)
01:35:13 Session AFP/Automatic_Refinement (AFP)
01:35:14 Session HOL/HOL-Imperative_HOL (timing)
01:35:14 Session AFP/Trie (AFP)
01:35:14 Session AFP/Flyspeck-Tame (AFP slow very_slow)
01:35:14 Session HOL/HOL-Word (main timing)
01:35:14 Session AFP/Native_Word (AFP)
01:35:15 Session AFP/Refine_Monadic (AFP)
01:35:15 Session AFP/Collections (AFP)
01:35:16 Session AFP/Word_Lib (AFP)
01:35:16 Session AFP/IP_Addresses (AFP)
01:35:16 Session AFP/Simple_Firewall (AFP)
01:35:17 Session AFP/Routing (AFP)
01:35:17 Session AFP/Iptables_Semantics (AFP)
01:35:17 Session AFP/Iptables_Semantics_Examples (AFP)
01:35:17 Session AFP/Iptables_Semantics_Examples_Big (AFP large slow very_slow)
01:35:18 Session AFP/JinjaThreads (AFP slow)
01:35:21 Building Pure ...
01:35:44 Pure: theory Pure
01:35:45 Pure: theory ML_Bootstrap
01:35:46 Pure: theory Pure.Sessions
01:35:49 Timing Pure (1 threads, 1.546s elapsed time, 1.512s cpu time, 0.052s GC time, factor 0.98)
01:35:49 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure
01:35:49 Finished Pure (0:00:26 elapsed time, 0:00:26 cpu time, factor 0.98)
01:35:49 Building HOL ...
01:35:53 HOL: theory HOL.Code_Generator
01:35:58 HOL: theory HOL.HOL
01:36:03 HOL: theory HOL.Argo
01:36:03 HOL: theory HOL.Orderings
01:36:03 HOL: theory HOL.Ctr_Sugar
01:36:05 HOL: theory HOL.SAT
01:36:05 HOL: theory HOL.Groups
01:36:09 HOL: theory HOL.Lattices
01:36:12 HOL: theory HOL.Set
01:36:14 HOL: theory HOL.Fun
01:36:14 HOL: theory HOL.Typedef
01:36:15 HOL: theory HOL.Complete_Lattices
01:36:15 HOL: theory HOL.Rings
01:36:18 HOL: theory HOL.Inductive
01:36:21 HOL: theory HOL.Product_Type
01:36:21 HOL: theory HOL.Sum_Type
01:36:23 HOL: theory HOL.Complete_Partial_Order
01:36:31 HOL: theory HOL.Nat
01:36:33 HOL: theory HOL.Meson
01:36:33 HOL: theory HOL.Fields
01:36:34 HOL: theory HOL.ATP
01:36:38 HOL: theory HOL.Metis
01:36:40 HOL: theory HOL.Finite_Set
01:36:43 HOL: theory HOL.Relation
01:36:45 HOL: theory HOL.Transitive_Closure
01:36:47 HOL: theory HOL.Wellfounded
01:36:48 HOL: theory HOL.Fun_Def_Base
01:36:48 HOL: theory HOL.Hilbert_Choice
01:36:48 HOL: theory HOL.Wfrec
01:36:48 HOL: theory HOL.Order_Relation
01:36:48 HOL: theory HOL.BNF_Wellorder_Relation
01:36:49 HOL: theory HOL.BNF_Wellorder_Embedding
01:36:49 HOL: theory HOL.Zorn
01:36:50 HOL: theory HOL.BNF_Wellorder_Constructions
01:36:51 HOL: theory HOL.BNF_Cardinal_Order_Relation
01:36:52 HOL: theory HOL.BNF_Cardinal_Arithmetic
01:36:53 HOL: theory HOL.BNF_Def
01:36:57 HOL: theory HOL.BNF_Composition
01:36:57 HOL: theory HOL.Basic_BNFs
01:36:59 HOL: theory HOL.BNF_Fixpoint_Base
01:37:03 HOL: theory HOL.BNF_Least_Fixpoint
01:37:08 HOL: theory HOL.Basic_BNF_LFPs
01:37:08 HOL: theory HOL.Transfer
01:37:09 HOL: theory HOL.Num
01:37:14 HOL: theory HOL.Power
01:37:17 HOL: theory HOL.Groups_Big
01:37:21 HOL: theory HOL.Equiv_Relations
01:37:21 HOL: theory HOL.Lifting
01:37:24 HOL: theory HOL.Lifting_Set
01:37:24 HOL: theory HOL.Option
01:37:24 HOL: theory HOL.Quotient
01:37:25 HOL: theory HOL.Extraction
01:37:25 HOL: theory HOL.Partial_Function
01:37:25 HOL: theory HOL.Lattices_Big
01:37:26 HOL: theory HOL.Fun_Def
01:37:29 HOL: theory HOL.Int
01:37:34 HOL: theory HOL.Euclidean_Division
01:37:42 HOL: theory HOL.Parity
01:37:47 HOL: theory HOL.Divides
01:37:51 HOL: theory HOL.Code_Numeral
01:37:51 HOL: theory HOL.Numeral_Simprocs
01:37:51 HOL: theory HOL.SMT
01:37:51 HOL: theory HOL.Set_Interval
01:37:53 HOL: theory HOL.Semiring_Normalization
01:37:57 HOL: theory HOL.Groebner_Basis
01:37:59 HOL: theory HOL.Conditionally_Complete_Lattices
01:37:59 HOL: theory HOL.Filter
01:37:59 HOL: theory HOL.Presburger
01:38:07 HOL: theory HOL.Sledgehammer
01:38:11 HOL: theory HOL.List
01:38:27 HOL: theory HOL.Groups_List
01:38:27 HOL: theory HOL.Map
01:38:29 HOL: theory HOL.Factorial
01:38:29 HOL: theory HOL.GCD
01:38:29 HOL: theory HOL.Enum
01:38:29 HOL: theory HOL.Random
01:38:30 HOL: theory HOL.Binomial
01:38:37 HOL: theory HOL.String
01:38:40 HOL: theory HOL.BNF_Greatest_Fixpoint
01:38:41 HOL: theory HOL.Predicate
01:38:41 HOL: theory HOL.Typerep
01:38:43 HOL: theory HOL.Lazy_Sequence
01:38:45 HOL: theory HOL.Limited_Sequence
01:38:45 HOL: theory HOL.Code_Evaluation
01:38:48 HOL: theory HOL.Quickcheck_Random
01:38:51 HOL: theory HOL.Quickcheck_Exhaustive
01:38:51 HOL: theory HOL.Quickcheck_Narrowing
01:38:51 HOL: theory HOL.Random_Pred
01:38:52 HOL: theory HOL.Random_Sequence
01:38:58 HOL: theory HOL.Predicate_Compile
01:38:58 HOL: theory HOL.Record
01:39:01 HOL: theory HOL.Nitpick
01:39:14 HOL: theory HOL.Nunchaku
01:39:16 HOL: theory Main
01:39:19 HOL: theory HOL.Archimedean_Field
01:39:19 HOL: theory HOL.Hull
01:39:19 HOL: theory HOL.Topological_Spaces
01:39:19 HOL: theory HOL.Modules
01:39:21 HOL: theory HOL.Vector_Spaces
01:39:32 HOL: theory HOL.Rat
01:39:38 HOL: theory HOL.Real
01:39:41 HOL: theory HOL.Real_Vector_Spaces
01:39:58 HOL: theory HOL.Inequalities
01:39:58 HOL: theory HOL.Limits
01:40:08 HOL: theory HOL.Deriv
01:40:08 HOL: theory HOL.Series
01:40:12 HOL: theory HOL.NthRoot
01:40:13 HOL: theory HOL.Transcendental
01:40:21 HOL: theory HOL.Complex
01:40:24 HOL: theory HOL.MacLaurin
01:40:25 HOL: theory Complex_Main
01:42:14 Timing HOL (8 threads, 286.123s elapsed time, 994.720s cpu time, 83.668s GC time, factor 3.48)
01:42:14 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL
01:42:14 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf
01:42:14 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf
01:42:14 Finished HOL (0:06:21 elapsed time, 0:19:37 cpu time, factor 3.09)
01:42:14 Running Flyspeck-Tame ...
01:42:15 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order
01:42:15 Flyspeck-Tame: theory HOL-Library.IArray
01:42:15 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl
01:42:15 Flyspeck-Tame: theory HOL-Library.AList
01:42:15 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat
01:42:15 Flyspeck-Tame: theory HOL-Library.While_Combinator
01:42:15 Flyspeck-Tame: theory HOL-Library.Code_Target_Int
01:42:15 Flyspeck-Tame: theory Flyspeck-Tame.ListAux
01:42:15 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat
01:42:15 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso
01:42:16 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral
01:42:16 Flyspeck-Tame: theory Flyspeck-Tame.Arch
01:42:17 Flyspeck-Tame: theory Flyspeck-Tame.Worklist
01:42:17 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax
01:42:18 Flyspeck-Tame: theory Flyspeck-Tame.ListSum
01:42:18 Flyspeck-Tame: theory Flyspeck-Tame.Rotation
01:42:18 Flyspeck-Tame: theory Flyspeck-Tame.Maps
01:42:18 Flyspeck-Tame: theory Flyspeck-Tame.Graph
01:42:18 Flyspeck-Tame: theory Trie.Trie
01:42:21 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision
01:42:21 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps
01:42:21 Flyspeck-Tame: theory Flyspeck-Tame.Tame
01:42:23 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator
01:42:23 Flyspeck-Tame: theory Trie.Tries
01:42:23 Flyspeck-Tame: theory Flyspeck-Tame.TameProps
01:42:23 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps
01:42:23 Flyspeck-Tame: theory Flyspeck-Tame.Plane
01:42:24 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps
01:42:25 Flyspeck-Tame: theory Flyspeck-Tame.Plane1
01:42:25 Flyspeck-Tame: theory Flyspeck-Tame.Generator
01:42:27 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum
01:42:33 Flyspeck-Tame: theory Flyspeck-Tame.Invariants
01:42:34 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux
01:42:35 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps
01:42:36 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps
01:42:36 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props
01:42:37 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound
01:42:37 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps
01:42:38 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps
01:42:38 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps
01:42:39 Flyspeck-Tame: theory Flyspeck-Tame.ArchComp
01:42:39 Flyspeck-Tame: theory Flyspeck-Tame.Completeness
15:42:21 *** Timeout
15:42:21 Flyspeck-Tame FAILED
15:42:21 (see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.7.1_x86_64-linux/log/Flyspeck-Tame)
15:42:21 ###           ("_position" v))))))
15:42:21 ### ("\<^const>HOL.Trueprop"
15:42:21 ###   ("_applC"
15:42:21 ###     ("\<^const>Graph.nextFace"
15:42:21 ###       ("\<^const>HOL.eq" ("_position" u) ("_position" f)))
15:42:21 ###     ("_applC" ("\<^const>Graph.nextFace" ("_position" f))
15:42:21 ###       ("_applC" ("\<^const>Graph.nextFace" ("_position" f))
15:42:21 ###         ("_position" v)))))
15:42:21 ### ("\<^const>HOL.Trueprop"
15:42:21 ###   ("\<^const>HOL.eq" ("_position" u)
15:42:21 ###     ("_applC" ("\<^const>Graph.nextVertex" ("_position" f))
15:42:21 ###       ("_applC" ("\<^const>Graph.nextFace" ("_position" f))
15:42:21 ###         ("_applC" ("\<^const>Graph.nextFace" ("_position" f))
15:42:21 ###           ("_position" v))))))
15:42:21 ### ("\<^const>HOL.Trueprop"
15:42:21 ###   ("\<^const>HOL.eq" ("_position" u)
15:42:21 ###     ("_applC" ("\<^const>Graph.nextFace" ("_position" f))
15:42:21 ###       ("_applC" ("\<^const>Graph.nextFace" ("_position" f))
15:42:21 ###         ("_applC" ("\<^const>Graph.nextFace" ("_position" f))
15:42:21 ###           ("_position" v))))))
15:42:21 ### ("\<^const>HOL.Trueprop"
15:42:21 ###   ("_applC"
15:42:21 ###     ("\<^const>Graph.nextFace"
15:42:21 ###       ("\<^const>HOL.eq" ("_position" u) ("_position" f)))
15:42:21 ###     ("_applC" ("\<^const>Graph.nextVertex" ("_position" f))
15:42:21 ###       ("_applC" ("\<^const>Graph.nextFace" ("_position" f))
15:42:21 ###         ("_position" v)))))
15:42:21 ### Fortunately, only one parse tree is well-formed and type-correct,
15:42:21 ### but you may still want to disambiguate your grammar or your input.
15:42:21 ### Ambiguous input (line 234 of "~~/afp/thys/Flyspeck-Tame/GeneratorProps.thy") produces 2 parse trees:
15:42:21 ### ("\<^const>HOL.Trueprop"
15:42:21 ###   ("\<^const>HOL.eq"
15:42:21 ###     ("_applC" ("\<^const>Graph.nextVertex" ("_position" f)) ("_position" u))
15:42:21 ###     ("_position" v)))
15:42:21 ### ("\<^const>HOL.Trueprop"
15:42:21 ###   ("\<^const>HOL.eq"
15:42:21 ###     ("_applC" ("\<^const>Graph.nextFace" ("_position" f)) ("_position" u))
15:42:21 ###     ("_position" v)))
15:42:21 ### Fortunately, only one parse tree is well-formed and type-correct,
15:42:21 ### but you may still want to disambiguate your grammar or your input.
15:42:21 Running JinjaThreads ...
15:42:24 JinjaThreads: theory HOL-Eisbach.Eisbach
15:42:24 JinjaThreads: theory Automatic_Refinement.Foldi
15:42:24 JinjaThreads: theory Automatic_Refinement.Prio_List
15:42:24 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1
15:42:24 JinjaThreads: theory Collections.ICF_Tools
15:42:24 JinjaThreads: theory Finger-Trees.FingerTree
15:42:24 JinjaThreads: theory HOL-Library.AList
15:42:24 JinjaThreads: theory HOL-Library.Adhoc_Overloading
15:42:24 JinjaThreads: theory HOL-Library.Bit
15:42:24 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot
15:42:24 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot
15:42:24 JinjaThreads: theory Collections.Ord_Code_Preproc
15:42:24 JinjaThreads: theory HOL-Library.Monad_Syntax
15:42:24 JinjaThreads: theory Collections.Locale_Code
15:42:24 JinjaThreads: theory Collections.Record_Intf
15:42:24 JinjaThreads: theory HOL-Library.Boolean_Algebra
15:42:24 JinjaThreads: theory Automatic_Refinement.Refine_Util
15:42:24 JinjaThreads: theory HOL-Library.Cancellation
15:42:25 JinjaThreads: theory HOL-Library.Case_Converter
15:42:25 JinjaThreads: theory HOL-Library.Code_Abstract_Nat
15:42:25 JinjaThreads: theory HOL-Library.Code_Target_Nat
15:42:25 JinjaThreads: theory HOL-Library.Code_Target_Int
15:42:25 JinjaThreads: theory HOL-Library.Simps_Case_Conv
15:42:25 JinjaThreads: theory Automatic_Refinement.Anti_Unification
15:42:25 JinjaThreads: theory Automatic_Refinement.Attr_Comb
15:42:25 JinjaThreads: theory Automatic_Refinement.Autoref_Data
15:42:25 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms
15:42:25 JinjaThreads: theory Automatic_Refinement.Indep_Vars
15:42:25 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp
15:42:25 JinjaThreads: theory Automatic_Refinement.Tagged_Solver
15:42:25 JinjaThreads: theory Automatic_Refinement.Select_Solve
15:42:25 JinjaThreads: theory HOL-Library.Dlist
15:42:25 JinjaThreads: theory HOL-Library.Infinite_Set
15:42:25 JinjaThreads: theory HOL-Library.Code_Target_Numeral
15:42:25 JinjaThreads: theory HOL-Library.Lattice_Syntax
15:42:25 JinjaThreads: theory HOL-Library.Complete_Partial_Order2
15:42:25 JinjaThreads: theory HOL-Library.Nat_Bijection
15:42:25 JinjaThreads: theory HOL-Library.Multiset
15:42:26 JinjaThreads: theory HOL-Library.Old_Datatype
15:42:26 JinjaThreads: theory HOL-Library.Option_ord
15:42:26 JinjaThreads: theory HOL-Library.Phantom_Type
15:42:27 JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs
15:42:27 JinjaThreads: theory Trie.Trie
15:42:27 JinjaThreads: theory HOL-Library.RBT_Impl
15:42:27 JinjaThreads: theory HOL-Library.Sublist
15:42:27 JinjaThreads: theory HOL-Library.Transitive_Closure_Table
15:42:28 JinjaThreads: theory HOL-Library.Cardinality
15:42:28 JinjaThreads: theory HOL-Library.While_Combinator
15:42:29 JinjaThreads: theory Collections.DatRef
15:42:29 JinjaThreads: theory HOL-Word.Bits
15:42:29 JinjaThreads: theory HOL-Word.Bits_Bit
15:42:29 JinjaThreads: theory HOL-Word.Misc_Numeric
15:42:30 JinjaThreads: theory HOL-Word.Bit_Representation
15:42:30 JinjaThreads: theory FinFun.FinFun
15:42:31 JinjaThreads: theory HOL-Library.Numeral_Type
15:42:31 JinjaThreads: theory HOL-Word.Word_Miscellaneous
15:42:31 JinjaThreads: theory HOL-Word.Misc_Typedef
15:42:32 JinjaThreads: theory HOL-Word.Bits_Int
15:42:32 JinjaThreads: theory HOL-Library.Countable
15:42:32 JinjaThreads: theory JinjaThreads.Set_Monad
15:42:32 JinjaThreads: theory JinjaThreads.Set_without_equal
15:42:32 JinjaThreads: theory Refine_Monadic.Refine_Chapter
15:42:33 JinjaThreads: theory HOL-Library.Type_Length
15:42:34 JinjaThreads: theory HOL-Library.Countable_Set
15:42:34 JinjaThreads: theory HOL-Word.Bool_List_Representation
15:42:34 JinjaThreads: theory HOL-Library.Countable_Complete_Lattices
15:42:34 JinjaThreads: theory Binomial-Heaps.BinomialHeap
15:42:34 JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap
15:42:35 JinjaThreads: theory HOL-ex.Quicksort
15:42:35 JinjaThreads: theory Native_Word.More_Bits_Int
15:42:35 JinjaThreads: theory HOL-Word.Word
15:42:36 JinjaThreads: theory Automatic_Refinement.Misc
15:42:37 JinjaThreads: theory HOL-Library.Order_Continuity
15:42:38 JinjaThreads: theory Native_Word.Bits_Integer
15:42:39 JinjaThreads: theory HOL-Library.Extended_Nat
15:42:41 JinjaThreads: theory JinjaThreads.Auxiliary
15:42:42 JinjaThreads: theory Coinductive.Coinductive_Nat
15:42:44 JinjaThreads: theory Coinductive.Coinductive_List
15:42:47 JinjaThreads: theory Native_Word.Word_Misc
15:42:48 JinjaThreads: theory Automatic_Refinement.Refine_Lib
15:42:48 JinjaThreads: theory Collections.SetIterator
15:42:48 JinjaThreads: theory Collections.Sorted_List_Operations
15:42:50 JinjaThreads: theory Automatic_Refinement.Autoref_Phases
15:42:50 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging
15:42:50 JinjaThreads: theory Automatic_Refinement.Relators
15:42:50 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover
15:42:50 JinjaThreads: theory Collections.SetIteratorOperations
15:42:52 JinjaThreads: theory Automatic_Refinement.Param_Tool
15:42:52 JinjaThreads: theory Automatic_Refinement.Param_HOL
15:42:54 JinjaThreads: theory Collections.Assoc_List
15:42:54 JinjaThreads: theory Collections.Dlist_add
15:42:54 JinjaThreads: theory Collections.Proper_Iterator
15:42:55 JinjaThreads: theory Automatic_Refinement.Parametricity
15:42:55 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops
15:42:55 JinjaThreads: theory Collections.SetIteratorGA
15:42:55 JinjaThreads: theory Collections.Diff_Array
15:42:55 JinjaThreads: theory Collections.Trie_Impl
15:42:55 JinjaThreads: theory Collections.It_to_It
15:42:57 JinjaThreads: theory Collections.Trie2
15:42:57 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel
15:42:59 JinjaThreads: theory Automatic_Refinement.Autoref_Translate
15:42:59 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo
15:42:59 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface
15:42:59 JinjaThreads: theory Automatic_Refinement.Autoref_Tool
15:43:00 JinjaThreads: theory Coinductive.Lazy_LList
15:43:00 JinjaThreads: theory Coinductive.TLList
15:43:02 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL
15:43:04 JinjaThreads: theory Native_Word.Code_Target_Bits_Int
15:43:04 JinjaThreads: theory Native_Word.Uint32
15:43:04 JinjaThreads: theory Collections.Code_Target_ICF
15:43:06 JinjaThreads: theory Coinductive.Lazy_TLList
15:43:08 JinjaThreads: theory Collections.HashCode
15:43:08 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement
15:43:08 JinjaThreads: theory Refine_Monadic.Refine_Misc
15:43:08 JinjaThreads: theory Collections.Idx_Iterator
15:43:10 JinjaThreads: theory Refine_Monadic.RefineG_Domain
15:43:10 JinjaThreads: theory Refine_Monadic.RefineG_Transfer
15:43:11 JinjaThreads: theory Refine_Monadic.RefineG_Assert
15:43:11 JinjaThreads: theory Refine_Monadic.RefineG_Recursion
15:43:11 JinjaThreads: theory Refine_Monadic.RefineG_While
15:43:11 JinjaThreads: theory Refine_Monadic.Refine_Basic
15:43:13 JinjaThreads: theory Refine_Monadic.Refine_Det
15:43:17 JinjaThreads: theory Refine_Monadic.Refine_Heuristics
15:43:17 JinjaThreads: theory Refine_Monadic.Refine_Leof
15:43:17 JinjaThreads: theory Refine_Monadic.Refine_Pfun
15:43:18 JinjaThreads: theory Refine_Monadic.Refine_More_Comb
15:43:18 JinjaThreads: theory Refine_Monadic.Refine_While
15:43:21 JinjaThreads: theory Refine_Monadic.Refine_Transfer
15:43:22 JinjaThreads: theory Refine_Monadic.Autoref_Monadic
15:43:22 JinjaThreads: theory Refine_Monadic.Refine_Automation
15:43:22 JinjaThreads: theory Refine_Monadic.Refine_Foreach
15:43:26 JinjaThreads: theory Refine_Monadic.Refine_Monadic
15:43:28 JinjaThreads: theory Collections.Gen_Iterator
15:43:28 JinjaThreads: theory Collections.Intf_Map
15:43:28 JinjaThreads: theory Collections.Intf_Set
15:43:29 JinjaThreads: theory Collections.Iterator
15:43:30 JinjaThreads: theory Collections.Array_Iterator
15:43:30 JinjaThreads: theory Collections.ICF_Spec_Base
15:43:30 JinjaThreads: theory Collections.AnnotatedListSpec
15:43:30 JinjaThreads: theory Collections.ListSpec
15:43:30 JinjaThreads: theory Collections.MapSpec
15:43:30 JinjaThreads: theory Collections.PrioSpec
15:43:30 JinjaThreads: theory Collections.PrioUniqueSpec
15:43:31 JinjaThreads: theory Collections.SetSpec
15:43:32 JinjaThreads: theory Collections.BinoPrioImpl
15:43:32 JinjaThreads: theory Collections.SkewPrioImpl
15:43:33 JinjaThreads: theory Collections.ListGA
15:43:34 JinjaThreads: theory Collections.FTAnnotatedListImpl
15:43:34 JinjaThreads: theory Collections.PrioByAnnotatedList
15:43:34 JinjaThreads: theory Collections.Fifo
15:43:37 JinjaThreads: theory HOL-Library.RBT
15:43:37 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList
15:43:38 JinjaThreads: theory Collections.RBT_add
15:43:39 JinjaThreads: theory Collections.Algos
15:43:39 JinjaThreads: theory Collections.SetIndex
15:43:39 JinjaThreads: theory Collections.SetIteratorCollectionsGA
15:43:40 JinjaThreads: theory Collections.MapGA
15:43:40 JinjaThreads: theory Collections.SetGA
15:43:43 JinjaThreads: theory Collections.FTPrioImpl
15:43:43 JinjaThreads: theory Collections.FTPrioUniqueImpl
15:43:45 JinjaThreads: theory Collections.ArrayMapImpl
15:43:45 JinjaThreads: theory Collections.ListMapImpl
15:43:45 JinjaThreads: theory Collections.ListMapImpl_Invar
15:43:45 JinjaThreads: theory Collections.TrieMapImpl
15:43:47 JinjaThreads: theory Collections.RBTMapImpl
15:43:49 JinjaThreads: theory Collections.ListSetImpl
15:43:50 JinjaThreads: theory Collections.ListSetImpl_Invar
15:43:50 JinjaThreads: theory Collections.ListSetImpl_NotDist
15:43:53 JinjaThreads: theory Collections.ArrayHashMap_Impl
15:43:55 JinjaThreads: theory Collections.ListSetImpl_Sorted
15:43:56 JinjaThreads: theory Collections.SetByMap
15:44:00 JinjaThreads: theory Collections.HashMap_Impl
15:44:01 JinjaThreads: theory Collections.ArraySetImpl
15:44:01 JinjaThreads: theory Collections.TrieSetImpl
15:44:01 JinjaThreads: theory Collections.RBTSetImpl
15:44:01 JinjaThreads: theory Collections.ArrayHashMap
15:44:03 JinjaThreads: theory Collections.HashMap
15:44:11 JinjaThreads: theory Collections.ArrayHashSet
15:44:14 JinjaThreads: theory Collections.HashSet
15:44:14 JinjaThreads: theory Collections.MapStdImpl
15:44:24 JinjaThreads: theory Collections.SetStdImpl
15:44:28 JinjaThreads: theory Collections.ICF_Impl
15:44:36 JinjaThreads: theory Collections.ICF_Refine_Monadic
15:44:37 JinjaThreads: theory Collections.ICF_Autoref
15:44:42 JinjaThreads: theory Collections.Collections
15:44:43 JinjaThreads: theory Collections.CollectionsV1
15:44:54 JinjaThreads: theory JinjaThreads.JT_ICF
15:44:54 JinjaThreads: theory JinjaThreads.Basic_Main
15:45:43 JinjaThreads: theory JinjaThreads.FWState
15:45:43 JinjaThreads: theory HOL-Library.Prefix_Order
15:45:43 JinjaThreads: theory JinjaThreads.Type
15:45:43 JinjaThreads: theory HOL-Library.Mapping
15:45:43 JinjaThreads: theory JinjaThreads.LTS
15:45:43 JinjaThreads: theory JinjaThreads.ListIndex
15:45:43 JinjaThreads: theory JinjaThreads.Orders
15:45:43 JinjaThreads: theory JinjaThreads.Semilat
15:45:44 JinjaThreads: theory JinjaThreads.Err
15:45:45 JinjaThreads: theory HOL-Library.AList_Mapping
15:45:46 JinjaThreads: theory JinjaThreads.Listn
15:45:46 JinjaThreads: theory JinjaThreads.Opt
15:45:46 JinjaThreads: theory JinjaThreads.Product
15:45:46 JinjaThreads: theory JinjaThreads.Semilattices
15:45:47 JinjaThreads: theory JinjaThreads.Typing_Framework
15:45:47 JinjaThreads: theory JinjaThreads.SemilatAlg
15:45:48 JinjaThreads: theory JinjaThreads.Decl
15:45:48 JinjaThreads: theory JinjaThreads.Kildall
15:45:48 JinjaThreads: theory JinjaThreads.LBVSpec
15:45:48 JinjaThreads: theory JinjaThreads.Bisimulation
15:45:49 JinjaThreads: theory JinjaThreads.Typing_Framework_err
15:45:49 JinjaThreads: theory JinjaThreads.LBVComplete
15:45:49 JinjaThreads: theory JinjaThreads.LBVCorrect
15:45:50 JinjaThreads: theory JinjaThreads.Abstract_BV
15:45:51 JinjaThreads: theory JinjaThreads.TypeRel
15:45:57 JinjaThreads: theory JinjaThreads.TypeRelRefine
15:45:57 JinjaThreads: theory JinjaThreads.Value
15:46:02 JinjaThreads: theory JinjaThreads.Exceptions
15:46:02 JinjaThreads: theory JinjaThreads.Heap
15:46:03 JinjaThreads: theory JinjaThreads.SystemClasses
15:46:05 JinjaThreads: theory JinjaThreads.MM
15:46:05 JinjaThreads: theory JinjaThreads.State
15:46:13 JinjaThreads: theory JinjaThreads.FWCondAction
15:46:14 JinjaThreads: theory JinjaThreads.FWInterrupt
15:46:14 JinjaThreads: theory JinjaThreads.FWLock
15:46:14 JinjaThreads: theory JinjaThreads.FWThread
15:46:14 JinjaThreads: theory JinjaThreads.FWWait
15:46:14 JinjaThreads: theory JinjaThreads.Observable_Events
15:46:17 JinjaThreads: theory JinjaThreads.FWLocking
15:46:18 JinjaThreads: theory JinjaThreads.FWLockingThread
15:46:18 JinjaThreads: theory JinjaThreads.FWWellform
15:46:20 JinjaThreads: theory JinjaThreads.FWSemantics
15:46:20 JinjaThreads: theory JinjaThreads.FWLifting
15:46:22 JinjaThreads: theory JinjaThreads.JVMState
15:46:22 JinjaThreads: theory JinjaThreads.StartConfig
15:46:22 JinjaThreads: theory JinjaThreads.JMM_Spec
15:46:23 JinjaThreads: theory JinjaThreads.FWLiftingSem
15:46:23 JinjaThreads: theory JinjaThreads.FWProgressAux
15:46:25 JinjaThreads: theory JinjaThreads.Conform
15:46:25 JinjaThreads: theory JinjaThreads.FWDeadlock
15:46:25 JinjaThreads: theory JinjaThreads.FWLTS
15:46:25 JinjaThreads: theory JinjaThreads.State_Refinement
15:46:28 JinjaThreads: theory JinjaThreads.ConformThreaded
15:46:29 JinjaThreads: theory JinjaThreads.ExternalCall
15:46:29 JinjaThreads: theory JinjaThreads.FWProgress
15:46:30 JinjaThreads: theory JinjaThreads.SC
15:46:30 JinjaThreads: theory JinjaThreads.SC_Collections
15:46:39 JinjaThreads: theory JinjaThreads.FWBisimulation
15:46:39 JinjaThreads: theory JinjaThreads.FWInitFinLift
15:46:39 JinjaThreads: theory JinjaThreads.Scheduler
15:46:39 JinjaThreads: theory JinjaThreads.JMM_DRF
15:46:39 JinjaThreads: theory JinjaThreads.Non_Speculative
15:46:39 JinjaThreads: theory JinjaThreads.SC_Legal
15:46:43 JinjaThreads: theory JinjaThreads.HB_Completion
15:46:44 JinjaThreads: theory JinjaThreads.SC_Completion
15:47:17 JinjaThreads: theory JinjaThreads.WellForm
15:47:17 JinjaThreads: theory JinjaThreads.ExternalCall_Execute
15:47:22 JinjaThreads: theory JinjaThreads.BinOp
15:47:22 JinjaThreads: theory JinjaThreads.ExternalCallWF
15:47:22 JinjaThreads: theory JinjaThreads.JMM_Heap
15:47:24 JinjaThreads: theory JinjaThreads.SemiType
15:47:30 JinjaThreads: theory JinjaThreads.JVM_SemiType
15:47:31 JinjaThreads: theory JinjaThreads.JMM_Type
15:47:32 JinjaThreads: theory JinjaThreads.JMM_Type2
15:47:34 JinjaThreads: theory JinjaThreads.Random_Scheduler
15:47:35 JinjaThreads: theory JinjaThreads.JMM_Framework
15:47:39 JinjaThreads: theory JinjaThreads.Round_Robin
15:48:13 JinjaThreads: theory JinjaThreads.SC_Schedulers
15:48:17 JinjaThreads: theory JinjaThreads.Expr
15:48:17 JinjaThreads: theory JinjaThreads.JVMInstructions
15:48:18 JinjaThreads: theory JinjaThreads.PCompiler
15:48:20 JinjaThreads: theory JinjaThreads.PCompilerRefine
15:48:35 JinjaThreads: theory JinjaThreads.JVMExceptions
15:48:35 JinjaThreads: theory JinjaThreads.JVMHeap
15:48:36 JinjaThreads: theory JinjaThreads.Effect
15:48:45 JinjaThreads: theory JinjaThreads.JVMExecInstr
15:48:49 JinjaThreads: theory JinjaThreads.CallExpr
15:48:50 JinjaThreads: theory JinjaThreads.DefAss
15:48:51 JinjaThreads: theory JinjaThreads.WWellForm
15:48:51 JinjaThreads: theory JinjaThreads.JHeap
15:48:51 JinjaThreads: theory JinjaThreads.JVMExec
15:48:52 JinjaThreads: theory JinjaThreads.WellType
15:48:54 JinjaThreads: theory JinjaThreads.ToString
15:48:56 JinjaThreads: theory JinjaThreads.JVMDefensive
15:48:59 JinjaThreads: theory JinjaThreads.J1State
15:49:01 JinjaThreads: theory JinjaThreads.SmallStep
15:49:01 JinjaThreads: theory JinjaThreads.Annotate
15:49:04 JinjaThreads: theory JinjaThreads.Compiler2
15:49:04 JinjaThreads: theory JinjaThreads.J1Heap
15:49:05 JinjaThreads: theory JinjaThreads.JVMThreaded
15:49:10 JinjaThreads: theory JinjaThreads.Compiler1
15:49:11 JinjaThreads: theory JinjaThreads.JMM_Typesafe
15:49:18 JinjaThreads: theory JinjaThreads.J1WellType
15:49:21 JinjaThreads: theory JinjaThreads.Exception_Tables
15:49:23 JinjaThreads: theory JinjaThreads.Compiler
15:49:24 JinjaThreads: theory JinjaThreads.JVM_Main
15:49:24 JinjaThreads: theory JinjaThreads.JMM_JVM
15:49:24 JinjaThreads: theory JinjaThreads.J1WellForm
15:49:24 JinjaThreads: theory JinjaThreads.JWellForm
15:49:24 JinjaThreads: theory JinjaThreads.WellTypeRT
15:49:26 JinjaThreads: theory JinjaThreads.JVMExec_Execute
15:49:27 JinjaThreads: theory JinjaThreads.JJ1WellForm
15:49:30 JinjaThreads: theory JinjaThreads.Preprocessor
15:49:33 JinjaThreads: theory JinjaThreads.JMM_Common
15:49:54 JinjaThreads: theory JinjaThreads.FWBisimDeadlock
15:49:54 JinjaThreads: theory JinjaThreads.FWBisimLift
15:49:55 JinjaThreads: theory JinjaThreads.J1
15:49:56 JinjaThreads: theory JinjaThreads.JMM_Typesafe2
15:50:20 JinjaThreads: theory JinjaThreads.BVSpec
15:50:21 JinjaThreads: theory JinjaThreads.EffectMono
15:50:21 JinjaThreads: theory JinjaThreads.BVConform
15:50:21 JinjaThreads: theory JinjaThreads.TypeComp
15:50:22 JinjaThreads: theory JinjaThreads.TF_JVM
15:50:28 JinjaThreads: theory JinjaThreads.BVExec
15:50:29 JinjaThreads: theory JinjaThreads.LBVJVM
15:50:35 JinjaThreads: theory JinjaThreads.BVSpecTypeSafe
15:50:43 JinjaThreads: theory JinjaThreads.Common_Main
15:50:51 JinjaThreads: theory JinjaThreads.BVNoTypeError
15:50:55 JinjaThreads: theory JinjaThreads.BVProgressThreaded
15:50:55 JinjaThreads: theory JinjaThreads.BCVExec
15:50:56 JinjaThreads: theory JinjaThreads.JVMExec_Execute2
15:50:59 JinjaThreads: theory JinjaThreads.JVMTau
15:51:02 JinjaThreads: theory JinjaThreads.J1Deadlock
15:51:37 JinjaThreads: theory JinjaThreads.Execs
15:52:27 JinjaThreads: theory JinjaThreads.DefAssPreservation
15:52:27 JinjaThreads: theory JinjaThreads.Threaded
15:52:28 JinjaThreads: theory JinjaThreads.Progress
15:52:37 JinjaThreads: theory JinjaThreads.TypeSafe
15:52:51 JinjaThreads: theory JinjaThreads.J1JVMBisim
15:53:02 JinjaThreads: theory JinjaThreads.J0
15:53:06 JinjaThreads: theory JinjaThreads.JMM_J
15:53:06 JinjaThreads: theory JinjaThreads.ProgressThreaded
15:53:06 JinjaThreads: theory JinjaThreads.J_Execute
15:53:08 JinjaThreads: theory JinjaThreads.DRF_JVM
15:53:13 JinjaThreads: theory JinjaThreads.JVMDeadlocked
15:53:21 JinjaThreads: theory JinjaThreads.JVM_Execute
15:53:25 JinjaThreads: theory JinjaThreads.JVM_Execute2
15:54:02 JinjaThreads: theory JinjaThreads.DRF_J
15:54:06 JinjaThreads: theory JinjaThreads.Deadlocked
15:54:08 JinjaThreads: theory JinjaThreads.BV_Main
15:54:12 JinjaThreads: theory JinjaThreads.Code_Generation
15:54:16 JinjaThreads: theory JinjaThreads.J0Bisim
15:54:23 JinjaThreads: theory JinjaThreads.J0J1Bisim
15:54:26 JinjaThreads: theory JinjaThreads.J_Main
15:54:28 JinjaThreads: theory JinjaThreads.ApprenticeChallenge
15:54:31 JinjaThreads: theory JinjaThreads.BufferExample
15:54:38 JinjaThreads: theory JinjaThreads.Java2Jinja
15:54:57 JinjaThreads: theory JinjaThreads.Examples_Main
15:55:42 JinjaThreads: theory JinjaThreads.Correctness1
15:55:42 JinjaThreads: theory JinjaThreads.Correctness1Threaded
16:04:51 JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe
16:05:08 JinjaThreads: theory JinjaThreads.Execute_Main
16:05:42 JinjaThreads: theory JinjaThreads.JMM_J_Typesafe
16:05:48 JinjaThreads: theory JinjaThreads.J1JVM
16:05:54 JinjaThreads: theory JinjaThreads.JVMJ1
16:07:31 JinjaThreads: theory JinjaThreads.Correctness2
16:10:01 JinjaThreads: theory JinjaThreads.Correctness
16:17:01 JinjaThreads: theory JinjaThreads.Compiler_Main
16:17:03 JinjaThreads: theory JinjaThreads.JMM_Compiler
16:17:07 JinjaThreads: theory JinjaThreads.SC_Interp
16:21:35 JinjaThreads: theory JinjaThreads.JMM_Interp
16:21:41 JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2
16:21:44 JinjaThreads: theory JinjaThreads.JMM
16:21:48 JinjaThreads: theory JinjaThreads.MM_Main
16:22:03 JinjaThreads: theory JinjaThreads.JinjaThreads
16:27:49 Timing JinjaThreads (8 threads, 2663.746s elapsed time, 12967.380s cpu time, 2245.480s GC time, factor 4.87)
16:27:49 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads
16:27:49 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf
16:27:49 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf
16:27:49 Finished JinjaThreads (0:45:25 elapsed time, 3:42:13 cpu time, factor 4.89)
16:27:49 Building AWN ...
16:27:50 AWN: theory AWN.Lib
16:27:50 AWN: theory AWN.TransitionSystems
16:27:50 AWN: theory AWN.AWN
16:27:51 AWN: theory AWN.Invariants
16:27:52 AWN: theory AWN.OInvariants
16:28:06 AWN: theory AWN.AWN_Cterms
16:28:06 AWN: theory AWN.AWN_SOS
16:28:07 AWN: theory AWN.OAWN_SOS
16:28:11 AWN: theory AWN.AWN_Labels
16:28:12 AWN: theory AWN.Pnet
16:28:13 AWN: theory AWN.Inv_Cterms
16:28:13 AWN: theory AWN.AWN_Invariants
16:28:14 AWN: theory AWN.Closed
16:28:14 AWN: theory AWN.AWN_SOS_Labels
16:28:15 AWN: theory AWN.Qmsg
16:28:17 AWN: theory AWN.OAWN_Invariants
16:28:17 AWN: theory AWN.ONode_Lifting
16:28:17 AWN: theory AWN.OAWN_SOS_Labels
16:28:17 AWN: theory AWN.OPnet
16:28:17 AWN: theory AWN.OPnet_Lifting
16:28:18 AWN: theory AWN.OClosed_Lifting
16:28:18 AWN: theory AWN.OClosed_Transfer
16:28:19 AWN: theory AWN.OAWN_Convert
16:28:19 AWN: theory AWN.Qmsg_Lifting
16:28:20 AWN: theory AWN.AWN_Main
16:28:20 AWN: theory AWN.Toy
16:28:36 AWN: theory AWN.AWN_Term_Graph
16:29:12 Timing AWN (8 threads, 50.002s elapsed time, 241.064s cpu time, 8.624s GC time, factor 4.82)
16:29:12 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN
16:29:12 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf
16:29:12 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf
16:29:12 Finished AWN (0:01:22 elapsed time, 0:05:07 cpu time, factor 3.74)
16:29:12 Running AODV ...
16:29:14 AODV: theory AODV.Aodv_Basic
16:29:16 AODV: theory AODV.A_Norreqid
16:29:16 AODV: theory AODV.Aodv_Data
16:29:16 AODV: theory AODV.Aodv_Message
16:29:16 AODV: theory AODV.B_Fwdrreps
16:29:16 AODV: theory AODV.C_Gtobcast
16:29:16 AODV: theory AODV.D_Fwdrreqs
16:29:16 AODV: theory AODV.E_All_ABCD
16:29:16 AODV: theory AODV.A_Aodv_Data
16:29:16 AODV: theory AODV.A_Aodv_Message
16:29:16 AODV: theory AODV.E_Aodv_Data
16:29:16 AODV: theory AODV.C_Aodv_Data
16:29:16 AODV: theory AODV.C_Aodv_Message
16:29:16 AODV: theory AODV.B_Aodv_Data
16:29:18 AODV: theory AODV.B_Aodv_Message
16:29:18 AODV: theory AODV.C_Fresher
16:29:18 AODV: theory AODV.D_Aodv_Data
16:29:18 AODV: theory AODV.D_Aodv_Message
16:29:19 AODV: theory AODV.A_Fresher
16:29:19 AODV: theory AODV.B_Fresher
16:29:19 AODV: theory AODV.E_Fresher
16:29:19 AODV: theory AODV.Fresher
16:29:19 AODV: theory AODV.E_Aodv_Message
16:29:20 AODV: theory AODV.A_Aodv
16:29:20 AODV: theory AODV.Aodv
16:29:20 AODV: theory AODV.C_Aodv
16:29:20 AODV: theory AODV.B_Aodv
16:29:20 AODV: theory AODV.D_Fresher
16:29:20 AODV: theory AODV.D_Aodv
16:29:21 AODV: theory AODV.E_Aodv
16:30:22 AODV: theory AODV.C_Aodv_Predicates
16:30:22 AODV: theory AODV.C_OAodv
16:30:22 AODV: theory AODV.C_Loop_Freedom
16:30:22 AODV: theory AODV.C_Quality_Increases
16:30:22 AODV: theory AODV.C_Seq_Invariants
16:30:23 AODV: theory AODV.C_Global_Invariants
16:30:26 AODV: theory AODV.C_Aodv_Loop_Freedom
16:30:40 AODV: theory AODV.Aodv_Predicates
16:30:40 AODV: theory AODV.Loop_Freedom
16:30:40 AODV: theory AODV.Quality_Increases
16:30:40 AODV: theory AODV.Seq_Invariants
16:30:41 AODV: theory AODV.OAodv
16:30:41 AODV: theory AODV.Global_Invariants
16:30:42 AODV: theory AODV.Aodv_Loop_Freedom
16:30:52 AODV: theory AODV.A_Aodv_Predicates
16:30:53 AODV: theory AODV.A_Loop_Freedom
16:30:53 AODV: theory AODV.A_Quality_Increases
16:30:54 AODV: theory AODV.A_Seq_Invariants
16:30:55 AODV: theory AODV.A_OAodv
16:30:56 AODV: theory AODV.A_Global_Invariants
16:30:57 AODV: theory AODV.A_Aodv_Loop_Freedom
16:30:58 AODV: theory AODV.E_Aodv_Predicates
16:30:58 AODV: theory AODV.E_OAodv
16:30:58 AODV: theory AODV.E_Loop_Freedom
16:30:59 AODV: theory AODV.E_Quality_Increases
16:30:59 AODV: theory AODV.E_Seq_Invariants
16:30:59 AODV: theory AODV.B_Aodv_Predicates
16:30:59 AODV: theory AODV.B_Loop_Freedom
16:31:00 AODV: theory AODV.B_Quality_Increases
16:31:00 AODV: theory AODV.B_Seq_Invariants
16:31:00 AODV: theory AODV.B_OAodv
16:31:00 AODV: theory AODV.E_Global_Invariants
16:31:01 AODV: theory AODV.B_Global_Invariants
16:31:02 AODV: theory AODV.E_Aodv_Loop_Freedom
16:31:02 AODV: theory AODV.B_Aodv_Loop_Freedom
16:31:08 AODV: theory AODV.D_Aodv_Predicates
16:31:08 AODV: theory AODV.D_OAodv
16:31:09 AODV: theory AODV.D_Loop_Freedom
16:31:09 AODV: theory AODV.D_Quality_Increases
16:31:09 AODV: theory AODV.D_Seq_Invariants
16:31:10 AODV: theory AODV.D_Global_Invariants
16:31:11 AODV: theory AODV.D_Aodv_Loop_Freedom
16:31:19 AODV: theory AODV.All
19:16:19 Timing AODV (8 threads, 10008.481s elapsed time, 54052.184s cpu time, 4496.788s GC time, factor 5.40)
19:16:19 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV
19:16:19 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/document.pdf
19:16:19 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/outline.pdf
19:16:19 Finished AODV (2:47:03 elapsed time, 15:01:18 cpu time, factor 5.39)
19:16:19 Building HOL-Library ...
19:16:22 HOL-Library: theory HOL-Library.AList
19:16:22 HOL-Library: theory HOL-Library.Adhoc_Overloading
19:16:22 HOL-Library: theory HOL-Library.BNF_Axiomatization
19:16:22 HOL-Library: theory HOL-Library.Bit
19:16:22 HOL-Library: theory HOL-Library.Boolean_Algebra
19:16:22 HOL-Library: theory HOL-Library.BNF_Corec
19:16:22 HOL-Library: theory HOL-Library.Cancellation
19:16:22 HOL-Library: theory HOL-Library.Cardinal_Notations
19:16:22 HOL-Library: theory HOL-Library.Case_Converter
19:16:22 HOL-Library: theory HOL-Library.Monad_Syntax
19:16:22 HOL-Library: theory HOL-Library.Char_ord
19:16:22 HOL-Library: theory HOL-Library.State_Monad
19:16:22 HOL-Library: theory HOL-Library.Code_Abstract_Nat
19:16:22 HOL-Library: theory HOL-Library.Code_Prolog
19:16:22 HOL-Library: theory HOL-Library.Code_Lazy
19:16:22 HOL-Library: theory HOL-Library.Simps_Case_Conv
19:16:23 HOL-Library: theory HOL-Library.Extended
19:16:23 HOL-Library: theory HOL-Library.Multiset
19:16:23 HOL-Library: theory HOL-Library.Code_Binary_Nat
19:16:23 HOL-Library: theory HOL-Library.Code_Target_Nat
19:16:23 HOL-Library: theory HOL-Library.Code_Target_Int
19:16:23 HOL-Library: theory HOL-Library.Code_Test
19:16:24 HOL-Library: theory HOL-Library.Comparator
19:16:24 HOL-Library: theory HOL-Library.Code_Target_Numeral
19:16:24 HOL-Library: theory HOL-Library.Conditional_Parametricity
19:16:24 HOL-Library: theory HOL-Library.Datatype_Records
19:16:25 HOL-Library: theory HOL-Library.Debug
19:16:25 HOL-Library: theory HOL-Library.Disjoint_Sets
19:16:25 HOL-Library: theory HOL-Library.DAList
19:16:25 HOL-Library: theory HOL-Library.Dlist
19:16:25 HOL-Library: theory HOL-Library.Fun_Lexorder
19:16:25 HOL-Library: theory HOL-Library.FuncSet
19:16:25 HOL-Library: theory HOL-Library.Function_Algebras
19:16:25 HOL-Library: theory HOL-Library.Groups_Big_Fun
19:16:25 HOL-Library: theory HOL-Library.Function_Division
19:16:25 HOL-Library: theory HOL-Library.IArray
19:16:26 HOL-Library: theory HOL-Library.Infinite_Set
19:16:26 HOL-Library: theory HOL-Library.LaTeXsugar
19:16:26 HOL-Library: theory HOL-Library.Lattice_Constructions
19:16:26 HOL-Library: theory HOL-Library.Equipollence
19:16:26 HOL-Library: theory HOL-Library.Lattice_Syntax
19:16:26 HOL-Library: theory HOL-Library.Combine_PER
19:16:26 HOL-Library: theory HOL-Library.Omega_Words_Fun
19:16:26 HOL-Library: theory HOL-Library.Ramsey
19:16:26 HOL-Library: theory HOL-Library.Complete_Partial_Order2
19:16:26 HOL-Library: theory HOL-Library.ListVector
19:16:27 HOL-Library: theory HOL-Library.List_Lexorder
19:16:27 HOL-Library: theory HOL-Library.Mapping
19:16:27 HOL-Library: theory HOL-Library.More_List
19:16:27 HOL-Library: theory HOL-Library.Nat_Bijection
19:16:27 HOL-Library: theory HOL-Library.Old_Datatype
19:16:27 HOL-Library: theory HOL-Library.Old_Recdef
19:16:27 HOL-Library: theory HOL-Library.Stream
19:16:29 HOL-Library: theory HOL-Library.Open_State_Syntax
19:16:29 HOL-Library: theory HOL-Library.Option_ord
19:16:29 HOL-Library: theory HOL-Library.AList_Mapping
19:16:30 HOL-Library: theory HOL-Library.Parallel
19:16:30 HOL-Library: theory HOL-Library.Pattern_Aliases
19:16:30 HOL-Library: theory HOL-Library.Perm
19:16:30 HOL-Library: theory HOL-Library.Phantom_Type
19:16:31 HOL-Library: theory HOL-Library.Power_By_Squaring
19:16:31 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
19:16:31 HOL-Library: theory HOL-Library.Preorder
19:16:31 HOL-Library: theory HOL-Library.Product_Lexorder
19:16:31 HOL-Library: theory HOL-Library.Product_Plus
19:16:31 HOL-Library: theory HOL-Library.Quotient_Syntax
19:16:31 HOL-Library: theory HOL-Library.Product_Order
19:16:31 HOL-Library: theory HOL-Library.Quotient_Option
19:16:32 HOL-Library: theory HOL-Library.Cardinality
19:16:32 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
19:16:32 HOL-Library: theory HOL-Library.Quotient_Product
19:16:32 HOL-Library: theory HOL-Library.Quotient_Set
19:16:32 HOL-Library: theory HOL-Library.Finite_Lattice
19:16:32 HOL-Library: theory HOL-Library.Quotient_Sum
19:16:32 HOL-Library: theory HOL-Library.Quotient_List
19:16:32 HOL-Library: theory HOL-Library.Quotient_Type
19:16:32 HOL-Library: theory HOL-Library.RBT_Impl
19:16:32 HOL-Library: theory HOL-Library.Realizers
19:16:32 HOL-Library: theory HOL-Library.DAList_Multiset
19:16:32 HOL-Library: theory HOL-Library.Multiset_Order
19:16:33 HOL-Library: theory HOL-Library.Permutation
19:16:33 HOL-Library: theory HOL-Library.Permutations
19:16:33 HOL-Library: theory HOL-Library.Reflection
19:16:33 HOL-Library: theory HOL-Library.Refute
19:16:33 HOL-Library: theory HOL-Library.Rewrite
19:16:33 HOL-Library: theory HOL-Library.Set_Algebras
19:16:33 HOL-Library: theory HOL-Library.Numeral_Type
19:16:34 HOL-Library: theory HOL-Library.Sorting_Algorithms
19:16:34 HOL-Library: theory HOL-Library.Stirling
19:16:34 HOL-Library: theory HOL-Library.Sublist
19:16:34 HOL-Library: theory HOL-Library.Transitive_Closure_Table
19:16:34 HOL-Library: theory HOL-Library.Tree
19:16:35 HOL-Library: theory HOL-Library.Uprod
19:16:36 HOL-Library: theory HOL-Library.While_Combinator
19:16:36 HOL-Library: theory HOL-Library.Countable
19:16:37 HOL-Library: theory HOL-Library.Type_Length
19:16:37 HOL-Library: theory HOL-Library.BigO
19:16:37 HOL-Library: theory HOL-Library.Saturated
19:16:37 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
19:16:38 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
19:16:38 HOL-Library: theory HOL-Library.Diagonal_Subsequence
19:16:38 HOL-Library: theory HOL-Library.Discrete
19:16:38 HOL-Library: theory HOL-Library.Prefix_Order
19:16:38 HOL-Library: theory HOL-Library.Subseq_Order
19:16:38 HOL-Library: theory HOL-Library.Going_To_Filter
19:16:38 HOL-Library: theory HOL-Library.Indicator_Function
19:16:38 HOL-Library: theory HOL-Library.Landau_Symbols
19:16:38 HOL-Library: theory HOL-Library.Lattice_Algebras
19:16:38 HOL-Library: theory HOL-Library.Liminf_Limsup
19:16:38 HOL-Library: theory HOL-Library.Countable_Set
19:16:39 HOL-Library: theory HOL-Library.FSet
19:16:39 HOL-Library: theory HOL-Library.Log_Nat
19:16:39 HOL-Library: theory HOL-Library.Lub_Glb
19:16:39 HOL-Library: theory HOL-Library.Countable_Complete_Lattices
19:16:39 HOL-Library: theory HOL-Library.Countable_Set_Type
19:16:40 HOL-Library: theory HOL-Library.Set_Idioms
19:16:40 HOL-Library: theory HOL-Library.Multiset_Permutations
19:16:40 HOL-Library: theory HOL-Library.Tree_Multiset
19:16:41 HOL-Library: theory HOL-Library.Nonpos_Ints
19:16:41 HOL-Library: theory HOL-Library.OptionalSugar
19:16:42 HOL-Library: theory HOL-Library.Periodic_Fun
19:16:42 HOL-Library: theory HOL-Library.Quadratic_Discriminant
19:16:42 HOL-Library: theory HOL-Library.Sum_of_Squares
19:16:42 HOL-Library: theory HOL-Library.Tree_Real
19:16:43 HOL-Library: theory HOL-Library.Order_Continuity
19:16:44 HOL-Library: theory HOL-Library.Extended_Nat
19:16:45 HOL-Library: theory HOL-Library.Finite_Map
19:16:45 HOL-Library: theory HOL-Library.Float
19:16:45 HOL-Library: theory HOL-Library.Extended_Real
19:16:46 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
19:16:52 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
19:17:09 HOL-Library: theory HOL-Library.Library
19:17:28 HOL-Library: theory HOL-Library.RBT
19:17:29 HOL-Library: theory HOL-Library.RBT_Mapping
19:17:29 HOL-Library: theory HOL-Library.RBT_Set
19:19:23 Timing HOL-Library (8 threads, 104.868s elapsed time, 670.000s cpu time, 38.920s GC time, factor 6.39)
19:19:23 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library
19:19:23 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf
19:19:23 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf
19:19:23 Finished HOL-Library (0:03:00 elapsed time, 0:14:21 cpu time, factor 4.78)
19:19:23 Building ConcurrentIMP ...
19:19:24 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred
19:19:25 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang
19:19:39 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg
19:19:41 ConcurrentIMP: theory ConcurrentIMP.CIMP
19:19:41 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer_ex
19:19:41 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer_ex
19:20:13 Timing ConcurrentIMP (8 threads, 21.862s elapsed time, 53.000s cpu time, 2.696s GC time, factor 2.42)
19:20:13 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP
19:20:13 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf
19:20:13 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf
19:20:13 Finished ConcurrentIMP (0:00:49 elapsed time, 0:01:48 cpu time, factor 2.20)
19:20:13 Running ConcurrentGC ...
19:20:14 ConcurrentGC: theory ConcurrentGC.Model
19:20:35 ConcurrentGC: theory ConcurrentGC.Tactics
19:20:45 ConcurrentGC: theory ConcurrentGC.Proofs_basis
19:20:49 ConcurrentGC: theory ConcurrentGC.TSO
19:21:08 ConcurrentGC: theory ConcurrentGC.Handshakes
19:25:16 ConcurrentGC: theory ConcurrentGC.MarkObject
19:28:40 ConcurrentGC: theory ConcurrentGC.StrongTricolour
19:30:08 ConcurrentGC: theory ConcurrentGC.Proofs
19:30:11 ConcurrentGC: theory ConcurrentGC.Concrete_heap
19:30:15 ConcurrentGC: theory ConcurrentGC.Concrete
21:47:28 Timing ConcurrentGC (8 threads, 8826.654s elapsed time, 32755.748s cpu time, 1897.660s GC time, factor 3.71)
21:47:28 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC
21:47:28 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf
21:47:29 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf
21:47:29 Finished ConcurrentGC (2:27:13 elapsed time, 9:06:08 cpu time, factor 3.71)
21:47:29 Building HOL-Word ...
21:47:30 HOL-Word: theory HOL-Word.Misc_Typedef
21:47:30 HOL-Word: theory HOL-Word.Misc_Numeric
21:47:30 HOL-Word: theory HOL-Library.Boolean_Algebra
21:47:30 HOL-Word: theory HOL-Word.Bits
21:47:30 HOL-Word: theory HOL-Library.Phantom_Type
21:47:30 HOL-Word: theory HOL-Library.Bit
21:47:30 HOL-Word: theory HOL-Word.Bit_Representation
21:47:31 HOL-Word: theory HOL-Word.Bits_Bit
21:47:31 HOL-Word: theory HOL-Word.Word_Miscellaneous
21:47:31 HOL-Word: theory HOL-Word.Bits_Int
21:47:31 HOL-Word: theory HOL-Library.Cardinality
21:47:33 HOL-Word: theory HOL-Library.Numeral_Type
21:47:33 HOL-Word: theory HOL-Word.Bit_Comparison
21:47:33 HOL-Word: theory HOL-Word.Bool_List_Representation
21:47:35 HOL-Word: theory HOL-Library.Type_Length
21:47:35 HOL-Word: theory HOL-Word.Word
21:47:41 HOL-Word: theory HOL-Word.WordBitwise
21:47:42 HOL-Word: theory HOL-Word.WordExamples
21:48:03 Timing HOL-Word (8 threads, 13.699s elapsed time, 69.264s cpu time, 2.384s GC time, factor 5.06)
21:48:03 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word
21:48:03 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf
21:48:03 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf
21:48:03 Finished HOL-Word (0:00:33 elapsed time, 0:01:48 cpu time, factor 3.21)
21:48:03 Building Word_Lib ...
21:48:04 Word_Lib: theory Word_Lib.Hex_Words
21:48:04 Word_Lib: theory Word_Lib.Signed_Words
21:48:04 Word_Lib: theory Word_Lib.Word_Type_Syntax
21:48:04 Word_Lib: theory HOL-Library.Sublist
21:48:04 Word_Lib: theory Word_Lib.Enumeration
21:48:04 Word_Lib: theory Word_Lib.HOL_Lemmas
21:48:04 Word_Lib: theory Word_Lib.More_Divides
21:48:04 Word_Lib: theory Word_Lib.Norm_Words
21:48:04 Word_Lib: theory Word_Lib.WordBitwise_Signed
21:48:05 Word_Lib: theory Word_Lib.Word_Syntax
21:48:06 Word_Lib: theory Word_Lib.Word_Lib
21:48:07 Word_Lib: theory Word_Lib.Word_Enum
21:48:07 Word_Lib: theory Word_Lib.Aligned
21:48:08 Word_Lib: theory Word_Lib.Word_Setup_32
21:48:08 Word_Lib: theory Word_Lib.Word_Setup_64
21:48:08 Word_Lib: theory Word_Lib.Word_Next
21:48:08 Word_Lib: theory Word_Lib.Word_Lemmas
21:48:15 Word_Lib: theory Word_Lib.Word_Lemmas_32
21:48:16 Word_Lib: theory Word_Lib.Word_Lemmas_64
21:49:35 Timing Word_Lib (8 threads, 73.089s elapsed time, 194.104s cpu time, 4.860s GC time, factor 2.66)
21:49:35 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib
21:49:35 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf
21:49:35 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf
21:49:35 Finished Word_Lib (0:01:31 elapsed time, 0:03:49 cpu time, factor 2.51)
21:49:35 Building IP_Addresses ...
21:49:36 IP_Addresses: theory HOL-Eisbach.Eisbach
21:49:36 IP_Addresses: theory HOL-Library.Infinite_Set
21:49:36 IP_Addresses: theory IP_Addresses.NumberWang_IPv6
21:49:36 IP_Addresses: theory HOL-Library.Option_ord
21:49:36 IP_Addresses: theory IP_Addresses.NumberWang_IPv4
21:49:36 IP_Addresses: theory HOL-Library.Cancellation
21:49:38 IP_Addresses: theory HOL-Library.Multiset
21:49:44 IP_Addresses: theory HOL-ex.Quicksort
21:49:45 IP_Addresses: theory Automatic_Refinement.Misc
21:49:53 IP_Addresses: theory HOL-Library.Code_Abstract_Nat
21:49:53 IP_Addresses: theory HOL-Library.Product_Lexorder
21:49:53 IP_Addresses: theory IP_Addresses.Hs_Compat
21:49:53 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
21:49:53 IP_Addresses: theory IP_Addresses.WordInterval
21:49:53 IP_Addresses: theory HOL-Library.Code_Target_Nat
21:49:53 IP_Addresses: theory IP_Addresses.Lib_List_toString
21:49:53 IP_Addresses: theory IP_Addresses.Lib_Word_toString
21:50:05 IP_Addresses: theory IP_Addresses.IP_Address
21:50:05 IP_Addresses: theory IP_Addresses.WordInterval_Sorted
21:50:12 IP_Addresses: theory IP_Addresses.IPv4
21:50:12 IP_Addresses: theory IP_Addresses.IPv6
21:50:12 IP_Addresses: theory IP_Addresses.Prefix_Match
21:50:13 IP_Addresses: theory IP_Addresses.CIDR_Split
21:51:56 IP_Addresses: theory IP_Addresses.IP_Address_Parser
21:51:56 IP_Addresses: theory IP_Addresses.IP_Address_toString
21:51:58 IP_Addresses: theory IP_Addresses.Prefix_Match_toString
21:55:47 Timing IP_Addresses (8 threads, 326.760s elapsed time, 945.024s cpu time, 56.864s GC time, factor 2.89)
21:55:47 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses
21:55:47 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf
21:55:47 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf
21:55:47 Finished IP_Addresses (0:06:10 elapsed time, 0:17:27 cpu time, factor 2.83)
21:55:47 Building Simple_Firewall ...
21:55:49 Simple_Firewall: theory HOL-Library.Char_ord
21:55:49 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
21:55:49 Simple_Firewall: theory Simple_Firewall.GroupF
21:55:49 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
21:55:49 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
21:55:49 Simple_Firewall: theory Simple_Firewall.Option_Helpers
21:55:49 Simple_Firewall: theory Simple_Firewall.List_Product_More
21:55:49 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
21:55:49 Simple_Firewall: theory Simple_Firewall.Iface
21:55:50 Simple_Firewall: theory Simple_Firewall.L4_Protocol
21:55:54 Simple_Firewall: theory Simple_Firewall.Simple_Packet
21:55:54 Simple_Firewall: theory Simple_Firewall.Primitives_toString
21:55:57 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
21:56:01 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
21:56:01 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString
21:56:05 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
21:56:05 Simple_Firewall: theory Simple_Firewall.Shadowed
21:56:05 Simple_Firewall: theory Simple_Firewall.Service_Matrix
21:56:43 Timing Simple_Firewall (8 threads, 26.157s elapsed time, 99.148s cpu time, 4.568s GC time, factor 3.79)
21:56:43 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall
21:56:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf
21:56:43 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf
21:56:43 Finished Simple_Firewall (0:00:55 elapsed time, 0:02:44 cpu time, factor 2.99)
21:56:43 Building Routing ...
21:56:45 Routing: theory HOL-Library.Adhoc_Overloading
21:56:45 Routing: theory Routing.Linorder_Helper
21:56:45 Routing: theory HOL-Library.Monad_Syntax
21:56:46 Routing: theory Routing.Routing_Table
21:56:51 Routing: theory Routing.IpRoute_Parser
21:56:51 Routing: theory Routing.Linux_Router
21:57:17 Timing Routing (8 threads, 13.096s elapsed time, 37.104s cpu time, 0.976s GC time, factor 2.83)
21:57:17 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing
21:57:17 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf
21:57:17 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf
21:57:17 Finished Routing (0:00:33 elapsed time, 0:01:16 cpu time, factor 2.30)
21:57:17 Building Iptables_Semantics ...
21:57:18 Iptables_Semantics: theory Iptables_Semantics.List_Misc
21:57:18 Iptables_Semantics: theory Iptables_Semantics.Negation_Type
21:57:21 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
21:57:22 Iptables_Semantics: theory HOL-Library.LaTeXsugar
21:57:22 Iptables_Semantics: theory HOL-Library.Code_Target_Int
21:57:22 Iptables_Semantics: theory Native_Word.More_Bits_Int
21:57:22 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
21:57:22 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
21:57:22 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
21:57:22 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
21:57:22 Iptables_Semantics: theory Iptables_Semantics.Ternary
21:57:23 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
21:57:23 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
21:57:23 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
21:57:23 Iptables_Semantics: theory Iptables_Semantics.IpAddresses
21:57:23 Iptables_Semantics: theory Iptables_Semantics.Word_Upto
21:57:24 Iptables_Semantics: theory Iptables_Semantics.Ports
21:57:25 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
21:57:26 Iptables_Semantics: theory Native_Word.Bits_Integer
21:57:27 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
21:57:45 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
21:57:45 Iptables_Semantics: theory Iptables_Semantics.Semantics
21:57:45 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
21:57:45 Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int
21:57:47 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
21:57:47 Iptables_Semantics: theory Iptables_Semantics.Matching
21:57:48 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
21:57:48 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
21:57:48 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
21:57:48 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
21:57:49 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
21:57:50 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
21:57:50 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
21:57:50 Iptables_Semantics: theory Iptables_Semantics.Optimizing
21:57:50 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
21:57:51 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
21:57:52 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
21:57:55 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
21:57:57 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
21:58:00 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
21:58:00 Iptables_Semantics: theory Iptables_Semantics.Ipassmt
21:58:05 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
21:58:59 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
21:58:59 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
21:58:59 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
21:58:59 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
21:59:00 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
21:59:00 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
21:59:00 Iptables_Semantics: theory Iptables_Semantics.No_Spoof
21:59:00 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
21:59:00 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
21:59:12 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
21:59:20 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
21:59:24 Iptables_Semantics: theory Iptables_Semantics.Transform
21:59:30 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
21:59:32 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
21:59:39 Iptables_Semantics: theory Iptables_Semantics.Code_Interface
21:59:39 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
21:59:40 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
21:59:41 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
21:59:41 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
21:59:49 Iptables_Semantics: theory Iptables_Semantics.Parser
21:59:49 Iptables_Semantics: theory Iptables_Semantics.Documentation
21:59:50 Iptables_Semantics: theory Iptables_Semantics.Code_haskell
22:01:18 Timing Iptables_Semantics (8 threads, 177.500s elapsed time, 795.840s cpu time, 62.504s GC time, factor 4.48)
22:01:18 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics
22:01:18 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf
22:01:18 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf
22:01:18 Finished Iptables_Semantics (0:03:59 elapsed time, 0:16:23 cpu time, factor 4.11)
22:01:18 Building Iptables_Semantics_Examples ...
22:01:20 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com
22:01:20 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company
22:01:20 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof
22:01:20 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6
22:01:20 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test
22:01:20 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing
22:01:20 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example
22:01:20 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall
22:01:22 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test
22:01:27 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail
22:01:28 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples
22:01:28 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed
22:01:29 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation
22:07:16 Timing Iptables_Semantics_Examples (8 threads, 327.888s elapsed time, 2140.580s cpu time, 227.228s GC time, factor 6.53)
22:07:16 Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples
22:07:16 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf
22:07:16 Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf
22:07:16 Finished Iptables_Semantics_Examples (0:05:56 elapsed time, 0:36:38 cpu time, factor 6.16)
22:07:16 Running Iptables_Semantics_Examples_Big ...
22:07:18 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern
22:07:18 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated
22:07:18 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small
22:07:18 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3
22:07:18 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall
22:12:34 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large
00:02:31 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW
00:53:15 Build timed out (after 1,400 minutes). Marking the build as aborted.
00:53:15 Build was aborted
00:53:15 Archiving artifacts
00:53:17 Started calculate disk usage of build
00:53:17 Finished Calculation of disk usage of build in 0 seconds
00:53:17 Started calculate disk usage of workspace
00:53:19 Finished Calculation of disk usage of workspace in  2 second
00:53:19 No emails were triggered.
00:53:19 Finished: ABORTED