Skip to content
Success

Console Output

22:55:37 Started by upstream project "isabelle-repo" build number 652

22:55:37 originally caused by:

22:55:37 Started by an SCM change

22:55:37 [EnvInject] - Loading node environment variables.

22:55:37 Building remotely on workermta4 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-repo-makeall

22:55:37 [isabelle-repo-makeall] $ hg showconfig paths.default

22:55:37 [isabelle-repo-makeall] $ hg pull --rev 135313951082b88699631362d13c7338923e8ab4

22:55:38 pulling from http://isabelle.in.tum.de/repos/isabelle/

22:55:38 searching for changes

22:55:38 adding changesets

22:55:38 adding manifests

22:55:38 adding file changes

22:55:38 added 1 changesets with 2 changes to 2 files

22:55:38 (run 'hg update' to get a working copy)

22:55:38 [isabelle-repo-makeall] $ hg update --clean --rev 135313951082b88699631362d13c7338923e8ab4

22:55:39 2 files updated, 0 files merged, 0 files removed, 0 files unresolved

22:55:39 [isabelle-repo-makeall] $ hg log --rev . --template {node}

22:55:39 [isabelle-repo-makeall] $ hg log --rev . --template {rev}

22:55:39 [isabelle-repo-makeall] $ hg id --branch

22:55:39 No emails were triggered.

22:55:39 [isabelle-repo-makeall] $ /bin/sh -xe /tmp/hudson7121080965356332908.sh

22:55:39 + Admin/jenkins/run_build makeall

22:55:39 + set -e

22:55:39 + PROFILE=makeall

22:55:39 + shift

22:55:39 + bin/isabelle components -a

22:55:39 + bin/isabelle jedit -bf

22:55:39 ### Building Isabelle/Scala ...

22:57:50 ### Building Isabelle/jEdit ...

22:58:16 + bin/isabelle ci_build_makeall

22:58:21

22:58:21 === CONFIGURATION ===

22:58:21

22:58:21 ISABELLE_BUILD_OPTIONS=""

22:58:21

22:58:21 ML_PLATFORM="x86_64-linux"

22:58:21 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"

22:58:21 ML_SYSTEM="polyml-5.6"

22:58:21 ML_OPTIONS="-H 4000 --maxheap 8G"

22:58:21

22:58:21 === BUILD ===

22:58:21

22:58:21 Build started at Wed, 28 Dec 2016 21:58:21 GMT

22:58:21 Isabelle id 135313951082

22:58:21

22:58:21 === LOG ===

22:58:21

22:58:21 Session Pure/Pure

22:58:22 Session CCL/CCL

22:58:22 Session CTT/CTT

22:58:22 Session Cube/Cube

22:58:22 Session FOL/FOL

22:58:22 Session FOL/FOL-ex

22:58:22 Session FOLP/FOLP

22:58:22 Session FOLP/FOLP-ex

22:58:22 Session HOL/HOL (main)

22:58:23 Session Doc/Classes (doc)

22:58:23 Session Doc/Codegen_Basics

22:58:23 Session Doc/Codegen (doc)

22:58:23 Session Doc/Corec (doc)

22:58:23 Session Doc/Datatypes (doc)

22:58:23 Session Doc/Functions (doc)

22:58:23 Session HOL/HOL-Algebra (main timing)

22:58:23 Session HOL/HOL-Analysis (main timing)

22:58:23 Session HOL/HOL-Analysis-ex

22:58:23 Session HOL/HOL-Probability (timing)

22:58:23 Session HOL/HOL-Probability-ex (timing)

22:58:23 Session HOL/HOL-Auth (timing)

22:58:23 Session HOL/HOL-UNITY (timing)

22:58:24 Session HOL/HOL-Bali (timing)

22:58:24 Session HOL/HOL-Cardinals (timing)

22:58:24 Session HOL/HOL-Corec_Examples (timing)

22:58:24 Session HOL/HOL-Data_Structures (timing)

22:58:24 Session HOL/HOL-Datatype_Examples (timing)

22:58:24 Session HOL/HOL-Decision_Procs (timing)

22:58:24 Session HOL/HOL-Eisbach

22:58:24 Session Doc/Eisbach (doc)

22:58:24 Session HOL/HOL-Hahn_Banach

22:58:24 Session HOL/HOL-Hoare

22:58:24 Session HOL/HOL-Hoare_Parallel (timing)

22:58:24 Session HOL/HOL-IMP (timing)

22:58:24 Session HOL/HOL-IMPP

22:58:24 Session HOL/HOL-IOA

22:58:24 Session HOL/HOL-Imperative_HOL

22:58:25 Session HOL/HOL-Import

22:58:25 Session HOL/HOL-Induct

22:58:25 Session HOL/HOL-Isar_Examples

22:58:25 Session HOL/HOL-Lattice

22:58:25 Session HOL/HOL-Library (main timing)

22:58:25 Session HOL/HOL-Codegenerator_Test

22:58:25 Session HOL/HOL-Matrix_LP

22:58:25 Session HOL/HOL-Metis_Examples (timing)

22:58:25 Session HOL/HOL-MicroJava (timing)

22:58:25 Session HOL/HOL-Mirabelle

22:58:25 Session HOL/HOL-Mirabelle-ex

22:58:25 Session HOL/HOL-Mutabelle

22:58:25 Session HOL/HOL-NanoJava

22:58:25 Session HOL/HOL-Nitpick_Examples

22:58:25 Session HOL/HOL-Nominal

22:58:25 Session HOL/HOL-Nominal-Examples (timing)

22:58:26 Session HOL/HOL-Nonstandard_Analysis (timing)

22:58:26 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)

22:58:26 Session HOL/HOL-Number_Theory (timing)

22:58:26 Session HOL/HOL-Nunchaku

22:58:26 Session HOL/HOL-Predicate_Compile_Examples (timing)

22:58:26 Session HOL/HOL-Prolog

22:58:26 Session HOL/HOL-Quickcheck_Examples (timing)

22:58:26 Session HOL/HOL-Quotient_Examples (timing)

22:58:26 Session HOL/HOL-SET_Protocol (timing)

22:58:26 Session HOL/HOL-Statespace

22:58:26 Session HOL/HOL-TLA

22:58:26 Session HOL/HOL-TLA-Buffer

22:58:26 Session HOL/HOL-TLA-Inc

22:58:26 Session HOL/HOL-TLA-Memory

22:58:26 Session HOL/HOL-TPTP

22:58:26 Session HOL/HOL-Types_To_Sets

22:58:26 Session HOL/HOL-Unix

22:58:26 Session HOL/HOL-Word (main timing)

22:58:27 Session HOL/HOL-SPARK (main)

22:58:27 Session HOL/HOL-SPARK-Examples

22:58:27 Session HOL/HOL-SPARK-Manual

22:58:27 Session HOL/HOL-Word-Examples

22:58:27 Session HOL/HOL-Word-SMT_Examples (timing)

22:58:27 Session HOL/HOL-ZF

22:58:27 Session HOL/HOL-ex

22:58:27 Session HOL/HOLCF (main timing)

22:58:27 Session HOL/HOLCF-FOCUS

22:58:27 Session HOL/HOLCF-IMP

22:58:27 Session HOL/HOLCF-Library

22:58:27 Session HOL/HOLCF-Tutorial

22:58:27 Session HOL/HOLCF-ex

22:58:27 Session HOL/IOA (timing)

22:58:27 Session HOL/IOA-ABP

22:58:27 Session HOL/IOA-NTP

22:58:27 Session HOL/IOA-Storage

22:58:27 Session HOL/IOA-ex

22:58:27 Session Doc/How_to_Prove_it

22:58:27 Session Doc/Implementation (doc)

22:58:27 Session Doc/Isar_Ref (doc)

22:58:27 Session Doc/JEdit (doc)

22:58:27 Session Doc/Locales (doc)

22:58:27 Session Doc/Main (doc)

22:58:27 Session Doc/Prog_Prove (doc)

22:58:27 Session Doc/Sugar (doc)

22:58:27 Session Doc/Tutorial (doc)

22:58:27 Session Doc/Typeclass_Hierarchy_Basics

22:58:27 Session Doc/Typeclass_Hierarchy (doc)

22:58:27 Session HOL/HOL-Proofs (timing)

22:58:28 Session HOL/HOL-Proofs-Extraction (timing)

22:58:28 Session HOL/HOL-Proofs-Lambda (timing)

22:58:28 Session HOL/HOL-Proofs-ex

22:58:28 Session Doc/Intro (doc)

22:58:28 Session LCF/LCF

22:58:28 Session Doc/Logics (doc)

22:58:28 Session Doc/Nitpick (doc)

22:58:28 Session Unsorted/SML

22:58:28 Session Sequents/Sequents

22:58:28 Session Doc/Sledgehammer (doc)

22:58:28 Session Unsorted/Spec_Check

22:58:28 Session Doc/System (doc)

22:58:28 Session ZF/ZF (main timing ZF)

22:58:28 Session Doc/Logics_ZF (doc)

22:58:28 Session ZF/ZF-AC (ZF)

22:58:28 Session ZF/ZF-Coind (ZF)

22:58:28 Session ZF/ZF-Constructible (ZF)

22:58:28 Session ZF/ZF-IMP (ZF)

22:58:28 Session ZF/ZF-Induct (ZF)

22:58:28 Session ZF/ZF-Resid (ZF)

22:58:28 Session ZF/ZF-UNITY (timing ZF)

22:58:28 Session ZF/ZF-ex (ZF)

22:58:30 Cleaning Pure ...

22:58:30 Cleaning SML ...

22:58:30 Cleaning Sequents ...

22:58:30 Cleaning Sledgehammer ...

22:58:30 Cleaning Spec_Check ...

22:58:30 Cleaning System ...

22:58:30 Cleaning ZF ...

22:58:30 Cleaning ZF-AC ...

22:58:30 Cleaning ZF-Coind ...

22:58:30 Cleaning ZF-Constructible ...

22:58:30 Cleaning ZF-IMP ...

22:58:30 Cleaning ZF-Induct ...

22:58:30 Cleaning ZF-Resid ...

22:58:30 Cleaning ZF-UNITY ...

22:58:30 Cleaning ZF-ex ...

22:58:30 Cleaning Nitpick ...

22:58:30 Cleaning Logics_ZF ...

22:58:30 Cleaning Logics ...

22:58:30 Cleaning LCF ...

22:58:30 Cleaning Intro ...

22:58:30 Cleaning HOL-Proofs ...

22:58:30 Cleaning HOL-Proofs-Extraction ...

22:58:30 Cleaning HOL-Proofs-Lambda ...

22:58:30 Cleaning HOL-Proofs-ex ...

22:58:30 Cleaning HOL ...

22:58:30 Cleaning HOL-Algebra ...

22:58:30 Cleaning HOL-Analysis ...

22:58:30 Cleaning HOL-Analysis-ex ...

22:58:30 Cleaning HOL-Probability ...

22:58:30 Cleaning HOL-Probability-ex ...

22:58:30 Cleaning HOL-Auth ...

22:58:30 Cleaning HOL-UNITY ...

22:58:30 Cleaning HOL-Bali ...

22:58:30 Cleaning HOL-Cardinals ...

22:58:30 Cleaning HOL-Corec_Examples ...

22:58:30 Cleaning HOL-Data_Structures ...

22:58:30 Cleaning HOL-Datatype_Examples ...

22:58:30 Cleaning HOL-Decision_Procs ...

22:58:30 Cleaning HOL-Eisbach ...

22:58:30 Cleaning HOL-Hahn_Banach ...

22:58:30 Cleaning HOL-Hoare ...

22:58:30 Cleaning HOL-Hoare_Parallel ...

22:58:30 Cleaning HOL-IMP ...

22:58:30 Cleaning HOL-IMPP ...

22:58:30 Cleaning HOL-IOA ...

22:58:30 Cleaning HOL-Imperative_HOL ...

22:58:30 Cleaning HOL-Import ...

22:58:30 Cleaning HOL-Induct ...

22:58:30 Cleaning HOL-Isar_Examples ...

22:58:30 Cleaning HOL-Lattice ...

22:58:30 Cleaning HOL-Library ...

22:58:30 Cleaning HOL-Codegenerator_Test ...

22:58:30 Cleaning HOL-Matrix_LP ...

22:58:30 Cleaning HOL-Metis_Examples ...

22:58:30 Cleaning HOL-MicroJava ...

22:58:30 Cleaning HOL-Mirabelle ...

22:58:30 Cleaning HOL-Mirabelle-ex ...

22:58:30 Cleaning HOL-Mutabelle ...

22:58:30 Cleaning HOL-NanoJava ...

22:58:30 Cleaning HOL-Nitpick_Examples ...

22:58:30 Cleaning HOL-Nominal ...

22:58:30 Cleaning HOL-Nominal-Examples ...

22:58:30 Cleaning HOL-Nonstandard_Analysis ...

22:58:30 Cleaning HOL-Nonstandard_Analysis-Examples ...

22:58:30 Cleaning HOL-Number_Theory ...

22:58:30 Cleaning HOL-Nunchaku ...

22:58:30 Cleaning HOL-Predicate_Compile_Examples ...

22:58:30 Cleaning HOL-Prolog ...

22:58:30 Cleaning HOL-Quickcheck_Examples ...

22:58:30 Cleaning HOL-Quotient_Examples ...

22:58:30 Cleaning HOL-SET_Protocol ...

22:58:30 Cleaning HOL-Statespace ...

22:58:30 Cleaning HOL-TLA ...

22:58:30 Cleaning HOL-TLA-Buffer ...

22:58:30 Cleaning HOL-TLA-Inc ...

22:58:30 Cleaning HOL-TLA-Memory ...

22:58:30 Cleaning HOL-TPTP ...

22:58:30 Cleaning HOL-Types_To_Sets ...

22:58:30 Cleaning HOL-Unix ...

22:58:30 Cleaning HOL-Word ...

22:58:30 Cleaning HOL-SPARK ...

22:58:30 Cleaning HOL-SPARK-Examples ...

22:58:30 Cleaning HOL-SPARK-Manual ...

22:58:30 Cleaning HOL-Word-Examples ...

22:58:30 Cleaning HOL-Word-SMT_Examples ...

22:58:30 Cleaning HOL-ZF ...

22:58:30 Cleaning HOL-ex ...

22:58:30 Cleaning HOLCF ...

22:58:30 Cleaning HOLCF-FOCUS ...

22:58:30 Cleaning HOLCF-IMP ...

22:58:30 Cleaning HOLCF-Library ...

22:58:30 Cleaning HOLCF-Tutorial ...

22:58:30 Cleaning HOLCF-ex ...

22:58:30 Cleaning IOA ...

22:58:30 Cleaning IOA-ABP ...

22:58:30 Cleaning IOA-NTP ...

22:58:30 Cleaning IOA-Storage ...

22:58:30 Cleaning IOA-ex ...

22:58:30 Cleaning How_to_Prove_it ...

22:58:30 Cleaning Implementation ...

22:58:30 Cleaning Isar_Ref ...

22:58:30 Cleaning JEdit ...

22:58:30 Cleaning Locales ...

22:58:30 Cleaning Main ...

22:58:30 Cleaning Prog_Prove ...

22:58:30 Cleaning Sugar ...

22:58:30 Cleaning Tutorial ...

22:58:30 Cleaning Typeclass_Hierarchy_Basics ...

22:58:30 Cleaning Typeclass_Hierarchy ...

22:58:30 Cleaning Functions ...

22:58:30 Cleaning FOLP ...

22:58:30 Cleaning FOLP-ex ...

22:58:30 Cleaning FOL ...

22:58:30 Cleaning FOL-ex ...

22:58:30 Cleaning Eisbach ...

22:58:30 Cleaning Datatypes ...

22:58:30 Cleaning Cube ...

22:58:30 Cleaning Corec ...

22:58:30 Cleaning Codegen_Basics ...

22:58:30 Cleaning Codegen ...

22:58:30 Cleaning Classes ...

22:58:30 Cleaning CTT ...

22:58:30 Cleaning CCL ...

22:58:30 Building Pure ...

22:58:41 Pure: theory Pure

22:58:41 Pure: theory ML_Bootstrap

22:58:44 Warning: missing document directory

22:58:44 Timing Pure (1 threads, 0.487s elapsed time, 0.488s cpu time, 0.000s GC time, factor 1.00)

22:58:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Pure/Pure

22:58:44 Finished Pure (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.99)

22:58:44 Building HOL ...

22:58:44 Building ZF ...

22:58:44 Building HOL-Proofs ...

22:58:44 ZF: theory IFOL

22:58:44 HOL-Proofs: theory Proofs

22:58:45 HOL-Proofs: theory Code_Generator

22:58:45 HOL: theory Code_Generator

22:58:45 ZF: theory FOL

22:58:47 ZF: theory ZF

22:58:47 ZF: theory upair

22:58:47 HOL-Proofs: theory HOL

22:58:47 ZF: theory pair

22:58:47 HOL: theory HOL

22:58:47 ZF: theory Bool

22:58:47 ZF: theory equalities

22:58:48 ZF: theory Fixedpt

22:58:48 ZF: theory Sum

22:58:48 ZF: theory func

22:58:48 ZF: theory Perm

22:58:48 ZF: theory QPair

22:58:49 ZF: theory Trancl

22:58:49 ZF: theory EquivClass

22:58:49 ZF: theory WF

22:58:49 ZF: theory Order

22:58:49 ZF: theory Ordinal

22:58:49 ZF: theory OrdQuant

22:58:49 ZF: theory OrderArith

22:58:50 ZF: theory Nat_ZF

22:58:50 ZF: theory Epsilon

22:58:50 ZF: theory OrderType

22:58:50 ZF: theory Inductive_ZF

22:58:50 ZF: theory Finite

22:58:50 ZF: theory Cardinal

22:58:50 HOL: theory Argo

22:58:51 HOL: theory Ctr_Sugar

22:58:51 ZF: theory Univ

22:58:51 HOL-Proofs: theory Argo

22:58:51 HOL-Proofs: theory Ctr_Sugar

22:58:51 ZF: theory Arith

22:58:51 ZF: theory QUniv

22:58:51 HOL: theory Orderings

22:58:51 ZF: theory Datatype_ZF

22:58:51 ZF: theory ArithSimp

22:58:52 ZF: theory Int_ZF

22:58:52 ZF: theory CardinalArith

22:58:52 HOL: theory SAT

22:58:52 HOL-Proofs: theory Orderings

22:58:52 ZF: theory List_ZF

22:58:52 ZF: theory Bin

22:58:52 HOL-Proofs: theory SAT

22:58:53 HOL: theory Groups

22:58:53 ZF: theory IntDiv_ZF

22:58:53 ZF: theory Main_ZF

22:58:53 ZF: theory AC

22:58:53 ZF: theory Zorn

22:58:54 ZF: theory Cardinal_AC

22:58:54 ZF: theory InfDatatype

22:58:54 ZF: theory Main

22:58:54 ZF: theory Main_ZFC

22:58:54 HOL-Proofs: theory Groups

22:58:55 HOL: theory Lattices

22:58:56 HOL: theory Set

22:58:57 HOL-Proofs: theory Lattices

22:58:58 HOL: theory Fun

22:58:58 HOL: theory Typedef

22:58:58 HOL: theory Rings

22:58:58 HOL: theory Complete_Lattices

22:59:01 HOL: theory Inductive

22:59:01 HOL-Proofs: theory Set

22:59:02 HOL: theory Product_Type

22:59:03 HOL: theory Complete_Partial_Order

22:59:04 HOL: theory Sum_Type

22:59:05 HOL-Proofs: theory Fun

22:59:06 HOL-Proofs: theory Typedef

22:59:06 HOL-Proofs: theory Rings

22:59:07 HOL: theory Nat

22:59:07 HOL-Proofs: theory Complete_Lattices

22:59:09 HOL: theory Fields

22:59:09 HOL: theory Meson

22:59:09 HOL: theory ATP

22:59:11 HOL: theory Metis

22:59:11 HOL-Proofs: theory Inductive

22:59:13 HOL: theory Finite_Set

22:59:13 HOL-Proofs: theory Product_Type

22:59:14 HOL: theory Relation

22:59:15 HOL-Proofs: theory Complete_Partial_Order

22:59:15 HOL: theory Transitive_Closure

22:59:16 HOL-Proofs: theory Sum_Type

22:59:16 HOL: theory Wellfounded

22:59:17 HOL: theory Fun_Def_Base

22:59:17 HOL: theory Hilbert_Choice

22:59:17 HOL: theory Wfrec

22:59:17 HOL: theory Order_Relation

22:59:17 HOL: theory BNF_Wellorder_Relation

22:59:17 HOL: theory Zorn

22:59:17 Timing ZF (2 threads, 21.489s elapsed time, 35.036s cpu time, 4.408s GC time, factor 1.63)

22:59:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF

22:59:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/document.pdf

22:59:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/outline.pdf

22:59:17 Finished ZF (0:00:33 elapsed time, 0:00:54 cpu time, factor 1.63)

22:59:17 HOL: theory BNF_Wellorder_Embedding

22:59:18 Building FOL ...

22:59:18 FOL: theory IFOL

22:59:18 HOL: theory BNF_Wellorder_Constructions

22:59:18 HOL: theory BNF_Cardinal_Order_Relation

22:59:19 FOL: theory FOL

22:59:19 HOL-Proofs: theory Nat

22:59:19 HOL: theory BNF_Cardinal_Arithmetic

22:59:20 HOL: theory BNF_Def

22:59:21 HOL: theory BNF_Composition

22:59:21 HOL: theory Basic_BNFs

22:59:22 HOL: theory BNF_Fixpoint_Base

22:59:23 HOL-Proofs: theory Fields

22:59:23 HOL-Proofs: theory Meson

22:59:23 Timing FOL (2 threads, 2.364s elapsed time, 2.676s cpu time, 0.144s GC time, factor 1.13)

22:59:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL

22:59:23 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/document.pdf

22:59:23 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/outline.pdf

22:59:23 Finished FOL (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.26)

22:59:23 Building FOLP ...

22:59:23 FOLP: theory IFOLP

22:59:23 HOL-Proofs: theory ATP

22:59:23 FOLP: theory FOLP

22:59:24 HOL: theory BNF_Least_Fixpoint

22:59:25 Timing FOLP (2 threads, 0.817s elapsed time, 0.824s cpu time, 0.000s GC time, factor 1.01)

22:59:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP

22:59:25 Finished FOLP (0:00:01 elapsed time)

22:59:25 Running ZF-UNITY ...

22:59:25 ZF-UNITY: theory FoldSet

22:59:25 ZF-UNITY: theory Acc

22:59:25 HOL-Proofs: theory Metis

22:59:25 ZF-UNITY: theory GenPrefix

22:59:25 ZF-UNITY: theory Multiset

22:59:26 ZF-UNITY: theory State

22:59:26 ZF-UNITY: theory UNITY

22:59:26 ZF-UNITY: theory MultisetSum

22:59:26 ZF-UNITY: theory Constrains

22:59:26 ZF-UNITY: theory Monotonicity

22:59:26 HOL: theory Basic_BNF_LFPs

22:59:26 ZF-UNITY: theory FP

22:59:26 ZF-UNITY: theory Increasing

22:59:26 ZF-UNITY: theory WFair

22:59:26 HOL: theory Transfer

22:59:27 ZF-UNITY: theory SubstAx

22:59:27 ZF-UNITY: theory Follows

22:59:27 ZF-UNITY: theory Mutex

22:59:27 ZF-UNITY: theory Union

22:59:28 HOL: theory Num

22:59:28 ZF-UNITY: theory Comp

22:59:28 ZF-UNITY: theory Guar

22:59:28 ZF-UNITY: theory AllocBase

22:59:29 ZF-UNITY: theory ClientImpl

22:59:29 ZF-UNITY: theory Distributor

22:59:29 ZF-UNITY: theory Merge

22:59:29 ZF-UNITY: theory AllocImpl

22:59:29 HOL-Proofs: theory Finite_Set

22:59:30 HOL: theory Power

22:59:32 HOL: theory Groups_Big

22:59:34 HOL: theory Equiv_Relations

22:59:35 HOL: theory Lifting

22:59:36 HOL: theory Lifting_Set

22:59:36 HOL: theory Option

22:59:36 HOL-Proofs: theory Relation

22:59:36 HOL: theory Quotient

22:59:36 HOL: theory Extraction

22:59:37 HOL: theory Lattices_Big

22:59:38 HOL: theory Partial_Function

22:59:39 HOL-Proofs: theory Transitive_Closure

22:59:39 HOL: theory Fun_Def

22:59:40 HOL: theory Int

22:59:42 HOL: theory Nat_Transfer

22:59:42 HOL-Proofs: theory Wellfounded

22:59:43 HOL: theory Parity

22:59:44 Timing ZF-UNITY (2 threads, 18.106s elapsed time, 31.628s cpu time, 1.144s GC time, factor 1.75)

22:59:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-UNITY

22:59:44 Finished ZF-UNITY (0:00:18 elapsed time, 0:00:32 cpu time, factor 1.72)

22:59:44 Running ZF-Constructible ...

22:59:44 ZF-Constructible: theory Formula

22:59:44 ZF-Constructible: theory MetaExists

22:59:44 ZF-Constructible: theory Normal

22:59:44 HOL: theory Divides

22:59:44 ZF-Constructible: theory Reflection

22:59:45 HOL-Proofs: theory Fun_Def_Base

22:59:45 ZF-Constructible: theory Relative

22:59:45 HOL-Proofs: theory Hilbert_Choice

22:59:46 ZF-Constructible: theory L_axioms

22:59:46 ZF-Constructible: theory Wellorderings

22:59:47 ZF-Constructible: theory WFrec

22:59:47 HOL-Proofs: theory Wfrec

22:59:47 HOL-Proofs: theory Order_Relation

22:59:47 ZF-Constructible: theory WF_absolute

22:59:48 ZF-Constructible: theory Datatype_absolute

22:59:48 ZF-Constructible: theory Rank

22:59:48 HOL-Proofs: theory BNF_Wellorder_Relation

22:59:48 HOL-Proofs: theory Zorn

22:59:49 ZF-Constructible: theory Separation

22:59:49 ZF-Constructible: theory Internalize

22:59:49 HOL-Proofs: theory BNF_Wellorder_Embedding

22:59:49 ZF-Constructible: theory AC_in_L

22:59:50 HOL: theory Code_Numeral

22:59:50 HOL: theory Numeral_Simprocs

22:59:50 ZF-Constructible: theory Rec_Separation

22:59:51 ZF-Constructible: theory Rank_Separation

22:59:51 ZF-Constructible: theory Satisfies_absolute

22:59:51 HOL-Proofs: theory BNF_Wellorder_Constructions

22:59:51 HOL: theory SMT

22:59:51 HOL: theory Semiring_Normalization

22:59:52 ZF-Constructible: theory DPow_absolute

22:59:53 HOL: theory Set_Interval

22:59:53 HOL: theory Groebner_Basis

22:59:55 HOL: theory Conditionally_Complete_Lattices

22:59:55 HOL: theory Filter

22:59:56 HOL-Proofs: theory BNF_Cardinal_Order_Relation

22:59:56 HOL: theory Presburger

22:59:58 HOL: theory Sledgehammer

23:00:00 HOL-Proofs: theory BNF_Cardinal_Arithmetic

23:00:00 HOL: theory List

23:00:01 HOL-Proofs: theory BNF_Def

23:00:03 Timing ZF-Constructible (2 threads, 14.591s elapsed time, 27.240s cpu time, 4.912s GC time, factor 1.87)

23:00:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible

23:00:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/document.pdf

23:00:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/outline.pdf

23:00:03 Finished ZF-Constructible (0:00:18 elapsed time, 0:00:33 cpu time, factor 1.82)

23:00:03 Running ZF-ex ...

23:00:03 ZF-ex: theory BinEx

23:00:03 ZF-ex: theory CoUnit

23:00:03 ZF-ex: theory Commutation

23:00:03 ZF-ex: theory Group

23:00:03 ZF-ex: theory LList

23:00:03 ZF-ex: theory Limit

23:00:04 ZF-ex: theory Ring

23:00:05 ZF-ex: theory NatSum

23:00:05 ZF-ex: theory Primes

23:00:05 ZF-ex: theory Ramsey

23:00:05 ZF-ex: theory misc

23:00:07 HOL: theory Groups_List

23:00:07 HOL-Proofs: theory BNF_Composition

23:00:07 HOL-Proofs: theory Basic_BNFs

23:00:07 HOL: theory Map

23:00:07 HOL: theory Random

23:00:08 HOL: theory Enum

23:00:08 HOL-Proofs: theory BNF_Fixpoint_Base

23:00:10 HOL: theory String

23:00:11 HOL: theory BNF_Greatest_Fixpoint

23:00:11 HOL: theory Predicate

23:00:11 HOL-Proofs: theory BNF_Least_Fixpoint

23:00:12 HOL: theory Lazy_Sequence

23:00:12 HOL: theory Limited_Sequence

23:00:13 HOL: theory Typerep

23:00:14 HOL-Proofs: theory Basic_BNF_LFPs

23:00:14 HOL: theory Code_Evaluation

23:00:14 HOL-Proofs: theory Transfer

23:00:14 Timing ZF-ex (2 threads, 10.398s elapsed time, 14.728s cpu time, 0.724s GC time, factor 1.42)

23:00:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-ex

23:00:14 Finished ZF-ex (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.39)

23:00:14 Running ZF-Induct ...

23:00:14 ZF-Induct: theory Binary_Trees

23:00:14 ZF-Induct: theory Acc

23:00:14 ZF-Induct: theory Comb

23:00:14 ZF-Induct: theory Datatypes

23:00:14 ZF-Induct: theory FoldSet

23:00:15 ZF-Induct: theory ListN

23:00:15 ZF-Induct: theory Mutil

23:00:15 ZF-Induct: theory Multiset

23:00:15 ZF-Induct: theory Ntree

23:00:15 ZF-Induct: theory Primrec

23:00:15 HOL: theory Quickcheck_Random

23:00:15 ZF-Induct: theory PropLog

23:00:15 ZF-Induct: theory Rmap

23:00:15 ZF-Induct: theory Term

23:00:15 ZF-Induct: theory Tree_Forest

23:00:16 ZF-Induct: theory Brouwer

23:00:16 HOL-Proofs: theory Num

23:00:17 HOL: theory Quickcheck_Exhaustive

23:00:17 HOL: theory Quickcheck_Narrowing

23:00:20 HOL-Proofs: theory Power

23:00:20 HOL: theory Random_Pred

23:00:21 HOL: theory Record

23:00:21 HOL: theory Random_Sequence

23:00:21 HOL: theory Predicate_Compile

23:00:22 HOL: theory Nitpick

23:00:23 HOL-Proofs: theory Groups_Big

23:00:24 Timing ZF-Induct (2 threads, 6.398s elapsed time, 10.332s cpu time, 0.376s GC time, factor 1.61)

23:00:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct

23:00:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/document.pdf

23:00:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/outline.pdf

23:00:24 Finished ZF-Induct (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.57)

23:00:24 Running ZF-AC ...

23:00:24 ZF-AC: theory AC_Equiv

23:00:24 ZF-AC: theory AC18_AC19

23:00:24 ZF-AC: theory AC7_AC9

23:00:24 ZF-AC: theory Cardinal_aux

23:00:24 ZF-AC: theory Hartog

23:00:24 ZF-AC: theory HH

23:00:24 ZF-AC: theory WO6_WO1

23:00:24 ZF-AC: theory AC16_lemmas

23:00:24 ZF-AC: theory AC16_WO4

23:00:24 ZF-AC: theory DC

23:00:25 ZF-AC: theory AC15_WO6

23:00:25 ZF-AC: theory AC17_AC1

23:00:25 ZF-AC: theory WO1_AC

23:00:25 ZF-AC: theory WO1_WO7

23:00:25 ZF-AC: theory WO2_AC16

23:00:27 HOL: theory Main

23:00:28 HOL: theory Archimedean_Field

23:00:28 HOL: theory Binomial

23:00:29 HOL: theory GCD

23:00:29 HOL-Proofs: theory Equiv_Relations

23:00:32 Timing ZF-AC (2 threads, 5.460s elapsed time, 9.232s cpu time, 0.464s GC time, factor 1.69)

23:00:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC

23:00:32 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/document.pdf

23:00:32 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/outline.pdf

23:00:32 Finished ZF-AC (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.60)

23:00:32 Running FOL-ex ...

23:00:32 FOL-ex: theory If

23:00:32 FOL-ex: theory Classical

23:00:32 FOL-ex: theory Intro

23:00:32 FOL-ex: theory Miniscope

23:00:32 FOL-ex: theory Nat

23:00:32 FOL-ex: theory Nat_Class

23:00:32 FOL-ex: theory Natural_Numbers

23:00:32 FOL-ex: theory Prolog

23:00:32 FOL-ex: theory Propositional_Cla

23:00:32 FOL-ex: theory Quantifiers_Cla

23:00:32 FOL-ex: theory Foundation

23:00:32 FOL-ex: theory Intuitionistic

23:00:32 FOL-ex: theory Propositional_Int

23:00:32 FOL-ex: theory Quantifiers_Int

23:00:32 HOL: theory Topological_Spaces

23:00:34 HOL: theory Rat

23:00:34 FOL-ex: theory Locale_Test1

23:00:35 HOL-Proofs: theory Lifting

23:00:36 HOL: theory Real

23:00:37 FOL-ex: theory Locale_Test2

23:00:37 FOL-ex: theory Locale_Test3

23:00:37 FOL-ex: theory Locale_Test

23:00:38 HOL-Proofs: theory Lifting_Set

23:00:39 HOL: theory Real_Vector_Spaces

23:00:39 Timing FOL-ex (2 threads, 5.220s elapsed time, 7.216s cpu time, 0.176s GC time, factor 1.38)

23:00:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex

23:00:39 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/document.pdf

23:00:39 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/outline.pdf

23:00:39 Finished FOL-ex (0:00:07 elapsed time, 0:00:10 cpu time, factor 1.40)

23:00:39 Running CCL ...

23:00:39 HOL-Proofs: theory Option

23:00:39 CCL: theory IFOL

23:00:39 HOL-Proofs: theory Quotient

23:00:40 CCL: theory FOL

23:00:40 HOL-Proofs: theory Extraction

23:00:42 CCL: theory Set

23:00:42 HOL-Proofs: theory Lattices_Big

23:00:42 CCL: theory Lfp

23:00:42 CCL: theory Gfp

23:00:42 CCL: theory CCL

23:00:42 CCL: theory Term

23:00:42 CCL: theory Trancl

23:00:42 CCL: theory Type

23:00:43 CCL: theory Fix

23:00:43 CCL: theory Hered

23:00:43 CCL: theory Wfd

23:00:43 HOL-Proofs: theory Partial_Function

23:00:43 CCL: theory Nat

23:00:43 CCL: theory List

23:00:44 CCL: theory Flag

23:00:44 CCL: theory Stream

23:00:44 Timing CCL (2 threads, 4.542s elapsed time, 6.660s cpu time, 0.160s GC time, factor 1.47)

23:00:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CCL/CCL

23:00:44 Finished CCL (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.41)

23:00:44 Running Sequents ...

23:00:44 Sequents: theory Sequents

23:00:44 Sequents: theory ILL

23:00:45 Sequents: theory LK0

23:00:45 Sequents: theory ILL_predlog

23:00:45 Sequents: theory Washing

23:00:45 Sequents: theory LK

23:00:45 Sequents: theory Modal0

23:00:45 Sequents: theory S4

23:00:45 Sequents: theory S43

23:00:45 Sequents: theory Hard_Quantifiers

23:00:45 Sequents: theory Nat

23:00:45 Sequents: theory Propositional

23:00:45 Sequents: theory Quantifiers

23:00:45 Sequents: theory T

23:00:45 HOL-Proofs: theory Fun_Def

23:00:47 HOL-Proofs: theory Int

23:00:48 Timing Sequents (2 threads, 3.393s elapsed time, 6.516s cpu time, 0.116s GC time, factor 1.92)

23:00:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Sequents/Sequents

23:00:48 Finished Sequents (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.81)

23:00:48 Running FOLP-ex ...

23:00:48 FOLP-ex: theory Classical

23:00:48 FOLP-ex: theory If

23:00:49 FOLP-ex: theory Intro

23:00:49 FOLP-ex: theory Nat

23:00:49 FOLP-ex: theory Propositional_Cla

23:00:49 FOLP-ex: theory Quantifiers_Cla

23:00:49 FOLP-ex: theory Foundation

23:00:49 FOLP-ex: theory Intuitionistic

23:00:49 HOL: theory Inequalities

23:00:50 HOL: theory Limits

23:00:50 FOLP-ex: theory Propositional_Int

23:00:51 FOLP-ex: theory Quantifiers_Int

23:00:51 HOL-Proofs: theory Nat_Transfer

23:00:52 Timing FOLP-ex (2 threads, 3.282s elapsed time, 5.604s cpu time, 0.076s GC time, factor 1.71)

23:00:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP-ex

23:00:52 Finished FOLP-ex (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.61)

23:00:52 Running LCF ...

23:00:52 LCF: theory IFOL

23:00:52 HOL: theory Deriv

23:00:53 HOL-Proofs: theory Parity

23:00:53 HOL: theory Series

23:00:53 LCF: theory FOL

23:00:54 HOL: theory NthRoot

23:00:55 LCF: theory LCF

23:00:55 LCF: theory Ex1

23:00:55 LCF: theory Ex2

23:00:55 LCF: theory Ex3

23:00:55 LCF: theory Ex4

23:00:55 HOL: theory Transcendental

23:00:55 HOL-Proofs: theory Divides

23:00:55 Timing LCF (2 threads, 2.410s elapsed time, 2.828s cpu time, 0.136s GC time, factor 1.17)

23:00:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/LCF/LCF

23:00:55 Finished LCF (0:00:02 elapsed time, 0:00:03 cpu time)

23:00:55 Running Spec_Check ...

23:00:55 Spec_Check: theory Spec_Check

23:00:56 Spec_Check: theory Examples

23:00:58 Warning: missing document directory

23:00:58 Timing Spec_Check (2 threads, 1.675s elapsed time, 3.056s cpu time, 0.012s GC time, factor 1.82)

23:00:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/Spec_Check

23:00:58 Finished Spec_Check (0:00:01 elapsed time, 0:00:03 cpu time)

23:00:58 Running ZF-Resid ...

23:00:58 ZF-Resid: theory Redex

23:00:58 ZF-Resid: theory Substitution

23:00:58 ZF-Resid: theory Residuals

23:00:59 HOL: theory Complex

23:00:59 ZF-Resid: theory Reduction

23:00:59 ZF-Resid: theory Confluence

23:00:59 HOL: theory MacLaurin

23:01:00 Timing ZF-Resid (2 threads, 1.514s elapsed time, 2.436s cpu time, 0.000s GC time, factor 1.61)

23:01:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Resid

23:01:00 Finished ZF-Resid (0:00:01 elapsed time)

23:01:00 Running ZF-IMP ...

23:01:00 ZF-IMP: theory Com

23:01:00 ZF-IMP: theory Denotation

23:01:00 HOL: theory Complex_Main

23:01:00 ZF-IMP: theory Equiv

23:01:01 Timing ZF-IMP (2 threads, 0.977s elapsed time, 1.128s cpu time, 0.000s GC time, factor 1.15)

23:01:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP

23:01:01 Finished ZF-IMP (0:00:01 elapsed time)

23:01:01 Running CTT ...

23:01:02 CTT: theory CTT

23:01:02 CTT: theory Bool

23:01:02 CTT: theory Elimination

23:01:02 CTT: theory Arith

23:01:02 CTT: theory Equality

23:01:02 CTT: theory Typechecking

23:01:02 CTT: theory Synthesis

23:01:02 CTT: theory Main

23:01:04 Timing CTT (2 threads, 0.674s elapsed time, 1.032s cpu time, 0.000s GC time, factor 1.53)

23:01:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT

23:01:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/document.pdf

23:01:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/outline.pdf

23:01:04 Finished CTT (0:00:02 elapsed time, 0:00:03 cpu time)

23:01:04 Running Cube ...

23:01:04 Cube: theory Cube

23:01:04 Cube: theory Example

23:01:04 Timing Cube (2 threads, 0.262s elapsed time, 0.268s cpu time, 0.000s GC time, factor 1.02)

23:01:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Cube/Cube

23:01:04 Finished Cube (0:00:00 elapsed time)

23:01:04 Running Intro ...

23:01:07 Timing Intro (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

23:01:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro

23:01:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro/intro.pdf

23:01:07 Finished Intro (0:00:02 elapsed time)

23:01:07 Running ZF-Coind ...

23:01:07 ZF-Coind: theory Language

23:01:07 ZF-Coind: theory Map

23:01:07 ZF-Coind: theory Types

23:01:07 ZF-Coind: theory Values

23:01:07 ZF-Coind: theory Dynamic

23:01:07 ZF-Coind: theory Static

23:01:08 ZF-Coind: theory ECR

23:01:08 HOL-Proofs: theory Code_Numeral

23:01:08 Timing ZF-Coind (2 threads, 0.670s elapsed time, 1.296s cpu time, 0.000s GC time, factor 1.93)

23:01:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Coind

23:01:08 Finished ZF-Coind (0:00:00 elapsed time)

23:01:08 Running System ...

23:01:08 System: theory Base

23:01:08 System: theory Misc

23:01:08 System: theory Environment

23:01:08 System: theory Presentation

23:01:08 System: theory Scala

23:01:08 System: theory Sessions

23:01:10 HOL-Proofs: theory Numeral_Simprocs

23:01:11 Timing System (2 threads, 0.295s elapsed time, 0.392s cpu time, 0.000s GC time, factor 1.33)

23:01:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System

23:01:11 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System/system.pdf

23:01:11 Finished System (0:00:02 elapsed time)

23:01:11 Running Logics_ZF ...

23:01:11 HOL-Proofs: theory SMT

23:01:11 Logics_ZF: theory FOL_examples

23:01:11 Logics_ZF: theory If

23:01:11 Logics_ZF: theory ZF_Isar

23:01:11 Logics_ZF: theory ZF_examples

23:01:11 Logics_ZF: theory IFOL_examples

23:01:12 HOL-Proofs: theory Semiring_Normalization

23:01:13 HOL-Proofs: theory Set_Interval

23:01:14 Timing Logics_ZF (2 threads, 0.267s elapsed time, 0.504s cpu time, 0.000s GC time, factor 1.89)

23:01:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF

23:01:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF/logics-ZF.pdf

23:01:14 Finished Logics_ZF (0:00:02 elapsed time)

23:01:14 Running SML ...

23:01:14 SML: theory Examples

23:01:14 HOL-Proofs: theory Groebner_Basis

23:01:14 Warning: missing document directory

23:01:14 Timing SML (2 threads, 0.013s elapsed time, 0.016s cpu time, 0.000s GC time, factor 1.24)

23:01:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/SML

23:01:14 Finished SML (0:00:00 elapsed time)

23:01:14 Running Logics ...

23:01:17 Timing Logics (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

23:01:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics

23:01:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics/logics.pdf

23:01:17 Finished Logics (0:00:02 elapsed time)

23:01:17 Running Nitpick ...

23:01:19 Timing Nitpick (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

23:01:19 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick

23:01:19 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick/nitpick.pdf

23:01:19 Finished Nitpick (0:00:02 elapsed time)

23:01:19 Running Sledgehammer ...

23:01:22 Timing Sledgehammer (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

23:01:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer

23:01:22 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer/sledgehammer.pdf

23:01:22 Finished Sledgehammer (0:00:02 elapsed time)

23:01:24 HOL-Proofs: theory Conditionally_Complete_Lattices

23:01:24 HOL-Proofs: theory Filter

23:01:29 HOL-Proofs: theory Presburger

23:01:40 HOL-Proofs: theory Sledgehammer

23:01:41 HOL-Proofs: theory List

23:02:17 HOL-Proofs: theory Groups_List

23:02:18 HOL-Proofs: theory Map

23:02:21 HOL-Proofs: theory Enum

23:02:37 HOL-Proofs: theory Random

23:03:17 HOL-Proofs: theory String

23:03:19 HOL-Proofs: theory BNF_Greatest_Fixpoint

23:03:23 HOL-Proofs: theory Predicate

23:03:25 HOL-Proofs: theory Lazy_Sequence

23:03:26 HOL-Proofs: theory Limited_Sequence

23:03:26 HOL-Proofs: theory Typerep

23:03:27 HOL-Proofs: theory Code_Evaluation

23:03:29 HOL-Proofs: theory Quickcheck_Random

23:03:31 HOL-Proofs: theory Quickcheck_Exhaustive

23:03:36 HOL-Proofs: theory Record

23:03:37 HOL-Proofs: theory Nitpick

23:03:42 HOL-Proofs: theory Quickcheck_Narrowing

23:03:46 HOL-Proofs: theory Random_Pred

23:03:47 HOL-Proofs: theory Random_Sequence

23:03:47 HOL-Proofs: theory Predicate_Compile

23:03:49 HOL-Proofs: theory Main

23:03:51 HOL-Proofs: theory Old_Datatype

23:03:56 Timing HOL (2 threads, 221.368s elapsed time, 413.760s cpu time, 28.892s GC time, factor 1.87)

23:03:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL

23:03:56 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/document.pdf

23:03:56 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/outline.pdf

23:03:56 Finished HOL (0:05:11 elapsed time, 0:09:19 cpu time, factor 1.80)

23:03:58 Building HOLCF ...

23:03:58 Building HOL-Word ...

23:03:59 HOLCF: theory Old_Datatype

23:03:59 HOLCF: theory Nat_Bijection

23:04:00 HOL-Word: theory Bit

23:04:00 HOL-Word: theory Bits

23:04:00 HOL-Word: theory Boolean_Algebra

23:04:00 HOL-Word: theory Bits_Bit

23:04:00 HOL-Word: theory Misc_Numeric

23:04:00 HOL-Word: theory Bit_Representation

23:04:00 HOL-Word: theory Misc_Typedef

23:04:01 HOL-Word: theory Phantom_Type

23:04:01 HOLCF: theory Countable

23:04:01 HOL-Word: theory Bits_Int

23:04:02 HOL-Word: theory Cardinality

23:04:02 HOLCF: theory Porder

23:04:02 HOL-Word: theory Bool_List_Representation

23:04:02 HOL-Word: theory Numeral_Type

23:04:03 HOLCF: theory Pcpo

23:04:03 HOL-Word: theory Word_Miscellaneous

23:04:03 HOL-Word: theory Type_Length

23:04:03 HOL-Word: theory Word

23:04:04 HOLCF: theory Cont

23:04:04 HOLCF: theory Adm

23:04:04 HOLCF: theory Discrete

23:04:05 HOLCF: theory Cpodef

23:04:05 HOLCF: theory Fun_Cpo

23:04:05 HOLCF: theory Product_Cpo

23:04:05 HOLCF: theory Cfun

23:04:06 HOLCF: theory Cprod

23:04:06 HOLCF: theory Fix

23:04:06 HOLCF: theory Sfun

23:04:06 HOLCF: theory Sprod

23:04:06 HOLCF: theory Up

23:04:07 HOLCF: theory Lift

23:04:07 HOLCF: theory Tr

23:04:07 HOLCF: theory One

23:04:08 HOLCF: theory Ssum

23:04:08 HOLCF: theory Plain_HOLCF

23:04:08 HOLCF: theory Completion

23:04:08 HOLCF: theory Deflation

23:04:09 HOLCF: theory Map_Functions

23:04:09 HOLCF: theory Fixrec

23:04:09 HOLCF: theory Bifinite

23:04:09 HOLCF: theory Domain_Aux

23:04:10 HOLCF: theory Universal

23:04:11 HOLCF: theory Algebraic

23:04:11 HOLCF: theory Compact_Basis

23:04:11 HOLCF: theory LowerPD

23:04:11 HOLCF: theory UpperPD

23:04:12 HOLCF: theory Representable

23:04:12 HOLCF: theory ConvexPD

23:04:14 HOLCF: theory Domain

23:04:16 HOLCF: theory Powerdomains

23:04:16 HOLCF: theory HOLCF

23:04:37 Timing HOLCF (2 threads, 17.325s elapsed time, 31.260s cpu time, 1.688s GC time, factor 1.80)

23:04:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF

23:04:37 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/document.pdf

23:04:37 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/outline.pdf

23:04:37 Finished HOLCF (0:00:39 elapsed time, 0:01:04 cpu time, factor 1.63)

23:04:38 Timing HOL-Word (2 threads, 18.769s elapsed time, 36.108s cpu time, 1.448s GC time, factor 1.92)

23:04:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word

23:04:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/document.pdf

23:04:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/outline.pdf

23:04:38 Finished HOL-Word (0:00:39 elapsed time, 0:01:06 cpu time, factor 1.69)

23:04:38 Building IOA ...

23:04:38 Building HOL-TLA ...

23:04:40 HOL-TLA: theory Intensional

23:04:40 HOL-TLA: theory Stfun

23:04:40 HOL-TLA: theory Action

23:04:40 IOA: theory Asig

23:04:40 IOA: theory Seq

23:04:40 HOL-TLA: theory Init

23:04:40 HOL-TLA: theory TLA

23:04:40 IOA: theory Automata

23:04:41 IOA: theory Sequence

23:04:41 IOA: theory Pred

23:04:42 IOA: theory Traces

23:04:42 IOA: theory TL

23:04:43 IOA: theory CompoExecs

23:04:43 IOA: theory RefMappings

23:04:43 IOA: theory CompoScheds

23:04:43 IOA: theory RefCorrectness

23:04:44 IOA: theory Simulations

23:04:44 IOA: theory SimCorrectness

23:04:44 IOA: theory Deadlock

23:04:45 IOA: theory ShortExecutions

23:04:45 IOA: theory CompoTraces

23:04:46 IOA: theory Compositionality

23:04:46 IOA: theory IOA

23:04:46 IOA: theory TLS

23:04:47 IOA: theory LiveIOA

23:04:47 IOA: theory Abstraction

23:04:53 Timing HOL-TLA (2 threads, 1.764s elapsed time, 2.756s cpu time, 0.000s GC time, factor 1.56)

23:04:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA

23:04:53 Finished HOL-TLA (0:00:15 elapsed time, 0:00:21 cpu time, factor 1.42)

23:04:53 Building HOL-Analysis ...

23:04:56 HOL-Analysis: theory FuncSet

23:04:56 HOL-Analysis: theory Disjoint_Sets

23:04:57 HOL-Analysis: theory Infinite_Set

23:04:57 HOL-Analysis: theory Multiset

23:04:57 HOL-Analysis: theory Nat_Bijection

23:04:58 HOL-Analysis: theory Old_Datatype

23:04:59 HOL-Analysis: theory Countable

23:05:01 HOL-Analysis: theory Countable_Set

23:05:01 HOL-Analysis: theory Countable_Complete_Lattices

23:05:02 HOL-Analysis: theory Permutations

23:05:03 HOL-Analysis: theory Phantom_Type

23:05:04 HOL-Analysis: theory Cardinality

23:05:04 HOL-Analysis: theory Product_Plus

23:05:04 HOL-Analysis: theory Numeral_Type

23:05:04 HOL-Analysis: theory Product_Order

23:05:05 HOL-Analysis: theory Set_Algebras

23:05:05 HOL-Analysis: theory L2_Norm

23:05:05 HOL-Analysis: theory Continuum_Not_Denumerable

23:05:06 HOL-Analysis: theory Discrete

23:05:06 HOL-Analysis: theory Indicator_Function

23:05:06 HOL-Analysis: theory Inner_Product

23:05:06 HOL-Analysis: theory Liminf_Limsup

23:05:07 HOL-Analysis: theory Nonpos_Ints

23:05:07 HOL-Analysis: theory Product_Vector

23:05:07 HOL-Analysis: theory Operator_Norm

23:05:07 HOL-Analysis: theory Order_Continuity

23:05:07 HOL-Analysis: theory Euclidean_Space

23:05:08 HOL-Analysis: theory Extended_Nat

23:05:09 HOL-Analysis: theory Extended_Real

23:05:09 HOL-Analysis: theory Finite_Cartesian_Product

23:05:10 HOL-Analysis: theory Linear_Algebra

23:05:12 Timing IOA (2 threads, 15.157s elapsed time, 28.368s cpu time, 0.988s GC time, factor 1.87)

23:05:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA

23:05:12 Finished IOA (0:00:34 elapsed time, 0:00:56 cpu time, factor 1.64)

23:05:13 Building HOL-SPARK ...

23:05:13 HOL-Analysis: theory Periodic_Fun

23:05:13 HOL-Analysis: theory Extended_Nonnegative_Real

23:05:13 HOL-Analysis: theory Poly_Roots

23:05:13 HOL-Analysis: theory Sum_of_Squares

23:05:15 HOL-Analysis: theory Sigma_Algebra

23:05:15 HOL-SPARK: theory Bit_Comparison

23:05:15 HOL-SPARK: theory SPARK_Setup

23:05:16 HOL-Analysis: theory Norm_Arith

23:05:16 HOL-Analysis: theory Topology_Euclidean_Space

23:05:17 HOL-SPARK: theory SPARK

23:05:18 HOL-Analysis: theory Measurable

23:05:18 HOL-Analysis: theory Measure_Space

23:05:21 HOL-Analysis: theory Caratheodory

23:05:21 HOL-Analysis: theory Summation_Tests

23:05:24 HOL-Analysis: theory Bounded_Linear_Function

23:05:24 HOL-Analysis: theory Convex_Euclidean_Space

23:05:25 HOL-Analysis: theory Extended_Real_Limits

23:05:26 HOL-Analysis: theory Tagged_Division

23:05:28 HOL-Analysis: theory Uniform_Limit

23:05:30 HOL-Analysis: theory Continuous_Extension

23:05:30 HOL-Analysis: theory Path_Connected

23:05:31 Timing HOL-SPARK (2 threads, 2.088s elapsed time, 3.532s cpu time, 0.112s GC time, factor 1.69)

23:05:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK

23:05:31 Finished HOL-SPARK (0:00:17 elapsed time, 0:00:25 cpu time, factor 1.46)

23:05:31 Building HOL-Library ...

23:05:34 HOL-Library: theory Lattice_Syntax

23:05:34 HOL-Library: theory Adhoc_Overloading

23:05:34 HOL-Library: theory AList

23:05:34 HOL-Analysis: theory Homeomorphism

23:05:34 HOL-Library: theory BNF_Axiomatization

23:05:34 HOL-Library: theory BNF_Corec

23:05:34 HOL-Analysis: theory Brouwer_Fixpoint

23:05:35 HOL-Library: theory DAList

23:05:36 HOL-Analysis: theory Derivative

23:05:36 HOL-Library: theory Stirling

23:05:37 HOL-Library: theory Bit

23:05:37 HOL-Library: theory Bits

23:05:38 HOL-Library: theory Bits_Bit

23:05:38 HOL-Analysis: theory Cartesian_Euclidean_Space

23:05:38 HOL-Analysis: theory Weierstrass_Theorems

23:05:38 HOL-Library: theory Boolean_Algebra

23:05:38 HOL-Library: theory Cardinal_Notations

23:05:38 HOL-Library: theory Char_ord

23:05:39 HOL-Library: theory Code_Abstract_Nat

23:05:39 HOL-Library: theory Code_Binary_Nat

23:05:39 HOL-Library: theory Code_Target_Nat

23:05:39 HOL-Library: theory Code_Char

23:05:39 HOL-Library: theory Code_Prolog

23:05:40 HOL-Library: theory Code_Test

23:05:40 HOL-Library: theory Combine_PER

23:05:40 HOL-Library: theory Complete_Partial_Order2

23:05:40 HOL-Analysis: theory Determinants

23:05:40 HOL-Library: theory Debug

23:05:40 HOL-Library: theory Disjoint_Sets

23:05:41 HOL-Analysis: theory Fashoda_Theorem

23:05:41 HOL-Library: theory Dlist

23:05:41 HOL-Analysis: theory Ordered_Euclidean_Space

23:05:41 HOL-Analysis: theory Polytope

23:05:42 HOL-Library: theory FSet

23:05:43 HOL-Library: theory Fraction_Field

23:05:44 HOL-Library: theory Fun_Lexorder

23:05:44 HOL-Library: theory FuncSet

23:05:44 HOL-Library: theory Function_Algebras

23:05:44 HOL-Library: theory Finite_Map

23:05:45 HOL-Library: theory Function_Division

23:05:45 HOL-Library: theory Code_Target_Int

23:05:45 HOL-Library: theory Code_Target_Numeral

23:05:45 HOL-Library: theory Groups_Big_Fun

23:05:46 HOL-Library: theory IArray

23:05:46 HOL-Analysis: theory Borel_Space

23:05:46 HOL-Library: theory Infinite_Set

23:05:46 HOL-Library: theory LaTeXsugar

23:05:47 HOL-Library: theory Omega_Words_Fun

23:05:47 HOL-Library: theory Lattice_Constructions

23:05:47 HOL-Library: theory ListVector

23:05:47 HOL-Library: theory List_lexord

23:05:48 HOL-Library: theory Mapping

23:05:48 HOL-Analysis: theory Nonnegative_Lebesgue_Integration

23:05:48 HOL-Analysis: theory Regularity

23:05:49 HOL-Library: theory AList_Mapping

23:05:49 HOL-Library: theory Misc_Numeric

23:05:49 HOL-Library: theory Bit_Representation

23:05:49 HOL-Library: theory Misc_Typedef

23:05:49 HOL-Library: theory Monad_Syntax

23:05:49 HOL-Library: theory More_List

23:05:50 HOL-Library: theory Bits_Int

23:05:50 HOL-Library: theory Multiset

23:05:51 HOL-Analysis: theory Binary_Product_Measure

23:05:51 HOL-Library: theory Bool_List_Representation

23:05:52 HOL-Analysis: theory Embed_Measure

23:05:52 HOL-Library: theory Nat_Bijection

23:05:52 HOL-Analysis: theory Finite_Product_Measure

23:05:52 HOL-Library: theory Stream

23:05:53 HOL-Library: theory Old_Datatype

23:05:53 HOL-Analysis: theory Bochner_Integration

23:05:54 HOL-Analysis: theory Function_Topology

23:05:54 HOL-Library: theory DAList_Multiset

23:05:55 HOL-Library: theory Factorial_Ring

23:05:55 HOL-Library: theory Multiset_Order

23:05:55 HOL-Library: theory Permutation

23:05:55 HOL-Analysis: theory Complete_Measure

23:05:55 HOL-Analysis: theory Radon_Nikodym

23:05:55 HOL-Library: theory Permutations

23:05:56 HOL-Analysis: theory Set_Integral

23:05:56 HOL-Analysis: theory Lebesgue_Measure

23:05:58 HOL-Analysis: theory Henstock_Kurzweil_Integration

23:05:58 HOL-Library: theory Countable

23:06:00 HOL-Library: theory Countable_Set

23:06:00 HOL-Library: theory Countable_Complete_Lattices

23:06:01 HOL-Analysis: theory Bounded_Continuous_Function

23:06:01 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration

23:06:01 HOL-Analysis: theory Integral_Test

23:06:02 HOL-Analysis: theory Complex_Analysis_Basics

23:06:02 HOL-Analysis: theory Interval_Integral

23:06:03 HOL-Analysis: theory Lebesgue_Integral_Substitution

23:06:03 HOL-Library: theory Countable_Set_Type

23:06:03 HOL-Analysis: theory Complex_Transcendental

23:06:04 HOL-Library: theory Euclidean_Algorithm

23:06:05 HOL-Library: theory Old_Recdef

23:06:05 HOL-Analysis: theory Generalised_Binomial_Theorem

23:06:05 HOL-Analysis: theory Harmonic_Numbers

23:06:05 HOL-Analysis: theory Cauchy_Integral_Theorem

23:06:06 HOL-Analysis: theory Gamma_Function

23:06:06 HOL-Library: theory Option_ord

23:06:06 HOL-Library: theory Parallel

23:06:06 HOL-Library: theory Perm

23:06:08 HOL-Library: theory Phantom_Type

23:06:08 HOL-Library: theory Cardinality

23:06:09 HOL-Analysis: theory Further_Topology

23:06:09 HOL-Library: theory FinFun

23:06:09 HOL-Analysis: theory Conformal_Mappings

23:06:12 HOL-Library: theory Numeral_Type

23:06:12 HOL-Analysis: theory Analysis

23:06:12 HOL-Library: theory Normalized_Fraction

23:06:13 HOL-Library: theory Type_Length

23:06:13 HOL-Library: theory Predicate_Compile_Alternative_Defs

23:06:13 HOL-Library: theory Saturated

23:06:13 HOL-Library: theory Predicate_Compile_Quickcheck

23:06:13 HOL-Library: theory Product_Lexorder

23:06:13 HOL-Library: theory Product_Plus

23:06:13 HOL-Library: theory Quotient_Syntax

23:06:13 HOL-Library: theory Quotient_Option

23:06:13 HOL-Library: theory Product_Order

23:06:13 HOL-Library: theory Quotient_Product

23:06:14 HOL-Library: theory Quotient_Set

23:06:14 HOL-Library: theory Finite_Lattice

23:06:14 HOL-Library: theory Quotient_List

23:06:14 HOL-Library: theory Quotient_Sum

23:06:14 HOL-Library: theory Quotient_Type

23:06:14 HOL-Library: theory RBT_Impl

23:06:17 HOL-Library: theory Ramsey

23:06:17 HOL-Library: theory Reflection

23:06:17 HOL-Library: theory Refute

23:06:17 HOL-Library: theory Rewrite

23:06:18 HOL-Library: theory Set_Algebras

23:06:18 HOL-Library: theory Simps_Case_Conv

23:06:18 HOL-Library: theory Extended

23:06:20 HOL-Library: theory State_Monad

23:06:20 HOL-Library: theory Sublist

23:06:21 HOL-Library: theory Prefix_Order

23:06:21 HOL-Library: theory Sublist_Order

23:06:21 HOL-Library: theory Polynomial

23:06:26 HOL-Library: theory BigO

23:06:27 HOL-Library: theory Code_Real_Approx_By_Float

23:06:27 HOL-Library: theory Diagonal_Subsequence

23:06:27 HOL-Library: theory Discrete

23:06:28 HOL-Library: theory Field_as_Ring

23:06:29 HOL-Library: theory Formal_Power_Series

23:06:33 HOL-Library: theory Polynomial_FPS

23:06:33 HOL-Library: theory Fundamental_Theorem_Algebra

23:06:34 HOL-Library: theory Indicator_Function

23:06:35 HOL-Library: theory Lattice_Algebras

23:06:40 HOL-Library: theory Liminf_Limsup

23:06:41 HOL-Library: theory Log_Nat

23:06:41 HOL-Library: theory Float

23:06:43 HOL-Library: theory Lub_Glb

23:06:44 HOL-Library: theory Multiset_Permutations

23:06:45 HOL-Library: theory RBT

23:06:45 HOL-Library: theory Nonpos_Ints

23:06:45 HOL-Library: theory OptionalSugar

23:06:45 HOL-Library: theory RBT_Mapping

23:06:45 HOL-Library: theory RBT_Set

23:06:46 HOL-Library: theory Order_Continuity

23:06:46 HOL-Library: theory Periodic_Fun

23:06:46 HOL-Library: theory Extended_Nat

23:06:47 HOL-Library: theory Polynomial_Factorial

23:06:47 HOL-Library: theory Extended_Real

23:06:51 HOL-Library: theory Extended_Nonnegative_Real

23:06:53 HOL-Library: theory Linear_Temporal_Logic_on_Streams

23:06:55 HOL-Library: theory Quadratic_Discriminant

23:06:55 HOL-Library: theory Sum_of_Squares

23:06:56 HOL-Library: theory Transitive_Closure_Table

23:06:57 HOL-Library: theory Tree

23:06:57 HOL-Library: theory While_Combinator

23:06:58 HOL-Library: theory Bourbaki_Witt_Fixpoint

23:06:58 HOL-Library: theory Word_Miscellaneous

23:06:58 HOL-Library: theory Word

23:07:00 HOL-Library: theory Tree_Multiset

23:07:00 HOL-Library: theory Preorder

23:07:00 HOL-Library: theory Function_Growth

23:07:01 HOL-Library: theory Library

23:07:04 HOL-Library: theory Old_SMT

23:07:59 Timing HOL-Proofs (2 threads, 441.483s elapsed time, 791.788s cpu time, 85.088s GC time, factor 1.79)

23:07:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs

23:07:59 Finished HOL-Proofs (0:09:14 elapsed time, 0:16:12 cpu time, factor 1.76)

23:08:01 Building HOL-Auth ...

23:08:03 HOL-Auth: theory Message

23:08:03 HOL-Auth: theory Nat_Bijection

23:08:04 HOL-Auth: theory Simps_Case_Conv

23:08:06 HOL-Auth: theory All_Symmetric

23:08:06 HOL-Auth: theory Event

23:08:06 HOL-Auth: theory EventSC

23:08:07 HOL-Auth: theory Extensions

23:08:07 HOL-Auth: theory Analz

23:08:08 HOL-Auth: theory List_Msg

23:08:08 HOL-Auth: theory Guard

23:08:08 HOL-Auth: theory GuardK

23:08:09 HOL-Auth: theory Public

23:08:10 HOL-Auth: theory Shared

23:08:10 HOL-Auth: theory CertifiedEmail

23:08:10 HOL-Auth: theory Guard_Public

23:08:10 HOL-Auth: theory Guard_NS_Public

23:08:10 HOL-Auth: theory P2

23:08:11 HOL-Auth: theory Proto

23:08:12 HOL-Auth: theory KerberosIV

23:08:13 HOL-Auth: theory KerberosIV_Gets

23:08:13 HOL-Auth: theory KerberosV

23:08:15 HOL-Auth: theory Kerberos_BAN

23:08:15 HOL-Auth: theory Kerberos_BAN_Gets

23:08:16 HOL-Auth: theory NS_Public

23:08:16 HOL-Auth: theory NS_Public_Bad

23:08:16 HOL-Auth: theory NS_Shared

23:08:16 HOL-Auth: theory OtwayRees

23:08:17 HOL-Auth: theory OtwayReesBella

23:08:17 HOL-Auth: theory OtwayRees_AN

23:08:17 HOL-Auth: theory OtwayRees_Bad

23:08:17 HOL-Auth: theory P1

23:08:18 HOL-Auth: theory Recur

23:08:19 HOL-Auth: theory WooLam

23:08:19 HOL-Auth: theory Yahalom

23:08:20 HOL-Auth: theory Yahalom2

23:08:21 HOL-Auth: theory Yahalom_Bad

23:08:21 HOL-Auth: theory ZhouGollmann

23:08:22 HOL-Auth: theory Auth_Shared

23:08:22 HOL-Auth: theory Auth_Guard_Public

23:08:23 HOL-Auth: theory Guard_Shared

23:08:23 HOL-Auth: theory Guard_OtwayRees

23:08:24 HOL-Auth: theory Guard_Yahalom

23:08:24 HOL-Auth: theory TLS

23:08:24 HOL-Auth: theory Auth_Guard_Shared

23:08:24 HOL-Auth: theory Smartcard

23:08:25 HOL-Auth: theory ShoupRubin

23:08:25 HOL-Auth: theory Auth_Public

23:08:26 HOL-Auth: theory ShoupRubinBella

23:08:28 HOL-Auth: theory Auth_Smartcard

23:11:22 Timing HOL-Library (2 threads, 246.627s elapsed time, 455.580s cpu time, 23.844s GC time, factor 1.85)

23:11:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library

23:11:22 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/document.pdf

23:11:22 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/outline.pdf

23:11:22 Finished HOL-Library (0:05:50 elapsed time, 0:10:21 cpu time, factor 1.78)

23:11:23 Building Codegen_Basics ...

23:11:25 Codegen_Basics: theory IArray

23:11:25 Codegen_Basics: theory Dlist

23:11:26 Codegen_Basics: theory Mapping

23:11:26 Codegen_Basics: theory RBT_Impl

23:11:26 Timing HOL-Auth (2 threads, 173.089s elapsed time, 273.832s cpu time, 8.576s GC time, factor 1.58)

23:11:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth

23:11:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/document.pdf

23:11:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/outline.pdf

23:11:26 Finished HOL-Auth (0:03:24 elapsed time, 0:05:24 cpu time, factor 1.58)

23:11:27 Building HOL-Nonstandard_Analysis ...

23:11:28 HOL-Nonstandard_Analysis: theory Infinite_Set

23:11:28 HOL-Nonstandard_Analysis: theory Lub_Glb

23:11:29 HOL-Nonstandard_Analysis: theory Free_Ultrafilter

23:11:29 HOL-Nonstandard_Analysis: theory StarDef

23:11:30 HOL-Nonstandard_Analysis: theory HyperNat

23:11:31 HOL-Nonstandard_Analysis: theory HyperDef

23:11:32 HOL-Nonstandard_Analysis: theory NSA

23:11:33 HOL-Nonstandard_Analysis: theory NSComplex

23:11:33 HOL-Nonstandard_Analysis: theory Star

23:11:34 HOL-Nonstandard_Analysis: theory HLim

23:11:34 HOL-Nonstandard_Analysis: theory NatStar

23:11:35 HOL-Nonstandard_Analysis: theory HDeriv

23:11:35 HOL-Nonstandard_Analysis: theory HSEQ

23:11:36 HOL-Nonstandard_Analysis: theory HSeries

23:11:36 HOL-Nonstandard_Analysis: theory HTranscendental

23:11:37 HOL-Nonstandard_Analysis: theory HLog

23:11:37 HOL-Nonstandard_Analysis: theory NSCA

23:11:38 HOL-Nonstandard_Analysis: theory Hyperreal

23:11:38 HOL-Nonstandard_Analysis: theory CStar

23:11:38 HOL-Nonstandard_Analysis: theory CLim

23:11:39 HOL-Nonstandard_Analysis: theory Hypercomplex

23:11:39 HOL-Nonstandard_Analysis: theory Nonstandard_Analysis

23:11:55 Codegen_Basics: theory RBT

23:11:55 Codegen_Basics: theory Setup

23:11:59 Timing HOL-Nonstandard_Analysis (2 threads, 13.647s elapsed time, 26.804s cpu time, 0.912s GC time, factor 1.96)

23:11:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis

23:11:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/document.pdf

23:11:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/outline.pdf

23:11:59 Finished HOL-Nonstandard_Analysis (0:00:32 elapsed time, 0:00:54 cpu time, factor 1.70)

23:11:59 Building Typeclass_Hierarchy_Basics ...

23:12:01 Typeclass_Hierarchy_Basics: theory Lattice_Syntax

23:12:01 Typeclass_Hierarchy_Basics: theory Multiset

23:12:06 Typeclass_Hierarchy_Basics: theory Setup

23:12:23 Timing Typeclass_Hierarchy_Basics (2 threads, 8.024s elapsed time, 15.068s cpu time, 0.656s GC time, factor 1.88)

23:12:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy_Basics

23:12:23 Finished Typeclass_Hierarchy_Basics (0:00:23 elapsed time, 0:00:37 cpu time, factor 1.60)

23:12:23 Building HOL-Nominal ...

23:12:25 HOL-Nominal: theory Infinite_Set

23:12:25 HOL-Nominal: theory Old_Datatype

23:12:27 HOL-Nominal: theory Nominal

23:12:43 Timing Codegen_Basics (2 threads, 50.326s elapsed time, 89.256s cpu time, 3.276s GC time, factor 1.77)

23:12:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen_Basics

23:12:43 Finished Codegen_Basics (0:01:19 elapsed time, 0:02:13 cpu time, factor 1.68)

23:12:43 Building HOL-Eisbach ...

23:12:46 HOL-Eisbach: theory Eisbach

23:12:46 HOL-Eisbach: theory IFOL

23:12:46 HOL-Eisbach: theory Eisbach_Old_Appl_Syntax

23:12:46 Timing HOL-Nominal (2 threads, 7.359s elapsed time, 14.440s cpu time, 0.800s GC time, factor 1.96)

23:12:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal

23:12:46 Finished HOL-Nominal (0:00:22 elapsed time, 0:00:36 cpu time, factor 1.62)

23:12:46 HOL-Eisbach: theory Eisbach_Tools

23:12:46 HOL-Eisbach: theory Examples

23:12:46 Building HOL-Mirabelle ...

23:12:47 HOL-Eisbach: theory Tests

23:12:47 HOL-Eisbach: theory FOL

23:12:48 HOL-Mirabelle: theory Mirabelle

23:12:48 HOL-Eisbach: theory Examples_FOL

23:12:48 HOL-Mirabelle: theory Mirabelle_Test

23:12:59 Timing HOL-Mirabelle (2 threads, 0.498s elapsed time, 0.552s cpu time, 0.000s GC time, factor 1.11)

23:12:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle

23:12:59 Finished HOL-Mirabelle (0:00:12 elapsed time, 0:00:17 cpu time, factor 1.38)

23:12:59 Running HOL-Nominal-Examples ...

23:12:59 Warning: missing document directory

23:12:59 Timing HOL-Eisbach (2 threads, 2.860s elapsed time, 5.620s cpu time, 0.132s GC time, factor 1.96)

23:12:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Eisbach

23:12:59 Finished HOL-Eisbach (0:00:16 elapsed time, 0:00:24 cpu time, factor 1.49)

23:13:00 Running HOL-Data_Structures ...

23:13:01 HOL-Nominal-Examples: theory CR_Takahashi

23:13:01 HOL-Nominal-Examples: theory CK_Machine

23:13:01 HOL-Data_Structures: theory Less_False

23:13:01 HOL-Data_Structures: theory Multiset

23:13:01 HOL-Data_Structures: theory Fib

23:13:04 HOL-Nominal-Examples: theory Class1

23:13:10 HOL-Data_Structures: theory Cmp

23:13:10 HOL-Data_Structures: theory Sorted_Less

23:13:10 HOL-Data_Structures: theory AList_Upd_Del

23:13:11 HOL-Data_Structures: theory List_Ins_Del

23:13:11 HOL-Data_Structures: theory Map_by_Ordered

23:13:11 HOL-Data_Structures: theory Tree

23:13:11 HOL-Data_Structures: theory Set_by_Ordered

23:13:11 HOL-Data_Structures: theory Brother12_Set

23:13:12 HOL-Nominal-Examples: theory Compile

23:13:14 HOL-Data_Structures: theory Balance

23:13:15 HOL-Data_Structures: theory Splay_Set

23:13:17 HOL-Data_Structures: theory Splay_Map

23:13:18 HOL-Data_Structures: theory Tree_Set

23:13:19 HOL-Data_Structures: theory Tree_Map

23:13:20 HOL-Data_Structures: theory Tree2

23:13:21 HOL-Data_Structures: theory Isin2

23:13:21 HOL-Data_Structures: theory AA_Set

23:13:23 HOL-Data_Structures: theory AVL_Set

23:13:25 HOL-Data_Structures: theory Leftist_Heap

23:13:28 HOL-Data_Structures: theory Lookup2

23:13:28 HOL-Nominal-Examples: theory Contexts

23:13:28 HOL-Data_Structures: theory AA_Map

23:13:29 HOL-Data_Structures: theory AVL_Map

23:13:30 HOL-Data_Structures: theory RBT

23:13:34 HOL-Nominal-Examples: theory Crary

23:13:38 HOL-Nominal-Examples: theory Fsub

23:13:39 HOL-Data_Structures: theory RBT_Set

23:13:42 HOL-Data_Structures: theory RBT_Map

23:13:45 HOL-Nominal-Examples: theory Height

23:13:46 HOL-Data_Structures: theory Tree23

23:13:47 HOL-Nominal-Examples: theory Lam_Funs

23:13:47 HOL-Data_Structures: theory Tree23_Set

23:13:50 HOL-Nominal-Examples: theory CR

23:13:50 HOL-Nominal-Examples: theory SN

23:13:52 HOL-Nominal-Examples: theory Lambda_mu

23:13:54 HOL-Data_Structures: theory Tree23_Map

23:13:55 HOL-Nominal-Examples: theory LocalWeakening

23:13:58 HOL-Data_Structures: theory Tree234

23:13:58 HOL-Nominal-Examples: theory Pattern

23:14:00 HOL-Data_Structures: theory Tree234_Set

23:14:07 HOL-Nominal-Examples: theory SOS

23:14:10 HOL-Nominal-Examples: theory Standardization

23:14:13 HOL-Nominal-Examples: theory Support

23:14:13 HOL-Nominal-Examples: theory Type_Preservation

23:14:16 HOL-Nominal-Examples: theory W

23:14:21 HOL-Nominal-Examples: theory Weakening

23:14:22 HOL-Data_Structures: theory Brother12_Map

23:14:27 HOL-Data_Structures: theory Tree234_Map

23:15:29 HOL-Nominal-Examples: theory Class2

23:15:32 HOL-Nominal-Examples: theory Class3

23:16:36 Timing HOL-Analysis (2 threads, 591.248s elapsed time, 1027.232s cpu time, 67.164s GC time, factor 1.74)

23:16:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis

23:16:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/document.pdf

23:16:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/outline.pdf

23:16:36 Finished HOL-Analysis (0:11:42 elapsed time, 0:19:57 cpu time, factor 1.70)

23:16:37 Building HOL-Probability ...

23:16:43 HOL-Probability: theory FSet

23:16:43 HOL-Probability: theory AList

23:16:44 HOL-Probability: theory Permutation

23:16:45 HOL-Probability: theory Diagonal_Subsequence

23:16:46 HOL-Probability: theory Finite_Map

23:16:54 HOL-Probability: theory Lattice_Syntax

23:16:54 HOL-Probability: theory Adhoc_Overloading

23:16:54 HOL-Probability: theory Complete_Partial_Order2

23:16:54 HOL-Probability: theory Mapping

23:16:55 HOL-Probability: theory AList_Mapping

23:16:55 HOL-Probability: theory Monad_Syntax

23:16:56 HOL-Probability: theory Stream

23:16:57 HOL-Probability: theory Rewrite

23:16:57 HOL-Probability: theory Sublist

23:16:57 HOL-Probability: theory Multiset_Permutations

23:16:58 HOL-Probability: theory Linear_Temporal_Logic_on_Streams

23:16:58 HOL-Probability: theory Fin_Map

23:16:59 HOL-Probability: theory Discrete_Topology

23:16:59 HOL-Probability: theory Essential_Supremum

23:17:00 HOL-Probability: theory Probability_Measure

23:17:00 HOL-Probability: theory Stopping_Time

23:17:01 HOL-Probability: theory Conditional_Expectation

23:17:02 HOL-Probability: theory Distribution_Functions

23:17:02 HOL-Probability: theory Weak_Convergence

23:17:02 HOL-Probability: theory Giry_Monad

23:17:02 HOL-Probability: theory Helly_Selection

23:17:04 HOL-Probability: theory Probability_Mass_Function

23:17:05 HOL-Probability: theory Projective_Family

23:17:06 HOL-Probability: theory Infinite_Product_Measure

23:17:06 HOL-Probability: theory PMF_Impl

23:17:07 HOL-Probability: theory Random_Permutations

23:17:08 HOL-Probability: theory SPMF

23:17:08 HOL-Probability: theory Independent_Family

23:17:10 HOL-Probability: theory Convolution

23:17:10 HOL-Probability: theory Information

23:17:12 HOL-Probability: theory Projective_Limit

23:17:13 HOL-Probability: theory Distributions

23:17:13 HOL-Probability: theory Stream_Space

23:17:15 HOL-Probability: theory Characteristic_Functions

23:17:15 HOL-Probability: theory Sinc_Integral

23:17:16 HOL-Probability: theory Levy

23:17:16 HOL-Probability: theory Central_Limit_Theorem

23:17:17 HOL-Probability: theory Probability

23:19:59 Timing HOL-Probability (2 threads, 148.263s elapsed time, 266.032s cpu time, 10.764s GC time, factor 1.79)

23:19:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability

23:19:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/document.pdf

23:19:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/outline.pdf

23:19:59 Finished HOL-Probability (0:03:21 elapsed time, 0:05:45 cpu time, factor 1.72)

23:20:00 Running HOL-Codegenerator_Test ...

23:20:08 HOL-Codegenerator_Test: theory Cmp

23:20:08 HOL-Codegenerator_Test: theory Code_Test_PolyML

23:20:08 HOL-Codegenerator_Test: theory Code_Test_Scala

23:20:08 HOL-Codegenerator_Test: theory Less_False

23:20:08 HOL-Codegenerator_Test: theory Sorted_Less

23:20:08 HOL-Codegenerator_Test: theory Primes

23:20:08 HOL-Codegenerator_Test: theory AList_Upd_Del

23:20:09 HOL-Codegenerator_Test: theory Map_by_Ordered

23:20:09 HOL-Codegenerator_Test: theory List_Ins_Del

23:20:09 HOL-Codegenerator_Test: theory Eratosthenes

23:20:10 HOL-Codegenerator_Test: theory Records

23:20:10 HOL-Codegenerator_Test: theory Set_by_Ordered

23:20:10 HOL-Codegenerator_Test: theory Tree_Set

23:20:11 HOL-Codegenerator_Test: theory Tree_Map

23:20:14 HOL-Codegenerator_Test: theory Candidates

23:20:16 HOL-Codegenerator_Test: theory Generate

23:20:16 HOL-Codegenerator_Test: theory Generate_Binary_Nat

23:24:07 HOL-Codegenerator_Test: theory Generate_Efficient_Datastructures

23:24:13 HOL-Codegenerator_Test: theory Generate_Pretty_Char

23:24:34 Timing HOL-Data_Structures (2 threads, 688.956s elapsed time, 941.264s cpu time, 54.252s GC time, factor 1.37)

23:24:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures

23:24:34 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures/document.pdf

23:24:34 Finished HOL-Data_Structures (0:11:33 elapsed time, 0:15:45 cpu time, factor 1.36)

23:24:34 Running HOL-ex ...

23:24:36 HOL-ex: theory Adhoc_Overloading

23:24:36 HOL-ex: theory Cartouche_Examples

23:24:36 HOL-ex: theory Chinese

23:24:36 HOL-ex: theory Code_Abstract_Nat

23:24:36 HOL-ex: theory Code_Binary_Nat

23:24:36 HOL-ex: theory FuncSet

23:24:37 HOL-ex: theory Hebrew

23:24:37 HOL-ex: theory Monad_Syntax

23:24:37 HOL-ex: theory Refute

23:24:38 HOL-ex: theory Serbian

23:24:39 HOL-ex: theory State_Monad

23:24:39 HOL-ex: theory Code_Binary_Nat_examples

23:24:39 HOL-ex: theory Eval_Examples

23:24:42 HOL-ex: theory Normalization_by_Evaluation

23:24:43 HOL-ex: theory Transitive_Closure_Table

23:25:02 HOL-ex: theory PresburgerEx

23:25:02 HOL-ex: theory Groebner_Examples

23:25:02 HOL-ex: theory AList

23:25:02 HOL-ex: theory Abstract_NAT

23:25:03 HOL-ex: theory Antiquote

23:25:03 HOL-ex: theory Arith_Examples

23:25:03 HOL-ex: theory CTL

23:25:03 HOL-ex: theory Classical

23:25:04 HOL-ex: theory Code_Target_Nat

23:25:04 HOL-ex: theory Coercion_Examples

23:25:04 HOL-ex: theory Coherent

23:25:05 HOL-ex: theory Commands

23:25:05 HOL-ex: theory Debug

23:25:05 HOL-ex: theory Dlist

23:25:06 HOL-ex: theory Erdoes_Szekeres

23:25:06 HOL-ex: theory Executable_Relation

23:25:06 HOL-ex: theory FSet

23:25:07 HOL-ex: theory Birthday_Paradox

23:25:07 HOL-ex: theory Code_Target_Int

23:25:07 HOL-ex: theory Code_Target_Numeral

23:25:08 HOL-ex: theory Transfer_Int_Nat

23:25:08 HOL-ex: theory Guess

23:25:08 HOL-ex: theory Hex_Bin_Examples

23:25:08 HOL-ex: theory IArray

23:25:09 HOL-ex: theory IArray_Examples

23:25:09 HOL-ex: theory Iff_Oracle

23:25:09 HOL-ex: theory Induction_Schema

23:25:09 HOL-ex: theory Infinite_Set

23:25:09 HOL-ex: theory Intuitionistic

23:25:09 HOL-ex: theory LaTeXsugar

23:25:09 HOL-ex: theory Adhoc_Overloading_Examples

23:25:10 HOL-ex: theory Lagrange

23:25:10 HOL-ex: theory List_to_Set_Comprehension_Examples

23:25:10 HOL-ex: theory LocaleTest2

23:25:11 HOL-ex: theory ML

23:25:11 HOL-ex: theory Mapping

23:25:12 HOL-ex: theory Functions

23:25:12 HOL-ex: theory AList_Mapping

23:25:12 HOL-ex: theory Execute_Choice

23:25:12 HOL-ex: theory MonoidGroup

23:25:13 HOL-ex: theory Multiquote

23:25:13 HOL-ex: theory Multiset

23:25:17 HOL-ex: theory NatSum

23:25:17 HOL-ex: theory PER

23:25:17 HOL-ex: theory Parallel

23:25:17 HOL-ex: theory Bubblesort

23:25:18 HOL-ex: theory Factorial_Ring

23:25:18 HOL-ex: theory MergeSort

23:25:19 HOL-ex: theory Quicksort

23:25:19 HOL-ex: theory Perm

23:25:21 HOL-ex: theory Perm_Fragments

23:25:21 HOL-ex: theory Phantom_Type

23:25:22 HOL-ex: theory Cardinality

23:25:23 HOL-ex: theory FinFun

23:25:25 HOL-ex: theory Euclidean_Algorithm

23:25:25 HOL-ex: theory FinFunPred

23:25:26 HOL-ex: theory Numeral_Type

23:25:27 HOL-ex: theory Type_Length

23:25:27 HOL-ex: theory Primrec

23:25:27 HOL-ex: theory Records

23:25:32 HOL-ex: theory Reflection

23:25:32 HOL-ex: theory Refute_Examples

23:25:34 HOL-ex: theory Primes

23:25:35 HOL-ex: theory Eratosthenes

23:25:35 HOL-ex: theory Code_Timing

23:25:35 HOL-ex: theory Rewrite

23:25:35 HOL-ex: theory Rewrite_Examples

23:25:36 HOL-ex: theory SAT_Examples

23:25:36 HOL-ex: theory Seq

23:25:36 HOL-ex: theory Set_Comprehension_Pointfree_Examples

23:25:37 HOL-ex: theory Set_Theory

23:25:37 HOL-ex: theory Simproc_Tests

23:25:37 HOL-ex: theory Simps_Case_Conv

23:25:37 HOL-ex: theory Simps_Case_Conv_Examples

23:25:38 HOL-ex: theory Sudoku

23:25:39 HOL-ex: theory Tarski

23:25:40 HOL-ex: theory Termination

23:25:41 HOL-ex: theory ThreeDivides

23:25:42 HOL-ex: theory Argo_Examples

23:25:44 HOL-ex: theory Ballot

23:25:45 HOL-ex: theory BinEx

23:25:46 HOL-ex: theory Cubic_Quartic

23:25:46 HOL-ex: theory Dedekind_Real

23:25:46 HOL-ex: theory Gauge_Integration

23:25:47 HOL-ex: theory HarmonicSeries

23:25:47 HOL-ex: theory Parallel_Example

23:25:47 HOL-ex: theory Pythagoras

23:25:47 HOL-ex: theory Reflection_Examples

23:25:48 HOL-ex: theory Sqrt

23:25:48 HOL-ex: theory Sqrt_Script

23:25:49 HOL-ex: theory Sum_of_Powers

23:25:49 HOL-ex: theory Sum_of_Squares

23:25:51 HOL-ex: theory SOS

23:25:52 HOL-ex: theory SOS_Cert

23:25:52 HOL-ex: theory Transfer_Debug

23:25:52 HOL-ex: theory Transfer_Ex

23:25:52 HOL-ex: theory Transitive_Closure_Table_Ex

23:25:53 HOL-ex: theory Tree23

23:25:57 HOL-Nominal-Examples: theory VC_Condition

23:26:01 Timing HOL-Nominal-Examples (2 threads, 778.990s elapsed time, 1358.356s cpu time, 110.416s GC time, factor 1.74)

23:26:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal-Examples

23:26:01 Finished HOL-Nominal-Examples (0:13:01 elapsed time, 0:22:40 cpu time, factor 1.74)

23:26:01 Running HOL-Decision_Procs ...

23:26:04 HOL-Decision_Procs: theory Code_Abstract_Nat

23:26:04 HOL-Decision_Procs: theory Commutative_Ring

23:26:04 HOL-Decision_Procs: theory Code_Target_Nat

23:26:05 HOL-Decision_Procs: theory DP_Library

23:26:05 HOL-Decision_Procs: theory Dense_Linear_Order

23:26:09 HOL-Decision_Procs: theory Dense_Linear_Order_Ex

23:26:10 HOL-Decision_Procs: theory Code_Target_Int

23:26:11 HOL-Decision_Procs: theory Code_Target_Numeral

23:26:11 HOL-Decision_Procs: theory Old_Recdef

23:26:13 HOL-Decision_Procs: theory Cooper

23:26:13 HOL-Decision_Procs: theory Commutative_Ring_Complete

23:26:14 HOL-Decision_Procs: theory Commutative_Ring_Ex

23:26:14 HOL-Decision_Procs: theory Ferrack

23:26:17 HOL-ex: theory Unification

23:26:19 HOL-ex: theory While_Combinator

23:26:20 HOL-ex: theory While_Combinator_Example

23:26:20 HOL-ex: theory Word_Type

23:26:38 HOL-Decision_Procs: theory Lattice_Algebras

23:26:46 HOL-Decision_Procs: theory Log_Nat

23:26:46 HOL-Decision_Procs: theory Float

23:26:48 HOL-Decision_Procs: theory MIR

23:26:49 HOL-Decision_Procs: theory Approximation

23:26:52 HOL-Codegenerator_Test: theory Generate_Target_Nat

23:27:28 HOL-Decision_Procs: theory Polynomial_List

23:27:42 HOL-Decision_Procs: theory Approximation_Ex

23:27:42 HOL-Decision_Procs: theory Approximation_Quickcheck_Ex

23:27:43 HOL-Decision_Procs: theory Rat_Pair

23:27:45 HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial

23:27:56 HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff

23:28:29 HOL-Decision_Procs: theory Decision_Procs

23:30:48 HOL-Codegenerator_Test: theory Code_Test_GHC

23:30:49 HOL-Codegenerator_Test: theory Code_Test_MLton

23:30:53 HOL-Codegenerator_Test: theory Code_Test_OCaml

23:30:53 HOL-Codegenerator_Test: theory Code_Test_SMLNJ

23:30:55 Timing HOL-Codegenerator_Test (2 threads, 646.485s elapsed time, 510.204s cpu time, 13.320s GC time, factor 0.79)

23:30:55 Finished HOL-Codegenerator_Test (0:10:54 elapsed time, 0:30:24 cpu time, factor 2.79)

23:30:55 Running HOL-Nitpick_Examples ...

23:30:57 HOL-Nitpick_Examples: theory Datatype_Nits

23:30:57 HOL-Nitpick_Examples: theory Core_Nits

23:30:57 HOL-Nitpick_Examples: theory Hotel_Nits

23:30:58 HOL-Nitpick_Examples: theory Induct_Nits

23:30:58 HOL-Nitpick_Examples: theory Integer_Nits

23:30:59 HOL-Nitpick_Examples: theory Mini_Nits

23:30:59 HOL-Nitpick_Examples: theory Mono_Nits

23:30:59 HOL-Nitpick_Examples: theory Pattern_Nits

23:31:00 HOL-Nitpick_Examples: theory Quotient_Syntax

23:31:00 HOL-Nitpick_Examples: theory Quotient_Product

23:31:00 HOL-Nitpick_Examples: theory Record_Nits

23:31:00 HOL-Nitpick_Examples: theory Manual_Nits

23:31:01 HOL-Nitpick_Examples: theory Refute_Nits

23:31:05 HOL-Nitpick_Examples: theory Special_Nits

23:31:06 HOL-Nitpick_Examples: theory Tests_Nits

23:31:07 HOL-Nitpick_Examples: theory Typedef_Nits

23:31:10 HOL-Nitpick_Examples: theory Nitpick_Examples

23:33:31 Timing HOL-Decision_Procs (2 threads, 446.361s elapsed time, 688.828s cpu time, 51.676s GC time, factor 1.54)

23:33:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Decision_Procs

23:33:31 Finished HOL-Decision_Procs (0:07:29 elapsed time, 0:11:31 cpu time, factor 1.54)

23:33:31 Running HOL-Corec_Examples ...

23:33:33 HOL-Corec_Examples: theory BNF_Axiomatization

23:33:33 HOL-Corec_Examples: theory BNF_Corec

23:33:33 HOL-Corec_Examples: theory FSet

23:33:37 HOL-Corec_Examples: theory Nat_Bijection

23:33:38 HOL-Corec_Examples: theory Stream

23:33:40 HOL-Corec_Examples: theory Iterate_GPV

23:33:40 HOL-Corec_Examples: theory LFilter

23:33:43 HOL-Corec_Examples: theory Simple_Nesting

23:33:49 HOL-Corec_Examples: theory Stream_Processor

23:34:03 HOL-Corec_Examples: theory Paper_Examples

23:34:40 HOL-ex: theory Meson_Test

23:34:56 HOL-Corec_Examples: theory Merge_A

23:34:56 HOL-Corec_Examples: theory GPV_Bare_Bones

23:35:00 HOL-Corec_Examples: theory Merge_B

23:35:03 HOL-Corec_Examples: theory Merge_C

23:35:06 HOL-Corec_Examples: theory Merge_Poly

23:35:08 HOL-Corec_Examples: theory Merge_D

23:35:12 Timing HOL-ex (2 threads, 622.547s elapsed time, 960.352s cpu time, 81.096s GC time, factor 1.54)

23:35:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex

23:35:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex/document.pdf

23:35:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex/outline.pdf

23:35:12 Finished HOL-ex (0:10:38 elapsed time, 0:16:57 cpu time, factor 1.59)

23:35:12 Running HOL-Datatype_Examples ...

23:35:14 HOL-Datatype_Examples: theory BNF_Axiomatization

23:35:14 HOL-Datatype_Examples: theory FSet

23:35:15 HOL-Datatype_Examples: theory Infinite_Set

23:35:15 HOL-Corec_Examples: theory Misc_Mono

23:35:15 HOL-Datatype_Examples: theory Lift_BNF

23:35:18 HOL-Datatype_Examples: theory Milner_Tofte

23:35:18 HOL-Datatype_Examples: theory Lambda_Term

23:35:19 HOL-Datatype_Examples: theory Misc_Codatatype

23:35:21 HOL-Datatype_Examples: theory Prelim

23:35:21 HOL-Datatype_Examples: theory DTree

23:35:21 HOL-Datatype_Examples: theory Parallel

23:35:22 HOL-Datatype_Examples: theory TreeFsetI

23:35:23 HOL-Datatype_Examples: theory Gram_Lang

23:35:24 HOL-Datatype_Examples: theory Nat_Bijection

23:35:24 HOL-Datatype_Examples: theory Stream

23:35:26 HOL-Datatype_Examples: theory Process

23:35:31 HOL-Datatype_Examples: theory Stream_Processor

23:35:36 HOL-Datatype_Examples: theory Old_Datatype

23:35:37 HOL-Datatype_Examples: theory Compat

23:35:48 Timing HOL-Nitpick_Examples (2 threads, 291.191s elapsed time, 112.360s cpu time, 2.076s GC time, factor 0.39)

23:35:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nitpick_Examples

23:35:48 Finished HOL-Nitpick_Examples (0:04:53 elapsed time, 0:10:17 cpu time, factor 2.10)

23:35:48 Running HOL-Hoare_Parallel ...

23:35:50 HOL-Hoare_Parallel: theory Graph

23:35:50 HOL-Hoare_Parallel: theory OG_Com

23:35:51 HOL-Hoare_Parallel: theory Quote_Antiquote

23:35:51 HOL-Hoare_Parallel: theory RG_Com

23:35:52 HOL-Corec_Examples: theory Misc_Poly

23:35:53 HOL-Hoare_Parallel: theory RG_Tran

23:35:53 HOL-Hoare_Parallel: theory OG_Tran

23:35:55 HOL-Hoare_Parallel: theory RG_Hoare

23:35:55 HOL-Hoare_Parallel: theory OG_Hoare

23:35:56 HOL-Hoare_Parallel: theory RG_Syntax

23:35:56 HOL-Hoare_Parallel: theory OG_Tactics

23:35:56 HOL-Hoare_Parallel: theory RG_Examples

23:35:56 HOL-Hoare_Parallel: theory OG_Syntax

23:35:56 HOL-Hoare_Parallel: theory Gar_Coll

23:35:58 HOL-Hoare_Parallel: theory Mul_Gar_Coll

23:35:58 HOL-Hoare_Parallel: theory OG_Examples

23:36:01 HOL-Hoare_Parallel: theory Hoare_Parallel

23:36:09 HOL-Datatype_Examples: theory Countable

23:36:10 HOL-Datatype_Examples: theory Misc_Datatype

23:36:26 HOL-Datatype_Examples: theory Misc_Primcorec

23:36:29 HOL-Datatype_Examples: theory TreeFI

23:36:29 HOL-Datatype_Examples: theory Koenig

23:36:48 HOL-Corec_Examples: theory Small_Concrete

23:37:15 HOL-Corec_Examples: theory Stream_Friends

23:37:22 HOL-Corec_Examples: theory TLList_Friends

23:37:25 HOL-Datatype_Examples: theory Misc_Primrec

23:37:39 HOL-Corec_Examples: theory Type_Class

23:37:58 Timing HOL-Datatype_Examples (2 threads, 162.486s elapsed time, 306.088s cpu time, 33.804s GC time, factor 1.88)

23:37:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Datatype_Examples

23:37:58 Finished HOL-Datatype_Examples (0:02:45 elapsed time, 0:05:29 cpu time, factor 1.99)

23:37:58 Running HOL-Proofs-Lambda ...

23:38:00 HOL-Proofs-Lambda: theory GCD

23:38:06 Timing HOL-Corec_Examples (2 threads, 271.506s elapsed time, 486.888s cpu time, 46.320s GC time, factor 1.79)

23:38:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Corec_Examples

23:38:06 Finished HOL-Corec_Examples (0:04:33 elapsed time, 0:08:09 cpu time, factor 1.79)

23:38:06 Running HOL-IMP ...

23:38:07 HOL-IMP: theory Char_ord

23:38:07 HOL-IMP: theory List_lexord

23:38:08 HOL-IMP: theory Quotient_Syntax

23:38:08 HOL-IMP: theory Simps_Case_Conv

23:38:08 HOL-IMP: theory Quotient_Option

23:38:08 HOL-IMP: theory Quotient_Product

23:38:08 HOL-IMP: theory Quotient_Set

23:38:08 HOL-IMP: theory Extended

23:38:08 HOL-IMP: theory Quotient_List

23:38:08 HOL-IMP: theory While_Combinator

23:38:12 HOL-IMP: theory AExp

23:38:12 HOL-IMP: theory C_like

23:38:13 HOL-IMP: theory ASM

23:38:13 HOL-Proofs-Lambda: theory Code_Target_Int

23:38:14 HOL-Proofs-Lambda: theory Commutation

23:38:14 HOL-Proofs-Lambda: theory Lambda

23:38:14 HOL-IMP: theory BExp

23:38:14 HOL-Proofs-Lambda: theory ListOrder

23:38:16 HOL-IMP: theory Complete_Lattice

23:38:16 HOL-IMP: theory OO

23:38:16 HOL-IMP: theory Com

23:38:16 HOL-Proofs-Lambda: theory ParRed

23:38:16 HOL-Proofs-Lambda: theory ListApplication

23:38:17 HOL-Proofs-Lambda: theory LambdaType

23:38:17 HOL-IMP: theory ACom

23:38:17 HOL-Proofs-Lambda: theory Eta

23:38:19 HOL-Proofs-Lambda: theory ListBeta

23:38:19 HOL-Proofs-Lambda: theory InductTermi

23:38:20 HOL-IMP: theory Abs_Int_Tests

23:38:20 HOL-Proofs-Lambda: theory StrongNorm

23:38:20 HOL-IMP: theory Big_Step

23:38:20 HOL-IMP: theory Denotational

23:38:20 HOL-IMP: theory Hoare

23:38:21 HOL-IMP: theory Hoare_Examples

23:38:21 HOL-Proofs-Lambda: theory NormalForm

23:38:21 HOL-IMP: theory Hoare_Total

23:38:21 HOL-Proofs-Lambda: theory Standardization

23:38:21 HOL-IMP: theory Hoare_Sound_Complete

23:38:21 HOL-IMP: theory Hoare_Total_EX

23:38:22 HOL-IMP: theory VCG_Total_EX

23:38:22 HOL-Proofs-Lambda: theory WeakNorm

23:38:23 HOL-IMP: theory VCG

23:38:24 HOL-IMP: theory Sec_Type_Expr

23:38:24 HOL-IMP: theory Sec_Typing

23:38:25 HOL-IMP: theory Sec_TypingT

23:38:25 HOL-IMP: theory Sem_Equiv

23:38:25 HOL-IMP: theory Vars

23:38:26 HOL-IMP: theory Def_Init

23:38:26 HOL-IMP: theory Def_Init_Exp

23:38:26 HOL-IMP: theory Fold

23:38:26 HOL-IMP: theory Def_Init_Big

23:38:26 HOL-IMP: theory Live

23:38:26 HOL-IMP: theory Procs

23:38:27 HOL-IMP: theory Collecting

23:38:28 HOL-IMP: theory Procs_Dyn_Vars_Dyn

23:38:28 HOL-IMP: theory Procs_Stat_Vars_Dyn

23:38:29 HOL-IMP: theory Procs_Stat_Vars_Stat

23:38:29 HOL-IMP: theory Collecting1

23:38:29 HOL-IMP: theory Collecting_Examples

23:38:30 HOL-IMP: theory Star

23:38:30 HOL-IMP: theory Compiler

23:38:34 HOL-IMP: theory Compiler2

23:38:34 HOL-IMP: theory Def_Init_Small

23:38:34 HOL-IMP: theory Small_Step

23:38:34 HOL-IMP: theory Types

23:38:35 HOL-IMP: theory Finite_Reachable

23:38:35 HOL-IMP: theory Abs_Int_init

23:38:36 HOL-IMP: theory Abs_Int0

23:38:37 HOL-IMP: theory Abs_State

23:38:38 HOL-IMP: theory Poly_Types

23:38:38 HOL-IMP: theory Abs_Int1

23:38:39 HOL-IMP: theory Abs_Int1_const

23:38:39 HOL-IMP: theory Abs_Int1_parity

23:38:40 HOL-IMP: theory Abs_Int2

23:38:40 HOL-IMP: theory Live_True

23:38:41 HOL-IMP: theory Abs_Int2_ivl

23:38:42 HOL-IMP: theory Abs_Int3

23:38:49 Timing HOL-Hoare_Parallel (2 threads, 174.552s elapsed time, 317.104s cpu time, 4.180s GC time, factor 1.82)

23:38:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel

23:38:49 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/document.pdf

23:38:49 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/outline.pdf

23:38:49 Finished HOL-Hoare_Parallel (0:02:59 elapsed time, 0:05:24 cpu time, factor 1.80)

23:38:49 Running HOL-MicroJava ...

23:38:51 HOL-MicroJava: theory While_Combinator

23:38:53 HOL-MicroJava: theory Eisbach

23:38:53 HOL-MicroJava: theory Transitive_Closure_Table

23:38:53 HOL-MicroJava: theory Semilat

23:38:53 HOL-MicroJava: theory JBasis

23:38:53 HOL-MicroJava: theory AuxLemmas

23:38:54 HOL-MicroJava: theory Type

23:38:54 HOL-MicroJava: theory Err

23:38:54 HOL-MicroJava: theory Listn

23:38:55 HOL-MicroJava: theory Typing_Framework

23:38:55 HOL-MicroJava: theory Opt

23:38:55 HOL-MicroJava: theory Product

23:38:55 HOL-MicroJava: theory SemilatAlg

23:38:56 HOL-MicroJava: theory Kildall

23:38:56 HOL-MicroJava: theory Decl

23:38:56 HOL-MicroJava: theory SystemClasses

23:38:56 HOL-MicroJava: theory TypeRel

23:38:56 HOL-MicroJava: theory Value

23:38:57 HOL-MicroJava: theory WellForm

23:38:57 HOL-MicroJava: theory State

23:38:57 HOL-MicroJava: theory Exceptions

23:38:57 HOL-MicroJava: theory Term

23:38:58 HOL-MicroJava: theory LBVSpec

23:38:58 HOL-MicroJava: theory LBVComplete

23:38:58 HOL-MicroJava: theory LBVCorrect

23:38:59 HOL-MicroJava: theory Typing_Framework_err

23:38:59 HOL-MicroJava: theory Abstract_BV

23:39:00 HOL-MicroJava: theory Semilattices

23:39:00 HOL-MicroJava: theory JType

23:39:00 HOL-MicroJava: theory JVMType

23:39:01 HOL-MicroJava: theory WellType

23:39:01 HOL-MicroJava: theory Conform

23:39:01 HOL-MicroJava: theory Eval

23:39:02 HOL-MicroJava: theory JVMState

23:39:02 HOL-MicroJava: theory JVMInstructions

23:39:03 HOL-MicroJava: theory JVMExceptions

23:39:04 HOL-MicroJava: theory JVMExecInstr

23:39:04 HOL-MicroJava: theory JVMExec

23:39:04 HOL-MicroJava: theory DefsComp

23:39:05 HOL-MicroJava: theory Index

23:39:05 HOL-MicroJava: theory JVMDefensive

23:39:06 HOL-MicroJava: theory JVMListExample

23:39:07 HOL-MicroJava: theory TypeInf

23:39:07 HOL-MicroJava: theory Effect

23:39:07 HOL-MicroJava: theory Example

23:39:09 HOL-MicroJava: theory JListExample

23:39:10 HOL-MicroJava: theory JTypeSafe

23:39:10 HOL-MicroJava: theory TranslCompTp

23:39:11 HOL-MicroJava: theory TranslComp

23:39:11 HOL-MicroJava: theory LemmasComp

23:39:11 HOL-MicroJava: theory CorrComp

23:39:29 HOL-MicroJava: theory BVSpec

23:39:29 HOL-MicroJava: theory EffectMono

23:39:29 HOL-MicroJava: theory Altern

23:39:29 HOL-MicroJava: theory Correct

23:39:30 HOL-MicroJava: theory Typing_Framework_JVM

23:39:30 HOL-MicroJava: theory BVSpecTypeSafe

23:39:30 HOL-MicroJava: theory JVM

23:39:31 HOL-MicroJava: theory CorrCompTp

23:39:31 HOL-MicroJava: theory BVNoTypeError

23:39:31 HOL-MicroJava: theory BVExample

23:39:32 HOL-MicroJava: theory LBVJVM

23:39:33 HOL-MicroJava: theory MicroJava

23:40:37 Timing HOL-Proofs-Lambda (2 threads, 153.695s elapsed time, 174.944s cpu time, 5.848s GC time, factor 1.14)

23:40:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda

23:40:37 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda/document.pdf

23:40:37 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda/outline.pdf

23:40:37 Finished HOL-Proofs-Lambda (0:02:38 elapsed time, 0:03:01 cpu time, factor 1.14)

23:40:37 Running HOL-Imperative_HOL ...

23:40:39 HOL-Imperative_HOL: theory Adhoc_Overloading

23:40:39 HOL-Imperative_HOL: theory LaTeXsugar

23:40:39 HOL-Imperative_HOL: theory Monad_Syntax

23:40:39 HOL-Imperative_HOL: theory Nat_Bijection

23:40:39 HOL-Imperative_HOL: theory Old_Datatype

23:40:40 HOL-Imperative_HOL: theory Countable

23:40:42 HOL-Imperative_HOL: theory Code_Abstract_Nat

23:40:42 HOL-Imperative_HOL: theory Code_Target_Int

23:40:42 HOL-Imperative_HOL: theory Code_Target_Nat

23:40:42 HOL-Imperative_HOL: theory Multiset

23:40:42 HOL-Imperative_HOL: theory Code_Target_Numeral

23:40:42 HOL-Imperative_HOL: theory Heap

23:40:44 HOL-Imperative_HOL: theory Heap_Monad

23:40:46 HOL-Imperative_HOL: theory Array

23:40:47 HOL-Imperative_HOL: theory List_Sublist

23:40:47 HOL-Imperative_HOL: theory Ref

23:40:47 HOL-Imperative_HOL: theory Subarray

23:40:47 HOL-Imperative_HOL: theory Imperative_HOL

23:40:47 Timing HOL-IMP (2 threads, 155.056s elapsed time, 269.868s cpu time, 13.184s GC time, factor 1.74)

23:40:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP

23:40:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP/document.pdf

23:40:47 Finished HOL-IMP (0:02:41 elapsed time, 0:04:36 cpu time, factor 1.72)

23:40:47 Running HOL-Proofs-Extraction ...

23:40:47 HOL-Imperative_HOL: theory Linked_Lists

23:40:48 HOL-Imperative_HOL: theory Overview

23:40:48 HOL-Imperative_HOL: theory Imperative_Quicksort

23:40:50 HOL-Proofs-Extraction: theory Adhoc_Overloading

23:40:50 HOL-Proofs-Extraction: theory Binomial

23:40:50 HOL-Proofs-Extraction: theory Code_Abstract_Nat

23:40:50 HOL-Proofs-Extraction: theory Code_Target_Nat

23:40:50 HOL-Proofs-Extraction: theory GCD

23:41:18 HOL-Proofs-Extraction: theory Code_Target_Int

23:41:18 HOL-Proofs-Extraction: theory Code_Target_Numeral

23:41:19 HOL-Proofs-Extraction: theory Monad_Syntax

23:41:19 HOL-Proofs-Extraction: theory Multiset

23:41:19 HOL-Imperative_HOL: theory Imperative_Reverse

23:41:20 HOL-Proofs-Extraction: theory State_Monad

23:41:24 HOL-Imperative_HOL: theory RBT_Impl

23:41:45 HOL-Proofs-Extraction: theory Factorial_Ring

23:41:49 HOL-Imperative_HOL: theory Sorted_List

23:41:56 HOL-Imperative_HOL: theory SatChecker

23:41:59 Timing HOL-MicroJava (2 threads, 184.152s elapsed time, 283.720s cpu time, 8.768s GC time, factor 1.54)

23:41:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava

23:41:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/document.pdf

23:41:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/outline.pdf

23:41:59 Finished HOL-MicroJava (0:03:10 elapsed time, 0:04:51 cpu time, factor 1.53)

23:41:59 Running HOL-Quickcheck_Examples ...

23:42:00 HOL-Proofs-Extraction: theory Euclidean_Algorithm

23:42:01 HOL-Quickcheck_Examples: theory Completeness

23:42:01 HOL-Quickcheck_Examples: theory AList

23:42:02 HOL-Quickcheck_Examples: theory Dlist

23:42:03 HOL-Quickcheck_Examples: theory Multiset

23:42:03 HOL-Quickcheck_Examples: theory DAList

23:42:04 HOL-Quickcheck_Examples: theory Quickcheck_Interfaces

23:42:05 HOL-Quickcheck_Examples: theory Quickcheck_Lattice_Examples

23:42:05 HOL-Imperative_HOL: theory Imperative_HOL_ex

23:42:05 HOL-Quickcheck_Examples: theory Quickcheck_Nesting

23:42:05 HOL-Quickcheck_Examples: theory Quickcheck_Nesting_Example

23:42:08 HOL-Quickcheck_Examples: theory DAList_Multiset

23:42:08 HOL-Quickcheck_Examples: theory Quickcheck_Examples

23:42:11 HOL-Proofs-Extraction: theory Primes

23:42:22 HOL-Proofs-Extraction: theory Higman

23:42:22 HOL-Proofs-Extraction: theory Util

23:42:22 HOL-Proofs-Extraction: theory Euclid

23:42:24 HOL-Proofs-Extraction: theory Pigeonhole

23:42:59 HOL-Proofs-Extraction: theory QuotRem

23:43:03 HOL-Proofs-Extraction: theory Greatest_Common_Divisor

23:43:10 HOL-Proofs-Extraction: theory Warshall

23:43:13 HOL-Proofs-Extraction: theory Higman_Extraction

23:43:14 Timing HOL-Imperative_HOL (2 threads, 154.014s elapsed time, 163.008s cpu time, 5.992s GC time, factor 1.06)

23:43:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL

23:43:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/document.pdf

23:43:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/outline.pdf

23:43:14 Finished HOL-Imperative_HOL (0:02:37 elapsed time, 0:07:06 cpu time, factor 2.71)

23:43:14 Running HOL-Bali ...

23:43:17 HOL-Bali: theory Old_Recdef

23:43:18 HOL-Bali: theory Basis

23:43:19 HOL-Bali: theory Name

23:43:19 HOL-Bali: theory Table

23:43:21 HOL-Bali: theory Type

23:43:22 HOL-Quickcheck_Examples: theory Predicate_Compile_Alternative_Defs

23:43:22 HOL-Quickcheck_Examples: theory Quickcheck_Narrowing_Examples

23:43:22 HOL-Quickcheck_Examples: theory Predicate_Compile_Quickcheck

23:43:23 HOL-Quickcheck_Examples: theory Hotel_Example

23:43:23 HOL-Bali: theory Value

23:43:23 HOL-Bali: theory Term

23:43:26 Timing HOL-Proofs-Extraction (2 threads, 154.551s elapsed time, 213.476s cpu time, 9.580s GC time, factor 1.38)

23:43:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction

23:43:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/document.pdf

23:43:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/outline.pdf

23:43:26 Finished HOL-Proofs-Extraction (0:02:38 elapsed time, 0:03:38 cpu time, factor 1.37)

23:43:26 Running HOL-Predicate_Compile_Examples ...

23:43:28 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Alternative_Defs

23:43:28 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck

23:43:28 HOL-Predicate_Compile_Examples: theory Examples

23:43:29 HOL-Predicate_Compile_Examples: theory IMP_1

23:43:29 HOL-Predicate_Compile_Examples: theory IMP_2

23:43:30 HOL-Predicate_Compile_Examples: theory IMP_3

23:43:31 HOL-Predicate_Compile_Examples: theory IMP_4

23:43:33 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck_Examples

23:43:38 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Tests

23:43:39 HOL-Bali: theory Decl

23:43:41 HOL-Predicate_Compile_Examples: theory Specialisation_Examples

23:43:43 HOL-Bali: theory TypeRel

23:43:44 HOL-Bali: theory DeclConcepts

23:43:46 HOL-Bali: theory State

23:43:46 HOL-Bali: theory WellType

23:43:47 HOL-Bali: theory Conform

23:43:48 HOL-Bali: theory Eval

23:43:52 HOL-Bali: theory DefiniteAssignment

23:44:02 HOL-Bali: theory WellForm

23:44:04 HOL-Bali: theory DefiniteAssignmentCorrect

23:44:04 HOL-Bali: theory Example

23:44:06 HOL-Bali: theory TypeSafe

23:44:11 HOL-Bali: theory Evaln

23:44:15 HOL-Bali: theory AxSem

23:44:15 HOL-Bali: theory Trans

23:44:20 HOL-Bali: theory AxCompl

23:44:20 HOL-Bali: theory AxSound

23:44:21 HOL-Bali: theory AxExample

23:44:29 Timing HOL-Quickcheck_Examples (2 threads, 147.830s elapsed time, 170.336s cpu time, 4.900s GC time, factor 1.15)

23:44:29 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quickcheck_Examples

23:44:29 Finished HOL-Quickcheck_Examples (0:02:30 elapsed time, 0:04:12 cpu time, factor 1.69)

23:44:30 Running HOL-Number_Theory ...

23:44:31 HOL-Number_Theory: theory Congruence

23:44:31 HOL-Number_Theory: theory FuncSet

23:44:32 HOL-Number_Theory: theory Multiset

23:44:32 HOL-Number_Theory: theory Lattice

23:44:34 HOL-Number_Theory: theory Group

23:44:36 HOL-Number_Theory: theory FiniteProduct

23:44:37 HOL-Number_Theory: theory Ring

23:44:57 HOL-Number_Theory: theory Factorial_Ring

23:44:57 HOL-Number_Theory: theory MiscAlgebra

23:44:58 HOL-Number_Theory: theory Fib

23:45:04 HOL-Number_Theory: theory Euclidean_Algorithm

23:45:05 HOL-Predicate_Compile_Examples: theory Hotel_Example

23:45:05 HOL-Predicate_Compile_Examples: theory Code_Prolog

23:45:05 HOL-Predicate_Compile_Examples: theory Code_Prolog_Examples

23:45:07 HOL-Predicate_Compile_Examples: theory Context_Free_Grammar_Example

23:45:08 HOL-Predicate_Compile_Examples: theory Lambda_Example

23:45:08 HOL-Predicate_Compile_Examples: theory Hotel_Example_Prolog

23:45:08 HOL-Predicate_Compile_Examples: theory List_Examples

23:45:12 HOL-Number_Theory: theory Primes

23:45:12 HOL-Number_Theory: theory Cong

23:45:12 HOL-Number_Theory: theory Eratosthenes

23:45:13 HOL-Number_Theory: theory Residues

23:45:13 HOL-Predicate_Compile_Examples: theory Reg_Exp_Example

23:45:15 HOL-Number_Theory: theory Euler_Criterion

23:45:15 HOL-Number_Theory: theory Gauss

23:45:15 HOL-Number_Theory: theory Quadratic_Reciprocity

23:45:15 HOL-Number_Theory: theory Pocklington

23:45:16 HOL-Number_Theory: theory Number_Theory

23:45:21 Timing HOL-Predicate_Compile_Examples (2 threads, 112.124s elapsed time, 182.632s cpu time, 8.516s GC time, factor 1.63)

23:45:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Predicate_Compile_Examples

23:45:21 Finished HOL-Predicate_Compile_Examples (0:01:54 elapsed time, 0:04:32 cpu time, factor 2.38)

23:45:21 Running HOL-Algebra ...

23:45:23 HOL-Algebra: theory Multiset

23:45:23 HOL-Algebra: theory FuncSet

23:45:27 HOL-Algebra: theory Factorial_Ring

23:45:27 HOL-Algebra: theory Permutation

23:45:34 HOL-Algebra: theory Euclidean_Algorithm

23:45:36 Timing HOL-Bali (2 threads, 129.641s elapsed time, 203.020s cpu time, 10.724s GC time, factor 1.57)

23:45:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali

23:45:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/document.pdf

23:45:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/outline.pdf

23:45:36 Finished HOL-Bali (0:02:21 elapsed time, 0:03:38 cpu time, factor 1.55)

23:45:36 Running HOL-UNITY ...

23:45:39 HOL-UNITY: theory ListOrder

23:45:39 HOL-UNITY: theory Multiset

23:45:40 HOL-UNITY: theory UNITY

23:45:40 HOL-UNITY: theory Constrains

23:45:41 HOL-UNITY: theory Deadlock

23:45:41 HOL-UNITY: theory FP

23:45:41 HOL-UNITY: theory Network

23:45:42 HOL-UNITY: theory WFair

23:45:42 HOL-UNITY: theory SubstAx

23:45:42 HOL-Algebra: theory Primes

23:45:43 HOL-UNITY: theory Detects

23:45:43 HOL-UNITY: theory Union

23:45:44 HOL-UNITY: theory Comp

23:45:44 HOL-UNITY: theory Multiset_Order

23:45:44 HOL-UNITY: theory Follows

23:45:44 HOL-UNITY: theory Guar

23:45:45 HOL-UNITY: theory Transformers

23:45:45 HOL-UNITY: theory Extend

23:45:45 HOL-UNITY: theory ProgressSets

23:45:45 HOL-UNITY: theory Project

23:45:45 HOL-UNITY: theory Rename

23:45:46 HOL-UNITY: theory Lift_prog

23:45:46 HOL-UNITY: theory ELT

23:45:46 HOL-UNITY: theory PPROD

23:45:46 HOL-UNITY: theory UNITY_Main

23:45:47 HOL-UNITY: theory Token

23:45:47 HOL-UNITY: theory AllocBase

23:45:47 HOL-Algebra: theory Congruence

23:45:47 HOL-Algebra: theory Exponent

23:45:47 HOL-UNITY: theory Alloc

23:45:47 HOL-UNITY: theory AllocImpl

23:45:48 HOL-Algebra: theory Lattice

23:45:50 HOL-UNITY: theory Client

23:45:50 HOL-Algebra: theory Group

23:45:50 HOL-UNITY: theory Channel

23:45:50 HOL-UNITY: theory Common

23:45:50 HOL-UNITY: theory Counter

23:45:51 HOL-UNITY: theory Counterc

23:45:51 HOL-UNITY: theory Handshake

23:45:51 HOL-UNITY: theory Lift

23:45:51 HOL-Algebra: theory Bij

23:45:51 HOL-UNITY: theory Mutex

23:45:51 HOL-Algebra: theory Coset

23:45:51 HOL-UNITY: theory NSP_Bad

23:45:52 HOL-UNITY: theory PriorityAux

23:45:52 HOL-UNITY: theory Priority

23:45:52 HOL-Algebra: theory FiniteProduct

23:45:52 HOL-UNITY: theory Progress

23:45:52 HOL-UNITY: theory Reach

23:45:52 HOL-UNITY: theory TimerArray

23:45:53 HOL-UNITY: theory Reachability

23:45:53 HOL-Algebra: theory Ring

23:45:53 HOL-Algebra: theory Sylow

23:45:54 Timing HOL-Number_Theory (2 threads, 79.228s elapsed time, 134.640s cpu time, 4.332s GC time, factor 1.70)

23:45:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory

23:45:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/document.pdf

23:45:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/outline.pdf

23:45:54 Finished HOL-Number_Theory (0:01:24 elapsed time, 0:02:21 cpu time, factor 1.67)

23:45:54 Running HOL-Word-SMT_Examples ...

23:45:54 HOL-Algebra: theory Divisibility

23:45:56 HOL-Algebra: theory AbelCoset

23:45:57 HOL-Word-SMT_Examples: theory Boogie

23:45:57 HOL-Word-SMT_Examples: theory SMT_Examples

23:45:57 HOL-Algebra: theory Module

23:45:57 HOL-Word-SMT_Examples: theory SMT_Tests

23:45:59 HOL-Word-SMT_Examples: theory SMT_Word_Examples

23:46:03 HOL-Algebra: theory Ideal

23:46:07 HOL-Algebra: theory RingHom

23:46:09 HOL-Algebra: theory QuotRing

23:46:09 HOL-Algebra: theory UnivPoly

23:46:10 HOL-Algebra: theory IntRing

23:46:45 Timing HOL-Algebra (2 threads, 77.854s elapsed time, 147.996s cpu time, 8.204s GC time, factor 1.90)

23:46:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra

23:46:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/document.pdf

23:46:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline.pdf

23:46:45 Finished HOL-Algebra (0:01:23 elapsed time, 0:02:36 cpu time, factor 1.87)

23:46:45 Running Corec ...

23:46:47 Corec: theory Setup

23:46:47 Corec: theory BNF_Corec

23:46:47 Corec: theory FSet

23:46:52 Corec: theory Corec

23:46:53 Timing HOL-UNITY (2 threads, 69.791s elapsed time, 106.036s cpu time, 4.532s GC time, factor 1.52)

23:46:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY

23:46:53 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/document.pdf

23:46:53 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/outline.pdf

23:46:53 Finished HOL-UNITY (0:01:16 elapsed time, 0:01:54 cpu time, factor 1.51)

23:46:53 Running HOL-SET_Protocol ...

23:46:55 HOL-SET_Protocol: theory Nat_Bijection

23:46:56 HOL-SET_Protocol: theory Message_SET

23:46:58 Timing HOL-Word-SMT_Examples (2 threads, 61.455s elapsed time, 80.544s cpu time, 0.760s GC time, factor 1.31)

23:46:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-SMT_Examples

23:46:58 Finished HOL-Word-SMT_Examples (0:01:04 elapsed time, 0:01:25 cpu time, factor 1.34)

23:46:58 Running Datatypes ...

23:46:59 HOL-SET_Protocol: theory Event_SET

23:47:00 HOL-SET_Protocol: theory Public_SET

23:47:00 Datatypes: theory Setup

23:47:00 HOL-SET_Protocol: theory Cardholder_Registration

23:47:00 HOL-SET_Protocol: theory Merchant_Registration

23:47:01 Datatypes: theory BNF_Axiomatization

23:47:01 Datatypes: theory Cardinal_Notations

23:47:01 Datatypes: theory FSet

23:47:01 Datatypes: theory Nat_Bijection

23:47:01 Datatypes: theory Old_Datatype

23:47:01 HOL-SET_Protocol: theory Purchase

23:47:03 Datatypes: theory Countable

23:47:03 HOL-SET_Protocol: theory SET_Protocol

23:47:04 Datatypes: theory Simps_Case_Conv

23:47:04 Datatypes: theory Datatypes

23:47:41 Timing Corec (2 threads, 52.487s elapsed time, 84.280s cpu time, 5.356s GC time, factor 1.61)

23:47:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec

23:47:41 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec/corec.pdf

23:47:41 Finished Corec (0:00:56 elapsed time, 0:01:28 cpu time, factor 1.56)

23:47:41 Running HOL-Quotient_Examples ...

23:47:43 HOL-Quotient_Examples: theory FuncSet

23:47:43 HOL-Quotient_Examples: theory Congruence

23:47:44 HOL-Quotient_Examples: theory Lift_DList

23:47:44 HOL-Quotient_Examples: theory Lattice

23:47:44 HOL-Quotient_Examples: theory Lift_FSet

23:47:44 Timing Datatypes (2 threads, 40.916s elapsed time, 68.756s cpu time, 4.960s GC time, factor 1.68)

23:47:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes

23:47:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes/datatypes.pdf

23:47:44 Finished Datatypes (0:00:45 elapsed time, 0:01:13 cpu time, factor 1.60)

23:47:44 Running HOL-Metis_Examples ...

23:47:45 HOL-Quotient_Examples: theory Lift_Set

23:47:45 HOL-Quotient_Examples: theory Lifting_Code_Dt_Test

23:47:46 HOL-Quotient_Examples: theory Group

23:47:46 HOL-Metis_Examples: theory Dense_Linear_Order

23:47:46 HOL-Metis_Examples: theory Binary_Tree

23:47:48 HOL-Metis_Examples: theory FuncSet

23:47:48 HOL-Quotient_Examples: theory Int_Pow

23:47:48 HOL-Quotient_Examples: theory Multiset

23:47:48 HOL-Metis_Examples: theory Abstraction

23:47:48 HOL-Metis_Examples: theory Function_Algebras

23:47:48 HOL-Metis_Examples: theory Message

23:47:48 HOL-Metis_Examples: theory Set_Algebras

23:47:49 HOL-Metis_Examples: theory Big_O

23:47:49 HOL-Metis_Examples: theory Sets

23:47:50 HOL-Metis_Examples: theory Tarski

23:47:51 HOL-Metis_Examples: theory Clausification

23:47:51 HOL-Metis_Examples: theory Trans_Closure

23:47:51 HOL-Metis_Examples: theory Type_Encodings

23:47:51 HOL-Metis_Examples: theory Proxies

23:47:51 Timing HOL-SET_Protocol (2 threads, 54.451s elapsed time, 90.688s cpu time, 1.792s GC time, factor 1.67)

23:47:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol

23:47:51 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/document.pdf

23:47:51 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/outline.pdf

23:47:51 Finished HOL-SET_Protocol (0:00:58 elapsed time, 0:01:35 cpu time, factor 1.64)

23:47:51 Running HOL-Analysis-ex ...

23:47:52 HOL-Quotient_Examples: theory Quotient_Syntax

23:47:53 HOL-Quotient_Examples: theory Lift_Fun

23:47:53 HOL-Quotient_Examples: theory Quotient_Message

23:47:54 HOL-Quotient_Examples: theory Quotient_Option

23:47:54 HOL-Quotient_Examples: theory Quotient_Product

23:47:54 HOL-Quotient_Examples: theory Quotient_Rat

23:47:55 HOL-Quotient_Examples: theory Quotient_Set

23:47:55 HOL-Quotient_Examples: theory Quotient_List

23:47:56 HOL-Quotient_Examples: theory DList

23:47:56 HOL-Quotient_Examples: theory Quotient_FSet

23:47:57 HOL-Quotient_Examples: theory Quotient_Int

23:47:57 HOL-Analysis-ex: theory Approximations

23:48:30 Timing HOL-Metis_Examples (2 threads, 42.626s elapsed time, 56.128s cpu time, 2.188s GC time, factor 1.32)

23:48:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Metis_Examples

23:48:30 Finished HOL-Metis_Examples (0:00:44 elapsed time, 0:01:10 cpu time, factor 1.56)

23:48:30 Running HOL-Probability-ex ...

23:48:33 Timing HOL-Quotient_Examples (2 threads, 49.114s elapsed time, 74.836s cpu time, 6.456s GC time, factor 1.52)

23:48:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quotient_Examples

23:48:33 Finished HOL-Quotient_Examples (0:00:51 elapsed time, 0:02:10 cpu time, factor 2.55)

23:48:33 Running HOL-Isar_Examples ...

23:48:35 HOL-Isar_Examples: theory Lattice_Syntax

23:48:35 HOL-Isar_Examples: theory Multiset

23:48:37 HOL-Probability-ex: theory Dining_Cryptographers

23:48:37 HOL-Probability-ex: theory Koepf_Duermuth_Countermeasure

23:48:38 HOL-Probability-ex: theory Measure_Not_CCC

23:48:40 HOL-Isar_Examples: theory Factorial_Ring

23:48:42 Warning: missing document directory

23:48:42 Timing HOL-Analysis-ex (2 threads, 43.747s elapsed time, 45.644s cpu time, 0.460s GC time, factor 1.04)

23:48:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis-ex

23:48:42 Finished HOL-Analysis-ex (0:00:49 elapsed time, 0:00:51 cpu time, factor 1.04)

23:48:42 Running Tutorial ...

23:48:44 Tutorial: theory ToyList_Test

23:48:45 Tutorial: theory AB

23:48:45 Tutorial: theory ABexpr

23:48:45 Tutorial: theory AdvancedInd

23:48:46 Tutorial: theory Base

23:48:46 Tutorial: theory CTL

23:48:46 Tutorial: theory CTLind

23:48:47 HOL-Isar_Examples: theory Euclidean_Algorithm

23:48:47 Tutorial: theory PDL

23:48:47 Tutorial: theory CodeGen

23:48:47 Tutorial: theory Nested

23:48:49 Tutorial: theory Even

23:48:49 Tutorial: theory Advanced

23:48:50 Tutorial: theory Fundata

23:48:51 Tutorial: theory Ifexpr

23:48:51 Tutorial: theory Itrev

23:48:51 Tutorial: theory Mutual

23:48:51 Tutorial: theory Option2

23:48:52 Tutorial: theory Plus

23:48:52 Tutorial: theory Star

23:48:52 Tutorial: theory ToyList

23:48:52 Tutorial: theory Tree

23:48:53 Tutorial: theory Trie

23:48:53 Tutorial: theory Tree2

23:48:53 Tutorial: theory appendix

23:48:53 Tutorial: theory case_exprs

23:48:53 Tutorial: theory fakenat

23:48:54 Tutorial: theory fun0

23:48:55 HOL-Isar_Examples: theory Primes

23:48:55 Tutorial: theory natsum

23:48:55 Tutorial: theory pairs2

23:48:55 Tutorial: theory prime_def

23:48:55 Tutorial: theory simp

23:48:55 Tutorial: theory simp2

23:48:55 Tutorial: theory types

23:48:55 Tutorial: theory unfoldnested

23:48:59 HOL-Isar_Examples: theory First_Order_Logic

23:48:59 HOL-Isar_Examples: theory Basic_Logic

23:48:59 HOL-Isar_Examples: theory Cantor

23:48:59 HOL-Isar_Examples: theory Drinker

23:48:59 HOL-Isar_Examples: theory Expr_Compiler

23:48:59 HOL-Isar_Examples: theory Group

23:48:59 HOL-Isar_Examples: theory Group_Context

23:48:59 HOL-Isar_Examples: theory Group_Notepad

23:49:00 HOL-Isar_Examples: theory Hoare

23:49:00 HOL-Isar_Examples: theory Knaster_Tarski

23:49:00 HOL-Isar_Examples: theory Fibonacci

23:49:00 HOL-Isar_Examples: theory Hoare_Ex

23:49:00 HOL-Isar_Examples: theory Mutilated_Checkerboard

23:49:01 HOL-Isar_Examples: theory Peirce

23:49:01 HOL-Isar_Examples: theory Puzzle

23:49:01 HOL-Isar_Examples: theory Structured_Statements

23:49:01 HOL-Isar_Examples: theory Summation

23:49:01 HOL-Isar_Examples: theory Higher_Order_Logic

23:49:07 Timing HOL-Isar_Examples (2 threads, 28.861s elapsed time, 52.940s cpu time, 2.196s GC time, factor 1.83)

23:49:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples

23:49:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/document.pdf

23:49:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/outline.pdf

23:49:07 Finished HOL-Isar_Examples (0:00:33 elapsed time, 0:00:58 cpu time, factor 1.76)

23:49:07 Running HOL-Nonstandard_Analysis-Examples ...

23:49:07 Tutorial: theory Message

23:49:07 Tutorial: theory Documents

23:49:09 Tutorial: theory Event

23:49:09 HOL-Nonstandard_Analysis-Examples: theory Multiset

23:49:09 Tutorial: theory Public

23:49:10 Tutorial: theory NS_Public

23:49:11 Tutorial: theory Setup

23:49:11 Tutorial: theory Basic

23:49:11 Tutorial: theory Blast

23:49:11 Tutorial: theory Force

23:49:11 Tutorial: theory Pairs

23:49:11 Tutorial: theory Records

23:49:11 Tutorial: theory Overloading

23:49:11 Tutorial: theory Axioms

23:49:12 Tutorial: theory Numbers

23:49:12 Tutorial: theory Typedefs

23:49:13 Tutorial: theory Recur

23:49:13 Tutorial: theory Functions

23:49:13 Tutorial: theory Relations

23:49:13 Tutorial: theory TPrimes

23:49:13 Tutorial: theory Tacticals

23:49:13 Tutorial: theory Forward

23:49:13 Tutorial: theory Examples

23:49:13 Tutorial: theory find2

23:49:13 HOL-Nonstandard_Analysis-Examples: theory Factorial_Ring

23:49:15 Warning: missing document directory

23:49:15 Timing HOL-Probability-ex (2 threads, 36.995s elapsed time, 47.120s cpu time, 1.024s GC time, factor 1.27)

23:49:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability-ex

23:49:15 Finished HOL-Probability-ex (0:00:45 elapsed time, 0:00:55 cpu time, factor 1.22)

23:49:15 Running HOL-Hoare ...

23:49:17 HOL-Hoare: theory Arith2

23:49:17 HOL-Hoare: theory Heap

23:49:17 HOL-Hoare: theory Hoare_Logic

23:49:18 HOL-Hoare: theory Hoare_Logic_Abort

23:49:19 Timing Tutorial (2 threads, 30.240s elapsed time, 55.508s cpu time, 7.016s GC time, factor 1.84)

23:49:19 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial

23:49:19 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial/tutorial.pdf

23:49:19 Finished Tutorial (0:00:36 elapsed time, 0:01:01 cpu time, factor 1.68)

23:49:19 Running HOL-Cardinals ...

23:49:19 HOL-Hoare: theory Examples

23:49:19 HOL-Hoare: theory HeapSyntax

23:49:19 HOL-Hoare: theory Pointer_Examples

23:49:19 HOL-Hoare: theory SchorrWaite

23:49:20 HOL-Hoare: theory Pointers0

23:49:20 HOL-Nonstandard_Analysis-Examples: theory Euclidean_Algorithm

23:49:21 HOL-Cardinals: theory Order_Union

23:49:21 HOL-Cardinals: theory Cardinal_Notations

23:49:21 HOL-Cardinals: theory Fun_More

23:49:21 HOL-Cardinals: theory Order_Relation_More

23:49:21 HOL-Cardinals: theory Wellorder_Extension

23:49:21 HOL-Hoare: theory ExamplesAbort

23:49:21 HOL-Cardinals: theory Wellfounded_More

23:49:21 HOL-Hoare: theory HeapSyntaxAbort

23:49:21 HOL-Cardinals: theory Wellorder_Relation

23:49:21 HOL-Cardinals: theory Wellorder_Embedding

23:49:21 HOL-Hoare: theory SepLogHeap

23:49:22 HOL-Hoare: theory Pointer_ExamplesAbort

23:49:22 HOL-Hoare: theory Separation

23:49:22 HOL-Cardinals: theory Wellorder_Constructions

23:49:22 HOL-Hoare: theory Hoare

23:49:23 HOL-Cardinals: theory Cardinal_Order_Relation

23:49:23 HOL-Cardinals: theory Ordinal_Arithmetic

23:49:24 HOL-Cardinals: theory Cardinal_Arithmetic

23:49:24 HOL-Cardinals: theory Cardinals

23:49:24 HOL-Cardinals: theory Bounded_Set

23:49:30 HOL-Nonstandard_Analysis-Examples: theory Primes

23:49:31 HOL-Nonstandard_Analysis-Examples: theory NSPrimes

23:49:37 Timing HOL-Nonstandard_Analysis-Examples (2 threads, 27.933s elapsed time, 48.860s cpu time, 1.900s GC time, factor 1.75)

23:49:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis-Examples

23:49:37 Finished HOL-Nonstandard_Analysis-Examples (0:00:30 elapsed time, 0:00:51 cpu time, factor 1.69)

23:49:37 Running HOL-Induct ...

23:49:39 HOL-Induct: theory Old_Datatype

23:49:40 HOL-Induct: theory Common_Patterns

23:49:41 Timing HOL-Cardinals (2 threads, 20.221s elapsed time, 37.104s cpu time, 1.412s GC time, factor 1.83)

23:49:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals

23:49:41 Finished HOL-Cardinals (0:00:22 elapsed time, 0:00:39 cpu time, factor 1.75)

23:49:41 Running HOL-Matrix_LP ...

23:49:42 HOL-Induct: theory Com

23:49:42 HOL-Induct: theory ABexp

23:49:42 Timing HOL-Hoare (2 threads, 22.887s elapsed time, 41.420s cpu time, 1.208s GC time, factor 1.81)

23:49:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare

23:49:42 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/document.pdf

23:49:42 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/outline.pdf

23:49:42 Finished HOL-Hoare (0:00:26 elapsed time, 0:00:46 cpu time, factor 1.72)

23:49:42 Running HOL-SPARK-Examples ...

23:49:43 HOL-Matrix_LP: theory Compute_Oracle

23:49:43 HOL-Matrix_LP: theory Lattice_Algebras

23:49:44 HOL-Matrix_LP: theory ComputeHOL

23:49:45 HOL-SPARK-Examples: theory RMD_Lemmas

23:49:45 HOL-SPARK-Examples: theory RMD

23:49:45 HOL-SPARK-Examples: theory Greatest_Common_Divisor

23:49:45 HOL-Induct: theory Comb

23:49:45 HOL-Induct: theory Nested_Datatype

23:49:45 HOL-SPARK-Examples: theory Longest_Increasing_Subsequence

23:49:45 HOL-SPARK-Examples: theory RMD_Specification

23:49:46 HOL-Induct: theory Sexp

23:49:46 HOL-SPARK-Examples: theory F

23:49:46 HOL-Induct: theory SList

23:49:46 HOL-Induct: theory Ordinals

23:49:46 HOL-Induct: theory PropLog

23:49:47 HOL-Induct: theory QuoDataType

23:49:48 HOL-Induct: theory QuoNestedDataType

23:49:48 HOL-Induct: theory Sigma_Algebra

23:49:48 HOL-SPARK-Examples: theory Hash

23:49:49 HOL-Induct: theory Term

23:49:49 HOL-Matrix_LP: theory ComputeFloat

23:49:49 HOL-Matrix_LP: theory ComputeNumeral

23:49:50 HOL-SPARK-Examples: theory K_L

23:49:50 HOL-Matrix_LP: theory LP

23:49:50 HOL-Matrix_LP: theory Matrix

23:49:50 HOL-Induct: theory Tree

23:49:50 HOL-SPARK-Examples: theory K_R

23:49:51 HOL-SPARK-Examples: theory R_L

23:49:51 HOL-Matrix_LP: theory SparseMatrix

23:49:51 HOL-SPARK-Examples: theory R_R

23:49:52 HOL-SPARK-Examples: theory Round

23:49:52 HOL-SPARK-Examples: theory S_L

23:49:53 HOL-SPARK-Examples: theory S_R

23:49:54 HOL-SPARK-Examples: theory Sqrt

23:49:54 HOL-Matrix_LP: theory Cplex

23:50:00 Timing HOL-Induct (2 threads, 18.766s elapsed time, 33.944s cpu time, 5.192s GC time, factor 1.81)

23:50:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct

23:50:00 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/document.pdf

23:50:00 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/outline.pdf

23:50:00 Finished HOL-Induct (0:00:22 elapsed time, 0:00:38 cpu time, factor 1.72)

23:50:00 Running HOL-Statespace ...

23:50:02 HOL-Statespace: theory DistinctTreeProver

23:50:02 Timing HOL-SPARK-Examples (2 threads, 17.201s elapsed time, 29.184s cpu time, 0.744s GC time, factor 1.70)

23:50:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Examples

23:50:02 Finished HOL-SPARK-Examples (0:00:19 elapsed time, 0:00:31 cpu time, factor 1.60)

23:50:02 Running HOLCF-ex ...

23:50:03 HOL-Statespace: theory StateFun

23:50:03 HOL-Statespace: theory StateSpaceLocale

23:50:04 Timing HOL-Matrix_LP (2 threads, 18.172s elapsed time, 32.020s cpu time, 1.136s GC time, factor 1.76)

23:50:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP

23:50:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/document.pdf

23:50:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/outline.pdf

23:50:04 Finished HOL-Matrix_LP (0:00:22 elapsed time, 0:00:37 cpu time, factor 1.66)

23:50:04 Running Isar_Ref ...

23:50:04 HOL-Statespace: theory StateSpaceSyntax

23:50:04 HOL-Statespace: theory StateSpaceEx

23:50:05 HOLCF-ex: theory Infinite_Set

23:50:05 HOLCF-ex: theory Concurrency_Monad

23:50:05 HOLCF-ex: theory Countable_Set

23:50:06 HOLCF-ex: theory Countable_Complete_Lattices

23:50:06 Isar_Ref: theory Adhoc_Overloading

23:50:06 Isar_Ref: theory Base

23:50:06 Isar_Ref: theory Dlist

23:50:06 Isar_Ref: theory First_Order_Logic

23:50:06 Isar_Ref: theory Document_Preparation

23:50:06 Isar_Ref: theory FSet

23:50:07 HOLCF-ex: theory Dnat

23:50:07 Isar_Ref: theory Framework

23:50:07 HOLCF-ex: theory Domain_Proofs

23:50:07 Isar_Ref: theory Generic

23:50:08 Isar_Ref: theory Inner_Syntax

23:50:08 Isar_Ref: theory Old_Datatype

23:50:08 HOLCF-ex: theory Fix2

23:50:08 HOLCF-ex: theory Hoare

23:50:08 HOLCF-ex: theory Letrec

23:50:09 HOLCF-ex: theory Loop

23:50:09 HOLCF-ex: theory Pattern_Match

23:50:09 HOLCF-ex: theory Powerdomain_ex

23:50:09 Isar_Ref: theory Old_Recdef

23:50:09 Isar_Ref: theory Outer_Syntax

23:50:09 HOLCF-ex: theory Order_Continuity

23:50:10 Isar_Ref: theory Preface

23:50:10 Isar_Ref: theory Proof

23:50:10 Isar_Ref: theory HOL_Specific

23:50:10 Isar_Ref: theory Proof_Script

23:50:10 HOLCF-ex: theory Extended_Nat

23:50:11 Isar_Ref: theory Quick_Reference

23:50:11 Isar_Ref: theory Spec

23:50:11 Isar_Ref: theory Symbols

23:50:11 Isar_Ref: theory Synopsis

23:50:11 HOLCF-ex: theory Stream

23:50:13 HOLCF-ex: theory Dagstuhl

23:50:13 HOLCF-ex: theory Focus_ex

23:50:20 Timing HOL-Statespace (2 threads, 16.370s elapsed time, 18.568s cpu time, 0.616s GC time, factor 1.13)

23:50:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace

23:50:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/document.pdf

23:50:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/outline.pdf

23:50:20 Finished HOL-Statespace (0:00:19 elapsed time, 0:00:22 cpu time, factor 1.14)

23:50:20 Timing HOLCF-ex (2 threads, 14.953s elapsed time, 27.476s cpu time, 1.096s GC time, factor 1.84)

23:50:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-ex

23:50:20 Finished HOLCF-ex (0:00:17 elapsed time, 0:00:30 cpu time, factor 1.70)

23:50:20 Running HOLCF-Library ...

23:50:20 Running HOLCF-FOCUS ...

23:50:23 HOLCF-Library: theory Infinite_Set

23:50:23 HOLCF-Library: theory Bool_Discrete

23:50:23 HOLCF-FOCUS: theory Infinite_Set

23:50:23 HOLCF-Library: theory Char_Discrete

23:50:23 HOLCF-Library: theory Countable_Set

23:50:23 HOLCF-Library: theory Defl_Bifinite

23:50:23 HOLCF-FOCUS: theory Countable_Set

23:50:24 HOLCF-Library: theory Countable_Complete_Lattices

23:50:24 HOLCF-FOCUS: theory Countable_Complete_Lattices

23:50:24 HOLCF-Library: theory Int_Discrete

23:50:24 HOLCF-Library: theory List_Cpo

23:50:25 HOLCF-Library: theory Nat_Discrete

23:50:25 HOLCF-Library: theory Sum_Cpo

23:50:25 HOLCF-Library: theory List_Predomain

23:50:26 HOLCF-Library: theory Option_Cpo

23:50:26 HOLCF-Library: theory Order_Continuity

23:50:27 HOLCF-FOCUS: theory Order_Continuity

23:50:27 HOLCF-Library: theory Extended_Nat

23:50:28 HOLCF-FOCUS: theory Extended_Nat

23:50:28 Timing Isar_Ref (2 threads, 14.594s elapsed time, 26.760s cpu time, 1.472s GC time, factor 1.83)

23:50:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref

23:50:28 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref/isar-ref.pdf

23:50:28 Finished Isar_Ref (0:00:23 elapsed time, 0:00:35 cpu time, factor 1.50)

23:50:28 Running HOLCF-Tutorial ...

23:50:28 HOLCF-FOCUS: theory Stream

23:50:28 HOLCF-Library: theory Stream

23:50:30 HOLCF-Library: theory HOLCF_Library

23:50:30 HOLCF-FOCUS: theory Fstream

23:50:30 HOLCF-FOCUS: theory Fstreams

23:50:30 HOLCF-FOCUS: theory FOCUS

23:50:30 HOLCF-Tutorial: theory Domain_ex

23:50:30 HOLCF-Tutorial: theory Fixrec_ex

23:50:30 HOLCF-FOCUS: theory Buffer

23:50:30 HOLCF-FOCUS: theory Stream_adm

23:50:32 HOLCF-FOCUS: theory Buffer_adm

23:50:33 HOLCF-Tutorial: theory New_Domain

23:50:36 Timing HOLCF-FOCUS (2 threads, 12.898s elapsed time, 25.092s cpu time, 0.832s GC time, factor 1.95)

23:50:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-FOCUS

23:50:36 Finished HOLCF-FOCUS (0:00:15 elapsed time, 0:00:27 cpu time, factor 1.77)

23:50:36 Running HOL-TLA-Memory ...

23:50:37 Timing HOLCF-Library (2 threads, 14.100s elapsed time, 26.152s cpu time, 1.000s GC time, factor 1.85)

23:50:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Library

23:50:37 Finished HOLCF-Library (0:00:16 elapsed time, 0:00:28 cpu time, factor 1.71)

23:50:37 Running HOL-ZF ...

23:50:39 HOL-TLA-Memory: theory RPCMemoryParams

23:50:39 HOL-TLA-Memory: theory MemoryParameters

23:50:39 HOL-TLA-Memory: theory ProcedureInterface

23:50:39 HOL-ZF: theory Multiset

23:50:39 HOL-ZF: theory HOLZF

23:50:39 HOL-TLA-Memory: theory RPCParameters

23:50:39 HOL-TLA-Memory: theory Memory

23:50:40 HOL-ZF: theory Zet

23:50:41 HOL-TLA-Memory: theory MemClerkParameters

23:50:41 HOL-TLA-Memory: theory RPC

23:50:41 HOL-TLA-Memory: theory MemClerk

23:50:42 HOL-TLA-Memory: theory MemoryImplementation

23:50:44 HOL-ZF: theory LProd

23:50:44 Timing HOLCF-Tutorial (2 threads, 11.693s elapsed time, 15.440s cpu time, 0.480s GC time, factor 1.32)

23:50:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial

23:50:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/document.pdf

23:50:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/outline.pdf

23:50:44 Finished HOLCF-Tutorial (0:00:15 elapsed time, 0:00:19 cpu time, factor 1.26)

23:50:44 Running HOL-Hahn_Banach ...

23:50:44 HOL-ZF: theory MainZF

23:50:44 HOL-ZF: theory Games

23:50:46 HOL-Hahn_Banach: theory Nat_Bijection

23:50:46 HOL-Hahn_Banach: theory Infinite_Set

23:50:46 HOL-Hahn_Banach: theory Old_Datatype

23:50:46 HOL-Hahn_Banach: theory Set_Algebras

23:50:47 HOL-Hahn_Banach: theory Zorn_Lemma

23:50:48 HOL-Hahn_Banach: theory Countable

23:50:49 HOL-Hahn_Banach: theory Countable_Set

23:50:50 HOL-Hahn_Banach: theory Continuum_Not_Denumerable

23:50:50 HOL-Hahn_Banach: theory Bounds

23:50:50 HOL-Hahn_Banach: theory Vector_Space

23:50:51 HOL-Hahn_Banach: theory Linearform

23:50:51 HOL-Hahn_Banach: theory Subspace

23:50:51 HOL-Hahn_Banach: theory Function_Order

23:50:51 HOL-Hahn_Banach: theory Normed_Space

23:50:52 HOL-Hahn_Banach: theory Function_Norm

23:50:52 HOL-Hahn_Banach: theory Hahn_Banach_Ext_Lemmas

23:50:52 HOL-Hahn_Banach: theory Hahn_Banach_Sup_Lemmas

23:50:52 HOL-Hahn_Banach: theory Hahn_Banach_Lemmas

23:50:53 HOL-Hahn_Banach: theory Hahn_Banach

23:50:53 Timing HOL-ZF (2 threads, 10.744s elapsed time, 20.652s cpu time, 0.892s GC time, factor 1.92)

23:50:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF

23:50:53 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/document.pdf

23:50:53 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/outline.pdf

23:50:53 Finished HOL-ZF (0:00:15 elapsed time, 0:00:26 cpu time, factor 1.72)

23:50:53 Running HOL-Unix ...

23:50:53 Timing HOL-TLA-Memory (2 threads, 13.956s elapsed time, 24.096s cpu time, 0.660s GC time, factor 1.73)

23:50:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Memory

23:50:53 Finished HOL-TLA-Memory (0:00:16 elapsed time, 0:00:26 cpu time, factor 1.60)

23:50:54 Running IOA-NTP ...

23:50:55 HOL-Unix: theory Nested_Environment

23:50:55 HOL-Unix: theory Sublist

23:50:56 IOA-NTP: theory Lemmas

23:50:56 IOA-NTP: theory Multiset

23:50:56 IOA-NTP: theory Packet

23:50:56 HOL-Unix: theory Unix

23:50:57 IOA-NTP: theory Action

23:50:58 IOA-NTP: theory Receiver

23:50:58 IOA-NTP: theory Abschannel

23:50:59 Timing HOL-Hahn_Banach (2 threads, 9.879s elapsed time, 19.180s cpu time, 0.900s GC time, factor 1.94)

23:50:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach

23:50:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/document.pdf

23:50:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/outline.pdf

23:50:59 Finished HOL-Hahn_Banach (0:00:14 elapsed time, 0:00:24 cpu time, factor 1.73)

23:50:59 Running HOL-Mirabelle-ex ...

23:50:59 IOA-NTP: theory Sender

23:51:00 IOA-NTP: theory Spec

23:51:00 IOA-NTP: theory Impl

23:51:00 IOA-NTP: theory Correctness

23:51:00 HOL-Mirabelle-ex: theory Ex

23:51:05 Timing IOA-NTP (2 threads, 7.723s elapsed time, 13.132s cpu time, 0.480s GC time, factor 1.70)

23:51:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-NTP

23:51:05 Finished IOA-NTP (0:00:10 elapsed time, 0:00:16 cpu time, factor 1.50)

23:51:05 Running HOLCF-IMP ...

23:51:06 Timing HOL-Unix (2 threads, 8.718s elapsed time, 16.560s cpu time, 0.868s GC time, factor 1.90)

23:51:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix

23:51:06 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/document.pdf

23:51:06 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/outline.pdf

23:51:06 Finished HOL-Unix (0:00:12 elapsed time, 0:00:20 cpu time, factor 1.69)

23:51:06 Running HOL-NanoJava ...

23:51:07 Timing HOL-Mirabelle-ex (2 threads, 5.710s elapsed time, 0.028s cpu time, 0.000s GC time, factor 0.00)

23:51:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle-ex

23:51:07 Finished HOL-Mirabelle-ex (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.21)

23:51:07 Running Codegen ...

23:51:07 HOLCF-IMP: theory AExp

23:51:07 HOL-NanoJava: theory Term

23:51:08 HOLCF-IMP: theory BExp

23:51:09 Codegen: theory Adaptation

23:51:09 Codegen: theory Evaluation

23:51:09 Codegen: theory Further

23:51:10 HOL-NanoJava: theory Decl

23:51:10 Codegen: theory Inductive_Predicate

23:51:10 HOLCF-IMP: theory Com

23:51:10 HOL-NanoJava: theory TypeRel

23:51:10 HOL-NanoJava: theory State

23:51:11 Codegen: theory Introduction

23:51:11 HOL-NanoJava: theory AxSem

23:51:11 HOL-NanoJava: theory OpSem

23:51:11 HOLCF-IMP: theory Big_Step

23:51:12 HOLCF-IMP: theory Denotational

23:51:12 HOL-NanoJava: theory Equivalence

23:51:12 Codegen: theory Refinement

23:51:12 Codegen: theory Foundations

23:51:12 HOLCF-IMP: theory HoareEx

23:51:12 HOL-NanoJava: theory Example

23:51:14 Timing HOLCF-IMP (2 threads, 6.254s elapsed time, 11.836s cpu time, 0.388s GC time, factor 1.89)

23:51:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP

23:51:14 Finished HOLCF-IMP (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.61)

23:51:14 Running IOA-ABP ...

23:51:15 Timing HOL-NanoJava (2 threads, 6.036s elapsed time, 10.552s cpu time, 0.576s GC time, factor 1.75)

23:51:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava

23:51:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/document.pdf

23:51:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/outline.pdf

23:51:15 Finished HOL-NanoJava (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.55)

23:51:15 Running Prog_Prove ...

23:51:17 Prog_Prove: theory Bool_nat_list

23:51:17 Prog_Prove: theory Basics

23:51:17 Prog_Prove: theory LaTeXsugar

23:51:17 IOA-ABP: theory Lemmas

23:51:17 IOA-ABP: theory Packet

23:51:17 Prog_Prove: theory Isar

23:51:17 IOA-ABP: theory Action

23:51:18 Prog_Prove: theory Logic

23:51:18 Timing Codegen (2 threads, 5.606s elapsed time, 10.868s cpu time, 0.452s GC time, factor 1.94)

23:51:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen

23:51:18 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen/codegen.pdf

23:51:18 Finished Codegen (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.46)

23:51:18 Running HOL-TPTP ...

23:51:18 Prog_Prove: theory MyList

23:51:19 IOA-ABP: theory Abschannel

23:51:19 IOA-ABP: theory Env

23:51:19 Prog_Prove: theory Types_and_funs

23:51:19 IOA-ABP: theory Receiver

23:51:20 HOL-TPTP: theory ATP_Theory_Export

23:51:20 HOL-TPTP: theory MaSh_Export_Base

23:51:20 IOA-ABP: theory Sender

23:51:20 HOL-TPTP: theory MaSh_Eval

23:51:20 HOL-TPTP: theory THF_Arith

23:51:20 IOA-ABP: theory Abschannel_finite

23:51:20 HOL-TPTP: theory TPTP_Parser

23:51:20 IOA-ABP: theory Spec

23:51:20 IOA-ABP: theory Impl

23:51:20 IOA-ABP: theory Impl_finite

23:51:21 IOA-ABP: theory Correctness

23:51:22 HOL-TPTP: theory TPTP_Interpret

23:51:22 HOL-TPTP: theory TPTP_Proof_Reconstruction

23:51:23 HOL-TPTP: theory Refute

23:51:23 Timing IOA-ABP (2 threads, 5.377s elapsed time, 9.740s cpu time, 0.164s GC time, factor 1.81)

23:51:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ABP

23:51:23 Finished IOA-ABP (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.49)

23:51:23 Running HOL-SPARK-Manual ...

23:51:24 HOL-TPTP: theory ATP_Problem_Import

23:51:25 Timing HOL-TPTP (2 threads, 4.837s elapsed time, 5.616s cpu time, 0.088s GC time, factor 1.16)

23:51:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TPTP

23:51:25 Finished HOL-TPTP (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.10)

23:51:25 Running HOL-IMPP ...

23:51:25 Timing Prog_Prove (2 threads, 5.275s elapsed time, 10.280s cpu time, 0.700s GC time, factor 1.95)

23:51:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove

23:51:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove/prog-prove.pdf

23:51:25 Finished Prog_Prove (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.49)

23:51:25 Running Implementation ...

23:51:25 HOL-SPARK-Manual: theory Greatest_Common_Divisor

23:51:25 HOL-SPARK-Manual: theory Complex_Types

23:51:26 HOL-SPARK-Manual: theory Proc1

23:51:26 HOL-SPARK-Manual: theory Proc2

23:51:26 HOL-IMPP: theory Com

23:51:26 HOL-SPARK-Manual: theory VC_Principles

23:51:27 HOL-SPARK-Manual: theory Reference

23:51:27 HOL-SPARK-Manual: theory Simple_Greatest_Common_Divisor

23:51:27 HOL-SPARK-Manual: theory Example_Verification

23:51:28 Implementation: theory Base

23:51:28 Implementation: theory Integration

23:51:28 Implementation: theory Eq

23:51:28 Implementation: theory Isar

23:51:28 Implementation: theory Local_Theory

23:51:28 HOL-IMPP: theory Natural

23:51:28 Implementation: theory ML

23:51:28 Implementation: theory Prelim

23:51:29 Implementation: theory Proof

23:51:29 HOL-IMPP: theory Hoare

23:51:29 Implementation: theory Syntax

23:51:29 Implementation: theory Tactic

23:51:29 HOL-IMPP: theory Misc

23:51:30 HOL-IMPP: theory EvenOdd

23:51:30 Implementation: theory Logic

23:51:31 Timing HOL-IMPP (2 threads, 3.926s elapsed time, 6.680s cpu time, 0.164s GC time, factor 1.70)

23:51:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMPP

23:51:31 Finished HOL-IMPP (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.44)

23:51:31 Running Functions ...

23:51:33 Functions: theory Functions

23:51:33 Timing HOL-SPARK-Manual (2 threads, 4.712s elapsed time, 8.336s cpu time, 0.192s GC time, factor 1.77)

23:51:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual

23:51:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/document.pdf

23:51:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/outline.pdf

23:51:33 Finished HOL-SPARK-Manual (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.50)

23:51:33 Running HOL-IOA ...

23:51:34 Timing Implementation (2 threads, 3.242s elapsed time, 5.572s cpu time, 0.056s GC time, factor 1.72)

23:51:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation

23:51:34 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation/implementation.pdf

23:51:34 Finished Implementation (0:00:08 elapsed time, 0:00:10 cpu time, factor 1.22)

23:51:34 Running HOL-TLA-Inc ...

23:51:36 HOL-IOA: theory Asig

23:51:36 HOL-IOA: theory IOA

23:51:36 HOL-TLA-Inc: theory Inc

23:51:36 HOL-IOA: theory Solve

23:51:37 Timing Functions (2 threads, 2.684s elapsed time, 3.796s cpu time, 0.212s GC time, factor 1.41)

23:51:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions

23:51:37 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions/functions.pdf

23:51:37 Finished Functions (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.12)

23:51:37 Running HOL-Lattice ...

23:51:39 Timing HOL-IOA (2 threads, 2.520s elapsed time, 3.660s cpu time, 0.132s GC time, factor 1.45)

23:51:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IOA

23:51:39 Finished HOL-IOA (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.21)

23:51:39 Timing HOL-TLA-Inc (2 threads, 2.210s elapsed time, 3.796s cpu time, 0.132s GC time, factor 1.72)

23:51:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Inc

23:51:39 Finished HOL-TLA-Inc (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.36)

23:51:39 Running HOL-Word-Examples ...

23:51:39 Running Classes ...

23:51:39 HOL-Lattice: theory Orders

23:51:40 HOL-Lattice: theory Bounds

23:51:40 HOL-Lattice: theory Lattice

23:51:41 HOL-Lattice: theory CompleteLattice

23:51:41 Classes: theory Setup

23:51:41 Classes: theory Classes

23:51:41 HOL-Word-Examples: theory WordBitwise

23:51:42 HOL-Word-Examples: theory WordExamples

23:51:43 Timing HOL-Lattice (2 threads, 2.013s elapsed time, 3.544s cpu time, 0.000s GC time, factor 1.76)

23:51:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice

23:51:43 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/document.pdf

23:51:43 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/outline.pdf

23:51:43 Finished HOL-Lattice (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.39)

23:51:43 Running Locales ...

23:51:44 Timing HOL-Word-Examples (2 threads, 2.062s elapsed time, 3.436s cpu time, 0.080s GC time, factor 1.67)

23:51:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-Examples

23:51:44 Finished HOL-Word-Examples (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.28)

23:51:44 Running IOA-Storage ...

23:51:45 Locales: theory Examples

23:51:45 Timing Classes (2 threads, 1.970s elapsed time, 2.208s cpu time, 0.000s GC time, factor 1.12)

23:51:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes

23:51:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes/classes.pdf

23:51:45 Finished Classes (0:00:05 elapsed time, 0:00:05 cpu time, factor 0.99)

23:51:45 Running Eisbach ...

23:51:45 Locales: theory Examples1

23:51:45 Locales: theory Examples2

23:51:45 Locales: theory Examples3

23:51:46 IOA-Storage: theory Action

23:51:47 Eisbach: theory Base

23:51:47 Eisbach: theory Manual

23:51:47 Eisbach: theory Preface

23:51:47 IOA-Storage: theory Impl

23:51:47 IOA-Storage: theory Spec

23:51:47 IOA-Storage: theory Correctness

23:51:48 Timing Locales (2 threads, 1.556s elapsed time, 2.700s cpu time, 0.000s GC time, factor 1.74)

23:51:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales

23:51:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales/locales.pdf

23:51:48 Finished Locales (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.16)

23:51:48 Timing IOA-Storage (2 threads, 1.564s elapsed time, 2.348s cpu time, 0.000s GC time, factor 1.50)

23:51:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-Storage

23:51:48 Finished IOA-Storage (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.16)

23:51:48 Running HOL-Mutabelle ...

23:51:48 Running Main ...

23:51:50 Main: theory Main_Doc

23:51:50 HOL-Mutabelle: theory Refute

23:51:50 Timing Eisbach (2 threads, 1.231s elapsed time, 1.620s cpu time, 0.000s GC time, factor 1.32)

23:51:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach

23:51:50 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach/eisbach.pdf

23:51:50 Finished Eisbach (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.02)

23:51:50 Running HOL-Proofs-ex ...

23:51:51 HOL-Mutabelle: theory MutabelleExtra

23:51:52 Timing HOL-Mutabelle (2 threads, 1.137s elapsed time, 1.232s cpu time, 0.000s GC time, factor 1.08)

23:51:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mutabelle

23:51:52 Finished HOL-Mutabelle (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.01)

23:51:52 Running HOL-Nunchaku ...

23:51:52 Timing Main (2 threads, 1.157s elapsed time, 1.236s cpu time, 0.000s GC time, factor 1.07)

23:51:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main

23:51:52 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main/main.pdf

23:51:52 Finished Main (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.96)

23:51:52 Running HOL-Types_To_Sets ...

23:51:52 HOL-Proofs-ex: theory Hilbert_Classical

23:51:52 HOL-Proofs-ex: theory Drinker

23:51:53 HOL-Proofs-ex: theory XML_Data

23:51:53 HOL-Proofs-ex: theory Proof_Terms

23:51:54 HOL-Nunchaku: theory Nunchaku

23:51:54 Timing HOL-Proofs-ex (2 threads, 1.045s elapsed time, 1.944s cpu time, 0.000s GC time, factor 1.86)

23:51:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-ex

23:51:54 Finished HOL-Proofs-ex (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.26)

23:51:54 Running Sugar ...

23:51:54 HOL-Types_To_Sets: theory Prerequisites

23:51:54 HOL-Types_To_Sets: theory Types_To_Sets

23:51:54 HOL-Types_To_Sets: theory Finite

23:51:54 HOL-Types_To_Sets: theory T2_Spaces

23:51:55 Timing HOL-Nunchaku (2 threads, 0.909s elapsed time, 0.976s cpu time, 0.000s GC time, factor 1.07)

23:51:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nunchaku

23:51:55 Finished HOL-Nunchaku (0:00:02 elapsed time)

23:51:55 Running HOL-Import ...

23:51:55 Timing HOL-Types_To_Sets (2 threads, 0.960s elapsed time, 1.508s cpu time, 0.000s GC time, factor 1.57)

23:51:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Types_To_Sets

23:51:55 Finished HOL-Types_To_Sets (0:00:02 elapsed time, 0:00:03 cpu time)

23:51:55 Running IOA-ex ...

23:51:56 Sugar: theory LaTeXsugar

23:51:56 Sugar: theory OptionalSugar

23:51:56 Sugar: theory Sugar

23:51:57 HOL-Import: theory Import_Setup

23:51:57 HOL-Import: theory HOL_Light_Maps

23:51:58 Timing Sugar (2 threads, 0.886s elapsed time, 1.060s cpu time, 0.000s GC time, factor 1.20)

23:51:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar

23:51:58 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar/sugar.pdf

23:51:58 Finished Sugar (0:00:04 elapsed time, 0:00:03 cpu time, factor 0.98)

23:51:58 Warning: missing document directory

23:51:58 Skipping theories "HOL_Light_Import" (undefined HOL_LIGHT_BUNDLE)

23:51:58 Timing HOL-Import (2 threads, 0.922s elapsed time, 1.596s cpu time, 0.000s GC time, factor 1.73)

23:51:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Import

23:51:58 Finished HOL-Import (0:00:02 elapsed time, 0:00:03 cpu time)

23:51:58 Running JEdit ...

23:51:58 Running HOL-TLA-Buffer ...

23:51:58 IOA-ex: theory TrivEx

23:51:58 IOA-ex: theory TrivEx2

23:51:59 Timing IOA-ex (2 threads, 0.743s elapsed time, 1.536s cpu time, 0.000s GC time, factor 2.07)

23:51:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ex

23:51:59 Finished IOA-ex (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.21)

23:51:59 Running How_to_Prove_it ...

23:52:00 JEdit: theory Base

23:52:00 HOL-TLA-Buffer: theory Buffer

23:52:00 JEdit: theory JEdit

23:52:00 HOL-TLA-Buffer: theory DBuffer

23:52:01 How_to_Prove_it: theory How_to_Prove_it

23:52:01 Timing HOL-TLA-Buffer (2 threads, 0.660s elapsed time, 1.116s cpu time, 0.000s GC time, factor 1.69)

23:52:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Buffer

23:52:01 Finished HOL-TLA-Buffer (0:00:02 elapsed time, 0:00:03 cpu time)

23:52:01 Running HOL-Prolog ...

23:52:02 Timing How_to_Prove_it (2 threads, 0.386s elapsed time, 0.488s cpu time, 0.000s GC time, factor 1.26)

23:52:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it

23:52:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it/how_to_prove_it.pdf

23:52:02 Finished How_to_Prove_it (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.97)

23:52:02 Running Typeclass_Hierarchy ...

23:52:03 HOL-Prolog: theory HOHH

23:52:03 HOL-Prolog: theory Func

23:52:03 HOL-Prolog: theory Test

23:52:03 HOL-Prolog: theory Type

23:52:04 Timing HOL-Prolog (2 threads, 0.296s elapsed time, 0.472s cpu time, 0.000s GC time, factor 1.59)

23:52:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Prolog

23:52:04 Finished HOL-Prolog (0:00:02 elapsed time)

23:52:05 Typeclass_Hierarchy: theory Typeclass_Hierarchy

23:52:07 Timing Typeclass_Hierarchy (2 threads, 0.320s elapsed time, 0.408s cpu time, 0.000s GC time, factor 1.27)

23:52:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy

23:52:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy/typeclass_hierarchy.pdf

23:52:07 Finished Typeclass_Hierarchy (0:00:04 elapsed time, 0:00:03 cpu time, factor 0.95)

23:52:08 Timing JEdit (2 threads, 0.708s elapsed time, 0.744s cpu time, 0.000s GC time, factor 1.05)

23:52:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit

23:52:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit/jedit.pdf

23:52:08 Finished JEdit (0:00:09 elapsed time, 0:00:09 cpu time, factor 0.96)

23:52:08

23:52:08 === TIMING ===

23:52:08

23:52:08 Group timing: 1:46:29 elapsed time, 2:56:21 cpu time, factor 1.66

23:52:08 Group doc: 0:04:10 elapsed time, 0:05:57 cpu time, factor 1.43

23:52:08 Group main: 0:26:17 elapsed time, 0:45:45 cpu time, factor 1.74

23:52:08 Group ZF: 0:01:41 elapsed time, 0:02:46 cpu time, factor 1.64

23:52:08 Overall: 0:53:47 elapsed time, 4:34:30 cpu time, factor 5.10

23:52:08 Archiving artifacts

23:52:09 Started calculate disk usage of build

23:52:09 Finished Calculation of disk usage of build in 0 seconds

23:52:16 Started calculate disk usage of workspace

23:52:16 Finished Calculation of disk usage of workspace in 0 seconds

23:52:16 No emails were triggered.

23:52:16 Finished: SUCCESS