Console Output

09:00:50 Started from command line by admin
09:00:50 Running as SYSTEM
09:00:50 [EnvInject] - Loading node environment variables.
09:00:50 Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow
09:00:50 $ hg clone --rev default --noupdate http://isabelle.in.tum.de/repos/isabelle/ /media/data/jenkins/workspace/isabelle-nightly-slow
09:00:50 real URL is https://isabelle.in.tum.de/repos/isabelle/
09:01:55 adding changesets
09:01:55 adding manifests
09:01:55 adding file changes
09:01:56 added 73513 changesets with 201016 changes to 11315 files
09:01:56 new changesets a5a9c433f639:e52a9b208481
09:01:56 [isabelle-nightly-slow] $ hg update --rev default
09:01:57 3484 files updated, 0 files merged, 0 files removed, 0 files unresolved
09:01:57 [isabelle-nightly-slow] $ hg log --rev . --template {node}
09:01:57 [isabelle-nightly-slow] $ hg log --rev . --template {rev}
09:01:57 [isabelle-nightly-slow] $ hg log --rev e52a9b2084813a18973a14d44894178d4a81a8b8 --template exists\n
09:01:57 exists
09:01:57 [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(e52a9b2084813a18973a14d44894178d4a81a8b8)" --encoding UTF-8 --encodingmode replace
09:01:57 $ hg clone --rev default --noupdate https://foss.heptapod.net/isa-afp/afp-devel/ /media/data/jenkins/workspace/isabelle-nightly-slow/afp
09:02:44 adding changesets
09:02:44 adding manifests
09:02:44 adding file changes
09:02:45 added 11710 changesets with 78903 changes to 12097 files
09:02:45 new changesets 86acbdb19eec:34dff8ee061c
09:02:45 [afp] $ hg update --rev default
09:02:47 9664 files updated, 0 files merged, 0 files removed, 0 files unresolved
09:02:47 [afp] $ hg log --rev . --template {node}
09:02:47 [afp] $ hg log --rev . --template {rev}
09:02:47 [afp] $ hg log --rev 34dff8ee061c1acd2210177c824a42b9b9efd22c --template exists\n
09:02:47 exists
09:02:47 [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(34dff8ee061c1acd2210177c824a42b9b9efd22c)" --encoding UTF-8 --encodingmode replace
09:02:47 No emails were triggered.
09:02:48 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins195534519608099086.sh
09:02:48 + Admin/jenkins/run_build slow
09:02:48 + set -e
09:02:48 + PROFILE=slow
09:02:48 + shift
09:02:48 + bin/isabelle components -a
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/bash_process-1.2.3-1"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/bib2xhtml-20190409"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/csdp-6.1.1"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/cvc4-1.8"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/e-2.5-1"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/flatlaf-1.0"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/jdk-15.0.2+7"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/jedit_build-20210201"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/jfreechart-1.5.1"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/jortho-1.0-2"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/nunchaku-0.5"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/opam-2.0.7"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/postgresql-42.2.18"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/scala-2.13.5"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/smbc-0.4.1"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/spass-3.8ds-2"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/sqlite-jdbc-3.34.0"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/ssh-java-20190323"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/stack-2.5.1"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/vampire-4.2.2"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/verit-2020.10-rmx-1"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/xz-java-1.8"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/z3-4.4.0pre-3"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/zipperposition-2.0-1"
09:02:48 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/ci-extras-1"
09:02:48 Getting "https://isabelle.sketis.net/components/bash_process-1.2.3-1.tar.gz"
09:02:48 Unpacking "/media/data/jenkins/.isabelle/contrib/bash_process-1.2.3-1.tar.gz"
09:02:49 Getting "https://isabelle.sketis.net/components/bib2xhtml-20190409.tar.gz"
09:02:49 Unpacking "/media/data/jenkins/.isabelle/contrib/bib2xhtml-20190409.tar.gz"
09:02:49 Getting "https://isabelle.sketis.net/components/csdp-6.1.1.tar.gz"
09:02:49 Unpacking "/media/data/jenkins/.isabelle/contrib/csdp-6.1.1.tar.gz"
09:02:50 Getting "https://isabelle.sketis.net/components/cvc4-1.8.tar.gz"
09:02:50 Unpacking "/media/data/jenkins/.isabelle/contrib/cvc4-1.8.tar.gz"
09:02:51 Getting "https://isabelle.sketis.net/components/e-2.5-1.tar.gz"
09:02:52 Unpacking "/media/data/jenkins/.isabelle/contrib/e-2.5-1.tar.gz"
09:02:53 Getting "https://isabelle.sketis.net/components/flatlaf-1.0.tar.gz"
09:02:53 Unpacking "/media/data/jenkins/.isabelle/contrib/flatlaf-1.0.tar.gz"
09:02:53 Getting "https://isabelle.sketis.net/components/isabelle_fonts-20210322.tar.gz"
09:02:53 Unpacking "/media/data/jenkins/.isabelle/contrib/isabelle_fonts-20210322.tar.gz"
09:02:54 Getting "https://isabelle.sketis.net/components/jdk-15.0.2+7.tar.gz"
09:03:11 Unpacking "/media/data/jenkins/.isabelle/contrib/jdk-15.0.2+7.tar.gz"
09:03:24 Getting "https://isabelle.sketis.net/components/jedit_build-20210201.tar.gz"
09:03:25 Unpacking "/media/data/jenkins/.isabelle/contrib/jedit_build-20210201.tar.gz"
09:03:25 Getting "https://isabelle.sketis.net/components/jfreechart-1.5.1.tar.gz"
09:03:25 Unpacking "/media/data/jenkins/.isabelle/contrib/jfreechart-1.5.1.tar.gz"
09:03:26 Getting "https://isabelle.sketis.net/components/jortho-1.0-2.tar.gz"
09:03:26 Unpacking "/media/data/jenkins/.isabelle/contrib/jortho-1.0-2.tar.gz"
09:03:26 Getting "https://isabelle.sketis.net/components/kodkodi-1.5.6.tar.gz"
09:03:26 Unpacking "/media/data/jenkins/.isabelle/contrib/kodkodi-1.5.6.tar.gz"
09:03:27 Getting "https://isabelle.sketis.net/components/nunchaku-0.5.tar.gz"
09:03:28 Unpacking "/media/data/jenkins/.isabelle/contrib/nunchaku-0.5.tar.gz"
09:03:28 Getting "https://isabelle.sketis.net/components/opam-2.0.7.tar.gz"
09:03:28 Unpacking "/media/data/jenkins/.isabelle/contrib/opam-2.0.7.tar.gz"
09:03:29 Getting "https://isabelle.sketis.net/components/polyml-test-f86ae3dc1686.tar.gz"
09:03:30 Unpacking "/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686.tar.gz"
09:03:31 Getting "https://isabelle.sketis.net/components/postgresql-42.2.18.tar.gz"
09:03:31 Unpacking "/media/data/jenkins/.isabelle/contrib/postgresql-42.2.18.tar.gz"
09:03:31 Getting "https://isabelle.sketis.net/components/scala-2.13.5.tar.gz"
09:03:33 Unpacking "/media/data/jenkins/.isabelle/contrib/scala-2.13.5.tar.gz"
09:03:34 Getting "https://isabelle.sketis.net/components/smbc-0.4.1.tar.gz"
09:03:34 Unpacking "/media/data/jenkins/.isabelle/contrib/smbc-0.4.1.tar.gz"
09:03:34 Getting "https://isabelle.sketis.net/components/spass-3.8ds-2.tar.gz"
09:03:35 Unpacking "/media/data/jenkins/.isabelle/contrib/spass-3.8ds-2.tar.gz"
09:03:35 Getting "https://isabelle.sketis.net/components/sqlite-jdbc-3.34.0.tar.gz"
09:03:35 Unpacking "/media/data/jenkins/.isabelle/contrib/sqlite-jdbc-3.34.0.tar.gz"
09:03:36 Getting "https://isabelle.sketis.net/components/ssh-java-20190323.tar.gz"
09:03:36 Unpacking "/media/data/jenkins/.isabelle/contrib/ssh-java-20190323.tar.gz"
09:03:36 Getting "https://isabelle.sketis.net/components/stack-2.5.1.tar.gz"
09:03:38 Unpacking "/media/data/jenkins/.isabelle/contrib/stack-2.5.1.tar.gz"
09:03:39 Getting "https://isabelle.sketis.net/components/vampire-4.2.2.tar.gz"
09:03:40 Unpacking "/media/data/jenkins/.isabelle/contrib/vampire-4.2.2.tar.gz"
09:03:41 Getting "https://isabelle.sketis.net/components/verit-2020.10-rmx-1.tar.gz"
09:03:42 Unpacking "/media/data/jenkins/.isabelle/contrib/verit-2020.10-rmx-1.tar.gz"
09:03:42 Getting "https://isabelle.sketis.net/components/xz-java-1.8.tar.gz"
09:03:43 Unpacking "/media/data/jenkins/.isabelle/contrib/xz-java-1.8.tar.gz"
09:03:43 Getting "https://isabelle.sketis.net/components/z3-4.4.0pre-3.tar.gz"
09:03:44 Unpacking "/media/data/jenkins/.isabelle/contrib/z3-4.4.0pre-3.tar.gz"
09:03:45 Getting "https://isabelle.sketis.net/components/zipperposition-2.0-1.tar.gz"
09:03:45 Unpacking "/media/data/jenkins/.isabelle/contrib/zipperposition-2.0-1.tar.gz"
09:03:46 Getting "https://isabelle.sketis.net/components/ci-extras-1.tar.gz"
09:03:49 Unpacking "/media/data/jenkins/.isabelle/contrib/ci-extras-1.tar.gz"
09:03:49 + bin/isabelle jedit -bf
09:03:49 ### Building graph browser ...
09:03:49 warning: [options] bootstrap class path not set in conjunction with -source 7
09:03:49 warning: [options] source value 7 is obsolete and will be removed in a future release
09:03:49 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
09:03:50 Note: Some input files use or override a deprecated API.
09:03:50 Note: Recompile with -Xlint:deprecation for details.
09:03:50 Note: Some input files use unchecked or unsafe operations.
09:03:50 Note: Recompile with -Xlint:unchecked for details.
09:03:50 3 warnings
09:03:51 ### Building Isabelle/Scala ...
09:04:18 ### Building Isabelle/jEdit ...
09:04:33 + bin/isabelle ocaml_setup
09:04:33 [NOTE] Will configure from built-in defaults.
09:04:33 Checking for available remotes: rsync and local, git, mercurial.
09:04:33   - you won't be able to use darcs repositories unless you install the darcs command on your system.
09:04:33 
09:04:33 
09:04:33 <><> Fetching repository information ><><><><><><><><><><><><><><><><><><><><><>
09:04:39 [default] Initialised
09:04:41 
09:04:41 <><> Creating initial switch (ocaml-base-compiler.4.07.0) <><><><><><><><><><><>
09:04:44 
09:04:44 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
09:04:47 [ocaml-base-compiler.4.07.0] downloaded from cache at https://opam.ocaml.org/cache
09:04:47 
09:04:47 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
09:04:47 ∗ installed base-bigarray.base
09:04:47 ∗ installed base-threads.base
09:04:47 ∗ installed base-unix.base
09:06:15 ∗ installed ocaml-base-compiler.4.07.0
09:06:15 ∗ installed ocaml-config.1
09:06:15 ∗ installed ocaml.4.07.0
09:06:15 Done.
09:06:15 # Run eval $(opam env) to update the current shell environment
09:06:19 The following actions will be performed:
09:06:19   ∗ install ocamlfind 1.9.1 [required by zarith]
09:06:19   ∗ install conf-gmp  3     [required by zarith]
09:06:19   ∗ install zarith    1.12
09:06:19 ===== ∗ 3 =====
09:06:19 
09:06:19 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
09:06:20 [zarith.1.12] downloaded from cache at https://opam.ocaml.org/cache
09:06:20 [ocamlfind.1.9.1] downloaded from cache at https://opam.ocaml.org/cache
09:06:20 
09:06:20 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
09:06:20 ∗ installed conf-gmp.3
09:06:24 ∗ installed ocamlfind.1.9.1
09:06:27 ∗ installed zarith.1.12
09:06:27 Done.
09:06:27 # Run eval $(opam env) to update the current shell environment
09:06:27 + bin/isabelle ghc_setup
09:06:27 Writing implicit global project config file to: /media/data/jenkins/.stack/global-project/stack.yaml
09:06:27 Note: You can change the snapshot via the resolver field there.
09:06:27 Using resolver: lts-16.31 specified on command line
09:06:28 Preparing to install GHC (tinfo6) to an isolated location.
09:06:28 This will not interfere with any system-level installation.
09:06:28 Preparing to download ghc-tinfo6-8.8.4 ...
09:06:28 ghc-tinfo6-8.8.4: download has begun
09:06:29 ghc-tinfo6-8.8.4:   39.09 MiB / 198.61 MiB ( 19.68%) downloaded...
09:06:30 ghc-tinfo6-8.8.4:   81.61 MiB / 198.61 MiB ( 41.09%) downloaded...
09:06:31 ghc-tinfo6-8.8.4:  125.54 MiB / 198.61 MiB ( 63.21%) downloaded...
09:06:32 ghc-tinfo6-8.8.4:  169.06 MiB / 198.61 MiB ( 85.12%) downloaded...
09:06:33 ghc-tinfo6-8.8.4:  198.61 MiB / 198.61 MiB (100.00%) downloaded...
09:06:33 Downloaded ghc-tinfo6-8.8.4.
09:06:33 Unpacking GHC into /media/data/jenkins/.stack/programs/x86_64-linux/ghc-tinfo6-8.8.4.temp/ ...
09:06:53 Configuring GHC ...
09:06:57 Installing GHC ...
09:07:25 Installed GHC.
09:07:27 stack will use a sandboxed GHC it installed
09:07:27 For more information on paths, see 'stack path' and 'stack exec env'
09:07:27 To use this GHC and packages outside of a project, consider using:
09:07:27 stack ghc, stack ghci, stack runghc, or stack exec
09:07:27 The Glorious Glasgow Haskell Compilation System, version 8.8.4
09:07:28 + bin/isabelle ci_build_slow
09:07:31 
09:07:31 === CONFIGURATION ===
09:07:31 
09:07:31 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
09:07:31 ISABELLE_BUILD_OPTIONS=""
09:07:31 
09:07:31 ML_PLATFORM="x86_64-linux"
09:07:31 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-f86ae3dc1686/x86_64-linux"
09:07:31 ML_SYSTEM="polyml-5.8.2"
09:07:31 ML_OPTIONS="-H 4000 --maxheap 20G"
09:07:31 jobs = 1, threads = 8, numa = false
09:07:31 
09:07:31 === BUILD ===
09:07:31 
09:07:31 Build started at Wed, 31 Mar 2021 07:07:31 GMT
09:07:31 Isabelle id e52a9b208481
09:07:32 Build for AFP id 34dff8ee061c
09:07:32 
09:07:32 === LOG ===
09:07:32 
09:07:33 Session Pure/Pure
09:07:34 Session FOL/FOL
09:07:34 Session Tools/Tools
09:07:34 Session HOL/HOL (main)
09:07:35 Session AFP/AWN (AFP)
09:07:35 Session AFP/AODV (AFP slow)
09:07:36 Session HOL/HOL-Cardinals (timing)
09:07:36 Session HOL/HOL-Library (main timing)
09:07:36 Session AFP/Binomial-Heaps (AFP)
09:07:36 Session AFP/ConcurrentIMP (AFP)
09:07:36 Session AFP/ConcurrentGC (AFP slow)
09:07:37 Session AFP/FinFun (AFP)
09:07:37 Session AFP/Finger-Trees (AFP)
09:07:37 Session HOL/HOL-Combinatorics (main timing)
09:07:37 Session HOL/HOL-Computational_Algebra (main timing)
09:07:37 Session HOL/HOL-Algebra (main timing)
09:07:38 Session HOL/HOL-Analysis (main timing)
09:07:39 Session AFP/Coinductive (AFP)
09:07:39 Session HOL/HOL-Eisbach
09:07:39 Session HOL/HOL-Number_Theory (main timing)
09:07:39 Session HOL/HOL-ex (timing)
09:07:40 Session AFP/Automatic_Refinement (AFP)
09:07:40 Session AFP/Refine_Monadic (AFP)
09:07:40 Session HOL/HOL-Imperative_HOL (timing)
09:07:41 Session AFP/HereditarilyFinite (AFP)
09:07:41 Session AFP/Category3 (AFP)
09:07:41 Session AFP/MonoidalCategory (AFP)
09:07:41 Session AFP/Bicategory (AFP slow)
09:07:42 Session AFP/Trie (AFP)
09:07:42 Session AFP/Flyspeck-Tame (AFP)
09:07:42 Session AFP/Flyspeck-Tame-Computation (AFP slow very_slow)
09:07:42 Session AFP/Word_Lib (AFP)
09:07:43 Session AFP/IP_Addresses (AFP)
09:07:43 Session AFP/Simple_Firewall (AFP)
09:07:43 Session AFP/Routing (AFP)
09:07:43 Session AFP/Native_Word (AFP)
09:07:43 Session AFP/Collections (AFP)
09:07:44 Session AFP/Iptables_Semantics (AFP)
09:07:44 Session AFP/Iptables_Semantics_Examples (AFP)
09:07:44 Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow)
09:07:44 Session AFP/JinjaThreads (AFP slow)
09:07:45 Building Pure ...
09:08:06 Pure: theory Pure
09:08:07 Pure: theory ML_Bootstrap
09:08:08 Pure: theory Pure.Sessions
09:08:10 Timing Pure (1 threads, 1.337s elapsed time, 1.381s cpu time, 0.067s GC time, factor 1.03)
09:08:10 Finished Pure (0:00:23 elapsed time, 0:00:23 cpu time, factor 0.99)
09:08:10 Building HOL ...
09:08:13 HOL: theory Tools.Code_Generator
09:08:19 HOL: theory HOL.HOL
09:08:25 HOL: theory HOL.Ctr_Sugar
09:08:25 HOL: theory HOL.Argo
09:08:25 HOL: theory HOL.Orderings
09:08:29 HOL: theory HOL.Groups
09:08:29 HOL: theory HOL.SAT
09:08:31 HOL: theory HOL.Lattices
09:08:34 HOL: theory HOL.Set
09:08:36 HOL: theory HOL.Fun
09:08:36 HOL: theory HOL.Typedef
09:08:37 HOL: theory HOL.Complete_Lattices
09:08:37 HOL: theory HOL.Rings
09:08:39 HOL: theory HOL.Inductive
09:08:43 HOL: theory HOL.Product_Type
09:08:43 HOL: theory HOL.Sum_Type
09:08:44 HOL: theory HOL.Complete_Partial_Order
09:08:49 HOL: theory HOL.Nat
09:08:51 HOL: theory HOL.Fields
09:08:51 HOL: theory HOL.Meson
09:08:52 HOL: theory HOL.ATP
09:08:57 HOL: theory HOL.Metis
09:08:58 HOL: theory HOL.Finite_Set
09:09:01 HOL: theory HOL.Relation
09:09:02 HOL: theory HOL.Transitive_Closure
09:09:03 HOL: theory HOL.Wellfounded
09:09:04 HOL: theory HOL.Fun_Def_Base
09:09:04 HOL: theory HOL.Hilbert_Choice
09:09:04 HOL: theory HOL.Wfrec
09:09:04 HOL: theory HOL.Order_Relation
09:09:05 HOL: theory HOL.BNF_Wellorder_Relation
09:09:07 HOL: theory HOL.BNF_Wellorder_Embedding
09:09:07 HOL: theory HOL.Zorn
09:09:08 HOL: theory HOL.BNF_Wellorder_Constructions
09:09:09 HOL: theory HOL.BNF_Cardinal_Order_Relation
09:09:09 HOL: theory HOL.BNF_Cardinal_Arithmetic
09:09:09 HOL: theory HOL.BNF_Def
09:09:14 HOL: theory HOL.BNF_Composition
09:09:14 HOL: theory HOL.Basic_BNFs
09:09:15 HOL: theory HOL.BNF_Fixpoint_Base
09:09:22 HOL: theory HOL.BNF_Least_Fixpoint
09:09:27 HOL: theory HOL.Basic_BNF_LFPs
09:09:27 HOL: theory HOL.Transfer
09:09:28 HOL: theory HOL.Num
09:09:31 HOL: theory HOL.Power
09:09:34 HOL: theory HOL.Groups_Big
09:09:37 HOL: theory HOL.Equiv_Relations
09:09:38 HOL: theory HOL.Lifting
09:09:40 HOL: theory HOL.Lifting_Set
09:09:40 HOL: theory HOL.Quotient
09:09:40 HOL: theory HOL.Option
09:09:40 HOL: theory HOL.Extraction
09:09:40 HOL: theory HOL.Lattices_Big
09:09:40 HOL: theory HOL.Partial_Function
09:09:42 HOL: theory HOL.Fun_Def
09:09:46 HOL: theory HOL.Int
09:09:49 HOL: theory HOL.Euclidean_Division
09:09:58 HOL: theory HOL.Parity
09:10:06 HOL: theory HOL.Divides
09:10:09 HOL: theory HOL.Code_Numeral
09:10:09 HOL: theory HOL.Numeral_Simprocs
09:10:09 HOL: theory HOL.Set_Interval
09:10:10 HOL: theory HOL.Semiring_Normalization
09:10:10 HOL: theory HOL.SMT
09:10:13 HOL: theory HOL.Groebner_Basis
09:10:16 HOL: theory HOL.Conditionally_Complete_Lattices
09:10:16 HOL: theory HOL.Filter
09:10:16 HOL: theory HOL.Presburger
09:10:21 HOL: theory HOL.Sledgehammer
09:10:25 HOL: theory HOL.List
09:10:35 HOL: theory HOL.Groups_List
09:10:35 HOL: theory HOL.Map
09:10:37 HOL: theory HOL.Factorial
09:10:37 HOL: theory HOL.GCD
09:10:37 HOL: theory HOL.Enum
09:10:37 HOL: theory HOL.Random
09:10:38 HOL: theory HOL.Binomial
09:10:42 HOL: theory HOL.String
09:10:44 HOL: theory HOL.BNF_Greatest_Fixpoint
09:10:44 HOL: theory HOL.Predicate
09:10:44 HOL: theory HOL.Typerep
09:10:45 HOL: theory HOL.Lazy_Sequence
09:10:46 HOL: theory HOL.Limited_Sequence
09:10:46 HOL: theory HOL.Code_Evaluation
09:10:48 HOL: theory HOL.Quickcheck_Random
09:10:53 HOL: theory HOL.Quickcheck_Exhaustive
09:10:53 HOL: theory HOL.Quickcheck_Narrowing
09:10:53 HOL: theory HOL.Random_Pred
09:10:53 HOL: theory HOL.Random_Sequence
09:10:59 HOL: theory HOL.Record
09:10:59 HOL: theory HOL.Predicate_Compile
09:11:01 HOL: theory HOL.Nitpick
09:11:08 HOL: theory HOL.Nunchaku
09:11:10 HOL: theory Main
09:11:10 HOL: theory HOL.Archimedean_Field
09:11:10 HOL: theory HOL.Hull
09:11:10 HOL: theory HOL.Topological_Spaces
09:11:10 HOL: theory HOL.Modules
09:11:11 HOL: theory HOL.Vector_Spaces
09:11:18 HOL: theory HOL.Rat
09:11:21 HOL: theory HOL.Real
09:11:23 HOL: theory HOL.Real_Vector_Spaces
09:11:40 HOL: theory HOL.Inequalities
09:11:40 HOL: theory HOL.Limits
09:11:49 HOL: theory HOL.Deriv
09:11:49 HOL: theory HOL.Series
09:11:51 HOL: theory HOL.NthRoot
09:11:52 HOL: theory HOL.Transcendental
09:11:58 HOL: theory HOL.Complex
09:11:58 HOL: theory HOL.MacLaurin
09:11:59 HOL: theory Complex_Main
09:13:08 Preparing HOL/document ...
09:14:34 Finished HOL/document (0:01:25 elapsed time)
09:14:34 Preparing HOL/outline ...
09:15:21 Finished HOL/outline (0:00:47 elapsed time)
09:15:26 Timing HOL (8 threads, 236.130s elapsed time, 763.148s cpu time, 59.370s GC time, factor 3.23)
09:15:26 Finished HOL (0:04:45 elapsed time, 0:14:24 cpu time, factor 3.02)
09:15:26 Running JinjaThreads ...
09:15:28 JinjaThreads: theory HOL-Eisbach.Eisbach
09:15:28 JinjaThreads: theory Automatic_Refinement.Foldi
09:15:28 JinjaThreads: theory Automatic_Refinement.Prio_List
09:15:28 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1
09:15:28 JinjaThreads: theory Collections.ICF_Tools
09:15:28 JinjaThreads: theory Finger-Trees.FingerTree
09:15:28 JinjaThreads: theory HOL-Library.Adhoc_Overloading
09:15:28 JinjaThreads: theory HOL-Library.AList
09:15:28 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot
09:15:28 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot
09:15:28 JinjaThreads: theory HOL-Library.Monad_Syntax
09:15:28 JinjaThreads: theory Collections.Ord_Code_Preproc
09:15:28 JinjaThreads: theory HOL-Library.Boolean_Algebra
09:15:28 JinjaThreads: theory HOL-Library.Cancellation
09:15:28 JinjaThreads: theory HOL-Library.Case_Converter
09:15:28 JinjaThreads: theory Collections.Locale_Code
09:15:29 JinjaThreads: theory Automatic_Refinement.Refine_Util
09:15:29 JinjaThreads: theory Collections.Record_Intf
09:15:29 JinjaThreads: theory HOL-Library.Bit_Operations
09:15:29 JinjaThreads: theory HOL-Library.Code_Abstract_Nat
09:15:29 JinjaThreads: theory HOL-Library.Simps_Case_Conv
09:15:29 JinjaThreads: theory HOL-Library.Code_Target_Nat
09:15:29 JinjaThreads: theory HOL-Library.Code_Target_Int
09:15:30 JinjaThreads: theory HOL-Library.Confluence
09:15:30 JinjaThreads: theory HOL-Library.Code_Target_Numeral
09:15:30 JinjaThreads: theory HOL-Library.Infinite_Set
09:15:30 JinjaThreads: theory HOL-Library.Multiset
09:15:30 JinjaThreads: theory HOL-Library.Confluent_Quotient
09:15:30 JinjaThreads: theory Automatic_Refinement.Anti_Unification
09:15:30 JinjaThreads: theory Automatic_Refinement.Attr_Comb
09:15:30 JinjaThreads: theory Automatic_Refinement.Autoref_Data
09:15:30 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms
09:15:30 JinjaThreads: theory Automatic_Refinement.Indep_Vars
09:15:30 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp
09:15:30 JinjaThreads: theory Automatic_Refinement.Tagged_Solver
09:15:30 JinjaThreads: theory Automatic_Refinement.Select_Solve
09:15:30 JinjaThreads: theory HOL-Library.Dlist
09:15:31 JinjaThreads: theory HOL-Library.Lattice_Syntax
09:15:31 JinjaThreads: theory HOL-Library.Nat_Bijection
09:15:31 JinjaThreads: theory HOL-Library.Old_Datatype
09:15:31 JinjaThreads: theory HOL-Library.Complete_Partial_Order2
09:15:31 JinjaThreads: theory Trie.Trie
09:15:31 JinjaThreads: theory HOL-Library.Option_ord
09:15:31 JinjaThreads: theory HOL-Library.Phantom_Type
09:15:31 JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs
09:15:32 JinjaThreads: theory HOL-Library.RBT_Impl
09:15:32 JinjaThreads: theory HOL-Library.Signed_Division
09:15:32 JinjaThreads: theory HOL-Library.Sublist
09:15:32 JinjaThreads: theory HOL-Library.Cardinality
09:15:33 JinjaThreads: theory HOL-Library.Transitive_Closure_Table
09:15:33 JinjaThreads: theory HOL-Library.While_Combinator
09:15:33 JinjaThreads: theory FinFun.FinFun
09:15:33 JinjaThreads: theory HOL-Library.Numeral_Type
09:15:34 JinjaThreads: theory Collections.DatRef
09:15:34 JinjaThreads: theory HOL-Library.Countable
09:15:35 JinjaThreads: theory HOL-Library.Type_Length
09:15:35 JinjaThreads: theory JinjaThreads.Set_Monad
09:15:35 JinjaThreads: theory JinjaThreads.Set_without_equal
09:15:35 JinjaThreads: theory Refine_Monadic.Refine_Chapter
09:15:35 JinjaThreads: theory Binomial-Heaps.BinomialHeap
09:15:35 JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap
09:15:35 JinjaThreads: theory HOL-ex.Quicksort
09:15:36 JinjaThreads: theory HOL-Library.Countable_Set
09:15:36 JinjaThreads: theory Automatic_Refinement.Misc
09:15:36 JinjaThreads: theory HOL-Library.Countable_Complete_Lattices
09:15:36 JinjaThreads: theory JinjaThreads.Auxiliary
09:15:36 JinjaThreads: theory HOL-Library.Word
09:15:38 JinjaThreads: theory Word_Lib.More_Arithmetic
09:15:39 JinjaThreads: theory HOL-Library.Order_Continuity
09:15:40 JinjaThreads: theory HOL-Library.Extended_Nat
09:15:40 JinjaThreads: theory Coinductive.Coinductive_Nat
09:15:41 JinjaThreads: theory Automatic_Refinement.Refine_Lib
09:15:41 JinjaThreads: theory Collections.SetIterator
09:15:41 JinjaThreads: theory Collections.Sorted_List_Operations
09:15:42 JinjaThreads: theory Coinductive.Coinductive_List
09:15:42 JinjaThreads: theory Automatic_Refinement.Autoref_Phases
09:15:42 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging
09:15:43 JinjaThreads: theory Automatic_Refinement.Relators
09:15:43 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover
09:15:43 JinjaThreads: theory Collections.SetIteratorOperations
09:15:44 JinjaThreads: theory Automatic_Refinement.Param_Tool
09:15:44 JinjaThreads: theory Automatic_Refinement.Param_HOL
09:15:46 JinjaThreads: theory Word_Lib.Bit_Comprehension
09:15:46 JinjaThreads: theory Word_Lib.More_Divides
09:15:46 JinjaThreads: theory Word_Lib.Signed_Words
09:15:46 JinjaThreads: theory Word_Lib.Signed_Division_Word
09:15:46 JinjaThreads: theory Word_Lib.More_Word
09:15:46 JinjaThreads: theory Automatic_Refinement.Parametricity
09:15:46 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops
09:15:46 JinjaThreads: theory Collections.Assoc_List
09:15:46 JinjaThreads: theory Collections.Dlist_add
09:15:46 JinjaThreads: theory Collections.Proper_Iterator
09:15:47 JinjaThreads: theory Collections.SetIteratorGA
09:15:47 JinjaThreads: theory Collections.Diff_Array
09:15:48 JinjaThreads: theory Collections.Trie_Impl
09:15:48 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel
09:15:48 JinjaThreads: theory Collections.It_to_It
09:15:48 JinjaThreads: theory Word_Lib.Traditional_Infix_Syntax
09:15:48 JinjaThreads: theory Collections.Trie2
09:15:48 JinjaThreads: theory Automatic_Refinement.Autoref_Translate
09:15:48 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface
09:15:48 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo
09:15:49 JinjaThreads: theory Automatic_Refinement.Autoref_Tool
09:15:49 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL
09:15:49 JinjaThreads: theory Word_Lib.Bits_Int
09:15:50 JinjaThreads: theory Coinductive.Lazy_LList
09:15:50 JinjaThreads: theory Coinductive.TLList
09:15:52 JinjaThreads: theory Native_Word.More_Bits_Int
09:15:53 JinjaThreads: theory Word_Lib.Least_significant_bit
09:15:53 JinjaThreads: theory Word_Lib.Most_significant_bit
09:15:53 JinjaThreads: theory Word_Lib.Generic_set_bit
09:15:53 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement
09:15:53 JinjaThreads: theory Collections.Idx_Iterator
09:15:54 JinjaThreads: theory Coinductive.Lazy_TLList
09:15:54 JinjaThreads: theory Refine_Monadic.Refine_Misc
09:15:54 JinjaThreads: theory Native_Word.Code_Symbolic_Bits_Int
09:15:55 JinjaThreads: theory Refine_Monadic.RefineG_Domain
09:15:55 JinjaThreads: theory Refine_Monadic.RefineG_Transfer
09:15:56 JinjaThreads: theory Native_Word.Bits_Integer
09:15:56 JinjaThreads: theory Refine_Monadic.RefineG_Assert
09:15:56 JinjaThreads: theory Refine_Monadic.RefineG_Recursion
09:15:57 JinjaThreads: theory Refine_Monadic.RefineG_While
09:15:57 JinjaThreads: theory Refine_Monadic.Refine_Basic
09:15:59 JinjaThreads: theory Refine_Monadic.Refine_Det
09:16:04 JinjaThreads: theory Refine_Monadic.Refine_Heuristics
09:16:04 JinjaThreads: theory Refine_Monadic.Refine_Leof
09:16:04 JinjaThreads: theory Refine_Monadic.Refine_Pfun
09:16:04 JinjaThreads: theory Refine_Monadic.Refine_More_Comb
09:16:04 JinjaThreads: theory Refine_Monadic.Refine_While
09:16:06 JinjaThreads: theory Refine_Monadic.Refine_Transfer
09:16:07 JinjaThreads: theory Refine_Monadic.Autoref_Monadic
09:16:07 JinjaThreads: theory Refine_Monadic.Refine_Automation
09:16:07 JinjaThreads: theory Refine_Monadic.Refine_Foreach
09:16:10 JinjaThreads: theory Refine_Monadic.Refine_Monadic
09:16:11 JinjaThreads: theory Collections.Gen_Iterator
09:16:11 JinjaThreads: theory Collections.Intf_Map
09:16:11 JinjaThreads: theory Collections.Intf_Set
09:16:12 JinjaThreads: theory Collections.Iterator
09:16:12 JinjaThreads: theory Native_Word.Code_Target_Bits_Int
09:16:12 JinjaThreads: theory Native_Word.Code_Target_Word_Base
09:16:13 JinjaThreads: theory Collections.Code_Target_ICF
09:16:13 JinjaThreads: theory Collections.Array_Iterator
09:16:13 JinjaThreads: theory Collections.ICF_Spec_Base
09:16:13 JinjaThreads: theory Native_Word.Uint32
09:16:13 JinjaThreads: theory Collections.AnnotatedListSpec
09:16:13 JinjaThreads: theory Collections.ListSpec
09:16:13 JinjaThreads: theory Collections.MapSpec
09:16:13 JinjaThreads: theory Collections.PrioSpec
09:16:13 JinjaThreads: theory Collections.PrioUniqueSpec
09:16:13 JinjaThreads: theory Collections.SetSpec
09:16:15 JinjaThreads: theory Collections.BinoPrioImpl
09:16:15 JinjaThreads: theory Collections.SkewPrioImpl
09:16:15 JinjaThreads: theory Collections.HashCode
09:16:15 JinjaThreads: theory Collections.ListGA
09:16:16 JinjaThreads: theory Collections.FTAnnotatedListImpl
09:16:16 JinjaThreads: theory Collections.PrioByAnnotatedList
09:16:16 JinjaThreads: theory Collections.Fifo
09:16:19 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList
09:16:19 JinjaThreads: theory Collections.Algos
09:16:19 JinjaThreads: theory Collections.SetIndex
09:16:20 JinjaThreads: theory Collections.SetIteratorCollectionsGA
09:16:21 JinjaThreads: theory Collections.MapGA
09:16:21 JinjaThreads: theory Collections.SetGA
09:16:22 JinjaThreads: theory Collections.FTPrioImpl
09:16:23 JinjaThreads: theory Collections.FTPrioUniqueImpl
09:16:24 JinjaThreads: theory Collections.ArrayMapImpl
09:16:24 JinjaThreads: theory Collections.ListMapImpl
09:16:24 JinjaThreads: theory Collections.ListMapImpl_Invar
09:16:24 JinjaThreads: theory Collections.TrieMapImpl
09:16:26 JinjaThreads: theory Collections.ListSetImpl
09:16:28 JinjaThreads: theory Collections.ListSetImpl_Invar
09:16:28 JinjaThreads: theory Collections.ListSetImpl_NotDist
09:16:30 JinjaThreads: theory Collections.ListSetImpl_Sorted
09:16:31 JinjaThreads: theory Collections.SetByMap
09:16:32 JinjaThreads: theory Collections.ArrayHashMap_Impl
09:16:34 JinjaThreads: theory Collections.ArraySetImpl
09:16:34 JinjaThreads: theory Collections.TrieSetImpl
09:16:36 JinjaThreads: theory HOL-Library.RBT
09:16:36 JinjaThreads: theory Collections.RBT_add
09:16:36 JinjaThreads: theory Collections.ArrayHashMap
09:16:39 JinjaThreads: theory Collections.RBTMapImpl
09:16:43 JinjaThreads: theory Collections.ArrayHashSet
09:16:46 JinjaThreads: theory Collections.RBTSetImpl
09:16:46 JinjaThreads: theory Collections.HashMap_Impl
09:16:48 JinjaThreads: theory Collections.HashMap
09:16:54 JinjaThreads: theory Collections.HashSet
09:16:54 JinjaThreads: theory Collections.MapStdImpl
09:17:00 JinjaThreads: theory Collections.SetStdImpl
09:17:04 JinjaThreads: theory Collections.ICF_Impl
09:17:09 JinjaThreads: theory Collections.ICF_Refine_Monadic
09:17:10 JinjaThreads: theory Collections.ICF_Autoref
09:17:14 JinjaThreads: theory Collections.Collections
09:17:14 JinjaThreads: theory Collections.CollectionsV1
09:17:20 JinjaThreads: theory JinjaThreads.JT_ICF
09:17:20 JinjaThreads: theory JinjaThreads.Basic_Main
09:18:23 JinjaThreads: theory HOL-Library.Prefix_Order
09:18:23 JinjaThreads: theory JinjaThreads.FWState
09:18:23 JinjaThreads: theory JinjaThreads.LTS
09:18:23 JinjaThreads: theory JinjaThreads.Type
09:18:23 JinjaThreads: theory JinjaThreads.ListIndex
09:18:23 JinjaThreads: theory JinjaThreads.Orders
09:18:23 JinjaThreads: theory JinjaThreads.Semilat
09:18:23 JinjaThreads: theory HOL-Library.Mapping
09:18:23 JinjaThreads: theory JinjaThreads.Err
09:18:25 JinjaThreads: theory HOL-Library.AList_Mapping
09:18:25 JinjaThreads: theory JinjaThreads.Listn
09:18:25 JinjaThreads: theory JinjaThreads.Opt
09:18:25 JinjaThreads: theory JinjaThreads.Product
09:18:25 JinjaThreads: theory JinjaThreads.Semilattices
09:18:26 JinjaThreads: theory JinjaThreads.Typing_Framework
09:18:26 JinjaThreads: theory JinjaThreads.Decl
09:18:26 JinjaThreads: theory JinjaThreads.SemilatAlg
09:18:26 JinjaThreads: theory JinjaThreads.Kildall
09:18:26 JinjaThreads: theory JinjaThreads.LBVSpec
09:18:27 JinjaThreads: theory JinjaThreads.Bisimulation
09:18:27 JinjaThreads: theory JinjaThreads.Typing_Framework_err
09:18:27 JinjaThreads: theory JinjaThreads.LBVComplete
09:18:27 JinjaThreads: theory JinjaThreads.LBVCorrect
09:18:28 JinjaThreads: theory JinjaThreads.Abstract_BV
09:18:28 JinjaThreads: theory JinjaThreads.TypeRel
09:18:33 JinjaThreads: theory JinjaThreads.TypeRelRefine
09:18:33 JinjaThreads: theory JinjaThreads.Value
09:18:37 JinjaThreads: theory JinjaThreads.Exceptions
09:18:37 JinjaThreads: theory JinjaThreads.Heap
09:18:38 JinjaThreads: theory JinjaThreads.SystemClasses
09:18:40 JinjaThreads: theory JinjaThreads.MM
09:18:40 JinjaThreads: theory JinjaThreads.State
09:18:47 JinjaThreads: theory JinjaThreads.FWCondAction
09:18:47 JinjaThreads: theory JinjaThreads.FWInterrupt
09:18:47 JinjaThreads: theory JinjaThreads.FWLock
09:18:47 JinjaThreads: theory JinjaThreads.FWThread
09:18:47 JinjaThreads: theory JinjaThreads.FWWait
09:18:47 JinjaThreads: theory JinjaThreads.Observable_Events
09:18:50 JinjaThreads: theory JinjaThreads.FWLocking
09:18:51 JinjaThreads: theory JinjaThreads.FWLockingThread
09:18:51 JinjaThreads: theory JinjaThreads.FWWellform
09:18:53 JinjaThreads: theory JinjaThreads.FWLifting
09:18:53 JinjaThreads: theory JinjaThreads.FWSemantics
09:18:59 JinjaThreads: theory JinjaThreads.JVMState
09:18:59 JinjaThreads: theory JinjaThreads.StartConfig
09:18:59 JinjaThreads: theory JinjaThreads.JMM_Spec
09:19:00 JinjaThreads: theory JinjaThreads.FWLiftingSem
09:19:00 JinjaThreads: theory JinjaThreads.FWProgressAux
09:19:01 JinjaThreads: theory JinjaThreads.Conform
09:19:01 JinjaThreads: theory JinjaThreads.State_Refinement
09:19:02 JinjaThreads: theory JinjaThreads.FWDeadlock
09:19:03 JinjaThreads: theory JinjaThreads.FWLTS
09:19:03 JinjaThreads: theory JinjaThreads.ConformThreaded
09:19:04 JinjaThreads: theory JinjaThreads.ExternalCall
09:19:04 JinjaThreads: theory JinjaThreads.SC
09:19:04 JinjaThreads: theory JinjaThreads.FWProgress
09:19:04 JinjaThreads: theory JinjaThreads.SC_Collections
09:19:13 JinjaThreads: theory JinjaThreads.JMM_DRF
09:19:13 JinjaThreads: theory JinjaThreads.SC_Legal
09:19:16 JinjaThreads: theory JinjaThreads.FWBisimulation
09:19:16 JinjaThreads: theory JinjaThreads.FWInitFinLift
09:19:17 JinjaThreads: theory JinjaThreads.Non_Speculative
09:19:17 JinjaThreads: theory JinjaThreads.Scheduler
09:19:19 JinjaThreads: theory JinjaThreads.HB_Completion
09:19:20 JinjaThreads: theory JinjaThreads.SC_Completion
09:19:32 JinjaThreads: theory JinjaThreads.WellForm
09:19:32 JinjaThreads: theory JinjaThreads.ExternalCall_Execute
09:19:34 JinjaThreads: theory JinjaThreads.ExternalCallWF
09:19:34 JinjaThreads: theory JinjaThreads.JMM_Heap
09:19:34 JinjaThreads: theory JinjaThreads.SemiType
09:19:34 JinjaThreads: theory JinjaThreads.BinOp
09:19:37 JinjaThreads: theory JinjaThreads.JVM_SemiType
09:19:39 JinjaThreads: theory JinjaThreads.JMM_Type
09:19:39 JinjaThreads: theory JinjaThreads.JMM_Type2
09:19:48 JinjaThreads: theory JinjaThreads.Random_Scheduler
09:19:48 JinjaThreads: theory JinjaThreads.Round_Robin
09:19:50 JinjaThreads: theory JinjaThreads.JMM_Framework
09:19:57 JinjaThreads: theory JinjaThreads.SC_Schedulers
09:19:59 JinjaThreads: theory JinjaThreads.Expr
09:20:00 JinjaThreads: theory JinjaThreads.JVMInstructions
09:20:00 JinjaThreads: theory JinjaThreads.PCompiler
09:20:01 JinjaThreads: theory JinjaThreads.PCompilerRefine
09:20:09 JinjaThreads: theory JinjaThreads.JVMExceptions
09:20:09 JinjaThreads: theory JinjaThreads.JVMHeap
09:20:09 JinjaThreads: theory JinjaThreads.Effect
09:20:15 JinjaThreads: theory JinjaThreads.JVMExecInstr
09:20:17 JinjaThreads: theory JinjaThreads.CallExpr
09:20:24 JinjaThreads: theory JinjaThreads.DefAss
09:20:27 JinjaThreads: theory JinjaThreads.JHeap
09:20:27 JinjaThreads: theory JinjaThreads.WWellForm
09:20:27 JinjaThreads: theory JinjaThreads.WellType
09:20:33 JinjaThreads: theory JinjaThreads.JVMExec
09:20:35 JinjaThreads: theory JinjaThreads.J1State
09:20:36 JinjaThreads: theory JinjaThreads.JVMDefensive
09:20:36 JinjaThreads: theory JinjaThreads.SmallStep
09:20:36 JinjaThreads: theory JinjaThreads.Annotate
09:20:38 JinjaThreads: theory JinjaThreads.J1Heap
09:20:41 JinjaThreads: theory JinjaThreads.J1WellType
09:20:42 JinjaThreads: theory JinjaThreads.JWellForm
09:20:42 JinjaThreads: theory JinjaThreads.WellTypeRT
09:20:43 JinjaThreads: theory JinjaThreads.JVMThreaded
09:20:45 JinjaThreads: theory JinjaThreads.J1WellForm
09:20:46 JinjaThreads: theory JinjaThreads.JVMExec_Execute
09:20:46 JinjaThreads: theory JinjaThreads.JMM_Typesafe
09:20:52 JinjaThreads: theory JinjaThreads.Compiler1
09:21:05 JinjaThreads: theory JinjaThreads.JJ1WellForm
09:21:05 JinjaThreads: theory JinjaThreads.Compiler2
09:21:06 JinjaThreads: theory JinjaThreads.Preprocessor
09:21:07 JinjaThreads: theory JinjaThreads.ToString
09:21:09 JinjaThreads: theory JinjaThreads.JMM_JVM
09:21:09 JinjaThreads: theory JinjaThreads.JVM_Main
09:21:12 JinjaThreads: theory JinjaThreads.JMM_Common
09:21:15 JinjaThreads: theory JinjaThreads.Compiler
09:21:15 JinjaThreads: theory JinjaThreads.Exception_Tables
09:21:16 JinjaThreads: theory JinjaThreads.BVSpec
09:21:16 JinjaThreads: theory JinjaThreads.EffectMono
09:21:17 JinjaThreads: theory JinjaThreads.TF_JVM
09:21:17 JinjaThreads: theory JinjaThreads.BVConform
09:21:17 JinjaThreads: theory JinjaThreads.TypeComp
09:21:19 JinjaThreads: theory JinjaThreads.JMM_Typesafe2
09:21:21 JinjaThreads: theory JinjaThreads.BVExec
09:21:21 JinjaThreads: theory JinjaThreads.LBVJVM
09:21:26 JinjaThreads: theory JinjaThreads.BVSpecTypeSafe
09:21:26 JinjaThreads: theory JinjaThreads.FWBisimDeadlock
09:21:26 JinjaThreads: theory JinjaThreads.FWBisimLift
09:21:27 JinjaThreads: theory JinjaThreads.J1
09:21:36 JinjaThreads: theory JinjaThreads.BVNoTypeError
09:21:40 JinjaThreads: theory JinjaThreads.BCVExec
09:21:41 JinjaThreads: theory JinjaThreads.JVMExec_Execute2
09:21:42 JinjaThreads: theory JinjaThreads.BVProgressThreaded
09:21:42 JinjaThreads: theory JinjaThreads.JVMTau
09:21:56 JinjaThreads: theory JinjaThreads.Common_Main
09:22:09 JinjaThreads: theory JinjaThreads.J1Deadlock
09:22:16 JinjaThreads: theory JinjaThreads.Execs
09:22:38 JinjaThreads: theory JinjaThreads.DefAssPreservation
09:22:38 JinjaThreads: theory JinjaThreads.Threaded
09:22:38 JinjaThreads: theory JinjaThreads.Progress
09:22:46 JinjaThreads: theory JinjaThreads.TypeSafe
09:23:17 JinjaThreads: theory JinjaThreads.J0
09:23:18 JinjaThreads: theory JinjaThreads.JMM_J
09:23:22 JinjaThreads: theory JinjaThreads.ProgressThreaded
09:23:25 JinjaThreads: theory JinjaThreads.J_Execute
09:23:47 JinjaThreads: theory JinjaThreads.J1JVMBisim
09:24:15 JinjaThreads: theory JinjaThreads.JVMDeadlocked
09:24:15 JinjaThreads: theory JinjaThreads.DRF_JVM
09:24:15 JinjaThreads: theory JinjaThreads.Deadlocked
09:24:16 JinjaThreads: theory JinjaThreads.DRF_J
09:24:16 JinjaThreads: theory JinjaThreads.JVM_Execute
09:28:38 JinjaThreads: theory JinjaThreads.JVM_Execute2
09:28:38 JinjaThreads: theory JinjaThreads.J_Main
09:28:38 JinjaThreads: theory JinjaThreads.J0Bisim
09:28:39 JinjaThreads: theory JinjaThreads.J0J1Bisim
09:29:00 JinjaThreads: theory JinjaThreads.BV_Main
09:29:16 JinjaThreads: theory JinjaThreads.Correctness1
09:29:19 JinjaThreads: theory JinjaThreads.Correctness1Threaded
09:29:23 JinjaThreads: theory JinjaThreads.Code_Generation
09:29:32 JinjaThreads: theory JinjaThreads.ApprenticeChallenge
09:29:33 JinjaThreads: theory JinjaThreads.BufferExample
09:29:37 JinjaThreads: theory JinjaThreads.Java2Jinja
09:29:46 JinjaThreads: theory JinjaThreads.Examples_Main
09:31:27 JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe
09:31:37 JinjaThreads: theory JinjaThreads.JMM_J_Typesafe
09:32:06 JinjaThreads: theory JinjaThreads.J1JVM
09:32:13 JinjaThreads: theory JinjaThreads.JVMJ1
09:32:16 JinjaThreads: theory JinjaThreads.Execute_Main
09:33:53 JinjaThreads: theory JinjaThreads.Correctness2
09:42:33 JinjaThreads: theory JinjaThreads.Correctness
09:47:53 JinjaThreads: theory JinjaThreads.JMM_Compiler
09:47:53 JinjaThreads: theory JinjaThreads.SC_Interp
09:47:54 JinjaThreads: theory JinjaThreads.Compiler_Main
09:51:26 JinjaThreads: theory JinjaThreads.JMM_Interp
09:51:30 JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2
09:51:32 JinjaThreads: theory JinjaThreads.JMM
09:51:35 JinjaThreads: theory JinjaThreads.MM_Main
09:51:41 JinjaThreads: theory JinjaThreads.JinjaThreads
10:02:05 Preparing JinjaThreads/document ...
10:03:21 Finished JinjaThreads/document (0:01:15 elapsed time)
10:03:21 Preparing JinjaThreads/outline ...
10:03:55 Finished JinjaThreads/outline (0:00:33 elapsed time)
10:03:56 Timing JinjaThreads (8 threads, 2778.809s elapsed time, 13069.488s cpu time, 5756.245s GC time, factor 4.70)
10:03:56 Finished JinjaThreads (0:46:24 elapsed time, 3:38:10 cpu time, factor 4.70)
10:03:56 Building Flyspeck-Tame ...
10:03:58 Flyspeck-Tame: theory Flyspeck-Tame.ListAux
10:03:58 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl
10:03:58 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat
10:03:58 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order
10:03:58 Flyspeck-Tame: theory HOL-Library.AList
10:03:58 Flyspeck-Tame: theory HOL-Library.Code_Target_Int
10:03:58 Flyspeck-Tame: theory HOL-Library.IArray
10:03:58 Flyspeck-Tame: theory HOL-Library.While_Combinator
10:03:58 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat
10:03:58 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso
10:03:58 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral
10:03:58 Flyspeck-Tame: theory Flyspeck-Tame.Arch
10:03:59 Flyspeck-Tame: theory Flyspeck-Tame.Worklist
10:03:59 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax
10:03:59 Flyspeck-Tame: theory Flyspeck-Tame.ListSum
10:03:59 Flyspeck-Tame: theory Flyspeck-Tame.Rotation
10:03:59 Flyspeck-Tame: theory Flyspeck-Tame.Graph
10:03:59 Flyspeck-Tame: theory Flyspeck-Tame.Maps
10:04:00 Flyspeck-Tame: theory Trie.Trie
10:04:01 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision
10:04:02 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps
10:04:02 Flyspeck-Tame: theory Flyspeck-Tame.Tame
10:04:02 Flyspeck-Tame: theory Trie.Tries
10:04:02 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator
10:04:03 Flyspeck-Tame: theory Flyspeck-Tame.TameProps
10:04:03 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps
10:04:03 Flyspeck-Tame: theory Flyspeck-Tame.Plane
10:04:03 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps
10:04:03 Flyspeck-Tame: theory Flyspeck-Tame.Plane1
10:04:04 Flyspeck-Tame: theory Flyspeck-Tame.Generator
10:04:04 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum
10:04:08 Flyspeck-Tame: theory Flyspeck-Tame.Invariants
10:04:08 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux
10:04:09 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps
10:04:09 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps
10:04:09 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props
10:04:10 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound
10:04:10 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps
10:04:10 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps
10:04:10 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps
10:04:11 Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness
10:05:31 Preparing Flyspeck-Tame/document ...
10:05:44 Finished Flyspeck-Tame/document (0:00:12 elapsed time)
10:05:44 Preparing Flyspeck-Tame/outline ...
10:05:50 Finished Flyspeck-Tame/outline (0:00:06 elapsed time)
10:05:52 Timing Flyspeck-Tame (8 threads, 57.995s elapsed time, 318.130s cpu time, 25.617s GC time, factor 5.49)
10:05:52 Finished Flyspeck-Tame (0:01:33 elapsed time, 0:06:32 cpu time, factor 4.18)
10:05:52 Running Flyspeck-Tame-Computation ...
10:05:53 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.ArchComp
10:05:54 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.Completeness
14:25:55 Timing Flyspeck-Tame-Computation (8 threads, 15598.137s elapsed time, 23411.770s cpu time, 856.221s GC time, factor 1.50)
14:25:55 Finished Flyspeck-Tame-Computation (4:20:00 elapsed time, 6:30:13 cpu time, factor 1.50)
14:25:55 Building AWN ...
14:25:57 AWN: theory AWN.TransitionSystems
14:25:57 AWN: theory AWN.Lib
14:25:57 AWN: theory AWN.AWN
14:25:58 AWN: theory AWN.Invariants
14:25:58 AWN: theory AWN.OInvariants
14:26:08 AWN: theory AWN.AWN_Cterms
14:26:08 AWN: theory AWN.AWN_SOS
14:26:09 AWN: theory AWN.OAWN_SOS
14:26:11 AWN: theory AWN.AWN_Labels
14:26:12 AWN: theory AWN.Pnet
14:26:12 AWN: theory AWN.Inv_Cterms
14:26:12 AWN: theory AWN.AWN_Invariants
14:26:13 AWN: theory AWN.Closed
14:26:13 AWN: theory AWN.AWN_SOS_Labels
14:26:14 AWN: theory AWN.Qmsg
14:26:15 AWN: theory AWN.OAWN_SOS_Labels
14:26:15 AWN: theory AWN.OAWN_Invariants
14:26:15 AWN: theory AWN.ONode_Lifting
14:26:15 AWN: theory AWN.OPnet
14:26:15 AWN: theory AWN.OPnet_Lifting
14:26:16 AWN: theory AWN.OClosed_Lifting
14:26:16 AWN: theory AWN.OClosed_Transfer
14:26:16 AWN: theory AWN.OAWN_Convert
14:26:16 AWN: theory AWN.Qmsg_Lifting
14:26:17 AWN: theory AWN.AWN_Main
14:26:17 AWN: theory AWN.Toy
14:26:27 AWN: theory AWN.AWN_Term_Graph
14:26:57 Preparing AWN/document ...
14:27:05 Finished AWN/document (0:00:08 elapsed time)
14:27:05 Preparing AWN/outline ...
14:27:10 Finished AWN/outline (0:00:05 elapsed time)
14:27:11 Timing AWN (8 threads, 33.052s elapsed time, 157.974s cpu time, 6.837s GC time, factor 4.78)
14:27:11 Finished AWN (0:01:00 elapsed time, 0:03:33 cpu time, factor 3.54)
14:27:11 Running AODV ...
14:27:13 AODV: theory AODV.Aodv_Basic
14:27:14 AODV: theory AODV.A_Norreqid
14:27:14 AODV: theory AODV.Aodv_Data
14:27:14 AODV: theory AODV.Aodv_Message
14:27:14 AODV: theory AODV.B_Fwdrreps
14:27:14 AODV: theory AODV.C_Gtobcast
14:27:14 AODV: theory AODV.D_Fwdrreqs
14:27:14 AODV: theory AODV.E_All_ABCD
14:27:14 AODV: theory AODV.A_Aodv_Data
14:27:14 AODV: theory AODV.A_Aodv_Message
14:27:14 AODV: theory AODV.B_Aodv_Data
14:27:14 AODV: theory AODV.B_Aodv_Message
14:27:14 AODV: theory AODV.C_Aodv_Data
14:27:14 AODV: theory AODV.C_Aodv_Message
14:27:17 AODV: theory AODV.C_Fresher
14:27:17 AODV: theory AODV.Fresher
14:27:17 AODV: theory AODV.D_Aodv_Data
14:27:17 AODV: theory AODV.D_Aodv_Message
14:27:17 AODV: theory AODV.E_Aodv_Data
14:27:17 AODV: theory AODV.B_Fresher
14:27:17 AODV: theory AODV.E_Aodv_Message
14:27:17 AODV: theory AODV.A_Fresher
14:27:19 AODV: theory AODV.A_Aodv
14:27:19 AODV: theory AODV.Aodv
14:27:19 AODV: theory AODV.B_Aodv
14:27:19 AODV: theory AODV.C_Aodv
14:27:19 AODV: theory AODV.E_Fresher
14:27:19 AODV: theory AODV.D_Fresher
14:27:20 AODV: theory AODV.D_Aodv
14:27:20 AODV: theory AODV.E_Aodv
14:27:54 AODV: theory AODV.Aodv_Predicates
14:27:54 AODV: theory AODV.Loop_Freedom
14:27:54 AODV: theory AODV.Quality_Increases
14:27:55 AODV: theory AODV.Seq_Invariants
14:27:55 AODV: theory AODV.OAodv
14:27:56 AODV: theory AODV.Global_Invariants
14:27:56 AODV: theory AODV.Aodv_Loop_Freedom
14:28:01 AODV: theory AODV.A_Aodv_Predicates
14:28:01 AODV: theory AODV.A_OAodv
14:28:01 AODV: theory AODV.A_Loop_Freedom
14:28:01 AODV: theory AODV.A_Quality_Increases
14:28:01 AODV: theory AODV.A_Seq_Invariants
14:28:02 AODV: theory AODV.A_Global_Invariants
14:28:03 AODV: theory AODV.A_Aodv_Loop_Freedom
14:28:03 AODV: theory AODV.C_Aodv_Predicates
14:28:03 AODV: theory AODV.C_OAodv
14:28:03 AODV: theory AODV.C_Loop_Freedom
14:28:04 AODV: theory AODV.C_Quality_Increases
14:28:04 AODV: theory AODV.C_Seq_Invariants
14:28:04 AODV: theory AODV.C_Global_Invariants
14:28:05 AODV: theory AODV.C_Aodv_Loop_Freedom
14:28:07 AODV: theory AODV.B_Aodv_Predicates
14:28:07 AODV: theory AODV.B_OAodv
14:28:07 AODV: theory AODV.B_Loop_Freedom
14:28:07 AODV: theory AODV.B_Quality_Increases
14:28:07 AODV: theory AODV.B_Seq_Invariants
14:28:07 AODV: theory AODV.E_Aodv_Predicates
14:28:07 AODV: theory AODV.E_OAodv
14:28:07 AODV: theory AODV.E_Loop_Freedom
14:28:08 AODV: theory AODV.E_Quality_Increases
14:28:08 AODV: theory AODV.E_Seq_Invariants
14:28:08 AODV: theory AODV.B_Global_Invariants
14:28:08 AODV: theory AODV.E_Global_Invariants
14:28:09 AODV: theory AODV.B_Aodv_Loop_Freedom
14:28:09 AODV: theory AODV.E_Aodv_Loop_Freedom
14:28:14 AODV: theory AODV.D_Aodv_Predicates
14:28:14 AODV: theory AODV.D_Loop_Freedom
14:28:14 AODV: theory AODV.D_Quality_Increases
14:28:14 AODV: theory AODV.D_Seq_Invariants
14:28:14 AODV: theory AODV.D_OAodv
14:28:15 AODV: theory AODV.D_Global_Invariants
14:28:15 AODV: theory AODV.D_Aodv_Loop_Freedom
14:28:19 AODV: theory AODV.All
15:39:18 Preparing AODV/document ...
15:39:35 Finished AODV/document (0:00:16 elapsed time)
15:39:35 Preparing AODV/outline ...
15:39:45 Finished AODV/outline (0:00:10 elapsed time)
15:39:47 Timing AODV (8 threads, 4320.965s elapsed time, 25308.085s cpu time, 1053.415s GC time, factor 5.86)
15:39:47 Finished AODV (1:12:03 elapsed time, 7:01:51 cpu time, factor 5.85)
15:39:47 Building Word_Lib ...
15:39:49 Word_Lib: theory HOL-Eisbach.Eisbach
15:39:49 Word_Lib: theory HOL-Library.Boolean_Algebra
15:39:49 Word_Lib: theory HOL-Library.Phantom_Type
15:39:49 Word_Lib: theory HOL-Library.Sublist
15:39:49 Word_Lib: theory HOL-Library.Signed_Division
15:39:49 Word_Lib: theory Word_Lib.Enumeration
15:39:49 Word_Lib: theory Word_Lib.More_Misc
15:39:49 Word_Lib: theory Word_Lib.Even_More_List
15:39:49 Word_Lib: theory HOL-Library.Bit_Operations
15:39:50 Word_Lib: theory HOL-Library.Cardinality
15:39:50 Word_Lib: theory HOL-Eisbach.Eisbach_Tools
15:39:51 Word_Lib: theory Word_Lib.More_Sublist
15:39:51 Word_Lib: theory HOL-Library.Numeral_Type
15:39:52 Word_Lib: theory HOL-Library.Type_Length
15:39:55 Word_Lib: theory HOL-Library.Word
15:39:56 Word_Lib: theory Word_Lib.More_Arithmetic
15:40:03 Word_Lib: theory Word_Lib.Bit_Comprehension
15:40:03 Word_Lib: theory Word_Lib.Hex_Words
15:40:03 Word_Lib: theory Word_Lib.Legacy_Aliases
15:40:03 Word_Lib: theory Word_Lib.More_Divides
15:40:03 Word_Lib: theory Word_Lib.Signed_Words
15:40:03 Word_Lib: theory Word_Lib.Type_Syntax
15:40:03 Word_Lib: theory Word_Lib.Word_Syntax
15:40:03 Word_Lib: theory Word_Lib.Signed_Division_Word
15:40:03 Word_Lib: theory Word_Lib.Word_Names
15:40:03 Word_Lib: theory Word_Lib.More_Word
15:40:04 Word_Lib: theory Word_Lib.Enumeration_Word
15:40:04 Word_Lib: theory Word_Lib.Many_More
15:40:04 Word_Lib: theory Word_Lib.Strict_part_mono
15:40:04 Word_Lib: theory Word_Lib.Traditional_Infix_Syntax
15:40:04 Word_Lib: theory Word_Lib.Word_16
15:40:06 Word_Lib: theory Word_Lib.Bits_Int
15:40:06 Word_Lib: theory Word_Lib.Word_EqI
15:40:08 Word_Lib: theory Word_Lib.Least_significant_bit
15:40:08 Word_Lib: theory Word_Lib.Norm_Words
15:40:08 Word_Lib: theory Word_Lib.Rsplit
15:40:08 Word_Lib: theory Word_Lib.Most_significant_bit
15:40:08 Word_Lib: theory Word_Lib.Typedef_Morphisms
15:40:09 Word_Lib: theory Word_Lib.Generic_set_bit
15:40:09 Word_Lib: theory Word_Lib.Aligned
15:40:10 Word_Lib: theory Word_Lib.Next_and_Prev
15:40:10 Word_Lib: theory Word_Lib.Word_Lemmas
15:40:10 Word_Lib: theory Word_Lib.Reversed_Bit_Lists
15:40:12 Word_Lib: theory Word_Lib.Word_8
15:40:12 Word_Lib: theory Word_Lib.Ancient_Numeral
15:40:12 Word_Lib: theory Word_Lib.Bitwise
15:40:12 Word_Lib: theory Word_Lib.More_Word_Operations
15:40:13 Word_Lib: theory Word_Lib.Bitwise_Signed
15:40:13 Word_Lib: theory Word_Lib.Examples
15:40:13 Word_Lib: theory Word_Lib.Word_32
15:40:13 Word_Lib: theory Word_Lib.Word_64
15:40:15 Word_Lib: theory Word_Lib.Word_Lib_Sumo
15:40:18 Word_Lib: theory Word_Lib.Guide
15:41:01 Preparing Word_Lib/document ...
15:41:09 Finished Word_Lib/document (0:00:07 elapsed time)
15:41:09 Preparing Word_Lib/outline ...
15:41:15 Finished Word_Lib/outline (0:00:06 elapsed time)
15:41:16 Timing Word_Lib (8 threads, 48.385s elapsed time, 243.135s cpu time, 20.509s GC time, factor 5.03)
15:41:16 Finished Word_Lib (0:01:12 elapsed time, 0:04:52 cpu time, factor 4.05)
15:41:16 Building IP_Addresses ...
15:41:18 IP_Addresses: theory HOL-Library.Cancellation
15:41:18 IP_Addresses: theory HOL-Library.Infinite_Set
15:41:18 IP_Addresses: theory HOL-Library.Option_ord
15:41:18 IP_Addresses: theory IP_Addresses.NumberWang_IPv6
15:41:18 IP_Addresses: theory IP_Addresses.NumberWang_IPv4
15:41:19 IP_Addresses: theory HOL-Library.Multiset
15:41:24 IP_Addresses: theory HOL-ex.Quicksort
15:41:24 IP_Addresses: theory Automatic_Refinement.Misc
15:41:30 IP_Addresses: theory HOL-Library.Code_Abstract_Nat
15:41:30 IP_Addresses: theory IP_Addresses.Hs_Compat
15:41:30 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
15:41:30 IP_Addresses: theory IP_Addresses.WordInterval
15:41:30 IP_Addresses: theory HOL-Library.Product_Lexorder
15:41:30 IP_Addresses: theory HOL-Library.Code_Target_Nat
15:41:30 IP_Addresses: theory IP_Addresses.Lib_List_toString
15:41:30 IP_Addresses: theory IP_Addresses.Lib_Word_toString
15:41:33 IP_Addresses: theory IP_Addresses.WordInterval_Sorted
15:41:33 IP_Addresses: theory IP_Addresses.IP_Address
15:41:40 IP_Addresses: theory IP_Addresses.IPv4
15:41:40 IP_Addresses: theory IP_Addresses.Prefix_Match
15:41:40 IP_Addresses: theory IP_Addresses.IPv6
15:41:41 IP_Addresses: theory IP_Addresses.CIDR_Split
15:42:39 IP_Addresses: theory IP_Addresses.IP_Address_Parser
15:42:39 IP_Addresses: theory IP_Addresses.IP_Address_toString
15:42:41 IP_Addresses: theory IP_Addresses.Prefix_Match_toString
15:45:05 Preparing IP_Addresses/document ...
15:45:09 Finished IP_Addresses/document (0:00:04 elapsed time)
15:45:09 Preparing IP_Addresses/outline ...
15:45:13 Finished IP_Addresses/outline (0:00:03 elapsed time)
15:45:14 Timing IP_Addresses (8 threads, 181.568s elapsed time, 623.237s cpu time, 46.238s GC time, factor 3.43)
15:45:14 Finished IP_Addresses (0:03:47 elapsed time, 0:11:53 cpu time, factor 3.14)
15:45:14 Building Simple_Firewall ...
15:45:16 Simple_Firewall: theory HOL-Library.Char_ord
15:45:16 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
15:45:16 Simple_Firewall: theory Simple_Firewall.GroupF
15:45:16 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
15:45:16 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
15:45:16 Simple_Firewall: theory Simple_Firewall.List_Product_More
15:45:16 Simple_Firewall: theory Simple_Firewall.Option_Helpers
15:45:16 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
15:45:16 Simple_Firewall: theory Simple_Firewall.Iface
15:45:17 Simple_Firewall: theory Simple_Firewall.L4_Protocol
15:45:19 Simple_Firewall: theory Simple_Firewall.Simple_Packet
15:45:19 Simple_Firewall: theory Simple_Firewall.Primitives_toString
15:45:22 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
15:45:25 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
15:45:25 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString
15:45:28 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
15:45:28 Simple_Firewall: theory Simple_Firewall.Shadowed
15:45:28 Simple_Firewall: theory Simple_Firewall.Service_Matrix
15:45:55 Preparing Simple_Firewall/document ...
15:46:02 Finished Simple_Firewall/document (0:00:06 elapsed time)
15:46:02 Preparing Simple_Firewall/outline ...
15:46:08 Finished Simple_Firewall/outline (0:00:05 elapsed time)
15:46:08 Timing Simple_Firewall (8 threads, 18.017s elapsed time, 89.918s cpu time, 6.259s GC time, factor 4.99)
15:46:08 Finished Simple_Firewall (0:00:40 elapsed time, 0:02:12 cpu time, factor 3.28)
15:46:08 Building Routing ...
15:46:11 Routing: theory Routing.Linorder_Helper
15:46:11 Routing: theory HOL-Library.Adhoc_Overloading
15:46:11 Routing: theory HOL-Library.Monad_Syntax
15:46:12 Routing: theory Routing.Routing_Table
15:46:15 Routing: theory Routing.IpRoute_Parser
15:46:15 Routing: theory Routing.Linux_Router
15:46:38 Preparing Routing/document ...
15:46:41 Finished Routing/document (0:00:02 elapsed time)
15:46:41 Preparing Routing/outline ...
15:46:43 Finished Routing/outline (0:00:02 elapsed time)
15:46:44 Timing Routing (8 threads, 11.675s elapsed time, 30.478s cpu time, 1.142s GC time, factor 2.61)
15:46:44 Finished Routing (0:00:28 elapsed time, 0:01:01 cpu time, factor 2.13)
15:46:44 Building Iptables_Semantics ...
15:46:46 Iptables_Semantics: theory Iptables_Semantics.Negation_Type
15:46:46 Iptables_Semantics: theory Iptables_Semantics.List_Misc
15:46:48 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
15:46:49 Iptables_Semantics: theory HOL-Library.Code_Target_Int
15:46:49 Iptables_Semantics: theory HOL-Library.LaTeXsugar
15:46:49 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
15:46:49 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
15:46:49 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
15:46:49 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
15:46:49 Iptables_Semantics: theory Iptables_Semantics.Ternary
15:46:49 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
15:46:49 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
15:46:49 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
15:46:49 Iptables_Semantics: theory Native_Word.More_Bits_Int
15:46:49 Iptables_Semantics: theory Iptables_Semantics.Word_Upto
15:46:49 Iptables_Semantics: theory Iptables_Semantics.IpAddresses
15:46:50 Iptables_Semantics: theory Iptables_Semantics.Ports
15:46:50 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
15:46:51 Iptables_Semantics: theory Native_Word.Code_Symbolic_Bits_Int
15:46:51 Iptables_Semantics: theory Native_Word.Bits_Integer
15:46:51 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
15:47:04 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
15:47:04 Iptables_Semantics: theory Iptables_Semantics.Semantics
15:47:04 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
15:47:05 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
15:47:05 Iptables_Semantics: theory Iptables_Semantics.Matching
15:47:05 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
15:47:06 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
15:47:06 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
15:47:06 Iptables_Semantics: theory Native_Word.Code_Target_Bits_Int
15:47:06 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
15:47:06 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
15:47:07 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
15:47:08 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
15:47:08 Iptables_Semantics: theory Iptables_Semantics.Optimizing
15:47:08 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
15:47:09 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
15:47:10 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
15:47:11 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
15:47:12 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
15:47:14 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
15:47:14 Iptables_Semantics: theory Iptables_Semantics.Ipassmt
15:47:17 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
15:47:49 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
15:47:49 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
15:47:49 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
15:47:49 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
15:47:50 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
15:47:50 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
15:47:50 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
15:47:50 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
15:47:50 Iptables_Semantics: theory Iptables_Semantics.No_Spoof
15:47:55 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
15:47:56 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
15:47:58 Iptables_Semantics: theory Iptables_Semantics.Transform
15:48:02 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
15:48:03 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
15:48:07 Iptables_Semantics: theory Iptables_Semantics.Code_Interface
15:48:07 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
15:48:08 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
15:48:08 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
15:48:08 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
15:48:13 Iptables_Semantics: theory Iptables_Semantics.Parser
15:48:13 Iptables_Semantics: theory Iptables_Semantics.Parser6
15:48:13 Iptables_Semantics: theory Iptables_Semantics.Documentation
15:48:14 Iptables_Semantics: theory Iptables_Semantics.Code_haskell
15:49:24 Preparing Iptables_Semantics/document ...
15:49:42 Finished Iptables_Semantics/document (0:00:17 elapsed time)
15:49:42 Preparing Iptables_Semantics/outline ...
15:49:52 Finished Iptables_Semantics/outline (0:00:09 elapsed time)
15:49:53 Timing Iptables_Semantics (8 threads, 107.928s elapsed time, 528.014s cpu time, 48.582s GC time, factor 4.89)
15:49:53 Finished Iptables_Semantics (0:02:38 elapsed time, 0:10:32 cpu time, factor 3.98)
15:49:53 Building Iptables_Semantics_Examples ...
15:49:56 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com
15:49:56 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company
15:49:56 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall
15:49:56 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example
15:49:56 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test
15:49:56 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing
15:49:56 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test
15:49:56 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof
15:50:00 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail
15:50:00 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples
15:50:00 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed
15:50:01 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation
15:53:25 Preparing Iptables_Semantics_Examples/document ...
15:53:29 Finished Iptables_Semantics_Examples/document (0:00:04 elapsed time)
15:53:29 Preparing Iptables_Semantics_Examples/outline ...
15:53:33 Finished Iptables_Semantics_Examples/outline (0:00:04 elapsed time)
15:53:34 Timing Iptables_Semantics_Examples (8 threads, 185.242s elapsed time, 1325.401s cpu time, 126.355s GC time, factor 7.15)
15:53:34 Finished Iptables_Semantics_Examples (0:03:30 elapsed time, 0:22:54 cpu time, factor 6.53)
15:53:34 Running Iptables_Semantics_Examples_Big ...
15:53:37 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated
15:53:37 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern
15:53:37 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3
15:53:37 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small
15:53:37 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall
15:55:53 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large
16:42:53 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW
17:40:19 Preparing Iptables_Semantics_Examples_Big/document ...
17:40:23 Finished Iptables_Semantics_Examples_Big/document (0:00:03 elapsed time)
17:40:23 Preparing Iptables_Semantics_Examples_Big/outline ...
17:40:26 Finished Iptables_Semantics_Examples_Big/outline (0:00:03 elapsed time)
17:40:28 Timing Iptables_Semantics_Examples_Big (8 threads, 6398.412s elapsed time, 30880.777s cpu time, 13761.596s GC time, factor 4.83)
17:40:28 Finished Iptables_Semantics_Examples_Big (1:46:43 elapsed time, 8:34:48 cpu time, factor 4.82)
17:40:28 Building HOL-Library ...
17:40:30 HOL-Library: theory HOL-Library.Adhoc_Overloading
17:40:30 HOL-Library: theory HOL-Library.Boolean_Algebra
17:40:30 HOL-Library: theory HOL-Library.Cancellation
17:40:30 HOL-Library: theory HOL-Library.Char_ord
17:40:30 HOL-Library: theory HOL-Library.Case_Converter
17:40:30 HOL-Library: theory HOL-Library.BNF_Axiomatization
17:40:30 HOL-Library: theory HOL-Library.BNF_Corec
17:40:30 HOL-Library: theory HOL-Library.AList
17:40:30 HOL-Library: theory HOL-Library.Code_Abstract_Nat
17:40:30 HOL-Library: theory HOL-Library.Code_Prolog
17:40:30 HOL-Library: theory HOL-Library.Code_Binary_Nat
17:40:30 HOL-Library: theory HOL-Library.Monad_Syntax
17:40:30 HOL-Library: theory HOL-Library.State_Monad
17:40:30 HOL-Library: theory HOL-Library.Bit_Operations
17:40:30 HOL-Library: theory HOL-Library.Code_Target_Nat
17:40:31 HOL-Library: theory HOL-Library.Code_Lazy
17:40:31 HOL-Library: theory HOL-Library.Simps_Case_Conv
17:40:31 HOL-Library: theory HOL-Library.Multiset
17:40:31 HOL-Library: theory HOL-Library.Extended
17:40:32 HOL-Library: theory HOL-Library.Code_Target_Int
17:40:32 HOL-Library: theory HOL-Library.Code_Test
17:40:32 HOL-Library: theory HOL-Library.Code_Target_Numeral
17:40:32 HOL-Library: theory HOL-Library.Comparator
17:40:32 HOL-Library: theory HOL-Library.Conditional_Parametricity
17:40:32 HOL-Library: theory HOL-Library.DAList
17:40:33 HOL-Library: theory HOL-Library.Confluence
17:40:33 HOL-Library: theory HOL-Library.Datatype_Records
17:40:33 HOL-Library: theory HOL-Library.Confluent_Quotient
17:40:33 HOL-Library: theory HOL-Library.Debug
17:40:33 HOL-Library: theory HOL-Library.Disjoint_Sets
17:40:33 HOL-Library: theory HOL-Library.Dlist
17:40:33 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
17:40:34 HOL-Library: theory HOL-Library.Fun_Lexorder
17:40:34 HOL-Library: theory HOL-Library.FuncSet
17:40:34 HOL-Library: theory HOL-Library.Function_Algebras
17:40:34 HOL-Library: theory HOL-Library.Groups_Big_Fun
17:40:34 HOL-Library: theory HOL-Library.Function_Division
17:40:34 HOL-Library: theory HOL-Library.IArray
17:40:34 HOL-Library: theory HOL-Library.Infinite_Set
17:40:34 HOL-Library: theory HOL-Library.LaTeXsugar
17:40:34 HOL-Library: theory HOL-Library.Lattice_Constructions
17:40:34 HOL-Library: theory HOL-Library.Lattice_Syntax
17:40:34 HOL-Library: theory HOL-Library.Equipollence
17:40:34 HOL-Library: theory HOL-Library.Combine_PER
17:40:35 HOL-Library: theory HOL-Library.Complete_Partial_Order2
17:40:35 HOL-Library: theory HOL-Library.Omega_Words_Fun
17:40:35 HOL-Library: theory HOL-Library.Ramsey
17:40:35 HOL-Library: theory HOL-Library.ListVector
17:40:35 HOL-Library: theory HOL-Library.List_Lenlexorder
17:40:35 HOL-Library: theory HOL-Library.List_Lexorder
17:40:35 HOL-Library: theory HOL-Library.Mapping
17:40:35 HOL-Library: theory HOL-Library.More_List
17:40:36 HOL-Library: theory HOL-Library.Nat_Bijection
17:40:36 HOL-Library: theory HOL-Library.Poly_Mapping
17:40:36 HOL-Library: theory HOL-Library.Stream
17:40:37 HOL-Library: theory HOL-Library.AList_Mapping
17:40:37 HOL-Library: theory HOL-Library.Old_Datatype
17:40:38 HOL-Library: theory HOL-Library.DAList_Multiset
17:40:38 HOL-Library: theory HOL-Library.Multiset_Order
17:40:40 HOL-Library: theory HOL-Library.Old_Recdef
17:40:40 HOL-Library: theory HOL-Library.Open_State_Syntax
17:40:40 HOL-Library: theory HOL-Library.Option_ord
17:40:40 HOL-Library: theory HOL-Library.Parallel
17:40:41 HOL-Library: theory HOL-Library.Pattern_Aliases
17:40:41 HOL-Library: theory HOL-Library.Perm
17:40:41 HOL-Library: theory HOL-Library.Phantom_Type
17:40:41 HOL-Library: theory HOL-Library.Power_By_Squaring
17:40:41 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
17:40:41 HOL-Library: theory HOL-Library.Preorder
17:40:42 HOL-Library: theory HOL-Library.Product_Lexorder
17:40:42 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
17:40:42 HOL-Library: theory HOL-Library.Product_Plus
17:40:42 HOL-Library: theory HOL-Library.Quotient_Syntax
17:40:42 HOL-Library: theory HOL-Library.Quotient_Option
17:40:42 HOL-Library: theory HOL-Library.Quotient_Product
17:40:42 HOL-Library: theory HOL-Library.Quotient_Set
17:40:42 HOL-Library: theory HOL-Library.Product_Order
17:40:42 HOL-Library: theory HOL-Library.Cardinality
17:40:42 HOL-Library: theory HOL-Library.Quotient_Sum
17:40:42 HOL-Library: theory HOL-Library.Quotient_Type
17:40:42 HOL-Library: theory HOL-Library.Quotient_List
17:40:43 HOL-Library: theory HOL-Library.RBT_Impl
17:40:43 HOL-Library: theory HOL-Library.Realizers
17:40:43 HOL-Library: theory HOL-Library.Finite_Lattice
17:40:43 HOL-Library: theory HOL-Library.Reflection
17:40:43 HOL-Library: theory HOL-Library.Refute
17:40:43 HOL-Library: theory HOL-Library.Rewrite
17:40:43 HOL-Library: theory HOL-Library.Set_Algebras
17:40:44 HOL-Library: theory HOL-Library.Signed_Division
17:40:44 HOL-Library: theory HOL-Library.Sorting_Algorithms
17:40:44 HOL-Library: theory HOL-Library.Sublist
17:40:44 HOL-Library: theory HOL-Library.Transitive_Closure_Table
17:40:45 HOL-Library: theory HOL-Library.Tree
17:40:45 HOL-Library: theory HOL-Library.Numeral_Type
17:40:45 HOL-Library: theory HOL-Library.Uprod
17:40:46 HOL-Library: theory HOL-Library.While_Combinator
17:40:46 HOL-Library: theory HOL-Library.Z2
17:40:47 HOL-Library: theory HOL-Library.Countable
17:40:47 HOL-Library: theory HOL-Library.BigO
17:40:47 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
17:40:47 HOL-Library: theory HOL-Library.Type_Length
17:40:47 HOL-Library: theory HOL-Library.Prefix_Order
17:40:47 HOL-Library: theory HOL-Library.Subseq_Order
17:40:47 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
17:40:47 HOL-Library: theory HOL-Library.Diagonal_Subsequence
17:40:47 HOL-Library: theory HOL-Library.Discrete
17:40:47 HOL-Library: theory HOL-Library.Going_To_Filter
17:40:47 HOL-Library: theory HOL-Library.Indicator_Function
17:40:48 HOL-Library: theory HOL-Library.Landau_Symbols
17:40:48 HOL-Library: theory HOL-Library.Saturated
17:40:48 HOL-Library: theory HOL-Library.Word
17:40:48 HOL-Library: theory HOL-Library.Countable_Set
17:40:48 HOL-Library: theory HOL-Library.FSet
17:40:48 HOL-Library: theory HOL-Library.Lattice_Algebras
17:40:48 HOL-Library: theory HOL-Library.Tree_Multiset
17:40:49 HOL-Library: theory HOL-Library.Liminf_Limsup
17:40:49 HOL-Library: theory HOL-Library.Countable_Complete_Lattices
17:40:49 HOL-Library: theory HOL-Library.Countable_Set_Type
17:40:49 HOL-Library: theory HOL-Library.Set_Idioms
17:40:50 HOL-Library: theory HOL-Library.Log_Nat
17:40:50 HOL-Library: theory HOL-Library.Lub_Glb
17:40:50 HOL-Library: theory HOL-Library.Nonpos_Ints
17:40:50 HOL-Library: theory HOL-Library.OptionalSugar
17:40:50 HOL-Library: theory HOL-Library.Periodic_Fun
17:40:50 HOL-Library: theory HOL-Library.Quadratic_Discriminant
17:40:50 HOL-Library: theory HOL-Library.Sum_of_Squares
17:40:50 HOL-Library: theory HOL-Library.Tree_Real
17:40:51 HOL-Library: theory HOL-Library.Order_Continuity
17:40:51 HOL-Library: theory HOL-Library.Finite_Map
17:40:51 HOL-Library: theory HOL-Library.Extended_Nat
17:40:52 HOL-Library: theory HOL-Library.Extended_Real
17:40:53 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
17:40:53 HOL-Library: theory HOL-Library.Interval
17:40:54 HOL-Library: theory HOL-Library.Float
17:40:56 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
17:40:56 HOL-Library: theory HOL-Library.Interval_Float
17:41:05 HOL-Library: theory HOL-Library.Disjoint_FSets
17:41:06 HOL-Library: theory HOL-Library.Library
17:41:30 HOL-Library: theory HOL-Library.RBT
17:41:31 HOL-Library: theory HOL-Library.RBT_Mapping
17:41:31 HOL-Library: theory HOL-Library.RBT_Set
17:43:33 Preparing HOL-Library/document ...
17:44:20 Finished HOL-Library/document (0:00:46 elapsed time)
17:44:20 Preparing HOL-Library/outline ...
17:44:49 Finished HOL-Library/outline (0:00:29 elapsed time)
17:44:52 Timing HOL-Library (8 threads, 120.907s elapsed time, 746.630s cpu time, 45.990s GC time, factor 6.18)
17:44:52 Finished HOL-Library (0:03:00 elapsed time, 0:14:31 cpu time, factor 4.83)
17:44:52 Building Category3 ...
17:44:54 Category3: theory HOL-Cardinals.Fun_More
17:44:54 Category3: theory HOL-Cardinals.Order_Union
17:44:54 Category3: theory HOL-Cardinals.Order_Relation_More
17:44:54 Category3: theory Category3.Category
17:44:54 Category3: theory HereditarilyFinite.HF
17:44:55 Category3: theory HOL-Cardinals.Wellorder_Extension
17:44:55 Category3: theory HOL-Cardinals.Wellfounded_More
17:44:55 Category3: theory HOL-Cardinals.Wellorder_Relation
17:44:55 Category3: theory Category3.ConcreteCategory
17:44:55 Category3: theory Category3.DiscreteCategory
17:44:55 Category3: theory Category3.DualCategory
17:44:55 Category3: theory Category3.EpiMonoIso
17:44:55 Category3: theory HOL-Cardinals.Wellorder_Embedding
17:44:56 Category3: theory HOL-Cardinals.Wellorder_Constructions
17:44:56 Category3: theory Category3.InitialTerminal
17:44:56 Category3: theory Category3.ProductCategory
17:44:57 Category3: theory HOL-Cardinals.Cardinal_Order_Relation
17:44:57 Category3: theory HOL-Cardinals.Ordinal_Arithmetic
17:44:57 Category3: theory Category3.FreeCategory
17:44:57 Category3: theory Category3.Functor
17:44:58 Category3: theory HOL-Cardinals.Cardinal_Arithmetic
17:44:58 Category3: theory HOL-Cardinals.Cardinals
17:45:01 Category3: theory Category3.NaturalTransformation
17:45:01 Category3: theory Category3.Subcategory
17:45:03 Category3: theory Category3.SetCategory
17:45:04 Category3: theory Category3.BinaryFunctor
17:45:07 Category3: theory Category3.SetCat
17:45:09 Category3: theory Category3.FunctorCategory
17:45:17 Category3: theory Category3.Yoneda
17:45:40 Category3: theory Category3.Adjunction
17:46:08 Category3: theory Category3.EquivalenceOfCategories
17:46:08 Category3: theory Category3.Limit
17:47:05 Category3: theory Category3.CartesianCategory
17:47:06 Category3: theory Category3.CategoryWithPullbacks
17:47:21 Category3: theory Category3.CartesianClosedCategory
17:47:21 Category3: theory Category3.CategoryWithFiniteLimits
17:47:25 Category3: theory Category3.HFSetCat
17:50:19 Preparing Category3/document ...
17:50:40 Finished Category3/document (0:00:20 elapsed time)
17:50:40 Preparing Category3/outline ...
17:50:48 Finished Category3/outline (0:00:08 elapsed time)
17:50:51 Timing Category3 (8 threads, 256.998s elapsed time, 1193.357s cpu time, 109.089s GC time, factor 4.64)
17:50:51 Finished Category3 (0:05:24 elapsed time, 0:22:11 cpu time, factor 4.10)
17:50:51 Building MonoidalCategory ...
17:50:54 MonoidalCategory: theory MonoidalCategory.MonoidalCategory
17:51:57 MonoidalCategory: theory MonoidalCategory.MonoidalFunctor
17:51:59 MonoidalCategory: theory MonoidalCategory.CartesianMonoidalCategory
17:52:22 MonoidalCategory: theory MonoidalCategory.FreeMonoidalCategory
17:57:18 Preparing MonoidalCategory/document ...
17:57:29 Finished MonoidalCategory/document (0:00:10 elapsed time)
17:57:29 Preparing MonoidalCategory/outline ...
17:57:34 Finished MonoidalCategory/outline (0:00:05 elapsed time)
17:57:36 Timing MonoidalCategory (8 threads, 323.621s elapsed time, 744.024s cpu time, 78.799s GC time, factor 2.30)
17:57:36 Finished MonoidalCategory (0:06:26 elapsed time, 0:14:28 cpu time, factor 2.25)
17:57:36 Running Bicategory ...
17:57:48 Bicategory: theory Bicategory.IsomorphismClass
17:57:49 Bicategory: theory Bicategory.Prebicategory
17:58:40 Bicategory: theory Bicategory.Bicategory
17:59:37 Bicategory: theory Bicategory.Coherence
17:59:39 Bicategory: theory Bicategory.InternalEquivalence
17:59:39 Bicategory: theory Bicategory.Subbicategory
18:02:05 Bicategory: theory Bicategory.CanonicalIsos
18:02:05 Bicategory: theory Bicategory.Pseudofunctor
18:05:49 Bicategory: theory Bicategory.Strictness
18:07:50 Bicategory: theory Bicategory.InternalAdjunction
18:11:11 Bicategory: theory Bicategory.PseudonaturalTransformation
18:11:11 Bicategory: theory Bicategory.Tabulation
18:11:12 Bicategory: theory Bicategory.SpanBicategory
18:17:53 Bicategory: theory Bicategory.EquivalenceOfBicategories
18:21:15 Bicategory: theory Bicategory.Modification
18:39:54 Bicategory: theory Bicategory.BicategoryOfSpans
19:00:28 Preparing Bicategory/document ...
19:01:51 Finished Bicategory/document (0:01:23 elapsed time)
19:01:51 Preparing Bicategory/outline ...
19:02:08 Finished Bicategory/outline (0:00:16 elapsed time)
19:02:09 Timing Bicategory (8 threads, 3761.189s elapsed time, 10016.859s cpu time, 1677.877s GC time, factor 2.66)
19:02:09 Finished Bicategory (1:02:46 elapsed time, 2:47:02 cpu time, factor 2.66)
19:02:09 Building ConcurrentIMP ...
19:02:11 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred
19:02:12 ConcurrentIMP: theory ConcurrentIMP.Infinite_Sequences
19:02:12 ConcurrentIMP: theory ConcurrentIMP.LTL
19:02:13 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang
19:02:19 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg
19:02:25 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg_rules
19:02:26 ConcurrentIMP: theory ConcurrentIMP.CIMP
19:02:26 ConcurrentIMP: theory ConcurrentIMP.CIMP_locales
19:02:26 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer
19:02:26 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer
19:02:55 Preparing ConcurrentIMP/document ...
19:03:00 Finished ConcurrentIMP/document (0:00:04 elapsed time)
19:03:00 Preparing ConcurrentIMP/outline ...
19:03:04 Finished ConcurrentIMP/outline (0:00:04 elapsed time)
19:03:04 Timing ConcurrentIMP (8 threads, 19.162s elapsed time, 65.659s cpu time, 5.215s GC time, factor 3.43)
19:03:04 Finished ConcurrentIMP (0:00:45 elapsed time, 0:01:57 cpu time, factor 2.56)
19:03:04 Running ConcurrentGC ...
19:03:06 ConcurrentGC: theory ConcurrentGC.Model
19:03:22 ConcurrentGC: theory ConcurrentGC.Proofs_Basis
19:03:33 ConcurrentGC: theory ConcurrentGC.Global_Invariants
19:03:33 ConcurrentGC: theory ConcurrentGC.Local_Invariants
19:03:33 ConcurrentGC: theory ConcurrentGC.Tactics
19:03:33 ConcurrentGC: theory ConcurrentGC.Concrete_heap
19:03:33 ConcurrentGC: theory ConcurrentGC.Global_Invariants_Lemmas
19:03:34 ConcurrentGC: theory ConcurrentGC.Concrete
19:03:36 ConcurrentGC: theory ConcurrentGC.Global_Noninterference
19:05:01 ConcurrentGC: theory ConcurrentGC.Local_Invariants_Lemmas
19:05:02 ConcurrentGC: theory ConcurrentGC.Initial_Conditions
19:05:02 ConcurrentGC: theory ConcurrentGC.MarkObject
19:05:03 ConcurrentGC: theory ConcurrentGC.Noninterference
19:05:03 ConcurrentGC: theory ConcurrentGC.Phases
19:05:03 ConcurrentGC: theory ConcurrentGC.StrongTricolour
19:05:03 ConcurrentGC: theory ConcurrentGC.TSO
19:05:03 ConcurrentGC: theory ConcurrentGC.Valid_Refs
19:05:04 ConcurrentGC: theory ConcurrentGC.Worklists
19:05:05 ConcurrentGC: theory ConcurrentGC.Proofs
19:18:40 Preparing ConcurrentGC/document ...
19:18:48 Finished ConcurrentGC/document (0:00:08 elapsed time)
19:18:49 Preparing ConcurrentGC/outline ...
19:18:55 Finished ConcurrentGC/outline (0:00:06 elapsed time)
19:18:55 Timing ConcurrentGC (8 threads, 932.415s elapsed time, 5248.371s cpu time, 214.590s GC time, factor 5.63)
19:18:55 Finished ConcurrentGC (0:15:35 elapsed time, 1:27:31 cpu time, factor 5.62)
19:18:55 Presentation in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info"
19:18:55 Presenting AODV ...
19:18:56 Presenting document AODV/document
19:18:56 Presenting document AODV/outline
19:18:56 Presenting theory AODV.Aodv_Basic
19:18:56 Presenting theory AODV.Aodv_Data
19:18:56 Presenting theory AODV.Aodv_Predicates
19:18:56 Presenting theory AODV.Aodv
19:18:56 Presenting theory AODV.Aodv_Message
19:18:56 Presenting theory AODV.OAodv
19:18:56 Presenting theory AODV.Fresher
19:18:56 Presenting theory AODV.Quality_Increases
19:18:56 Presenting theory AODV.Seq_Invariants
19:18:56 Presenting theory AODV.Global_Invariants
19:18:56 Presenting theory AODV.Loop_Freedom
19:18:56 Presenting theory AODV.Aodv_Loop_Freedom
19:18:56 Presenting theory AODV.A_Norreqid
19:18:56 Presenting theory AODV.A_Aodv_Data
19:18:58 Presenting theory AODV.A_Aodv_Message
19:18:58 Presenting theory AODV.A_Aodv
19:18:59 Presenting theory AODV.A_Aodv_Predicates
19:18:59 Presenting theory AODV.A_Fresher
19:19:00 Presenting theory AODV.A_Seq_Invariants
19:19:00 Presenting theory AODV.A_Quality_Increases
19:19:00 Presenting theory AODV.A_OAodv
19:19:00 Presenting theory AODV.A_Global_Invariants
19:19:01 Presenting theory AODV.A_Loop_Freedom
19:19:01 Presenting theory AODV.A_Aodv_Loop_Freedom
19:19:01 Presenting theory AODV.B_Fwdrreps
19:19:01 Presenting theory AODV.B_Aodv_Data
19:19:01 Presenting theory AODV.B_Aodv_Message
19:19:01 Presenting theory AODV.B_Aodv
19:19:02 Presenting theory AODV.B_Aodv_Predicates
19:19:03 Presenting theory AODV.B_Fresher
19:19:03 Presenting theory AODV.B_Seq_Invariants
19:19:03 Presenting theory AODV.B_Quality_Increases
19:19:03 Presenting theory AODV.B_OAodv
19:19:03 Presenting theory AODV.B_Global_Invariants
19:19:04 Presenting theory AODV.B_Loop_Freedom
19:19:04 Presenting theory AODV.B_Aodv_Loop_Freedom
19:19:04 Presenting theory AODV.C_Gtobcast
19:19:04 Presenting theory AODV.C_Aodv_Data
19:19:05 Presenting theory AODV.C_Aodv_Message
19:19:05 Presenting theory AODV.C_Aodv
19:19:06 Presenting theory AODV.C_Aodv_Predicates
19:19:06 Presenting theory AODV.C_Fresher
19:19:06 Presenting theory AODV.C_Seq_Invariants
19:19:06 Presenting theory AODV.C_Quality_Increases
19:19:07 Presenting theory AODV.C_OAodv
19:19:07 Presenting theory AODV.C_Global_Invariants
19:19:07 Presenting theory AODV.C_Loop_Freedom
19:19:07 Presenting theory AODV.C_Aodv_Loop_Freedom
19:19:08 Presenting theory AODV.D_Fwdrreqs
19:19:08 Presenting theory AODV.D_Aodv_Data
19:19:08 Presenting theory AODV.D_Aodv_Message
19:19:08 Presenting theory AODV.D_Aodv
19:19:08 Presenting theory AODV.D_Aodv_Predicates
19:19:09 Presenting theory AODV.D_Fresher
19:19:09 Presenting theory AODV.D_Seq_Invariants
19:19:09 Presenting theory AODV.D_Quality_Increases
19:19:09 Presenting theory AODV.D_OAodv
19:19:09 Presenting theory AODV.D_Global_Invariants
19:19:10 Presenting theory AODV.D_Loop_Freedom
19:19:10 Presenting theory AODV.D_Aodv_Loop_Freedom
19:19:10 Presenting theory AODV.E_All_ABCD
19:19:10 Presenting theory AODV.E_Aodv_Data
19:19:11 Presenting theory AODV.E_Aodv_Message
19:19:11 Presenting theory AODV.E_Aodv
19:19:12 Presenting theory AODV.E_Aodv_Predicates
19:19:12 Presenting theory AODV.E_Fresher
19:19:12 Presenting theory AODV.E_Seq_Invariants
19:19:12 Presenting theory AODV.E_Quality_Increases
19:19:13 Presenting theory AODV.E_OAodv
19:19:13 Presenting theory AODV.E_Global_Invariants
19:19:13 Presenting theory AODV.E_Loop_Freedom
19:19:13 Presenting theory AODV.E_Aodv_Loop_Freedom
19:19:13 Presenting theory AODV.All
19:19:15 Presenting Flyspeck-Tame-Computation ...
19:19:15 Presenting theory Flyspeck-Tame-Computation.ArchComp
19:19:15 Presenting theory Flyspeck-Tame-Computation.Completeness
19:19:15 Presenting Bicategory ...
19:19:15 Presenting document Bicategory/document
19:19:15 Presenting document Bicategory/outline
19:19:15 Presenting theory Bicategory.IsomorphismClass
19:19:15 Presenting theory Bicategory.Prebicategory
19:19:15 Presenting theory Bicategory.Bicategory
19:19:15 Presenting theory Bicategory.Coherence
19:19:15 Presenting theory Bicategory.CanonicalIsos
19:19:15 Presenting theory Bicategory.Subbicategory
19:19:15 Presenting theory Bicategory.InternalEquivalence
19:19:15 Presenting theory Bicategory.Pseudofunctor
19:19:15 Presenting theory Bicategory.Strictness
19:19:16 Presenting theory Bicategory.InternalAdjunction
19:19:17 Presenting theory Bicategory.PseudonaturalTransformation
19:19:18 Presenting theory Bicategory.EquivalenceOfBicategories
19:19:19 Presenting theory Bicategory.SpanBicategory
19:19:19 Presenting theory Bicategory.Tabulation
19:19:21 Presenting theory Bicategory.BicategoryOfSpans
19:19:23 Presenting theory Bicategory.Modification
19:19:36 Presenting ConcurrentGC ...
19:19:36 Presenting document ConcurrentGC/document
19:19:36 Presenting document ConcurrentGC/outline
19:19:36 Presenting theory ConcurrentGC.Model
19:19:36 Presenting theory ConcurrentGC.Proofs_Basis
19:19:36 Presenting theory ConcurrentGC.Local_Invariants
19:19:36 Presenting theory ConcurrentGC.Global_Invariants
19:19:36 Presenting theory ConcurrentGC.Tactics
19:19:36 Presenting theory ConcurrentGC.Global_Invariants_Lemmas
19:19:36 Presenting theory ConcurrentGC.Local_Invariants_Lemmas
19:19:36 Presenting theory ConcurrentGC.Initial_Conditions
19:19:36 Presenting theory ConcurrentGC.Noninterference
19:19:37 Presenting theory ConcurrentGC.Global_Noninterference
19:19:37 Presenting theory ConcurrentGC.MarkObject
19:19:37 Presenting theory ConcurrentGC.Phases
19:19:37 Presenting theory ConcurrentGC.StrongTricolour
19:19:37 Presenting theory ConcurrentGC.TSO
19:19:38 Presenting theory ConcurrentGC.Valid_Refs
19:19:38 Presenting theory ConcurrentGC.Worklists
19:19:38 Presenting theory ConcurrentGC.Proofs
19:19:38 Presenting theory ConcurrentGC.Concrete_heap
19:19:38 Presenting theory ConcurrentGC.Concrete
19:19:39 Presenting JinjaThreads ...
19:19:39 Presenting document JinjaThreads/document
19:19:39 Presenting document JinjaThreads/outline
19:19:39 Presenting theory JinjaThreads.Set_without_equal
19:19:39 Presenting theory JinjaThreads.Set_Monad
19:19:39 Presenting theory JinjaThreads.JT_ICF
19:19:39 Presenting theory JinjaThreads.Basic_Main
19:19:39 Presenting theory JinjaThreads.FWState
19:19:39 Presenting theory JinjaThreads.FWLock
19:19:39 Presenting theory JinjaThreads.FWLocking
19:19:39 Presenting theory JinjaThreads.Auxiliary
19:19:39 Presenting theory JinjaThreads.FWThread
19:19:39 Presenting theory JinjaThreads.FWWait
19:19:39 Presenting theory JinjaThreads.FWCondAction
19:19:39 Presenting theory JinjaThreads.FWWellform
19:19:40 Presenting theory JinjaThreads.FWLockingThread
19:19:40 Presenting theory JinjaThreads.FWInterrupt
19:19:40 Presenting theory JinjaThreads.FWSemantics
19:19:40 Presenting theory JinjaThreads.FWProgressAux
19:19:40 Presenting theory JinjaThreads.FWDeadlock
19:19:40 Presenting theory JinjaThreads.FWProgress
19:19:40 Presenting theory JinjaThreads.FWLifting
19:19:40 Presenting theory JinjaThreads.LTS
19:19:41 Presenting theory JinjaThreads.FWLTS
19:19:41 Presenting theory JinjaThreads.Bisimulation
19:19:41 Presenting theory JinjaThreads.FWBisimulation
19:19:41 Presenting theory JinjaThreads.FWBisimDeadlock
19:19:42 Presenting theory JinjaThreads.FWLiftingSem
19:19:43 Presenting theory JinjaThreads.FWInitFinLift
19:19:43 Presenting theory JinjaThreads.FWBisimLift
19:19:44 Presenting theory JinjaThreads.Semilat
19:19:45 Presenting theory JinjaThreads.Err
19:19:45 Presenting theory JinjaThreads.Opt
19:19:45 Presenting theory JinjaThreads.Product
19:19:46 Presenting theory JinjaThreads.Listn
19:19:46 Presenting theory JinjaThreads.Semilattices
19:19:46 Presenting theory JinjaThreads.Typing_Framework
19:19:46 Presenting theory JinjaThreads.SemilatAlg
19:19:46 Presenting theory JinjaThreads.Typing_Framework_err
19:19:46 Presenting theory JinjaThreads.Kildall
19:19:46 Presenting theory JinjaThreads.LBVSpec
19:19:46 Presenting theory JinjaThreads.LBVCorrect
19:19:46 Presenting theory JinjaThreads.LBVComplete
19:19:47 Presenting theory JinjaThreads.Abstract_BV
19:19:47 Presenting theory JinjaThreads.Type
19:19:47 Presenting theory JinjaThreads.Decl
19:19:47 Presenting theory JinjaThreads.TypeRel
19:19:47 Presenting theory JinjaThreads.Value
19:19:47 Presenting theory JinjaThreads.Exceptions
19:19:47 Presenting theory JinjaThreads.SystemClasses
19:19:47 Presenting theory JinjaThreads.Heap
19:19:47 Presenting theory JinjaThreads.Observable_Events
19:19:47 Presenting theory JinjaThreads.StartConfig
19:19:47 Presenting theory JinjaThreads.Conform
19:19:47 Presenting theory JinjaThreads.ExternalCall
19:19:47 Presenting theory JinjaThreads.WellForm
19:19:48 Presenting theory JinjaThreads.ExternalCallWF
19:19:48 Presenting theory JinjaThreads.ConformThreaded
19:19:48 Presenting theory JinjaThreads.BinOp
19:19:48 Presenting theory JinjaThreads.SemiType
19:19:48 Presenting theory JinjaThreads.Common_Main
19:19:48 Presenting theory JinjaThreads.State
19:19:48 Presenting theory JinjaThreads.Expr
19:19:49 Presenting theory JinjaThreads.JHeap
19:19:49 Presenting theory JinjaThreads.SmallStep
19:19:49 Presenting theory JinjaThreads.WWellForm
19:19:49 Presenting theory JinjaThreads.WellType
19:19:49 Presenting theory JinjaThreads.DefAss
19:19:49 Presenting theory JinjaThreads.JWellForm
19:19:49 Presenting theory JinjaThreads.Threaded
19:19:49 Presenting theory JinjaThreads.WellTypeRT
19:19:50 Presenting theory JinjaThreads.Progress
19:19:51 Presenting theory JinjaThreads.DefAssPreservation
19:19:51 Presenting theory JinjaThreads.TypeSafe
19:19:51 Presenting theory JinjaThreads.ProgressThreaded
19:19:51 Presenting theory JinjaThreads.Deadlocked
19:19:51 Presenting theory JinjaThreads.Annotate
19:19:52 Presenting theory JinjaThreads.J_Main
19:19:52 Presenting theory JinjaThreads.JVMState
19:19:53 Presenting theory JinjaThreads.JVMInstructions
19:19:53 Presenting theory JinjaThreads.JVMHeap
19:19:53 Presenting theory JinjaThreads.JVMExecInstr
19:19:53 Presenting theory JinjaThreads.JVMExceptions
19:19:53 Presenting theory JinjaThreads.JVMExec
19:19:54 Presenting theory JinjaThreads.JVMDefensive
19:19:54 Presenting theory JinjaThreads.JVMThreaded
19:19:54 Presenting theory JinjaThreads.JVM_Main
19:19:54 Presenting theory JinjaThreads.JVM_SemiType
19:19:55 Presenting theory JinjaThreads.Effect
19:19:55 Presenting theory JinjaThreads.BVSpec
19:19:56 Presenting theory JinjaThreads.BVConform
19:19:56 Presenting theory JinjaThreads.BVSpecTypeSafe
19:19:56 Presenting theory JinjaThreads.BVNoTypeError
19:19:56 Presenting theory JinjaThreads.BVProgressThreaded
19:19:56 Presenting theory JinjaThreads.JVMDeadlocked
19:19:57 Presenting theory JinjaThreads.EffectMono
19:19:57 Presenting theory JinjaThreads.TF_JVM
19:19:57 Presenting theory JinjaThreads.LBVJVM
19:19:57 Presenting theory JinjaThreads.BVExec
19:19:58 Presenting theory JinjaThreads.BCVExec
19:19:58 Presenting theory JinjaThreads.BV_Main
19:19:58 Presenting theory JinjaThreads.CallExpr
19:19:59 Presenting theory JinjaThreads.J0
19:19:59 Presenting theory JinjaThreads.J0Bisim
19:19:59 Presenting theory JinjaThreads.J1State
19:19:59 Presenting theory JinjaThreads.J1Heap
19:20:00 Presenting theory JinjaThreads.J1
19:20:00 Presenting theory JinjaThreads.J1Deadlock
19:20:00 Presenting theory JinjaThreads.PCompiler
19:20:02 Presenting theory JinjaThreads.Compiler2
19:20:02 Presenting theory JinjaThreads.Exception_Tables
19:20:02 Presenting theory JinjaThreads.J1WellType
19:20:03 Presenting theory JinjaThreads.J1WellForm
19:20:03 Presenting theory JinjaThreads.TypeComp
19:20:03 Presenting theory JinjaThreads.JVMTau
19:20:04 Presenting theory JinjaThreads.Execs
19:20:04 Presenting theory JinjaThreads.J1JVMBisim
19:20:05 Presenting theory JinjaThreads.J1JVM
19:20:07 Presenting theory JinjaThreads.JVMJ1
19:20:07 Presenting theory JinjaThreads.Correctness2
19:20:07 Presenting theory JinjaThreads.ListIndex
19:20:07 Presenting theory JinjaThreads.Compiler1
19:20:07 Presenting theory JinjaThreads.J0J1Bisim
19:20:08 Presenting theory JinjaThreads.Correctness1Threaded
19:20:08 Presenting theory JinjaThreads.Correctness1
19:20:10 Presenting theory JinjaThreads.JJ1WellForm
19:20:10 Presenting theory JinjaThreads.Compiler
19:20:10 Presenting theory JinjaThreads.Correctness
19:20:11 Presenting theory JinjaThreads.Preprocessor
19:20:11 Presenting theory JinjaThreads.Compiler_Main
19:20:11 Presenting theory JinjaThreads.MM
19:20:11 Presenting theory JinjaThreads.SC
19:20:12 Presenting theory JinjaThreads.SC_Interp
19:20:12 Presenting theory JinjaThreads.SC_Collections
19:20:14 Presenting theory JinjaThreads.Orders
19:20:15 Presenting theory JinjaThreads.JMM_Spec
19:20:15 Presenting theory JinjaThreads.JMM_DRF
19:20:15 Presenting theory JinjaThreads.SC_Legal
19:20:17 Presenting theory JinjaThreads.Non_Speculative
19:20:18 Presenting theory JinjaThreads.SC_Completion
19:20:20 Presenting theory JinjaThreads.HB_Completion
19:20:20 Presenting theory JinjaThreads.JMM_Heap
19:20:21 Presenting theory JinjaThreads.JMM_Framework
19:20:24 Presenting theory JinjaThreads.JMM_Typesafe
19:20:28 Presenting theory JinjaThreads.JMM_Common
19:20:31 Presenting theory JinjaThreads.JMM_J
19:20:31 Presenting theory JinjaThreads.DRF_J
19:20:32 Presenting theory JinjaThreads.JMM_JVM
19:20:32 Presenting theory JinjaThreads.DRF_JVM
19:20:35 Presenting theory JinjaThreads.JMM_Type
19:20:36 Presenting theory JinjaThreads.JMM_Compiler
19:20:36 Presenting theory JinjaThreads.JMM_Type2
19:20:37 Presenting theory JinjaThreads.JMM_Interp
19:20:37 Presenting theory JinjaThreads.JMM_Typesafe2
19:20:37 Presenting theory JinjaThreads.JMM_J_Typesafe
19:20:39 Presenting theory JinjaThreads.JMM_JVM_Typesafe
19:20:40 Presenting theory JinjaThreads.JMM_Compiler_Type2
19:20:40 Presenting theory JinjaThreads.JMM
19:20:40 Presenting theory JinjaThreads.MM_Main
19:20:40 Presenting theory JinjaThreads.State_Refinement
19:20:40 Presenting theory JinjaThreads.Scheduler
19:20:40 Presenting theory JinjaThreads.Random_Scheduler
19:20:41 Presenting theory JinjaThreads.Round_Robin
19:20:42 Presenting theory JinjaThreads.SC_Schedulers
19:20:42 Presenting theory JinjaThreads.TypeRelRefine
19:20:42 Presenting theory JinjaThreads.PCompilerRefine
19:20:43 Presenting theory JinjaThreads.J_Execute
19:20:44 Presenting theory JinjaThreads.ExternalCall_Execute
19:20:44 Presenting theory JinjaThreads.JVMExec_Execute2
19:20:44 Presenting theory JinjaThreads.JVM_Execute2
19:20:45 Presenting theory JinjaThreads.Code_Generation
19:20:45 Presenting theory JinjaThreads.JVMExec_Execute
19:20:47 Presenting theory JinjaThreads.JVM_Execute
19:20:47 Presenting theory JinjaThreads.ToString
19:20:48 Presenting theory JinjaThreads.Java2Jinja
19:20:48 Presenting theory JinjaThreads.Execute_Main
19:20:48 Presenting theory JinjaThreads.ApprenticeChallenge
19:20:48 Presenting theory JinjaThreads.BufferExample
19:20:48 Presenting theory JinjaThreads.Examples_Main
19:20:49 Presenting theory JinjaThreads.JinjaThreads
19:20:52 Presenting Iptables_Semantics_Examples_Big ...
19:20:52 Presenting document Iptables_Semantics_Examples_Big/document
19:20:52 Presenting document Iptables_Semantics_Examples_Big/outline
19:20:52 Presenting theory Iptables_Semantics_Examples_Big.Analyze_topos_generated
19:20:52 Presenting theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small
19:20:52 Presenting theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall
19:20:52 Presenting theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3
19:20:52 Presenting theory Iptables_Semantics_Examples_Big.Analyze_Containern
19:20:52 Presenting theory Iptables_Semantics_Examples_Big.TUM_Simple_FW
19:20:52 Presenting theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large
19:20:54 
19:20:54 === TIMING ===
19:20:54 
19:20:54 Group slow: 9:23:34 elapsed time, 29:59:38 cpu time, factor 3.19
19:20:54 Group AFP: 9:51:03 elapsed time, 31:41:48 cpu time, factor 3.22
19:20:54 Group main: 0:07:46 elapsed time, 0:28:56 cpu time, factor 3.72
19:20:54 Group timing: 0:03:00 elapsed time, 0:14:31 cpu time, factor 4.83
19:20:54 Group very_slow: 6:06:44 elapsed time, 15:05:02 cpu time, factor 2.47
19:20:54 Overall: 10:13:22 elapsed time, 32:11:07 cpu time, factor 3.15
19:20:59 Archiving artifacts
19:21:08 Started calculate disk usage of build
19:21:08 Finished Calculation of disk usage of build in 0 seconds
19:21:11 Started calculate disk usage of workspace
19:21:12 Finished Calculation of disk usage of workspace in 0 seconds
19:21:12 No emails were triggered.
19:21:12 Finished: SUCCESS