Started by an SCM change
Running as SYSTEM
[EnvInject] - Loading node environment variables.
Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow
[isabelle-nightly-slow] $ hg showconfig paths.default
[isabelle-nightly-slow] $ hg pull --rev default
pulling from http://isabelle.in.tum.de/repos/isabelle/
no changes found
[isabelle-nightly-slow] $ hg update --clean --rev default
0 files updated, 0 files merged, 0 files removed, 0 files unresolved
[isabelle-nightly-slow] $ hg --config extensions.purge= clean --all
[isabelle-nightly-slow] $ hg log --rev . --template {node}
[isabelle-nightly-slow] $ hg log --rev . --template {rev}
[isabelle-nightly-slow] $ hg log --rev 49ae62f849017ceef7ad7da12e8f824487672152 --template exists\n
exists
[isabelle-nightly-slow] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(49ae62f849017ceef7ad7da12e8f824487672152)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
[afp] $ hg pull --rev default
pulling from https://bitbucket.org/isa-afp/afp-devel/
no changes found
[afp] $ hg update --clean --rev default
15 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg --config extensions.purge= clean --all
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg log --rev ef5c588d2a90519ab94547e5c7b99f470c95d0f9 --template exists\n
exists
[afp] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(ef5c588d2a90519ab94547e5c7b99f470c95d0f9)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins4242490235834895215.sh
+ Admin/jenkins/run_build slow
+ set -e
+ PROFILE=slow
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### Building graph browser ...
warning: [options] bootstrap class path not set in conjunction with -source 6
warning: [options] source value 6 is obsolete and will be removed in a future release
warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
Note: Some input files use or override a deprecated API.
Note: Recompile with -Xlint:deprecation for details.
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
3 warnings
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
+ bin/isabelle ocaml_setup
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
opam update
[NOTE] Package zarith is already installed (current version is 1.7).
+ bin/isabelle ghc_setup
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
The Glorious Glasgow Haskell Compilation System, version 8.4.4
+ bin/isabelle ci_build_slow
=== CONFIGURATION ===
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64-linux"
ML_SYSTEM="polyml-5.8"
ML_OPTIONS="-H 4000 --maxheap 20G"
jobs = 1, threads = 8, numa = false
=== BUILD ===
Build started at Fri, 20 Sep 2019 23:34:14 GMT
Isabelle id 49ae62f84901
Build for AFP id a2c03373dc20
=== LOG ===
Session Pure/Pure
Session FOL/FOL
Session HOL/HOL (main)
Session AFP/AWN (AFP)
Session AFP/AODV (AFP slow)
Session HOL/HOL-Cardinals (timing)
Session HOL/HOL-Eisbach
Session HOL/HOL-Library (main timing)
Session AFP/Binomial-Heaps (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/ConcurrentGC (AFP slow)
Session AFP/FinFun (AFP)
Session AFP/Finger-Trees (AFP)
Session HOL/HOL-Computational_Algebra (main timing)
Session HOL/HOL-Algebra (main timing)
Session HOL/HOL-Analysis (main timing)
Session AFP/Coinductive (AFP)
Session HOL/HOL-Number_Theory (main timing)
Session HOL/HOL-ex (timing)
Session AFP/Automatic_Refinement (AFP)
Session HOL/HOL-Imperative_HOL (timing)
Session AFP/Trie (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Flyspeck-Tame-Computation (AFP slow very_slow)
Session HOL/HOL-Word (main timing)
Session AFP/Native_Word (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Collections (AFP)
Session AFP/Word_Lib (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Routing (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow)
Session AFP/JinjaThreads (AFP slow)
Building Pure ...
Pure: theory Pure
Pure: theory ML_Bootstrap
Pure: theory Pure.Sessions
Timing Pure (1 threads, 1.058s elapsed time, 1.054s cpu time, 0.039s GC time, factor 1.00)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure
Timing Pure (1 threads, 1.058s elapsed time, 1.054s cpu time, 0.039s GC time, factor 1.00)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure
Finished Pure (0:00:21 elapsed time, 0:00:21 cpu time, factor 0.99)
Building HOL ...
HOL: theory HOL.Code_Generator
HOL: theory HOL.HOL
HOL: theory HOL.Argo
HOL: theory HOL.Ctr_Sugar
HOL: theory HOL.Orderings
HOL: theory HOL.Groups
HOL: theory HOL.SAT
HOL: theory HOL.Lattices
HOL: theory HOL.Set
HOL: theory HOL.Fun
HOL: theory HOL.Typedef
HOL: theory HOL.Complete_Lattices
HOL: theory HOL.Rings
HOL: theory HOL.Inductive
HOL: theory HOL.Product_Type
HOL: theory HOL.Sum_Type
HOL: theory HOL.Complete_Partial_Order
HOL: theory HOL.Nat
HOL: theory HOL.Fields
HOL: theory HOL.Meson
HOL: theory HOL.ATP
HOL: theory HOL.Metis
HOL: theory HOL.Finite_Set
HOL: theory HOL.Relation
HOL: theory HOL.Transitive_Closure
HOL: theory HOL.Wellfounded
HOL: theory HOL.Fun_Def_Base
HOL: theory HOL.Hilbert_Choice
HOL: theory HOL.Wfrec
HOL: theory HOL.Order_Relation
HOL: theory HOL.BNF_Wellorder_Relation
HOL: theory HOL.BNF_Wellorder_Embedding
HOL: theory HOL.Zorn
HOL: theory HOL.BNF_Wellorder_Constructions
HOL: theory HOL.BNF_Cardinal_Order_Relation
HOL: theory HOL.BNF_Cardinal_Arithmetic
HOL: theory HOL.BNF_Def
HOL: theory HOL.BNF_Composition
HOL: theory HOL.Basic_BNFs
HOL: theory HOL.BNF_Fixpoint_Base
HOL: theory HOL.BNF_Least_Fixpoint
HOL: theory HOL.Basic_BNF_LFPs
HOL: theory HOL.Transfer
HOL: theory HOL.Num
HOL: theory HOL.Power
HOL: theory HOL.Groups_Big
HOL: theory HOL.Equiv_Relations
HOL: theory HOL.Lifting
HOL: theory HOL.Lifting_Set
HOL: theory HOL.Option
HOL: theory HOL.Quotient
HOL: theory HOL.Extraction
HOL: theory HOL.Lattices_Big
HOL: theory HOL.Partial_Function
HOL: theory HOL.Fun_Def
HOL: theory HOL.Int
HOL: theory HOL.Euclidean_Division
HOL: theory HOL.Parity
HOL: theory HOL.Divides
HOL: theory HOL.Code_Numeral
HOL: theory HOL.Set_Interval
HOL: theory HOL.Numeral_Simprocs
HOL: theory HOL.SMT
HOL: theory HOL.Semiring_Normalization
HOL: theory HOL.Groebner_Basis
HOL: theory HOL.Conditionally_Complete_Lattices
HOL: theory HOL.Presburger
HOL: theory HOL.Filter
HOL: theory HOL.Sledgehammer
HOL: theory HOL.List
HOL: theory HOL.Groups_List
HOL: theory HOL.Map
HOL: theory HOL.Factorial
HOL: theory HOL.Enum
HOL: theory HOL.GCD
HOL: theory HOL.Random
HOL: theory HOL.Binomial
HOL: theory HOL.String
HOL: theory HOL.BNF_Greatest_Fixpoint
HOL: theory HOL.Predicate
HOL: theory HOL.Typerep
HOL: theory HOL.Lazy_Sequence
HOL: theory HOL.Limited_Sequence
HOL: theory HOL.Code_Evaluation
HOL: theory HOL.Quickcheck_Random
HOL: theory HOL.Quickcheck_Exhaustive
HOL: theory HOL.Quickcheck_Narrowing
HOL: theory HOL.Random_Pred
HOL: theory HOL.Random_Sequence
HOL: theory HOL.Record
HOL: theory HOL.Predicate_Compile
HOL: theory HOL.Nitpick
HOL: theory HOL.Nunchaku
HOL: theory Main
HOL: theory HOL.Archimedean_Field
HOL: theory HOL.Hull
HOL: theory HOL.Topological_Spaces
HOL: theory HOL.Modules
HOL: theory HOL.Vector_Spaces
HOL: theory HOL.Rat
HOL: theory HOL.Real
HOL: theory HOL.Real_Vector_Spaces
HOL: theory HOL.Inequalities
HOL: theory HOL.Limits
HOL: theory HOL.Deriv
HOL: theory HOL.Series
HOL: theory HOL.NthRoot
HOL: theory HOL.Transcendental
HOL: theory HOL.Complex
HOL: theory HOL.MacLaurin
HOL: theory Complex_Main
Timing HOL (8 threads, 206.122s elapsed time, 711.726s cpu time, 79.996s GC time, factor 3.45)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf
Timing HOL (8 threads, 206.122s elapsed time, 711.726s cpu time, 79.996s GC time, factor 3.45)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf
Finished HOL (0:04:42 elapsed time, 0:14:20 cpu time, factor 3.05)
Running JinjaThreads ...
JinjaThreads: theory HOL-Eisbach.Eisbach
JinjaThreads: theory Automatic_Refinement.Foldi
JinjaThreads: theory Automatic_Refinement.Prio_List
JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1
JinjaThreads: theory Collections.ICF_Tools
JinjaThreads: theory HOL-Library.Adhoc_Overloading
JinjaThreads: theory Finger-Trees.FingerTree
JinjaThreads: theory HOL-Library.AList
JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot
JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot
JinjaThreads: theory HOL-Library.Monad_Syntax
JinjaThreads: theory Collections.Ord_Code_Preproc
JinjaThreads: theory HOL-Library.Boolean_Algebra
JinjaThreads: theory HOL-Library.Cancellation
JinjaThreads: theory HOL-Library.Case_Converter
JinjaThreads: theory Collections.Locale_Code
JinjaThreads: theory Automatic_Refinement.Refine_Util
JinjaThreads: theory Collections.Record_Intf
JinjaThreads: theory HOL-Library.Code_Abstract_Nat
JinjaThreads: theory HOL-Library.Simps_Case_Conv
JinjaThreads: theory HOL-Library.Code_Target_Nat
JinjaThreads: theory HOL-Library.Code_Target_Int
JinjaThreads: theory HOL-Library.Dlist
JinjaThreads: theory HOL-Library.Infinite_Set
JinjaThreads: theory HOL-Library.Lattice_Syntax
JinjaThreads: theory HOL-Library.Code_Target_Numeral
JinjaThreads: theory HOL-Library.Complete_Partial_Order2
JinjaThreads: theory Automatic_Refinement.Anti_Unification
JinjaThreads: theory Automatic_Refinement.Attr_Comb
JinjaThreads: theory Automatic_Refinement.Autoref_Data
JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms
JinjaThreads: theory Automatic_Refinement.Indep_Vars
JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp
JinjaThreads: theory Automatic_Refinement.Tagged_Solver
JinjaThreads: theory Automatic_Refinement.Select_Solve
JinjaThreads: theory HOL-Library.Multiset
JinjaThreads: theory HOL-Library.Nat_Bijection
JinjaThreads: theory HOL-Library.Old_Datatype
JinjaThreads: theory HOL-Library.Option_ord
JinjaThreads: theory HOL-Library.Phantom_Type
JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs
JinjaThreads: theory HOL-Library.RBT_Impl
JinjaThreads: theory Trie.Trie
JinjaThreads: theory HOL-Library.Sublist
JinjaThreads: theory HOL-Library.Transitive_Closure_Table
JinjaThreads: theory HOL-Library.While_Combinator
JinjaThreads: theory HOL-Library.Cardinality
JinjaThreads: theory Collections.DatRef
JinjaThreads: theory HOL-Library.Z2
JinjaThreads: theory HOL-Word.Bits
JinjaThreads: theory HOL-Word.Misc_Auxiliary
JinjaThreads: theory HOL-Word.Bits_Z2
JinjaThreads: theory HOL-Word.Bits_Int
JinjaThreads: theory FinFun.FinFun
JinjaThreads: theory HOL-Library.Numeral_Type
JinjaThreads: theory HOL-Word.Misc_Arithmetic
JinjaThreads: theory HOL-Word.Misc_Typedef
JinjaThreads: theory HOL-Library.Countable
JinjaThreads: theory JinjaThreads.Set_Monad
JinjaThreads: theory JinjaThreads.Set_without_equal
JinjaThreads: theory Refine_Monadic.Refine_Chapter
JinjaThreads: theory HOL-Library.Type_Length
JinjaThreads: theory HOL-Library.Countable_Set
JinjaThreads: theory Binomial-Heaps.BinomialHeap
JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap
JinjaThreads: theory HOL-ex.Quicksort
JinjaThreads: theory HOL-Library.Countable_Complete_Lattices
JinjaThreads: theory HOL-Word.Bit_Comprehension
JinjaThreads: theory Native_Word.More_Bits_Int
JinjaThreads: theory HOL-Word.Word
JinjaThreads: theory Automatic_Refinement.Misc
JinjaThreads: theory Native_Word.Code_Symbolic_Bits_Int
JinjaThreads: theory Native_Word.Bits_Integer
JinjaThreads: theory HOL-Library.Order_Continuity
JinjaThreads: theory JinjaThreads.Auxiliary
JinjaThreads: theory HOL-Library.Extended_Nat
JinjaThreads: theory Coinductive.Coinductive_Nat
JinjaThreads: theory Coinductive.Coinductive_List
JinjaThreads: theory Automatic_Refinement.Refine_Lib
JinjaThreads: theory Collections.SetIterator
JinjaThreads: theory Collections.Sorted_List_Operations
JinjaThreads: theory Automatic_Refinement.Autoref_Phases
JinjaThreads: theory Automatic_Refinement.Autoref_Tagging
JinjaThreads: theory Automatic_Refinement.Relators
JinjaThreads: theory Collections.SetIteratorOperations
JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover
JinjaThreads: theory Automatic_Refinement.Param_Tool
JinjaThreads: theory Automatic_Refinement.Param_HOL
JinjaThreads: theory Collections.Assoc_List
JinjaThreads: theory Collections.Dlist_add
JinjaThreads: theory Automatic_Refinement.Parametricity
JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops
JinjaThreads: theory Collections.Proper_Iterator
JinjaThreads: theory Collections.SetIteratorGA
JinjaThreads: theory Collections.Diff_Array
JinjaThreads: theory Collections.Trie_Impl
JinjaThreads: theory Collections.It_to_It
JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel
JinjaThreads: theory Collections.Trie2
JinjaThreads: theory Automatic_Refinement.Autoref_Translate
JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface
JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo
JinjaThreads: theory Automatic_Refinement.Autoref_Tool
JinjaThreads: theory Coinductive.Lazy_LList
JinjaThreads: theory Coinductive.TLList
JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL
JinjaThreads: theory Native_Word.Code_Target_Bits_Int
JinjaThreads: theory Native_Word.Code_Target_Word_Base
JinjaThreads: theory Collections.Code_Target_ICF
JinjaThreads: theory Native_Word.Uint32
JinjaThreads: theory Coinductive.Lazy_TLList
JinjaThreads: theory Collections.HashCode
JinjaThreads: theory Automatic_Refinement.Automatic_Refinement
JinjaThreads: theory Collections.Idx_Iterator
JinjaThreads: theory Refine_Monadic.Refine_Misc
JinjaThreads: theory Refine_Monadic.RefineG_Domain
JinjaThreads: theory Refine_Monadic.RefineG_Transfer
JinjaThreads: theory Refine_Monadic.RefineG_Assert
JinjaThreads: theory Refine_Monadic.RefineG_Recursion
JinjaThreads: theory Refine_Monadic.RefineG_While
JinjaThreads: theory Refine_Monadic.Refine_Basic
JinjaThreads: theory Refine_Monadic.Refine_Det
JinjaThreads: theory Refine_Monadic.Refine_Heuristics
JinjaThreads: theory Refine_Monadic.Refine_Leof
JinjaThreads: theory Refine_Monadic.Refine_Pfun
JinjaThreads: theory Refine_Monadic.Refine_More_Comb
JinjaThreads: theory Refine_Monadic.Refine_While
JinjaThreads: theory Refine_Monadic.Refine_Transfer
JinjaThreads: theory Refine_Monadic.Autoref_Monadic
JinjaThreads: theory Refine_Monadic.Refine_Automation
JinjaThreads: theory Refine_Monadic.Refine_Foreach
JinjaThreads: theory Refine_Monadic.Refine_Monadic
JinjaThreads: theory Collections.Gen_Iterator
JinjaThreads: theory Collections.Intf_Map
JinjaThreads: theory Collections.Intf_Set
JinjaThreads: theory Collections.Iterator
JinjaThreads: theory Collections.Array_Iterator
JinjaThreads: theory Collections.ICF_Spec_Base
JinjaThreads: theory Collections.AnnotatedListSpec
JinjaThreads: theory Collections.ListSpec
JinjaThreads: theory Collections.MapSpec
JinjaThreads: theory Collections.PrioSpec
JinjaThreads: theory Collections.PrioUniqueSpec
JinjaThreads: theory HOL-Library.RBT
JinjaThreads: theory Collections.SetSpec
JinjaThreads: theory Collections.RBT_add
JinjaThreads: theory Collections.BinoPrioImpl
JinjaThreads: theory Collections.SkewPrioImpl
JinjaThreads: theory Collections.ListGA
JinjaThreads: theory Collections.FTAnnotatedListImpl
JinjaThreads: theory Collections.PrioByAnnotatedList
JinjaThreads: theory Collections.PrioUniqueByAnnotatedList
JinjaThreads: theory Collections.Fifo
JinjaThreads: theory Collections.Algos
JinjaThreads: theory Collections.SetIndex
JinjaThreads: theory Collections.SetIteratorCollectionsGA
JinjaThreads: theory Collections.MapGA
JinjaThreads: theory Collections.SetGA
JinjaThreads: theory Collections.FTPrioImpl
JinjaThreads: theory Collections.FTPrioUniqueImpl
JinjaThreads: theory Collections.ArrayMapImpl
JinjaThreads: theory Collections.ListMapImpl
JinjaThreads: theory Collections.ListMapImpl_Invar
JinjaThreads: theory Collections.TrieMapImpl
JinjaThreads: theory Collections.RBTMapImpl
JinjaThreads: theory Collections.ListSetImpl
JinjaThreads: theory Collections.ListSetImpl_Invar
JinjaThreads: theory Collections.ListSetImpl_NotDist
JinjaThreads: theory Collections.ListSetImpl_Sorted
JinjaThreads: theory Collections.ArrayHashMap_Impl
JinjaThreads: theory Collections.SetByMap
JinjaThreads: theory Collections.HashMap_Impl
JinjaThreads: theory Collections.ArraySetImpl
JinjaThreads: theory Collections.TrieSetImpl
JinjaThreads: theory Collections.RBTSetImpl
JinjaThreads: theory Collections.ArrayHashMap
JinjaThreads: theory Collections.HashMap
JinjaThreads: theory Collections.ArrayHashSet
JinjaThreads: theory Collections.HashSet
JinjaThreads: theory Collections.MapStdImpl
JinjaThreads: theory Collections.SetStdImpl
JinjaThreads: theory Collections.ICF_Impl
JinjaThreads: theory Collections.ICF_Refine_Monadic
JinjaThreads: theory Collections.ICF_Autoref
JinjaThreads: theory Collections.Collections
JinjaThreads: theory Collections.CollectionsV1
JinjaThreads: theory JinjaThreads.JT_ICF
JinjaThreads: theory JinjaThreads.Basic_Main
JinjaThreads: theory HOL-Library.Mapping
JinjaThreads: theory HOL-Library.Prefix_Order
JinjaThreads: theory JinjaThreads.FWState
JinjaThreads: theory JinjaThreads.LTS
JinjaThreads: theory JinjaThreads.Type
JinjaThreads: theory JinjaThreads.ListIndex
JinjaThreads: theory JinjaThreads.Orders
JinjaThreads: theory JinjaThreads.Semilat
JinjaThreads: theory JinjaThreads.Err
JinjaThreads: theory HOL-Library.AList_Mapping
JinjaThreads: theory JinjaThreads.Listn
JinjaThreads: theory JinjaThreads.Opt
JinjaThreads: theory JinjaThreads.Product
JinjaThreads: theory JinjaThreads.Semilattices
JinjaThreads: theory JinjaThreads.Typing_Framework
JinjaThreads: theory JinjaThreads.Decl
JinjaThreads: theory JinjaThreads.SemilatAlg
JinjaThreads: theory JinjaThreads.Kildall
JinjaThreads: theory JinjaThreads.LBVSpec
JinjaThreads: theory JinjaThreads.Bisimulation
JinjaThreads: theory JinjaThreads.Typing_Framework_err
JinjaThreads: theory JinjaThreads.LBVComplete
JinjaThreads: theory JinjaThreads.LBVCorrect
JinjaThreads: theory JinjaThreads.Abstract_BV
JinjaThreads: theory JinjaThreads.TypeRel
JinjaThreads: theory JinjaThreads.TypeRelRefine
JinjaThreads: theory JinjaThreads.Value
JinjaThreads: theory JinjaThreads.Exceptions
JinjaThreads: theory JinjaThreads.Heap
JinjaThreads: theory JinjaThreads.SystemClasses
JinjaThreads: theory JinjaThreads.MM
JinjaThreads: theory JinjaThreads.State
JinjaThreads: theory JinjaThreads.FWCondAction
JinjaThreads: theory JinjaThreads.FWInterrupt
JinjaThreads: theory JinjaThreads.FWLock
JinjaThreads: theory JinjaThreads.FWThread
JinjaThreads: theory JinjaThreads.FWWait
JinjaThreads: theory JinjaThreads.Observable_Events
JinjaThreads: theory JinjaThreads.FWLocking
JinjaThreads: theory JinjaThreads.FWLockingThread
JinjaThreads: theory JinjaThreads.FWWellform
JinjaThreads: theory JinjaThreads.FWLifting
JinjaThreads: theory JinjaThreads.FWSemantics
JinjaThreads: theory JinjaThreads.JVMState
JinjaThreads: theory JinjaThreads.StartConfig
JinjaThreads: theory JinjaThreads.JMM_Spec
JinjaThreads: theory JinjaThreads.FWLiftingSem
JinjaThreads: theory JinjaThreads.FWProgressAux
JinjaThreads: theory JinjaThreads.Conform
JinjaThreads: theory JinjaThreads.State_Refinement
JinjaThreads: theory JinjaThreads.FWDeadlock
JinjaThreads: theory JinjaThreads.FWLTS
JinjaThreads: theory JinjaThreads.ConformThreaded
JinjaThreads: theory JinjaThreads.ExternalCall
JinjaThreads: theory JinjaThreads.SC
JinjaThreads: theory JinjaThreads.FWProgress
JinjaThreads: theory JinjaThreads.SC_Collections
JinjaThreads: theory JinjaThreads.JMM_DRF
JinjaThreads: theory JinjaThreads.SC_Legal
JinjaThreads: theory JinjaThreads.FWBisimulation
JinjaThreads: theory JinjaThreads.FWInitFinLift
JinjaThreads: theory JinjaThreads.Non_Speculative
JinjaThreads: theory JinjaThreads.Scheduler
JinjaThreads: theory JinjaThreads.HB_Completion
JinjaThreads: theory JinjaThreads.SC_Completion
JinjaThreads: theory JinjaThreads.WellForm
JinjaThreads: theory JinjaThreads.ExternalCall_Execute
JinjaThreads: theory JinjaThreads.BinOp
JinjaThreads: theory JinjaThreads.ExternalCallWF
JinjaThreads: theory JinjaThreads.JMM_Heap
JinjaThreads: theory JinjaThreads.SemiType
JinjaThreads: theory JinjaThreads.JVM_SemiType
JinjaThreads: theory JinjaThreads.JMM_Type
JinjaThreads: theory JinjaThreads.JMM_Type2
JinjaThreads: theory JinjaThreads.Random_Scheduler
JinjaThreads: theory JinjaThreads.Round_Robin
JinjaThreads: theory JinjaThreads.JMM_Framework
JinjaThreads: theory JinjaThreads.Expr
JinjaThreads: theory JinjaThreads.JVMInstructions
JinjaThreads: theory JinjaThreads.PCompiler
JinjaThreads: theory JinjaThreads.PCompilerRefine
JinjaThreads: theory JinjaThreads.SC_Schedulers
JinjaThreads: theory JinjaThreads.JVMExceptions
JinjaThreads: theory JinjaThreads.JVMHeap
JinjaThreads: theory JinjaThreads.Effect
JinjaThreads: theory JinjaThreads.JVMExecInstr
JinjaThreads: theory JinjaThreads.CallExpr
JinjaThreads: theory JinjaThreads.DefAss
JinjaThreads: theory JinjaThreads.WWellForm
JinjaThreads: theory JinjaThreads.JHeap
JinjaThreads: theory JinjaThreads.JVMExec
JinjaThreads: theory JinjaThreads.JVMDefensive
JinjaThreads: theory JinjaThreads.J1State
JinjaThreads: theory JinjaThreads.WellType
JinjaThreads: theory JinjaThreads.SmallStep
JinjaThreads: theory JinjaThreads.JVMExec_Execute
JinjaThreads: theory JinjaThreads.Compiler2
JinjaThreads: theory JinjaThreads.JVMThreaded
JinjaThreads: theory JinjaThreads.J1Heap
JinjaThreads: theory JinjaThreads.Compiler1
JinjaThreads: theory JinjaThreads.J1WellType
JinjaThreads: theory JinjaThreads.Exception_Tables
JinjaThreads: theory JinjaThreads.Compiler
JinjaThreads: theory JinjaThreads.J1WellForm
JinjaThreads: theory JinjaThreads.Annotate
JinjaThreads: theory JinjaThreads.JWellForm
JinjaThreads: theory JinjaThreads.WellTypeRT
JinjaThreads: theory JinjaThreads.JJ1WellForm
JinjaThreads: theory JinjaThreads.JVM_Main
JinjaThreads: theory JinjaThreads.ToString
JinjaThreads: theory JinjaThreads.Preprocessor
JinjaThreads: theory JinjaThreads.JMM_JVM
JinjaThreads: theory JinjaThreads.JMM_Typesafe
JinjaThreads: theory JinjaThreads.BVSpec
JinjaThreads: theory JinjaThreads.BVConform
JinjaThreads: theory JinjaThreads.TypeComp
JinjaThreads: theory JinjaThreads.EffectMono
JinjaThreads: theory JinjaThreads.TF_JVM
JinjaThreads: theory JinjaThreads.BVExec
JinjaThreads: theory JinjaThreads.BVSpecTypeSafe
JinjaThreads: theory JinjaThreads.JMM_Common
JinjaThreads: theory JinjaThreads.LBVJVM
JinjaThreads: theory JinjaThreads.JMM_Typesafe2
JinjaThreads: theory JinjaThreads.BVNoTypeError
JinjaThreads: theory JinjaThreads.FWBisimDeadlock
JinjaThreads: theory JinjaThreads.FWBisimLift
JinjaThreads: theory JinjaThreads.J1
JinjaThreads: theory JinjaThreads.BVProgressThreaded
JinjaThreads: theory JinjaThreads.BCVExec
JinjaThreads: theory JinjaThreads.JVMExec_Execute2
JinjaThreads: theory JinjaThreads.JVMTau
JinjaThreads: theory JinjaThreads.Common_Main
JinjaThreads: theory JinjaThreads.Execs
JinjaThreads: theory JinjaThreads.J1Deadlock
JinjaThreads: theory JinjaThreads.DefAssPreservation
JinjaThreads: theory JinjaThreads.Threaded
JinjaThreads: theory JinjaThreads.Progress
JinjaThreads: theory JinjaThreads.TypeSafe
JinjaThreads: theory JinjaThreads.J0
JinjaThreads: theory JinjaThreads.JMM_J
JinjaThreads: theory JinjaThreads.ProgressThreaded
JinjaThreads: theory JinjaThreads.J_Execute
JinjaThreads: theory JinjaThreads.J1JVMBisim
JinjaThreads: theory JinjaThreads.DRF_J
JinjaThreads: theory JinjaThreads.Deadlocked
JinjaThreads: theory JinjaThreads.DRF_JVM
JinjaThreads: theory JinjaThreads.JVMDeadlocked
JinjaThreads: theory JinjaThreads.JVM_Execute
JinjaThreads: theory JinjaThreads.JVM_Execute2
JinjaThreads: theory JinjaThreads.J_Main
JinjaThreads: theory JinjaThreads.J0Bisim
JinjaThreads: theory JinjaThreads.J0J1Bisim
JinjaThreads: theory JinjaThreads.BV_Main
JinjaThreads: theory JinjaThreads.Code_Generation
JinjaThreads: theory JinjaThreads.Correctness1
JinjaThreads: theory JinjaThreads.Correctness1Threaded
JinjaThreads: theory JinjaThreads.ApprenticeChallenge
JinjaThreads: theory JinjaThreads.BufferExample
JinjaThreads: theory JinjaThreads.Java2Jinja
JinjaThreads: theory JinjaThreads.Examples_Main
JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe
JinjaThreads: theory JinjaThreads.JMM_J_Typesafe
JinjaThreads: theory JinjaThreads.Execute_Main
JinjaThreads: theory JinjaThreads.J1JVM
JinjaThreads: theory JinjaThreads.JVMJ1
JinjaThreads: theory JinjaThreads.Correctness2
JinjaThreads: theory JinjaThreads.Correctness
JinjaThreads: theory JinjaThreads.Compiler_Main
JinjaThreads: theory JinjaThreads.JMM_Compiler
JinjaThreads: theory JinjaThreads.SC_Interp
JinjaThreads: theory JinjaThreads.JMM_Interp
JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2
JinjaThreads: theory JinjaThreads.JMM
JinjaThreads: theory JinjaThreads.MM_Main
JinjaThreads: theory JinjaThreads.JinjaThreads
Timing JinjaThreads (8 threads, 2384.953s elapsed time, 10902.395s cpu time, 3983.619s GC time, factor 4.57)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf
Timing JinjaThreads (8 threads, 2384.953s elapsed time, 10902.395s cpu time, 3983.619s GC time, factor 4.57)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads/outline.pdf
Finished JinjaThreads (0:40:20 elapsed time, 3:05:13 cpu time, factor 4.59)
Building Flyspeck-Tame ...
Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat
Flyspeck-Tame: theory HOL-Library.Code_Target_Int
Flyspeck-Tame: theory HOL-Library.AList
Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order
Flyspeck-Tame: theory Flyspeck-Tame.RTranCl
Flyspeck-Tame: theory HOL-Library.IArray
Flyspeck-Tame: theory Flyspeck-Tame.ListAux
Flyspeck-Tame: theory HOL-Library.While_Combinator
Flyspeck-Tame: theory HOL-Library.Code_Target_Nat
Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso
Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral
Flyspeck-Tame: theory Flyspeck-Tame.Arch
Flyspeck-Tame: theory Flyspeck-Tame.Worklist
Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax
Flyspeck-Tame: theory Flyspeck-Tame.ListSum
Flyspeck-Tame: theory Flyspeck-Tame.Rotation
Flyspeck-Tame: theory Flyspeck-Tame.Graph
Flyspeck-Tame: theory Flyspeck-Tame.Maps
Flyspeck-Tame: theory Trie.Trie
Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision
Flyspeck-Tame: theory Flyspeck-Tame.GraphProps
Flyspeck-Tame: theory Flyspeck-Tame.Tame
Flyspeck-Tame: theory Trie.Tries
Flyspeck-Tame: theory Flyspeck-Tame.Enumerator
Flyspeck-Tame: theory Flyspeck-Tame.TameProps
Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps
Flyspeck-Tame: theory Flyspeck-Tame.Plane
Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps
Flyspeck-Tame: theory Flyspeck-Tame.Plane1
Flyspeck-Tame: theory Flyspeck-Tame.Generator
Flyspeck-Tame: theory Flyspeck-Tame.TameEnum
Flyspeck-Tame: theory Flyspeck-Tame.Invariants
Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps
Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux
Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps
Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props
Flyspeck-Tame: theory Flyspeck-Tame.LowerBound
Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps
Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps
Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps
Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness
Timing Flyspeck-Tame (8 threads, 56.298s elapsed time, 305.407s cpu time, 23.472s GC time, factor 5.42)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf
Timing Flyspeck-Tame (8 threads, 56.298s elapsed time, 305.407s cpu time, 23.472s GC time, factor 5.42)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf
Finished Flyspeck-Tame (0:01:35 elapsed time, 0:06:26 cpu time, factor 4.04)
Running Flyspeck-Tame-Computation ...
Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.ArchComp
Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.Completeness
Timing Flyspeck-Tame-Computation (8 threads, 16379.362s elapsed time, 24486.422s cpu time, 1940.447s GC time, factor 1.49)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame-Computation
Timing Flyspeck-Tame-Computation (8 threads, 16379.362s elapsed time, 24486.422s cpu time, 1940.447s GC time, factor 1.49)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame-Computation
Finished Flyspeck-Tame-Computation (4:33:00 elapsed time, 6:48:07 cpu time, factor 1.49)
Building AWN ...
AWN: theory AWN.Lib
AWN: theory AWN.TransitionSystems
AWN: theory AWN.AWN
AWN: theory AWN.Invariants
AWN: theory AWN.OInvariants
AWN: theory AWN.AWN_Cterms
AWN: theory AWN.AWN_SOS
AWN: theory AWN.OAWN_SOS
AWN: theory AWN.AWN_Labels
AWN: theory AWN.Pnet
AWN: theory AWN.Inv_Cterms
AWN: theory AWN.AWN_Invariants
AWN: theory AWN.Closed
AWN: theory AWN.AWN_SOS_Labels
AWN: theory AWN.Qmsg
AWN: theory AWN.OAWN_Invariants
AWN: theory AWN.ONode_Lifting
AWN: theory AWN.OPnet
AWN: theory AWN.OAWN_SOS_Labels
AWN: theory AWN.OPnet_Lifting
AWN: theory AWN.OClosed_Lifting
AWN: theory AWN.OClosed_Transfer
AWN: theory AWN.OAWN_Convert
AWN: theory AWN.Qmsg_Lifting
AWN: theory AWN.AWN_Main
AWN: theory AWN.Toy
AWN: theory AWN.AWN_Term_Graph
Timing AWN (8 threads, 31.106s elapsed time, 150.600s cpu time, 6.410s GC time, factor 4.84)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf
Timing AWN (8 threads, 31.106s elapsed time, 150.600s cpu time, 6.410s GC time, factor 4.84)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf
Finished AWN (0:01:00 elapsed time, 0:03:31 cpu time, factor 3.50)
Running AODV ...
AODV: theory AODV.Aodv_Basic
AODV: theory AODV.Aodv_Data
AODV: theory AODV.A_Norreqid
AODV: theory AODV.Aodv_Message
AODV: theory AODV.B_Fwdrreps
AODV: theory AODV.C_Gtobcast
AODV: theory AODV.D_Fwdrreqs
AODV: theory AODV.E_All_ABCD
AODV: theory AODV.E_Aodv_Message
AODV: theory AODV.E_Aodv_Data
AODV: theory AODV.D_Aodv_Data
AODV: theory AODV.A_Aodv_Data
AODV: theory AODV.A_Aodv_Message
AODV: theory AODV.B_Aodv_Data
AODV: theory AODV.B_Aodv_Message
AODV: theory AODV.A_Fresher
AODV: theory AODV.C_Aodv_Data
AODV: theory AODV.B_Fresher
AODV: theory AODV.Fresher
AODV: theory AODV.C_Aodv_Message
AODV: theory AODV.D_Fresher
AODV: theory AODV.D_Aodv_Message
AODV: theory AODV.E_Fresher
AODV: theory AODV.A_Aodv
AODV: theory AODV.Aodv
AODV: theory AODV.E_Aodv
AODV: theory AODV.C_Fresher
AODV: theory AODV.B_Aodv
AODV: theory AODV.C_Aodv
AODV: theory AODV.D_Aodv
AODV: theory AODV.E_Aodv_Predicates
AODV: theory AODV.E_Loop_Freedom
AODV: theory AODV.E_Quality_Increases
AODV: theory AODV.E_Seq_Invariants
AODV: theory AODV.E_OAodv
AODV: theory AODV.E_Global_Invariants
AODV: theory AODV.E_Aodv_Loop_Freedom
AODV: theory AODV.Aodv_Predicates
AODV: theory AODV.OAodv
AODV: theory AODV.Loop_Freedom
AODV: theory AODV.Quality_Increases
AODV: theory AODV.Seq_Invariants
AODV: theory AODV.Global_Invariants
AODV: theory AODV.Aodv_Loop_Freedom
AODV: theory AODV.A_Aodv_Predicates
AODV: theory AODV.A_OAodv
AODV: theory AODV.A_Loop_Freedom
AODV: theory AODV.A_Quality_Increases
AODV: theory AODV.A_Seq_Invariants
AODV: theory AODV.A_Global_Invariants
AODV: theory AODV.C_Aodv_Predicates
AODV: theory AODV.C_OAodv
AODV: theory AODV.C_Loop_Freedom
AODV: theory AODV.C_Quality_Increases
AODV: theory AODV.C_Seq_Invariants
AODV: theory AODV.A_Aodv_Loop_Freedom
AODV: theory AODV.B_Aodv_Predicates
AODV: theory AODV.B_OAodv
AODV: theory AODV.B_Loop_Freedom
AODV: theory AODV.B_Quality_Increases
AODV: theory AODV.B_Seq_Invariants
AODV: theory AODV.C_Global_Invariants
AODV: theory AODV.B_Global_Invariants
AODV: theory AODV.C_Aodv_Loop_Freedom
AODV: theory AODV.B_Aodv_Loop_Freedom
AODV: theory AODV.D_Aodv_Predicates
AODV: theory AODV.D_OAodv
AODV: theory AODV.D_Loop_Freedom
AODV: theory AODV.D_Quality_Increases
AODV: theory AODV.D_Seq_Invariants
AODV: theory AODV.D_Global_Invariants
AODV: theory AODV.D_Aodv_Loop_Freedom
AODV: theory AODV.All
Timing AODV (8 threads, 4971.614s elapsed time, 27182.765s cpu time, 1477.624s GC time, factor 5.47)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/outline.pdf
Timing AODV (8 threads, 4971.614s elapsed time, 27182.765s cpu time, 1477.624s GC time, factor 5.47)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV/outline.pdf
Finished AODV (1:23:01 elapsed time, 7:33:20 cpu time, factor 5.46)
Building HOL-Library ...
HOL-Library: theory HOL-Library.AList
HOL-Library: theory HOL-Library.Adhoc_Overloading
HOL-Library: theory HOL-Library.BNF_Axiomatization
HOL-Library: theory HOL-Library.BNF_Corec
HOL-Library: theory HOL-Library.Boolean_Algebra
HOL-Library: theory HOL-Library.Cancellation
HOL-Library: theory HOL-Library.Case_Converter
HOL-Library: theory HOL-Library.Char_ord
HOL-Library: theory HOL-Library.Monad_Syntax
HOL-Library: theory HOL-Library.State_Monad
HOL-Library: theory HOL-Library.Code_Abstract_Nat
HOL-Library: theory HOL-Library.Code_Prolog
HOL-Library: theory HOL-Library.Code_Target_Int
HOL-Library: theory HOL-Library.Code_Binary_Nat
HOL-Library: theory HOL-Library.Code_Lazy
HOL-Library: theory HOL-Library.Simps_Case_Conv
HOL-Library: theory HOL-Library.Code_Target_Nat
HOL-Library: theory HOL-Library.Extended
HOL-Library: theory HOL-Library.Multiset
HOL-Library: theory HOL-Library.Code_Target_Numeral
HOL-Library: theory HOL-Library.Code_Test
HOL-Library: theory HOL-Library.Comparator
HOL-Library: theory HOL-Library.Conditional_Parametricity
HOL-Library: theory HOL-Library.Datatype_Records
HOL-Library: theory HOL-Library.Debug
HOL-Library: theory HOL-Library.Disjoint_Sets
HOL-Library: theory HOL-Library.DAList
HOL-Library: theory HOL-Library.Dlist
HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
HOL-Library: theory HOL-Library.Fun_Lexorder
HOL-Library: theory HOL-Library.FuncSet
HOL-Library: theory HOL-Library.Function_Algebras
HOL-Library: theory HOL-Library.Function_Division
HOL-Library: theory HOL-Library.Groups_Big_Fun
HOL-Library: theory HOL-Library.IArray
HOL-Library: theory HOL-Library.Infinite_Set
HOL-Library: theory HOL-Library.LaTeXsugar
HOL-Library: theory HOL-Library.Equipollence
HOL-Library: theory HOL-Library.Lattice_Constructions
HOL-Library: theory HOL-Library.Omega_Words_Fun
HOL-Library: theory HOL-Library.Ramsey
HOL-Library: theory HOL-Library.Lattice_Syntax
HOL-Library: theory HOL-Library.Combine_PER
HOL-Library: theory HOL-Library.Complete_Partial_Order2
HOL-Library: theory HOL-Library.ListVector
HOL-Library: theory HOL-Library.List_Lexorder
HOL-Library: theory HOL-Library.Mapping
HOL-Library: theory HOL-Library.More_List
HOL-Library: theory HOL-Library.Nat_Bijection
HOL-Library: theory HOL-Library.Old_Datatype
HOL-Library: theory HOL-Library.Poly_Mapping
HOL-Library: theory HOL-Library.Stream
HOL-Library: theory HOL-Library.Old_Recdef
HOL-Library: theory HOL-Library.AList_Mapping
HOL-Library: theory HOL-Library.Open_State_Syntax
HOL-Library: theory HOL-Library.Option_ord
HOL-Library: theory HOL-Library.Parallel
HOL-Library: theory HOL-Library.Pattern_Aliases
HOL-Library: theory HOL-Library.Perm
HOL-Library: theory HOL-Library.Phantom_Type
HOL-Library: theory HOL-Library.Power_By_Squaring
HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
HOL-Library: theory HOL-Library.Preorder
HOL-Library: theory HOL-Library.Product_Lexorder
HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
HOL-Library: theory HOL-Library.Product_Plus
HOL-Library: theory HOL-Library.Quotient_Syntax
HOL-Library: theory HOL-Library.DAList_Multiset
HOL-Library: theory HOL-Library.Multiset_Order
HOL-Library: theory HOL-Library.Permutation
HOL-Library: theory HOL-Library.Permutations
HOL-Library: theory HOL-Library.Cardinality
HOL-Library: theory HOL-Library.Product_Order
HOL-Library: theory HOL-Library.Quotient_Option
HOL-Library: theory HOL-Library.Quotient_Product
HOL-Library: theory HOL-Library.Quotient_Set
HOL-Library: theory HOL-Library.Quotient_Sum
HOL-Library: theory HOL-Library.Quotient_List
HOL-Library: theory HOL-Library.Finite_Lattice
HOL-Library: theory HOL-Library.Quotient_Type
HOL-Library: theory HOL-Library.RBT_Impl
HOL-Library: theory HOL-Library.Realizers
HOL-Library: theory HOL-Library.Reflection
HOL-Library: theory HOL-Library.Refute
HOL-Library: theory HOL-Library.Rewrite
HOL-Library: theory HOL-Library.Set_Algebras
HOL-Library: theory HOL-Library.Sorting_Algorithms
HOL-Library: theory HOL-Library.Stirling
HOL-Library: theory HOL-Library.Sublist
HOL-Library: theory HOL-Library.Numeral_Type
HOL-Library: theory HOL-Library.Transitive_Closure_Table
HOL-Library: theory HOL-Library.Tree
HOL-Library: theory HOL-Library.Uprod
HOL-Library: theory HOL-Library.While_Combinator
HOL-Library: theory HOL-Library.Type_Length
HOL-Library: theory HOL-Library.Z2
HOL-Library: theory HOL-Library.Saturated
HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
HOL-Library: theory HOL-Library.Countable
HOL-Library: theory HOL-Library.BigO
HOL-Library: theory HOL-Library.Prefix_Order
HOL-Library: theory HOL-Library.Subseq_Order
HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
HOL-Library: theory HOL-Library.Diagonal_Subsequence
HOL-Library: theory HOL-Library.Discrete
HOL-Library: theory HOL-Library.Going_To_Filter
HOL-Library: theory HOL-Library.Indicator_Function
HOL-Library: theory HOL-Library.Landau_Symbols
HOL-Library: theory HOL-Library.Lattice_Algebras
HOL-Library: theory HOL-Library.Liminf_Limsup
HOL-Library: theory HOL-Library.Log_Nat
HOL-Library: theory HOL-Library.Lub_Glb
HOL-Library: theory HOL-Library.Multiset_Permutations
HOL-Library: theory HOL-Library.Countable_Set
HOL-Library: theory HOL-Library.FSet
HOL-Library: theory HOL-Library.Nonpos_Ints
HOL-Library: theory HOL-Library.OptionalSugar
HOL-Library: theory HOL-Library.Tree_Multiset
HOL-Library: theory HOL-Library.Countable_Complete_Lattices
HOL-Library: theory HOL-Library.Countable_Set_Type
HOL-Library: theory HOL-Library.Set_Idioms
HOL-Library: theory HOL-Library.Periodic_Fun
HOL-Library: theory HOL-Library.Quadratic_Discriminant
HOL-Library: theory HOL-Library.Sum_of_Squares
HOL-Library: theory HOL-Library.Tree_Real
HOL-Library: theory HOL-Library.Order_Continuity
HOL-Library: theory HOL-Library.Extended_Nat
HOL-Library: theory HOL-Library.Finite_Map
HOL-Library: theory HOL-Library.Float
HOL-Library: theory HOL-Library.Extended_Real
HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
HOL-Library: theory HOL-Library.Library
HOL-Library: theory HOL-Library.RBT
HOL-Library: theory HOL-Library.RBT_Mapping
HOL-Library: theory HOL-Library.RBT_Set
Timing HOL-Library (8 threads, 65.072s elapsed time, 425.221s cpu time, 27.227s GC time, factor 6.53)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf
Timing HOL-Library (8 threads, 65.072s elapsed time, 425.221s cpu time, 27.227s GC time, factor 6.53)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf
Finished HOL-Library (0:02:08 elapsed time, 0:09:33 cpu time, factor 4.47)
Building ConcurrentIMP ...
ConcurrentIMP: theory ConcurrentIMP.CIMP_pred
ConcurrentIMP: theory ConcurrentIMP.CIMP_lang
ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg
ConcurrentIMP: theory ConcurrentIMP.CIMP
ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer_ex
ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer_ex
Timing ConcurrentIMP (8 threads, 15.904s elapsed time, 41.191s cpu time, 2.462s GC time, factor 2.59)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf
Timing ConcurrentIMP (8 threads, 15.904s elapsed time, 41.191s cpu time, 2.462s GC time, factor 2.59)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf
Finished ConcurrentIMP (0:00:38 elapsed time, 0:01:27 cpu time, factor 2.30)
Running ConcurrentGC ...
ConcurrentGC: theory ConcurrentGC.Model
ConcurrentGC: theory ConcurrentGC.Tactics
ConcurrentGC: theory ConcurrentGC.Proofs_basis
ConcurrentGC: theory ConcurrentGC.TSO
ConcurrentGC: theory ConcurrentGC.Handshakes
ConcurrentGC: theory ConcurrentGC.MarkObject
ConcurrentGC: theory ConcurrentGC.StrongTricolour
ConcurrentGC: theory ConcurrentGC.Proofs
ConcurrentGC: theory ConcurrentGC.Concrete_heap
ConcurrentGC: theory ConcurrentGC.Concrete
Timing ConcurrentGC (8 threads, 1728.443s elapsed time, 10418.240s cpu time, 713.737s GC time, factor 6.03)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf
Timing ConcurrentGC (8 threads, 1728.443s elapsed time, 10418.240s cpu time, 713.737s GC time, factor 6.03)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC/outline.pdf
Finished ConcurrentGC (0:28:53 elapsed time, 2:53:49 cpu time, factor 6.01)
Building HOL-Word ...
HOL-Word: theory HOL-Library.Boolean_Algebra
HOL-Word: theory HOL-Library.Phantom_Type
HOL-Word: theory HOL-Word.Bits
HOL-Word: theory HOL-Word.Misc_Auxiliary
HOL-Word: theory HOL-Library.Z2
HOL-Word: theory HOL-Word.Misc_Typedef
HOL-Word: theory HOL-Word.Bits_Int
HOL-Word: theory HOL-Word.Bits_Z2
HOL-Word: theory HOL-Word.Misc_Arithmetic
HOL-Word: theory HOL-Library.Cardinality
HOL-Word: theory HOL-Library.Numeral_Type
HOL-Word: theory HOL-Word.Bit_Comprehension
HOL-Word: theory HOL-Library.Type_Length
HOL-Word: theory HOL-Word.Word
HOL-Word: theory HOL-Word.Word_Bitwise
HOL-Word: theory HOL-Word.More_Word
HOL-Word: theory HOL-Word.Word_Examples
Timing HOL-Word (8 threads, 8.607s elapsed time, 46.220s cpu time, 2.141s GC time, factor 5.37)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf
Timing HOL-Word (8 threads, 8.607s elapsed time, 46.220s cpu time, 2.141s GC time, factor 5.37)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf
Finished HOL-Word (0:00:26 elapsed time, 0:01:22 cpu time, factor 3.16)
Building Word_Lib ...
Word_Lib: theory HOL-Library.Sublist
Word_Lib: theory Word_Lib.Signed_Words
Word_Lib: theory Word_Lib.Hex_Words
Word_Lib: theory Word_Lib.Word_Type_Syntax
Word_Lib: theory Word_Lib.HOL_Lemmas
Word_Lib: theory Word_Lib.Enumeration
Word_Lib: theory Word_Lib.More_Divides
Word_Lib: theory Word_Lib.Norm_Words
Word_Lib: theory Word_Lib.WordBitwise_Signed
Word_Lib: theory Word_Lib.Word_Syntax
Word_Lib: theory Word_Lib.Word_Lib
Word_Lib: theory Word_Lib.Word_Enum
Word_Lib: theory Word_Lib.Aligned
Word_Lib: theory Word_Lib.Word_Setup_32
Word_Lib: theory Word_Lib.Word_Setup_64
Word_Lib: theory Word_Lib.Word_Next
Word_Lib: theory Word_Lib.Word_Lemmas
Word_Lib: theory Word_Lib.Word_Lemmas_32
Word_Lib: theory Word_Lib.Word_Lemmas_64
Timing Word_Lib (8 threads, 26.547s elapsed time, 80.125s cpu time, 4.672s GC time, factor 3.02)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf
Timing Word_Lib (8 threads, 26.547s elapsed time, 80.125s cpu time, 4.672s GC time, factor 3.02)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf
Finished Word_Lib (0:00:44 elapsed time, 0:01:56 cpu time, factor 2.64)
Building IP_Addresses ...
IP_Addresses: theory HOL-Eisbach.Eisbach
IP_Addresses: theory HOL-Library.Cancellation
IP_Addresses: theory HOL-Library.Infinite_Set
IP_Addresses: theory HOL-Library.Option_ord
IP_Addresses: theory IP_Addresses.NumberWang_IPv4
IP_Addresses: theory IP_Addresses.NumberWang_IPv6
IP_Addresses: theory HOL-Library.Multiset
IP_Addresses: theory HOL-ex.Quicksort
IP_Addresses: theory Automatic_Refinement.Misc
IP_Addresses: theory HOL-Library.Code_Abstract_Nat
IP_Addresses: theory HOL-Library.Product_Lexorder
IP_Addresses: theory IP_Addresses.Hs_Compat
IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
IP_Addresses: theory IP_Addresses.WordInterval
IP_Addresses: theory HOL-Library.Code_Target_Nat
IP_Addresses: theory IP_Addresses.Lib_List_toString
IP_Addresses: theory IP_Addresses.Lib_Word_toString
IP_Addresses: theory IP_Addresses.IP_Address
IP_Addresses: theory IP_Addresses.WordInterval_Sorted
IP_Addresses: theory IP_Addresses.IPv4
IP_Addresses: theory IP_Addresses.IPv6
IP_Addresses: theory IP_Addresses.Prefix_Match
IP_Addresses: theory IP_Addresses.CIDR_Split
IP_Addresses: theory IP_Addresses.IP_Address_Parser
IP_Addresses: theory IP_Addresses.IP_Address_toString
IP_Addresses: theory IP_Addresses.Prefix_Match_toString
Timing IP_Addresses (8 threads, 189.063s elapsed time, 597.300s cpu time, 45.583s GC time, factor 3.16)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf
Timing IP_Addresses (8 threads, 189.063s elapsed time, 597.300s cpu time, 45.583s GC time, factor 3.16)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf
Finished IP_Addresses (0:03:51 elapsed time, 0:11:27 cpu time, factor 2.98)
Building Simple_Firewall ...
Simple_Firewall: theory HOL-Library.Char_ord
Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
Simple_Firewall: theory Simple_Firewall.GroupF
Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
Simple_Firewall: theory Simple_Firewall.Option_Helpers
Simple_Firewall: theory Simple_Firewall.List_Product_More
Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
Simple_Firewall: theory Simple_Firewall.Iface
Simple_Firewall: theory Simple_Firewall.L4_Protocol
Simple_Firewall: theory Simple_Firewall.Simple_Packet
Simple_Firewall: theory Simple_Firewall.Primitives_toString
Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
Simple_Firewall: theory Simple_Firewall.SimpleFw_toString
Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
Simple_Firewall: theory Simple_Firewall.Shadowed
Simple_Firewall: theory Simple_Firewall.Service_Matrix
Timing Simple_Firewall (8 threads, 16.040s elapsed time, 64.458s cpu time, 3.384s GC time, factor 4.02)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf
Timing Simple_Firewall (8 threads, 16.040s elapsed time, 64.458s cpu time, 3.384s GC time, factor 4.02)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf
Finished Simple_Firewall (0:00:38 elapsed time, 0:01:56 cpu time, factor 3.01)
Building Routing ...
Routing: theory HOL-Library.Adhoc_Overloading
Routing: theory Routing.Linorder_Helper
Routing: theory HOL-Library.Monad_Syntax
Routing: theory Routing.Routing_Table
Routing: theory Routing.IpRoute_Parser
Routing: theory Routing.Linux_Router
Timing Routing (8 threads, 9.202s elapsed time, 25.603s cpu time, 0.835s GC time, factor 2.78)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf
Timing Routing (8 threads, 9.202s elapsed time, 25.603s cpu time, 0.835s GC time, factor 2.78)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf
Finished Routing (0:00:26 elapsed time, 0:01:01 cpu time, factor 2.34)
Building Iptables_Semantics ...
Iptables_Semantics: theory Iptables_Semantics.List_Misc
Iptables_Semantics: theory Iptables_Semantics.Negation_Type
Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
Iptables_Semantics: theory HOL-Library.LaTeXsugar
Iptables_Semantics: theory HOL-Library.Code_Target_Int
Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
Iptables_Semantics: theory Native_Word.More_Bits_Int
Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
Iptables_Semantics: theory Iptables_Semantics.Ternary
Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
Iptables_Semantics: theory Iptables_Semantics.IpAddresses
Iptables_Semantics: theory Iptables_Semantics.Word_Upto
Iptables_Semantics: theory Iptables_Semantics.Ports
Iptables_Semantics: theory Native_Word.Code_Symbolic_Bits_Int
Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
Iptables_Semantics: theory Native_Word.Bits_Integer
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
Iptables_Semantics: theory Iptables_Semantics.Semantics
Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int
Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
Iptables_Semantics: theory Iptables_Semantics.Matching
Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
Iptables_Semantics: theory Iptables_Semantics.Optimizing
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
Iptables_Semantics: theory Iptables_Semantics.Ipassmt
Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
Iptables_Semantics: theory Iptables_Semantics.No_Spoof
Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
Iptables_Semantics: theory Iptables_Semantics.Transform
Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
Iptables_Semantics: theory Iptables_Semantics.Code_Interface
Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Parser
Iptables_Semantics: theory Iptables_Semantics.Parser6
Iptables_Semantics: theory Iptables_Semantics.Documentation
Iptables_Semantics: theory Iptables_Semantics.Code_haskell
Timing Iptables_Semantics (8 threads, 102.645s elapsed time, 460.452s cpu time, 42.654s GC time, factor 4.49)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf
Timing Iptables_Semantics (8 threads, 102.645s elapsed time, 460.452s cpu time, 42.654s GC time, factor 4.49)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf
Finished Iptables_Semantics (0:02:37 elapsed time, 0:10:11 cpu time, factor 3.87)
Building Iptables_Semantics_Examples ...
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation
Timing Iptables_Semantics_Examples (8 threads, 193.895s elapsed time, 1322.685s cpu time, 148.457s GC time, factor 6.82)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf
Timing Iptables_Semantics_Examples (8 threads, 193.895s elapsed time, 1322.685s cpu time, 148.457s GC time, factor 6.82)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples/outline.pdf
Finished Iptables_Semantics_Examples (0:03:42 elapsed time, 0:23:02 cpu time, factor 6.21)
Running Iptables_Semantics_Examples_Big ...
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW
Timing Iptables_Semantics_Examples_Big (8 threads, 6821.546s elapsed time, 30456.720s cpu time, 13246.748s GC time, factor 4.46)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/outline.pdf
Timing Iptables_Semantics_Examples_Big (8 threads, 6821.546s elapsed time, 30456.720s cpu time, 13246.748s GC time, factor 4.46)
Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/document.pdf
Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big/outline.pdf
Finished Iptables_Semantics_Examples_Big (1:53:47 elapsed time, 8:27:54 cpu time, factor 4.46)
=== TIMING ===
Group slow: 8:59:03 elapsed time, 28:48:26 cpu time, factor 3.21
Group AFP: 9:14:19 elapsed time, 29:49:29 cpu time, factor 3.23
Group main: 0:07:16 elapsed time, 0:25:16 cpu time, factor 3.47
Group timing: 0:02:34 elapsed time, 0:10:56 cpu time, factor 4.25
Group very_slow: 6:26:48 elapsed time, 15:16:02 cpu time, factor 2.37
Overall: 9:22:30 elapsed time, 30:15:07 cpu time, factor 3.23
Archiving artifacts
Started calculate disk usage of build
Finished Calculation of disk usage of build in 0 seconds
Started calculate disk usage of workspace
Finished Calculation of disk usage of workspace in 0 seconds
No emails were triggered.
Finished: SUCCESS