Skip to content
Failed

Console Output

01:33:08 Started by an SCM change

01:33:08 Running as SYSTEM

01:33:08 [EnvInject] - Loading node environment variables.

01:33:08 Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow

01:33:09 [isabelle-nightly-slow] $ hg showconfig paths.default

01:33:09 [isabelle-nightly-slow] $ hg pull --rev default

01:33:09 pulling from http://isabelle.in.tum.de/repos/isabelle/

01:33:09 real URL is https://isabelle.in.tum.de/repos/isabelle/

01:33:09 no changes found

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

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

01:33:09 [isabelle-nightly-slow] $ hg --config extensions.purge= clean --all

01:33:10 [isabelle-nightly-slow] $ hg log --rev . --template {node}

01:33:10 [isabelle-nightly-slow] $ hg log --rev . --template {rev}

01:33:10 [isabelle-nightly-slow] $ hg log --rev 89cf7c903acad179e40c10f2f6643d3c21448f47 --template exists\n

01:33:10 exists

01:33:10 [isabelle-nightly-slow] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(89cf7c903acad179e40c10f2f6643d3c21448f47)" --encoding UTF-8 --encodingmode replace

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

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

01:33:12 pulling from https://foss.heptapod.net/isa-afp/afp-devel/

01:33:12 no changes found

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

01:33:12 0 files updated, 0 files merged, 0 files removed, 0 files unresolved

01:33:12 [afp] $ hg --config extensions.purge= clean --all

01:33:12 [afp] $ hg log --rev . --template {node}

01:33:12 [afp] $ hg log --rev . --template {rev}

01:33:12 [afp] $ hg log --rev 589a6dadfa8457e122c1ce391455d52ddc134cf2 --template exists\n

01:33:12 exists

01:33:12 [afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(589a6dadfa8457e122c1ce391455d52ddc134cf2)" --encoding UTF-8 --encodingmode replace

01:33:12 No emails were triggered.

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

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

01:33:12 + set -e

01:33:12 + PROFILE=slow

01:33:12 + shift

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

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

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

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

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

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

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

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

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

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

01:33:14 3 warnings

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

01:33:42 ### Building Isabelle/jEdit ...

01:33:58 + bin/isabelle ocaml_setup

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

01:34:00 [NOTE] Package zarith is already installed (current version is 1.12).

01:34:00 + bin/isabelle ghc_setup

01:34:01 stack will use a sandboxed GHC it installed

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

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

01:34:01 stack ghc, stack ghci, stack runghc, or stack exec

01:34:01 The Glorious Glasgow Haskell Compilation System, version 8.8.4

01:34:02 + bin/isabelle ci_build_slow

01:34:05

01:34:05 === CONFIGURATION ===

01:34:05

01:34:05 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"

01:34:05 ISABELLE_BUILD_OPTIONS=""

01:34:05

01:34:05 ML_PLATFORM="x86_64-linux"

01:34:05 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686/x86_64-linux"

01:34:05 ML_SYSTEM="polyml-5.8.2"

01:34:05 ML_OPTIONS="-H 4000 --maxheap 20G"

01:34:05 jobs = 1, threads = 8, numa = false

01:34:05

01:34:05 === BUILD ===

01:34:05

01:34:05 Build started at Fri, 2 Apr 2021 23:34:05 GMT

01:34:05 Isabelle id 5fa2e2786ecf

01:34:06 Build for AFP id 589a6dadfa84

01:34:06

01:34:06 === LOG ===

01:34:06

01:34:07 Session Pure/Pure

01:34:07 Session FOL/FOL

01:34:08 Session Tools/Tools

01:34:08 Session HOL/HOL (main)

01:34:09 Session AFP/AWN (AFP)

01:34:09 Session AFP/AODV (AFP slow)

01:34:09 Session HOL/HOL-Cardinals (timing)

01:34:09 Session HOL/HOL-Library (main timing)

01:34:10 Session AFP/Binomial-Heaps (AFP)

01:34:10 Session AFP/ConcurrentIMP (AFP)

01:34:10 Session AFP/ConcurrentGC (AFP slow)

01:34:10 Session AFP/FinFun (AFP)

01:34:11 Session AFP/Finger-Trees (AFP)

01:34:11 Session HOL/HOL-Combinatorics (main timing)

01:34:11 Session HOL/HOL-Computational_Algebra (main timing)

01:34:11 Session HOL/HOL-Algebra (main timing)

01:34:12 Session HOL/HOL-Analysis (main timing)

01:34:13 Session AFP/Coinductive (AFP)

01:34:13 Session HOL/HOL-Eisbach

01:34:13 Session HOL/HOL-Number_Theory (main timing)

01:34:13 Session HOL/HOL-ex (timing)

01:34:14 Session AFP/Automatic_Refinement (AFP)

01:34:14 Session AFP/Refine_Monadic (AFP)

01:34:14 Session HOL/HOL-Imperative_HOL (timing)

01:34:15 Session AFP/HereditarilyFinite (AFP)

01:34:15 Session AFP/Category3 (AFP)

01:34:15 Session AFP/MonoidalCategory (AFP)

01:34:15 Session AFP/Bicategory (AFP slow)

01:34:16 Session AFP/Trie (AFP)

01:34:16 Session AFP/Flyspeck-Tame (AFP)

01:34:16 Session AFP/Flyspeck-Tame-Computation (AFP slow very_slow)

01:34:16 Session AFP/Word_Lib (AFP)

01:34:17 Session AFP/IP_Addresses (AFP)

01:34:17 Session AFP/Simple_Firewall (AFP)

01:34:17 Session AFP/Routing (AFP)

01:34:17 Session AFP/Native_Word (AFP)

01:34:18 Session AFP/Collections (AFP)

01:34:18 Session AFP/Iptables_Semantics (AFP)

01:34:18 Session AFP/Iptables_Semantics_Examples (AFP)

01:34:18 Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow)

01:34:18 Session AFP/JinjaThreads (AFP slow)

01:34:20 Building Pure ...

01:34:42 Pure: theory Pure

01:34:43 Pure: theory ML_Bootstrap

01:34:43 Pure: theory Pure.Sessions

01:34:46 Timing Pure (1 threads, 1.411s elapsed time, 1.441s cpu time, 0.059s GC time, factor 1.02)

01:34:46 Finished Pure (0:00:24 elapsed time, 0:00:24 cpu time, factor 0.98)

01:34:46 Building HOL ...

01:34:49 HOL: theory Tools.Code_Generator

01:34:54 HOL: theory HOL.HOL

01:35:00 HOL: theory HOL.Argo

01:35:00 HOL: theory HOL.Ctr_Sugar

01:35:00 HOL: theory HOL.Orderings

01:35:03 HOL: theory HOL.Groups

01:35:04 HOL: theory HOL.SAT

01:35:06 HOL: theory HOL.Lattices

01:35:09 HOL: theory HOL.Set

01:35:11 HOL: theory HOL.Fun

01:35:11 HOL: theory HOL.Typedef

01:35:12 HOL: theory HOL.Complete_Lattices

01:35:12 HOL: theory HOL.Rings

01:35:14 HOL: theory HOL.Inductive

01:35:18 HOL: theory HOL.Product_Type

01:35:18 HOL: theory HOL.Sum_Type

01:35:19 HOL: theory HOL.Complete_Partial_Order

01:35:24 HOL: theory HOL.Nat

01:35:27 HOL: theory HOL.Fields

01:35:27 HOL: theory HOL.Meson

01:35:27 HOL: theory HOL.ATP

01:35:32 HOL: theory HOL.Metis

01:35:33 HOL: theory HOL.Finite_Set

01:35:35 HOL: theory HOL.Relation

01:35:37 HOL: theory HOL.Transitive_Closure

01:35:38 HOL: theory HOL.Wellfounded

01:35:39 HOL: theory HOL.Fun_Def_Base

01:35:39 HOL: theory HOL.Hilbert_Choice

01:35:39 HOL: theory HOL.Wfrec

01:35:39 HOL: theory HOL.Order_Relation

01:35:40 HOL: theory HOL.BNF_Wellorder_Relation

01:35:43 HOL: theory HOL.BNF_Wellorder_Embedding

01:35:43 HOL: theory HOL.Zorn

01:35:44 HOL: theory HOL.BNF_Wellorder_Constructions

01:35:45 HOL: theory HOL.BNF_Cardinal_Order_Relation

01:35:46 HOL: theory HOL.BNF_Cardinal_Arithmetic

01:35:46 HOL: theory HOL.BNF_Def

01:35:49 HOL: theory HOL.BNF_Composition

01:35:49 HOL: theory HOL.Basic_BNFs

01:35:49 HOL: theory HOL.BNF_Fixpoint_Base

01:35:54 HOL: theory HOL.BNF_Least_Fixpoint

01:35:59 HOL: theory HOL.Basic_BNF_LFPs

01:35:59 HOL: theory HOL.Transfer

01:36:00 HOL: theory HOL.Num

01:36:05 HOL: theory HOL.Power

01:36:09 HOL: theory HOL.Groups_Big

01:36:12 HOL: theory HOL.Equiv_Relations

01:36:12 HOL: theory HOL.Lifting

01:36:15 HOL: theory HOL.Lifting_Set

01:36:15 HOL: theory HOL.Option

01:36:15 HOL: theory HOL.Quotient

01:36:16 HOL: theory HOL.Extraction

01:36:16 HOL: theory HOL.Lattices_Big

01:36:16 HOL: theory HOL.Partial_Function

01:36:17 HOL: theory HOL.Fun_Def

01:36:22 HOL: theory HOL.Int

01:36:26 HOL: theory HOL.Euclidean_Division

01:36:38 HOL: theory HOL.Parity

01:36:46 HOL: theory HOL.Divides

01:36:49 HOL: theory HOL.Numeral_Simprocs

01:36:49 HOL: theory HOL.Code_Numeral

01:36:49 HOL: theory HOL.Set_Interval

01:36:50 HOL: theory HOL.Semiring_Normalization

01:36:50 HOL: theory HOL.SMT

01:36:54 HOL: theory HOL.Groebner_Basis

01:36:56 HOL: theory HOL.Conditionally_Complete_Lattices

01:36:56 HOL: theory HOL.Filter

01:36:56 HOL: theory HOL.Presburger

01:37:01 HOL: theory HOL.Sledgehammer

01:37:05 HOL: theory HOL.List

01:37:16 HOL: theory HOL.Groups_List

01:37:16 HOL: theory HOL.Map

01:37:18 HOL: theory HOL.Factorial

01:37:18 HOL: theory HOL.Enum

01:37:18 HOL: theory HOL.GCD

01:37:18 HOL: theory HOL.Random

01:37:19 HOL: theory HOL.Binomial

01:37:23 HOL: theory HOL.String

01:37:25 HOL: theory HOL.BNF_Greatest_Fixpoint

01:37:25 HOL: theory HOL.Typerep

01:37:25 HOL: theory HOL.Predicate

01:37:27 HOL: theory HOL.Lazy_Sequence

01:37:27 HOL: theory HOL.Limited_Sequence

01:37:28 HOL: theory HOL.Code_Evaluation

01:37:29 HOL: theory HOL.Quickcheck_Random

01:37:34 HOL: theory HOL.Quickcheck_Exhaustive

01:37:34 HOL: theory HOL.Quickcheck_Narrowing

01:37:34 HOL: theory HOL.Random_Pred

01:37:35 HOL: theory HOL.Random_Sequence

01:37:39 HOL: theory HOL.Record

01:37:39 HOL: theory HOL.Predicate_Compile

01:37:42 HOL: theory HOL.Nitpick

01:37:49 HOL: theory HOL.Nunchaku

01:37:50 HOL: theory Main

01:37:52 HOL: theory HOL.Archimedean_Field

01:37:52 HOL: theory HOL.Hull

01:37:52 HOL: theory HOL.Topological_Spaces

01:37:52 HOL: theory HOL.Modules

01:37:53 HOL: theory HOL.Vector_Spaces

01:38:02 HOL: theory HOL.Rat

01:38:04 HOL: theory HOL.Real

01:38:06 HOL: theory HOL.Real_Vector_Spaces

01:38:25 HOL: theory HOL.Inequalities

01:38:25 HOL: theory HOL.Limits

01:38:32 HOL: theory HOL.Deriv

01:38:32 HOL: theory HOL.Series

01:38:35 HOL: theory HOL.NthRoot

01:38:36 HOL: theory HOL.Transcendental

01:38:42 HOL: theory HOL.Complex

01:38:43 HOL: theory HOL.MacLaurin

01:38:44 HOL: theory Complex_Main

01:39:55 Preparing HOL/document ...

01:41:12 Finished HOL/document (0:01:17 elapsed time)

01:41:12 Preparing HOL/outline ...

01:41:59 Finished HOL/outline (0:00:46 elapsed time)

01:42:02 Timing HOL (8 threads, 245.647s elapsed time, 808.774s cpu time, 66.065s GC time, factor 3.29)

01:42:02 Finished HOL (0:04:56 elapsed time, 0:15:15 cpu time, factor 3.09)

01:42:02 Running JinjaThreads ...

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

01:42:04 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1

01:42:04 JinjaThreads: theory Collections.ICF_Tools

01:42:04 JinjaThreads: theory Automatic_Refinement.Foldi

01:42:04 JinjaThreads: theory Automatic_Refinement.Prio_List

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

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

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

01:42:04 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot

01:42:04 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot

01:42:04 JinjaThreads: theory Collections.Ord_Code_Preproc

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

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

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

01:42:05 JinjaThreads: theory Collections.Locale_Code

01:42:05 JinjaThreads: theory Collections.Record_Intf

01:42:05 JinjaThreads: theory Automatic_Refinement.Refine_Util

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

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

01:42:05 JinjaThreads: theory HOL-Library.Bit_Operations

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

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

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

01:42:06 JinjaThreads: theory HOL-Library.Confluence

01:42:06 JinjaThreads: theory Automatic_Refinement.Anti_Unification

01:42:06 JinjaThreads: theory Automatic_Refinement.Attr_Comb

01:42:06 JinjaThreads: theory Automatic_Refinement.Autoref_Data

01:42:06 JinjaThreads: theory Automatic_Refinement.Indep_Vars

01:42:06 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp

01:42:06 JinjaThreads: theory Automatic_Refinement.Tagged_Solver

01:42:07 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms

01:42:07 JinjaThreads: theory Automatic_Refinement.Select_Solve

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

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

01:42:07 JinjaThreads: theory HOL-Library.Confluent_Quotient

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

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

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

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

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

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

01:42:07 JinjaThreads: theory Trie.Trie

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

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

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

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

01:42:08 JinjaThreads: theory HOL-Library.Signed_Division

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

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

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

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

01:42:10 JinjaThreads: theory FinFun.FinFun

01:42:10 JinjaThreads: theory HOL-Library.Numeral_Type

01:42:10 JinjaThreads: theory Collections.DatRef

01:42:10 JinjaThreads: theory HOL-Library.Countable

01:42:11 JinjaThreads: theory HOL-Library.Type_Length

01:42:11 JinjaThreads: theory JinjaThreads.Set_Monad

01:42:11 JinjaThreads: theory JinjaThreads.Set_without_equal

01:42:12 JinjaThreads: theory Refine_Monadic.Refine_Chapter

01:42:12 JinjaThreads: theory HOL-Library.Countable_Set

01:42:12 JinjaThreads: theory Binomial-Heaps.BinomialHeap

01:42:12 JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap

01:42:12 JinjaThreads: theory HOL-ex.Quicksort

01:42:12 JinjaThreads: theory HOL-Library.Countable_Complete_Lattices

01:42:12 JinjaThreads: theory JinjaThreads.Auxiliary

01:42:12 JinjaThreads: theory HOL-Library.Word

01:42:12 JinjaThreads: theory Automatic_Refinement.Misc

01:42:15 JinjaThreads: theory Word_Lib.More_Arithmetic

01:42:15 JinjaThreads: theory HOL-Library.Order_Continuity

01:42:16 JinjaThreads: theory HOL-Library.Extended_Nat

01:42:17 JinjaThreads: theory Coinductive.Coinductive_Nat

01:42:18 JinjaThreads: theory Automatic_Refinement.Refine_Lib

01:42:18 JinjaThreads: theory Collections.SetIterator

01:42:18 JinjaThreads: theory Collections.Sorted_List_Operations

01:42:18 JinjaThreads: theory Coinductive.Coinductive_List

01:42:19 JinjaThreads: theory Automatic_Refinement.Autoref_Phases

01:42:19 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging

01:42:19 JinjaThreads: theory Automatic_Refinement.Relators

01:42:20 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover

01:42:20 JinjaThreads: theory Collections.SetIteratorOperations

01:42:21 JinjaThreads: theory Automatic_Refinement.Param_Tool

01:42:21 JinjaThreads: theory Word_Lib.Bit_Comprehension

01:42:22 JinjaThreads: theory Automatic_Refinement.Param_HOL

01:42:22 JinjaThreads: theory Word_Lib.More_Divides

01:42:22 JinjaThreads: theory Word_Lib.Signed_Words

01:42:22 JinjaThreads: theory Word_Lib.Signed_Division_Word

01:42:22 JinjaThreads: theory Word_Lib.More_Word

01:42:23 JinjaThreads: theory Automatic_Refinement.Parametricity

01:42:23 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops

01:42:23 JinjaThreads: theory Collections.Assoc_List

01:42:24 JinjaThreads: theory Collections.Dlist_add

01:42:24 JinjaThreads: theory Collections.Proper_Iterator

01:42:24 JinjaThreads: theory Collections.SetIteratorGA

01:42:24 JinjaThreads: theory Word_Lib.Traditional_Infix_Syntax

01:42:24 JinjaThreads: theory Collections.Diff_Array

01:42:24 JinjaThreads: theory Collections.Trie_Impl

01:42:24 JinjaThreads: theory Collections.It_to_It

01:42:24 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel

01:42:25 JinjaThreads: theory Collections.Trie2

01:42:25 JinjaThreads: theory Automatic_Refinement.Autoref_Translate

01:42:25 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface

01:42:25 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo

01:42:25 JinjaThreads: theory Automatic_Refinement.Autoref_Tool

01:42:26 JinjaThreads: theory Word_Lib.Bits_Int

01:42:27 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL

01:42:27 JinjaThreads: theory Coinductive.Lazy_LList

01:42:27 JinjaThreads: theory Coinductive.TLList

01:42:28 JinjaThreads: theory Native_Word.More_Bits_Int

01:42:28 JinjaThreads: theory Word_Lib.Least_significant_bit

01:42:28 JinjaThreads: theory Word_Lib.Most_significant_bit

01:42:29 JinjaThreads: theory Word_Lib.Generic_set_bit

01:42:30 JinjaThreads: theory Coinductive.Lazy_TLList

01:42:30 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement

01:42:30 JinjaThreads: theory Collections.Idx_Iterator

01:42:30 JinjaThreads: theory Refine_Monadic.Refine_Misc

01:42:31 JinjaThreads: theory Native_Word.Code_Symbolic_Bits_Int

01:42:31 JinjaThreads: theory Refine_Monadic.RefineG_Domain

01:42:31 JinjaThreads: theory Refine_Monadic.RefineG_Transfer

01:42:31 JinjaThreads: theory Native_Word.Bits_Integer

01:42:32 JinjaThreads: theory Refine_Monadic.RefineG_Assert

01:42:32 JinjaThreads: theory Refine_Monadic.RefineG_Recursion

01:42:33 JinjaThreads: theory Refine_Monadic.RefineG_While

01:42:33 JinjaThreads: theory Refine_Monadic.Refine_Basic

01:42:34 JinjaThreads: theory Refine_Monadic.Refine_Det

01:42:39 JinjaThreads: theory Refine_Monadic.Refine_Heuristics

01:42:39 JinjaThreads: theory Refine_Monadic.Refine_Leof

01:42:39 JinjaThreads: theory Refine_Monadic.Refine_Pfun

01:42:39 JinjaThreads: theory Refine_Monadic.Refine_More_Comb

01:42:39 JinjaThreads: theory Refine_Monadic.Refine_While

01:42:41 JinjaThreads: theory Refine_Monadic.Refine_Transfer

01:42:42 JinjaThreads: theory Refine_Monadic.Autoref_Monadic

01:42:42 JinjaThreads: theory Refine_Monadic.Refine_Automation

01:42:42 JinjaThreads: theory Refine_Monadic.Refine_Foreach

01:42:45 JinjaThreads: theory Refine_Monadic.Refine_Monadic

01:42:47 JinjaThreads: theory Collections.Gen_Iterator

01:42:47 JinjaThreads: theory Collections.Intf_Map

01:42:47 JinjaThreads: theory Collections.Intf_Set

01:42:47 JinjaThreads: theory Native_Word.Code_Target_Bits_Int

01:42:47 JinjaThreads: theory Native_Word.Code_Target_Word_Base

01:42:47 JinjaThreads: theory Collections.Iterator

01:42:48 JinjaThreads: theory Collections.Code_Target_ICF

01:42:48 JinjaThreads: theory Native_Word.Uint32

01:42:48 JinjaThreads: theory Collections.Array_Iterator

01:42:48 JinjaThreads: theory Collections.ICF_Spec_Base

01:42:49 JinjaThreads: theory Collections.AnnotatedListSpec

01:42:49 JinjaThreads: theory Collections.ListSpec

01:42:49 JinjaThreads: theory Collections.MapSpec

01:42:49 JinjaThreads: theory Collections.PrioSpec

01:42:49 JinjaThreads: theory Collections.PrioUniqueSpec

01:42:49 JinjaThreads: theory Collections.SetSpec

01:42:52 JinjaThreads: theory Collections.HashCode

01:42:52 JinjaThreads: theory Collections.BinoPrioImpl

01:42:52 JinjaThreads: theory Collections.SkewPrioImpl

01:42:53 JinjaThreads: theory Collections.ListGA

01:42:54 JinjaThreads: theory Collections.FTAnnotatedListImpl

01:42:54 JinjaThreads: theory Collections.PrioByAnnotatedList

01:42:54 JinjaThreads: theory Collections.Fifo

01:42:56 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList

01:42:58 JinjaThreads: theory Collections.Algos

01:42:58 JinjaThreads: theory Collections.SetIndex

01:42:58 JinjaThreads: theory Collections.SetIteratorCollectionsGA

01:42:58 JinjaThreads: theory Collections.MapGA

01:42:58 JinjaThreads: theory Collections.SetGA

01:43:01 JinjaThreads: theory Collections.FTPrioImpl

01:43:02 JinjaThreads: theory Collections.FTPrioUniqueImpl

01:43:04 JinjaThreads: theory Collections.ArrayMapImpl

01:43:04 JinjaThreads: theory Collections.ListMapImpl

01:43:04 JinjaThreads: theory Collections.ListMapImpl_Invar

01:43:06 JinjaThreads: theory Collections.TrieMapImpl

01:43:07 JinjaThreads: theory Collections.ListSetImpl

01:43:07 JinjaThreads: theory Collections.ListSetImpl_Invar

01:43:07 JinjaThreads: theory Collections.ListSetImpl_NotDist

01:43:10 JinjaThreads: theory Collections.ListSetImpl_Sorted

01:43:12 JinjaThreads: theory Collections.SetByMap

01:43:12 JinjaThreads: theory Collections.ArrayHashMap_Impl

01:43:15 JinjaThreads: theory Collections.ArraySetImpl

01:43:15 JinjaThreads: theory Collections.TrieSetImpl

01:43:15 JinjaThreads: theory HOL-Library.RBT

01:43:16 JinjaThreads: theory Collections.RBT_add

01:43:17 JinjaThreads: theory Collections.ArrayHashMap

01:43:19 JinjaThreads: theory Collections.RBTMapImpl

01:43:24 JinjaThreads: theory Collections.ArrayHashSet

01:43:26 JinjaThreads: theory Collections.RBTSetImpl

01:43:26 JinjaThreads: theory Collections.HashMap_Impl

01:43:29 JinjaThreads: theory Collections.HashMap

01:43:35 JinjaThreads: theory Collections.HashSet

01:43:35 JinjaThreads: theory Collections.MapStdImpl

01:43:41 JinjaThreads: theory Collections.SetStdImpl

01:43:46 JinjaThreads: theory Collections.ICF_Impl

01:43:52 JinjaThreads: theory Collections.ICF_Refine_Monadic

01:43:52 JinjaThreads: theory Collections.ICF_Autoref

01:43:56 JinjaThreads: theory Collections.Collections

01:43:56 JinjaThreads: theory Collections.CollectionsV1

01:44:02 JinjaThreads: theory JinjaThreads.JT_ICF

01:44:02 JinjaThreads: theory JinjaThreads.Basic_Main

01:45:07 JinjaThreads: theory HOL-Library.Mapping

01:45:07 JinjaThreads: theory JinjaThreads.FWState

01:45:07 JinjaThreads: theory JinjaThreads.LTS

01:45:07 JinjaThreads: theory JinjaThreads.Type

01:45:07 JinjaThreads: theory JinjaThreads.ListIndex

01:45:07 JinjaThreads: theory JinjaThreads.Orders

01:45:07 JinjaThreads: theory JinjaThreads.Semilat

01:45:07 JinjaThreads: theory HOL-Library.Prefix_Order

01:45:08 JinjaThreads: theory JinjaThreads.Err

01:45:09 JinjaThreads: theory HOL-Library.AList_Mapping

01:45:09 JinjaThreads: theory JinjaThreads.Listn

01:45:09 JinjaThreads: theory JinjaThreads.Opt

01:45:09 JinjaThreads: theory JinjaThreads.Product

01:45:10 JinjaThreads: theory JinjaThreads.Semilattices

01:45:10 JinjaThreads: theory JinjaThreads.Decl

01:45:10 JinjaThreads: theory JinjaThreads.Typing_Framework

01:45:10 JinjaThreads: theory JinjaThreads.SemilatAlg

01:45:11 JinjaThreads: theory JinjaThreads.Kildall

01:45:11 JinjaThreads: theory JinjaThreads.Bisimulation

01:45:11 JinjaThreads: theory JinjaThreads.LBVSpec

01:45:11 JinjaThreads: theory JinjaThreads.Typing_Framework_err

01:45:11 JinjaThreads: theory JinjaThreads.LBVComplete

01:45:11 JinjaThreads: theory JinjaThreads.LBVCorrect

01:45:12 JinjaThreads: theory JinjaThreads.Abstract_BV

01:45:12 JinjaThreads: theory JinjaThreads.TypeRel

01:45:15 JinjaThreads: theory JinjaThreads.TypeRelRefine

01:45:16 JinjaThreads: theory JinjaThreads.Value

01:45:19 JinjaThreads: theory JinjaThreads.Exceptions

01:45:19 JinjaThreads: theory JinjaThreads.Heap

01:45:20 JinjaThreads: theory JinjaThreads.SystemClasses

01:45:21 JinjaThreads: theory JinjaThreads.MM

01:45:21 JinjaThreads: theory JinjaThreads.State

01:45:26 JinjaThreads: theory JinjaThreads.FWCondAction

01:45:27 JinjaThreads: theory JinjaThreads.FWInterrupt

01:45:27 JinjaThreads: theory JinjaThreads.FWThread

01:45:27 JinjaThreads: theory JinjaThreads.FWLock

01:45:27 JinjaThreads: theory JinjaThreads.FWWait

01:45:27 JinjaThreads: theory JinjaThreads.Observable_Events

01:45:29 JinjaThreads: theory JinjaThreads.FWLocking

01:45:30 JinjaThreads: theory JinjaThreads.FWLockingThread

01:45:30 JinjaThreads: theory JinjaThreads.FWWellform

01:45:31 JinjaThreads: theory JinjaThreads.FWLifting

01:45:31 JinjaThreads: theory JinjaThreads.FWSemantics

01:45:33 JinjaThreads: theory JinjaThreads.JVMState

01:45:33 JinjaThreads: theory JinjaThreads.StartConfig

01:45:33 JinjaThreads: theory JinjaThreads.JMM_Spec

01:45:34 JinjaThreads: theory JinjaThreads.FWLiftingSem

01:45:34 JinjaThreads: theory JinjaThreads.FWProgressAux

01:45:35 JinjaThreads: theory JinjaThreads.Conform

01:45:35 JinjaThreads: theory JinjaThreads.State_Refinement

01:45:35 JinjaThreads: theory JinjaThreads.FWDeadlock

01:45:36 JinjaThreads: theory JinjaThreads.FWLTS

01:45:36 JinjaThreads: theory JinjaThreads.ConformThreaded

01:45:36 JinjaThreads: theory JinjaThreads.ExternalCall

01:45:36 JinjaThreads: theory JinjaThreads.SC

01:45:38 JinjaThreads: theory JinjaThreads.SC_Collections

01:45:38 JinjaThreads: theory JinjaThreads.FWProgress

01:45:43 JinjaThreads: theory JinjaThreads.JMM_DRF

01:45:43 JinjaThreads: theory JinjaThreads.SC_Legal

01:45:46 JinjaThreads: theory JinjaThreads.FWBisimulation

01:45:46 JinjaThreads: theory JinjaThreads.FWInitFinLift

01:45:46 JinjaThreads: theory JinjaThreads.Non_Speculative

01:45:47 JinjaThreads: theory JinjaThreads.Scheduler

01:45:49 JinjaThreads: theory JinjaThreads.HB_Completion

01:45:50 JinjaThreads: theory JinjaThreads.SC_Completion

01:46:03 JinjaThreads: theory JinjaThreads.WellForm

01:46:03 JinjaThreads: theory JinjaThreads.ExternalCall_Execute

01:46:05 JinjaThreads: theory JinjaThreads.ExternalCallWF

01:46:05 JinjaThreads: theory JinjaThreads.JMM_Heap

01:46:06 JinjaThreads: theory JinjaThreads.SemiType

01:46:09 JinjaThreads: theory JinjaThreads.BinOp

01:46:10 JinjaThreads: theory JinjaThreads.JVM_SemiType

01:46:10 JinjaThreads: theory JinjaThreads.JMM_Type

01:46:12 JinjaThreads: theory JinjaThreads.JMM_Type2

01:46:24 JinjaThreads: theory JinjaThreads.Random_Scheduler

01:46:24 JinjaThreads: theory JinjaThreads.Round_Robin

01:46:29 JinjaThreads: theory JinjaThreads.JMM_Framework

01:46:41 JinjaThreads: theory JinjaThreads.SC_Schedulers

01:46:49 JinjaThreads: theory JinjaThreads.Expr

01:46:49 JinjaThreads: theory JinjaThreads.JVMInstructions

01:46:49 JinjaThreads: theory JinjaThreads.PCompiler

01:46:52 JinjaThreads: theory JinjaThreads.PCompilerRefine

01:47:08 JinjaThreads: theory JinjaThreads.JVMExceptions

01:47:09 JinjaThreads: theory JinjaThreads.Effect

01:47:10 JinjaThreads: theory JinjaThreads.JVMHeap

01:47:33 JinjaThreads: theory JinjaThreads.JVMExecInstr

01:47:34 JinjaThreads: theory JinjaThreads.CallExpr

01:47:34 JinjaThreads: theory JinjaThreads.DefAss

01:47:36 JinjaThreads: theory JinjaThreads.JHeap

01:47:36 JinjaThreads: theory JinjaThreads.WWellForm

01:47:36 JinjaThreads: theory JinjaThreads.WellType

01:47:37 JinjaThreads: theory JinjaThreads.JVMExec

01:47:49 JinjaThreads: theory JinjaThreads.JVMDefensive

01:47:52 JinjaThreads: theory JinjaThreads.J1State

01:47:52 JinjaThreads: theory JinjaThreads.SmallStep

01:48:00 JinjaThreads: theory JinjaThreads.Annotate

01:48:01 JinjaThreads: theory JinjaThreads.JWellForm

01:48:01 JinjaThreads: theory JinjaThreads.J1Heap

01:48:01 JinjaThreads: theory JinjaThreads.J1WellType

01:48:02 JinjaThreads: theory JinjaThreads.WellTypeRT

01:48:05 JinjaThreads: theory JinjaThreads.JVMThreaded

01:48:06 JinjaThreads: theory JinjaThreads.JMM_Typesafe

01:48:06 JinjaThreads: theory JinjaThreads.J1WellForm

01:48:06 JinjaThreads: theory JinjaThreads.JVMExec_Execute

01:48:07 JinjaThreads: theory JinjaThreads.Compiler1

01:48:07 JinjaThreads: theory JinjaThreads.Compiler2

01:48:12 JinjaThreads: theory JinjaThreads.Preprocessor

01:48:12 JinjaThreads: theory JinjaThreads.JJ1WellForm

01:48:15 JinjaThreads: theory JinjaThreads.ToString

01:48:19 JinjaThreads: theory JinjaThreads.JMM_JVM

01:48:19 JinjaThreads: theory JinjaThreads.JVM_Main

01:48:19 JinjaThreads: theory JinjaThreads.Compiler

01:48:20 JinjaThreads: theory JinjaThreads.Exception_Tables

01:48:21 JinjaThreads: theory JinjaThreads.JMM_Common

01:48:30 JinjaThreads: theory JinjaThreads.JMM_Typesafe2

01:48:34 JinjaThreads: theory JinjaThreads.BVSpec

01:48:34 JinjaThreads: theory JinjaThreads.EffectMono

01:48:35 JinjaThreads: theory JinjaThreads.TF_JVM

01:48:35 JinjaThreads: theory JinjaThreads.BVConform

01:48:36 JinjaThreads: theory JinjaThreads.TypeComp

01:48:39 JinjaThreads: theory JinjaThreads.FWBisimDeadlock

01:48:39 JinjaThreads: theory JinjaThreads.FWBisimLift

01:48:40 JinjaThreads: theory JinjaThreads.J1

01:48:44 JinjaThreads: theory JinjaThreads.BVExec

01:48:47 JinjaThreads: theory JinjaThreads.LBVJVM

01:48:47 JinjaThreads: theory JinjaThreads.BVSpecTypeSafe

01:49:16 JinjaThreads: theory JinjaThreads.BVNoTypeError

01:49:20 JinjaThreads: theory JinjaThreads.BCVExec

01:49:21 JinjaThreads: theory JinjaThreads.JVMExec_Execute2

01:49:21 JinjaThreads: theory JinjaThreads.BVProgressThreaded

01:49:22 JinjaThreads: theory JinjaThreads.JVMTau

01:49:30 JinjaThreads: theory JinjaThreads.Common_Main

01:49:45 JinjaThreads: theory JinjaThreads.J1Deadlock

01:49:59 JinjaThreads: theory JinjaThreads.Execs

01:50:14 JinjaThreads: theory JinjaThreads.DefAssPreservation

01:50:16 JinjaThreads: theory JinjaThreads.Threaded

01:50:18 JinjaThreads: theory JinjaThreads.Progress

01:50:27 JinjaThreads: theory JinjaThreads.TypeSafe

01:50:57 JinjaThreads: theory JinjaThreads.J0

01:50:57 JinjaThreads: theory JinjaThreads.JMM_J

01:50:58 JinjaThreads: theory JinjaThreads.ProgressThreaded

01:50:59 JinjaThreads: theory JinjaThreads.J_Execute

01:55:19 JinjaThreads: theory JinjaThreads.J1JVMBisim

01:55:32 JinjaThreads: theory JinjaThreads.Deadlocked

01:55:34 JinjaThreads: theory JinjaThreads.DRF_J

01:55:36 JinjaThreads: theory JinjaThreads.JVMDeadlocked

01:55:40 JinjaThreads: theory JinjaThreads.J_Main

01:55:41 JinjaThreads: theory JinjaThreads.DRF_JVM

01:55:41 JinjaThreads: theory JinjaThreads.JVM_Execute

01:55:42 JinjaThreads: theory JinjaThreads.J0Bisim

01:55:42 JinjaThreads: theory JinjaThreads.J0J1Bisim

01:55:46 JinjaThreads: theory JinjaThreads.JVM_Execute2

01:56:08 JinjaThreads: theory JinjaThreads.BV_Main

01:56:27 JinjaThreads: theory JinjaThreads.Correctness1

01:56:33 JinjaThreads: theory JinjaThreads.Correctness1Threaded

01:56:49 JinjaThreads: theory JinjaThreads.Code_Generation

01:56:58 JinjaThreads: theory JinjaThreads.ApprenticeChallenge

01:56:58 JinjaThreads: theory JinjaThreads.BufferExample

01:57:06 JinjaThreads: theory JinjaThreads.Java2Jinja

01:57:19 JinjaThreads: theory JinjaThreads.Examples_Main

01:59:44 JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe

01:59:48 JinjaThreads: theory JinjaThreads.JMM_J_Typesafe

02:00:26 JinjaThreads: theory JinjaThreads.J1JVM

02:00:32 JinjaThreads: theory JinjaThreads.JVMJ1

02:00:38 JinjaThreads: theory JinjaThreads.Execute_Main

02:02:44 JinjaThreads: theory JinjaThreads.Correctness2

02:12:09 JinjaThreads: theory JinjaThreads.Correctness

02:15:29 JinjaThreads: theory JinjaThreads.JMM_Compiler

02:15:40 JinjaThreads: theory JinjaThreads.SC_Interp

02:15:40 JinjaThreads: theory JinjaThreads.Compiler_Main

02:18:31 JinjaThreads: theory JinjaThreads.JMM_Interp

02:18:35 JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2

02:18:38 JinjaThreads: theory JinjaThreads.JMM

02:18:41 JinjaThreads: theory JinjaThreads.MM_Main

02:18:49 JinjaThreads: theory JinjaThreads.JinjaThreads

09:42:19 *** Timeout

09:42:19 JinjaThreads FAILED

09:42:19 (see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.8.2_x86_64-linux/log/JinjaThreads)

09:42:19 *** Interrupt

09:42:19 Building Flyspeck-Tame ...

09:42:21 Flyspeck-Tame: theory Flyspeck-Tame.ListAux

09:42:21 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order

09:42:21 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl

09:42:21 Flyspeck-Tame: theory HOL-Library.AList

09:42:21 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat

09:42:21 Flyspeck-Tame: theory HOL-Library.Code_Target_Int

09:42:21 Flyspeck-Tame: theory HOL-Library.IArray

09:42:21 Flyspeck-Tame: theory HOL-Library.While_Combinator

09:42:21 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso

09:42:21 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat

09:42:22 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral

09:42:22 Flyspeck-Tame: theory Flyspeck-Tame.Arch

09:42:22 Flyspeck-Tame: theory Flyspeck-Tame.Worklist

09:42:22 Flyspeck-Tame: theory Flyspeck-Tame.ListSum

09:42:22 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax

09:42:22 Flyspeck-Tame: theory Flyspeck-Tame.Rotation

09:42:23 Flyspeck-Tame: theory Flyspeck-Tame.Graph

09:42:23 Flyspeck-Tame: theory Flyspeck-Tame.Maps

09:42:23 Flyspeck-Tame: theory Trie.Trie

09:42:24 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision

09:42:24 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps

09:42:25 Flyspeck-Tame: theory Flyspeck-Tame.Tame

09:42:25 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator

09:42:26 Flyspeck-Tame: theory Trie.Tries

09:42:26 Flyspeck-Tame: theory Flyspeck-Tame.TameProps

09:42:26 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps

09:42:26 Flyspeck-Tame: theory Flyspeck-Tame.Plane

09:42:27 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps

09:42:27 Flyspeck-Tame: theory Flyspeck-Tame.Plane1

09:42:27 Flyspeck-Tame: theory Flyspeck-Tame.Generator

09:42:27 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum

09:42:31 Flyspeck-Tame: theory Flyspeck-Tame.Invariants

09:42:31 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux

09:42:32 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps

09:42:32 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps

09:42:32 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props

09:42:33 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound

09:42:33 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps

09:42:34 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps

09:42:34 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps

09:42:34 Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness

09:43:56 Preparing Flyspeck-Tame/document ...

09:44:08 Finished Flyspeck-Tame/document (0:00:12 elapsed time)

09:44:08 Preparing Flyspeck-Tame/outline ...

09:44:15 Finished Flyspeck-Tame/outline (0:00:06 elapsed time)

09:44:16 Timing Flyspeck-Tame (8 threads, 59.880s elapsed time, 324.491s cpu time, 25.775s GC time, factor 5.42)

09:44:16 Finished Flyspeck-Tame (0:01:35 elapsed time, 0:06:37 cpu time, factor 4.18)

09:44:16 Running Flyspeck-Tame-Computation ...

09:44:18 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.ArchComp

09:44:18 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.Completeness

14:05:59 Timing Flyspeck-Tame-Computation (8 threads, 15696.900s elapsed time, 23483.167s cpu time, 903.794s GC time, factor 1.50)

14:05:59 Finished Flyspeck-Tame-Computation (4:21:39 elapsed time, 6:31:25 cpu time, factor 1.50)

14:05:59 Building AWN ...

14:06:00 AWN: theory AWN.TransitionSystems

14:06:00 AWN: theory AWN.Lib

14:06:00 AWN: theory AWN.AWN

14:06:01 AWN: theory AWN.Invariants

14:06:01 AWN: theory AWN.OInvariants

14:06:11 AWN: theory AWN.AWN_Cterms

14:06:11 AWN: theory AWN.AWN_SOS

14:06:12 AWN: theory AWN.OAWN_SOS

14:06:14 AWN: theory AWN.AWN_Labels

14:06:15 AWN: theory AWN.Pnet

14:06:15 AWN: theory AWN.Inv_Cterms

14:06:15 AWN: theory AWN.AWN_Invariants

14:06:16 AWN: theory AWN.Closed

14:06:16 AWN: theory AWN.AWN_SOS_Labels

14:06:17 AWN: theory AWN.Qmsg

14:06:18 AWN: theory AWN.OAWN_Invariants

14:06:18 AWN: theory AWN.OAWN_SOS_Labels

14:06:18 AWN: theory AWN.OPnet

14:06:18 AWN: theory AWN.ONode_Lifting

14:06:19 AWN: theory AWN.OPnet_Lifting

14:06:19 AWN: theory AWN.OClosed_Lifting

14:06:19 AWN: theory AWN.OClosed_Transfer

14:06:19 AWN: theory AWN.OAWN_Convert

14:06:19 AWN: theory AWN.Qmsg_Lifting

14:06:20 AWN: theory AWN.AWN_Main

14:06:21 AWN: theory AWN.Toy

14:06:31 AWN: theory AWN.AWN_Term_Graph

14:07:01 Preparing AWN/document ...

14:07:10 Finished AWN/document (0:00:08 elapsed time)

14:07:10 Preparing AWN/outline ...

14:07:15 Finished AWN/outline (0:00:05 elapsed time)

14:07:16 Timing AWN (8 threads, 33.818s elapsed time, 163.762s cpu time, 6.997s GC time, factor 4.84)

14:07:16 Finished AWN (0:01:01 elapsed time, 0:03:39 cpu time, factor 3.57)

14:07:16 Running AODV ...

14:07:18 AODV: theory AODV.Aodv_Basic

14:07:19 AODV: theory AODV.A_Norreqid

14:07:19 AODV: theory AODV.Aodv_Message

14:07:19 AODV: theory AODV.Aodv_Data

14:07:19 AODV: theory AODV.B_Fwdrreps

14:07:19 AODV: theory AODV.C_Gtobcast

14:07:19 AODV: theory AODV.D_Fwdrreqs

14:07:19 AODV: theory AODV.E_All_ABCD

14:07:20 AODV: theory AODV.A_Aodv_Data

14:07:20 AODV: theory AODV.A_Aodv_Message

14:07:20 AODV: theory AODV.B_Aodv_Data

14:07:20 AODV: theory AODV.B_Aodv_Message

14:07:20 AODV: theory AODV.D_Aodv_Data

14:07:20 AODV: theory AODV.C_Aodv_Data

14:07:22 AODV: theory AODV.C_Fresher

14:07:22 AODV: theory AODV.Fresher

14:07:22 AODV: theory AODV.B_Fresher

14:07:23 AODV: theory AODV.C_Aodv_Message

14:07:23 AODV: theory AODV.D_Aodv_Message

14:07:23 AODV: theory AODV.A_Fresher

14:07:23 AODV: theory AODV.D_Fresher

14:07:23 AODV: theory AODV.E_Aodv_Data

14:07:23 AODV: theory AODV.E_Aodv_Message

14:07:24 AODV: theory AODV.A_Aodv

14:07:24 AODV: theory AODV.Aodv

14:07:25 AODV: theory AODV.B_Aodv

14:07:25 AODV: theory AODV.E_Fresher

14:07:25 AODV: theory AODV.C_Aodv

14:07:25 AODV: theory AODV.D_Aodv

14:07:25 AODV: theory AODV.E_Aodv

14:08:06 AODV: theory AODV.Aodv_Predicates

14:08:06 AODV: theory AODV.OAodv

14:08:07 AODV: theory AODV.Loop_Freedom

14:08:07 AODV: theory AODV.Quality_Increases

14:08:07 AODV: theory AODV.Seq_Invariants

14:08:08 AODV: theory AODV.Global_Invariants

14:08:08 AODV: theory AODV.Aodv_Loop_Freedom

14:08:14 AODV: theory AODV.A_Aodv_Predicates

14:08:14 AODV: theory AODV.A_Loop_Freedom

14:08:14 AODV: theory AODV.A_Quality_Increases

14:08:15 AODV: theory AODV.A_Seq_Invariants

14:08:15 AODV: theory AODV.A_OAodv

14:08:15 AODV: theory AODV.A_Global_Invariants

14:08:16 AODV: theory AODV.A_Aodv_Loop_Freedom

14:08:18 AODV: theory AODV.B_Aodv_Predicates

14:08:19 AODV: theory AODV.B_Loop_Freedom

14:08:19 AODV: theory AODV.B_Quality_Increases

14:08:19 AODV: theory AODV.B_Seq_Invariants

14:08:19 AODV: theory AODV.B_OAodv

14:08:20 AODV: theory AODV.B_Global_Invariants

14:08:20 AODV: theory AODV.B_Aodv_Loop_Freedom

14:08:21 AODV: theory AODV.C_Aodv_Predicates

14:08:21 AODV: theory AODV.C_OAodv

14:08:21 AODV: theory AODV.C_Loop_Freedom

14:08:22 AODV: theory AODV.C_Quality_Increases

14:08:22 AODV: theory AODV.C_Seq_Invariants

14:08:22 AODV: theory AODV.E_Aodv_Predicates

14:08:22 AODV: theory AODV.E_OAodv

14:08:22 AODV: theory AODV.E_Loop_Freedom

14:08:22 AODV: theory AODV.E_Quality_Increases

14:08:23 AODV: theory AODV.E_Seq_Invariants

14:08:23 AODV: theory AODV.C_Global_Invariants

14:08:23 AODV: theory AODV.E_Global_Invariants

14:08:24 AODV: theory AODV.C_Aodv_Loop_Freedom

14:08:24 AODV: theory AODV.E_Aodv_Loop_Freedom

14:08:30 AODV: theory AODV.D_Aodv_Predicates

14:08:30 AODV: theory AODV.D_OAodv

14:08:30 AODV: theory AODV.D_Loop_Freedom

14:08:30 AODV: theory AODV.D_Quality_Increases

14:08:30 AODV: theory AODV.D_Seq_Invariants

14:08:31 AODV: theory AODV.D_Global_Invariants

14:08:32 AODV: theory AODV.D_Aodv_Loop_Freedom

14:08:36 AODV: theory AODV.All

15:27:35 Preparing AODV/document ...

15:27:52 Finished AODV/document (0:00:17 elapsed time)

15:27:52 Preparing AODV/outline ...

15:28:02 Finished AODV/outline (0:00:10 elapsed time)

15:28:04 Timing AODV (8 threads, 4812.322s elapsed time, 28492.537s cpu time, 1108.725s GC time, factor 5.92)

15:28:04 Finished AODV (1:20:14 elapsed time, 7:54:55 cpu time, factor 5.92)

15:28:04 Building Word_Lib ...

15:28:05 Word_Lib: theory HOL-Eisbach.Eisbach

15:28:05 Word_Lib: theory HOL-Library.Boolean_Algebra

15:28:05 Word_Lib: theory HOL-Library.Phantom_Type

15:28:05 Word_Lib: theory HOL-Library.Signed_Division

15:28:05 Word_Lib: theory HOL-Library.Sublist

15:28:05 Word_Lib: theory Word_Lib.Enumeration

15:28:05 Word_Lib: theory Word_Lib.More_Misc

15:28:05 Word_Lib: theory Word_Lib.Even_More_List

15:28:06 Word_Lib: theory HOL-Library.Bit_Operations

15:28:07 Word_Lib: theory HOL-Library.Cardinality

15:28:07 Word_Lib: theory HOL-Eisbach.Eisbach_Tools

15:28:08 Word_Lib: theory Word_Lib.More_Sublist

15:28:08 Word_Lib: theory HOL-Library.Numeral_Type

15:28:09 Word_Lib: theory HOL-Library.Type_Length

15:28:12 Word_Lib: theory HOL-Library.Word

15:28:13 Word_Lib: theory Word_Lib.More_Arithmetic

15:28:19 Word_Lib: theory Word_Lib.Bit_Comprehension

15:28:19 Word_Lib: theory Word_Lib.Hex_Words

15:28:19 Word_Lib: theory Word_Lib.Legacy_Aliases

15:28:19 Word_Lib: theory Word_Lib.More_Divides

15:28:19 Word_Lib: theory Word_Lib.Signed_Words

15:28:19 Word_Lib: theory Word_Lib.Type_Syntax

15:28:19 Word_Lib: theory Word_Lib.Word_Syntax

15:28:19 Word_Lib: theory Word_Lib.Signed_Division_Word

15:28:19 Word_Lib: theory Word_Lib.Word_Names

15:28:19 Word_Lib: theory Word_Lib.More_Word

15:28:20 Word_Lib: theory Word_Lib.Enumeration_Word

15:28:20 Word_Lib: theory Word_Lib.Many_More

15:28:20 Word_Lib: theory Word_Lib.Strict_part_mono

15:28:20 Word_Lib: theory Word_Lib.Traditional_Infix_Syntax

15:28:20 Word_Lib: theory Word_Lib.Word_16

15:28:22 Word_Lib: theory Word_Lib.Bits_Int

15:28:22 Word_Lib: theory Word_Lib.Word_EqI

15:28:25 Word_Lib: theory Word_Lib.Least_significant_bit

15:28:25 Word_Lib: theory Word_Lib.Norm_Words

15:28:25 Word_Lib: theory Word_Lib.Rsplit

15:28:25 Word_Lib: theory Word_Lib.Most_significant_bit

15:28:25 Word_Lib: theory Word_Lib.Typedef_Morphisms

15:28:25 Word_Lib: theory Word_Lib.Generic_set_bit

15:28:26 Word_Lib: theory Word_Lib.Aligned

15:28:27 Word_Lib: theory Word_Lib.Next_and_Prev

15:28:27 Word_Lib: theory Word_Lib.Word_Lemmas

15:28:27 Word_Lib: theory Word_Lib.Reversed_Bit_Lists

15:28:29 Word_Lib: theory Word_Lib.Word_8

15:28:30 Word_Lib: theory Word_Lib.Ancient_Numeral

15:28:30 Word_Lib: theory Word_Lib.Bitwise

15:28:30 Word_Lib: theory Word_Lib.More_Word_Operations

15:28:30 Word_Lib: theory Word_Lib.Bitwise_Signed

15:28:30 Word_Lib: theory Word_Lib.Examples

15:28:30 Word_Lib: theory Word_Lib.Word_32

15:28:30 Word_Lib: theory Word_Lib.Word_64

15:28:31 Word_Lib: theory Word_Lib.Word_Lib_Sumo

15:28:34 Word_Lib: theory Word_Lib.Guide

15:29:16 Preparing Word_Lib/document ...

15:29:24 Finished Word_Lib/document (0:00:08 elapsed time)

15:29:24 Preparing Word_Lib/outline ...

15:29:30 Finished Word_Lib/outline (0:00:06 elapsed time)

15:29:32 Timing Word_Lib (8 threads, 47.946s elapsed time, 238.101s cpu time, 14.360s GC time, factor 4.97)

15:29:32 Finished Word_Lib (0:01:10 elapsed time, 0:04:45 cpu time, factor 4.04)

15:29:32 Building IP_Addresses ...

15:29:33 IP_Addresses: theory HOL-Library.Cancellation

15:29:33 IP_Addresses: theory HOL-Library.Option_ord

15:29:33 IP_Addresses: theory HOL-Library.Infinite_Set

15:29:33 IP_Addresses: theory IP_Addresses.NumberWang_IPv4

15:29:33 IP_Addresses: theory IP_Addresses.NumberWang_IPv6

15:29:34 IP_Addresses: theory HOL-Library.Multiset

15:29:39 IP_Addresses: theory HOL-ex.Quicksort

15:29:39 IP_Addresses: theory Automatic_Refinement.Misc

15:29:45 IP_Addresses: theory HOL-Library.Product_Lexorder

15:29:45 IP_Addresses: theory HOL-Library.Code_Abstract_Nat

15:29:45 IP_Addresses: theory IP_Addresses.Hs_Compat

15:29:45 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString

15:29:45 IP_Addresses: theory IP_Addresses.WordInterval

15:29:45 IP_Addresses: theory HOL-Library.Code_Target_Nat

15:29:45 IP_Addresses: theory IP_Addresses.Lib_List_toString

15:29:45 IP_Addresses: theory IP_Addresses.Lib_Word_toString

15:29:49 IP_Addresses: theory IP_Addresses.WordInterval_Sorted

15:29:49 IP_Addresses: theory IP_Addresses.IP_Address

15:29:55 IP_Addresses: theory IP_Addresses.IPv4

15:29:55 IP_Addresses: theory IP_Addresses.Prefix_Match

15:29:55 IP_Addresses: theory IP_Addresses.IPv6

15:29:56 IP_Addresses: theory IP_Addresses.CIDR_Split

15:30:54 IP_Addresses: theory IP_Addresses.IP_Address_toString

15:30:54 IP_Addresses: theory IP_Addresses.IP_Address_Parser

15:30:56 IP_Addresses: theory IP_Addresses.Prefix_Match_toString

15:33:19 Preparing IP_Addresses/document ...

15:33:24 Finished IP_Addresses/document (0:00:04 elapsed time)

15:33:24 Preparing IP_Addresses/outline ...

15:33:28 Finished IP_Addresses/outline (0:00:03 elapsed time)

15:33:28 Timing IP_Addresses (8 threads, 183.285s elapsed time, 647.763s cpu time, 49.949s GC time, factor 3.53)

15:33:28 Finished IP_Addresses (0:03:46 elapsed time, 0:12:14 cpu time, factor 3.25)

15:33:28 Building Simple_Firewall ...

15:33:30 Simple_Firewall: theory HOL-Library.Char_ord

15:33:30 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State

15:33:30 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString

15:33:30 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries

15:33:30 Simple_Firewall: theory Simple_Firewall.GroupF

15:33:30 Simple_Firewall: theory Simple_Firewall.List_Product_More

15:33:30 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString

15:33:30 Simple_Firewall: theory Simple_Firewall.Option_Helpers

15:33:30 Simple_Firewall: theory Simple_Firewall.Iface

15:33:31 Simple_Firewall: theory Simple_Firewall.L4_Protocol

15:33:33 Simple_Firewall: theory Simple_Firewall.Simple_Packet

15:33:33 Simple_Firewall: theory Simple_Firewall.Primitives_toString

15:33:37 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax

15:33:40 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics

15:33:40 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString

15:33:41 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw

15:33:41 Simple_Firewall: theory Simple_Firewall.Shadowed

15:33:41 Simple_Firewall: theory Simple_Firewall.Service_Matrix

15:34:10 Preparing Simple_Firewall/document ...

15:34:17 Finished Simple_Firewall/document (0:00:06 elapsed time)

15:34:17 Preparing Simple_Firewall/outline ...

15:34:23 Finished Simple_Firewall/outline (0:00:05 elapsed time)

15:34:24 Timing Simple_Firewall (8 threads, 17.581s elapsed time, 90.989s cpu time, 6.446s GC time, factor 5.18)

15:34:24 Finished Simple_Firewall (0:00:41 elapsed time, 0:02:16 cpu time, factor 3.30)

15:34:24 Building Routing ...

15:34:26 Routing: theory Routing.Linorder_Helper

15:34:26 Routing: theory HOL-Library.Adhoc_Overloading

15:34:26 Routing: theory HOL-Library.Monad_Syntax

15:34:27 Routing: theory Routing.Routing_Table

15:34:30 Routing: theory Routing.IpRoute_Parser

15:34:30 Routing: theory Routing.Linux_Router

15:34:53 Preparing Routing/document ...

15:34:56 Finished Routing/document (0:00:02 elapsed time)

15:34:56 Preparing Routing/outline ...

15:34:58 Finished Routing/outline (0:00:02 elapsed time)

15:34:59 Timing Routing (8 threads, 11.441s elapsed time, 32.647s cpu time, 1.235s GC time, factor 2.85)

15:34:59 Finished Routing (0:00:28 elapsed time, 0:01:05 cpu time, factor 2.27)

15:34:59 Building Iptables_Semantics ...

15:35:01 Iptables_Semantics: theory Iptables_Semantics.List_Misc

15:35:01 Iptables_Semantics: theory Iptables_Semantics.Negation_Type

15:35:03 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists

15:35:04 Iptables_Semantics: theory HOL-Library.Code_Target_Int

15:35:04 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors

15:35:04 Iptables_Semantics: theory Iptables_Semantics.Ternary

15:35:04 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize

15:35:04 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev

15:35:04 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF

15:35:04 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State

15:35:04 Iptables_Semantics: theory HOL-Library.LaTeXsugar

15:35:04 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags

15:35:04 Iptables_Semantics: theory Native_Word.More_Bits_Int

15:35:04 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common

15:35:04 Iptables_Semantics: theory Iptables_Semantics.Word_Upto

15:35:04 Iptables_Semantics: theory Iptables_Semantics.IpAddresses

15:35:05 Iptables_Semantics: theory Iptables_Semantics.Ports

15:35:05 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet

15:35:05 Iptables_Semantics: theory Native_Word.Code_Symbolic_Bits_Int

15:35:06 Iptables_Semantics: theory Native_Word.Bits_Integer

15:35:06 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax

15:35:18 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary

15:35:18 Iptables_Semantics: theory Iptables_Semantics.Semantics

15:35:18 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto

15:35:19 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics

15:35:19 Iptables_Semantics: theory Iptables_Semantics.Matching

15:35:20 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update

15:35:20 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful

15:35:20 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding

15:35:21 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary

15:35:21 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs

15:35:21 Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int

15:35:21 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings

15:35:22 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action

15:35:22 Iptables_Semantics: theory Iptables_Semantics.Optimizing

15:35:22 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic

15:35:23 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches

15:35:24 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching

15:35:25 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization

15:35:27 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher

15:35:29 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold

15:35:29 Iptables_Semantics: theory Iptables_Semantics.Ipassmt

15:35:32 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt

15:35:59 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas

15:35:59 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform

15:35:59 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics

15:35:59 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString

15:36:01 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize

15:36:01 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize

15:36:01 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize

15:36:01 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize

15:36:01 Iptables_Semantics: theory Iptables_Semantics.No_Spoof

15:36:06 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace

15:36:07 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace

15:36:09 Iptables_Semantics: theory Iptables_Semantics.Transform

15:36:13 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract

15:36:14 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance

15:36:18 Iptables_Semantics: theory Iptables_Semantics.Code_Interface

15:36:18 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings

15:36:19 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings

15:36:19 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics

15:36:19 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings

15:36:24 Iptables_Semantics: theory Iptables_Semantics.Parser

15:36:24 Iptables_Semantics: theory Iptables_Semantics.Parser6

15:36:25 Iptables_Semantics: theory Iptables_Semantics.Documentation

15:36:25 Iptables_Semantics: theory Iptables_Semantics.Code_haskell

15:37:39 Preparing Iptables_Semantics/document ...

15:37:57 Finished Iptables_Semantics/document (0:00:17 elapsed time)

15:37:57 Preparing Iptables_Semantics/outline ...

15:38:07 Finished Iptables_Semantics/outline (0:00:10 elapsed time)

15:38:09 Timing Iptables_Semantics (8 threads, 104.715s elapsed time, 520.595s cpu time, 47.922s GC time, factor 4.97)

15:38:09 Finished Iptables_Semantics (0:02:38 elapsed time, 0:10:29 cpu time, factor 3.98)

15:38:09 Building Iptables_Semantics_Examples ...

15:38:12 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall

15:38:12 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com

15:38:12 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example

15:38:12 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test

15:38:12 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test

15:38:12 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing

15:38:12 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof

15:38:12 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company

15:38:15 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail

15:38:16 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples

15:38:16 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed

15:38:17 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation

15:41:40 Preparing Iptables_Semantics_Examples/document ...

15:41:45 Finished Iptables_Semantics_Examples/document (0:00:04 elapsed time)

15:41:45 Preparing Iptables_Semantics_Examples/outline ...

15:41:49 Finished Iptables_Semantics_Examples/outline (0:00:04 elapsed time)

15:41:49 Timing Iptables_Semantics_Examples (8 threads, 184.740s elapsed time, 1343.429s cpu time, 121.937s GC time, factor 7.27)

15:41:49 Finished Iptables_Semantics_Examples (0:03:30 elapsed time, 0:23:13 cpu time, factor 6.63)

15:41:49 Running Iptables_Semantics_Examples_Big ...

15:41:52 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated

15:41:52 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small

15:41:52 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3

15:41:52 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall

15:41:52 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern

15:44:22 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large

16:14:48 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW

17:28:01 Preparing Iptables_Semantics_Examples_Big/document ...

17:28:05 Finished Iptables_Semantics_Examples_Big/document (0:00:03 elapsed time)

17:28:05 Preparing Iptables_Semantics_Examples_Big/outline ...

17:28:08 Finished Iptables_Semantics_Examples_Big/outline (0:00:03 elapsed time)

17:28:10 Timing Iptables_Semantics_Examples_Big (8 threads, 6364.483s elapsed time, 30761.617s cpu time, 13752.732s GC time, factor 4.83)

17:28:10 Finished Iptables_Semantics_Examples_Big (1:46:10 elapsed time, 8:32:52 cpu time, factor 4.83)

17:28:10 Building HOL-Library ...

17:28:12 HOL-Library: theory HOL-Library.Adhoc_Overloading

17:28:12 HOL-Library: theory HOL-Library.AList

17:28:12 HOL-Library: theory HOL-Library.Boolean_Algebra

17:28:12 HOL-Library: theory HOL-Library.Cancellation

17:28:12 HOL-Library: theory HOL-Library.BNF_Corec

17:28:12 HOL-Library: theory HOL-Library.BNF_Axiomatization

17:28:12 HOL-Library: theory HOL-Library.Case_Converter

17:28:12 HOL-Library: theory HOL-Library.Char_ord

17:28:12 HOL-Library: theory HOL-Library.Code_Abstract_Nat

17:28:13 HOL-Library: theory HOL-Library.Monad_Syntax

17:28:13 HOL-Library: theory HOL-Library.Code_Binary_Nat

17:28:13 HOL-Library: theory HOL-Library.State_Monad

17:28:13 HOL-Library: theory HOL-Library.Code_Target_Nat

17:28:13 HOL-Library: theory HOL-Library.Bit_Operations

17:28:13 HOL-Library: theory HOL-Library.Code_Prolog

17:28:13 HOL-Library: theory HOL-Library.Code_Lazy

17:28:13 HOL-Library: theory HOL-Library.Simps_Case_Conv

17:28:14 HOL-Library: theory HOL-Library.Extended

17:28:14 HOL-Library: theory HOL-Library.Multiset

17:28:14 HOL-Library: theory HOL-Library.Code_Target_Int

17:28:15 HOL-Library: theory HOL-Library.Code_Test

17:28:15 HOL-Library: theory HOL-Library.Code_Target_Numeral

17:28:15 HOL-Library: theory HOL-Library.Comparator

17:28:15 HOL-Library: theory HOL-Library.Conditional_Parametricity

17:28:15 HOL-Library: theory HOL-Library.DAList

17:28:16 HOL-Library: theory HOL-Library.Confluence

17:28:16 HOL-Library: theory HOL-Library.Datatype_Records

17:28:16 HOL-Library: theory HOL-Library.Confluent_Quotient

17:28:16 HOL-Library: theory HOL-Library.Dlist

17:28:16 HOL-Library: theory HOL-Library.Debug

17:28:16 HOL-Library: theory HOL-Library.Disjoint_Sets

17:28:16 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice

17:28:16 HOL-Library: theory HOL-Library.Fun_Lexorder

17:28:16 HOL-Library: theory HOL-Library.FuncSet

17:28:16 HOL-Library: theory HOL-Library.Function_Algebras

17:28:17 HOL-Library: theory HOL-Library.Groups_Big_Fun

17:28:17 HOL-Library: theory HOL-Library.Function_Division

17:28:17 HOL-Library: theory HOL-Library.IArray

17:28:17 HOL-Library: theory HOL-Library.Infinite_Set

17:28:17 HOL-Library: theory HOL-Library.LaTeXsugar

17:28:17 HOL-Library: theory HOL-Library.Lattice_Constructions

17:28:17 HOL-Library: theory HOL-Library.Lattice_Syntax

17:28:17 HOL-Library: theory HOL-Library.Combine_PER

17:28:17 HOL-Library: theory HOL-Library.Equipollence

17:28:17 HOL-Library: theory HOL-Library.Complete_Partial_Order2

17:28:17 HOL-Library: theory HOL-Library.Omega_Words_Fun

17:28:18 HOL-Library: theory HOL-Library.Ramsey

17:28:18 HOL-Library: theory HOL-Library.ListVector

17:28:18 HOL-Library: theory HOL-Library.List_Lenlexorder

17:28:18 HOL-Library: theory HOL-Library.List_Lexorder

17:28:18 HOL-Library: theory HOL-Library.Mapping

17:28:18 HOL-Library: theory HOL-Library.More_List

17:28:19 HOL-Library: theory HOL-Library.Nat_Bijection

17:28:19 HOL-Library: theory HOL-Library.Poly_Mapping

17:28:19 HOL-Library: theory HOL-Library.Stream

17:28:20 HOL-Library: theory HOL-Library.AList_Mapping

17:28:20 HOL-Library: theory HOL-Library.Old_Datatype

17:28:20 HOL-Library: theory HOL-Library.DAList_Multiset

17:28:20 HOL-Library: theory HOL-Library.Multiset_Order

17:28:21 HOL-Library: theory HOL-Library.Old_Recdef

17:28:23 HOL-Library: theory HOL-Library.Open_State_Syntax

17:28:23 HOL-Library: theory HOL-Library.Option_ord

17:28:23 HOL-Library: theory HOL-Library.Parallel

17:28:23 HOL-Library: theory HOL-Library.Pattern_Aliases

17:28:24 HOL-Library: theory HOL-Library.Perm

17:28:24 HOL-Library: theory HOL-Library.Phantom_Type

17:28:24 HOL-Library: theory HOL-Library.Power_By_Squaring

17:28:24 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs

17:28:24 HOL-Library: theory HOL-Library.Preorder

17:28:24 HOL-Library: theory HOL-Library.Product_Lexorder

17:28:24 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck

17:28:24 HOL-Library: theory HOL-Library.Product_Plus

17:28:25 HOL-Library: theory HOL-Library.Product_Order

17:28:25 HOL-Library: theory HOL-Library.Cardinality

17:28:25 HOL-Library: theory HOL-Library.Quotient_Syntax

17:28:25 HOL-Library: theory HOL-Library.Quotient_Type

17:28:26 HOL-Library: theory HOL-Library.Quotient_Option

17:28:26 HOL-Library: theory HOL-Library.Quotient_Product

17:28:26 HOL-Library: theory HOL-Library.Quotient_Set

17:28:26 HOL-Library: theory HOL-Library.Finite_Lattice

17:28:26 HOL-Library: theory HOL-Library.Quotient_Sum

17:28:26 HOL-Library: theory HOL-Library.RBT_Impl

17:28:26 HOL-Library: theory HOL-Library.Realizers

17:28:26 HOL-Library: theory HOL-Library.Quotient_List

17:28:26 HOL-Library: theory HOL-Library.Reflection

17:28:27 HOL-Library: theory HOL-Library.Refute

17:28:27 HOL-Library: theory HOL-Library.Rewrite

17:28:27 HOL-Library: theory HOL-Library.Set_Algebras

17:28:27 HOL-Library: theory HOL-Library.Signed_Division

17:28:28 HOL-Library: theory HOL-Library.Sorting_Algorithms

17:28:28 HOL-Library: theory HOL-Library.Sublist

17:28:28 HOL-Library: theory HOL-Library.Transitive_Closure_Table

17:28:28 HOL-Library: theory HOL-Library.Numeral_Type

17:28:29 HOL-Library: theory HOL-Library.Tree

17:28:29 HOL-Library: theory HOL-Library.Uprod

17:28:30 HOL-Library: theory HOL-Library.While_Combinator

17:28:30 HOL-Library: theory HOL-Library.Z2

17:28:30 HOL-Library: theory HOL-Library.Countable

17:28:31 HOL-Library: theory HOL-Library.Type_Length

17:28:31 HOL-Library: theory HOL-Library.BigO

17:28:31 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint

17:28:31 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float

17:28:31 HOL-Library: theory HOL-Library.Prefix_Order

17:28:31 HOL-Library: theory HOL-Library.Subseq_Order

17:28:31 HOL-Library: theory HOL-Library.Diagonal_Subsequence

17:28:31 HOL-Library: theory HOL-Library.Saturated

17:28:31 HOL-Library: theory HOL-Library.Word

17:28:31 HOL-Library: theory HOL-Library.Discrete

17:28:31 HOL-Library: theory HOL-Library.Going_To_Filter

17:28:31 HOL-Library: theory HOL-Library.Indicator_Function

17:28:31 HOL-Library: theory HOL-Library.Landau_Symbols

17:28:31 HOL-Library: theory HOL-Library.Lattice_Algebras

17:28:31 HOL-Library: theory HOL-Library.Countable_Set

17:28:32 HOL-Library: theory HOL-Library.FSet

17:28:32 HOL-Library: theory HOL-Library.Tree_Multiset

17:28:32 HOL-Library: theory HOL-Library.Liminf_Limsup

17:28:32 HOL-Library: theory HOL-Library.Countable_Complete_Lattices

17:28:33 HOL-Library: theory HOL-Library.Countable_Set_Type

17:28:33 HOL-Library: theory HOL-Library.Set_Idioms

17:28:33 HOL-Library: theory HOL-Library.Log_Nat

17:28:33 HOL-Library: theory HOL-Library.Lub_Glb

17:28:34 HOL-Library: theory HOL-Library.Nonpos_Ints

17:28:34 HOL-Library: theory HOL-Library.OptionalSugar

17:28:34 HOL-Library: theory HOL-Library.Periodic_Fun

17:28:34 HOL-Library: theory HOL-Library.Quadratic_Discriminant

17:28:34 HOL-Library: theory HOL-Library.Sum_of_Squares

17:28:34 HOL-Library: theory HOL-Library.Tree_Real

17:28:35 HOL-Library: theory HOL-Library.Order_Continuity

17:28:35 HOL-Library: theory HOL-Library.Finite_Map

17:28:35 HOL-Library: theory HOL-Library.Extended_Nat

17:28:35 HOL-Library: theory HOL-Library.Extended_Real

17:28:35 HOL-Library: theory HOL-Library.Interval

17:28:36 HOL-Library: theory HOL-Library.Float

17:28:39 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams

17:28:39 HOL-Library: theory HOL-Library.Interval_Float

17:28:39 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real

17:28:50 HOL-Library: theory HOL-Library.Disjoint_FSets

17:28:50 HOL-Library: theory HOL-Library.Library

17:29:14 HOL-Library: theory HOL-Library.RBT

17:29:14 HOL-Library: theory HOL-Library.RBT_Mapping

17:29:14 HOL-Library: theory HOL-Library.RBT_Set

17:31:20 Preparing HOL-Library/document ...

17:32:07 Finished HOL-Library/document (0:00:47 elapsed time)

17:32:07 Preparing HOL-Library/outline ...

17:32:37 Finished HOL-Library/outline (0:00:29 elapsed time)

17:32:39 Timing HOL-Library (8 threads, 124.922s elapsed time, 774.857s cpu time, 44.883s GC time, factor 6.20)

17:32:39 Finished HOL-Library (0:03:05 elapsed time, 0:15:01 cpu time, factor 4.87)

17:32:39 Building Category3 ...

17:32:42 Category3: theory HOL-Cardinals.Order_Relation_More

17:32:42 Category3: theory HOL-Cardinals.Fun_More

17:32:42 Category3: theory HOL-Cardinals.Order_Union

17:32:42 Category3: theory Category3.Category

17:32:42 Category3: theory HereditarilyFinite.HF

17:32:42 Category3: theory HOL-Cardinals.Wellorder_Extension

17:32:43 Category3: theory HOL-Cardinals.Wellfounded_More

17:32:43 Category3: theory HOL-Cardinals.Wellorder_Relation

17:32:43 Category3: theory Category3.ConcreteCategory

17:32:43 Category3: theory Category3.DiscreteCategory

17:32:43 Category3: theory Category3.DualCategory

17:32:43 Category3: theory Category3.EpiMonoIso

17:32:43 Category3: theory HOL-Cardinals.Wellorder_Embedding

17:32:44 Category3: theory HOL-Cardinals.Wellorder_Constructions

17:32:44 Category3: theory Category3.InitialTerminal

17:32:44 Category3: theory Category3.ProductCategory

17:32:45 Category3: theory HOL-Cardinals.Cardinal_Order_Relation

17:32:45 Category3: theory HOL-Cardinals.Ordinal_Arithmetic

17:32:45 Category3: theory Category3.FreeCategory

17:32:45 Category3: theory Category3.Functor

17:32:45 Category3: theory HOL-Cardinals.Cardinal_Arithmetic

17:32:46 Category3: theory HOL-Cardinals.Cardinals

17:32:49 Category3: theory Category3.Subcategory

17:32:49 Category3: theory Category3.NaturalTransformation

17:32:52 Category3: theory Category3.BinaryFunctor

17:32:52 Category3: theory Category3.SetCategory

17:32:55 Category3: theory Category3.SetCat

17:32:57 Category3: theory Category3.FunctorCategory

17:33:05 Category3: theory Category3.Yoneda

17:33:28 Category3: theory Category3.Adjunction

17:33:58 Category3: theory Category3.EquivalenceOfCategories

17:33:58 Category3: theory Category3.Limit

17:34:52 Category3: theory Category3.CartesianCategory

17:34:54 Category3: theory Category3.CategoryWithPullbacks

17:35:05 Category3: theory Category3.CartesianClosedCategory

17:35:06 Category3: theory Category3.CategoryWithFiniteLimits

17:35:07 Category3: theory Category3.HFSetCat

17:38:12 Preparing Category3/document ...

17:38:33 Finished Category3/document (0:00:20 elapsed time)

17:38:33 Preparing Category3/outline ...

17:38:41 Finished Category3/outline (0:00:08 elapsed time)

17:38:43 Timing Category3 (8 threads, 263.326s elapsed time, 1201.906s cpu time, 94.113s GC time, factor 4.56)

17:38:43 Finished Category3 (0:05:29 elapsed time, 0:22:19 cpu time, factor 4.06)

17:38:43 Building MonoidalCategory ...

17:38:47 MonoidalCategory: theory MonoidalCategory.MonoidalCategory

17:39:53 MonoidalCategory: theory MonoidalCategory.MonoidalFunctor

17:39:53 MonoidalCategory: theory MonoidalCategory.CartesianMonoidalCategory

17:40:18 MonoidalCategory: theory MonoidalCategory.FreeMonoidalCategory

17:45:15 Preparing MonoidalCategory/document ...

17:45:25 Finished MonoidalCategory/document (0:00:10 elapsed time)

17:45:25 Preparing MonoidalCategory/outline ...

17:45:30 Finished MonoidalCategory/outline (0:00:05 elapsed time)

17:45:33 Timing MonoidalCategory (8 threads, 325.021s elapsed time, 757.099s cpu time, 72.732s GC time, factor 2.33)

17:45:33 Finished MonoidalCategory (0:06:29 elapsed time, 0:14:46 cpu time, factor 2.27)

17:45:33 Running Bicategory ...

17:45:46 Bicategory: theory Bicategory.IsomorphismClass

17:45:46 Bicategory: theory Bicategory.Prebicategory

17:46:41 Bicategory: theory Bicategory.Bicategory

17:47:35 Bicategory: theory Bicategory.Coherence

17:47:39 Bicategory: theory Bicategory.InternalEquivalence

17:47:39 Bicategory: theory Bicategory.Subbicategory

17:50:06 Bicategory: theory Bicategory.CanonicalIsos

17:50:06 Bicategory: theory Bicategory.Pseudofunctor

17:53:55 Bicategory: theory Bicategory.Strictness

17:55:55 Bicategory: theory Bicategory.InternalAdjunction

17:59:18 Bicategory: theory Bicategory.PseudonaturalTransformation

17:59:18 Bicategory: theory Bicategory.Tabulation

17:59:18 Bicategory: theory Bicategory.SpanBicategory

18:06:18 Bicategory: theory Bicategory.EquivalenceOfBicategories

18:09:55 Bicategory: theory Bicategory.Modification

18:27:20 Bicategory: theory Bicategory.BicategoryOfSpans

18:48:07 Preparing Bicategory/document ...

18:49:30 Finished Bicategory/document (0:01:22 elapsed time)

18:49:30 Preparing Bicategory/outline ...

18:49:46 Finished Bicategory/outline (0:00:16 elapsed time)

18:49:48 Timing Bicategory (8 threads, 3743.500s elapsed time, 10185.819s cpu time, 1687.025s GC time, factor 2.72)

18:49:48 Finished Bicategory (1:02:29 elapsed time, 2:49:51 cpu time, factor 2.72)

18:49:48 Building ConcurrentIMP ...

18:49:50 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred

18:49:50 ConcurrentIMP: theory ConcurrentIMP.Infinite_Sequences

18:49:51 ConcurrentIMP: theory ConcurrentIMP.LTL

18:49:52 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang

18:49:58 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg

18:50:05 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg_rules

18:50:05 ConcurrentIMP: theory ConcurrentIMP.CIMP

18:50:06 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer

18:50:06 ConcurrentIMP: theory ConcurrentIMP.CIMP_locales

18:50:06 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer

18:50:33 Preparing ConcurrentIMP/document ...

18:50:37 Finished ConcurrentIMP/document (0:00:04 elapsed time)

18:50:37 Preparing ConcurrentIMP/outline ...

18:50:42 Finished ConcurrentIMP/outline (0:00:04 elapsed time)

18:50:43 Timing ConcurrentIMP (8 threads, 20.285s elapsed time, 67.451s cpu time, 5.148s GC time, factor 3.33)

18:50:43 Finished ConcurrentIMP (0:00:44 elapsed time, 0:01:54 cpu time, factor 2.55)

18:50:43 Running ConcurrentGC ...

18:50:45 ConcurrentGC: theory ConcurrentGC.Model

18:51:01 ConcurrentGC: theory ConcurrentGC.Proofs_Basis

18:51:12 ConcurrentGC: theory ConcurrentGC.Global_Invariants

18:51:12 ConcurrentGC: theory ConcurrentGC.Local_Invariants

18:51:12 ConcurrentGC: theory ConcurrentGC.Tactics

18:51:13 ConcurrentGC: theory ConcurrentGC.Concrete_heap

18:51:13 ConcurrentGC: theory ConcurrentGC.Global_Invariants_Lemmas

18:51:13 ConcurrentGC: theory ConcurrentGC.Concrete

18:51:15 ConcurrentGC: theory ConcurrentGC.Global_Noninterference

18:52:38 ConcurrentGC: theory ConcurrentGC.Local_Invariants_Lemmas

18:52:38 ConcurrentGC: theory ConcurrentGC.Initial_Conditions

18:52:39 ConcurrentGC: theory ConcurrentGC.MarkObject

18:52:39 ConcurrentGC: theory ConcurrentGC.Noninterference

18:52:39 ConcurrentGC: theory ConcurrentGC.Phases

18:52:40 ConcurrentGC: theory ConcurrentGC.StrongTricolour

18:52:40 ConcurrentGC: theory ConcurrentGC.TSO

18:52:40 ConcurrentGC: theory ConcurrentGC.Valid_Refs

18:52:40 ConcurrentGC: theory ConcurrentGC.Worklists

18:52:42 ConcurrentGC: theory ConcurrentGC.Proofs

19:07:25 Preparing ConcurrentGC/document ...

19:07:33 Finished ConcurrentGC/document (0:00:08 elapsed time)

19:07:33 Preparing ConcurrentGC/outline ...

19:07:39 Finished ConcurrentGC/outline (0:00:06 elapsed time)

19:07:40 Timing ConcurrentGC (8 threads, 996.987s elapsed time, 5616.914s cpu time, 298.377s GC time, factor 5.63)

19:07:40 Finished ConcurrentGC (0:16:39 elapsed time, 1:33:40 cpu time, factor 5.62)

19:07:40 Unfinished session(s): JinjaThreads

19:07:40

19:07:40 === TIMING ===

19:07:40

19:07:40 Group slow: 16:47:14 elapsed time, 42:01:20 cpu time, factor 2.50

19:07:40 Group AFP: 17:14:52 elapsed time, 43:44:45 cpu time, factor 2.54

19:07:40 Group main: 0:08:01 elapsed time, 0:30:16 cpu time, factor 3.77

19:07:40 Group timing: 0:03:05 elapsed time, 0:15:01 cpu time, factor 4.87

19:07:40 Group very_slow: 6:07:50 elapsed time, 15:04:17 cpu time, factor 2.46

19:07:40 Overall: 17:33:34 elapsed time, 44:15:26 cpu time, factor 2.52

19:07:40

19:07:40 === FAILED SESSIONS ===

19:07:40

19:07:40 Session JinjaThreads: FAILED 142

19:07:40 Build step 'Execute shell' marked build as failure

19:07:40 Archiving artifacts

19:07:48 Started calculate disk usage of build

19:07:48 Finished Calculation of disk usage of build in 0 seconds

19:07:52 Started calculate disk usage of workspace

19:07:52 Finished Calculation of disk usage of workspace in 0 seconds

19:07:52 No emails were triggered.

19:07:52 Finished: FAILURE