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/ real URL is https://isabelle.in.tum.de/repos/isabelle/ no changes found [isabelle-nightly-slow] $ hg update --clean --rev default 17 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 dbafa8d688fbe403771ea9d03a8780ffa736ad43 --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(dbafa8d688fbe403771ea9d03a8780ffa736ad43)" --encoding UTF-8 --encodingmode replace [afp] $ hg showconfig paths.default [afp] $ hg pull --rev default pulling from https://foss.heptapod.net/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 26adfcf755e4fcfe8b6b7d9392ee2b5fd31ae132 --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(26adfcf755e4fcfe8b6b7d9392ee2b5fd31ae132)" --encoding UTF-8 --encodingmode replace No emails were triggered. [isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins5842215610310097466.sh + Admin/jenkins/run_build slow + set -e + PROFILE=slow + shift + bin/isabelle components -a ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/jdk-17.0.4.1+1" ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/scala-3.2.0" Unknown ISABELLE_JDK_HOME -- Java development tools unavailable Getting "https://isabelle.sketis.net/components/jdk-17.0.4.1+1.tar.gz" Unpacking "/media/data/jenkins/.isabelle/contrib/jdk-17.0.4.1+1.tar.gz" Getting "https://isabelle.sketis.net/components/scala-3.2.0.tar.gz" Unpacking "/media/data/jenkins/.isabelle/contrib/scala-3.2.0.tar.gz" + bin/isabelle jedit -bf ### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle.jar) ... ### Building graph browser (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle_graphbrowser.jar) ... Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. ### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle_admin.jar) ... ### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-nightly-slow/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ... + 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.12). + 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.10.7 + bin/isabelle ci_build_slow === CONFIGURATION === ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g" ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-15c840d48c9a/x86_64-linux" ML_SYSTEM="polyml-5.9" ML_OPTIONS="-H 4000 --maxheap 20G" jobs = 1, threads = 8, numa = false === BUILD === Build started at Fri, 16 Sep 2022 23:37:37 GMT Isabelle id 49b16832f173 Build for AFP id b1e98098b68a === LOG === Session Pure/Pure Session FOL/FOL Session Pure/Pure-Examples Session Pure/Pure-ex Session Misc/Tools Session HOL/HOL (main) Session AFP/AWN (AFP) Session AFP/AODV (AFP slow) Session HOL/HOL-Cardinals (timing) 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-Combinatorics (main timing) 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-Eisbach Session HOL/HOL-Number_Theory (main timing) Session HOL/HOL-ex (timing) Session AFP/Automatic_Refinement (AFP) Session AFP/Refine_Monadic (AFP) Session HOL/HOL-Imperative_HOL (timing) Session AFP/HereditarilyFinite (AFP) Session AFP/Trie (AFP) Session AFP/Flyspeck-Tame (AFP) Session AFP/Flyspeck-Tame-Computation (AFP slow very_slow) Session AFP/Word_Lib (AFP) Session AFP/IP_Addresses (AFP) Session AFP/Simple_Firewall (AFP) Session AFP/Routing (AFP) Session AFP/Native_Word (AFP) Session AFP/Collections (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) Session AFP/ZFC_in_HOL (AFP) Session AFP/Category3 (AFP) Session AFP/MonoidalCategory (AFP) Session AFP/Bicategory (AFP slow) Building Pure ... Pure: theory Pure Pure: theory ML_Bootstrap Pure: theory Pure.Sessions Timing Pure (1 threads, 1.331s elapsed time, 1.348s cpu time, 0.046s GC time, factor 1.01) Finished Pure (0:00:23 elapsed time, 0:00:22 cpu time, factor 0.97) Building HOL ... HOL: theory Tools.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.Boolean_Algebras HOL: theory HOL.Set HOL: theory HOL.Typedef HOL: theory HOL.Fun 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.Meson HOL: theory HOL.Fields 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.Zorn HOL: theory HOL.BNF_Wellorder_Embedding HOL: theory HOL.ATP 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.Metis 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.Equiv_Relations HOL: theory HOL.Transfer HOL: theory HOL.Lifting HOL: theory HOL.Num HOL: theory HOL.Option HOL: theory HOL.Quotient HOL: theory HOL.Extraction HOL: theory HOL.Partial_Function HOL: theory HOL.Power HOL: theory HOL.Fun_Def HOL: theory HOL.Groups_Big HOL: theory HOL.Int HOL: theory HOL.Lattices_Big HOL: theory HOL.Lifting_Set HOL: theory HOL.Euclidean_Division HOL: theory HOL.Parity HOL: theory HOL.Divides HOL: theory HOL.Set_Interval HOL: theory HOL.Numeral_Simprocs HOL: theory HOL.Semiring_Normalization HOL: theory HOL.SMT HOL: theory HOL.Groebner_Basis HOL: theory HOL.Conditionally_Complete_Lattices HOL: theory HOL.Filter HOL: theory HOL.Presburger HOL: theory HOL.Sledgehammer HOL: theory HOL.List HOL: theory HOL.Groups_List HOL: theory HOL.Map HOL: theory HOL.Bit_Operations HOL: theory HOL.Enum HOL: theory HOL.Factorial HOL: theory HOL.Binomial HOL: theory HOL.Code_Numeral HOL: theory HOL.GCD HOL: theory HOL.String HOL: theory HOL.Random HOL: theory HOL.BNF_Greatest_Fixpoint HOL: theory HOL.Typerep HOL: theory HOL.Predicate 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.Mirabelle 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.Limits HOL: theory HOL.Inequalities 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 Preparing HOL/document ... Finished HOL/document (0:01:26 elapsed time) Preparing HOL/outline ... Finished HOL/outline (0:00:49 elapsed time) Timing HOL (8 threads, 252.949s elapsed time, 912.617s cpu time, 57.950s GC time, factor 3.61) Finished HOL (0:05:12 elapsed time, 0:17:11 cpu time, factor 3.31) Running JinjaThreads ... JinjaThreads: theory HOL-Eisbach.Eisbach JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1 JinjaThreads: theory Automatic_Refinement.Foldi JinjaThreads: theory Automatic_Refinement.Prio_List JinjaThreads: theory Finger-Trees.FingerTree JinjaThreads: theory HOL-Library.AList JinjaThreads: theory Collections.ICF_Tools JinjaThreads: theory HOL-Library.Adhoc_Overloading 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.Cancellation JinjaThreads: theory HOL-Library.Case_Converter JinjaThreads: theory HOL-Library.Code_Abstract_Nat JinjaThreads: theory Collections.Locale_Code JinjaThreads: theory Automatic_Refinement.Refine_Util JinjaThreads: theory Collections.Record_Intf JinjaThreads: theory HOL-Library.Code_Target_Nat JinjaThreads: theory HOL-Library.Code_Target_Int JinjaThreads: theory HOL-Library.Simps_Case_Conv JinjaThreads: theory HOL-Library.Complete_Partial_Order2 JinjaThreads: theory HOL-Library.Confluence JinjaThreads: theory HOL-Library.Code_Target_Numeral JinjaThreads: theory HOL-Library.Confluent_Quotient JinjaThreads: theory HOL-Library.Infinite_Set JinjaThreads: theory HOL-Library.Multiset JinjaThreads: theory HOL-Library.Nat_Bijection JinjaThreads: theory Automatic_Refinement.Anti_Unification JinjaThreads: theory Automatic_Refinement.Attr_Comb JinjaThreads: theory Automatic_Refinement.Autoref_Data JinjaThreads: theory Automatic_Refinement.Indep_Vars JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp JinjaThreads: theory Automatic_Refinement.Tagged_Solver JinjaThreads: theory Automatic_Refinement.Select_Solve JinjaThreads: theory HOL-Library.Dlist JinjaThreads: theory HOL-Library.Old_Datatype JinjaThreads: theory HOL-Library.Option_ord JinjaThreads: theory HOL-Library.Phantom_Type JinjaThreads: theory Trie.Trie JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs JinjaThreads: theory HOL-Library.RBT_Impl JinjaThreads: theory HOL-Library.Signed_Division JinjaThreads: theory HOL-Library.Sublist JinjaThreads: theory HOL-Library.Cardinality JinjaThreads: theory HOL-Library.Transitive_Closure_Table JinjaThreads: theory HOL-Library.While_Combinator JinjaThreads: theory FinFun.FinFun JinjaThreads: theory HOL-Library.Numeral_Type JinjaThreads: theory Collections.DatRef JinjaThreads: theory HOL-Library.Countable JinjaThreads: theory JinjaThreads.Set_Monad JinjaThreads: theory JinjaThreads.Set_without_equal JinjaThreads: theory Native_Word.Code_Int_Integer_Conversion JinjaThreads: theory Refine_Monadic.Refine_Chapter JinjaThreads: theory HOL-Library.Type_Length JinjaThreads: theory HOL-Library.Word JinjaThreads: theory Word_Lib.More_Arithmetic JinjaThreads: theory HOL-Library.Countable_Set JinjaThreads: theory JinjaThreads.Auxiliary JinjaThreads: theory Binomial-Heaps.BinomialHeap JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap JinjaThreads: theory HOL-ex.Quicksort JinjaThreads: theory HOL-Library.Countable_Complete_Lattices JinjaThreads: theory Automatic_Refinement.Misc JinjaThreads: theory HOL-Library.Order_Continuity 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 Refine_Monadic.Refine_Mono_Prover JinjaThreads: theory Collections.SetIteratorOperations JinjaThreads: theory Word_Lib.Bit_Comprehension JinjaThreads: theory Word_Lib.More_Divides JinjaThreads: theory Word_Lib.Signed_Division_Word JinjaThreads: theory Word_Lib.More_Word JinjaThreads: theory Automatic_Refinement.Param_Tool JinjaThreads: theory Automatic_Refinement.Param_HOL JinjaThreads: theory Native_Word.Code_Target_Word_Base JinjaThreads: theory Word_Lib.Bit_Shifts_Infix_Syntax JinjaThreads: theory Word_Lib.Least_significant_bit JinjaThreads: theory Collections.Assoc_List JinjaThreads: theory Automatic_Refinement.Parametricity JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops JinjaThreads: theory Collections.Dlist_add 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 Word_Lib.Most_significant_bit JinjaThreads: theory Word_Lib.Generic_set_bit 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 Native_Word.Code_Target_Integer_Bit JinjaThreads: theory Coinductive.Lazy_LList JinjaThreads: theory Coinductive.TLList JinjaThreads: theory Native_Word.Word_Type_Copies JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL JinjaThreads: theory Coinductive.Lazy_TLList 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 Native_Word.Code_Target_Int_Bit JinjaThreads: theory Native_Word.Uint32 JinjaThreads: theory Collections.Code_Target_ICF 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 Collections.HashCode 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 Collections.SetSpec JinjaThreads: theory Collections.BinoPrioImpl JinjaThreads: theory Collections.SkewPrioImpl JinjaThreads: theory Collections.ListGA JinjaThreads: theory Collections.FTAnnotatedListImpl JinjaThreads: theory Collections.PrioByAnnotatedList JinjaThreads: theory Collections.Fifo JinjaThreads: theory Collections.PrioUniqueByAnnotatedList 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.ListSetImpl JinjaThreads: theory Collections.ListSetImpl_Invar JinjaThreads: theory Collections.ListSetImpl_NotDist JinjaThreads: theory Collections.ListSetImpl_Sorted JinjaThreads: theory Collections.SetByMap JinjaThreads: theory Collections.ArrayHashMap_Impl JinjaThreads: theory Collections.TrieSetImpl JinjaThreads: theory Collections.ArraySetImpl JinjaThreads: theory Collections.ArrayHashMap JinjaThreads: theory Collections.ArrayHashSet JinjaThreads: theory HOL-Library.RBT JinjaThreads: theory Collections.RBT_add JinjaThreads: theory Collections.RBTMapImpl JinjaThreads: theory Collections.RBTSetImpl JinjaThreads: theory Collections.HashMap_Impl JinjaThreads: theory Collections.HashMap 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.Code_Cardinality JinjaThreads: theory HOL-Library.Prefix_Order JinjaThreads: theory JinjaThreads.LTS JinjaThreads: theory JinjaThreads.Type JinjaThreads: theory JinjaThreads.FWState JinjaThreads: theory JinjaThreads.ListIndex JinjaThreads: theory JinjaThreads.Orders JinjaThreads: theory JinjaThreads.Semilat JinjaThreads: theory JinjaThreads.Err JinjaThreads: theory JinjaThreads.Listn JinjaThreads: theory JinjaThreads.Opt JinjaThreads: theory JinjaThreads.Product JinjaThreads: theory JinjaThreads.Semilattices JinjaThreads: theory HOL-Library.AList_Mapping JinjaThreads: theory JinjaThreads.Decl JinjaThreads: theory JinjaThreads.Typing_Framework JinjaThreads: theory JinjaThreads.SemilatAlg JinjaThreads: theory JinjaThreads.Kildall JinjaThreads: theory JinjaThreads.LBVSpec JinjaThreads: theory JinjaThreads.Typing_Framework_err JinjaThreads: theory JinjaThreads.Bisimulation 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.StartConfig JinjaThreads: theory JinjaThreads.JVMState 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.SC_Collections JinjaThreads: theory JinjaThreads.FWProgress 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.ExternalCallWF JinjaThreads: theory JinjaThreads.JMM_Heap JinjaThreads: theory JinjaThreads.SemiType JinjaThreads: theory JinjaThreads.BinOp JinjaThreads: theory JinjaThreads.JMM_Type JinjaThreads: theory JinjaThreads.JMM_Type2 JinjaThreads: theory JinjaThreads.JVM_SemiType JinjaThreads: theory JinjaThreads.Random_Scheduler JinjaThreads: theory JinjaThreads.Round_Robin JinjaThreads: theory JinjaThreads.JMM_Framework JinjaThreads: theory JinjaThreads.SC_Schedulers JinjaThreads: theory JinjaThreads.Expr JinjaThreads: theory JinjaThreads.JVMInstructions JinjaThreads: theory JinjaThreads.PCompiler JinjaThreads: theory JinjaThreads.PCompilerRefine 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.JHeap JinjaThreads: theory JinjaThreads.WWellForm JinjaThreads: theory JinjaThreads.WellType JinjaThreads: theory JinjaThreads.JVMExec JinjaThreads: theory JinjaThreads.J1State JinjaThreads: theory JinjaThreads.JVMDefensive JinjaThreads: theory JinjaThreads.SmallStep JinjaThreads: theory JinjaThreads.JVMExec_Execute JinjaThreads: theory JinjaThreads.Annotate JinjaThreads: theory JinjaThreads.J1Heap JinjaThreads: theory JinjaThreads.J1WellType JinjaThreads: theory JinjaThreads.JWellForm JinjaThreads: theory JinjaThreads.WellTypeRT JinjaThreads: theory JinjaThreads.JVMThreaded JinjaThreads: theory JinjaThreads.JMM_Typesafe JinjaThreads: theory JinjaThreads.Compiler1 JinjaThreads: theory JinjaThreads.J1WellForm JinjaThreads: theory JinjaThreads.Compiler2 JinjaThreads: theory JinjaThreads.Preprocessor JinjaThreads: theory JinjaThreads.JJ1WellForm JinjaThreads: theory JinjaThreads.ToString JinjaThreads: theory JinjaThreads.JMM_JVM JinjaThreads: theory JinjaThreads.JVM_Main JinjaThreads: theory JinjaThreads.JMM_Common JinjaThreads: theory JinjaThreads.Compiler JinjaThreads: theory JinjaThreads.Exception_Tables JinjaThreads: theory JinjaThreads.JMM_Typesafe2 JinjaThreads: theory JinjaThreads.BVSpec JinjaThreads: theory JinjaThreads.EffectMono JinjaThreads: theory JinjaThreads.TF_JVM JinjaThreads: theory JinjaThreads.BVConform JinjaThreads: theory JinjaThreads.TypeComp JinjaThreads: theory JinjaThreads.FWBisimDeadlock JinjaThreads: theory JinjaThreads.FWBisimLift JinjaThreads: theory JinjaThreads.J1 JinjaThreads: theory JinjaThreads.BVExec JinjaThreads: theory JinjaThreads.LBVJVM JinjaThreads: theory JinjaThreads.BVSpecTypeSafe JinjaThreads: theory JinjaThreads.BVNoTypeError JinjaThreads: theory JinjaThreads.BCVExec JinjaThreads: theory JinjaThreads.JVMExec_Execute2 JinjaThreads: theory JinjaThreads.BVProgressThreaded JinjaThreads: theory JinjaThreads.JVMTau JinjaThreads: theory JinjaThreads.Common_Main JinjaThreads: theory JinjaThreads.J1Deadlock JinjaThreads: theory JinjaThreads.Execs JinjaThreads: theory JinjaThreads.DefAssPreservation JinjaThreads: theory JinjaThreads.Threaded JinjaThreads: theory JinjaThreads.Progress JinjaThreads: theory JinjaThreads.TypeSafe JinjaThreads: theory JinjaThreads.J1JVMBisim JinjaThreads: theory JinjaThreads.J0 JinjaThreads: theory JinjaThreads.JMM_J JinjaThreads: theory JinjaThreads.ProgressThreaded JinjaThreads: theory JinjaThreads.J_Execute JinjaThreads: theory JinjaThreads.JVMDeadlocked JinjaThreads: theory JinjaThreads.DRF_JVM JinjaThreads: theory JinjaThreads.JVM_Execute JinjaThreads: theory JinjaThreads.JVM_Execute2 JinjaThreads: theory JinjaThreads.Deadlocked JinjaThreads: theory JinjaThreads.DRF_J JinjaThreads: theory JinjaThreads.BV_Main JinjaThreads: theory JinjaThreads.J_Main JinjaThreads: theory JinjaThreads.J0Bisim JinjaThreads: theory JinjaThreads.J0J1Bisim JinjaThreads: theory JinjaThreads.Correctness1 JinjaThreads: theory JinjaThreads.Correctness1Threaded JinjaThreads: theory JinjaThreads.Code_Generation 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.J1JVM JinjaThreads: theory JinjaThreads.JVMJ1 JinjaThreads: theory JinjaThreads.Execute_Main JinjaThreads: theory JinjaThreads.Correctness2 JinjaThreads: theory JinjaThreads.Correctness JinjaThreads: theory JinjaThreads.JMM_Compiler JinjaThreads: theory JinjaThreads.SC_Interp JinjaThreads: theory JinjaThreads.Compiler_Main JinjaThreads: theory JinjaThreads.JMM_Interp JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2 JinjaThreads: theory JinjaThreads.JMM JinjaThreads: theory JinjaThreads.MM_Main JinjaThreads: theory JinjaThreads.JinjaThreads Preparing JinjaThreads/document ... Finished JinjaThreads/document (0:01:24 elapsed time) Preparing JinjaThreads/outline ... Finished JinjaThreads/outline (0:00:34 elapsed time) Timing JinjaThreads (8 threads, 3547.652s elapsed time, 16307.565s cpu time, 6318.783s GC time, factor 4.60) Finished JinjaThreads (0:59:10 elapsed time, 4:31:50 cpu time, factor 4.59) Building Flyspeck-Tame ... Flyspeck-Tame: theory Flyspeck-Tame.ListAux Flyspeck-Tame: theory Flyspeck-Tame.RTranCl Flyspeck-Tame: theory HOL-Library.AList Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order Flyspeck-Tame: theory HOL-Library.Code_Target_Int Flyspeck-Tame: theory HOL-Library.IArray Flyspeck-Tame: theory HOL-Library.While_Combinator Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso Flyspeck-Tame: theory HOL-Library.Code_Target_Nat 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.ArchCompAux Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps 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 Preparing Flyspeck-Tame/document ... Finished Flyspeck-Tame/document (0:00:13 elapsed time) Preparing Flyspeck-Tame/outline ... Finished Flyspeck-Tame/outline (0:00:06 elapsed time) Timing Flyspeck-Tame (8 threads, 64.968s elapsed time, 346.997s cpu time, 28.457s GC time, factor 5.34) Finished Flyspeck-Tame (0:01:45 elapsed time, 0:07:08 cpu time, factor 4.07) 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, 16243.038s elapsed time, 24147.610s cpu time, 772.887s GC time, factor 1.49) Finished Flyspeck-Tame-Computation (4:30:45 elapsed time, 6:42:29 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.Inv_Cterms AWN: theory AWN.AWN_Invariants AWN: theory AWN.Pnet AWN: theory AWN.Closed AWN: theory AWN.AWN_SOS_Labels AWN: theory AWN.Qmsg AWN: theory AWN.OAWN_Invariants AWN: theory AWN.OAWN_SOS_Labels AWN: theory AWN.ONode_Lifting AWN: theory AWN.OPnet 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 Preparing AWN/document ... Finished AWN/document (0:00:08 elapsed time) Preparing AWN/outline ... Finished AWN/outline (0:00:05 elapsed time) Timing AWN (8 threads, 37.642s elapsed time, 184.411s cpu time, 10.535s GC time, factor 4.90) Finished AWN (0:01:07 elapsed time, 0:04:01 cpu time, factor 3.61) Running AODV ... AODV: theory AODV.Aodv_Basic AODV: theory AODV.A_Norreqid AODV: theory AODV.Aodv_Data 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.A_Aodv_Data AODV: theory AODV.A_Aodv_Message AODV: theory AODV.B_Aodv_Data AODV: theory AODV.B_Aodv_Message AODV: theory AODV.C_Aodv_Data AODV: theory AODV.C_Aodv_Message AODV: theory AODV.C_Fresher AODV: theory AODV.D_Aodv_Data AODV: theory AODV.Fresher AODV: theory AODV.A_Fresher AODV: theory AODV.D_Aodv_Message AODV: theory AODV.B_Fresher AODV: theory AODV.E_Aodv_Data AODV: theory AODV.E_Aodv_Message AODV: theory AODV.A_Aodv AODV: theory AODV.Aodv AODV: theory AODV.B_Aodv AODV: theory AODV.C_Aodv AODV: theory AODV.E_Fresher AODV: theory AODV.D_Fresher AODV: theory AODV.D_Aodv AODV: theory AODV.E_Aodv 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.A_Aodv_Loop_Freedom AODV: theory AODV.C_Aodv_Predicates AODV: theory AODV.C_Loop_Freedom AODV: theory AODV.C_Quality_Increases AODV: theory AODV.C_Seq_Invariants AODV: theory AODV.C_OAodv AODV: theory AODV.C_Global_Invariants AODV: theory AODV.C_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.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.E_Aodv_Predicates AODV: theory AODV.E_Loop_Freedom AODV: theory AODV.E_Quality_Increases AODV: theory AODV.E_Seq_Invariants AODV: theory AODV.B_Global_Invariants AODV: theory AODV.E_OAodv AODV: theory AODV.B_Aodv_Loop_Freedom AODV: theory AODV.E_Global_Invariants AODV: theory AODV.E_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 Preparing AODV/document ... Finished AODV/document (0:00:18 elapsed time) Preparing AODV/outline ... Finished AODV/outline (0:00:10 elapsed time) Timing AODV (8 threads, 5351.781s elapsed time, 31076.359s cpu time, 1216.835s GC time, factor 5.81) Finished AODV (1:29:14 elapsed time, 8:37:58 cpu time, factor 5.80) Building Word_Lib ... Word_Lib: theory HOL-Library.Signed_Division Word_Lib: theory HOL-Library.Sublist Word_Lib: theory Word_Lib.Even_More_List Word_Lib: theory Word_Lib.More_Misc Word_Lib: theory HOL-Library.Phantom_Type Word_Lib: theory HOL-Library.Cardinality Word_Lib: theory HOL-Library.Numeral_Type Word_Lib: theory Word_Lib.More_Sublist Word_Lib: theory HOL-Library.Type_Length Word_Lib: theory HOL-Library.Word Word_Lib: theory Word_Lib.More_Arithmetic Word_Lib: theory Word_Lib.Bit_Comprehension Word_Lib: theory Word_Lib.Legacy_Aliases Word_Lib: theory Word_Lib.More_Divides Word_Lib: theory Word_Lib.Signed_Division_Word Word_Lib: theory Word_Lib.More_Word Word_Lib: theory Word_Lib.Bit_Shifts_Infix_Syntax Word_Lib: theory Word_Lib.Least_significant_bit Word_Lib: theory Word_Lib.Many_More Word_Lib: theory Word_Lib.Strict_part_mono Word_Lib: theory Word_Lib.Aligned Word_Lib: theory Word_Lib.Singleton_Bit_Shifts Word_Lib: theory Word_Lib.Most_significant_bit Word_Lib: theory Word_Lib.Generic_set_bit Word_Lib: theory Word_Lib.Next_and_Prev Word_Lib: theory Word_Lib.Bits_Int Word_Lib: theory Word_Lib.Typedef_Morphisms Word_Lib: theory Word_Lib.Reversed_Bit_Lists Word_Lib: theory Word_Lib.Bitwise Word_Lib: theory Word_Lib.Examples Word_Lib: theory HOL-Eisbach.Eisbach Word_Lib: theory Word_Lib.Signed_Words Word_Lib: theory Word_Lib.Bit_Comprehension_Int Word_Lib: theory Word_Lib.Hex_Words Word_Lib: theory Word_Lib.Syntax_Bundles Word_Lib: theory Word_Lib.Type_Syntax Word_Lib: theory Word_Lib.Word_Syntax Word_Lib: theory Word_Lib.Enumeration Word_Lib: theory Word_Lib.Rsplit Word_Lib: theory Word_Lib.Norm_Words Word_Lib: theory Word_Lib.Word_Names Word_Lib: theory Word_Lib.Word_16 Word_Lib: theory Word_Lib.Bitwise_Signed Word_Lib: theory Word_Lib.Enumeration_Word Word_Lib: theory HOL-Eisbach.Eisbach_Tools Word_Lib: theory Word_Lib.Word_EqI Word_Lib: theory Word_Lib.Word_Lemmas Word_Lib: theory Word_Lib.Word_8 Word_Lib: theory Word_Lib.More_Word_Operations Word_Lib: theory Word_Lib.Word_32 Word_Lib: theory Word_Lib.Word_64 Word_Lib: theory Word_Lib.Machine_Word_64_Basics Word_Lib: theory Word_Lib.Machine_Word_64 Word_Lib: theory Word_Lib.Machine_Word_32_Basics Word_Lib: theory Word_Lib.Machine_Word_32 Word_Lib: theory Word_Lib.Word_Lib_Sumo Word_Lib: theory Word_Lib.Guide Preparing Word_Lib/document ... Finished Word_Lib/document (0:00:03 elapsed time) Preparing Word_Lib/outline ... Finished Word_Lib/outline (0:00:02 elapsed time) Timing Word_Lib (8 threads, 40.726s elapsed time, 211.150s cpu time, 16.698s GC time, factor 5.18) Finished Word_Lib (0:01:05 elapsed time, 0:04:18 cpu time, factor 3.95) Building IP_Addresses ... IP_Addresses: theory IP_Addresses.NumberWang_IPv4 IP_Addresses: theory HOL-Library.Infinite_Set IP_Addresses: theory IP_Addresses.NumberWang_IPv6 IP_Addresses: theory HOL-Library.Option_ord IP_Addresses: theory HOL-Library.Cancellation IP_Addresses: theory HOL-Library.Multiset IP_Addresses: theory HOL-ex.Quicksort IP_Addresses: theory Automatic_Refinement.Misc IP_Addresses: theory IP_Addresses.Hs_Compat IP_Addresses: theory HOL-Library.Code_Abstract_Nat IP_Addresses: theory IP_Addresses.Lib_Numbers_toString IP_Addresses: theory HOL-Library.Product_Lexorder 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.WordInterval_Sorted IP_Addresses: theory IP_Addresses.IP_Address IP_Addresses: theory IP_Addresses.IPv4 IP_Addresses: theory IP_Addresses.Prefix_Match IP_Addresses: theory IP_Addresses.IPv6 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 Preparing IP_Addresses/document ... Finished IP_Addresses/document (0:00:03 elapsed time) Preparing IP_Addresses/outline ... Finished IP_Addresses/outline (0:00:02 elapsed time) Timing IP_Addresses (8 threads, 209.271s elapsed time, 682.774s cpu time, 48.891s GC time, factor 3.26) Finished IP_Addresses (0:04:16 elapsed time, 0:12:55 cpu time, factor 3.02) Building Simple_Firewall ... Simple_Firewall: theory HOL-Library.Char_ord Simple_Firewall: theory Simple_Firewall.GroupF Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString Simple_Firewall: theory Simple_Firewall.List_Product_More Simple_Firewall: theory Simple_Firewall.Option_Helpers 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_Semantics Simple_Firewall: theory Simple_Firewall.SimpleFw_toString Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw Simple_Firewall: theory Simple_Firewall.Shadowed Simple_Firewall: theory Simple_Firewall.Service_Matrix Preparing Simple_Firewall/document ... Finished Simple_Firewall/document (0:00:06 elapsed time) Preparing Simple_Firewall/outline ... Finished Simple_Firewall/outline (0:00:05 elapsed time) Timing Simple_Firewall (8 threads, 18.783s elapsed time, 77.516s cpu time, 6.326s GC time, factor 4.13) Finished Simple_Firewall (0:00:45 elapsed time, 0:02:06 cpu time, factor 2.79) Building Routing ... Routing: theory Pure-ex.Guess 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 Preparing Routing/document ... Finished Routing/document (0:00:01 elapsed time) Preparing Routing/outline ... Finished Routing/outline (0:00:01 elapsed time) Timing Routing (8 threads, 9.099s elapsed time, 27.954s cpu time, 1.235s GC time, factor 3.07) Finished Routing (0:00:29 elapsed time, 0:01:05 cpu time, factor 2.21) 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 Iptables_Semantics.Negation_Type_DNF Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev Iptables_Semantics: theory Iptables_Semantics.Ternary Iptables_Semantics: theory Native_Word.Code_Int_Integer_Conversion Iptables_Semantics: theory Iptables_Semantics.Conntrack_State Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags Iptables_Semantics: theory Native_Word.Code_Target_Integer_Bit Iptables_Semantics: theory Iptables_Semantics.Firewall_Common Iptables_Semantics: theory Iptables_Semantics.Word_Upto Iptables_Semantics: theory Iptables_Semantics.IpAddresses Iptables_Semantics: theory Iptables_Semantics.Ports Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax Iptables_Semantics: theory Native_Word.Code_Target_Int_Bit Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary Iptables_Semantics: theory Iptables_Semantics.Semantics Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics Iptables_Semantics: theory Iptables_Semantics.Matching Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update 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.Normalized_Matches Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic 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_Lemmas Iptables_Semantics: theory Iptables_Semantics.Example_Semantics Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize Iptables_Semantics: theory Iptables_Semantics.No_Spoof 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 Preparing Iptables_Semantics/document ... Finished Iptables_Semantics/document (0:00:19 elapsed time) Preparing Iptables_Semantics/outline ... Finished Iptables_Semantics/outline (0:00:10 elapsed time) Timing Iptables_Semantics (8 threads, 109.835s elapsed time, 510.115s cpu time, 49.409s GC time, factor 4.64) Finished Iptables_Semantics (0:02:47 elapsed time, 0:10:25 cpu time, factor 3.74) Building Iptables_Semantics_Examples ... Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall 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.SNS_IAS_Eduroam_Spoofing 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.Analyze_medium_sized_company 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 Preparing Iptables_Semantics_Examples/document ... Finished Iptables_Semantics_Examples/document (0:00:04 elapsed time) Preparing Iptables_Semantics_Examples/outline ... Finished Iptables_Semantics_Examples/outline (0:00:03 elapsed time) Timing Iptables_Semantics_Examples (8 threads, 227.254s elapsed time, 1244.555s cpu time, 98.748s GC time, factor 5.48) Finished Iptables_Semantics_Examples (0:04:11 elapsed time, 0:21:32 cpu time, factor 5.14) 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.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.Analyze_topos_generated Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large Run out of store - interrupting threads Iptables_Semantics_Examples_Big FAILED (see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.9_x86_64-linux/log/Iptables_Semantics_Examples_Big) *** Interrupt Building HOL-Library ... HOL-Library: theory HOL-Library.README HOL-Library: theory HOL-Library.Adhoc_Overloading HOL-Library: theory HOL-Library.Case_Converter HOL-Library: theory HOL-Library.BNF_Axiomatization HOL-Library: theory HOL-Library.BNF_Corec HOL-Library: theory HOL-Library.AList HOL-Library: theory HOL-Library.Cancellation HOL-Library: theory HOL-Library.Char_ord HOL-Library: theory HOL-Library.Code_Abstract_Nat HOL-Library: theory HOL-Library.Code_Abstract_Char HOL-Library: theory HOL-Library.Code_Binary_Nat HOL-Library: theory HOL-Library.Monad_Syntax HOL-Library: theory HOL-Library.Code_Target_Nat HOL-Library: theory HOL-Library.State_Monad HOL-Library: theory HOL-Library.Code_Prolog HOL-Library: theory HOL-Library.Code_Target_Int HOL-Library: theory HOL-Library.Code_Lazy HOL-Library: theory HOL-Library.Multiset HOL-Library: theory HOL-Library.Simps_Case_Conv HOL-Library: theory HOL-Library.Extended HOL-Library: theory HOL-Library.Code_Target_Numeral HOL-Library: theory HOL-Library.Code_Test HOL-Library: theory HOL-Library.Combine_PER HOL-Library: theory HOL-Library.Comparator HOL-Library: theory HOL-Library.Complete_Partial_Order2 HOL-Library: theory HOL-Library.DAList HOL-Library: theory HOL-Library.Conditional_Parametricity HOL-Library: theory HOL-Library.Confluence HOL-Library: theory HOL-Library.Confluent_Quotient HOL-Library: theory HOL-Library.Dlist HOL-Library: theory HOL-Library.Datatype_Records HOL-Library: theory HOL-Library.Debug 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.Groups_Big_Fun HOL-Library: theory HOL-Library.IArray HOL-Library: theory HOL-Library.Function_Division HOL-Library: theory HOL-Library.Infinite_Set HOL-Library: theory HOL-Library.Disjoint_Sets HOL-Library: theory HOL-Library.Equipollence HOL-Library: theory HOL-Library.Omega_Words_Fun HOL-Library: theory HOL-Library.Ramsey HOL-Library: theory HOL-Library.LaTeXsugar HOL-Library: theory HOL-Library.Lattice_Constructions HOL-Library: theory HOL-Library.ListVector HOL-Library: theory HOL-Library.List_Lenlexorder 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.NList HOL-Library: theory HOL-Library.Nat_Bijection HOL-Library: theory HOL-Library.Poly_Mapping HOL-Library: theory HOL-Library.Old_Datatype 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.DAList_Multiset HOL-Library: theory HOL-Library.Multiset_Order 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.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.Product_Plus HOL-Library: theory HOL-Library.Quotient_Syntax HOL-Library: theory HOL-Library.Quotient_Option HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck HOL-Library: theory HOL-Library.Quotient_Product HOL-Library: theory HOL-Library.Product_Order 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.Quotient_Type HOL-Library: theory HOL-Library.Cardinality HOL-Library: theory HOL-Library.RBT_Impl HOL-Library: theory HOL-Library.Finite_Lattice 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.Rounded_Division HOL-Library: theory HOL-Library.Set_Algebras HOL-Library: theory HOL-Library.Signed_Division HOL-Library: theory HOL-Library.Code_Cardinality HOL-Library: theory HOL-Library.Numeral_Type HOL-Library: theory HOL-Library.Sorting_Algorithms HOL-Library: theory HOL-Library.Sublist 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.Bourbaki_Witt_Fixpoint HOL-Library: theory HOL-Library.Z2 HOL-Library: theory HOL-Library.Saturated HOL-Library: theory HOL-Library.Word 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.Complex_Order 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.Tree_Multiset 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.Countable_Set HOL-Library: theory HOL-Library.FSet HOL-Library: theory HOL-Library.Liminf_Limsup 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.Log_Nat HOL-Library: theory HOL-Library.Lub_Glb HOL-Library: theory HOL-Library.Nonpos_Ints HOL-Library: theory HOL-Library.OptionalSugar 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.Finite_Map HOL-Library: theory HOL-Library.Extended_Nat HOL-Library: theory HOL-Library.Extended_Real HOL-Library: theory HOL-Library.Interval HOL-Library: theory HOL-Library.Float HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams HOL-Library: theory HOL-Library.Code_Target_Numeral_Float HOL-Library: theory HOL-Library.Interval_Float HOL-Library: theory HOL-Library.Extended_Nonnegative_Real HOL-Library: theory HOL-Library.Disjoint_FSets 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 Preparing HOL-Library/document ... Finished HOL-Library/document (0:00:50 elapsed time) Preparing HOL-Library/outline ... Finished HOL-Library/outline (0:00:28 elapsed time) Timing HOL-Library (8 threads, 146.282s elapsed time, 882.967s cpu time, 50.959s GC time, factor 6.04) Finished HOL-Library (0:03:33 elapsed time, 0:16:56 cpu time, factor 4.76) Building Category3 ... Category3: theory HOL-Cardinals.Fun_More Category3: theory HOL-Cardinals.Order_Relation_More Category3: theory HOL-Cardinals.Order_Union Category3: theory Category3.Category Category3: theory HereditarilyFinite.HF Category3: theory HOL-Cardinals.Wellorder_Extension Category3: theory HOL-Cardinals.Wellfounded_More Category3: theory HOL-Cardinals.Wellorder_Relation Category3: theory Category3.ConcreteCategory Category3: theory Category3.DiscreteCategory Category3: theory Category3.DualCategory Category3: theory Category3.EpiMonoIso Category3: theory HOL-Cardinals.Wellorder_Embedding Category3: theory HOL-Cardinals.Wellorder_Constructions Category3: theory Category3.InitialTerminal Category3: theory Category3.ProductCategory Category3: theory HOL-Cardinals.Cardinal_Order_Relation Category3: theory HOL-Cardinals.Ordinal_Arithmetic Category3: theory Category3.FreeCategory Category3: theory Category3.Functor Category3: theory HOL-Cardinals.Cardinal_Arithmetic Category3: theory HOL-Cardinals.Cardinals Category3: theory ZFC_in_HOL.ZFC_Library Category3: theory ZFC_in_HOL.ZFC_in_HOL Category3: theory ZFC_in_HOL.ZFC_Cardinals Category3: theory Category3.NaturalTransformation Category3: theory Category3.Subcategory Category3: theory Category3.BinaryFunctor Category3: theory Category3.SetCategory Category3: theory Category3.FunctorCategory Category3: theory Category3.SetCat Category3: theory Category3.Yoneda Category3: theory Category3.Adjunction Category3: theory Category3.EquivalenceOfCategories Category3: theory Category3.Limit Category3: theory Category3.CategoryWithPullbacks Category3: theory Category3.ZFC_SetCat Category3: theory Category3.CartesianCategory Category3: theory Category3.CartesianClosedCategory Category3: theory Category3.CategoryWithFiniteLimits Category3: theory Category3.HFSetCat Preparing Category3/document ... Finished Category3/document (0:00:23 elapsed time) Preparing Category3/outline ... Finished Category3/outline (0:00:08 elapsed time) Timing Category3 (8 threads, 312.729s elapsed time, 1566.668s cpu time, 147.193s GC time, factor 5.01) Finished Category3 (0:06:32 elapsed time, 0:28:48 cpu time, factor 4.40) Building MonoidalCategory ... MonoidalCategory: theory MonoidalCategory.MonoidalCategory MonoidalCategory: theory MonoidalCategory.MonoidalFunctor MonoidalCategory: theory MonoidalCategory.CartesianMonoidalCategory MonoidalCategory: theory MonoidalCategory.FreeMonoidalCategory Preparing MonoidalCategory/document ... Finished MonoidalCategory/document (0:00:11 elapsed time) Preparing MonoidalCategory/outline ... Finished MonoidalCategory/outline (0:00:04 elapsed time) Timing MonoidalCategory (8 threads, 302.647s elapsed time, 692.953s cpu time, 48.175s GC time, factor 2.29) Finished MonoidalCategory (0:06:14 elapsed time, 0:13:50 cpu time, factor 2.22) Running Bicategory ... Bicategory: theory Bicategory.IsomorphismClass Bicategory: theory Bicategory.Prebicategory Bicategory: theory Bicategory.Bicategory Bicategory: theory Bicategory.Coherence Bicategory: theory Bicategory.ConcreteBicategory Bicategory: theory Bicategory.InternalEquivalence Bicategory: theory Bicategory.Subbicategory Bicategory: theory Bicategory.CanonicalIsos Bicategory: theory Bicategory.Pseudofunctor Bicategory: theory Bicategory.Strictness Bicategory: theory Bicategory.CatBicat Bicategory: theory Bicategory.InternalAdjunction Bicategory: theory Bicategory.PseudonaturalTransformation Bicategory: theory Bicategory.Tabulation Bicategory: theory Bicategory.SpanBicategory Bicategory: theory Bicategory.EquivalenceOfBicategories Bicategory: theory Bicategory.Modification Bicategory: theory Bicategory.BicategoryOfSpans Preparing Bicategory/document ... Finished Bicategory/document (0:01:27 elapsed time) Preparing Bicategory/outline ... Finished Bicategory/outline (0:00:17 elapsed time) Timing Bicategory (8 threads, 4470.224s elapsed time, 11279.548s cpu time, 1995.586s GC time, factor 2.52) Finished Bicategory (1:14:36 elapsed time, 3:08:05 cpu time, factor 2.52) Building ConcurrentIMP ... ConcurrentIMP: theory ConcurrentIMP.CIMP_pred ConcurrentIMP: theory ConcurrentIMP.Infinite_Sequences ConcurrentIMP: theory ConcurrentIMP.LTL ConcurrentIMP: theory ConcurrentIMP.CIMP_lang ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg_rules ConcurrentIMP: theory ConcurrentIMP.CIMP ConcurrentIMP: theory ConcurrentIMP.CIMP_locales ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer Preparing ConcurrentIMP/document ... Finished ConcurrentIMP/document (0:00:04 elapsed time) Preparing ConcurrentIMP/outline ... Finished ConcurrentIMP/outline (0:00:03 elapsed time) Timing ConcurrentIMP (8 threads, 20.000s elapsed time, 70.717s cpu time, 5.664s GC time, factor 3.54) Finished ConcurrentIMP (0:00:45 elapsed time, 0:02:00 cpu time, factor 2.63) Running ConcurrentGC ... ConcurrentGC: theory ConcurrentGC.Model ConcurrentGC: theory ConcurrentGC.Proofs_Basis ConcurrentGC: theory ConcurrentGC.Global_Invariants ConcurrentGC: theory ConcurrentGC.Local_Invariants ConcurrentGC: theory ConcurrentGC.Tactics ConcurrentGC: theory ConcurrentGC.Concrete_heap ConcurrentGC: theory ConcurrentGC.Global_Invariants_Lemmas ConcurrentGC: theory ConcurrentGC.Concrete ConcurrentGC: theory ConcurrentGC.Global_Noninterference ConcurrentGC: theory ConcurrentGC.Local_Invariants_Lemmas ConcurrentGC: theory ConcurrentGC.Initial_Conditions ConcurrentGC: theory ConcurrentGC.MarkObject ConcurrentGC: theory ConcurrentGC.Noninterference ConcurrentGC: theory ConcurrentGC.Phases ConcurrentGC: theory ConcurrentGC.StrongTricolour ConcurrentGC: theory ConcurrentGC.TSO ConcurrentGC: theory ConcurrentGC.Valid_Refs ConcurrentGC: theory ConcurrentGC.Worklists ConcurrentGC: theory ConcurrentGC.Proofs Preparing ConcurrentGC/document ... Finished ConcurrentGC/document (0:00:08 elapsed time) Preparing ConcurrentGC/outline ... Finished ConcurrentGC/outline (0:00:06 elapsed time) Timing ConcurrentGC (8 threads, 1005.588s elapsed time, 5681.557s cpu time, 238.747s GC time, factor 5.65) Finished ConcurrentGC (0:16:48 elapsed time, 1:34:44 cpu time, factor 5.64) Unfinished session(s): Iptables_Semantics_Examples_Big === TIMING === Group slow: 8:46:21 elapsed time, 26:13:15 cpu time, factor 2.99 Group AFP: 9:16:22 elapsed time, 28:01:28 cpu time, factor 3.02 Group main: 0:08:45 elapsed time, 0:34:08 cpu time, factor 3.90 Group timing: 0:03:33 elapsed time, 0:16:56 cpu time, factor 4.76 Group very_slow: 4:46:32 elapsed time, 8:20:36 cpu time, factor 1.75 Overall: 9:37:44 elapsed time, 28:36:00 cpu time, factor 2.97 === FAILED SESSIONS === Session Iptables_Semantics_Examples_Big: FAILED 1 Build step 'Execute shell' marked build as failure 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 Email was triggered for: Failure - 1st Trigger Failure - Any was overridden by another trigger and will not send an email. Trigger Failure - Still was overridden by another trigger and will not send an email. Sending email for trigger: Failure - 1st Sending email to: isabelle-ci@mailman46.in.tum.de Finished: FAILURE