Skip to content
Success

Console Output

22:56:12 Started by upstream project "isabelle-repo" build number 666

22:56:12 originally caused by:

22:56:12 Started by an SCM change

22:56:12 [EnvInject] - Loading node environment variables.

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

22:56:12 [isabelle-repo-makeall] $ hg showconfig paths.default

22:56:12 [isabelle-repo-makeall] $ hg pull --rev 6be5ec46688f58a91e9299741ea6aa308217ec4f

22:56:13 pulling from http://isabelle.in.tum.de/repos/isabelle/

22:56:13 searching for changes

22:56:13 adding changesets

22:56:13 adding manifests

22:56:13 adding file changes

22:56:13 added 1 changesets with 1 changes to 1 files

22:56:13 (run 'hg update' to get a working copy)

22:56:13 [isabelle-repo-makeall] $ hg update --clean --rev 6be5ec46688f58a91e9299741ea6aa308217ec4f

22:56:13 1 files updated, 0 files merged, 0 files removed, 0 files unresolved

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

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

22:56:13 [isabelle-repo-makeall] $ hg id --branch

22:56:13 No emails were triggered.

22:56:13 [isabelle-repo-makeall] $ /bin/sh -xe /tmp/hudson6539623080747660304.sh

22:56:13 + Admin/jenkins/run_build makeall

22:56:13 + set -e

22:56:13 + PROFILE=makeall

22:56:13 + shift

22:56:13 + bin/isabelle components -a

22:56:13 + bin/isabelle jedit -bf

22:56:13 ### Building Isabelle/Scala ...

22:58:10 ### Building Isabelle/jEdit ...

22:58:35 + bin/isabelle ci_build_makeall

22:58:40

22:58:40 === CONFIGURATION ===

22:58:40

22:58:40 ISABELLE_BUILD_OPTIONS=""

22:58:40

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

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

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

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

22:58:40

22:58:40 === BUILD ===

22:58:40

22:58:40 Build started at Tue, 3 Jan 2017 21:58:40 GMT

22:58:40 Isabelle id 6be5ec46688f

22:58:40

22:58:40 === LOG ===

22:58:40

22:58:40 Session Pure/Pure

22:58:41 Session CCL/CCL

22:58:41 Session CTT/CTT

22:58:41 Session Cube/Cube

22:58:41 Session FOL/FOL

22:58:41 Session FOL/FOL-ex

22:58:41 Session FOLP/FOLP

22:58:41 Session FOLP/FOLP-ex

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

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

22:58:42 Session Doc/Codegen_Basics

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

22:58:43 Session HOL/HOL-Eisbach

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

22:58:43 Session HOL/HOL-Hahn_Banach

22:58:43 Session HOL/HOL-Hoare

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

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

22:58:43 Session HOL/HOL-IMPP

22:58:43 Session HOL/HOL-IOA

22:58:43 Session HOL/HOL-Imperative_HOL

22:58:44 Session HOL/HOL-Import

22:58:44 Session HOL/HOL-Induct

22:58:44 Session HOL/HOL-Isar_Examples

22:58:44 Session HOL/HOL-Lattice

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

22:58:44 Session HOL/HOL-Codegenerator_Test

22:58:44 Session HOL/HOL-Matrix_LP

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

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

22:58:44 Session HOL/HOL-Mirabelle

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

22:58:44 Session HOL/HOL-Mutabelle

22:58:44 Session HOL/HOL-NanoJava

22:58:44 Session HOL/HOL-Nitpick_Examples

22:58:44 Session HOL/HOL-Nominal

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

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

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

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

22:58:45 Session HOL/HOL-Nunchaku

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

22:58:45 Session HOL/HOL-Prolog

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

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

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

22:58:45 Session HOL/HOL-Statespace

22:58:45 Session HOL/HOL-TLA

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

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

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

22:58:46 Session HOL/HOL-TPTP

22:58:46 Session HOL/HOL-Types_To_Sets

22:58:46 Session HOL/HOL-Unix

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

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

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

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

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

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

22:58:46 Session HOL/HOL-ZF

22:58:46 Session HOL/HOL-ex

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

22:58:46 Session HOL/HOLCF-FOCUS

22:58:46 Session HOL/HOLCF-IMP

22:58:46 Session HOL/HOLCF-Library

22:58:46 Session HOL/HOLCF-Tutorial

22:58:46 Session HOL/HOLCF-ex

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

22:58:46 Session HOL/IOA-ABP

22:58:46 Session HOL/IOA-NTP

22:58:46 Session HOL/IOA-Storage

22:58:46 Session HOL/IOA-ex

22:58:46 Session Doc/How_to_Prove_it

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

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

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

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

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

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

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

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

22:58:47 Session Doc/Typeclass_Hierarchy_Basics

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

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

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

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

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

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

22:58:47 Session LCF/LCF

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

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

22:58:47 Session Unsorted/SML

22:58:47 Session Sequents/Sequents

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

22:58:47 Session Unsorted/Spec_Check

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

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

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

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

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

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

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

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

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

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

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

22:58:48 Cleaning Pure ...

22:58:48 Cleaning SML ...

22:58:48 Cleaning Sequents ...

22:58:48 Cleaning Sledgehammer ...

22:58:48 Cleaning Spec_Check ...

22:58:48 Cleaning System ...

22:58:48 Cleaning ZF ...

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

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

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

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

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

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

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

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

22:58:48 Cleaning Nitpick ...

22:58:48 Cleaning Logics_ZF ...

22:58:48 Cleaning Logics ...

22:58:48 Cleaning LCF ...

22:58:48 Cleaning Intro ...

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

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

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

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

22:58:48 Cleaning HOL ...

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

22:58:49 Cleaning HOLCF ...

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

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

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

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

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

22:58:49 Cleaning IOA ...

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

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

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

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

22:58:49 Cleaning How_to_Prove_it ...

22:58:49 Cleaning Implementation ...

22:58:49 Cleaning Isar_Ref ...

22:58:49 Cleaning JEdit ...

22:58:49 Cleaning Locales ...

22:58:49 Cleaning Main ...

22:58:49 Cleaning Prog_Prove ...

22:58:49 Cleaning Sugar ...

22:58:49 Cleaning Tutorial ...

22:58:49 Cleaning Typeclass_Hierarchy_Basics ...

22:58:49 Cleaning Typeclass_Hierarchy ...

22:58:49 Cleaning Functions ...

22:58:49 Cleaning FOLP ...

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

22:58:49 Cleaning FOL ...

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

22:58:49 Cleaning Eisbach ...

22:58:49 Cleaning Datatypes ...

22:58:49 Cleaning Cube ...

22:58:49 Cleaning Corec ...

22:58:49 Cleaning Codegen_Basics ...

22:58:49 Cleaning Codegen ...

22:58:49 Cleaning Classes ...

22:58:49 Cleaning CTT ...

22:58:49 Cleaning CCL ...

22:58:49 Building Pure ...

22:59:01 Pure: theory Pure

22:59:01 Pure: theory ML_Bootstrap

22:59:04 Warning: missing document directory

22:59:04 Timing Pure (1 threads, 0.591s elapsed time, 0.592s cpu time, 0.000s GC time, factor 1.00)

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

22:59:04 Finished Pure (0:00:14 elapsed time, 0:00:14 cpu time, factor 1.00)

22:59:04 Building HOL ...

22:59:04 Building ZF ...

22:59:04 Building HOL-Proofs ...

22:59:04 ZF: theory IFOL

22:59:04 HOL-Proofs: theory Proofs

22:59:05 HOL: theory Code_Generator

22:59:05 HOL-Proofs: theory Code_Generator

22:59:05 ZF: theory FOL

22:59:06 ZF: theory ZF

22:59:07 ZF: theory upair

22:59:07 ZF: theory pair

22:59:07 ZF: theory Bool

22:59:07 ZF: theory equalities

22:59:07 HOL: theory HOL

22:59:07 HOL-Proofs: theory HOL

22:59:07 ZF: theory Fixedpt

22:59:07 ZF: theory Sum

22:59:08 ZF: theory func

22:59:08 ZF: theory Perm

22:59:08 ZF: theory QPair

22:59:08 ZF: theory Trancl

22:59:08 ZF: theory EquivClass

22:59:09 ZF: theory WF

22:59:09 ZF: theory Order

22:59:09 ZF: theory Ordinal

22:59:09 ZF: theory OrdQuant

22:59:09 ZF: theory OrderArith

22:59:09 ZF: theory Nat_ZF

22:59:10 ZF: theory Epsilon

22:59:10 ZF: theory OrderType

22:59:10 ZF: theory Inductive_ZF

22:59:10 ZF: theory Finite

22:59:10 ZF: theory Cardinal

22:59:10 HOL: theory Argo

22:59:10 ZF: theory Univ

22:59:10 HOL: theory Ctr_Sugar

22:59:11 ZF: theory Arith

22:59:11 ZF: theory QUniv

22:59:11 HOL-Proofs: theory Argo

22:59:11 HOL-Proofs: theory Ctr_Sugar

22:59:11 ZF: theory Datatype_ZF

22:59:11 HOL: theory Orderings

22:59:11 ZF: theory ArithSimp

22:59:11 ZF: theory Int_ZF

22:59:11 ZF: theory CardinalArith

22:59:12 HOL: theory SAT

22:59:12 HOL-Proofs: theory Orderings

22:59:12 ZF: theory List_ZF

22:59:12 ZF: theory Bin

22:59:12 HOL-Proofs: theory SAT

22:59:12 HOL: theory Groups

22:59:12 ZF: theory IntDiv_ZF

22:59:13 ZF: theory Main_ZF

22:59:13 ZF: theory AC

22:59:13 ZF: theory Zorn

22:59:13 ZF: theory Cardinal_AC

22:59:13 ZF: theory Main

22:59:14 ZF: theory InfDatatype

22:59:14 ZF: theory Main_ZFC

22:59:14 HOL-Proofs: theory Groups

22:59:14 HOL: theory Lattices

22:59:16 HOL: theory Set

22:59:17 HOL-Proofs: theory Lattices

22:59:18 HOL: theory Fun

22:59:18 HOL: theory Typedef

22:59:18 HOL: theory Rings

22:59:18 HOL: theory Complete_Lattices

22:59:21 HOL: theory Inductive

22:59:21 HOL-Proofs: theory Set

22:59:22 HOL: theory Product_Type

22:59:23 HOL: theory Complete_Partial_Order

22:59:24 HOL: theory Sum_Type

22:59:25 HOL-Proofs: theory Fun

22:59:26 HOL-Proofs: theory Typedef

22:59:26 HOL-Proofs: theory Rings

22:59:27 HOL: theory Nat

22:59:27 HOL-Proofs: theory Complete_Lattices

22:59:29 HOL: theory Fields

22:59:29 HOL: theory Meson

22:59:29 HOL: theory ATP

22:59:31 HOL: theory Metis

22:59:31 HOL-Proofs: theory Inductive

22:59:33 HOL-Proofs: theory Product_Type

22:59:33 HOL: theory Finite_Set

22:59:34 HOL: theory Relation

22:59:35 HOL-Proofs: theory Complete_Partial_Order

22:59:35 HOL: theory Transitive_Closure

22:59:35 HOL-Proofs: theory Sum_Type

22:59:36 HOL: theory Wellfounded

22:59:37 HOL: theory Fun_Def_Base

22:59:37 HOL: theory Hilbert_Choice

22:59:37 HOL: theory Wfrec

22:59:37 HOL: theory Order_Relation

22:59:37 Timing ZF (2 threads, 21.320s elapsed time, 35.392s cpu time, 4.640s GC time, factor 1.66)

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

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

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

22:59:37 Finished ZF (0:00:32 elapsed time, 0:00:54 cpu time, factor 1.66)

22:59:37 HOL: theory BNF_Wellorder_Relation

22:59:37 HOL: theory Zorn

22:59:37 Building FOL ...

22:59:37 HOL: theory BNF_Wellorder_Embedding

22:59:37 FOL: theory IFOL

22:59:38 HOL: theory BNF_Wellorder_Constructions

22:59:38 FOL: theory FOL

22:59:38 HOL: theory BNF_Cardinal_Order_Relation

22:59:39 HOL-Proofs: theory Nat

22:59:39 HOL: theory BNF_Cardinal_Arithmetic

22:59:39 HOL: theory BNF_Def

22:59:41 HOL: theory BNF_Composition

22:59:41 HOL: theory Basic_BNFs

22:59:42 HOL: theory BNF_Fixpoint_Base

22:59:42 HOL-Proofs: theory Fields

22:59:42 Timing FOL (2 threads, 2.302s elapsed time, 2.576s cpu time, 0.136s GC time, factor 1.12)

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

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

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

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

22:59:42 Building FOLP ...

22:59:43 FOLP: theory IFOLP

22:59:43 HOL-Proofs: theory Meson

22:59:43 FOLP: theory FOLP

22:59:43 HOL-Proofs: theory ATP

22:59:44 HOL: theory BNF_Least_Fixpoint

22:59:45 Timing FOLP (2 threads, 0.813s elapsed time, 0.820s cpu time, 0.000s GC time, factor 1.01)

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

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

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

22:59:45 ZF-UNITY: theory Acc

22:59:45 ZF-UNITY: theory FoldSet

22:59:45 ZF-UNITY: theory GenPrefix

22:59:45 ZF-UNITY: theory Multiset

22:59:45 HOL-Proofs: theory Metis

22:59:45 ZF-UNITY: theory State

22:59:45 ZF-UNITY: theory UNITY

22:59:46 ZF-UNITY: theory Constrains

22:59:46 ZF-UNITY: theory MultisetSum

22:59:46 HOL: theory Basic_BNF_LFPs

22:59:46 ZF-UNITY: theory Monotonicity

22:59:46 HOL: theory Transfer

22:59:46 ZF-UNITY: theory FP

22:59:46 ZF-UNITY: theory Increasing

22:59:46 ZF-UNITY: theory WFair

22:59:46 ZF-UNITY: theory SubstAx

22:59:47 ZF-UNITY: theory Follows

22:59:47 ZF-UNITY: theory Mutex

22:59:47 ZF-UNITY: theory Union

22:59:47 HOL: theory Num

22:59:47 ZF-UNITY: theory Comp

22:59:48 ZF-UNITY: theory Guar

22:59:48 ZF-UNITY: theory AllocBase

22:59:48 ZF-UNITY: theory ClientImpl

22:59:48 ZF-UNITY: theory Distributor

22:59:49 HOL-Proofs: theory Finite_Set

22:59:49 ZF-UNITY: theory Merge

22:59:49 ZF-UNITY: theory AllocImpl

22:59:50 HOL: theory Power

22:59:52 HOL: theory Groups_Big

22:59:54 HOL: theory Equiv_Relations

22:59:54 HOL: theory Lifting

22:59:55 HOL-Proofs: theory Relation

22:59:55 HOL: theory Lifting_Set

22:59:56 HOL: theory Option

22:59:56 HOL: theory Quotient

22:59:56 HOL: theory Extraction

22:59:57 HOL: theory Lattices_Big

22:59:58 HOL-Proofs: theory Transitive_Closure

22:59:58 HOL: theory Partial_Function

22:59:59 HOL: theory Fun_Def

23:00:00 HOL: theory Int

23:00:02 HOL-Proofs: theory Wellfounded

23:00:02 HOL: theory Nat_Transfer

23:00:02 HOL: theory Parity

23:00:03 Timing ZF-UNITY (2 threads, 17.874s elapsed time, 31.856s cpu time, 1.176s GC time, factor 1.78)

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

23:00:03 Finished ZF-UNITY (0:00:18 elapsed time, 0:00:32 cpu time, factor 1.76)

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

23:00:03 ZF-Constructible: theory Formula

23:00:03 ZF-Constructible: theory MetaExists

23:00:03 ZF-Constructible: theory Normal

23:00:04 ZF-Constructible: theory Reflection

23:00:04 HOL-Proofs: theory Fun_Def_Base

23:00:04 HOL: theory Divides

23:00:04 ZF-Constructible: theory Relative

23:00:04 HOL-Proofs: theory Hilbert_Choice

23:00:06 ZF-Constructible: theory L_axioms

23:00:06 ZF-Constructible: theory Wellorderings

23:00:06 HOL-Proofs: theory Wfrec

23:00:06 ZF-Constructible: theory WFrec

23:00:06 HOL-Proofs: theory Order_Relation

23:00:07 ZF-Constructible: theory WF_absolute

23:00:07 ZF-Constructible: theory Datatype_absolute

23:00:07 HOL-Proofs: theory BNF_Wellorder_Relation

23:00:07 HOL-Proofs: theory Zorn

23:00:07 ZF-Constructible: theory Rank

23:00:08 ZF-Constructible: theory Separation

23:00:08 HOL-Proofs: theory BNF_Wellorder_Embedding

23:00:08 ZF-Constructible: theory Internalize

23:00:08 ZF-Constructible: theory AC_in_L

23:00:10 ZF-Constructible: theory Rec_Separation

23:00:10 ZF-Constructible: theory Rank_Separation

23:00:10 HOL: theory Code_Numeral

23:00:10 HOL: theory Numeral_Simprocs

23:00:10 ZF-Constructible: theory Satisfies_absolute

23:00:10 HOL-Proofs: theory BNF_Wellorder_Constructions

23:00:11 HOL: theory SMT

23:00:11 HOL: theory Semiring_Normalization

23:00:11 ZF-Constructible: theory DPow_absolute

23:00:12 HOL: theory Set_Interval

23:00:13 HOL: theory Groebner_Basis

23:00:15 HOL: theory Conditionally_Complete_Lattices

23:00:15 HOL: theory Filter

23:00:15 HOL-Proofs: theory BNF_Cardinal_Order_Relation

23:00:16 HOL: theory Presburger

23:00:18 HOL: theory Sledgehammer

23:00:19 HOL-Proofs: theory BNF_Cardinal_Arithmetic

23:00:19 HOL: theory List

23:00:21 HOL-Proofs: theory BNF_Def

23:00:22 Timing ZF-Constructible (2 threads, 14.660s elapsed time, 27.320s cpu time, 5.020s GC time, factor 1.86)

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

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

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

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

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

23:00:22 ZF-ex: theory BinEx

23:00:22 ZF-ex: theory CoUnit

23:00:22 ZF-ex: theory Commutation

23:00:22 ZF-ex: theory Group

23:00:22 ZF-ex: theory LList

23:00:22 ZF-ex: theory Limit

23:00:23 ZF-ex: theory Ring

23:00:23 ZF-ex: theory NatSum

23:00:23 ZF-ex: theory Primes

23:00:23 ZF-ex: theory Ramsey

23:00:23 ZF-ex: theory misc

23:00:26 HOL-Proofs: theory BNF_Composition

23:00:26 HOL: theory Groups_List

23:00:26 HOL-Proofs: theory Basic_BNFs

23:00:26 HOL: theory Map

23:00:27 HOL: theory Random

23:00:27 HOL: theory Enum

23:00:27 HOL-Proofs: theory BNF_Fixpoint_Base

23:00:29 HOL: theory String

23:00:30 HOL: theory BNF_Greatest_Fixpoint

23:00:30 HOL: theory Predicate

23:00:30 HOL-Proofs: theory BNF_Least_Fixpoint

23:00:31 HOL: theory Lazy_Sequence

23:00:32 HOL: theory Limited_Sequence

23:00:32 HOL: theory Typerep

23:00:33 HOL-Proofs: theory Basic_BNF_LFPs

23:00:33 Timing ZF-ex (2 threads, 10.296s elapsed time, 14.576s cpu time, 0.700s GC time, factor 1.42)

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

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

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

23:00:33 HOL: theory Code_Evaluation

23:00:33 ZF-Induct: theory Acc

23:00:33 ZF-Induct: theory Binary_Trees

23:00:33 ZF-Induct: theory Comb

23:00:33 ZF-Induct: theory Datatypes

23:00:33 HOL-Proofs: theory Transfer

23:00:33 ZF-Induct: theory FoldSet

23:00:33 ZF-Induct: theory ListN

23:00:33 ZF-Induct: theory Mutil

23:00:33 ZF-Induct: theory Ntree

23:00:33 ZF-Induct: theory Multiset

23:00:34 ZF-Induct: theory Primrec

23:00:34 ZF-Induct: theory PropLog

23:00:34 ZF-Induct: theory Rmap

23:00:34 ZF-Induct: theory Term

23:00:34 ZF-Induct: theory Tree_Forest

23:00:34 HOL: theory Quickcheck_Random

23:00:34 ZF-Induct: theory Brouwer

23:00:35 HOL-Proofs: theory Num

23:00:36 HOL: theory Quickcheck_Exhaustive

23:00:36 HOL: theory Quickcheck_Narrowing

23:00:39 HOL-Proofs: theory Power

23:00:39 HOL: theory Random_Pred

23:00:40 HOL: theory Record

23:00:40 HOL: theory Random_Sequence

23:00:41 HOL: theory Predicate_Compile

23:00:41 HOL: theory Nitpick

23:00:42 Timing ZF-Induct (2 threads, 6.194s elapsed time, 10.100s cpu time, 0.428s GC time, factor 1.63)

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

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

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

23:00:42 Finished ZF-Induct (0:00:08 elapsed time, 0:00:13 cpu time, factor 1.58)

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

23:00:42 HOL-Proofs: theory Groups_Big

23:00:42 ZF-AC: theory AC_Equiv

23:00:42 ZF-AC: theory AC18_AC19

23:00:42 ZF-AC: theory AC7_AC9

23:00:42 ZF-AC: theory Cardinal_aux

23:00:42 ZF-AC: theory Hartog

23:00:42 ZF-AC: theory WO6_WO1

23:00:42 ZF-AC: theory AC16_lemmas

23:00:42 ZF-AC: theory AC16_WO4

23:00:43 ZF-AC: theory DC

23:00:43 ZF-AC: theory HH

23:00:43 ZF-AC: theory AC15_WO6

23:00:43 ZF-AC: theory AC17_AC1

23:00:43 ZF-AC: theory WO1_AC

23:00:43 ZF-AC: theory WO1_WO7

23:00:43 ZF-AC: theory WO2_AC16

23:00:45 HOL: theory Main

23:00:47 HOL: theory Archimedean_Field

23:00:47 HOL: theory Binomial

23:00:48 HOL-Proofs: theory Equiv_Relations

23:00:48 HOL: theory GCD

23:00:49 Timing ZF-AC (2 threads, 5.441s elapsed time, 9.092s cpu time, 0.444s GC time, factor 1.67)

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

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

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

23:00:49 Finished ZF-AC (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.59)

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

23:00:49 FOL-ex: theory If

23:00:49 FOL-ex: theory Classical

23:00:50 FOL-ex: theory Intro

23:00:50 FOL-ex: theory Miniscope

23:00:50 FOL-ex: theory Nat

23:00:50 FOL-ex: theory Nat_Class

23:00:50 FOL-ex: theory Natural_Numbers

23:00:50 FOL-ex: theory Prolog

23:00:50 FOL-ex: theory Propositional_Cla

23:00:50 FOL-ex: theory Quantifiers_Cla

23:00:50 FOL-ex: theory Foundation

23:00:50 FOL-ex: theory Intuitionistic

23:00:50 FOL-ex: theory Propositional_Int

23:00:50 FOL-ex: theory Quantifiers_Int

23:00:50 HOL-Proofs: theory Lifting

23:00:51 HOL: theory Topological_Spaces

23:00:52 FOL-ex: theory Locale_Test1

23:00:53 HOL: theory Rat

23:00:54 HOL-Proofs: theory Lifting_Set

23:00:54 FOL-ex: theory Locale_Test2

23:00:54 FOL-ex: theory Locale_Test3

23:00:54 FOL-ex: theory Locale_Test

23:00:55 HOL: theory Real

23:00:55 HOL-Proofs: theory Option

23:00:57 Timing FOL-ex (2 threads, 5.085s elapsed time, 7.132s cpu time, 0.172s GC time, factor 1.40)

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

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

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

23:00:57 Finished FOL-ex (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.41)

23:00:57 Running CCL ...

23:00:57 CCL: theory IFOL

23:00:58 HOL: theory Real_Vector_Spaces

23:00:58 CCL: theory FOL

23:00:59 HOL-Proofs: theory Quotient

23:00:59 CCL: theory Set

23:00:59 HOL-Proofs: theory Extraction

23:01:00 CCL: theory Lfp

23:01:00 CCL: theory Gfp

23:01:00 CCL: theory CCL

23:01:00 CCL: theory Term

23:01:00 CCL: theory Trancl

23:01:00 CCL: theory Type

23:01:00 CCL: theory Fix

23:01:01 CCL: theory Hered

23:01:01 CCL: theory Wfd

23:01:01 CCL: theory Nat

23:01:01 CCL: theory List

23:01:01 CCL: theory Flag

23:01:01 CCL: theory Stream

23:01:02 HOL-Proofs: theory Lattices_Big

23:01:02 Timing CCL (2 threads, 4.650s elapsed time, 6.620s cpu time, 0.140s GC time, factor 1.42)

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

23:01:02 Finished CCL (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.38)

23:01:02 Running Sequents ...

23:01:02 HOL-Proofs: theory Partial_Function

23:01:03 Sequents: theory Sequents

23:01:03 Sequents: theory ILL

23:01:03 Sequents: theory LK0

23:01:03 Sequents: theory ILL_predlog

23:01:03 Sequents: theory Washing

23:01:03 Sequents: theory LK

23:01:03 Sequents: theory Modal0

23:01:03 Sequents: theory S4

23:01:03 Sequents: theory S43

23:01:03 Sequents: theory Hard_Quantifiers

23:01:03 Sequents: theory Nat

23:01:03 Sequents: theory Propositional

23:01:03 Sequents: theory Quantifiers

23:01:03 Sequents: theory T

23:01:04 HOL-Proofs: theory Fun_Def

23:01:06 HOL-Proofs: theory Int

23:01:06 Timing Sequents (2 threads, 3.443s elapsed time, 6.616s cpu time, 0.124s GC time, factor 1.92)

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

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

23:01:06 Running FOLP-ex ...

23:01:07 FOLP-ex: theory Classical

23:01:07 FOLP-ex: theory If

23:01:07 FOLP-ex: theory Intro

23:01:07 FOLP-ex: theory Nat

23:01:07 FOLP-ex: theory Propositional_Cla

23:01:07 FOLP-ex: theory Quantifiers_Cla

23:01:07 FOLP-ex: theory Foundation

23:01:07 FOLP-ex: theory Intuitionistic

23:01:08 HOL: theory Inequalities

23:01:09 FOLP-ex: theory Propositional_Int

23:01:09 HOL: theory Limits

23:01:09 FOLP-ex: theory Quantifiers_Int

23:01:10 Timing FOLP-ex (2 threads, 3.208s elapsed time, 5.484s cpu time, 0.076s GC time, factor 1.71)

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

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

23:01:10 Running LCF ...

23:01:11 LCF: theory IFOL

23:01:11 HOL-Proofs: theory Nat_Transfer

23:01:11 LCF: theory FOL

23:01:11 HOL: theory Deriv

23:01:12 HOL: theory Series

23:01:12 HOL-Proofs: theory Parity

23:01:13 LCF: theory LCF

23:01:13 HOL: theory NthRoot

23:01:13 LCF: theory Ex1

23:01:13 LCF: theory Ex2

23:01:13 LCF: theory Ex3

23:01:13 LCF: theory Ex4

23:01:13 Timing LCF (2 threads, 2.558s elapsed time, 2.968s cpu time, 0.148s GC time, factor 1.16)

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

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

23:01:13 Running Spec_Check ...

23:01:14 Spec_Check: theory Spec_Check

23:01:14 HOL: theory Transcendental

23:01:14 Spec_Check: theory Examples

23:01:15 HOL-Proofs: theory Divides

23:01:16 Warning: missing document directory

23:01:16 Timing Spec_Check (2 threads, 1.601s elapsed time, 2.964s cpu time, 0.012s GC time, factor 1.85)

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

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

23:01:16 Running ZF-Resid ...

23:01:16 ZF-Resid: theory Redex

23:01:16 ZF-Resid: theory Substitution

23:01:17 ZF-Resid: theory Residuals

23:01:17 ZF-Resid: theory Reduction

23:01:17 ZF-Resid: theory Confluence

23:01:18 HOL: theory Complex

23:01:18 HOL: theory MacLaurin

23:01:18 Timing ZF-Resid (2 threads, 1.466s elapsed time, 2.420s cpu time, 0.000s GC time, factor 1.65)

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

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

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

23:01:18 ZF-IMP: theory Com

23:01:18 ZF-IMP: theory Denotation

23:01:18 ZF-IMP: theory Equiv

23:01:19 HOL: theory Complex_Main

23:01:20 Timing ZF-IMP (2 threads, 0.932s elapsed time, 1.092s cpu time, 0.000s GC time, factor 1.17)

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

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

23:01:20 Running CTT ...

23:01:20 CTT: theory CTT

23:01:20 CTT: theory Bool

23:01:20 CTT: theory Elimination

23:01:20 CTT: theory Arith

23:01:20 CTT: theory Equality

23:01:20 CTT: theory Typechecking

23:01:20 CTT: theory Synthesis

23:01:20 CTT: theory Main

23:01:22 Timing CTT (2 threads, 0.685s elapsed time, 1.052s cpu time, 0.000s GC time, factor 1.54)

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

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

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

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

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

23:01:22 ZF-Coind: theory Language

23:01:22 ZF-Coind: theory Map

23:01:22 ZF-Coind: theory Types

23:01:22 ZF-Coind: theory Values

23:01:22 ZF-Coind: theory Dynamic

23:01:22 ZF-Coind: theory Static

23:01:23 ZF-Coind: theory ECR

23:01:23 Timing ZF-Coind (2 threads, 0.618s elapsed time, 1.200s cpu time, 0.000s GC time, factor 1.94)

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

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

23:01:23 Running Cube ...

23:01:23 Cube: theory Cube

23:01:23 Cube: theory Example

23:01:24 Timing Cube (2 threads, 0.266s elapsed time, 0.272s cpu time, 0.000s GC time, factor 1.02)

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

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

23:01:24 Running Logics_ZF ...

23:01:24 Logics_ZF: theory FOL_examples

23:01:24 Logics_ZF: theory If

23:01:24 Logics_ZF: theory ZF_Isar

23:01:24 Logics_ZF: theory ZF_examples

23:01:24 Logics_ZF: theory IFOL_examples

23:01:27 Timing Logics_ZF (2 threads, 0.282s elapsed time, 0.544s cpu time, 0.000s GC time, factor 1.93)

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

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

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

23:01:27 Running System ...

23:01:27 System: theory Base

23:01:27 System: theory Environment

23:01:27 System: theory Misc

23:01:27 System: theory Presentation

23:01:27 System: theory Scala

23:01:27 System: theory Sessions

23:01:29 Timing System (2 threads, 0.257s elapsed time, 0.344s cpu time, 0.000s GC time, factor 1.34)

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

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

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

23:01:29 Running SML ...

23:01:29 SML: theory Examples

23:01:30 Warning: missing document directory

23:01:30 Timing SML (2 threads, 0.018s elapsed time, 0.020s cpu time, 0.000s GC time, factor 1.12)

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

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

23:01:30 Running Intro ...

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

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

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

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

23:01:32 Running Logics ...

23:01:32 HOL-Proofs: theory Code_Numeral

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

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

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

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

23:01:35 Running Nitpick ...

23:01:36 HOL-Proofs: theory Numeral_Simprocs

23:01:37 HOL-Proofs: theory SMT

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

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

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

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

23:01:37 Running Sledgehammer ...

23:01:39 HOL-Proofs: theory Semiring_Normalization

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

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

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

23:01:39 Finished Sledgehammer (0:00:01 elapsed time)

23:01:41 HOL-Proofs: theory Groebner_Basis

23:01:42 HOL-Proofs: theory Set_Interval

23:01:52 HOL-Proofs: theory Conditionally_Complete_Lattices

23:01:52 HOL-Proofs: theory Filter

23:01:56 HOL-Proofs: theory Presburger

23:02:07 HOL-Proofs: theory Sledgehammer

23:02:09 HOL-Proofs: theory List

23:02:43 HOL-Proofs: theory Groups_List

23:02:45 HOL-Proofs: theory Map

23:02:47 HOL-Proofs: theory Enum

23:03:00 HOL-Proofs: theory Random

23:03:45 HOL-Proofs: theory String

23:03:47 HOL-Proofs: theory BNF_Greatest_Fixpoint

23:03:51 HOL-Proofs: theory Predicate

23:03:53 HOL-Proofs: theory Lazy_Sequence

23:03:54 HOL-Proofs: theory Limited_Sequence

23:03:54 HOL-Proofs: theory Typerep

23:03:55 HOL-Proofs: theory Code_Evaluation

23:03:57 HOL-Proofs: theory Quickcheck_Random

23:03:59 HOL-Proofs: theory Quickcheck_Exhaustive

23:04:03 HOL-Proofs: theory Record

23:04:05 HOL-Proofs: theory Nitpick

23:04:10 HOL-Proofs: theory Quickcheck_Narrowing

23:04:14 HOL-Proofs: theory Random_Pred

23:04:15 HOL-Proofs: theory Random_Sequence

23:04:16 HOL-Proofs: theory Predicate_Compile

23:04:17 HOL-Proofs: theory Main

23:04:19 HOL-Proofs: theory Old_Datatype

23:04:21 Timing HOL (2 threads, 228.530s elapsed time, 428.052s cpu time, 42.188s GC time, factor 1.87)

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

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

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

23:04:21 Finished HOL (0:05:16 elapsed time, 0:09:31 cpu time, factor 1.80)

23:04:23 Building HOLCF ...

23:04:23 Building HOL-Word ...

23:04:25 HOLCF: theory Nat_Bijection

23:04:25 HOLCF: theory Old_Datatype

23:04:25 HOL-Word: theory Bit

23:04:25 HOL-Word: theory Bits

23:04:25 HOL-Word: theory Boolean_Algebra

23:04:26 HOL-Word: theory Bits_Bit

23:04:26 HOL-Word: theory Misc_Numeric

23:04:26 HOL-Word: theory Bit_Representation

23:04:26 HOL-Word: theory Misc_Typedef

23:04:26 HOL-Word: theory Phantom_Type

23:04:26 HOLCF: theory Countable

23:04:27 HOL-Word: theory Bits_Int

23:04:27 HOL-Word: theory Cardinality

23:04:28 HOLCF: theory Porder

23:04:28 HOL-Word: theory Bool_List_Representation

23:04:28 HOL-Word: theory Numeral_Type

23:04:28 HOLCF: theory Pcpo

23:04:29 HOL-Word: theory Word_Miscellaneous

23:04:29 HOL-Word: theory Type_Length

23:04:29 HOL-Word: theory Word

23:04:30 HOLCF: theory Cont

23:04:30 HOLCF: theory Adm

23:04:30 HOLCF: theory Discrete

23:04:30 HOLCF: theory Cpodef

23:04:30 HOLCF: theory Fun_Cpo

23:04:30 HOLCF: theory Product_Cpo

23:04:31 HOLCF: theory Cfun

23:04:31 HOLCF: theory Cprod

23:04:31 HOLCF: theory Fix

23:04:32 HOLCF: theory Sfun

23:04:32 HOLCF: theory Sprod

23:04:32 HOLCF: theory Up

23:04:32 HOLCF: theory Lift

23:04:33 HOLCF: theory One

23:04:33 HOLCF: theory Tr

23:04:33 HOLCF: theory Ssum

23:04:33 HOLCF: theory Plain_HOLCF

23:04:34 HOLCF: theory Completion

23:04:34 HOLCF: theory Deflation

23:04:34 HOLCF: theory Fixrec

23:04:34 HOLCF: theory Map_Functions

23:04:35 HOLCF: theory Bifinite

23:04:35 HOLCF: theory Domain_Aux

23:04:36 HOLCF: theory Universal

23:04:37 HOLCF: theory Algebraic

23:04:37 HOLCF: theory Compact_Basis

23:04:37 HOLCF: theory LowerPD

23:04:37 HOLCF: theory UpperPD

23:04:37 HOLCF: theory Representable

23:04:37 HOLCF: theory ConvexPD

23:04:40 HOLCF: theory Domain

23:04:41 HOLCF: theory Powerdomains

23:04:42 HOLCF: theory HOLCF

23:05:02 Timing HOL-Word (2 threads, 18.637s elapsed time, 35.828s cpu time, 1.452s GC time, factor 1.92)

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

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

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

23:05:02 Finished HOL-Word (0:00:38 elapsed time, 0:01:05 cpu time, factor 1.70)

23:05:02 Building HOL-TLA ...

23:05:03 Timing HOLCF (2 threads, 17.230s elapsed time, 31.268s cpu time, 1.692s GC time, factor 1.81)

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

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

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

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

23:05:03 Building IOA ...

23:05:04 HOL-TLA: theory Intensional

23:05:04 HOL-TLA: theory Stfun

23:05:04 HOL-TLA: theory Action

23:05:04 HOL-TLA: theory Init

23:05:05 HOL-TLA: theory TLA

23:05:05 IOA: theory Asig

23:05:05 IOA: theory Seq

23:05:05 IOA: theory Automata

23:05:06 IOA: theory Sequence

23:05:07 IOA: theory Pred

23:05:07 IOA: theory Traces

23:05:08 IOA: theory TL

23:05:08 IOA: theory CompoExecs

23:05:08 IOA: theory RefMappings

23:05:08 IOA: theory RefCorrectness

23:05:09 IOA: theory CompoScheds

23:05:09 IOA: theory Simulations

23:05:09 IOA: theory SimCorrectness

23:05:10 IOA: theory Deadlock

23:05:10 IOA: theory ShortExecutions

23:05:10 IOA: theory CompoTraces

23:05:11 IOA: theory Compositionality

23:05:11 IOA: theory IOA

23:05:11 IOA: theory TLS

23:05:12 IOA: theory LiveIOA

23:05:12 IOA: theory Abstraction

23:05:17 Timing HOL-TLA (2 threads, 1.697s elapsed time, 2.716s cpu time, 0.000s GC time, factor 1.60)

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

23:05:17 Finished HOL-TLA (0:00:14 elapsed time, 0:00:20 cpu time, factor 1.43)

23:05:17 Building HOL-Analysis ...

23:05:20 HOL-Analysis: theory FuncSet

23:05:20 HOL-Analysis: theory Disjoint_Sets

23:05:20 HOL-Analysis: theory Infinite_Set

23:05:21 HOL-Analysis: theory Multiset

23:05:21 HOL-Analysis: theory Nat_Bijection

23:05:21 HOL-Analysis: theory Old_Datatype

23:05:22 HOL-Analysis: theory Countable

23:05:24 HOL-Analysis: theory Countable_Set

23:05:25 HOL-Analysis: theory Countable_Complete_Lattices

23:05:25 HOL-Analysis: theory Permutations

23:05:27 HOL-Analysis: theory Phantom_Type

23:05:27 HOL-Analysis: theory Cardinality

23:05:27 HOL-Analysis: theory Product_Plus

23:05:28 HOL-Analysis: theory Product_Order

23:05:28 HOL-Analysis: theory Set_Algebras

23:05:28 HOL-Analysis: theory L2_Norm

23:05:28 HOL-Analysis: theory Numeral_Type

23:05:28 HOL-Analysis: theory Continuum_Not_Denumerable

23:05:29 HOL-Analysis: theory Discrete

23:05:29 HOL-Analysis: theory Indicator_Function

23:05:29 HOL-Analysis: theory Inner_Product

23:05:30 HOL-Analysis: theory Liminf_Limsup

23:05:30 HOL-Analysis: theory Product_Vector

23:05:30 HOL-Analysis: theory Nonpos_Ints

23:05:31 HOL-Analysis: theory Operator_Norm

23:05:31 HOL-Analysis: theory Euclidean_Space

23:05:31 HOL-Analysis: theory Order_Continuity

23:05:31 HOL-Analysis: theory Extended_Nat

23:05:33 HOL-Analysis: theory Finite_Cartesian_Product

23:05:33 HOL-Analysis: theory Linear_Algebra

23:05:33 HOL-Analysis: theory Extended_Real

23:05:35 HOL-Analysis: theory Periodic_Fun

23:05:36 HOL-Analysis: theory Poly_Roots

23:05:36 HOL-Analysis: theory Sum_of_Squares

23:05:36 Timing IOA (2 threads, 15.157s elapsed time, 28.464s cpu time, 0.952s GC time, factor 1.88)

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

23:05:36 Finished IOA (0:00:32 elapsed time, 0:00:53 cpu time, factor 1.64)

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

23:05:37 HOL-Analysis: theory Extended_Nonnegative_Real

23:05:38 HOL-Analysis: theory Norm_Arith

23:05:38 HOL-Analysis: theory Topology_Euclidean_Space

23:05:38 HOL-SPARK: theory Bit_Comparison

23:05:39 HOL-SPARK: theory SPARK_Setup

23:05:39 HOL-Analysis: theory Sigma_Algebra

23:05:40 HOL-SPARK: theory SPARK

23:05:42 HOL-Analysis: theory Measurable

23:05:42 HOL-Analysis: theory Measure_Space

23:05:45 HOL-Analysis: theory Caratheodory

23:05:45 HOL-Analysis: theory Summation_Tests

23:05:47 HOL-Analysis: theory Bounded_Linear_Function

23:05:47 HOL-Analysis: theory Convex_Euclidean_Space

23:05:48 HOL-Analysis: theory Extended_Real_Limits

23:05:49 HOL-Analysis: theory Tagged_Division

23:05:50 HOL-Analysis: theory Uniform_Limit

23:05:52 HOL-Analysis: theory Continuous_Extension

23:05:52 HOL-Analysis: theory Path_Connected

23:05:54 Timing HOL-SPARK (2 threads, 2.104s elapsed time, 3.624s cpu time, 0.112s GC time, factor 1.72)

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

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

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

23:05:56 HOL-Analysis: theory Homeomorphism

23:05:56 HOL-Analysis: theory Brouwer_Fixpoint

23:05:56 HOL-Library: theory Adhoc_Overloading

23:05:56 HOL-Library: theory Lattice_Syntax

23:05:56 HOL-Library: theory AList

23:05:57 HOL-Library: theory BNF_Axiomatization

23:05:57 HOL-Library: theory BNF_Corec

23:05:58 HOL-Analysis: theory Derivative

23:05:58 HOL-Library: theory DAList

23:05:59 HOL-Library: theory Stirling

23:05:59 HOL-Library: theory Bit

23:06:00 HOL-Analysis: theory Cartesian_Euclidean_Space

23:06:00 HOL-Analysis: theory Weierstrass_Theorems

23:06:00 HOL-Library: theory Bits

23:06:00 HOL-Library: theory Bits_Bit

23:06:01 HOL-Library: theory Boolean_Algebra

23:06:01 HOL-Library: theory Cardinal_Notations

23:06:01 HOL-Library: theory Char_ord

23:06:01 HOL-Library: theory Code_Abstract_Nat

23:06:01 HOL-Library: theory Code_Binary_Nat

23:06:02 HOL-Library: theory Code_Target_Nat

23:06:02 HOL-Library: theory Code_Char

23:06:02 HOL-Library: theory Code_Prolog

23:06:02 HOL-Library: theory Code_Test

23:06:02 HOL-Library: theory Combine_PER

23:06:02 HOL-Analysis: theory Determinants

23:06:02 HOL-Analysis: theory Fashoda_Theorem

23:06:03 HOL-Library: theory Complete_Partial_Order2

23:06:03 HOL-Analysis: theory Ordered_Euclidean_Space

23:06:03 HOL-Library: theory Debug

23:06:03 HOL-Library: theory Disjoint_Sets

23:06:03 HOL-Analysis: theory Polytope

23:06:03 HOL-Library: theory Dlist

23:06:04 HOL-Library: theory FSet

23:06:06 HOL-Library: theory Fraction_Field

23:06:07 HOL-Library: theory Fun_Lexorder

23:06:07 HOL-Library: theory FuncSet

23:06:07 HOL-Library: theory Function_Algebras

23:06:07 HOL-Library: theory Finite_Map

23:06:07 HOL-Library: theory Function_Division

23:06:08 HOL-Library: theory Code_Target_Int

23:06:08 HOL-Analysis: theory Borel_Space

23:06:08 HOL-Library: theory Code_Target_Numeral

23:06:08 HOL-Library: theory Groups_Big_Fun

23:06:09 HOL-Library: theory IArray

23:06:09 HOL-Library: theory Infinite_Set

23:06:09 HOL-Library: theory Omega_Words_Fun

23:06:09 HOL-Library: theory LaTeXsugar

23:06:09 HOL-Library: theory Lattice_Constructions

23:06:10 HOL-Library: theory ListVector

23:06:10 HOL-Library: theory List_lexord

23:06:10 HOL-Library: theory Mapping

23:06:10 HOL-Analysis: theory Nonnegative_Lebesgue_Integration

23:06:11 HOL-Library: theory AList_Mapping

23:06:11 HOL-Library: theory Misc_Numeric

23:06:11 HOL-Library: theory Bit_Representation

23:06:12 HOL-Analysis: theory Regularity

23:06:12 HOL-Library: theory Misc_Typedef

23:06:12 HOL-Library: theory Monad_Syntax

23:06:12 HOL-Library: theory Bits_Int

23:06:12 HOL-Library: theory More_List

23:06:12 HOL-Library: theory Multiset

23:06:12 HOL-Analysis: theory Binary_Product_Measure

23:06:13 HOL-Analysis: theory Embed_Measure

23:06:14 HOL-Library: theory Bool_List_Representation

23:06:14 HOL-Analysis: theory Finite_Product_Measure

23:06:14 HOL-Library: theory Nat_Bijection

23:06:15 HOL-Library: theory Stream

23:06:15 HOL-Analysis: theory Bochner_Integration

23:06:15 HOL-Analysis: theory Function_Topology

23:06:16 HOL-Library: theory Old_Datatype

23:06:17 HOL-Analysis: theory Complete_Measure

23:06:17 HOL-Analysis: theory Radon_Nikodym

23:06:17 HOL-Library: theory DAList_Multiset

23:06:17 HOL-Library: theory Factorial_Ring

23:06:17 HOL-Analysis: theory Set_Integral

23:06:17 HOL-Library: theory Multiset_Order

23:06:18 HOL-Analysis: theory Lebesgue_Measure

23:06:18 HOL-Library: theory Permutation

23:06:18 HOL-Library: theory Permutations

23:06:19 HOL-Analysis: theory Henstock_Kurzweil_Integration

23:06:21 HOL-Library: theory Countable

23:06:22 HOL-Library: theory Countable_Set

23:06:22 HOL-Analysis: theory Bounded_Continuous_Function

23:06:22 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration

23:06:23 HOL-Library: theory Countable_Complete_Lattices

23:06:23 HOL-Analysis: theory Integral_Test

23:06:23 HOL-Analysis: theory Complex_Analysis_Basics

23:06:23 HOL-Analysis: theory Interval_Integral

23:06:24 HOL-Analysis: theory Lebesgue_Integral_Substitution

23:06:25 HOL-Analysis: theory Complex_Transcendental

23:06:26 HOL-Library: theory Countable_Set_Type

23:06:26 HOL-Library: theory Euclidean_Algorithm

23:06:27 HOL-Analysis: theory Generalised_Binomial_Theorem

23:06:27 HOL-Analysis: theory Harmonic_Numbers

23:06:27 HOL-Analysis: theory Cauchy_Integral_Theorem

23:06:27 HOL-Library: theory Old_Recdef

23:06:28 HOL-Analysis: theory Gamma_Function

23:06:28 HOL-Library: theory Option_ord

23:06:29 HOL-Library: theory Parallel

23:06:29 HOL-Library: theory Perm

23:06:30 HOL-Library: theory Phantom_Type

23:06:31 HOL-Library: theory Cardinality

23:06:31 HOL-Analysis: theory Conformal_Mappings

23:06:31 HOL-Analysis: theory Further_Topology

23:06:32 HOL-Library: theory FinFun

23:06:33 HOL-Analysis: theory Analysis

23:06:34 HOL-Library: theory Numeral_Type

23:06:35 HOL-Library: theory Type_Length

23:06:35 HOL-Library: theory Saturated

23:06:35 HOL-Library: theory Normalized_Fraction

23:06:35 HOL-Library: theory Predicate_Compile_Alternative_Defs

23:06:36 HOL-Library: theory Predicate_Compile_Quickcheck

23:06:36 HOL-Library: theory Product_Lexorder

23:06:36 HOL-Library: theory Product_Plus

23:06:36 HOL-Library: theory Quotient_Syntax

23:06:36 HOL-Library: theory Quotient_Option

23:06:36 HOL-Library: theory Product_Order

23:06:36 HOL-Library: theory Quotient_Product

23:06:36 HOL-Library: theory Quotient_Set

23:06:36 HOL-Library: theory Finite_Lattice

23:06:36 HOL-Library: theory Quotient_List

23:06:37 HOL-Library: theory Quotient_Sum

23:06:37 HOL-Library: theory Quotient_Type

23:06:37 HOL-Library: theory RBT_Impl

23:06:39 HOL-Library: theory Ramsey

23:06:39 HOL-Library: theory Reflection

23:06:40 HOL-Library: theory Refute

23:06:40 HOL-Library: theory Rewrite

23:06:41 HOL-Library: theory Set_Algebras

23:06:41 HOL-Library: theory Simps_Case_Conv

23:06:41 HOL-Library: theory Extended

23:06:42 HOL-Library: theory State_Monad

23:06:42 HOL-Library: theory Sublist

23:06:43 HOL-Library: theory Prefix_Order

23:06:43 HOL-Library: theory Sublist_Order

23:06:44 HOL-Library: theory Polynomial

23:06:48 HOL-Library: theory BigO

23:06:49 HOL-Library: theory Code_Real_Approx_By_Float

23:06:50 HOL-Library: theory Diagonal_Subsequence

23:06:50 HOL-Library: theory Discrete

23:06:50 HOL-Library: theory Field_as_Ring

23:06:52 HOL-Library: theory Formal_Power_Series

23:06:55 HOL-Library: theory Polynomial_FPS

23:06:56 HOL-Library: theory Fundamental_Theorem_Algebra

23:06:57 HOL-Library: theory Indicator_Function

23:06:57 HOL-Library: theory Lattice_Algebras

23:07:02 HOL-Library: theory Liminf_Limsup

23:07:03 HOL-Library: theory Log_Nat

23:07:03 HOL-Library: theory Float

23:07:05 HOL-Library: theory Lub_Glb

23:07:06 HOL-Library: theory Multiset_Permutations

23:07:07 HOL-Library: theory RBT

23:07:07 HOL-Library: theory Nonpos_Ints

23:07:07 HOL-Library: theory OptionalSugar

23:07:07 HOL-Library: theory RBT_Mapping

23:07:07 HOL-Library: theory RBT_Set

23:07:07 HOL-Library: theory Order_Continuity

23:07:08 HOL-Library: theory Extended_Nat

23:07:08 HOL-Library: theory Periodic_Fun

23:07:09 HOL-Library: theory Polynomial_Factorial

23:07:09 HOL-Library: theory Extended_Real

23:07:13 HOL-Library: theory Extended_Nonnegative_Real

23:07:15 HOL-Library: theory Linear_Temporal_Logic_on_Streams

23:07:16 HOL-Library: theory Quadratic_Discriminant

23:07:17 HOL-Library: theory Sum_of_Squares

23:07:18 HOL-Library: theory Transitive_Closure_Table

23:07:19 HOL-Library: theory Tree

23:07:19 HOL-Library: theory While_Combinator

23:07:19 HOL-Library: theory Bourbaki_Witt_Fixpoint

23:07:20 HOL-Library: theory Word_Miscellaneous

23:07:20 HOL-Library: theory Word

23:07:21 HOL-Library: theory Tree_Multiset

23:07:22 HOL-Library: theory Preorder

23:07:22 HOL-Library: theory Function_Growth

23:07:23 HOL-Library: theory Library

23:07:25 HOL-Library: theory Old_SMT

23:08:12 Timing HOL-Proofs (2 threads, 437.403s elapsed time, 789.608s cpu time, 85.048s GC time, factor 1.81)

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

23:08:12 Finished HOL-Proofs (0:09:07 elapsed time, 0:16:07 cpu time, factor 1.77)

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

23:08:16 HOL-Auth: theory Message

23:08:16 HOL-Auth: theory Nat_Bijection

23:08:17 HOL-Auth: theory Simps_Case_Conv

23:08:19 HOL-Auth: theory All_Symmetric

23:08:19 HOL-Auth: theory Event

23:08:19 HOL-Auth: theory EventSC

23:08:20 HOL-Auth: theory Extensions

23:08:21 HOL-Auth: theory Analz

23:08:21 HOL-Auth: theory List_Msg

23:08:21 HOL-Auth: theory Guard

23:08:22 HOL-Auth: theory GuardK

23:08:22 HOL-Auth: theory Public

23:08:23 HOL-Auth: theory CertifiedEmail

23:08:23 HOL-Auth: theory Guard_Public

23:08:23 HOL-Auth: theory Guard_NS_Public

23:08:23 HOL-Auth: theory P2

23:08:24 HOL-Auth: theory Proto

23:08:25 HOL-Auth: theory KerberosIV

23:08:26 HOL-Auth: theory KerberosIV_Gets

23:08:27 HOL-Auth: theory KerberosV

23:08:28 HOL-Auth: theory Kerberos_BAN

23:08:28 HOL-Auth: theory Kerberos_BAN_Gets

23:08:29 HOL-Auth: theory NS_Public

23:08:29 HOL-Auth: theory NS_Public_Bad

23:08:29 HOL-Auth: theory NS_Shared

23:08:29 HOL-Auth: theory OtwayRees

23:08:30 HOL-Auth: theory OtwayReesBella

23:08:30 HOL-Auth: theory OtwayRees_AN

23:08:30 HOL-Auth: theory OtwayRees_Bad

23:08:31 HOL-Auth: theory P1

23:08:31 HOL-Auth: theory Recur

23:08:32 HOL-Auth: theory WooLam

23:08:32 HOL-Auth: theory Yahalom

23:08:33 HOL-Auth: theory Yahalom2

23:08:34 HOL-Auth: theory Yahalom_Bad

23:08:34 HOL-Auth: theory ZhouGollmann

23:08:35 HOL-Auth: theory Auth_Shared

23:08:35 HOL-Auth: theory Auth_Guard_Public

23:08:36 HOL-Auth: theory Shared

23:08:36 HOL-Auth: theory Guard_Shared

23:08:36 HOL-Auth: theory Guard_OtwayRees

23:08:36 HOL-Auth: theory Guard_Yahalom

23:08:37 HOL-Auth: theory TLS

23:08:37 HOL-Auth: theory Auth_Guard_Shared

23:08:37 HOL-Auth: theory Smartcard

23:08:37 HOL-Auth: theory ShoupRubin

23:08:38 HOL-Auth: theory Auth_Public

23:08:39 HOL-Auth: theory ShoupRubinBella

23:08:40 HOL-Auth: theory Auth_Smartcard

23:11:33 Timing HOL-Auth (2 threads, 168.589s elapsed time, 265.340s cpu time, 8.208s GC time, factor 1.57)

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

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

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

23:11:33 Finished HOL-Auth (0:03:18 elapsed time, 0:05:12 cpu time, factor 1.57)

23:11:34 Building Codegen_Basics ...

23:11:36 Codegen_Basics: theory IArray

23:11:36 Codegen_Basics: theory Dlist

23:11:36 Timing HOL-Library (2 threads, 241.777s elapsed time, 447.688s cpu time, 23.096s GC time, factor 1.85)

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

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

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

23:11:36 Finished HOL-Library (0:05:41 elapsed time, 0:10:08 cpu time, factor 1.78)

23:11:37 Codegen_Basics: theory Mapping

23:11:37 Codegen_Basics: theory RBT_Impl

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

23:11:40 HOL-Nonstandard_Analysis: theory Infinite_Set

23:11:40 HOL-Nonstandard_Analysis: theory Lub_Glb

23:11:40 HOL-Nonstandard_Analysis: theory Free_Ultrafilter

23:11:40 HOL-Nonstandard_Analysis: theory StarDef

23:11:41 HOL-Nonstandard_Analysis: theory HyperNat

23:11:42 HOL-Nonstandard_Analysis: theory HyperDef

23:11:43 HOL-Nonstandard_Analysis: theory NSA

23:11:45 HOL-Nonstandard_Analysis: theory NSComplex

23:11:45 HOL-Nonstandard_Analysis: theory Star

23:11:45 HOL-Nonstandard_Analysis: theory HLim

23:11:46 HOL-Nonstandard_Analysis: theory NatStar

23:11:46 HOL-Nonstandard_Analysis: theory HDeriv

23:11:46 HOL-Nonstandard_Analysis: theory HSEQ

23:11:47 HOL-Nonstandard_Analysis: theory HSeries

23:11:47 HOL-Nonstandard_Analysis: theory HTranscendental

23:11:48 HOL-Nonstandard_Analysis: theory HLog

23:11:48 HOL-Nonstandard_Analysis: theory NSCA

23:11:49 HOL-Nonstandard_Analysis: theory Hyperreal

23:11:49 HOL-Nonstandard_Analysis: theory CStar

23:11:49 HOL-Nonstandard_Analysis: theory CLim

23:11:50 HOL-Nonstandard_Analysis: theory Hypercomplex

23:11:50 HOL-Nonstandard_Analysis: theory Nonstandard_Analysis

23:12:05 Codegen_Basics: theory RBT

23:12:05 Codegen_Basics: theory Setup

23:12:09 Timing HOL-Nonstandard_Analysis (2 threads, 13.567s elapsed time, 26.660s cpu time, 0.916s GC time, factor 1.97)

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

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

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

23:12:09 Finished HOL-Nonstandard_Analysis (0:00:31 elapsed time, 0:00:53 cpu time, factor 1.70)

23:12:09 Building Typeclass_Hierarchy_Basics ...

23:12:11 Typeclass_Hierarchy_Basics: theory Lattice_Syntax

23:12:11 Typeclass_Hierarchy_Basics: theory Multiset

23:12:16 Typeclass_Hierarchy_Basics: theory Setup

23:12:33 Timing Typeclass_Hierarchy_Basics (2 threads, 8.215s elapsed time, 14.764s cpu time, 0.668s GC time, factor 1.80)

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

23:12:33 Finished Typeclass_Hierarchy_Basics (0:00:23 elapsed time, 0:00:36 cpu time, factor 1.56)

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

23:12:35 HOL-Nominal: theory Infinite_Set

23:12:35 HOL-Nominal: theory Old_Datatype

23:12:37 HOL-Nominal: theory Nominal

23:12:52 Timing Codegen_Basics (2 threads, 49.534s elapsed time, 87.928s cpu time, 3.228s GC time, factor 1.78)

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

23:12:52 Finished Codegen_Basics (0:01:18 elapsed time, 0:02:12 cpu time, factor 1.69)

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

23:12:54 HOL-Eisbach: theory Eisbach

23:12:54 HOL-Eisbach: theory IFOL

23:12:55 HOL-Eisbach: theory Eisbach_Old_Appl_Syntax

23:12:55 HOL-Eisbach: theory Eisbach_Tools

23:12:55 HOL-Eisbach: theory Examples

23:12:55 HOL-Eisbach: theory Tests

23:12:55 HOL-Eisbach: theory FOL

23:12:56 Timing HOL-Nominal (2 threads, 7.291s elapsed time, 14.048s cpu time, 0.644s GC time, factor 1.93)

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

23:12:56 Finished HOL-Nominal (0:00:22 elapsed time, 0:00:35 cpu time, factor 1.61)

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

23:12:57 HOL-Eisbach: theory Examples_FOL

23:12:58 HOL-Mirabelle: theory Mirabelle

23:12:58 HOL-Mirabelle: theory Mirabelle_Test

23:13:08 Warning: missing document directory

23:13:08 Timing HOL-Eisbach (2 threads, 2.790s elapsed time, 5.224s cpu time, 0.156s GC time, factor 1.87)

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

23:13:08 Finished HOL-Eisbach (0:00:15 elapsed time, 0:00:22 cpu time, factor 1.49)

23:13:08 Timing HOL-Mirabelle (2 threads, 0.448s elapsed time, 0.520s cpu time, 0.000s GC time, factor 1.16)

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

23:13:08 Finished HOL-Mirabelle (0:00:11 elapsed time, 0:00:16 cpu time, factor 1.39)

23:13:08 Running HOL-Nominal-Examples ...

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

23:13:10 HOL-Data_Structures: theory Multiset

23:13:10 HOL-Data_Structures: theory Less_False

23:13:10 HOL-Data_Structures: theory Fib

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

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

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

23:13:19 HOL-Data_Structures: theory Sorted_Less

23:13:19 HOL-Data_Structures: theory Cmp

23:13:19 HOL-Data_Structures: theory AList_Upd_Del

23:13:19 HOL-Data_Structures: theory List_Ins_Del

23:13:19 HOL-Data_Structures: theory Map_by_Ordered

23:13:20 HOL-Data_Structures: theory Set_by_Ordered

23:13:20 HOL-Data_Structures: theory Tree

23:13:20 HOL-Data_Structures: theory Brother12_Set

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

23:13:23 HOL-Data_Structures: theory Balance

23:13:24 HOL-Data_Structures: theory Splay_Set

23:13:25 HOL-Data_Structures: theory Splay_Map

23:13:27 HOL-Data_Structures: theory Tree_Set

23:13:28 HOL-Data_Structures: theory Tree_Map

23:13:28 HOL-Data_Structures: theory Tree2

23:13:29 HOL-Data_Structures: theory Isin2

23:13:30 HOL-Data_Structures: theory AA_Set

23:13:31 HOL-Data_Structures: theory AVL_Set

23:13:32 HOL-Data_Structures: theory Leftist_Heap

23:13:34 HOL-Data_Structures: theory Lookup2

23:13:35 HOL-Data_Structures: theory AA_Map

23:13:35 HOL-Data_Structures: theory AVL_Map

23:13:36 HOL-Data_Structures: theory RBT

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

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

23:13:45 HOL-Data_Structures: theory RBT_Set

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

23:13:48 HOL-Data_Structures: theory RBT_Map

23:13:51 HOL-Data_Structures: theory Tree23

23:13:52 HOL-Data_Structures: theory Tree23_Set

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

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

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

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

23:13:59 HOL-Data_Structures: theory Tree23_Map

23:14:00 HOL-Nominal-Examples: theory Lambda_mu

23:14:02 HOL-Data_Structures: theory Tree234

23:14:03 HOL-Nominal-Examples: theory LocalWeakening

23:14:05 HOL-Data_Structures: theory Tree234_Set

23:14:06 HOL-Nominal-Examples: theory Pattern

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

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

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

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

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

23:14:28 HOL-Data_Structures: theory Brother12_Map

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

23:14:31 HOL-Data_Structures: theory Tree234_Map

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

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

23:16:51 Timing HOL-Analysis (2 threads, 582.834s elapsed time, 1014.848s cpu time, 69.752s GC time, factor 1.74)

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

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

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

23:16:51 Finished HOL-Analysis (0:11:34 elapsed time, 0:19:46 cpu time, factor 1.71)

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

23:16:58 HOL-Probability: theory AList

23:16:58 HOL-Probability: theory FSet

23:17:00 HOL-Probability: theory Permutation

23:17:00 HOL-Probability: theory Diagonal_Subsequence

23:17:01 HOL-Probability: theory Finite_Map

23:17:09 HOL-Probability: theory Lattice_Syntax

23:17:09 HOL-Probability: theory Adhoc_Overloading

23:17:09 HOL-Probability: theory Complete_Partial_Order2

23:17:09 HOL-Probability: theory Mapping

23:17:10 HOL-Probability: theory AList_Mapping

23:17:10 HOL-Probability: theory Monad_Syntax

23:17:11 HOL-Probability: theory Stream

23:17:12 HOL-Probability: theory Rewrite

23:17:12 HOL-Probability: theory Sublist

23:17:12 HOL-Probability: theory Multiset_Permutations

23:17:13 HOL-Probability: theory Linear_Temporal_Logic_on_Streams

23:17:13 HOL-Probability: theory Fin_Map

23:17:14 HOL-Probability: theory Discrete_Topology

23:17:14 HOL-Probability: theory Essential_Supremum

23:17:15 HOL-Probability: theory Probability_Measure

23:17:15 HOL-Probability: theory Stopping_Time

23:17:16 HOL-Probability: theory Conditional_Expectation

23:17:16 HOL-Probability: theory Distribution_Functions

23:17:17 HOL-Probability: theory Weak_Convergence

23:17:17 HOL-Probability: theory Giry_Monad

23:17:17 HOL-Probability: theory Helly_Selection

23:17:19 HOL-Probability: theory Probability_Mass_Function

23:17:19 HOL-Probability: theory Projective_Family

23:17:20 HOL-Probability: theory Infinite_Product_Measure

23:17:21 HOL-Probability: theory PMF_Impl

23:17:21 HOL-Probability: theory Random_Permutations

23:17:22 HOL-Probability: theory SPMF

23:17:23 HOL-Probability: theory Independent_Family

23:17:24 HOL-Probability: theory Convolution

23:17:25 HOL-Probability: theory Information

23:17:26 HOL-Probability: theory Projective_Limit

23:17:27 HOL-Probability: theory Distributions

23:17:28 HOL-Probability: theory Stream_Space

23:17:29 HOL-Probability: theory Characteristic_Functions

23:17:29 HOL-Probability: theory Sinc_Integral

23:17:29 HOL-Probability: theory Levy

23:17:30 HOL-Probability: theory Central_Limit_Theorem

23:17:31 HOL-Probability: theory Probability

23:20:10 Timing HOL-Probability (2 threads, 144.342s elapsed time, 258.572s cpu time, 10.780s GC time, factor 1.79)

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

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

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

23:20:10 Finished HOL-Probability (0:03:16 elapsed time, 0:05:36 cpu time, factor 1.71)

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

23:20:17 HOL-Codegenerator_Test: theory Code_Test_PolyML

23:20:17 HOL-Codegenerator_Test: theory Cmp

23:20:17 HOL-Codegenerator_Test: theory Code_Test_Scala

23:20:17 HOL-Codegenerator_Test: theory Less_False

23:20:17 HOL-Codegenerator_Test: theory Sorted_Less

23:20:17 HOL-Codegenerator_Test: theory Primes

23:20:17 HOL-Codegenerator_Test: theory AList_Upd_Del

23:20:18 HOL-Codegenerator_Test: theory List_Ins_Del

23:20:18 HOL-Codegenerator_Test: theory Map_by_Ordered

23:20:18 HOL-Codegenerator_Test: theory Eratosthenes

23:20:19 HOL-Codegenerator_Test: theory Set_by_Ordered

23:20:19 HOL-Codegenerator_Test: theory Records

23:20:19 HOL-Codegenerator_Test: theory Tree_Set

23:20:19 HOL-Codegenerator_Test: theory Tree_Map

23:20:22 HOL-Codegenerator_Test: theory Candidates

23:20:25 HOL-Codegenerator_Test: theory Generate

23:20:26 HOL-Codegenerator_Test: theory Generate_Binary_Nat

23:24:14 HOL-Codegenerator_Test: theory Generate_Efficient_Datastructures

23:24:22 HOL-Codegenerator_Test: theory Generate_Pretty_Char

23:24:32 Timing HOL-Data_Structures (2 threads, 678.321s elapsed time, 915.536s cpu time, 51.928s GC time, factor 1.35)

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

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

23:24:32 Finished HOL-Data_Structures (0:11:23 elapsed time, 0:15:20 cpu time, factor 1.35)

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

23:24:34 HOL-ex: theory Cartouche_Examples

23:24:34 HOL-ex: theory Adhoc_Overloading

23:24:34 HOL-ex: theory Chinese

23:24:34 HOL-ex: theory Code_Abstract_Nat

23:24:34 HOL-ex: theory Code_Binary_Nat

23:24:35 HOL-ex: theory FuncSet

23:24:35 HOL-ex: theory Hebrew

23:24:35 HOL-ex: theory Monad_Syntax

23:24:35 HOL-ex: theory Refute

23:24:36 HOL-ex: theory Serbian

23:24:37 HOL-ex: theory State_Monad

23:24:37 HOL-ex: theory Code_Binary_Nat_examples

23:24:38 HOL-ex: theory Eval_Examples

23:24:40 HOL-ex: theory Normalization_by_Evaluation

23:24:41 HOL-ex: theory Transitive_Closure_Table

23:25:00 HOL-ex: theory Groebner_Examples

23:25:00 HOL-ex: theory PresburgerEx

23:25:01 HOL-ex: theory AList

23:25:01 HOL-ex: theory Abstract_NAT

23:25:01 HOL-ex: theory Antiquote

23:25:01 HOL-ex: theory Arith_Examples

23:25:01 HOL-ex: theory CTL

23:25:01 HOL-ex: theory Classical

23:25:02 HOL-ex: theory Code_Target_Nat

23:25:02 HOL-ex: theory Coercion_Examples

23:25:02 HOL-ex: theory Coherent

23:25:03 HOL-ex: theory Commands

23:25:03 HOL-ex: theory Debug

23:25:03 HOL-ex: theory Dlist

23:25:04 HOL-ex: theory Erdoes_Szekeres

23:25:04 HOL-ex: theory Executable_Relation

23:25:04 HOL-ex: theory FSet

23:25:04 HOL-ex: theory Birthday_Paradox

23:25:05 HOL-ex: theory Code_Target_Int

23:25:05 HOL-ex: theory Code_Target_Numeral

23:25:05 HOL-ex: theory Transfer_Int_Nat

23:25:05 HOL-ex: theory Guess

23:25:05 HOL-ex: theory Hex_Bin_Examples

23:25:05 HOL-ex: theory IArray

23:25:06 HOL-ex: theory IArray_Examples

23:25:07 HOL-ex: theory Iff_Oracle

23:25:07 HOL-ex: theory Induction_Schema

23:25:07 HOL-ex: theory Infinite_Set

23:25:07 HOL-ex: theory Intuitionistic

23:25:07 HOL-ex: theory Adhoc_Overloading_Examples

23:25:07 HOL-ex: theory LaTeXsugar

23:25:07 HOL-ex: theory Lagrange

23:25:07 HOL-ex: theory List_to_Set_Comprehension_Examples

23:25:08 HOL-ex: theory LocaleTest2

23:25:08 HOL-ex: theory ML

23:25:08 HOL-ex: theory Mapping

23:25:09 HOL-ex: theory Functions

23:25:09 HOL-ex: theory AList_Mapping

23:25:10 HOL-ex: theory Execute_Choice

23:25:10 HOL-ex: theory MonoidGroup

23:25:10 HOL-ex: theory Multiquote

23:25:11 HOL-ex: theory Multiset

23:25:14 HOL-ex: theory NatSum

23:25:14 HOL-ex: theory PER

23:25:14 HOL-ex: theory Parallel

23:25:15 HOL-ex: theory Bubblesort

23:25:15 HOL-ex: theory Factorial_Ring

23:25:16 HOL-ex: theory MergeSort

23:25:17 HOL-ex: theory Quicksort

23:25:17 HOL-ex: theory Perm

23:25:18 HOL-ex: theory Perm_Fragments

23:25:19 HOL-ex: theory Phantom_Type

23:25:20 HOL-ex: theory Cardinality

23:25:21 HOL-ex: theory FinFun

23:25:22 HOL-ex: theory Euclidean_Algorithm

23:25:23 HOL-ex: theory FinFunPred

23:25:23 HOL-ex: theory Numeral_Type

23:25:24 HOL-ex: theory Type_Length

23:25:24 HOL-ex: theory Primrec

23:25:25 HOL-ex: theory Records

23:25:29 HOL-ex: theory Reflection

23:25:29 HOL-ex: theory Refute_Examples

23:25:30 HOL-ex: theory Primes

23:25:30 HOL-ex: theory Eratosthenes

23:25:31 HOL-ex: theory Code_Timing

23:25:31 HOL-ex: theory Rewrite

23:25:32 HOL-ex: theory Rewrite_Examples

23:25:32 HOL-ex: theory SAT_Examples

23:25:32 HOL-ex: theory Seq

23:25:32 HOL-ex: theory Set_Comprehension_Pointfree_Examples

23:25:33 HOL-ex: theory Set_Theory

23:25:33 HOL-ex: theory Simproc_Tests

23:25:33 HOL-ex: theory Simps_Case_Conv

23:25:33 HOL-ex: theory Simps_Case_Conv_Examples

23:25:34 HOL-ex: theory Sudoku

23:25:35 HOL-ex: theory Tarski

23:25:36 HOL-ex: theory Termination

23:25:37 HOL-ex: theory ThreeDivides

23:25:38 HOL-ex: theory Argo_Examples

23:25:40 HOL-ex: theory Ballot

23:25:41 HOL-ex: theory BinEx

23:25:42 HOL-ex: theory Cubic_Quartic

23:25:42 HOL-ex: theory Dedekind_Real

23:25:42 HOL-ex: theory Gauge_Integration

23:25:43 HOL-ex: theory HarmonicSeries

23:25:43 HOL-ex: theory Parallel_Example

23:25:43 HOL-ex: theory Pythagoras

23:25:43 HOL-ex: theory Reflection_Examples

23:25:44 HOL-ex: theory Sqrt

23:25:44 HOL-ex: theory Sqrt_Script

23:25:45 HOL-ex: theory Sum_of_Powers

23:25:45 HOL-ex: theory Sum_of_Squares

23:25:48 HOL-ex: theory SOS

23:25:48 HOL-ex: theory SOS_Cert

23:25:48 HOL-ex: theory Transfer_Debug

23:25:48 HOL-ex: theory Transfer_Ex

23:25:48 HOL-ex: theory Transitive_Closure_Table_Ex

23:25:49 HOL-ex: theory Tree23

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

23:25:55 Timing HOL-Nominal-Examples (2 threads, 764.254s elapsed time, 1325.688s cpu time, 111.076s GC time, factor 1.73)

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

23:25:55 Finished HOL-Nominal-Examples (0:12:46 elapsed time, 0:22:08 cpu time, factor 1.73)

23:25:56 Running HOL-Decision_Procs ...

23:25:58 HOL-Decision_Procs: theory Code_Abstract_Nat

23:25:58 HOL-Decision_Procs: theory Commutative_Ring

23:25:58 HOL-Decision_Procs: theory Code_Target_Nat

23:25:58 HOL-Decision_Procs: theory DP_Library

23:25:58 HOL-Decision_Procs: theory Dense_Linear_Order

23:26:00 HOL-Decision_Procs: theory Dense_Linear_Order_Ex

23:26:00 HOL-Decision_Procs: theory Code_Target_Int

23:26:01 HOL-Decision_Procs: theory Code_Target_Numeral

23:26:01 HOL-Decision_Procs: theory Old_Recdef

23:26:02 HOL-Decision_Procs: theory Cooper

23:26:03 HOL-Decision_Procs: theory Commutative_Ring_Complete

23:26:03 HOL-Decision_Procs: theory Commutative_Ring_Ex

23:26:04 HOL-Decision_Procs: theory Ferrack

23:26:09 HOL-ex: theory Unification

23:26:12 HOL-ex: theory While_Combinator

23:26:13 HOL-ex: theory While_Combinator_Example

23:26:13 HOL-ex: theory Word_Type

23:26:28 HOL-Decision_Procs: theory Lattice_Algebras

23:26:34 HOL-Decision_Procs: theory Log_Nat

23:26:34 HOL-Decision_Procs: theory MIR

23:26:35 HOL-Decision_Procs: theory Float

23:26:40 HOL-Decision_Procs: theory Approximation

23:26:59 HOL-Codegenerator_Test: theory Generate_Target_Nat

23:27:21 HOL-Decision_Procs: theory Polynomial_List

23:27:31 HOL-Decision_Procs: theory Rat_Pair

23:27:31 HOL-Decision_Procs: theory Approximation_Ex

23:27:32 HOL-Decision_Procs: theory Approximation_Quickcheck_Ex

23:27:32 HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial

23:27:47 HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff

23:28:22 HOL-Decision_Procs: theory Decision_Procs

23:30:52 HOL-Codegenerator_Test: theory Code_Test_GHC

23:30:54 HOL-Codegenerator_Test: theory Code_Test_MLton

23:30:57 HOL-Codegenerator_Test: theory Code_Test_OCaml

23:30:58 HOL-Codegenerator_Test: theory Code_Test_SMLNJ

23:30:59 Timing HOL-Codegenerator_Test (2 threads, 641.660s elapsed time, 497.276s cpu time, 12.588s GC time, factor 0.77)

23:30:59 Finished HOL-Codegenerator_Test (0:10:48 elapsed time, 0:30:18 cpu time, factor 2.80)

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

23:31:01 HOL-Nitpick_Examples: theory Core_Nits

23:31:01 HOL-Nitpick_Examples: theory Datatype_Nits

23:31:02 HOL-Nitpick_Examples: theory Hotel_Nits

23:31:03 HOL-Nitpick_Examples: theory Induct_Nits

23:31:03 HOL-Nitpick_Examples: theory Integer_Nits

23:31:03 HOL-Nitpick_Examples: theory Mini_Nits

23:31:04 HOL-Nitpick_Examples: theory Mono_Nits

23:31:04 HOL-Nitpick_Examples: theory Pattern_Nits

23:31:04 HOL-Nitpick_Examples: theory Quotient_Syntax

23:31:04 HOL-Nitpick_Examples: theory Quotient_Product

23:31:04 HOL-Nitpick_Examples: theory Manual_Nits

23:31:05 HOL-Nitpick_Examples: theory Record_Nits

23:31:06 HOL-Nitpick_Examples: theory Refute_Nits

23:31:09 HOL-Nitpick_Examples: theory Special_Nits

23:31:10 HOL-Nitpick_Examples: theory Tests_Nits

23:31:11 HOL-Nitpick_Examples: theory Typedef_Nits

23:31:15 HOL-Nitpick_Examples: theory Nitpick_Examples

23:33:20 Timing HOL-Decision_Procs (2 threads, 441.858s elapsed time, 672.456s cpu time, 49.548s GC time, factor 1.52)

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

23:33:20 Finished HOL-Decision_Procs (0:07:24 elapsed time, 0:11:14 cpu time, factor 1.52)

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

23:33:22 HOL-Corec_Examples: theory BNF_Corec

23:33:22 HOL-Corec_Examples: theory BNF_Axiomatization

23:33:22 HOL-Corec_Examples: theory FSet

23:33:26 HOL-Corec_Examples: theory Nat_Bijection

23:33:27 HOL-Corec_Examples: theory Stream

23:33:29 HOL-Corec_Examples: theory Iterate_GPV

23:33:29 HOL-Corec_Examples: theory LFilter

23:33:33 HOL-Corec_Examples: theory Simple_Nesting

23:33:38 HOL-Corec_Examples: theory Stream_Processor

23:33:51 HOL-Corec_Examples: theory Paper_Examples

23:34:42 HOL-Corec_Examples: theory GPV_Bare_Bones

23:34:42 HOL-Corec_Examples: theory Merge_A

23:34:43 HOL-ex: theory Meson_Test

23:34:46 HOL-Corec_Examples: theory Merge_B

23:34:49 HOL-Corec_Examples: theory Merge_C

23:34:52 HOL-Corec_Examples: theory Merge_Poly

23:34:53 HOL-Corec_Examples: theory Merge_D

23:35:00 HOL-Corec_Examples: theory Misc_Mono

23:35:14 Timing HOL-ex (2 threads, 625.466s elapsed time, 969.412s cpu time, 82.684s GC time, factor 1.55)

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

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

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

23:35:14 Finished HOL-ex (0:10:41 elapsed time, 0:17:05 cpu time, factor 1.60)

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

23:35:16 HOL-Hoare_Parallel: theory Graph

23:35:16 HOL-Hoare_Parallel: theory OG_Com

23:35:16 HOL-Hoare_Parallel: theory Quote_Antiquote

23:35:16 HOL-Hoare_Parallel: theory RG_Com

23:35:18 HOL-Hoare_Parallel: theory RG_Tran

23:35:19 HOL-Hoare_Parallel: theory OG_Tran

23:35:21 HOL-Hoare_Parallel: theory RG_Hoare

23:35:21 HOL-Hoare_Parallel: theory OG_Hoare

23:35:21 HOL-Hoare_Parallel: theory OG_Tactics

23:35:21 HOL-Hoare_Parallel: theory RG_Syntax

23:35:22 HOL-Hoare_Parallel: theory RG_Examples

23:35:22 HOL-Hoare_Parallel: theory OG_Syntax

23:35:22 HOL-Hoare_Parallel: theory Gar_Coll

23:35:24 HOL-Hoare_Parallel: theory Mul_Gar_Coll

23:35:24 HOL-Hoare_Parallel: theory OG_Examples

23:35:27 HOL-Hoare_Parallel: theory Hoare_Parallel

23:35:34 HOL-Corec_Examples: theory Misc_Poly

23:35:46 Timing HOL-Nitpick_Examples (2 threads, 284.433s elapsed time, 110.448s cpu time, 2.140s GC time, factor 0.39)

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

23:35:46 Finished HOL-Nitpick_Examples (0:04:46 elapsed time, 0:10:05 cpu time, factor 2.11)

23:35:46 Running HOL-Proofs-Lambda ...

23:35:48 HOL-Proofs-Lambda: theory GCD

23:36:02 HOL-Proofs-Lambda: theory Code_Target_Int

23:36:03 HOL-Proofs-Lambda: theory Commutation

23:36:03 HOL-Proofs-Lambda: theory Lambda

23:36:03 HOL-Proofs-Lambda: theory ListOrder

23:36:05 HOL-Proofs-Lambda: theory ListApplication

23:36:05 HOL-Proofs-Lambda: theory ParRed

23:36:05 HOL-Proofs-Lambda: theory LambdaType

23:36:06 HOL-Proofs-Lambda: theory Eta

23:36:07 HOL-Proofs-Lambda: theory ListBeta

23:36:08 HOL-Proofs-Lambda: theory InductTermi

23:36:08 HOL-Proofs-Lambda: theory StrongNorm

23:36:09 HOL-Proofs-Lambda: theory NormalForm

23:36:10 HOL-Proofs-Lambda: theory Standardization

23:36:11 HOL-Proofs-Lambda: theory WeakNorm

23:36:27 HOL-Corec_Examples: theory Small_Concrete

23:36:54 HOL-Corec_Examples: theory Stream_Friends

23:37:01 HOL-Corec_Examples: theory TLList_Friends

23:37:17 HOL-Corec_Examples: theory Type_Class

23:37:40 Timing HOL-Corec_Examples (2 threads, 257.720s elapsed time, 469.828s cpu time, 46.640s GC time, factor 1.82)

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

23:37:40 Finished HOL-Corec_Examples (0:04:20 elapsed time, 0:07:52 cpu time, factor 1.81)

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

23:37:42 HOL-MicroJava: theory While_Combinator

23:37:44 HOL-MicroJava: theory Eisbach

23:37:44 HOL-MicroJava: theory Transitive_Closure_Table

23:37:44 HOL-MicroJava: theory Semilat

23:37:44 HOL-MicroJava: theory JBasis

23:37:45 HOL-MicroJava: theory AuxLemmas

23:37:45 HOL-MicroJava: theory Type

23:37:45 HOL-MicroJava: theory Err

23:37:45 HOL-MicroJava: theory Listn

23:37:46 HOL-MicroJava: theory Typing_Framework

23:37:46 HOL-MicroJava: theory Opt

23:37:46 HOL-MicroJava: theory Product

23:37:46 HOL-MicroJava: theory SemilatAlg

23:37:47 HOL-MicroJava: theory Decl

23:37:47 HOL-MicroJava: theory Value

23:37:47 HOL-MicroJava: theory SystemClasses

23:37:47 HOL-MicroJava: theory TypeRel

23:37:48 HOL-MicroJava: theory Term

23:37:48 HOL-MicroJava: theory WellForm

23:37:48 HOL-MicroJava: theory State

23:37:49 HOL-MicroJava: theory Exceptions

23:37:49 HOL-MicroJava: theory Kildall

23:37:49 HOL-MicroJava: theory LBVSpec

23:37:50 HOL-MicroJava: theory LBVComplete

23:37:51 HOL-MicroJava: theory LBVCorrect

23:37:51 HOL-MicroJava: theory Typing_Framework_err

23:37:51 HOL-MicroJava: theory WellType

23:37:51 HOL-MicroJava: theory Abstract_BV

23:37:51 HOL-MicroJava: theory Semilattices

23:37:52 HOL-MicroJava: theory Conform

23:37:52 HOL-MicroJava: theory Eval

23:37:52 HOL-MicroJava: theory JVMState

23:37:52 HOL-MicroJava: theory JVMInstructions

23:37:54 HOL-MicroJava: theory JVMExceptions

23:37:54 HOL-MicroJava: theory JVMExecInstr

23:37:54 HOL-MicroJava: theory JVMExec

23:37:55 HOL-MicroJava: theory DefsComp

23:37:55 HOL-MicroJava: theory Index

23:37:55 HOL-MicroJava: theory JVMDefensive

23:37:56 HOL-MicroJava: theory JVMListExample

23:37:56 HOL-MicroJava: theory Example

23:37:57 HOL-MicroJava: theory JListExample

23:37:57 HOL-MicroJava: theory JTypeSafe

23:37:57 HOL-MicroJava: theory TypeInf

23:37:58 HOL-MicroJava: theory JType

23:37:58 HOL-MicroJava: theory JVMType

23:37:58 HOL-MicroJava: theory Effect

23:37:58 HOL-MicroJava: theory TranslCompTp

23:37:59 HOL-MicroJava: theory TranslComp

23:37:59 HOL-MicroJava: theory LemmasComp

23:38:00 HOL-MicroJava: theory CorrComp

23:38:16 Timing HOL-Hoare_Parallel (2 threads, 176.851s elapsed time, 316.740s cpu time, 4.628s GC time, factor 1.79)

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

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

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

23:38:16 Finished HOL-Hoare_Parallel (0:03:02 elapsed time, 0:05:23 cpu time, factor 1.78)

23:38:16 Running HOL-Datatype_Examples ...

23:38:18 HOL-Datatype_Examples: theory BNF_Axiomatization

23:38:18 HOL-Datatype_Examples: theory FSet

23:38:18 Timing HOL-Proofs-Lambda (2 threads, 147.489s elapsed time, 168.636s cpu time, 5.860s GC time, factor 1.14)

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

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

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

23:38:18 Finished HOL-Proofs-Lambda (0:02:32 elapsed time, 0:02:54 cpu time, factor 1.15)

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

23:38:19 HOL-Datatype_Examples: theory Infinite_Set

23:38:19 HOL-Datatype_Examples: theory Lift_BNF

23:38:20 HOL-MicroJava: theory BVSpec

23:38:20 HOL-MicroJava: theory EffectMono

23:38:20 HOL-MicroJava: theory Altern

23:38:20 HOL-MicroJava: theory Correct

23:38:20 HOL-MicroJava: theory Typing_Framework_JVM

23:38:20 HOL-IMP: theory List_lexord

23:38:20 HOL-IMP: theory Char_ord

23:38:21 HOL-IMP: theory Quotient_Syntax

23:38:21 HOL-IMP: theory Simps_Case_Conv

23:38:21 HOL-IMP: theory Quotient_Option

23:38:21 HOL-IMP: theory Quotient_Product

23:38:21 HOL-IMP: theory Quotient_Set

23:38:21 HOL-MicroJava: theory BVSpecTypeSafe

23:38:21 HOL-IMP: theory Extended

23:38:21 HOL-IMP: theory Quotient_List

23:38:21 HOL-MicroJava: theory JVM

23:38:21 HOL-MicroJava: theory CorrCompTp

23:38:21 HOL-IMP: theory While_Combinator

23:38:21 HOL-Datatype_Examples: theory Milner_Tofte

23:38:22 HOL-MicroJava: theory BVNoTypeError

23:38:22 HOL-Datatype_Examples: theory Lambda_Term

23:38:22 HOL-MicroJava: theory BVExample

23:38:23 HOL-MicroJava: theory LBVJVM

23:38:23 HOL-MicroJava: theory MicroJava

23:38:23 HOL-Datatype_Examples: theory Misc_Codatatype

23:38:24 HOL-Datatype_Examples: theory Prelim

23:38:24 HOL-Datatype_Examples: theory DTree

23:38:25 HOL-Datatype_Examples: theory Parallel

23:38:25 HOL-IMP: theory AExp

23:38:25 HOL-IMP: theory C_like

23:38:25 HOL-Datatype_Examples: theory TreeFsetI

23:38:26 HOL-Datatype_Examples: theory Gram_Lang

23:38:26 HOL-IMP: theory ASM

23:38:27 HOL-Datatype_Examples: theory Nat_Bijection

23:38:27 HOL-IMP: theory BExp

23:38:27 HOL-Datatype_Examples: theory Stream

23:38:29 HOL-IMP: theory Complete_Lattice

23:38:29 HOL-Datatype_Examples: theory Process

23:38:29 HOL-IMP: theory Com

23:38:29 HOL-IMP: theory Procs

23:38:30 HOL-IMP: theory ACom

23:38:30 HOL-IMP: theory Abs_Int_Tests

23:38:30 HOL-IMP: theory Big_Step

23:38:31 HOL-IMP: theory Denotational

23:38:31 HOL-IMP: theory Hoare

23:38:31 HOL-IMP: theory Hoare_Examples

23:38:32 HOL-IMP: theory Hoare_Total

23:38:32 HOL-IMP: theory Hoare_Sound_Complete

23:38:32 HOL-IMP: theory Hoare_Total_EX

23:38:32 HOL-Datatype_Examples: theory Stream_Processor

23:38:32 HOL-IMP: theory VCG

23:38:32 HOL-IMP: theory VCG_Total_EX

23:38:33 HOL-IMP: theory Sec_Type_Expr

23:38:33 HOL-IMP: theory Sem_Equiv

23:38:34 HOL-IMP: theory Sec_Typing

23:38:34 HOL-IMP: theory Sec_TypingT

23:38:34 HOL-IMP: theory Vars

23:38:34 HOL-IMP: theory Procs_Dyn_Vars_Dyn

23:38:35 HOL-IMP: theory Def_Init

23:38:35 HOL-IMP: theory Def_Init_Exp

23:38:35 HOL-IMP: theory Fold

23:38:35 HOL-IMP: theory Def_Init_Big

23:38:35 HOL-IMP: theory Live

23:38:35 HOL-IMP: theory Procs_Stat_Vars_Dyn

23:38:36 HOL-IMP: theory Procs_Stat_Vars_Stat

23:38:36 HOL-IMP: theory Collecting

23:38:37 HOL-IMP: theory Collecting1

23:38:37 HOL-IMP: theory Collecting_Examples

23:38:38 HOL-IMP: theory OO

23:38:38 HOL-Datatype_Examples: theory Old_Datatype

23:38:39 HOL-Datatype_Examples: theory Compat

23:38:42 HOL-IMP: theory Star

23:38:42 HOL-IMP: theory Compiler

23:38:47 HOL-IMP: theory Compiler2

23:38:48 HOL-IMP: theory Def_Init_Small

23:38:48 HOL-IMP: theory Small_Step

23:38:49 HOL-IMP: theory Types

23:38:49 HOL-IMP: theory Finite_Reachable

23:38:49 HOL-IMP: theory Abs_Int_init

23:38:50 HOL-IMP: theory Abs_Int0

23:38:52 HOL-IMP: theory Abs_State

23:38:52 HOL-IMP: theory Abs_Int1

23:38:53 HOL-IMP: theory Poly_Types

23:38:53 HOL-IMP: theory Abs_Int1_const

23:38:53 HOL-IMP: theory Abs_Int1_parity

23:38:54 HOL-IMP: theory Abs_Int2

23:38:54 HOL-IMP: theory Live_True

23:38:55 HOL-IMP: theory Abs_Int2_ivl

23:38:57 HOL-IMP: theory Abs_Int3

23:39:12 HOL-Datatype_Examples: theory Countable

23:39:13 HOL-Datatype_Examples: theory Misc_Datatype

23:39:30 HOL-Datatype_Examples: theory Misc_Primcorec

23:39:32 HOL-Datatype_Examples: theory TreeFI

23:39:33 HOL-Datatype_Examples: theory Koenig

23:40:24 HOL-Datatype_Examples: theory Misc_Primrec

23:40:29 Timing HOL-MicroJava (2 threads, 162.214s elapsed time, 276.944s cpu time, 8.044s GC time, factor 1.71)

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

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

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

23:40:29 Finished HOL-MicroJava (0:02:47 elapsed time, 0:04:44 cpu time, factor 1.69)

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

23:40:31 HOL-Imperative_HOL: theory Adhoc_Overloading

23:40:31 HOL-Imperative_HOL: theory LaTeXsugar

23:40:31 HOL-Imperative_HOL: theory Monad_Syntax

23:40:31 HOL-Imperative_HOL: theory Nat_Bijection

23:40:31 HOL-Imperative_HOL: theory Old_Datatype

23:40:32 HOL-Imperative_HOL: theory Countable

23:40:34 HOL-Imperative_HOL: theory Code_Abstract_Nat

23:40:34 HOL-Imperative_HOL: theory Code_Target_Int

23:40:34 HOL-Imperative_HOL: theory Code_Target_Nat

23:40:34 HOL-Imperative_HOL: theory Multiset

23:40:34 HOL-Imperative_HOL: theory Code_Target_Numeral

23:40:34 HOL-Imperative_HOL: theory Heap

23:40:36 HOL-Imperative_HOL: theory Heap_Monad

23:40:38 HOL-Imperative_HOL: theory Array

23:40:39 HOL-Imperative_HOL: theory Ref

23:40:39 HOL-Imperative_HOL: theory List_Sublist

23:40:39 HOL-Imperative_HOL: theory Imperative_HOL

23:40:39 HOL-Imperative_HOL: theory Linked_Lists

23:40:39 HOL-Imperative_HOL: theory Overview

23:40:39 HOL-Imperative_HOL: theory Subarray

23:40:40 HOL-Imperative_HOL: theory Imperative_Quicksort

23:41:08 Timing HOL-Datatype_Examples (2 threads, 168.970s elapsed time, 300.212s cpu time, 35.888s GC time, factor 1.78)

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

23:41:08 Finished HOL-Datatype_Examples (0:02:51 elapsed time, 0:05:23 cpu time, factor 1.89)

23:41:08 Running HOL-Proofs-Extraction ...

23:41:08 HOL-Imperative_HOL: theory Imperative_Reverse

23:41:11 HOL-Proofs-Extraction: theory Adhoc_Overloading

23:41:11 HOL-Proofs-Extraction: theory Binomial

23:41:11 HOL-Proofs-Extraction: theory Code_Abstract_Nat

23:41:11 HOL-Proofs-Extraction: theory Code_Target_Nat

23:41:12 HOL-Imperative_HOL: theory RBT_Impl

23:41:12 HOL-Proofs-Extraction: theory GCD

23:41:13 Timing HOL-IMP (2 threads, 166.923s elapsed time, 268.832s cpu time, 11.676s GC time, factor 1.61)

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

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

23:41:13 Finished HOL-IMP (0:02:54 elapsed time, 0:04:35 cpu time, factor 1.58)

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

23:41:15 HOL-Quickcheck_Examples: theory AList

23:41:15 HOL-Quickcheck_Examples: theory Completeness

23:41:15 HOL-Quickcheck_Examples: theory Dlist

23:41:17 HOL-Quickcheck_Examples: theory Multiset

23:41:17 HOL-Quickcheck_Examples: theory DAList

23:41:18 HOL-Quickcheck_Examples: theory Quickcheck_Interfaces

23:41:19 HOL-Quickcheck_Examples: theory Quickcheck_Lattice_Examples

23:41:20 HOL-Quickcheck_Examples: theory Quickcheck_Nesting

23:41:21 HOL-Quickcheck_Examples: theory Quickcheck_Nesting_Example

23:41:24 HOL-Quickcheck_Examples: theory DAList_Multiset

23:41:24 HOL-Quickcheck_Examples: theory Quickcheck_Examples

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

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

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

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

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

23:41:35 HOL-Imperative_HOL: theory Sorted_List

23:41:44 HOL-Imperative_HOL: theory SatChecker

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

23:41:53 HOL-Imperative_HOL: theory Imperative_HOL_ex

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

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

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

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

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

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

23:42:40 HOL-Quickcheck_Examples: theory Predicate_Compile_Alternative_Defs

23:42:40 HOL-Quickcheck_Examples: theory Quickcheck_Narrowing_Examples

23:42:41 HOL-Quickcheck_Examples: theory Predicate_Compile_Quickcheck

23:42:41 HOL-Quickcheck_Examples: theory Hotel_Example

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

23:43:01 Timing HOL-Imperative_HOL (2 threads, 148.841s elapsed time, 161.324s cpu time, 5.552s GC time, factor 1.08)

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

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

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

23:43:01 Finished HOL-Imperative_HOL (0:02:32 elapsed time, 0:06:40 cpu time, factor 2.63)

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

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

23:43:03 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Alternative_Defs

23:43:03 HOL-Predicate_Compile_Examples: theory Examples

23:43:03 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck

23:43:03 HOL-Predicate_Compile_Examples: theory IMP_1

23:43:04 HOL-Predicate_Compile_Examples: theory IMP_2

23:43:05 HOL-Predicate_Compile_Examples: theory IMP_3

23:43:06 HOL-Predicate_Compile_Examples: theory IMP_4

23:43:07 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck_Examples

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

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

23:43:12 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Tests

23:43:15 HOL-Predicate_Compile_Examples: theory Specialisation_Examples

23:43:27 Timing HOL-Proofs-Extraction (2 threads, 132.730s elapsed time, 209.204s cpu time, 9.516s GC time, factor 1.58)

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

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

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

23:43:27 Finished HOL-Proofs-Extraction (0:02:18 elapsed time, 0:03:33 cpu time, factor 1.54)

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

23:43:30 HOL-Bali: theory Old_Recdef

23:43:32 HOL-Bali: theory Basis

23:43:34 HOL-Bali: theory Name

23:43:34 HOL-Bali: theory Table

23:43:38 HOL-Bali: theory Type

23:43:40 HOL-Bali: theory Value

23:43:41 HOL-Bali: theory Term

23:43:45 Timing HOL-Quickcheck_Examples (2 threads, 149.574s elapsed time, 167.208s cpu time, 5.132s GC time, factor 1.12)

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

23:43:45 Finished HOL-Quickcheck_Examples (0:02:31 elapsed time, 0:04:07 cpu time, factor 1.63)

23:43:45 Running HOL-Number_Theory ...

23:43:49 HOL-Number_Theory: theory Congruence

23:43:49 HOL-Number_Theory: theory FuncSet

23:43:50 HOL-Number_Theory: theory Multiset

23:43:51 HOL-Number_Theory: theory Lattice

23:43:54 HOL-Number_Theory: theory Group

23:43:55 HOL-Number_Theory: theory FiniteProduct

23:43:56 HOL-Number_Theory: theory Ring

23:44:02 HOL-Bali: theory Decl

23:44:06 HOL-Bali: theory TypeRel

23:44:06 HOL-Bali: theory DeclConcepts

23:44:09 HOL-Bali: theory State

23:44:09 HOL-Bali: theory WellType

23:44:10 HOL-Bali: theory Conform

23:44:11 HOL-Bali: theory Eval

23:44:13 HOL-Bali: theory DefiniteAssignment

23:44:16 HOL-Number_Theory: theory MiscAlgebra

23:44:16 HOL-Number_Theory: theory Factorial_Ring

23:44:17 HOL-Number_Theory: theory Fib

23:44:19 HOL-Bali: theory WellForm

23:44:20 HOL-Bali: theory DefiniteAssignmentCorrect

23:44:20 HOL-Bali: theory Example

23:44:21 HOL-Bali: theory TypeSafe

23:44:23 HOL-Bali: theory Evaln

23:44:23 HOL-Number_Theory: theory Euclidean_Algorithm

23:44:26 HOL-Bali: theory AxSem

23:44:26 HOL-Bali: theory Trans

23:44:29 HOL-Bali: theory AxCompl

23:44:29 HOL-Bali: theory AxSound

23:44:30 HOL-Bali: theory AxExample

23:44:31 HOL-Number_Theory: theory Primes

23:44:32 HOL-Number_Theory: theory Cong

23:44:32 HOL-Number_Theory: theory Eratosthenes

23:44:32 HOL-Number_Theory: theory Residues

23:44:34 HOL-Number_Theory: theory Euler_Criterion

23:44:35 HOL-Number_Theory: theory Gauss

23:44:35 HOL-Number_Theory: theory Quadratic_Reciprocity

23:44:35 HOL-Number_Theory: theory Pocklington

23:44:35 HOL-Number_Theory: theory Number_Theory

23:44:39 HOL-Predicate_Compile_Examples: theory Code_Prolog

23:44:39 HOL-Predicate_Compile_Examples: theory Hotel_Example

23:44:39 HOL-Predicate_Compile_Examples: theory Code_Prolog_Examples

23:44:41 HOL-Predicate_Compile_Examples: theory Context_Free_Grammar_Example

23:44:41 HOL-Predicate_Compile_Examples: theory Lambda_Example

23:44:42 HOL-Predicate_Compile_Examples: theory Hotel_Example_Prolog

23:44:42 HOL-Predicate_Compile_Examples: theory List_Examples

23:44:47 HOL-Predicate_Compile_Examples: theory Reg_Exp_Example

23:44:54 Timing HOL-Predicate_Compile_Examples (2 threads, 110.443s elapsed time, 179.964s cpu time, 8.300s GC time, factor 1.63)

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

23:44:54 Finished HOL-Predicate_Compile_Examples (0:01:52 elapsed time, 0:04:41 cpu time, factor 2.50)

23:44:54 Running HOL-Algebra ...

23:44:56 HOL-Algebra: theory FuncSet

23:44:56 HOL-Algebra: theory Multiset

23:45:01 HOL-Algebra: theory Factorial_Ring

23:45:01 HOL-Algebra: theory Permutation

23:45:08 HOL-Algebra: theory Euclidean_Algorithm

23:45:16 Timing HOL-Number_Theory (2 threads, 83.215s elapsed time, 134.996s cpu time, 4.300s GC time, factor 1.62)

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

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

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

23:45:16 Finished HOL-Number_Theory (0:01:30 elapsed time, 0:02:21 cpu time, factor 1.57)

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

23:45:16 HOL-Algebra: theory Primes

23:45:18 HOL-UNITY: theory Multiset

23:45:18 HOL-UNITY: theory ListOrder

23:45:19 HOL-UNITY: theory UNITY

23:45:20 HOL-UNITY: theory Constrains

23:45:20 HOL-Algebra: theory Exponent

23:45:20 HOL-Algebra: theory Congruence

23:45:20 HOL-UNITY: theory Deadlock

23:45:20 HOL-UNITY: theory FP

23:45:20 HOL-UNITY: theory Network

23:45:21 HOL-Algebra: theory Lattice

23:45:21 HOL-UNITY: theory WFair

23:45:22 HOL-UNITY: theory SubstAx

23:45:22 HOL-Algebra: theory Group

23:45:23 HOL-UNITY: theory Detects

23:45:23 HOL-UNITY: theory Union

23:45:23 HOL-UNITY: theory Comp

23:45:23 HOL-UNITY: theory Multiset_Order

23:45:23 HOL-UNITY: theory Follows

23:45:24 HOL-UNITY: theory Guar

23:45:24 HOL-Algebra: theory Bij

23:45:24 HOL-Algebra: theory Coset

23:45:24 HOL-UNITY: theory Extend

23:45:24 HOL-UNITY: theory Transformers

23:45:24 HOL-UNITY: theory ProgressSets

23:45:25 HOL-UNITY: theory Project

23:45:25 HOL-UNITY: theory Rename

23:45:25 HOL-Algebra: theory FiniteProduct

23:45:25 HOL-UNITY: theory Lift_prog

23:45:25 HOL-UNITY: theory ELT

23:45:25 HOL-Algebra: theory Ring

23:45:26 HOL-UNITY: theory PPROD

23:45:26 HOL-UNITY: theory Token

23:45:26 HOL-UNITY: theory UNITY_Main

23:45:26 HOL-Algebra: theory Sylow

23:45:26 HOL-UNITY: theory AllocBase

23:45:27 HOL-UNITY: theory Alloc

23:45:27 HOL-UNITY: theory AllocImpl

23:45:27 HOL-Algebra: theory Divisibility

23:45:29 HOL-Algebra: theory AbelCoset

23:45:29 HOL-UNITY: theory Client

23:45:29 HOL-UNITY: theory Channel

23:45:29 HOL-UNITY: theory Common

23:45:29 HOL-UNITY: theory Counter

23:45:30 HOL-UNITY: theory Counterc

23:45:30 HOL-Algebra: theory Module

23:45:30 HOL-UNITY: theory Handshake

23:45:30 HOL-UNITY: theory Lift

23:45:30 HOL-UNITY: theory Mutex

23:45:31 HOL-UNITY: theory NSP_Bad

23:45:31 HOL-UNITY: theory PriorityAux

23:45:31 HOL-UNITY: theory Priority

23:45:31 HOL-UNITY: theory Progress

23:45:31 HOL-UNITY: theory Reach

23:45:32 HOL-UNITY: theory TimerArray

23:45:32 HOL-UNITY: theory Reachability

23:45:35 HOL-Algebra: theory Ideal

23:45:39 HOL-Algebra: theory RingHom

23:45:40 Timing HOL-Bali (2 threads, 120.719s elapsed time, 197.632s cpu time, 10.632s GC time, factor 1.64)

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

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

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

23:45:40 Finished HOL-Bali (0:02:13 elapsed time, 0:03:33 cpu time, factor 1.60)

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

23:45:41 HOL-Algebra: theory QuotRing

23:45:41 HOL-Algebra: theory UnivPoly

23:45:42 HOL-Algebra: theory IntRing

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

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

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

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

23:46:16 Timing HOL-Algebra (2 threads, 76.383s elapsed time, 144.468s cpu time, 7.808s GC time, factor 1.89)

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

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

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

23:46:16 Finished HOL-Algebra (0:01:22 elapsed time, 0:02:32 cpu time, factor 1.85)

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

23:46:18 HOL-SET_Protocol: theory Nat_Bijection

23:46:19 HOL-SET_Protocol: theory Message_SET

23:46:21 HOL-SET_Protocol: theory Event_SET

23:46:22 HOL-SET_Protocol: theory Public_SET

23:46:23 HOL-SET_Protocol: theory Cardholder_Registration

23:46:23 HOL-SET_Protocol: theory Merchant_Registration

23:46:24 HOL-SET_Protocol: theory Purchase

23:46:26 HOL-SET_Protocol: theory SET_Protocol

23:46:27 Timing HOL-UNITY (2 threads, 64.580s elapsed time, 101.108s cpu time, 4.228s GC time, factor 1.57)

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

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

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

23:46:27 Finished HOL-UNITY (0:01:10 elapsed time, 0:01:49 cpu time, factor 1.55)

23:46:27 Running Corec ...

23:46:29 Corec: theory Setup

23:46:29 Corec: theory BNF_Corec

23:46:29 Corec: theory FSet

23:46:34 Corec: theory Corec

23:46:44 Timing HOL-Word-SMT_Examples (2 threads, 60.755s elapsed time, 79.572s cpu time, 0.784s GC time, factor 1.31)

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

23:46:44 Finished HOL-Word-SMT_Examples (0:01:03 elapsed time, 0:01:24 cpu time, factor 1.33)

23:46:44 Running HOL-Quotient_Examples ...

23:46:46 HOL-Quotient_Examples: theory FuncSet

23:46:46 HOL-Quotient_Examples: theory Congruence

23:46:46 HOL-Quotient_Examples: theory Lift_DList

23:46:47 HOL-Quotient_Examples: theory Lattice

23:46:47 HOL-Quotient_Examples: theory Lift_FSet

23:46:47 HOL-Quotient_Examples: theory Lift_Set

23:46:48 HOL-Quotient_Examples: theory Lifting_Code_Dt_Test

23:46:49 HOL-Quotient_Examples: theory Group

23:46:50 HOL-Quotient_Examples: theory Int_Pow

23:46:51 HOL-Quotient_Examples: theory Multiset

23:46:55 HOL-Quotient_Examples: theory Quotient_Syntax

23:46:55 HOL-Quotient_Examples: theory Lift_Fun

23:46:55 HOL-Quotient_Examples: theory Quotient_Message

23:46:56 HOL-Quotient_Examples: theory Quotient_Option

23:46:56 HOL-Quotient_Examples: theory Quotient_Product

23:46:56 HOL-Quotient_Examples: theory Quotient_Rat

23:46:57 HOL-Quotient_Examples: theory Quotient_Set

23:46:57 HOL-Quotient_Examples: theory Quotient_List

23:46:58 HOL-Quotient_Examples: theory DList

23:46:58 HOL-Quotient_Examples: theory Quotient_FSet

23:46:59 HOL-Quotient_Examples: theory Quotient_Int

23:47:14 Timing HOL-SET_Protocol (2 threads, 51.779s elapsed time, 85.360s cpu time, 1.808s GC time, factor 1.65)

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

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

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

23:47:14 Finished HOL-SET_Protocol (0:00:57 elapsed time, 0:01:29 cpu time, factor 1.56)

23:47:14 Running Datatypes ...

23:47:16 Datatypes: theory Setup

23:47:16 Datatypes: theory BNF_Axiomatization

23:47:16 Datatypes: theory Cardinal_Notations

23:47:17 Datatypes: theory FSet

23:47:17 Datatypes: theory Nat_Bijection

23:47:18 Datatypes: theory Old_Datatype

23:47:20 Datatypes: theory Countable

23:47:23 Datatypes: theory Simps_Case_Conv

23:47:23 Datatypes: theory Datatypes

23:47:27 Timing Corec (2 threads, 56.124s elapsed time, 80.300s cpu time, 4.944s GC time, factor 1.43)

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

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

23:47:27 Finished Corec (0:01:00 elapsed time, 0:01:24 cpu time, factor 1.40)

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

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

23:47:34 Timing HOL-Quotient_Examples (2 threads, 47.646s elapsed time, 73.860s cpu time, 6.788s GC time, factor 1.55)

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

23:47:34 Finished HOL-Quotient_Examples (0:00:49 elapsed time, 0:02:08 cpu time, factor 2.58)

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

23:47:36 HOL-Metis_Examples: theory Binary_Tree

23:47:36 HOL-Metis_Examples: theory Dense_Linear_Order

23:47:37 HOL-Metis_Examples: theory FuncSet

23:47:38 HOL-Metis_Examples: theory Abstraction

23:47:38 HOL-Metis_Examples: theory Function_Algebras

23:47:38 HOL-Metis_Examples: theory Message

23:47:38 HOL-Metis_Examples: theory Set_Algebras

23:47:39 HOL-Metis_Examples: theory Big_O

23:47:39 HOL-Metis_Examples: theory Sets

23:47:39 HOL-Metis_Examples: theory Tarski

23:47:41 HOL-Metis_Examples: theory Clausification

23:47:41 HOL-Metis_Examples: theory Trans_Closure

23:47:41 HOL-Metis_Examples: theory Type_Encodings

23:47:41 HOL-Metis_Examples: theory Proxies

23:48:02 Timing Datatypes (2 threads, 43.124s elapsed time, 66.448s cpu time, 4.752s GC time, factor 1.54)

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

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

23:48:02 Finished Datatypes (0:00:47 elapsed time, 0:01:10 cpu time, factor 1.48)

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

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

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

23:48:10 Warning: missing document directory

23:48:10 Timing HOL-Analysis-ex (2 threads, 36.981s elapsed time, 43.824s cpu time, 0.496s GC time, factor 1.19)

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

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

23:48:10 Running Tutorial ...

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

23:48:12 Tutorial: theory ToyList_Test

23:48:13 Timing HOL-Metis_Examples (2 threads, 36.293s elapsed time, 56.164s cpu time, 2.288s GC time, factor 1.55)

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

23:48:13 Finished HOL-Metis_Examples (0:00:38 elapsed time, 0:01:11 cpu time, factor 1.85)

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

23:48:13 Tutorial: theory ABexpr

23:48:13 Tutorial: theory AB

23:48:14 Tutorial: theory AdvancedInd

23:48:14 Tutorial: theory Base

23:48:14 Tutorial: theory CTL

23:48:15 HOL-Isar_Examples: theory Lattice_Syntax

23:48:15 HOL-Isar_Examples: theory Multiset

23:48:15 Tutorial: theory CTLind

23:48:15 Tutorial: theory PDL

23:48:16 Tutorial: theory CodeGen

23:48:16 Tutorial: theory Nested

23:48:18 Tutorial: theory Even

23:48:18 Tutorial: theory Fundata

23:48:18 Tutorial: theory Advanced

23:48:19 Tutorial: theory Ifexpr

23:48:20 HOL-Isar_Examples: theory Factorial_Ring

23:48:20 Tutorial: theory Itrev

23:48:20 Tutorial: theory Mutual

23:48:20 Tutorial: theory Option2

23:48:20 Tutorial: theory Plus

23:48:20 Tutorial: theory Star

23:48:21 Tutorial: theory ToyList

23:48:21 Tutorial: theory Tree

23:48:22 Tutorial: theory Trie

23:48:22 Tutorial: theory Tree2

23:48:22 Tutorial: theory appendix

23:48:22 Tutorial: theory case_exprs

23:48:22 Tutorial: theory fakenat

23:48:22 Tutorial: theory fun0

23:48:23 Tutorial: theory natsum

23:48:23 Tutorial: theory pairs2

23:48:23 Tutorial: theory prime_def

23:48:23 Tutorial: theory simp

23:48:23 Tutorial: theory simp2

23:48:23 Tutorial: theory types

23:48:23 Tutorial: theory unfoldnested

23:48:27 HOL-Isar_Examples: theory Euclidean_Algorithm

23:48:35 HOL-Isar_Examples: theory Primes

23:48:35 Tutorial: theory Message

23:48:35 Tutorial: theory Documents

23:48:37 Tutorial: theory Event

23:48:38 Tutorial: theory Public

23:48:38 Tutorial: theory NS_Public

23:48:39 HOL-Isar_Examples: theory First_Order_Logic

23:48:39 HOL-Isar_Examples: theory Basic_Logic

23:48:39 HOL-Isar_Examples: theory Cantor

23:48:39 HOL-Isar_Examples: theory Drinker

23:48:39 HOL-Isar_Examples: theory Expr_Compiler

23:48:39 HOL-Isar_Examples: theory Group

23:48:39 Tutorial: theory Setup

23:48:39 HOL-Isar_Examples: theory Group_Context

23:48:39 Tutorial: theory Basic

23:48:39 Tutorial: theory Blast

23:48:39 HOL-Isar_Examples: theory Group_Notepad

23:48:40 Tutorial: theory Force

23:48:40 Tutorial: theory Pairs

23:48:40 HOL-Isar_Examples: theory Hoare

23:48:40 Tutorial: theory Records

23:48:40 Tutorial: theory Overloading

23:48:40 Tutorial: theory Axioms

23:48:40 HOL-Isar_Examples: theory Knaster_Tarski

23:48:40 Tutorial: theory Numbers

23:48:40 HOL-Isar_Examples: theory Fibonacci

23:48:40 HOL-Isar_Examples: theory Hoare_Ex

23:48:41 Tutorial: theory Typedefs

23:48:41 HOL-Isar_Examples: theory Mutilated_Checkerboard

23:48:41 HOL-Isar_Examples: theory Peirce

23:48:41 HOL-Isar_Examples: theory Puzzle

23:48:41 HOL-Isar_Examples: theory Structured_Statements

23:48:41 HOL-Isar_Examples: theory Summation

23:48:41 HOL-Isar_Examples: theory Higher_Order_Logic

23:48:41 Tutorial: theory Recur

23:48:41 Tutorial: theory Functions

23:48:41 Tutorial: theory Relations

23:48:41 Tutorial: theory TPrimes

23:48:41 Tutorial: theory Tacticals

23:48:41 Tutorial: theory Examples

23:48:41 Tutorial: theory Forward

23:48:42 Tutorial: theory find2

23:48:46 Timing HOL-Isar_Examples (2 threads, 28.761s elapsed time, 51.888s cpu time, 2.192s GC time, factor 1.80)

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

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

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

23:48:46 Finished HOL-Isar_Examples (0:00:32 elapsed time, 0:00:57 cpu time, factor 1.73)

23:48:46 Running HOL-Nonstandard_Analysis-Examples ...

23:48:47 Warning: missing document directory

23:48:47 Timing HOL-Probability-ex (2 threads, 35.423s elapsed time, 44.916s cpu time, 1.056s GC time, factor 1.27)

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

23:48:47 Finished HOL-Probability-ex (0:00:43 elapsed time, 0:00:53 cpu time, factor 1.21)

23:48:47 Timing Tutorial (2 threads, 29.833s elapsed time, 54.684s cpu time, 6.700s GC time, factor 1.83)

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

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

23:48:47 Finished Tutorial (0:00:35 elapsed time, 0:01:00 cpu time, factor 1.68)

23:48:47 Running HOL-Hoare ...

23:48:47 Running HOL-Cardinals ...

23:48:48 HOL-Nonstandard_Analysis-Examples: theory Multiset

23:48:48 HOL-Hoare: theory Arith2

23:48:48 HOL-Hoare: theory Heap

23:48:48 HOL-Cardinals: theory Order_Union

23:48:48 HOL-Cardinals: theory Cardinal_Notations

23:48:49 HOL-Cardinals: theory Fun_More

23:48:49 HOL-Hoare: theory Hoare_Logic

23:48:49 HOL-Cardinals: theory Order_Relation_More

23:48:49 HOL-Cardinals: theory Wellorder_Extension

23:48:49 HOL-Cardinals: theory Wellfounded_More

23:48:49 HOL-Cardinals: theory Wellorder_Relation

23:48:49 HOL-Hoare: theory Hoare_Logic_Abort

23:48:49 HOL-Cardinals: theory Wellorder_Embedding

23:48:49 HOL-Cardinals: theory Wellorder_Constructions

23:48:50 HOL-Hoare: theory Examples

23:48:50 HOL-Cardinals: theory Cardinal_Order_Relation

23:48:51 HOL-Cardinals: theory Ordinal_Arithmetic

23:48:51 HOL-Hoare: theory HeapSyntax

23:48:51 HOL-Hoare: theory Pointer_Examples

23:48:51 HOL-Hoare: theory SchorrWaite

23:48:51 HOL-Cardinals: theory Cardinal_Arithmetic

23:48:52 HOL-Hoare: theory Pointers0

23:48:52 HOL-Cardinals: theory Cardinals

23:48:52 HOL-Cardinals: theory Bounded_Set

23:48:52 HOL-Hoare: theory ExamplesAbort

23:48:52 HOL-Hoare: theory HeapSyntaxAbort

23:48:53 HOL-Nonstandard_Analysis-Examples: theory Factorial_Ring

23:48:53 HOL-Hoare: theory Pointer_ExamplesAbort

23:48:53 HOL-Hoare: theory SepLogHeap

23:48:53 HOL-Hoare: theory Separation

23:48:53 HOL-Hoare: theory Hoare

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

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

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

23:49:09 Timing HOL-Cardinals (2 threads, 19.638s elapsed time, 36.196s cpu time, 1.356s GC time, factor 1.84)

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

23:49:09 Finished HOL-Cardinals (0:00:21 elapsed time, 0:00:38 cpu time, factor 1.76)

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

23:49:10 HOL-Induct: theory Old_Datatype

23:49:12 HOL-Induct: theory Common_Patterns

23:49:13 HOL-Induct: theory ABexp

23:49:13 HOL-Induct: theory Com

23:49:14 Timing HOL-Hoare (2 threads, 22.715s elapsed time, 41.332s cpu time, 1.132s GC time, factor 1.82)

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

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

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

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

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

23:49:14 Timing HOL-Nonstandard_Analysis-Examples (2 threads, 25.721s elapsed time, 45.644s cpu time, 1.632s GC time, factor 1.77)

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

23:49:14 Finished HOL-Nonstandard_Analysis-Examples (0:00:27 elapsed time, 0:00:47 cpu time, factor 1.71)

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

23:49:15 HOL-Matrix_LP: theory Compute_Oracle

23:49:15 HOL-Matrix_LP: theory Lattice_Algebras

23:49:16 HOL-Matrix_LP: theory ComputeHOL

23:49:16 HOL-Induct: theory Comb

23:49:16 HOL-Induct: theory Nested_Datatype

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

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

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

23:49:17 HOL-Induct: theory Sexp

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

23:49:17 HOL-Induct: theory SList

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

23:49:17 HOL-Induct: theory Ordinals

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

23:49:18 HOL-Induct: theory PropLog

23:49:18 HOL-Induct: theory QuoDataType

23:49:19 HOL-Induct: theory QuoNestedDataType

23:49:20 HOL-Induct: theory Sigma_Algebra

23:49:20 HOL-Induct: theory Term

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

23:49:21 HOL-Induct: theory Tree

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

23:49:21 HOL-Matrix_LP: theory ComputeFloat

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

23:49:22 HOL-Matrix_LP: theory ComputeNumeral

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

23:49:22 HOL-Matrix_LP: theory LP

23:49:22 HOL-Matrix_LP: theory Matrix

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

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

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

23:49:24 HOL-Matrix_LP: theory SparseMatrix

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

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

23:49:26 HOL-Matrix_LP: theory Cplex

23:49:31 Timing HOL-Induct (2 threads, 17.775s elapsed time, 31.976s cpu time, 4.868s GC time, factor 1.80)

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

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

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

23:49:31 Finished HOL-Induct (0:00:21 elapsed time, 0:00:36 cpu time, factor 1.70)

23:49:31 Running HOL-Statespace ...

23:49:32 HOL-Statespace: theory DistinctTreeProver

23:49:34 Timing HOL-SPARK-Examples (2 threads, 16.737s elapsed time, 28.396s cpu time, 0.732s GC time, factor 1.70)

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

23:49:34 Finished HOL-SPARK-Examples (0:00:19 elapsed time, 0:00:31 cpu time, factor 1.59)

23:49:34 Running HOLCF-ex ...

23:49:34 HOL-Statespace: theory StateFun

23:49:34 HOL-Statespace: theory StateSpaceLocale

23:49:34 HOL-Statespace: theory StateSpaceSyntax

23:49:34 HOL-Statespace: theory StateSpaceEx

23:49:36 HOLCF-ex: theory Infinite_Set

23:49:36 HOLCF-ex: theory Concurrency_Monad

23:49:36 Timing HOL-Matrix_LP (2 threads, 18.106s elapsed time, 31.788s cpu time, 1.140s GC time, factor 1.76)

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

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

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

23:49:36 Finished HOL-Matrix_LP (0:00:22 elapsed time, 0:00:36 cpu time, factor 1.66)

23:49:36 Running Isar_Ref ...

23:49:37 HOLCF-ex: theory Countable_Set

23:49:37 HOLCF-ex: theory Countable_Complete_Lattices

23:49:38 HOLCF-ex: theory Dnat

23:49:38 Isar_Ref: theory Base

23:49:38 Isar_Ref: theory Adhoc_Overloading

23:49:38 Isar_Ref: theory Dlist

23:49:38 Isar_Ref: theory First_Order_Logic

23:49:38 Isar_Ref: theory Document_Preparation

23:49:38 HOLCF-ex: theory Domain_Proofs

23:49:39 Isar_Ref: theory FSet

23:49:39 Isar_Ref: theory Framework

23:49:40 HOLCF-ex: theory Fix2

23:49:40 HOLCF-ex: theory Hoare

23:49:40 Isar_Ref: theory Generic

23:49:40 HOLCF-ex: theory Letrec

23:49:40 HOLCF-ex: theory Loop

23:49:40 HOLCF-ex: theory Pattern_Match

23:49:40 Isar_Ref: theory Inner_Syntax

23:49:40 HOLCF-ex: theory Powerdomain_ex

23:49:40 Isar_Ref: theory Old_Datatype

23:49:41 HOLCF-ex: theory Order_Continuity

23:49:42 Isar_Ref: theory Old_Recdef

23:49:42 HOLCF-ex: theory Extended_Nat

23:49:42 Isar_Ref: theory Outer_Syntax

23:49:42 Isar_Ref: theory Preface

23:49:42 Isar_Ref: theory Proof

23:49:43 HOLCF-ex: theory Stream

23:49:43 Isar_Ref: theory HOL_Specific

23:49:43 Isar_Ref: theory Proof_Script

23:49:43 Isar_Ref: theory Quick_Reference

23:49:43 Isar_Ref: theory Spec

23:49:43 Isar_Ref: theory Symbols

23:49:44 Isar_Ref: theory Synopsis

23:49:44 HOLCF-ex: theory Dagstuhl

23:49:44 HOLCF-ex: theory Focus_ex

23:49:50 Timing HOL-Statespace (2 threads, 16.022s elapsed time, 18.428s cpu time, 0.616s GC time, factor 1.15)

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

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

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

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

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

23:49:51 Timing HOLCF-ex (2 threads, 14.455s elapsed time, 26.752s cpu time, 1.048s GC time, factor 1.85)

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

23:49:51 Finished HOLCF-ex (0:00:17 elapsed time, 0:00:29 cpu time, factor 1.71)

23:49:51 Running HOLCF-FOCUS ...

23:49:53 HOLCF-Library: theory Infinite_Set

23:49:53 HOLCF-Library: theory Bool_Discrete

23:49:53 HOLCF-Library: theory Char_Discrete

23:49:53 HOLCF-Library: theory Countable_Set

23:49:53 HOLCF-Library: theory Defl_Bifinite

23:49:53 HOLCF-Library: theory Countable_Complete_Lattices

23:49:54 HOLCF-Library: theory Int_Discrete

23:49:54 HOLCF-FOCUS: theory Infinite_Set

23:49:54 HOLCF-Library: theory List_Cpo

23:49:54 HOLCF-FOCUS: theory Countable_Set

23:49:54 HOLCF-Library: theory Nat_Discrete

23:49:54 HOLCF-Library: theory Sum_Cpo

23:49:55 HOLCF-FOCUS: theory Countable_Complete_Lattices

23:49:55 HOLCF-Library: theory List_Predomain

23:49:56 HOLCF-Library: theory Option_Cpo

23:49:56 HOLCF-Library: theory Order_Continuity

23:49:57 HOLCF-Library: theory Extended_Nat

23:49:58 HOLCF-FOCUS: theory Order_Continuity

23:49:58 HOLCF-Library: theory Stream

23:49:58 HOLCF-FOCUS: theory Extended_Nat

23:49:59 HOLCF-FOCUS: theory Stream

23:49:59 HOLCF-Library: theory HOLCF_Library

23:50:00 Timing Isar_Ref (2 threads, 14.200s elapsed time, 26.272s cpu time, 1.428s GC time, factor 1.85)

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

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

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

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

23:50:01 HOLCF-FOCUS: theory Fstream

23:50:01 HOLCF-FOCUS: theory Fstreams

23:50:01 HOLCF-FOCUS: theory FOCUS

23:50:01 HOLCF-FOCUS: theory Buffer

23:50:01 HOLCF-FOCUS: theory Stream_adm

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

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

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

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

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

23:50:02 HOLCF-FOCUS: theory Buffer_adm

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

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

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

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

23:50:06 Timing HOLCF-Library (2 threads, 13.128s elapsed time, 24.396s cpu time, 0.864s GC time, factor 1.86)

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

23:50:06 Finished HOLCF-Library (0:00:15 elapsed time, 0:00:27 cpu time, factor 1.71)

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

23:50:07 Timing HOLCF-FOCUS (2 threads, 12.698s elapsed time, 24.744s cpu time, 0.812s GC time, factor 1.95)

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

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

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

23:50:09 HOLCF-Tutorial: theory Fixrec_ex

23:50:09 HOLCF-Tutorial: theory Domain_ex

23:50:09 HOL-ZF: theory HOLZF

23:50:09 HOL-ZF: theory Multiset

23:50:09 HOL-ZF: theory Zet

23:50:11 HOLCF-Tutorial: theory New_Domain

23:50:13 HOL-ZF: theory LProd

23:50:14 HOL-ZF: theory MainZF

23:50:14 Timing HOL-TLA-Memory (2 threads, 11.386s elapsed time, 20.064s cpu time, 0.560s GC time, factor 1.76)

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

23:50:14 Finished HOL-TLA-Memory (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.63)

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

23:50:14 HOL-ZF: theory Games

23:50:16 HOL-Hahn_Banach: theory Nat_Bijection

23:50:16 HOL-Hahn_Banach: theory Infinite_Set

23:50:16 HOL-Hahn_Banach: theory Old_Datatype

23:50:16 HOL-Hahn_Banach: theory Set_Algebras

23:50:17 HOL-Hahn_Banach: theory Zorn_Lemma

23:50:18 HOL-Hahn_Banach: theory Countable

23:50:19 HOL-Hahn_Banach: theory Countable_Set

23:50:20 HOL-Hahn_Banach: theory Continuum_Not_Denumerable

23:50:20 HOL-Hahn_Banach: theory Bounds

23:50:20 HOL-Hahn_Banach: theory Vector_Space

23:50:20 HOL-Hahn_Banach: theory Linearform

23:50:20 HOL-Hahn_Banach: theory Subspace

23:50:21 HOL-Hahn_Banach: theory Function_Order

23:50:21 HOL-Hahn_Banach: theory Normed_Space

23:50:21 HOL-Hahn_Banach: theory Function_Norm

23:50:22 HOL-Hahn_Banach: theory Hahn_Banach_Ext_Lemmas

23:50:22 HOL-Hahn_Banach: theory Hahn_Banach_Sup_Lemmas

23:50:22 Timing HOLCF-Tutorial (2 threads, 11.619s elapsed time, 15.312s cpu time, 0.436s GC time, factor 1.32)

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

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

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

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

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

23:50:22 HOL-Hahn_Banach: theory Hahn_Banach_Lemmas

23:50:22 HOL-Hahn_Banach: theory Hahn_Banach

23:50:23 Timing HOL-ZF (2 threads, 11.115s elapsed time, 21.112s cpu time, 0.960s GC time, factor 1.90)

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

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

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

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

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

23:50:24 HOL-Unix: theory Sublist

23:50:24 HOL-Unix: theory Nested_Environment

23:50:25 HOL-Unix: theory Unix

23:50:26 IOA-NTP: theory Lemmas

23:50:26 IOA-NTP: theory Multiset

23:50:26 IOA-NTP: theory Packet

23:50:26 IOA-NTP: theory Action

23:50:27 Timing HOL-Hahn_Banach (2 threads, 9.083s elapsed time, 17.904s cpu time, 0.884s GC time, factor 1.97)

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

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

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

23:50:27 Finished HOL-Hahn_Banach (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.73)

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

23:50:28 IOA-NTP: theory Abschannel

23:50:28 IOA-NTP: theory Receiver

23:50:28 IOA-NTP: theory Sender

23:50:29 IOA-NTP: theory Spec

23:50:29 IOA-NTP: theory Impl

23:50:29 HOL-Mirabelle-ex: theory Ex

23:50:30 IOA-NTP: theory Correctness

23:50:34 Timing IOA-NTP (2 threads, 7.645s elapsed time, 13.052s cpu time, 0.540s GC time, factor 1.71)

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

23:50:34 Finished IOA-NTP (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.50)

23:50:34 Running HOLCF-IMP ...

23:50:34 Timing HOL-Unix (2 threads, 8.665s elapsed time, 16.216s cpu time, 0.788s GC time, factor 1.87)

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

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

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

23:50:34 Finished HOL-Unix (0:00:12 elapsed time, 0:00:20 cpu time, factor 1.68)

23:50:34 Running Codegen ...

23:50:35 Timing HOL-Mirabelle-ex (2 threads, 5.842s elapsed time, 0.020s cpu time, 0.000s GC time, factor 0.00)

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

23:50:35 Finished HOL-Mirabelle-ex (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.22)

23:50:35 Running HOL-NanoJava ...

23:50:36 HOLCF-IMP: theory AExp

23:50:37 Codegen: theory Adaptation

23:50:37 Codegen: theory Evaluation

23:50:37 Codegen: theory Further

23:50:37 HOL-NanoJava: theory Term

23:50:37 Codegen: theory Inductive_Predicate

23:50:38 HOLCF-IMP: theory BExp

23:50:38 Codegen: theory Introduction

23:50:39 HOLCF-IMP: theory Com

23:50:39 HOL-NanoJava: theory Decl

23:50:39 Codegen: theory Refinement

23:50:39 Codegen: theory Foundations

23:50:40 HOL-NanoJava: theory TypeRel

23:50:40 HOL-NanoJava: theory State

23:50:40 HOLCF-IMP: theory Big_Step

23:50:41 HOL-NanoJava: theory AxSem

23:50:41 HOL-NanoJava: theory OpSem

23:50:41 HOLCF-IMP: theory Denotational

23:50:41 HOL-NanoJava: theory Equivalence

23:50:41 HOLCF-IMP: theory HoareEx

23:50:42 HOL-NanoJava: theory Example

23:50:42 Timing HOLCF-IMP (2 threads, 5.801s elapsed time, 10.968s cpu time, 0.380s GC time, factor 1.89)

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

23:50:42 Finished HOLCF-IMP (0:00:08 elapsed time, 0:00:13 cpu time, factor 1.60)

23:50:42 Running IOA-ABP ...

23:50:45 Timing HOL-NanoJava (2 threads, 5.764s elapsed time, 10.036s cpu time, 0.492s GC time, factor 1.74)

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

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

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

23:50:45 Finished HOL-NanoJava (0:00:09 elapsed time, 0:00:13 cpu time, factor 1.53)

23:50:45 Running Prog_Prove ...

23:50:45 IOA-ABP: theory Packet

23:50:45 IOA-ABP: theory Lemmas

23:50:45 IOA-ABP: theory Action

23:50:46 Timing Codegen (2 threads, 5.466s elapsed time, 10.580s cpu time, 0.408s GC time, factor 1.94)

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

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

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

23:50:46 Running HOL-TPTP ...

23:50:47 IOA-ABP: theory Abschannel

23:50:47 IOA-ABP: theory Env

23:50:47 Prog_Prove: theory Bool_nat_list

23:50:47 Prog_Prove: theory Basics

23:50:47 Prog_Prove: theory LaTeXsugar

23:50:47 Prog_Prove: theory Isar

23:50:47 IOA-ABP: theory Receiver

23:50:47 HOL-TPTP: theory MaSh_Export_Base

23:50:47 HOL-TPTP: theory ATP_Theory_Export

23:50:48 Prog_Prove: theory Logic

23:50:48 HOL-TPTP: theory MaSh_Eval

23:50:48 HOL-TPTP: theory THF_Arith

23:50:48 IOA-ABP: theory Sender

23:50:48 HOL-TPTP: theory TPTP_Parser

23:50:48 IOA-ABP: theory Abschannel_finite

23:50:48 IOA-ABP: theory Spec

23:50:48 IOA-ABP: theory Impl

23:50:48 Prog_Prove: theory MyList

23:50:48 IOA-ABP: theory Impl_finite

23:50:49 IOA-ABP: theory Correctness

23:50:49 Prog_Prove: theory Types_and_funs

23:50:50 HOL-TPTP: theory TPTP_Interpret

23:50:50 HOL-TPTP: theory TPTP_Proof_Reconstruction

23:50:51 Timing IOA-ABP (2 threads, 5.317s elapsed time, 9.716s cpu time, 0.180s GC time, factor 1.83)

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

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

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

23:50:51 HOL-TPTP: theory Refute

23:50:52 HOL-TPTP: theory ATP_Problem_Import

23:50:53 Timing HOL-TPTP (2 threads, 4.778s elapsed time, 5.568s cpu time, 0.104s GC time, factor 1.17)

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

23:50:53 Finished HOL-TPTP (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.11)

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

23:50:53 HOL-SPARK-Manual: theory Complex_Types

23:50:53 HOL-SPARK-Manual: theory Greatest_Common_Divisor

23:50:54 HOL-SPARK-Manual: theory Proc1

23:50:54 HOL-SPARK-Manual: theory Proc2

23:50:54 HOL-SPARK-Manual: theory VC_Principles

23:50:54 HOL-IMPP: theory Com

23:50:54 HOL-SPARK-Manual: theory Reference

23:50:55 Timing Prog_Prove (2 threads, 5.159s elapsed time, 9.992s cpu time, 0.580s GC time, factor 1.94)

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

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

23:50:55 Finished Prog_Prove (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.47)

23:50:55 Running Implementation ...

23:50:55 HOL-SPARK-Manual: theory Simple_Greatest_Common_Divisor

23:50:55 HOL-SPARK-Manual: theory Example_Verification

23:50:56 HOL-IMPP: theory Natural

23:50:56 HOL-IMPP: theory Hoare

23:50:57 Implementation: theory Base

23:50:57 Implementation: theory Eq

23:50:57 Implementation: theory Integration

23:50:57 Implementation: theory Isar

23:50:57 Implementation: theory Local_Theory

23:50:57 Implementation: theory ML

23:50:57 Implementation: theory Prelim

23:50:57 HOL-IMPP: theory Misc

23:50:57 HOL-IMPP: theory EvenOdd

23:50:57 Implementation: theory Proof

23:50:58 Implementation: theory Syntax

23:50:58 Implementation: theory Tactic

23:50:59 Timing HOL-IMPP (2 threads, 3.835s elapsed time, 6.520s cpu time, 0.164s GC time, factor 1.70)

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

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

23:50:59 Running Functions ...

23:50:59 Implementation: theory Logic

23:51:00 Functions: theory Functions

23:51:01 Timing HOL-SPARK-Manual (2 threads, 4.682s elapsed time, 8.212s cpu time, 0.176s GC time, factor 1.75)

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

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

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

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

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

23:51:03 HOL-IOA: theory Asig

23:51:03 HOL-IOA: theory IOA

23:51:03 Timing Implementation (2 threads, 3.396s elapsed time, 5.912s cpu time, 0.076s GC time, factor 1.74)

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

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

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

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

23:51:04 HOL-IOA: theory Solve

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

23:51:05 Timing Functions (2 threads, 2.654s elapsed time, 3.720s cpu time, 0.204s GC time, factor 1.40)

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

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

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

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

23:51:06 Timing HOL-IOA (2 threads, 2.459s elapsed time, 3.616s cpu time, 0.132s GC time, factor 1.47)

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

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

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

23:51:07 HOL-Lattice: theory Orders

23:51:08 Timing HOL-TLA-Inc (2 threads, 2.098s elapsed time, 3.648s cpu time, 0.076s GC time, factor 1.74)

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

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

23:51:08 Running Classes ...

23:51:08 HOL-Lattice: theory Bounds

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

23:51:08 HOL-Lattice: theory Lattice

23:51:08 HOL-Lattice: theory CompleteLattice

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

23:51:10 Classes: theory Setup

23:51:10 Classes: theory Classes

23:51:11 Timing HOL-Lattice (2 threads, 1.989s elapsed time, 3.492s cpu time, 0.000s GC time, factor 1.76)

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

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

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

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

23:51:11 Timing HOL-Word-Examples (2 threads, 2.066s elapsed time, 3.384s cpu time, 0.088s GC time, factor 1.64)

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

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

23:51:11 Running Locales ...

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

23:51:12 Locales: theory Examples

23:51:13 Locales: theory Examples1

23:51:13 Locales: theory Examples2

23:51:13 Locales: theory Examples3

23:51:13 IOA-Storage: theory Action

23:51:14 Timing Classes (2 threads, 1.813s elapsed time, 2.076s cpu time, 0.000s GC time, factor 1.14)

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

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

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

23:51:14 Running Eisbach ...

23:51:14 IOA-Storage: theory Impl

23:51:14 IOA-Storage: theory Spec

23:51:14 IOA-Storage: theory Correctness

23:51:15 Timing IOA-Storage (2 threads, 1.591s elapsed time, 2.324s cpu time, 0.000s GC time, factor 1.46)

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

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

23:51:15 Running Main ...

23:51:16 Eisbach: theory Base

23:51:16 Eisbach: theory Manual

23:51:16 Eisbach: theory Preface

23:51:16 Timing Locales (2 threads, 1.615s elapsed time, 2.704s cpu time, 0.000s GC time, factor 1.67)

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

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

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

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

23:51:17 Main: theory Main_Doc

23:51:18 HOL-Mutabelle: theory Refute

23:51:19 HOL-Mutabelle: theory MutabelleExtra

23:51:19 Timing Eisbach (2 threads, 1.259s elapsed time, 1.688s cpu time, 0.000s GC time, factor 1.34)

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

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

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

23:51:19 Timing Main (2 threads, 1.187s elapsed time, 1.244s cpu time, 0.000s GC time, factor 1.05)

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

23:51:19 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main/main.pdf

23:51:19 Finished Main (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.97)

23:51:19 Running Sugar ...

23:51:19 Running HOL-Types_To_Sets ...

23:51:20 Timing HOL-Mutabelle (2 threads, 1.134s elapsed time, 1.220s cpu time, 0.000s GC time, factor 1.08)

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

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

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

23:51:21 Sugar: theory LaTeXsugar

23:51:21 HOL-Types_To_Sets: theory Prerequisites

23:51:21 HOL-Types_To_Sets: theory Types_To_Sets

23:51:21 Sugar: theory OptionalSugar

23:51:21 HOL-Types_To_Sets: theory Finite

23:51:21 HOL-Types_To_Sets: theory T2_Spaces

23:51:21 Sugar: theory Sugar

23:51:22 HOL-Proofs-ex: theory Drinker

23:51:22 HOL-Proofs-ex: theory Hilbert_Classical

23:51:22 HOL-Proofs-ex: theory Proof_Terms

23:51:22 HOL-Proofs-ex: theory XML_Data

23:51:22 Timing HOL-Types_To_Sets (2 threads, 0.980s elapsed time, 1.520s cpu time, 0.000s GC time, factor 1.55)

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

23:51:22 Finished HOL-Types_To_Sets (0:00:02 elapsed time, 0:00:03 cpu time)

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

23:51:23 Timing Sugar (2 threads, 0.897s elapsed time, 1.076s cpu time, 0.000s GC time, factor 1.20)

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

23:51:23 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar/sugar.pdf

23:51:23 Finished Sugar (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.99)

23:51:23 Timing HOL-Proofs-ex (2 threads, 1.008s elapsed time, 1.868s cpu time, 0.000s GC time, factor 1.85)

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

23:51:23 Finished HOL-Proofs-ex (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.23)

23:51:23 Running HOL-Import ...

23:51:23 Running IOA-ex ...

23:51:24 HOL-Nunchaku: theory Nunchaku

23:51:25 HOL-Import: theory Import_Setup

23:51:25 Timing HOL-Nunchaku (2 threads, 0.953s elapsed time, 1.028s cpu time, 0.000s GC time, factor 1.08)

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

23:51:25 Finished HOL-Nunchaku (0:00:02 elapsed time)

23:51:25 Running HOL-TLA-Buffer ...

23:51:25 HOL-Import: theory HOL_Light_Maps

23:51:26 IOA-ex: theory TrivEx2

23:51:26 IOA-ex: theory TrivEx

23:51:26 Warning: missing document directory

23:51:26 Skipping theories "HOL_Light_Import" (undefined HOL_LIGHT_BUNDLE)

23:51:26 Timing HOL-Import (2 threads, 0.975s elapsed time, 1.636s cpu time, 0.000s GC time, factor 1.68)

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

23:51:26 Finished HOL-Import (0:00:02 elapsed time, 0:00:03 cpu time)

23:51:26 Running JEdit ...

23:51:27 HOL-TLA-Buffer: theory Buffer

23:51:27 Timing IOA-ex (2 threads, 0.771s elapsed time, 1.584s cpu time, 0.000s GC time, factor 2.05)

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

23:51:27 Finished IOA-ex (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.21)

23:51:27 Running How_to_Prove_it ...

23:51:27 HOL-TLA-Buffer: theory DBuffer

23:51:28 JEdit: theory Base

23:51:28 JEdit: theory JEdit

23:51:28 Timing HOL-TLA-Buffer (2 threads, 0.674s elapsed time, 1.136s cpu time, 0.000s GC time, factor 1.69)

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

23:51:28 Finished HOL-TLA-Buffer (0:00:02 elapsed time, 0:00:03 cpu time)

23:51:28 Running Typeclass_Hierarchy ...

23:51:29 How_to_Prove_it: theory How_to_Prove_it

23:51:30 Typeclass_Hierarchy: theory Typeclass_Hierarchy

23:51:31 Timing How_to_Prove_it (2 threads, 0.444s elapsed time, 0.572s cpu time, 0.000s GC time, factor 1.29)

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

23:51:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it/how_to_prove_it.pdf

23:51:31 Finished How_to_Prove_it (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.98)

23:51:31 Running HOL-Prolog ...

23:51:33 HOL-Prolog: theory HOHH

23:51:33 HOL-Prolog: theory Func

23:51:33 HOL-Prolog: theory Test

23:51:33 HOL-Prolog: theory Type

23:51:33 Timing Typeclass_Hierarchy (2 threads, 0.332s elapsed time, 0.420s cpu time, 0.000s GC time, factor 1.27)

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

23:51:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy/typeclass_hierarchy.pdf

23:51:33 Finished Typeclass_Hierarchy (0:00:04 elapsed time, 0:00:03 cpu time, factor 0.95)

23:51:33 Timing HOL-Prolog (2 threads, 0.290s elapsed time, 0.464s cpu time, 0.000s GC time, factor 1.60)

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

23:51:33 Finished HOL-Prolog (0:00:02 elapsed time)

23:51:36 Timing JEdit (2 threads, 0.581s elapsed time, 0.624s cpu time, 0.000s GC time, factor 1.07)

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

23:51:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit/jedit.pdf

23:51:36 Finished JEdit (0:00:09 elapsed time, 0:00:09 cpu time, factor 0.96)

23:51:36

23:51:36 === TIMING ===

23:51:36

23:51:36 Group main: 0:26:02 elapsed time, 0:45:27 cpu time, factor 1.75

23:51:36 Group doc: 0:04:12 elapsed time, 0:05:47 cpu time, factor 1.37

23:51:36 Group timing: 1:44:16 elapsed time, 2:53:03 cpu time, factor 1.66

23:51:36 Group ZF: 0:01:40 elapsed time, 0:02:46 cpu time, factor 1.66

23:51:36 Overall: 0:52:55 elapsed time, 4:30:13 cpu time, factor 5.11

23:51:36 Archiving artifacts

23:51:37 Started calculate disk usage of build

23:51:37 Finished Calculation of disk usage of build in 0 seconds

23:51:44 Started calculate disk usage of workspace

23:51:44 Finished Calculation of disk usage of workspace in 0 seconds

23:51:44 No emails were triggered.

23:51:44 Finished: SUCCESS