Skip to content
Success

Console Output

18:49:25 Started by upstream project "isabelle-repo" build number 1491

18:49:25 originally caused by:

18:49:25 Started by an SCM change

18:49:25 [EnvInject] - Loading node environment variables.

18:49:25 Building remotely on workermta3 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-repo-makeall

18:49:25 [isabelle-repo-makeall] $ hg showconfig paths.default

18:49:25 [isabelle-repo-makeall] $ hg pull --rev 7b0b0a02b303649475fb11d066bc675c79c6bb0c

18:49:26 pulling from http://isabelle.in.tum.de/repos/isabelle/

18:49:26 searching for changes

18:49:26 adding changesets

18:49:26 adding manifests

18:49:26 adding file changes

18:49:26 added 2 changesets with 1 changes to 1 files

18:49:26 (run 'hg update' to get a working copy)

18:49:26 [isabelle-repo-makeall] $ hg update --clean --rev 7b0b0a02b303649475fb11d066bc675c79c6bb0c

18:49:26 1 files updated, 0 files merged, 0 files removed, 0 files unresolved

18:49:26 [isabelle-repo-makeall] $ hg log --rev . --template {node}

18:49:26 [isabelle-repo-makeall] $ hg log --rev . --template {rev}

18:49:26 [isabelle-repo-makeall] $ hg id --branch

18:49:26 No emails were triggered.

18:49:26 [isabelle-repo-makeall] $ /bin/sh -xe /tmp/jenkins1820452043574839189.sh

18:49:26 + Admin/jenkins/run_build makeall

18:49:26 + set -e

18:49:26 + PROFILE=makeall

18:49:26 + shift

18:49:26 + bin/isabelle components -a

18:49:27 + bin/isabelle jedit -bf

18:49:27 ### Building Isabelle/Scala ...

18:49:56 ### Building Isabelle/jEdit ...

18:50:14 + bin/isabelle ci_build_makeall

18:50:19

18:50:19 === CONFIGURATION ===

18:50:19

18:50:19 ISABELLE_BUILD_OPTIONS=""

18:50:19

18:50:19 ML_PLATFORM="x86_64-linux"

18:50:19 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7.1-5/x86_64-linux"

18:50:19 ML_SYSTEM="polyml-5.7.1"

18:50:19 ML_OPTIONS="-H 4000 --maxheap 8G"

18:50:19

18:50:19 === BUILD ===

18:50:19

18:50:19 Build started at Wed, 28 Feb 2018 17:50:19 GMT

18:50:19 Isabelle id 7b0b0a02b303

18:50:19

18:50:19 === LOG ===

18:50:19

18:50:19 Session Pure/Pure

18:50:20 Session CTT/CTT

18:50:20 Session Cube/Cube

18:50:20 Session FOL/FOL

18:50:20 Session CCL/CCL

18:50:20 Session FOL/FOL-ex

18:50:20 Session FOLP/FOLP

18:50:20 Session FOLP/FOLP-ex

18:50:20 Session HOL/HOL (main)

18:50:21 Session Doc/Classes (doc)

18:50:21 Session Doc/Functions (doc)

18:50:21 Session HOL/HOL-Eisbach

18:50:21 Session Doc/Eisbach (doc)

18:50:21 Session HOL/HOL-Hoare

18:50:22 Session HOL/HOL-Hoare_Parallel (timing)

18:50:22 Session HOL/HOL-IMPP

18:50:22 Session HOL/HOL-IOA

18:50:22 Session HOL/HOL-Import

18:50:22 Session HOL/HOL-Lattice

18:50:22 Session HOL/HOL-Library (main timing)

18:50:22 Session Doc/Codegen_Basics

18:50:22 Session Doc/Codegen (doc)

18:50:22 Session Doc/Datatypes (doc)

18:50:22 Session Doc/Corec (doc)

18:50:22 Session HOL/HOL-Auth (timing)

18:50:23 Session HOL/HOL-UNITY (timing)

18:50:23 Session HOL/HOL-Bali (timing)

18:50:23 Session HOL/HOL-Cardinals (timing)

18:50:23 Session HOL/HOL-Computational_Algebra (main timing)

18:50:23 Session HOL/HOL-Algebra (main timing)

18:50:23 Session HOL/HOL-Decision_Procs (timing)

18:50:24 Session HOL/HOL-Quotient_Examples (timing)

18:50:24 Session HOL/HOL-Analysis (main timing)

18:50:24 Session HOL/HOL-Analysis-ex

18:50:25 Session HOL/HOL-Probability (main timing)

18:50:25 Session HOL/HOL-Probability-ex (timing)

18:50:25 Session HOL/HOL-Isar_Examples

18:50:25 Session HOL/HOL-Nonstandard_Analysis (timing)

18:50:25 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)

18:50:25 Session HOL/HOL-Number_Theory (main timing)

18:50:25 Session HOL/HOL-Data_Structures (timing)

18:50:26 Session HOL/HOL-ex (timing)

18:50:26 Session HOL/HOL-Codegenerator_Test

18:50:26 Session HOL/HOL-Corec_Examples (timing)

18:50:26 Session HOL/HOL-Datatype_Examples (timing)

18:50:26 Session HOL/HOL-Hahn_Banach

18:50:26 Session HOL/HOL-IMP (timing)

18:50:26 Session HOL/HOL-Imperative_HOL (timing)

18:50:26 Session HOL/HOL-Induct

18:50:26 Session HOL/HOL-Matrix_LP

18:50:27 Session HOL/HOL-Metis_Examples (timing)

18:50:27 Session HOL/HOL-MicroJava (timing)

18:50:27 Session HOL/HOL-Mutabelle

18:50:27 Session HOL/HOL-Nitpick_Examples

18:50:27 Session HOL/HOL-Nominal

18:50:27 Session HOL/HOL-Nominal-Examples (timing)

18:50:27 Session HOL/HOL-Predicate_Compile_Examples (timing)

18:50:27 Session HOL/HOL-Quickcheck_Examples (timing)

18:50:27 Session HOL/HOL-SET_Protocol (timing)

18:50:27 Session HOL/HOL-TPTP

18:50:28 Session HOL/HOL-Unix

18:50:28 Session HOL/HOL-ZF

18:50:28 Session Doc/Isar_Ref (doc)

18:50:28 Session Doc/Typeclass_Hierarchy_Basics

18:50:28 Session Doc/Typeclass_Hierarchy (doc)

18:50:28 Session HOL/HOL-Mirabelle

18:50:28 Session HOL/HOL-Mirabelle-ex

18:50:28 Session HOL/HOL-NanoJava

18:50:28 Session HOL/HOL-Prolog

18:50:28 Session HOL/HOL-Statespace

18:50:28 Session HOL/HOL-TLA

18:50:28 Session HOL/HOL-TLA-Buffer

18:50:28 Session HOL/HOL-TLA-Inc

18:50:28 Session HOL/HOL-TLA-Memory

18:50:28 Session HOL/HOL-Types_To_Sets

18:50:28 Session HOL/HOL-Word (main timing)

18:50:28 Session HOL/HOL-SPARK (main)

18:50:29 Session HOL/HOL-SPARK-Examples

18:50:29 Session HOL/HOL-SPARK-Manual

18:50:29 Session HOL/HOL-Word-SMT_Examples (timing)

18:50:29 Session HOL/HOLCF (main timing)

18:50:29 Session HOL/HOLCF-IMP

18:50:29 Session HOL/HOLCF-Library

18:50:29 Session HOL/HOLCF-FOCUS

18:50:29 Session HOL/HOLCF-ex

18:50:29 Session HOL/HOLCF-Tutorial

18:50:29 Session HOL/IOA (timing)

18:50:30 Session HOL/IOA-ABP

18:50:30 Session HOL/IOA-NTP

18:50:30 Session HOL/IOA-Storage

18:50:30 Session HOL/IOA-ex

18:50:30 Session Doc/How_to_Prove_it

18:50:30 Session Doc/Implementation (doc)

18:50:30 Session Doc/JEdit (doc)

18:50:30 Session Doc/Locales (doc)

18:50:30 Session Doc/Main (doc)

18:50:30 Session Doc/Prog_Prove (doc)

18:50:30 Session Doc/Sugar (doc)

18:50:30 Session Doc/Tutorial (doc)

18:50:30 Session HOL/HOL-Proofs (timing)

18:50:31 Session HOL/HOL-Proofs-Extraction (timing)

18:50:31 Session HOL/HOL-Proofs-Lambda (timing)

18:50:31 Session HOL/HOL-Proofs-ex

18:50:31 Session Doc/Intro (doc)

18:50:31 Session LCF/LCF

18:50:31 Session Doc/Logics (doc)

18:50:31 Session Doc/Nitpick (doc)

18:50:31 Session Unsorted/SML

18:50:31 Session Sequents/Sequents

18:50:31 Session Doc/Sledgehammer (doc)

18:50:31 Session Unsorted/Spec_Check

18:50:32 Session Doc/System (doc)

18:50:32 Session ZF/ZF (main timing)

18:50:32 Session Doc/Logics_ZF (doc)

18:50:32 Session ZF/ZF-AC

18:50:32 Session ZF/ZF-Coind

18:50:32 Session ZF/ZF-Constructible

18:50:32 Session ZF/ZF-IMP

18:50:32 Session ZF/ZF-Induct

18:50:32 Session ZF/ZF-UNITY (timing)

18:50:32 Session ZF/ZF-Resid

18:50:32 Session ZF/ZF-ex

18:50:34 Cleaning Pure ...

18:50:34 Cleaning SML ...

18:50:34 Cleaning Sequents ...

18:50:34 Cleaning Sledgehammer ...

18:50:34 Cleaning Spec_Check ...

18:50:34 Cleaning System ...

18:50:34 Cleaning ZF ...

18:50:34 Cleaning ZF-AC ...

18:50:34 Cleaning ZF-Coind ...

18:50:34 Cleaning ZF-Constructible ...

18:50:34 Cleaning ZF-IMP ...

18:50:34 Cleaning ZF-Induct ...

18:50:34 Cleaning ZF-UNITY ...

18:50:34 Cleaning ZF-Resid ...

18:50:34 Cleaning ZF-ex ...

18:50:34 Cleaning Nitpick ...

18:50:34 Cleaning Logics_ZF ...

18:50:34 Cleaning Logics ...

18:50:34 Cleaning LCF ...

18:50:34 Cleaning Intro ...

18:50:34 Cleaning HOL-Proofs ...

18:50:34 Cleaning HOL-Proofs-Extraction ...

18:50:34 Cleaning HOL-Proofs-Lambda ...

18:50:34 Cleaning HOL-Proofs-ex ...

18:50:34 Cleaning HOL ...

18:50:34 Cleaning HOL-Analysis ...

18:50:34 Cleaning HOL-Analysis-ex ...

18:50:34 Cleaning HOL-Probability ...

18:50:34 Cleaning HOL-Probability-ex ...

18:50:34 Cleaning HOL-Data_Structures ...

18:50:34 Cleaning HOL-Eisbach ...

18:50:34 Cleaning HOL-Hoare ...

18:50:34 Cleaning HOL-Hoare_Parallel ...

18:50:34 Cleaning HOL-IMPP ...

18:50:34 Cleaning HOL-IOA ...

18:50:34 Cleaning HOL-Import ...

18:50:34 Cleaning HOL-Lattice ...

18:50:34 Cleaning HOL-Library ...

18:50:34 Cleaning HOL-Auth ...

18:50:34 Cleaning HOL-UNITY ...

18:50:34 Cleaning HOL-Bali ...

18:50:34 Cleaning HOL-Cardinals ...

18:50:34 Cleaning HOL-Computational_Algebra ...

18:50:34 Cleaning HOL-Algebra ...

18:50:34 Cleaning HOL-Decision_Procs ...

18:50:34 Cleaning HOL-Quotient_Examples ...

18:50:34 Cleaning HOL-Isar_Examples ...

18:50:34 Cleaning HOL-Nonstandard_Analysis ...

18:50:34 Cleaning HOL-Nonstandard_Analysis-Examples ...

18:50:34 Cleaning HOL-Number_Theory ...

18:50:34 Cleaning HOL-Codegenerator_Test ...

18:50:34 Cleaning HOL-ex ...

18:50:34 Cleaning HOL-Corec_Examples ...

18:50:34 Cleaning HOL-Datatype_Examples ...

18:50:34 Cleaning HOL-Hahn_Banach ...

18:50:34 Cleaning HOL-IMP ...

18:50:34 Cleaning HOL-Imperative_HOL ...

18:50:34 Cleaning HOL-Induct ...

18:50:34 Cleaning HOL-Matrix_LP ...

18:50:34 Cleaning HOL-Metis_Examples ...

18:50:34 Cleaning HOL-MicroJava ...

18:50:34 Cleaning HOL-Mutabelle ...

18:50:34 Cleaning HOL-Nitpick_Examples ...

18:50:34 Cleaning HOL-Nominal ...

18:50:34 Cleaning HOL-Nominal-Examples ...

18:50:34 Cleaning HOL-Predicate_Compile_Examples ...

18:50:34 Cleaning HOL-Quickcheck_Examples ...

18:50:34 Cleaning HOL-SET_Protocol ...

18:50:34 Cleaning HOL-TPTP ...

18:50:34 Cleaning HOL-Unix ...

18:50:34 Cleaning HOL-ZF ...

18:50:34 Cleaning Isar_Ref ...

18:50:34 Cleaning Typeclass_Hierarchy_Basics ...

18:50:34 Cleaning Typeclass_Hierarchy ...

18:50:34 Cleaning HOL-Mirabelle ...

18:50:34 Cleaning HOL-Mirabelle-ex ...

18:50:34 Cleaning HOL-NanoJava ...

18:50:34 Cleaning HOL-Prolog ...

18:50:34 Cleaning HOL-Statespace ...

18:50:34 Cleaning HOL-TLA ...

18:50:34 Cleaning HOL-TLA-Buffer ...

18:50:34 Cleaning HOL-TLA-Inc ...

18:50:34 Cleaning HOL-TLA-Memory ...

18:50:34 Cleaning HOL-Types_To_Sets ...

18:50:34 Cleaning HOL-Word ...

18:50:34 Cleaning HOL-SPARK ...

18:50:34 Cleaning HOL-SPARK-Examples ...

18:50:34 Cleaning HOL-SPARK-Manual ...

18:50:34 Cleaning HOL-Word-SMT_Examples ...

18:50:34 Cleaning HOLCF ...

18:50:34 Cleaning HOLCF-IMP ...

18:50:34 Cleaning HOLCF-Library ...

18:50:34 Cleaning HOLCF-FOCUS ...

18:50:34 Cleaning HOLCF-ex ...

18:50:34 Cleaning HOLCF-Tutorial ...

18:50:34 Cleaning IOA ...

18:50:34 Cleaning IOA-ABP ...

18:50:34 Cleaning IOA-NTP ...

18:50:34 Cleaning IOA-Storage ...

18:50:34 Cleaning IOA-ex ...

18:50:34 Cleaning How_to_Prove_it ...

18:50:34 Cleaning Implementation ...

18:50:34 Cleaning JEdit ...

18:50:34 Cleaning Locales ...

18:50:34 Cleaning Main ...

18:50:34 Cleaning Prog_Prove ...

18:50:34 Cleaning Sugar ...

18:50:34 Cleaning Tutorial ...

18:50:34 Cleaning Functions ...

18:50:34 Cleaning FOLP ...

18:50:34 Cleaning FOLP-ex ...

18:50:34 Cleaning FOL ...

18:50:34 Cleaning FOL-ex ...

18:50:34 Cleaning Eisbach ...

18:50:34 Cleaning Datatypes ...

18:50:34 Cleaning Cube ...

18:50:34 Cleaning Corec ...

18:50:34 Cleaning Codegen_Basics ...

18:50:34 Cleaning Codegen ...

18:50:34 Cleaning Classes ...

18:50:34 Cleaning CTT ...

18:50:34 Cleaning CCL ...

18:50:34 Building Pure ...

18:50:50 Pure: theory Pure

18:50:51 Pure: theory ML_Bootstrap

18:50:51 Pure: theory Pure.Sessions

18:50:54 Timing Pure (1 threads, 0.691s elapsed time, 0.692s cpu time, 0.000s GC time, factor 1.00)

18:50:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Pure/Pure

18:50:54 Finished Pure (0:00:18 elapsed time, 0:00:17 cpu time, factor 0.97)

18:50:54 Building HOL ...

18:50:54 Building ZF ...

18:50:54 Building HOL-Proofs ...

18:50:55 ZF: theory IFOL

18:50:56 ZF: theory FOL

18:50:57 HOL-Proofs: theory HOL.Code_Generator

18:50:57 HOL: theory HOL.Code_Generator

18:50:58 ZF: theory ZF.ZF_Base

18:50:58 ZF: theory ZF.upair

18:50:59 ZF: theory ZF.pair

18:50:59 ZF: theory ZF.Bool

18:50:59 ZF: theory ZF.equalities

18:51:00 ZF: theory ZF.Sum

18:51:00 ZF: theory ZF.Fixedpt

18:51:00 HOL-Proofs: theory HOL.HOL

18:51:00 ZF: theory ZF.func

18:51:00 HOL: theory HOL.HOL

18:51:01 ZF: theory ZF.Perm

18:51:01 ZF: theory ZF.QPair

18:51:01 ZF: theory ZF.Trancl

18:51:01 ZF: theory ZF.EquivClass

18:51:01 ZF: theory ZF.WF

18:51:01 ZF: theory ZF.Order

18:51:01 ZF: theory ZF.Ordinal

18:51:01 ZF: theory ZF.OrdQuant

18:51:01 ZF: theory ZF.OrderArith

18:51:02 ZF: theory ZF.Nat_ZF

18:51:02 ZF: theory ZF.Epsilon

18:51:02 ZF: theory ZF.OrderType

18:51:02 ZF: theory ZF.Inductive_ZF

18:51:03 ZF: theory ZF.Finite

18:51:03 ZF: theory ZF.Cardinal

18:51:04 ZF: theory ZF.Univ

18:51:04 ZF: theory ZF.Arith

18:51:04 ZF: theory ZF.QUniv

18:51:04 ZF: theory ZF.Datatype_ZF

18:51:04 ZF: theory ZF.ArithSimp

18:51:05 ZF: theory ZF.Int_ZF

18:51:05 ZF: theory ZF.CardinalArith

18:51:05 HOL-Proofs: theory HOL.Argo

18:51:05 HOL-Proofs: theory HOL.Ctr_Sugar

18:51:05 ZF: theory ZF.List_ZF

18:51:06 HOL: theory HOL.Argo

18:51:06 HOL: theory HOL.Ctr_Sugar

18:51:06 ZF: theory ZF.Bin

18:51:07 HOL-Proofs: theory HOL.Orderings

18:51:07 ZF: theory ZF.IntDiv_ZF

18:51:07 HOL: theory HOL.Orderings

18:51:08 HOL-Proofs: theory HOL.SAT

18:51:08 ZF: theory ZF

18:51:08 HOL: theory HOL.SAT

18:51:08 ZF: theory ZF.AC

18:51:08 ZF: theory ZF.Zorn

18:51:09 ZF: theory ZF.Cardinal_AC

18:51:09 ZF: theory ZF.InfDatatype

18:51:09 ZF: theory ZFC

18:51:10 HOL: theory HOL.Groups

18:51:10 HOL-Proofs: theory HOL.Groups

18:51:13 HOL: theory HOL.Lattices

18:51:14 HOL-Proofs: theory HOL.Lattices

18:51:15 HOL: theory HOL.Set

18:51:17 HOL: theory HOL.Fun

18:51:17 HOL: theory HOL.Typedef

18:51:17 HOL: theory HOL.Rings

18:51:18 HOL: theory HOL.Complete_Lattices

18:51:19 HOL-Proofs: theory HOL.Set

18:51:20 HOL: theory HOL.Inductive

18:51:23 HOL: theory HOL.Product_Type

18:51:25 HOL-Proofs: theory HOL.Fun

18:51:25 HOL: theory HOL.Complete_Partial_Order

18:51:26 HOL: theory HOL.Sum_Type

18:51:27 HOL-Proofs: theory HOL.Typedef

18:51:27 HOL-Proofs: theory HOL.Rings

18:51:28 HOL-Proofs: theory HOL.Complete_Lattices

18:51:29 HOL: theory HOL.Nat

18:51:31 HOL: theory HOL.Fields

18:51:31 HOL: theory HOL.Meson

18:51:32 HOL: theory HOL.ATP

18:51:33 HOL-Proofs: theory HOL.Inductive

18:51:36 HOL: theory HOL.Metis

18:51:36 Timing ZF (2 threads, 27.287s elapsed time, 45.180s cpu time, 2.916s GC time, factor 1.66)

18:51:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF

18:51:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/document.pdf

18:51:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/outline.pdf

18:51:36 Finished ZF (0:00:41 elapsed time, 0:01:08 cpu time, factor 1.67)

18:51:36 Building ZF-Induct ...

18:51:36 HOL-Proofs: theory HOL.Product_Type

18:51:36 ZF-Induct: theory ZF-Induct.Acc

18:51:36 ZF-Induct: theory ZF-Induct.Binary_Trees

18:51:36 ZF-Induct: theory ZF-Induct.Comb

18:51:36 ZF-Induct: theory ZF-Induct.Datatypes

18:51:37 ZF-Induct: theory ZF-Induct.FoldSet

18:51:37 ZF-Induct: theory ZF-Induct.ListN

18:51:37 HOL: theory HOL.Finite_Set

18:51:37 ZF-Induct: theory ZF-Induct.Mutil

18:51:37 ZF-Induct: theory ZF-Induct.Ntree

18:51:37 ZF-Induct: theory ZF-Induct.Multiset

18:51:37 ZF-Induct: theory ZF-Induct.Primrec

18:51:37 ZF-Induct: theory ZF-Induct.PropLog

18:51:38 ZF-Induct: theory ZF-Induct.Rmap

18:51:38 ZF-Induct: theory ZF-Induct.Term

18:51:38 ZF-Induct: theory ZF-Induct.Tree_Forest

18:51:38 ZF-Induct: theory ZF-Induct.Brouwer

18:51:39 HOL: theory HOL.Relation

18:51:39 HOL-Proofs: theory HOL.Complete_Partial_Order

18:51:40 HOL: theory HOL.Transitive_Closure

18:51:40 HOL-Proofs: theory HOL.Sum_Type

18:51:42 HOL: theory HOL.Wellfounded

18:51:42 HOL: theory HOL.Fun_Def_Base

18:51:43 HOL: theory HOL.Hilbert_Choice

18:51:43 HOL: theory HOL.Wfrec

18:51:43 HOL: theory HOL.Order_Relation

18:51:43 HOL-Proofs: theory HOL.Nat

18:51:43 HOL: theory HOL.BNF_Wellorder_Relation

18:51:43 HOL: theory HOL.Zorn

18:51:43 HOL: theory HOL.BNF_Wellorder_Embedding

18:51:44 HOL: theory HOL.BNF_Wellorder_Constructions

18:51:45 HOL: theory HOL.BNF_Cardinal_Order_Relation

18:51:46 HOL: theory HOL.BNF_Cardinal_Arithmetic

18:51:46 HOL: theory HOL.BNF_Def

18:51:48 HOL-Proofs: theory HOL.Fields

18:51:48 HOL-Proofs: theory HOL.Meson

18:51:49 HOL-Proofs: theory HOL.ATP

18:51:49 HOL: theory HOL.BNF_Composition

18:51:49 HOL: theory HOL.Basic_BNFs

18:51:51 HOL: theory HOL.BNF_Fixpoint_Base

18:51:52 Timing ZF-Induct (2 threads, 7.577s elapsed time, 12.256s cpu time, 0.516s GC time, factor 1.62)

18:51:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct

18:51:52 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/document.pdf

18:51:52 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/outline.pdf

18:51:52 Finished ZF-Induct (0:00:15 elapsed time, 0:00:24 cpu time, factor 1.59)

18:51:52 Building FOL ...

18:51:52 FOL: theory IFOL

18:51:52 HOL-Proofs: theory HOL.Metis

18:51:53 FOL: theory FOL

18:51:55 HOL: theory HOL.BNF_Least_Fixpoint

18:51:57 HOL-Proofs: theory HOL.Finite_Set

18:51:59 HOL: theory HOL.Basic_BNF_LFPs

18:51:59 HOL: theory HOL.Transfer

18:52:00 HOL: theory HOL.Num

18:52:01 Timing FOL (2 threads, 3.726s elapsed time, 4.096s cpu time, 0.188s GC time, factor 1.10)

18:52:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL

18:52:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/document.pdf

18:52:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/outline.pdf

18:52:01 Finished FOL (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.38)

18:52:01 Building FOLP ...

18:52:01 FOLP: theory IFOLP

18:52:02 FOLP: theory FOLP

18:52:04 HOL: theory HOL.Power

18:52:04 Timing FOLP (2 threads, 1.293s elapsed time, 1.308s cpu time, 0.000s GC time, factor 1.01)

18:52:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP

18:52:04 Finished FOLP (0:00:02 elapsed time)

18:52:04 Running ZF-Constructible ...

18:52:04 ZF-Constructible: theory ZF-Constructible.Formula

18:52:04 ZF-Constructible: theory ZF-Constructible.MetaExists

18:52:04 ZF-Constructible: theory ZF-Constructible.Normal

18:52:05 ZF-Constructible: theory ZF-Constructible.Reflection

18:52:05 ZF-Constructible: theory ZF-Constructible.Relative

18:52:05 HOL-Proofs: theory HOL.Relation

18:52:06 HOL: theory HOL.Groups_Big

18:52:07 ZF-Constructible: theory ZF-Constructible.L_axioms

18:52:07 ZF-Constructible: theory ZF-Constructible.Wellorderings

18:52:08 ZF-Constructible: theory ZF-Constructible.WFrec

18:52:08 ZF-Constructible: theory ZF-Constructible.WF_absolute

18:52:09 HOL: theory HOL.Equiv_Relations

18:52:09 HOL-Proofs: theory HOL.Transitive_Closure

18:52:09 HOL: theory HOL.Lifting

18:52:09 ZF-Constructible: theory ZF-Constructible.Datatype_absolute

18:52:09 ZF-Constructible: theory ZF-Constructible.Rank

18:52:11 ZF-Constructible: theory ZF-Constructible.Separation

18:52:11 ZF-Constructible: theory ZF-Constructible.Internalize

18:52:11 ZF-Constructible: theory ZF-Constructible.AC_in_L

18:52:11 HOL: theory HOL.Lifting_Set

18:52:11 HOL: theory HOL.Option

18:52:11 HOL: theory HOL.Quotient

18:52:12 HOL: theory HOL.Extraction

18:52:13 ZF-Constructible: theory ZF-Constructible.Rec_Separation

18:52:13 ZF-Constructible: theory ZF-Constructible.Rank_Separation

18:52:13 ZF-Constructible: theory ZF-Constructible.Satisfies_absolute

18:52:14 HOL: theory HOL.Lattices_Big

18:52:14 HOL-Proofs: theory HOL.Wellfounded

18:52:15 ZF-Constructible: theory ZF-Constructible.DPow_absolute

18:52:15 HOL: theory HOL.Partial_Function

18:52:16 HOL: theory HOL.Fun_Def

18:52:17 HOL-Proofs: theory HOL.Fun_Def_Base

18:52:18 HOL-Proofs: theory HOL.Hilbert_Choice

18:52:18 HOL: theory HOL.Int

18:52:21 HOL-Proofs: theory HOL.Wfrec

18:52:21 HOL: theory HOL.Euclidean_Division

18:52:21 HOL-Proofs: theory HOL.Order_Relation

18:52:22 HOL-Proofs: theory HOL.BNF_Wellorder_Relation

18:52:23 HOL-Proofs: theory HOL.Zorn

18:52:24 HOL-Proofs: theory HOL.BNF_Wellorder_Embedding

18:52:26 HOL: theory HOL.Parity

18:52:26 HOL-Proofs: theory HOL.BNF_Wellorder_Constructions

18:52:29 HOL: theory HOL.Divides

18:52:31 Timing ZF-Constructible (2 threads, 19.514s elapsed time, 37.100s cpu time, 7.448s GC time, factor 1.90)

18:52:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible

18:52:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/document.pdf

18:52:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/outline.pdf

18:52:31 Finished ZF-Constructible (0:00:26 elapsed time, 0:00:49 cpu time, factor 1.86)

18:52:31 Running ZF-UNITY ...

18:52:31 ZF-UNITY: theory ZF-UNITY.GenPrefix

18:52:31 ZF-UNITY: theory ZF-UNITY.MultisetSum

18:52:32 ZF-UNITY: theory ZF-UNITY.State

18:52:32 ZF-UNITY: theory ZF-UNITY.UNITY

18:52:32 HOL: theory HOL.Code_Numeral

18:52:32 HOL: theory HOL.Numeral_Simprocs

18:52:32 ZF-UNITY: theory ZF-UNITY.Monotonicity

18:52:32 HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation

18:52:32 ZF-UNITY: theory ZF-UNITY.Constrains

18:52:32 ZF-UNITY: theory ZF-UNITY.FP

18:52:32 ZF-UNITY: theory ZF-UNITY.WFair

18:52:33 ZF-UNITY: theory ZF-UNITY.Increasing

18:52:33 HOL: theory HOL.SMT

18:52:33 ZF-UNITY: theory ZF-UNITY.SubstAx

18:52:33 HOL: theory HOL.Semiring_Normalization

18:52:33 ZF-UNITY: theory ZF-UNITY.Follows

18:52:33 ZF-UNITY: theory ZF-UNITY.Mutex

18:52:34 ZF-UNITY: theory ZF-UNITY.Union

18:52:34 ZF-UNITY: theory ZF-UNITY.Comp

18:52:35 ZF-UNITY: theory ZF-UNITY.Guar

18:52:35 ZF-UNITY: theory ZF-UNITY.AllocBase

18:52:35 HOL: theory HOL.Set_Interval

18:52:36 ZF-UNITY: theory ZF-UNITY.ClientImpl

18:52:36 ZF-UNITY: theory ZF-UNITY.Distributor

18:52:36 ZF-UNITY: theory ZF-UNITY.AllocImpl

18:52:36 HOL: theory HOL.Groebner_Basis

18:52:36 ZF-UNITY: theory ZF-UNITY.Merge

18:52:38 HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic

18:52:40 HOL-Proofs: theory HOL.BNF_Def

18:52:40 HOL: theory HOL.Conditionally_Complete_Lattices

18:52:41 HOL: theory HOL.Filter

18:52:42 HOL: theory HOL.Presburger

18:52:45 HOL-Proofs: theory HOL.BNF_Composition

18:52:45 HOL: theory HOL.Sledgehammer

18:52:45 HOL-Proofs: theory HOL.Basic_BNFs

18:52:47 HOL-Proofs: theory HOL.BNF_Fixpoint_Base

18:52:48 HOL: theory HOL.List

18:52:51 Timing ZF-UNITY (2 threads, 18.814s elapsed time, 33.956s cpu time, 1.480s GC time, factor 1.80)

18:52:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-UNITY

18:52:51 Finished ZF-UNITY (0:00:19 elapsed time, 0:00:34 cpu time, factor 1.74)

18:52:51 Running ZF-ex ...

18:52:52 ZF-ex: theory ZF-ex.BinEx

18:52:52 ZF-ex: theory ZF-ex.CoUnit

18:52:52 ZF-ex: theory ZF-ex.Commutation

18:52:52 ZF-ex: theory ZF-ex.Group

18:52:52 ZF-ex: theory ZF-ex.LList

18:52:52 ZF-ex: theory ZF-ex.Limit

18:52:52 HOL-Proofs: theory HOL.BNF_Least_Fixpoint

18:52:53 ZF-ex: theory ZF-ex.Ring

18:52:53 ZF-ex: theory ZF-ex.NatSum

18:52:53 ZF-ex: theory ZF-ex.Primes

18:52:54 ZF-ex: theory ZF-ex.Ramsey

18:52:54 ZF-ex: theory ZF-ex.misc

18:52:57 HOL-Proofs: theory HOL.Basic_BNF_LFPs

18:52:57 HOL-Proofs: theory HOL.Transfer

18:52:58 HOL: theory HOL.Groups_List

18:52:59 HOL: theory HOL.Map

18:52:59 HOL: theory HOL.Factorial

18:52:59 HOL: theory HOL.GCD

18:52:59 HOL: theory HOL.Binomial

18:52:59 HOL-Proofs: theory HOL.Num

18:53:00 HOL: theory HOL.Enum

18:53:03 HOL: theory HOL.String

18:53:03 HOL: theory HOL.BNF_Greatest_Fixpoint

18:53:04 HOL-Proofs: theory HOL.Power

18:53:05 Timing ZF-ex (2 threads, 12.077s elapsed time, 17.796s cpu time, 0.636s GC time, factor 1.47)

18:53:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-ex

18:53:05 Finished ZF-ex (0:00:13 elapsed time, 0:00:18 cpu time, factor 1.40)

18:53:05 Running CCL ...

18:53:05 CCL: theory IFOL

18:53:05 HOL: theory HOL.Predicate

18:53:06 CCL: theory FOL

18:53:07 HOL: theory HOL.Lazy_Sequence

18:53:08 HOL: theory HOL.Limited_Sequence

18:53:08 HOL: theory HOL.Typerep

18:53:08 HOL-Proofs: theory HOL.Groups_Big

18:53:08 CCL: theory CCL.Set

18:53:09 CCL: theory CCL.Lfp

18:53:09 CCL: theory CCL.Gfp

18:53:09 CCL: theory CCL.CCL

18:53:09 CCL: theory CCL.Term

18:53:09 CCL: theory CCL.Trancl

18:53:09 HOL: theory HOL.Code_Evaluation

18:53:09 CCL: theory CCL.Type

18:53:10 CCL: theory CCL.Fix

18:53:10 CCL: theory CCL.Hered

18:53:10 CCL: theory CCL.Wfd

18:53:11 CCL: theory CCL.Nat

18:53:11 CCL: theory CCL.List

18:53:11 HOL: theory HOL.Random

18:53:11 CCL: theory CCL.Flag

18:53:11 CCL: theory CCL.Stream

18:53:12 HOL: theory HOL.Quickcheck_Random

18:53:12 Timing CCL (2 threads, 6.373s elapsed time, 9.104s cpu time, 0.724s GC time, factor 1.43)

18:53:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CCL/CCL

18:53:12 Finished CCL (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.31)

18:53:12 Running ZF-AC ...

18:53:13 ZF-AC: theory ZF-AC.AC_Equiv

18:53:13 ZF-AC: theory ZF-AC.AC18_AC19

18:53:13 ZF-AC: theory ZF-AC.AC7_AC9

18:53:13 ZF-AC: theory ZF-AC.Cardinal_aux

18:53:13 ZF-AC: theory ZF-AC.Hartog

18:53:13 ZF-AC: theory ZF-AC.HH

18:53:13 ZF-AC: theory ZF-AC.WO6_WO1

18:53:13 ZF-AC: theory ZF-AC.AC16_lemmas

18:53:14 ZF-AC: theory ZF-AC.AC16_WO4

18:53:14 ZF-AC: theory ZF-AC.DC

18:53:14 ZF-AC: theory ZF-AC.AC15_WO6

18:53:14 ZF-AC: theory ZF-AC.AC17_AC1

18:53:14 ZF-AC: theory ZF-AC.WO1_AC

18:53:14 ZF-AC: theory ZF-AC.WO1_WO7

18:53:14 ZF-AC: theory ZF-AC.WO2_AC16

18:53:15 HOL: theory HOL.Quickcheck_Exhaustive

18:53:15 HOL: theory HOL.Quickcheck_Narrowing

18:53:19 HOL: theory HOL.Random_Pred

18:53:19 HOL: theory HOL.Record

18:53:19 HOL: theory HOL.Random_Sequence

18:53:20 HOL: theory HOL.Predicate_Compile

18:53:20 HOL-Proofs: theory HOL.Equiv_Relations

18:53:21 HOL: theory HOL.Nitpick

18:53:23 HOL-Proofs: theory HOL.Lifting

18:53:24 Timing ZF-AC (2 threads, 6.620s elapsed time, 10.468s cpu time, 0.572s GC time, factor 1.58)

18:53:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC

18:53:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/document.pdf

18:53:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/outline.pdf

18:53:24 Finished ZF-AC (0:00:10 elapsed time, 0:00:17 cpu time, factor 1.63)

18:53:24 Running FOL-ex ...

18:53:24 FOL-ex: theory FOL-ex.If

18:53:24 FOL-ex: theory FOL-ex.Classical

18:53:24 FOL-ex: theory FOL-ex.Intro

18:53:24 FOL-ex: theory FOL-ex.Miniscope

18:53:24 FOL-ex: theory FOL-ex.Nat

18:53:24 FOL-ex: theory FOL-ex.Nat_Class

18:53:24 FOL-ex: theory FOL-ex.Natural_Numbers

18:53:24 FOL-ex: theory FOL-ex.Prolog

18:53:24 FOL-ex: theory FOL-ex.Propositional_Cla

18:53:24 FOL-ex: theory FOL-ex.Quantifiers_Cla

18:53:24 FOL-ex: theory FOL-ex.Foundation

18:53:24 FOL-ex: theory FOL-ex.Intuitionistic

18:53:24 FOL-ex: theory FOL-ex.Propositional_Int

18:53:24 FOL-ex: theory FOL-ex.Quantifiers_Int

18:53:26 HOL-Proofs: theory HOL.Lifting_Set

18:53:27 HOL-Proofs: theory HOL.Option

18:53:27 FOL-ex: theory FOL-ex.Locale_Test1

18:53:28 HOL-Proofs: theory HOL.Quotient

18:53:28 HOL-Proofs: theory HOL.Extraction

18:53:28 HOL: theory HOL.Nunchaku

18:53:29 HOL: theory Main

18:53:30 FOL-ex: theory FOL-ex.Locale_Test2

18:53:30 FOL-ex: theory FOL-ex.Locale_Test3

18:53:30 FOL-ex: theory FOL-ex.Locale_Test

18:53:31 HOL-Proofs: theory HOL.Lattices_Big

18:53:31 HOL: theory HOL.Archimedean_Field

18:53:31 HOL: theory HOL.Topological_Spaces

18:53:32 HOL-Proofs: theory HOL.Partial_Function

18:53:34 HOL-Proofs: theory HOL.Fun_Def

18:53:35 Timing FOL-ex (2 threads, 6.089s elapsed time, 8.680s cpu time, 0.224s GC time, factor 1.43)

18:53:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex

18:53:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/document.pdf

18:53:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/outline.pdf

18:53:35 Finished FOL-ex (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.50)

18:53:35 Running FOLP-ex ...

18:53:35 FOLP-ex: theory FOLP-ex.Classical

18:53:35 FOLP-ex: theory FOLP-ex.If

18:53:35 FOLP-ex: theory FOLP-ex.Intro

18:53:35 FOLP-ex: theory FOLP-ex.Nat

18:53:35 FOLP-ex: theory FOLP-ex.Propositional_Cla

18:53:35 HOL: theory HOL.Rat

18:53:36 FOLP-ex: theory FOLP-ex.Quantifiers_Cla

18:53:36 FOLP-ex: theory FOLP-ex.Foundation

18:53:36 FOLP-ex: theory FOLP-ex.Intuitionistic

18:53:36 HOL-Proofs: theory HOL.Int

18:53:37 FOLP-ex: theory FOLP-ex.Propositional_Int

18:53:37 FOLP-ex: theory FOLP-ex.Quantifiers_Int

18:53:38 HOL: theory HOL.Real

18:53:40 Timing FOLP-ex (2 threads, 3.849s elapsed time, 6.608s cpu time, 0.088s GC time, factor 1.72)

18:53:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP-ex

18:53:40 Finished FOLP-ex (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.49)

18:53:40 Running Sequents ...

18:53:40 Sequents: theory Sequents.Sequents

18:53:40 Sequents: theory Sequents.LK0

18:53:40 Sequents: theory Sequents.ILL

18:53:40 HOL: theory HOL.Real_Vector_Spaces

18:53:40 Sequents: theory Sequents.ILL_predlog

18:53:40 Sequents: theory Sequents.Washing

18:53:40 Sequents: theory Sequents.LK

18:53:40 Sequents: theory Sequents.Modal0

18:53:40 Sequents: theory Sequents.S4

18:53:40 Sequents: theory Sequents.S43

18:53:40 Sequents: theory Sequents.Hard_Quantifiers

18:53:41 Sequents: theory Sequents.Nat

18:53:41 Sequents: theory Sequents.Propositional

18:53:41 Sequents: theory Sequents.Quantifiers

18:53:41 Sequents: theory Sequents.T

18:53:43 HOL-Proofs: theory HOL.Euclidean_Division

18:53:45 Timing Sequents (2 threads, 3.774s elapsed time, 7.260s cpu time, 0.156s GC time, factor 1.92)

18:53:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Sequents/Sequents

18:53:45 Finished Sequents (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.65)

18:53:45 Running LCF ...

18:53:45 LCF: theory IFOL

18:53:46 LCF: theory FOL

18:53:48 LCF: theory LCF.LCF

18:53:49 LCF: theory LCF.Ex1

18:53:49 LCF: theory LCF.Ex2

18:53:49 LCF: theory LCF.Ex3

18:53:49 LCF: theory LCF.Ex4

18:53:50 Timing LCF (2 threads, 3.854s elapsed time, 4.332s cpu time, 0.160s GC time, factor 1.12)

18:53:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/LCF/LCF

18:53:50 Finished LCF (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.00)

18:53:50 Running Spec_Check ...

18:53:50 HOL: theory HOL.Inequalities

18:53:50 HOL: theory HOL.Limits

18:53:50 Spec_Check: theory Spec_Check.Spec_Check

18:53:50 Spec_Check: theory Spec_Check.Examples

18:53:53 HOL-Proofs: theory HOL.Parity

18:53:53 Timing Spec_Check (2 threads, 1.967s elapsed time, 3.208s cpu time, 0.012s GC time, factor 1.63)

18:53:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/Spec_Check

18:53:53 Finished Spec_Check (0:00:02 elapsed time, 0:00:03 cpu time)

18:53:53 Running ZF-Resid ...

18:53:53 HOL: theory HOL.Deriv

18:53:53 ZF-Resid: theory ZF-Resid.Redex

18:53:53 ZF-Resid: theory ZF-Resid.Substitution

18:53:53 ZF-Resid: theory ZF-Resid.Residuals

18:53:54 ZF-Resid: theory ZF-Resid.Reduction

18:53:54 ZF-Resid: theory ZF-Resid.Confluence

18:53:55 HOL: theory HOL.NthRoot

18:53:55 HOL: theory HOL.Series

18:53:55 Timing ZF-Resid (2 threads, 1.669s elapsed time, 2.680s cpu time, 0.000s GC time, factor 1.61)

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

18:53:55 Finished ZF-Resid (0:00:02 elapsed time)

18:53:55 Running ZF-IMP ...

18:53:56 ZF-IMP: theory ZF-IMP.Com

18:53:56 ZF-IMP: theory ZF-IMP.Denotation

18:53:56 ZF-IMP: theory ZF-IMP.Equiv

18:53:56 HOL: theory HOL.Transcendental

18:53:57 HOL-Proofs: theory HOL.Divides

18:54:00 Timing ZF-IMP (2 threads, 1.069s elapsed time, 1.244s cpu time, 0.000s GC time, factor 1.16)

18:54:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP

18:54:00 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP/document.pdf

18:54:00 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP/outline.pdf

18:54:00 Finished ZF-IMP (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.61)

18:54:00 Running CTT ...

18:54:01 CTT: theory CTT.CTT

18:54:01 CTT: theory CTT.Elimination

18:54:01 CTT: theory CTT.Equality

18:54:01 CTT: theory CTT.Synthesis

18:54:01 CTT: theory CTT.Typechecking

18:54:02 HOL: theory HOL.Complex

18:54:02 HOL: theory HOL.MacLaurin

18:54:04 HOL-Proofs: theory HOL.Code_Numeral

18:54:04 HOL: theory Complex_Main

18:54:05 HOL-Proofs: theory HOL.Numeral_Simprocs

18:54:06 Timing CTT (2 threads, 0.928s elapsed time, 1.308s cpu time, 0.000s GC time, factor 1.41)

18:54:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT

18:54:06 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/document.pdf

18:54:06 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/outline.pdf

18:54:06 Finished CTT (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.59)

18:54:06 Running ZF-Coind ...

18:54:06 ZF-Coind: theory ZF-Coind.Language

18:54:06 ZF-Coind: theory ZF-Coind.Map

18:54:06 ZF-Coind: theory ZF-Coind.Types

18:54:06 ZF-Coind: theory ZF-Coind.Values

18:54:06 ZF-Coind: theory ZF-Coind.Dynamic

18:54:06 HOL-Proofs: theory HOL.Semiring_Normalization

18:54:06 ZF-Coind: theory ZF-Coind.Static

18:54:06 ZF-Coind: theory ZF-Coind.ECR

18:54:07 Timing ZF-Coind (2 threads, 0.775s elapsed time, 1.456s cpu time, 0.000s GC time, factor 1.88)

18:54:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Coind

18:54:07 Finished ZF-Coind (0:00:01 elapsed time)

18:54:07 Running Cube ...

18:54:07 Cube: theory Cube.Cube

18:54:07 Cube: theory Cube.Example

18:54:08 HOL-Proofs: theory HOL.SMT

18:54:08 Timing Cube (2 threads, 0.321s elapsed time, 0.332s cpu time, 0.000s GC time, factor 1.03)

18:54:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Cube/Cube

18:54:08 Finished Cube (0:00:00 elapsed time)

18:54:08 Running Logics_ZF ...

18:54:08 Logics_ZF: theory Logics_ZF.FOL_examples

18:54:08 Logics_ZF: theory Logics_ZF.If

18:54:08 Logics_ZF: theory Logics_ZF.ZF_Isar

18:54:08 HOL-Proofs: theory HOL.Set_Interval

18:54:08 Logics_ZF: theory Logics_ZF.ZF_examples

18:54:09 Logics_ZF: theory Logics_ZF.IFOL_examples

18:54:11 HOL-Proofs: theory HOL.Groebner_Basis

18:54:14 Timing Logics_ZF (2 threads, 0.310s elapsed time, 0.600s cpu time, 0.000s GC time, factor 1.93)

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

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

18:54:14 Finished Logics_ZF (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.07)

18:54:14 Running Intro ...

18:54:18 Timing Intro (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

18:54:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro

18:54:18 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro/intro.pdf

18:54:18 Finished Intro (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.07)

18:54:18 Running Logics ...

18:54:23 HOL-Proofs: theory HOL.Conditionally_Complete_Lattices

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

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

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

18:54:23 Finished Logics (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.07)

18:54:23 Running Nitpick ...

18:54:23 HOL-Proofs: theory HOL.Filter

18:54:27 Timing Nitpick (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

18:54:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick

18:54:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick/nitpick.pdf

18:54:27 Finished Nitpick (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.07)

18:54:27 Running System ...

18:54:28 System: theory System.Base

18:54:28 System: theory System.Environment

18:54:28 System: theory System.Misc

18:54:28 System: theory System.Presentation

18:54:28 System: theory System.Scala

18:54:28 System: theory System.Sessions

18:54:28 HOL-Proofs: theory HOL.Presburger

18:54:33 Timing System (2 threads, 0.341s elapsed time, 0.484s cpu time, 0.000s GC time, factor 1.42)

18:54:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System

18:54:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System/system.pdf

18:54:33 Finished System (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.10)

18:54:33 Running SML ...

18:54:33 SML: theory SML.Examples

18:54:34 Timing SML (2 threads, 0.016s elapsed time, 0.016s cpu time, 0.000s GC time, factor 0.98)

18:54:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/SML

18:54:34 Finished SML (0:00:00 elapsed time)

18:54:34 Running Sledgehammer ...

18:54:38 Timing Sledgehammer (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

18:54:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer

18:54:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer/sledgehammer.pdf

18:54:38 Finished Sledgehammer (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.07)

18:54:42 HOL-Proofs: theory HOL.Sledgehammer

18:54:45 HOL-Proofs: theory HOL.List

18:55:51 HOL-Proofs: theory HOL.Groups_List

18:55:52 HOL-Proofs: theory HOL.Factorial

18:55:54 HOL-Proofs: theory HOL.Binomial

18:55:59 HOL-Proofs: theory HOL.GCD

18:56:06 HOL-Proofs: theory HOL.Map

18:56:10 HOL-Proofs: theory HOL.Enum

18:56:30 HOL-Proofs: theory HOL.Random

18:57:17 HOL-Proofs: theory HOL.String

18:57:19 HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint

18:57:28 HOL-Proofs: theory HOL.Predicate

18:57:30 HOL-Proofs: theory HOL.Lazy_Sequence

18:57:30 Timing HOL (2 threads, 305.298s elapsed time, 569.676s cpu time, 58.996s GC time, factor 1.87)

18:57:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL

18:57:30 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/document.pdf

18:57:30 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/outline.pdf

18:57:30 Finished HOL (0:06:33 elapsed time, 0:11:45 cpu time, factor 1.79)

18:57:30 Building HOL-Library ...

18:57:31 Building HOLCF ...

18:57:32 HOL-Proofs: theory HOL.Limited_Sequence

18:57:32 HOL-Proofs: theory HOL.Typerep

18:57:32 HOLCF: theory HOL-Library.Nat_Bijection

18:57:32 HOLCF: theory HOL-Library.Old_Datatype

18:57:32 HOL-Library: theory HOL-Library.Adhoc_Overloading

18:57:32 HOL-Library: theory HOL-Library.Lattice_Syntax

18:57:32 HOL-Library: theory HOL-Library.AList

18:57:32 HOL-Library: theory HOL-Library.BNF_Axiomatization

18:57:32 HOL-Library: theory HOL-Library.BNF_Corec

18:57:33 HOLCF: theory HOLCF.Porder

18:57:33 HOLCF: theory HOL-Library.Countable

18:57:33 HOLCF: theory HOLCF.Pcpo

18:57:33 HOL-Proofs: theory HOL.Code_Evaluation

18:57:34 HOL-Library: theory HOL-Library.DAList

18:57:34 HOLCF: theory HOLCF.Cont

18:57:35 HOLCF: theory HOLCF.Adm

18:57:35 HOLCF: theory HOLCF.Discrete

18:57:35 HOLCF: theory HOLCF.Cpodef

18:57:35 HOL-Proofs: theory HOL.Quickcheck_Random

18:57:35 HOLCF: theory HOLCF.Fun_Cpo

18:57:35 HOLCF: theory HOLCF.Product_Cpo

18:57:35 HOLCF: theory HOLCF.Cfun

18:57:36 HOL-Library: theory HOL-Library.Bit

18:57:36 HOL-Library: theory HOL-Library.Boolean_Algebra

18:57:36 HOLCF: theory HOLCF.Completion

18:57:36 HOLCF: theory HOLCF.Cprod

18:57:36 HOLCF: theory HOLCF.Deflation

18:57:36 HOL-Library: theory HOL-Library.Cancellation

18:57:36 HOLCF: theory HOLCF.Fix

18:57:37 HOLCF: theory HOLCF.Sfun

18:57:37 HOLCF: theory HOLCF.Sprod

18:57:37 HOLCF: theory HOLCF.Up

18:57:37 HOL-Library: theory HOL-Library.Multiset

18:57:38 HOLCF: theory HOLCF.Lift

18:57:38 HOL-Proofs: theory HOL.Quickcheck_Exhaustive

18:57:38 HOLCF: theory HOLCF.One

18:57:38 HOLCF: theory HOLCF.Tr

18:57:39 HOLCF: theory HOLCF.Ssum

18:57:39 HOLCF: theory HOLCF.Fixrec

18:57:39 HOLCF: theory HOLCF.Map_Functions

18:57:40 HOLCF: theory HOLCF.Bifinite

18:57:40 HOLCF: theory HOLCF.Domain_Aux

18:57:41 HOLCF: theory HOLCF.Universal

18:57:41 HOL-Library: theory HOL-Library.Cardinal_Notations

18:57:41 HOL-Library: theory HOL-Library.Char_ord

18:57:41 HOL-Library: theory HOL-Library.Code_Abstract_Nat

18:57:41 HOL-Library: theory HOL-Library.Code_Binary_Nat

18:57:41 HOL-Library: theory HOL-Library.Code_Target_Nat

18:57:41 HOL-Library: theory HOL-Library.Code_Char

18:57:41 HOL-Library: theory HOL-Library.Code_Prolog

18:57:42 HOL-Library: theory HOL-Library.Code_Target_Int

18:57:42 HOL-Library: theory HOL-Library.Code_Target_Numeral

18:57:42 HOL-Library: theory HOL-Library.Code_Test

18:57:42 HOLCF: theory HOLCF.Algebraic

18:57:42 HOLCF: theory HOLCF.Compact_Basis

18:57:42 HOL-Library: theory HOL-Library.DAList_Multiset

18:57:43 HOLCF: theory HOLCF.LowerPD

18:57:43 HOLCF: theory HOLCF.UpperPD

18:57:43 HOLCF: theory HOLCF.Representable

18:57:43 HOLCF: theory HOLCF.ConvexPD

18:57:43 HOL-Library: theory HOL-Library.Multiset_Order

18:57:43 HOL-Library: theory HOL-Library.Permutation

18:57:43 HOL-Library: theory HOL-Library.Combine_PER

18:57:44 HOL-Library: theory HOL-Library.Complete_Partial_Order2

18:57:44 HOL-Library: theory HOL-Library.Conditional_Parametricity

18:57:44 HOL-Proofs: theory HOL.Record

18:57:44 HOL-Library: theory HOL-Library.Datatype_Records

18:57:44 HOL-Library: theory HOL-Library.Debug

18:57:45 HOL-Library: theory HOL-Library.Disjoint_Sets

18:57:45 HOL-Library: theory HOL-Library.Permutations

18:57:46 HOLCF: theory HOLCF.Domain

18:57:46 HOL-Library: theory HOL-Library.Dlist

18:57:46 HOL-Proofs: theory HOL.Nitpick

18:57:47 HOL-Library: theory HOL-Library.Fun_Lexorder

18:57:47 HOL-Library: theory HOL-Library.FuncSet

18:57:47 HOL-Library: theory HOL-Library.Function_Algebras

18:57:47 HOL-Library: theory HOL-Library.Function_Division

18:57:47 HOLCF: theory HOLCF.Powerdomains

18:57:47 HOL-Library: theory HOL-Library.Groups_Big_Fun

18:57:47 HOL-Library: theory HOL-Library.IArray

18:57:48 HOL-Library: theory HOL-Library.Infinite_Set

18:57:48 HOL-Library: theory HOL-Library.Omega_Words_Fun

18:57:48 HOL-Library: theory HOL-Library.Ramsey

18:57:48 HOL-Library: theory HOL-Library.LaTeXsugar

18:57:48 HOLCF: theory HOLCF

18:57:49 HOL-Library: theory HOL-Library.Lattice_Constructions

18:57:49 HOL-Library: theory HOL-Library.ListVector

18:57:49 HOL-Library: theory HOL-Library.List_lexord

18:57:49 HOL-Library: theory HOL-Library.Mapping

18:57:50 HOL-Library: theory HOL-Library.AList_Mapping

18:57:51 HOL-Library: theory HOL-Library.Monad_Syntax

18:57:51 HOL-Library: theory HOL-Library.State_Monad

18:57:53 HOL-Library: theory HOL-Library.More_List

18:57:54 HOL-Library: theory HOL-Library.Nat_Bijection

18:57:54 HOL-Library: theory HOL-Library.Old_Datatype

18:57:54 HOL-Library: theory HOL-Library.Stream

18:57:55 HOL-Proofs: theory HOL.Nunchaku

18:57:55 HOL-Library: theory HOL-Library.Old_Recdef

18:57:56 HOL-Library: theory HOL-Library.Open_State_Syntax

18:57:56 HOL-Library: theory HOL-Library.Option_ord

18:57:56 HOL-Library: theory HOL-Library.Parallel

18:57:56 HOL-Library: theory HOL-Library.Pattern_Aliases

18:57:56 HOL-Proofs: theory HOL.Quickcheck_Narrowing

18:57:56 HOL-Library: theory HOL-Library.Perm

18:57:56 HOL-Library: theory HOL-Library.Phantom_Type

18:57:58 HOL-Library: theory HOL-Library.Cardinality

18:57:58 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs

18:57:59 HOL-Library: theory HOL-Library.Numeral_Type

18:57:59 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck

18:57:59 HOL-Library: theory HOL-Library.Preorder

18:57:59 HOL-Library: theory HOL-Library.Product_Lexorder

18:57:59 HOL-Library: theory HOL-Library.Product_Plus

18:57:59 HOL-Library: theory HOL-Library.Product_Order

18:58:00 HOL-Library: theory HOL-Library.Finite_Lattice

18:58:00 HOL-Library: theory HOL-Library.Type_Length

18:58:00 HOL-Library: theory HOL-Library.Saturated

18:58:00 HOL-Library: theory HOL-Library.Quotient_Syntax

18:58:00 HOL-Library: theory HOL-Library.Quotient_Option

18:58:00 HOL-Library: theory HOL-Library.Quotient_Product

18:58:00 HOL-Library: theory HOL-Library.Quotient_Set

18:58:01 HOL-Library: theory HOL-Library.Quotient_List

18:58:01 HOL-Proofs: theory HOL.Random_Pred

18:58:01 HOL-Library: theory HOL-Library.Quotient_Sum

18:58:01 HOL-Library: theory HOL-Library.Quotient_Type

18:58:01 HOL-Library: theory HOL-Library.RBT_Impl

18:58:02 HOL-Proofs: theory HOL.Random_Sequence

18:58:02 HOL-Library: theory HOL-Library.Realizers

18:58:02 HOL-Library: theory HOL-Library.Reflection

18:58:02 HOL-Library: theory HOL-Library.Refute

18:58:03 HOL-Proofs: theory HOL.Predicate_Compile

18:58:04 HOL-Library: theory HOL-Library.Rewrite

18:58:04 HOL-Library: theory HOL-Library.Set_Algebras

18:58:04 HOL-Library: theory HOL-Library.Simps_Case_Conv

18:58:04 HOL-Library: theory HOL-Library.Extended

18:58:06 HOL-Proofs: theory Main

18:58:06 HOL-Library: theory HOL-Library.Stirling

18:58:07 HOL-Library: theory HOL-Library.Sublist

18:58:08 HOL-Proofs: theory HOL-Library.Realizers

18:58:08 HOL-Library: theory HOL-Library.Prefix_Order

18:58:08 HOL-Library: theory HOL-Library.Subseq_Order

18:58:08 HOL-Library: theory HOL-Library.Transitive_Closure_Table

18:58:11 Timing HOLCF (2 threads, 18.296s elapsed time, 35.984s cpu time, 2.304s GC time, factor 1.97)

18:58:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF

18:58:11 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/document.pdf

18:58:11 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/outline.pdf

18:58:11 Finished HOLCF (0:00:39 elapsed time, 0:01:05 cpu time, factor 1.69)

18:58:11 Building IOA ...

18:58:11 HOL-Library: theory HOL-Library.Tree

18:58:12 IOA: theory IOA.Asig

18:58:12 IOA: theory IOA.Seq

18:58:12 IOA: theory IOA.Automata

18:58:13 IOA: theory IOA.Sequence

18:58:13 IOA: theory IOA.Pred

18:58:14 HOL-Library: theory HOL-Library.Tree_Multiset

18:58:14 IOA: theory IOA.Traces

18:58:14 IOA: theory IOA.TL

18:58:15 HOL-Library: theory HOL-Library.Uprod

18:58:15 IOA: theory IOA.CompoExecs

18:58:16 HOL-Library: theory HOL-Library.While_Combinator

18:58:16 IOA: theory IOA.RefMappings

18:58:16 IOA: theory IOA.RefCorrectness

18:58:16 IOA: theory IOA.CompoScheds

18:58:16 IOA: theory IOA.Simulations

18:58:16 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint

18:58:17 IOA: theory IOA.SimCorrectness

18:58:17 HOL-Library: theory HOL-Library.Countable

18:58:17 IOA: theory IOA.ShortExecutions

18:58:17 IOA: theory IOA.Deadlock

18:58:17 IOA: theory IOA.CompoTraces

18:58:18 HOL-Library: theory HOL-Library.Countable_Set

18:58:19 IOA: theory IOA.Compositionality

18:58:19 HOL-Library: theory HOL-Library.Countable_Complete_Lattices

18:58:19 IOA: theory IOA.IOA

18:58:19 IOA: theory IOA.TLS

18:58:20 IOA: theory IOA.LiveIOA

18:58:20 IOA: theory IOA.Abstraction

18:58:21 HOL-Library: theory HOL-Library.Countable_Set_Type

18:58:24 HOL-Library: theory HOL-Library.FSet

18:58:28 HOL-Library: theory HOL-Library.Finite_Map

18:58:31 HOL-Library: theory HOL-Library.BigO

18:58:32 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float

18:58:33 HOL-Library: theory HOL-Library.Diagonal_Subsequence

18:58:33 HOL-Library: theory HOL-Library.Discrete

18:58:33 HOL-Library: theory HOL-Library.Going_To_Filter

18:58:33 HOL-Library: theory HOL-Library.Indicator_Function

18:58:34 HOL-Library: theory HOL-Library.Lattice_Algebras

18:58:38 HOL-Library: theory HOL-Library.Liminf_Limsup

18:58:38 HOL-Library: theory HOL-Library.Log_Nat

18:58:39 HOL-Library: theory HOL-Library.Float

18:58:40 HOL-Library: theory HOL-Library.RBT

18:58:41 HOL-Library: theory HOL-Library.RBT_Mapping

18:58:41 HOL-Library: theory HOL-Library.RBT_Set

18:58:42 HOL-Library: theory HOL-Library.Lub_Glb

18:58:42 HOL-Library: theory HOL-Library.Multiset_Permutations

18:58:42 HOL-Library: theory HOL-Library.Nonpos_Ints

18:58:43 HOL-Library: theory HOL-Library.OptionalSugar

18:58:43 HOL-Library: theory HOL-Library.Order_Continuity

18:58:43 HOL-Library: theory HOL-Library.Periodic_Fun

18:58:43 HOL-Library: theory HOL-Library.Quadratic_Discriminant

18:58:43 HOL-Library: theory HOL-Library.Sum_of_Squares

18:58:44 HOL-Library: theory HOL-Library.Extended_Nat

18:58:45 HOL-Library: theory HOL-Library.Extended_Real

18:58:45 Timing IOA (2 threads, 18.706s elapsed time, 34.856s cpu time, 1.460s GC time, factor 1.86)

18:58:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA

18:58:45 Finished IOA (0:00:33 elapsed time, 0:00:54 cpu time, factor 1.60)

18:58:45 Building HOL-TLA ...

18:58:46 HOL-TLA: theory HOL-TLA.Intensional

18:58:46 HOL-TLA: theory HOL-TLA.Stfun

18:58:46 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams

18:58:47 HOL-TLA: theory HOL-TLA.Action

18:58:47 HOL-TLA: theory HOL-TLA.Init

18:58:47 HOL-TLA: theory HOL-TLA.TLA

18:58:48 HOL-Library: theory HOL-Library.Tree_Real

18:58:50 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real

18:58:52 HOL-Library: theory HOL-Library.Library

18:58:58 Timing HOL-TLA (2 threads, 1.890s elapsed time, 2.984s cpu time, 0.000s GC time, factor 1.58)

18:58:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA

18:58:58 Finished HOL-TLA (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.27)

18:58:58 Building HOL-Analysis ...

18:59:15 HOL-Analysis: theory HOL-Library.Cancellation

18:59:15 HOL-Analysis: theory HOL-Library.Disjoint_Sets

18:59:16 HOL-Analysis: theory HOL-Library.FuncSet

18:59:16 HOL-Analysis: theory HOL-Library.Multiset

18:59:16 HOL-Analysis: theory HOL-Library.Infinite_Set

18:59:16 HOL-Analysis: theory HOL-Library.Nat_Bijection

18:59:17 HOL-Analysis: theory HOL-Library.Old_Datatype

18:59:17 HOL-Analysis: theory HOL-Library.Phantom_Type

18:59:18 HOL-Analysis: theory HOL-Library.Cardinality

18:59:20 HOL-Analysis: theory HOL-Library.Numeral_Type

18:59:21 HOL-Analysis: theory HOL-Library.Product_Plus

18:59:21 HOL-Analysis: theory HOL-Library.Product_Order

18:59:21 HOL-Analysis: theory HOL-Library.Set_Algebras

18:59:22 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring

18:59:22 HOL-Analysis: theory HOL-Library.Permutations

18:59:23 HOL-Analysis: theory HOL-Library.Countable

18:59:24 HOL-Analysis: theory HOL-Library.Countable_Set

18:59:25 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices

18:59:27 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable

18:59:27 HOL-Analysis: theory HOL-Analysis.Infinite_Products

18:59:28 HOL-Analysis: theory HOL-Analysis.Inner_Product

18:59:28 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm

18:59:29 HOL-Analysis: theory HOL-Analysis.Product_Vector

18:59:29 HOL-Analysis: theory HOL-Analysis.L2_Norm

18:59:29 HOL-Analysis: theory HOL-Analysis.Euclidean_Space

18:59:31 HOL-Analysis: theory HOL-Analysis.Linear_Algebra

18:59:34 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product

18:59:35 HOL-Analysis: theory HOL-Analysis.Operator_Norm

18:59:36 HOL-Analysis: theory HOL-Computational_Algebra.Primes

18:59:36 HOL-Analysis: theory HOL-Analysis.Poly_Roots

18:59:36 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series

18:59:36 HOL-Analysis: theory HOL-Library.Discrete

18:59:36 HOL-Analysis: theory HOL-Library.Indicator_Function

18:59:37 HOL-Analysis: theory HOL-Library.Liminf_Limsup

18:59:37 HOL-Analysis: theory HOL-Library.Nonpos_Ints

18:59:38 HOL-Analysis: theory HOL-Library.Order_Continuity

18:59:38 HOL-Analysis: theory HOL-Library.Extended_Nat

18:59:39 HOL-Analysis: theory HOL-Library.Extended_Real

18:59:40 HOL-Analysis: theory HOL-Library.Periodic_Fun

18:59:40 HOL-Analysis: theory HOL-Library.Sum_of_Squares

18:59:43 HOL-Analysis: theory HOL-Analysis.Norm_Arith

18:59:44 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space

18:59:44 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real

18:59:46 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra

18:59:49 HOL-Analysis: theory HOL-Analysis.Measurable

18:59:50 HOL-Analysis: theory HOL-Analysis.Measure_Space

18:59:50 HOL-Analysis: theory HOL-Analysis.Connected

18:59:53 HOL-Analysis: theory HOL-Analysis.Caratheodory

18:59:53 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space

18:59:53 HOL-Analysis: theory HOL-Analysis.Tagged_Division

18:59:55 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits

18:59:56 HOL-Analysis: theory HOL-Analysis.Summation_Tests

18:59:57 HOL-Analysis: theory HOL-Analysis.Starlike

18:59:57 HOL-Analysis: theory HOL-Analysis.Uniform_Limit

18:59:59 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function

19:00:00 HOL-Analysis: theory HOL-Analysis.Continuous_Extension

19:00:00 HOL-Analysis: theory HOL-Analysis.Path_Connected

19:00:08 HOL-Analysis: theory HOL-Analysis.Homeomorphism

19:00:09 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint

19:00:11 HOL-Analysis: theory HOL-Analysis.Derivative

19:00:13 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space

19:00:13 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems

19:00:16 HOL-Analysis: theory HOL-Analysis.Determinants

19:00:16 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem

19:00:16 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space

19:00:17 HOL-Analysis: theory HOL-Analysis.Polytope

19:00:20 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected

19:00:20 HOL-Analysis: theory HOL-Analysis.Borel_Space

19:00:22 HOL-Analysis: theory HOL-Analysis.Lipschitz

19:00:22 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration

19:00:23 HOL-Analysis: theory HOL-Analysis.Regularity

19:00:25 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure

19:00:26 HOL-Analysis: theory HOL-Analysis.Embed_Measure

19:00:26 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure

19:00:27 HOL-Analysis: theory HOL-Analysis.Bochner_Integration

19:00:27 HOL-Analysis: theory HOL-Analysis.Function_Topology

19:00:29 HOL-Analysis: theory HOL-Analysis.Complete_Measure

19:00:29 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym

19:00:30 HOL-Analysis: theory HOL-Analysis.Set_Integral

19:00:30 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure

19:00:30 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum

19:00:32 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration

19:00:36 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function

19:00:36 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration

19:00:37 HOL-Analysis: theory HOL-Analysis.Integral_Test

19:00:38 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics

19:00:38 HOL-Analysis: theory HOL-Analysis.Improper_Integral

19:00:38 HOL-Analysis: theory HOL-Analysis.Interval_Integral

19:00:39 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution

19:00:40 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental

19:00:42 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem

19:00:42 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers

19:00:43 HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem

19:00:43 HOL-Analysis: theory HOL-Analysis.Further_Topology

19:00:46 HOL-Analysis: theory HOL-Analysis.Jordan_Curve

19:00:47 HOL-Analysis: theory HOL-Analysis.Conformal_Mappings

19:00:50 HOL-Analysis: theory HOL-Analysis.FPS_Convergence

19:00:50 HOL-Analysis: theory HOL-Analysis.Gamma_Function

19:00:52 HOL-Analysis: theory HOL-Analysis.Great_Picard

19:00:53 HOL-Analysis: theory HOL-Analysis.Riemann_Mapping

19:00:53 HOL-Analysis: theory HOL-Analysis.Ball_Volume

19:00:54 HOL-Analysis: theory HOL-Analysis.Winding_Numbers

19:00:55 HOL-Analysis: theory HOL-Analysis.Analysis

19:02:11 Timing HOL-Library (2 threads, 208.339s elapsed time, 390.280s cpu time, 26.672s GC time, factor 1.87)

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

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

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

19:02:11 Finished HOL-Library (0:04:38 elapsed time, 0:08:16 cpu time, factor 1.79)

19:02:11 Building HOL-Computational_Algebra ...

19:02:13 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure

19:02:13 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field

19:02:13 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring

19:02:21 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm

19:02:21 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial

19:02:29 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction

19:02:29 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes

19:02:30 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers

19:02:30 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree

19:02:30 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring

19:02:30 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series

19:02:31 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra

19:02:33 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial

19:02:35 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS

19:02:47 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra

19:03:49 Timing HOL-Computational_Algebra (2 threads, 69.698s elapsed time, 122.940s cpu time, 6.084s GC time, factor 1.76)

19:03:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Computational_Algebra

19:03:49 Finished HOL-Computational_Algebra (0:01:37 elapsed time, 0:02:37 cpu time, factor 1.62)

19:03:49 Building HOL-Number_Theory ...

19:03:51 HOL-Number_Theory: theory HOL-Algebra.Congruence

19:03:51 HOL-Number_Theory: theory HOL-Number_Theory.Cong

19:03:52 HOL-Number_Theory: theory HOL-Algebra.Order

19:03:53 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes

19:03:53 HOL-Number_Theory: theory HOL-Number_Theory.Fib

19:03:54 HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers

19:03:54 HOL-Number_Theory: theory HOL-Algebra.Lattice

19:03:55 HOL-Number_Theory: theory HOL-Number_Theory.Totient

19:03:55 HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice

19:03:57 HOL-Number_Theory: theory HOL-Algebra.Group

19:03:58 HOL-Number_Theory: theory HOL-Algebra.Coset

19:03:58 HOL-Number_Theory: theory HOL-Algebra.FiniteProduct

19:03:59 HOL-Number_Theory: theory HOL-Algebra.Ring

19:04:03 HOL-Number_Theory: theory HOL-Algebra.AbelCoset

19:04:04 HOL-Number_Theory: theory HOL-Algebra.Module

19:04:06 HOL-Number_Theory: theory HOL-Algebra.More_Group

19:04:06 HOL-Number_Theory: theory HOL-Algebra.More_Finite_Product

19:04:06 HOL-Number_Theory: theory HOL-Algebra.More_Ring

19:04:07 HOL-Number_Theory: theory HOL-Algebra.Ideal

19:04:10 HOL-Number_Theory: theory HOL-Algebra.RingHom

19:04:13 HOL-Number_Theory: theory HOL-Algebra.UnivPoly

19:04:25 HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group

19:04:28 HOL-Number_Theory: theory HOL-Number_Theory.Residues

19:04:31 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion

19:04:31 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington

19:04:31 HOL-Number_Theory: theory HOL-Number_Theory.Gauss

19:04:31 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity

19:04:32 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory

19:06:36 Timing HOL-Number_Theory (2 threads, 112.737s elapsed time, 202.000s cpu time, 12.908s GC time, factor 1.79)

19:06:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory

19:06:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/document.pdf

19:06:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/outline.pdf

19:06:36 Finished HOL-Number_Theory (0:02:46 elapsed time, 0:04:29 cpu time, factor 1.62)

19:06:36 Building HOL-Algebra ...

19:06:38 HOL-Algebra: theory HOL-Algebra.Exponent

19:06:38 HOL-Algebra: theory HOL-Algebra.Congruence

19:06:39 HOL-Algebra: theory HOL-Algebra.Order

19:06:41 HOL-Algebra: theory HOL-Algebra.Lattice

19:06:42 HOL-Algebra: theory HOL-Algebra.Complete_Lattice

19:06:43 HOL-Algebra: theory HOL-Algebra.Galois_Connection

19:06:45 HOL-Algebra: theory HOL-Algebra.Group

19:06:46 HOL-Algebra: theory HOL-Algebra.Bij

19:06:47 HOL-Algebra: theory HOL-Algebra.Coset

19:06:47 HOL-Algebra: theory HOL-Algebra.FiniteProduct

19:06:48 HOL-Algebra: theory HOL-Algebra.Sylow

19:06:48 HOL-Algebra: theory HOL-Algebra.Divisibility

19:06:49 HOL-Algebra: theory HOL-Algebra.Ring

19:06:52 HOL-Algebra: theory HOL-Algebra.AbelCoset

19:06:53 HOL-Algebra: theory HOL-Algebra.Module

19:06:54 HOL-Algebra: theory HOL-Algebra.More_Group

19:06:54 HOL-Algebra: theory HOL-Algebra.More_Finite_Product

19:06:55 HOL-Algebra: theory HOL-Algebra.More_Ring

19:06:58 HOL-Algebra: theory HOL-Algebra.Ideal

19:07:01 HOL-Algebra: theory HOL-Algebra.RingHom

19:07:02 HOL-Algebra: theory HOL-Algebra.QuotRing

19:07:03 HOL-Algebra: theory HOL-Algebra.UnivPoly

19:07:04 HOL-Algebra: theory HOL-Algebra.IntRing

19:07:16 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group

19:09:09 Timing HOL-Algebra (2 threads, 90.742s elapsed time, 163.864s cpu time, 18.384s GC time, factor 1.81)

19:09:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra

19:09:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/document.pdf

19:09:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline.pdf

19:09:09 Finished HOL-Algebra (0:02:31 elapsed time, 0:04:02 cpu time, factor 1.60)

19:09:09 Building HOL-Word ...

19:09:10 HOL-Word: theory HOL-Library.Boolean_Algebra

19:09:10 HOL-Word: theory HOL-Library.Bit

19:09:10 HOL-Word: theory HOL-Library.Phantom_Type

19:09:11 HOL-Word: theory HOL-Word.Bits

19:09:11 HOL-Word: theory HOL-Word.Bits_Bit

19:09:11 HOL-Word: theory HOL-Word.Misc_Numeric

19:09:11 HOL-Word: theory HOL-Library.Cardinality

19:09:11 HOL-Word: theory HOL-Word.Bit_Representation

19:09:12 HOL-Word: theory HOL-Word.Bits_Int

19:09:13 HOL-Word: theory HOL-Library.Numeral_Type

19:09:14 HOL-Word: theory HOL-Library.Type_Length

19:09:14 HOL-Word: theory HOL-Word.Bit_Comparison

19:09:14 HOL-Word: theory HOL-Word.Bool_List_Representation

19:09:14 HOL-Word: theory HOL-Word.Word_Miscellaneous

19:09:14 HOL-Word: theory HOL-Word.Misc_Typedef

19:09:15 HOL-Word: theory HOL-Word.Word

19:09:21 HOL-Word: theory HOL-Word.WordBitwise

19:09:21 HOL-Word: theory HOL-Word.WordExamples

19:09:53 Timing HOL-Word (2 threads, 24.303s elapsed time, 46.412s cpu time, 2.164s GC time, factor 1.91)

19:09:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word

19:09:53 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/document.pdf

19:09:53 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/outline.pdf

19:09:53 Finished HOL-Word (0:00:43 elapsed time, 0:01:14 cpu time, factor 1.72)

19:09:53 Building HOLCF-Library ...

19:09:54 HOLCF-Library: theory HOL-Library.Infinite_Set

19:09:54 HOLCF-Library: theory HOLCF-Library.Bool_Discrete

19:09:55 HOLCF-Library: theory HOLCF-Library.Char_Discrete

19:09:55 HOLCF-Library: theory HOLCF-Library.Int_Discrete

19:09:55 HOLCF-Library: theory HOL-Library.Countable_Set

19:09:55 HOLCF-Library: theory HOLCF-Library.Defl_Bifinite

19:09:55 HOLCF-Library: theory HOL-Library.Countable_Complete_Lattices

19:09:56 HOLCF-Library: theory HOLCF-Library.List_Cpo

19:09:56 HOLCF-Library: theory HOLCF-Library.Nat_Discrete

19:09:56 HOLCF-Library: theory HOLCF-Library.Sum_Cpo

19:09:57 HOLCF-Library: theory HOLCF-Library.List_Predomain

19:09:58 HOLCF-Library: theory HOL-Library.Order_Continuity

19:09:58 HOLCF-Library: theory HOLCF-Library.Option_Cpo

19:09:58 HOLCF-Library: theory HOLCF-Library.HOL_Cpo

19:09:59 HOLCF-Library: theory HOL-Library.Extended_Nat

19:10:00 HOLCF-Library: theory HOLCF-Library.Stream

19:10:02 HOLCF-Library: theory HOLCF-Library.HOLCF_Library

19:10:24 Timing HOLCF-Library (2 threads, 15.734s elapsed time, 28.944s cpu time, 1.352s GC time, factor 1.84)

19:10:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Library

19:10:24 Finished HOLCF-Library (0:00:30 elapsed time, 0:00:47 cpu time, factor 1.57)

19:10:24 Building HOL-SPARK ...

19:10:25 HOL-SPARK: theory HOL-SPARK.SPARK_Setup

19:10:27 HOL-SPARK: theory HOL-SPARK.SPARK

19:10:37 Timing HOL-Proofs (2 threads, 1083.408s elapsed time, 1845.856s cpu time, 353.280s GC time, factor 1.70)

19:10:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs

19:10:37 Finished HOL-Proofs (0:19:39 elapsed time, 0:33:00 cpu time, factor 1.68)

19:10:37 Building HOL-Auth ...

19:10:39 HOL-Auth: theory HOL-Auth.Message

19:10:39 Timing HOL-SPARK (2 threads, 2.577s elapsed time, 3.444s cpu time, 0.140s GC time, factor 1.34)

19:10:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK

19:10:39 Finished HOL-SPARK (0:00:13 elapsed time, 0:00:17 cpu time, factor 1.27)

19:10:39 Building HOL-Nonstandard_Analysis ...

19:10:40 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Free_Ultrafilter

19:10:40 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.StarDef

19:10:42 HOL-Auth: theory HOL-Auth.All_Symmetric

19:10:42 HOL-Auth: theory HOL-Auth.Event

19:10:42 HOL-Auth: theory HOL-Auth.EventSC

19:10:42 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperNat

19:10:42 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperDef

19:10:42 HOL-Auth: theory HOL-Auth.Extensions

19:10:43 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSA

19:10:43 HOL-Auth: theory HOL-Auth.Analz

19:10:44 HOL-Auth: theory HOL-Auth.Guard

19:10:44 HOL-Auth: theory HOL-Auth.GuardK

19:10:45 HOL-Auth: theory HOL-Auth.List_Msg

19:10:45 HOL-Auth: theory HOL-Auth.Public

19:10:45 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSComplex

19:10:45 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Star

19:10:45 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLim

19:10:45 HOL-Auth: theory HOL-Auth.CertifiedEmail

19:10:46 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NatStar

19:10:46 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HDeriv

19:10:46 HOL-Auth: theory HOL-Auth.Guard_Public

19:10:46 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSEQ

19:10:47 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSeries

19:10:47 HOL-Auth: theory HOL-Auth.Guard_NS_Public

19:10:47 HOL-Auth: theory HOL-Auth.P2

19:10:47 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HTranscendental

19:10:47 HOL-Auth: theory HOL-Auth.Proto

19:10:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLog

19:10:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSCA

19:10:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hyperreal

19:10:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CStar

19:10:49 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CLim

19:10:49 HOL-Auth: theory HOL-Auth.KerberosIV

19:10:49 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hypercomplex

19:10:49 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Nonstandard_Analysis

19:10:51 HOL-Auth: theory HOL-Auth.KerberosIV_Gets

19:10:51 HOL-Auth: theory HOL-Auth.KerberosV

19:10:52 HOL-Auth: theory HOL-Auth.Kerberos_BAN

19:10:53 HOL-Auth: theory HOL-Auth.Kerberos_BAN_Gets

19:10:53 HOL-Auth: theory HOL-Auth.NS_Public

19:10:54 HOL-Auth: theory HOL-Auth.NS_Public_Bad

19:10:54 HOL-Auth: theory HOL-Auth.NS_Shared

19:10:54 HOL-Auth: theory HOL-Auth.OtwayRees

19:10:55 HOL-Auth: theory HOL-Auth.OtwayReesBella

19:10:55 HOL-Auth: theory HOL-Auth.OtwayRees_AN

19:10:55 HOL-Auth: theory HOL-Auth.OtwayRees_Bad

19:10:56 HOL-Auth: theory HOL-Auth.P1

19:10:56 HOL-Auth: theory HOL-Auth.Recur

19:10:57 HOL-Auth: theory HOL-Auth.WooLam

19:10:57 HOL-Auth: theory HOL-Auth.Yahalom

19:10:58 HOL-Auth: theory HOL-Auth.Yahalom2

19:10:59 HOL-Auth: theory HOL-Auth.Yahalom_Bad

19:11:00 HOL-Auth: theory HOL-Auth.ZhouGollmann

19:11:00 HOL-Auth: theory HOL-Auth.Auth_Shared

19:11:01 HOL-Auth: theory HOL-Auth.Auth_Guard_Public

19:11:02 HOL-Auth: theory HOL-Auth.Shared

19:11:02 HOL-Auth: theory HOL-Auth.Guard_Shared

19:11:03 HOL-Auth: theory HOL-Auth.TLS

19:11:03 HOL-Auth: theory HOL-Auth.Guard_OtwayRees

19:11:03 HOL-Auth: theory HOL-Auth.Guard_Yahalom

19:11:04 HOL-Auth: theory HOL-Auth.Auth_Guard_Shared

19:11:04 HOL-Auth: theory HOL-Auth.Smartcard

19:11:05 HOL-Auth: theory HOL-Auth.ShoupRubin

19:11:05 HOL-Auth: theory HOL-Auth.Auth_Public

19:11:06 HOL-Auth: theory HOL-Auth.ShoupRubinBella

19:11:08 HOL-Auth: theory HOL-Auth.Auth_Smartcard

19:11:18 Timing HOL-Nonstandard_Analysis (2 threads, 11.795s elapsed time, 22.168s cpu time, 1.188s GC time, factor 1.88)

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

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

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

19:11:18 Finished HOL-Nonstandard_Analysis (0:00:38 elapsed time, 0:01:00 cpu time, factor 1.58)

19:11:18 Building HOL-Nominal ...

19:11:19 HOL-Nominal: theory HOL-Nominal.Nominal

19:11:43 Timing HOL-Nominal (2 threads, 7.831s elapsed time, 13.912s cpu time, 0.776s GC time, factor 1.78)

19:11:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal

19:11:43 Finished HOL-Nominal (0:00:24 elapsed time, 0:00:35 cpu time, factor 1.44)

19:11:43 Building HOL-Eisbach ...

19:11:43 HOL-Eisbach: theory HOL-Eisbach.Eisbach

19:11:43 HOL-Eisbach: theory IFOL

19:11:44 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Old_Appl_Syntax

19:11:44 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Tools

19:11:44 HOL-Eisbach: theory HOL-Eisbach.Examples

19:11:45 HOL-Eisbach: theory HOL-Eisbach.Tests

19:11:45 HOL-Eisbach: theory FOL

19:11:47 HOL-Eisbach: theory HOL-Eisbach.Examples_FOL

19:11:58 Timing HOL-Eisbach (2 threads, 3.940s elapsed time, 7.864s cpu time, 0.200s GC time, factor 2.00)

19:11:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Eisbach

19:11:58 Finished HOL-Eisbach (0:00:14 elapsed time, 0:00:21 cpu time, factor 1.47)

19:11:58 Building Codegen_Basics ...

19:11:59 Codegen_Basics: theory Codegen_Basics.Setup

19:12:15 Timing Codegen_Basics (2 threads, 1.459s elapsed time, 1.544s cpu time, 0.000s GC time, factor 1.06)

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

19:12:15 Finished Codegen_Basics (0:00:17 elapsed time, 0:00:22 cpu time, factor 1.26)

19:12:15 Building Typeclass_Hierarchy_Basics ...

19:12:17 Typeclass_Hierarchy_Basics: theory Typeclass_Hierarchy_Basics.Setup

19:12:32 Timing Typeclass_Hierarchy_Basics (2 threads, 0.886s elapsed time, 0.996s cpu time, 0.000s GC time, factor 1.12)

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

19:12:32 Finished Typeclass_Hierarchy_Basics (0:00:16 elapsed time, 0:00:20 cpu time, factor 1.25)

19:12:32 Building HOL-Mirabelle ...

19:12:33 HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle

19:12:33 HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle_Test

19:12:43 Timing HOL-Mirabelle (2 threads, 0.569s elapsed time, 0.652s cpu time, 0.000s GC time, factor 1.15)

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

19:12:43 Finished HOL-Mirabelle (0:00:10 elapsed time, 0:00:13 cpu time, factor 1.25)

19:12:43 Running HOL-Nominal-Examples ...

19:12:45 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CK_Machine

19:12:45 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR_Takahashi

19:12:48 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class1

19:12:57 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Compile

19:13:16 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Contexts

19:13:23 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Crary

19:13:28 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Fsub

19:13:36 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Height

19:13:38 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lam_Funs

19:13:42 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR

19:13:42 HOL-Nominal-Examples: theory HOL-Nominal-Examples.SN

19:13:44 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lambda_mu

19:13:48 HOL-Nominal-Examples: theory HOL-Nominal-Examples.LocalWeakening

19:13:51 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Pattern

19:14:00 Timing HOL-Analysis (2 threads, 801.860s elapsed time, 1405.308s cpu time, 61.192s GC time, factor 1.75)

19:14:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis

19:14:00 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/document.pdf

19:14:00 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/manual.pdf

19:14:00 Finished HOL-Analysis (0:15:00 elapsed time, 0:25:34 cpu time, factor 1.71)

19:14:00 Building HOL-Probability ...

19:14:00 HOL-Nominal-Examples: theory HOL-Nominal-Examples.SOS

19:14:01 HOL-Probability: theory HOL-Library.Adhoc_Overloading

19:14:01 HOL-Probability: theory HOL-Library.Lattice_Syntax

19:14:01 HOL-Probability: theory HOL-Library.AList

19:14:02 HOL-Probability: theory HOL-Library.Complete_Partial_Order2

19:14:04 HOL-Probability: theory HOL-Library.Mapping

19:14:04 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Standardization

19:14:05 HOL-Probability: theory HOL-Library.AList_Mapping

19:14:05 HOL-Probability: theory HOL-Library.Monad_Syntax

19:14:05 HOL-Probability: theory HOL-Library.Stream

19:14:05 HOL-Probability: theory HOL-Library.Rewrite

19:14:06 HOL-Probability: theory HOL-Library.Sublist

19:14:07 HOL-Probability: theory HOL-Library.Tree

19:14:08 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Support

19:14:08 HOL-Probability: theory HOL-Library.FSet

19:14:08 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Type_Preservation

19:14:10 HOL-Probability: theory HOL-Library.Diagonal_Subsequence

19:14:10 HOL-Probability: theory HOL-Library.Multiset_Permutations

19:14:11 HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams

19:14:12 HOL-Probability: theory HOL-Library.Finite_Map

19:14:12 HOL-Nominal-Examples: theory HOL-Nominal-Examples.W

19:14:13 HOL-Probability: theory HOL-Probability.Discrete_Topology

19:14:14 HOL-Probability: theory HOL-Probability.Essential_Supremum

19:14:14 HOL-Probability: theory HOL-Probability.Probability_Measure

19:14:14 HOL-Probability: theory HOL-Probability.Fin_Map

19:14:16 HOL-Probability: theory HOL-Probability.Conditional_Expectation

19:14:16 HOL-Probability: theory HOL-Probability.Distribution_Functions

19:14:17 HOL-Probability: theory HOL-Probability.Giry_Monad

19:14:17 HOL-Probability: theory HOL-Probability.Weak_Convergence

19:14:17 HOL-Probability: theory HOL-Probability.Helly_Selection

19:14:20 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening

19:14:21 HOL-Probability: theory HOL-Probability.Stopping_Time

19:14:21 HOL-Probability: theory HOL-Probability.Probability_Mass_Function

19:14:21 HOL-Probability: theory HOL-Probability.Projective_Family

19:14:22 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure

19:14:22 Timing HOL-Auth (2 threads, 190.988s elapsed time, 304.316s cpu time, 12.524s GC time, factor 1.59)

19:14:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth

19:14:22 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/document.pdf

19:14:22 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/outline.pdf

19:14:22 Finished HOL-Auth (0:03:44 elapsed time, 0:05:54 cpu time, factor 1.57)

19:14:22 Running HOL-Decision_Procs ...

19:14:23 HOL-Probability: theory HOL-Probability.Independent_Family

19:14:23 HOL-Probability: theory HOL-Probability.PMF_Impl

19:14:24 HOL-Probability: theory HOL-Probability.Random_Permutations

19:14:25 HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library

19:14:25 HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions

19:14:25 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order

19:14:25 HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux

19:14:26 HOL-Probability: theory HOL-Probability.SPMF

19:14:26 HOL-Probability: theory HOL-Probability.Convolution

19:14:26 HOL-Probability: theory HOL-Probability.Information

19:14:26 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring

19:14:28 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order_Ex

19:14:28 HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper

19:14:29 HOL-Probability: theory HOL-Probability.Distributions

19:14:30 HOL-Probability: theory HOL-Probability.Projective_Limit

19:14:31 HOL-Probability: theory HOL-Probability.Characteristic_Functions

19:14:32 HOL-Probability: theory HOL-Probability.Sinc_Integral

19:14:32 HOL-Probability: theory HOL-Probability.Stream_Space

19:14:32 HOL-Probability: theory HOL-Probability.Levy

19:14:33 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem

19:14:33 HOL-Probability: theory HOL-Probability.Tree_Space

19:14:34 HOL-Probability: theory HOL-Probability.Probability

19:14:38 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Complete

19:14:38 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflective_Field

19:14:53 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex

19:14:54 HOL-Decision_Procs: theory HOL-Decision_Procs.Ferrack

19:15:25 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2

19:15:29 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3

19:15:57 HOL-Decision_Procs: theory HOL-Decision_Procs.MIR

19:16:48 HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List

19:16:58 HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair

19:16:58 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial

19:17:09 HOL-Decision_Procs: theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff

19:17:41 Timing HOL-Probability (2 threads, 173.914s elapsed time, 317.312s cpu time, 20.452s GC time, factor 1.82)

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

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

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

19:17:41 Finished HOL-Probability (0:03:39 elapsed time, 0:06:22 cpu time, factor 1.74)

19:17:41 Running HOL-Data_Structures ...

19:17:42 HOL-Data_Structures: theory HOL-Data_Structures.Less_False

19:17:42 HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less

19:17:42 HOL-Data_Structures: theory HOL-Data_Structures.Cmp

19:17:42 HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del

19:17:42 HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del

19:17:43 HOL-Data_Structures: theory HOL-Data_Structures.Map_by_Ordered

19:17:43 HOL-Data_Structures: theory HOL-Data_Structures.Tree2

19:17:43 HOL-Data_Structures: theory HOL-Data_Structures.Set_by_Ordered

19:17:43 HOL-Data_Structures: theory HOL-Data_Structures.Tree23

19:17:44 HOL-Data_Structures: theory HOL-Data_Structures.Isin2

19:17:45 HOL-Data_Structures: theory HOL-Data_Structures.AA_Set

19:17:45 HOL-Data_Structures: theory HOL-Data_Structures.Lookup2

19:17:45 HOL-Data_Structures: theory HOL-Data_Structures.RBT

19:17:46 HOL-Data_Structures: theory HOL-Data_Structures.AA_Map

19:17:48 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set

19:17:49 HOL-Data_Structures: theory HOL-Data_Structures.Tree234

19:17:52 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set

19:17:56 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map

19:18:02 HOL-Data_Structures: theory HOL-Library.Cancellation

19:18:03 HOL-Data_Structures: theory HOL-Library.Multiset

19:18:08 HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue

19:18:08 HOL-Data_Structures: theory HOL-Library.Pattern_Aliases

19:18:08 HOL-Data_Structures: theory HOL-Data_Structures.Base_FDS

19:18:08 HOL-Data_Structures: theory HOL-Library.Tree

19:18:11 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set

19:18:12 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map

19:18:12 HOL-Data_Structures: theory HOL-Data_Structures.Binomial_Heap

19:18:16 HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap

19:18:18 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set

19:18:19 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Bounds

19:18:20 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map

19:18:24 HOL-Data_Structures: theory HOL-Data_Structures.Sorting

19:18:26 HOL-Data_Structures: theory HOL-Library.Tree_Real

19:18:26 HOL-Data_Structures: theory HOL-Data_Structures.Balance

19:18:27 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map

19:18:27 HOL-Data_Structures: theory HOL-Number_Theory.Fib

19:18:27 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set

19:18:29 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map

19:18:30 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set

19:18:32 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation

19:19:21 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Ex

19:19:21 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Quickcheck_Ex

19:19:42 HOL-Decision_Procs: theory HOL-Decision_Procs.Decision_Procs

19:20:05 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Map

19:23:45 HOL-Nominal-Examples: theory HOL-Nominal-Examples.VC_Condition

19:23:50 Timing HOL-Nominal-Examples (2 threads, 663.502s elapsed time, 1200.564s cpu time, 125.252s GC time, factor 1.81)

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

19:23:50 Finished HOL-Nominal-Examples (0:11:06 elapsed time, 0:20:02 cpu time, factor 1.81)

19:23:50 Running HOL-Codegenerator_Test ...

19:23:52 HOL-Codegenerator_Test: theory HOL-Data_Structures.Less_False

19:23:52 HOL-Codegenerator_Test: theory HOL-Data_Structures.Cmp

19:23:52 HOL-Codegenerator_Test: theory HOL-Data_Structures.Sorted_Less

19:23:52 HOL-Codegenerator_Test: theory HOL-Data_Structures.AList_Upd_Del

19:23:52 HOL-Codegenerator_Test: theory HOL-Data_Structures.List_Ins_Del

19:23:52 HOL-Codegenerator_Test: theory HOL-Data_Structures.Map_by_Ordered

19:23:53 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_PolyML

19:23:53 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_Scala

19:23:53 HOL-Codegenerator_Test: theory HOL-ex.Records

19:23:53 HOL-Codegenerator_Test: theory HOL-Data_Structures.Set_by_Ordered

19:23:53 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Set

19:23:54 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Map

19:23:59 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Candidates

19:24:02 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate

19:24:08 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Binary_Nat

19:24:58 Timing HOL-Decision_Procs (2 threads, 632.166s elapsed time, 1208.972s cpu time, 100.936s GC time, factor 1.91)

19:24:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Decision_Procs

19:24:58 Finished HOL-Decision_Procs (0:10:35 elapsed time, 0:20:11 cpu time, factor 1.91)

19:24:58 Running HOL-ex ...

19:25:01 HOL-ex: theory HOL-ex.Computations

19:25:01 HOL-ex: theory HOL-ex.Bubblesort

19:25:01 HOL-ex: theory HOL-ex.MergeSort

19:25:02 HOL-ex: theory HOL-ex.Quicksort

19:25:02 HOL-ex: theory HOL-ex.Conditional_Parametricity_Examples

19:25:02 HOL-ex: theory HOL-ex.Datatype_Record_Examples

19:25:03 HOL-ex: theory HOL-ex.IArray_Examples

19:25:03 HOL-ex: theory HOL-ex.Perm_Fragments

19:25:04 HOL-ex: theory HOL-ex.Refute_Examples

19:25:06 HOL-ex: theory HOL-ex.Simps_Case_Conv_Examples

19:25:07 HOL-ex: theory HOL-ex.Radix_Sort

19:25:07 HOL-ex: theory HOL-ex.Transitive_Closure_Table_Ex

19:25:07 HOL-ex: theory HOL-ex.While_Combinator_Example

19:25:07 HOL-ex: theory HOL-ex.Code_Timing

19:25:08 HOL-ex: theory HOL-ex.Adhoc_Overloading_Examples

19:25:09 HOL-ex: theory HOL-ex.Antiquote

19:25:09 HOL-ex: theory HOL-ex.Arith_Examples

19:25:09 HOL-ex: theory HOL-ex.Birthday_Paradox

19:25:09 HOL-ex: theory HOL-ex.CTL

19:25:10 HOL-ex: theory HOL-ex.Cartouche_Examples

19:25:10 HOL-ex: theory HOL-ex.Case_Product

19:25:10 HOL-ex: theory HOL-ex.Chinese

19:25:10 HOL-ex: theory HOL-ex.Classical

19:25:11 HOL-ex: theory HOL-ex.Coercion_Examples

19:25:11 HOL-ex: theory HOL-ex.Coherent

19:25:11 HOL-ex: theory HOL-ex.Commands

19:25:11 HOL-ex: theory HOL-ex.Erdoes_Szekeres

19:25:11 HOL-ex: theory HOL-ex.Executable_Relation

19:25:12 HOL-ex: theory HOL-ex.Execute_Choice

19:25:12 HOL-ex: theory HOL-ex.Functions

19:25:12 HOL-ex: theory HOL-ex.Groebner_Examples

19:25:12 HOL-ex: theory HOL-ex.Guess

19:25:12 HOL-ex: theory HOL-ex.Hebrew

19:25:16 HOL-ex: theory HOL-ex.Hex_Bin_Examples

19:25:16 HOL-ex: theory HOL-ex.Iff_Oracle

19:25:16 HOL-ex: theory HOL-ex.Induction_Schema

19:25:16 HOL-ex: theory HOL-ex.Intuitionistic

19:25:16 HOL-ex: theory HOL-ex.Lagrange

19:25:16 HOL-ex: theory HOL-ex.List_to_Set_Comprehension_Examples

19:25:16 HOL-ex: theory HOL-ex.LocaleTest2

19:25:17 HOL-ex: theory HOL-ex.ML

19:25:20 HOL-ex: theory HOL-ex.MonoidGroup

19:25:21 HOL-ex: theory HOL-ex.Multiquote

19:25:21 HOL-ex: theory HOL-ex.NatSum

19:25:21 HOL-ex: theory HOL-ex.PER

19:25:21 HOL-ex: theory HOL-ex.Peano_Axioms

19:25:21 HOL-ex: theory HOL-ex.PresburgerEx

19:25:22 HOL-ex: theory HOL-ex.Primrec

19:25:22 HOL-ex: theory HOL-ex.Records

19:25:22 HOL-ex: theory HOL-ex.Rewrite_Examples

19:25:22 HOL-ex: theory HOL-ex.Seq

19:25:23 HOL-ex: theory HOL-ex.Serbian

19:25:28 HOL-ex: theory HOL-ex.Set_Comprehension_Pointfree_Examples

19:25:28 HOL-ex: theory HOL-ex.Set_Theory

19:25:29 HOL-ex: theory HOL-ex.Simproc_Tests

19:25:33 HOL-ex: theory HOL-ex.Sudoku

19:25:34 HOL-ex: theory HOL-ex.Tarski

19:25:35 HOL-ex: theory HOL-ex.Termination

19:25:36 HOL-ex: theory HOL-ex.ThreeDivides

19:25:36 HOL-ex: theory HOL-ex.Transfer_Int_Nat

19:25:36 HOL-ex: theory HOL-ex.Tree23

19:25:45 HOL-ex: theory HOL-ex.Unification

19:25:47 HOL-ex: theory HOL-ex.Word_Type

19:25:50 HOL-ex: theory HOL-ex.veriT_Preprocessing

19:25:51 HOL-ex: theory HOL-ex.Transfer_Debug

19:25:51 HOL-ex: theory HOL-ex.Function_Growth

19:25:51 HOL-ex: theory HOL-ex.SOS

19:25:52 HOL-ex: theory HOL-ex.SOS_Cert

19:25:52 HOL-ex: theory HOL-ex.Argo_Examples

19:25:55 HOL-ex: theory HOL-ex.Ballot

19:25:56 HOL-ex: theory HOL-ex.BinEx

19:25:57 HOL-ex: theory HOL-ex.Code_Binary_Nat_examples

19:25:57 HOL-ex: theory HOL-ex.Cubic_Quartic

19:25:57 HOL-ex: theory HOL-ex.Dedekind_Real

19:25:58 HOL-ex: theory HOL-ex.Eval_Examples

19:26:01 HOL-ex: theory HOL-ex.Gauge_Integration

19:26:01 HOL-ex: theory HOL-ex.HarmonicSeries

19:26:02 HOL-ex: theory HOL-ex.Normalization_by_Evaluation

19:26:02 HOL-ex: theory HOL-ex.Parallel_Example

19:26:03 HOL-ex: theory HOL-ex.Pythagoras

19:26:03 HOL-ex: theory HOL-ex.Reflection_Examples

19:26:21 HOL-ex: theory HOL-ex.Sqrt

19:26:23 HOL-ex: theory HOL-ex.Sqrt_Script

19:26:24 HOL-ex: theory HOL-ex.Sum_of_Powers

19:27:04 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Efficient_Datastructures

19:27:14 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Pretty_Char

19:27:47 Timing HOL-Data_Structures (2 threads, 599.669s elapsed time, 888.852s cpu time, 26.032s GC time, factor 1.48)

19:27:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures

19:27:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures/document.pdf

19:27:47 Finished HOL-Data_Structures (0:10:06 elapsed time, 0:14:55 cpu time, factor 1.48)

19:27:47 Running HOL-Corec_Examples ...

19:27:48 HOL-Corec_Examples: theory HOL-Corec_Examples.Iterate_GPV

19:27:48 HOL-Corec_Examples: theory HOL-Corec_Examples.LFilter

19:27:52 HOL-Corec_Examples: theory HOL-Corec_Examples.Simple_Nesting

19:28:02 HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Processor

19:28:17 HOL-Corec_Examples: theory HOL-Corec_Examples.Paper_Examples

19:29:14 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_A

19:29:14 HOL-Corec_Examples: theory HOL-Corec_Examples.GPV_Bare_Bones

19:29:20 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_B

19:29:24 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_C

19:29:27 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_Poly

19:29:31 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_D

19:29:48 HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Mono

19:30:24 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Target_Nat

19:30:47 HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Poly

19:32:01 HOL-Corec_Examples: theory HOL-Corec_Examples.Small_Concrete

19:32:34 HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Friends

19:32:43 HOL-Corec_Examples: theory HOL-Corec_Examples.TLList_Friends

19:33:05 HOL-Corec_Examples: theory HOL-Corec_Examples.Type_Class

19:33:13 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_GHC

19:33:15 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_MLton

19:33:19 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_OCaml

19:33:19 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_SMLNJ

19:33:21 Timing HOL-Codegenerator_Test (2 threads, 568.243s elapsed time, 480.996s cpu time, 19.352s GC time, factor 0.85)

19:33:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Codegenerator_Test

19:33:21 Finished HOL-Codegenerator_Test (0:09:31 elapsed time, 0:21:03 cpu time, factor 2.21)

19:33:21 Running HOL-Nitpick_Examples ...

19:33:23 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Datatype_Nits

19:33:23 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Core_Nits

19:33:24 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Hotel_Nits

19:33:24 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Induct_Nits

19:33:25 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Integer_Nits

19:33:25 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Mini_Nits

19:33:26 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Mono_Nits

19:33:27 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Pattern_Nits

19:33:28 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Record_Nits

19:33:29 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Refute_Nits

19:33:30 HOL-ex: theory HOL-ex.Meson_Test

19:33:30 HOL-ex: theory HOL-ex.SAT_Examples

19:33:35 Timing HOL-Corec_Examples (2 threads, 345.089s elapsed time, 607.800s cpu time, 65.832s GC time, factor 1.76)

19:33:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Corec_Examples

19:33:35 Finished HOL-Corec_Examples (0:05:47 elapsed time, 0:10:10 cpu time, factor 1.75)

19:33:35 Running HOL-Hoare_Parallel ...

19:33:36 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Graph

19:33:36 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Com

19:33:36 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Quote_Antiquote

19:33:37 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Com

19:33:38 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Tran

19:33:39 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tran

19:33:41 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Special_Nits

19:33:41 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Hoare

19:33:41 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Tests_Nits

19:33:41 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Hoare

19:33:42 Timing HOL-ex (2 threads, 519.659s elapsed time, 893.216s cpu time, 37.052s GC time, factor 1.72)

19:33:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex

19:33:42 Finished HOL-ex (0:08:42 elapsed time, 0:15:24 cpu time, factor 1.77)

19:33:42 Running HOL-Datatype_Examples ...

19:33:42 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Manual_Nits

19:33:42 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Syntax

19:33:42 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tactics

19:33:42 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Examples

19:33:43 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Syntax

19:33:43 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Gar_Coll

19:33:43 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lift_BNF

19:33:43 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Compat

19:33:45 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Mul_Gar_Coll

19:33:45 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Examples

19:33:47 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Milner_Tofte

19:33:48 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Typedef_Nits

19:33:49 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Hoare_Parallel

19:33:50 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFI

19:33:51 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Koenig

19:33:51 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Process

19:33:56 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Stream_Processor

19:34:01 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lambda_Term

19:34:01 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Nitpick_Examples

19:34:04 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Codatatype

19:34:11 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Datatype

19:35:22 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primcorec

19:35:25 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Prelim

19:35:25 HOL-Datatype_Examples: theory HOL-Datatype_Examples.DTree

19:35:26 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Gram_Lang

19:35:27 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Parallel_Composition

19:35:28 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFsetI

19:35:49 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primrec

19:36:40 Timing HOL-Hoare_Parallel (2 threads, 178.127s elapsed time, 308.368s cpu time, 4.852s GC time, factor 1.73)

19:36:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel

19:36:40 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/document.pdf

19:36:40 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/outline.pdf

19:36:40 Finished HOL-Hoare_Parallel (0:03:05 elapsed time, 0:05:18 cpu time, factor 1.72)

19:36:40 Running HOL-MicroJava ...

19:36:42 HOL-MicroJava: theory HOL-Eisbach.Eisbach

19:36:42 HOL-MicroJava: theory HOL-MicroJava.Semilat

19:36:42 HOL-MicroJava: theory HOL-MicroJava.Err

19:36:43 HOL-MicroJava: theory HOL-MicroJava.JBasis

19:36:43 HOL-MicroJava: theory HOL-MicroJava.AuxLemmas

19:36:43 HOL-MicroJava: theory HOL-MicroJava.Type

19:36:44 HOL-MicroJava: theory HOL-MicroJava.Listn

19:36:44 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework

19:36:44 HOL-MicroJava: theory HOL-MicroJava.Opt

19:36:44 HOL-MicroJava: theory HOL-MicroJava.Product

19:36:44 Timing HOL-Datatype_Examples (2 threads, 179.931s elapsed time, 326.504s cpu time, 40.740s GC time, factor 1.81)

19:36:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Datatype_Examples

19:36:44 Finished HOL-Datatype_Examples (0:03:02 elapsed time, 0:05:28 cpu time, factor 1.80)

19:36:44 Running HOL-IMP ...

19:36:44 HOL-MicroJava: theory HOL-MicroJava.SemilatAlg

19:36:45 HOL-MicroJava: theory HOL-MicroJava.Kildall

19:36:45 HOL-MicroJava: theory HOL-MicroJava.LBVSpec

19:36:46 HOL-MicroJava: theory HOL-MicroJava.Decl

19:36:46 HOL-MicroJava: theory HOL-MicroJava.SystemClasses

19:36:46 HOL-MicroJava: theory HOL-MicroJava.TypeRel

19:36:46 HOL-IMP: theory HOL-IMP.AExp

19:36:46 HOL-IMP: theory HOL-IMP.C_like

19:36:46 HOL-MicroJava: theory HOL-MicroJava.Value

19:36:47 HOL-MicroJava: theory HOL-MicroJava.WellForm

19:36:47 HOL-MicroJava: theory HOL-MicroJava.State

19:36:47 HOL-IMP: theory HOL-IMP.ASM

19:36:48 HOL-MicroJava: theory HOL-MicroJava.Exceptions

19:36:48 HOL-MicroJava: theory HOL-MicroJava.Term

19:36:48 HOL-MicroJava: theory HOL-MicroJava.LBVComplete

19:36:48 HOL-MicroJava: theory HOL-MicroJava.LBVCorrect

19:36:48 HOL-IMP: theory HOL-IMP.BExp

19:36:49 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_err

19:36:49 HOL-MicroJava: theory HOL-MicroJava.Abstract_BV

19:36:49 HOL-MicroJava: theory HOL-MicroJava.Semilattices

19:36:50 HOL-MicroJava: theory HOL-MicroJava.JType

19:36:50 HOL-MicroJava: theory HOL-MicroJava.JVMType

19:36:50 HOL-IMP: theory HOL-IMP.Complete_Lattice

19:36:50 HOL-IMP: theory HOL-IMP.OO

19:36:51 HOL-IMP: theory HOL-IMP.Com

19:36:52 HOL-IMP: theory HOL-IMP.ACom

19:36:52 HOL-MicroJava: theory HOL-MicroJava.WellType

19:36:53 HOL-MicroJava: theory HOL-MicroJava.Conform

19:36:53 HOL-MicroJava: theory HOL-MicroJava.JVMState

19:36:53 HOL-MicroJava: theory HOL-MicroJava.JVMInstructions

19:36:54 HOL-MicroJava: theory HOL-MicroJava.Eval

19:36:55 HOL-MicroJava: theory HOL-MicroJava.JVMExceptions

19:36:55 HOL-IMP: theory HOL-IMP.Abs_Int_Tests

19:36:55 HOL-MicroJava: theory HOL-MicroJava.JVMExecInstr

19:36:55 HOL-IMP: theory HOL-IMP.Big_Step

19:36:56 HOL-MicroJava: theory HOL-MicroJava.JVMExec

19:36:56 HOL-IMP: theory HOL-IMP.Denotational

19:36:56 HOL-MicroJava: theory HOL-MicroJava.DefsComp

19:36:56 HOL-IMP: theory HOL-IMP.Hoare

19:36:56 HOL-MicroJava: theory HOL-MicroJava.Index

19:36:57 HOL-IMP: theory HOL-IMP.Hoare_Examples

19:36:57 HOL-IMP: theory HOL-IMP.Hoare_Total

19:36:57 HOL-IMP: theory HOL-IMP.Hoare_Sound_Complete

19:36:57 HOL-IMP: theory HOL-IMP.Hoare_Total_EX

19:36:57 HOL-MicroJava: theory HOL-MicroJava.JVMDefensive

19:36:57 HOL-IMP: theory HOL-IMP.VCG_Total_EX

19:36:58 HOL-MicroJava: theory HOL-MicroJava.JVMListExample

19:36:59 HOL-MicroJava: theory HOL-MicroJava.Example

19:36:59 HOL-MicroJava: theory HOL-MicroJava.JListExample

19:36:59 HOL-IMP: theory HOL-IMP.Hoare_Total_EX2

19:36:59 HOL-IMP: theory HOL-IMP.VCG_Total_EX2

19:37:01 HOL-IMP: theory HOL-IMP.VCG

19:37:01 HOL-MicroJava: theory HOL-MicroJava.JTypeSafe

19:37:02 HOL-MicroJava: theory HOL-MicroJava.TypeInf

19:37:02 HOL-MicroJava: theory HOL-MicroJava.Effect

19:37:02 HOL-IMP: theory HOL-IMP.Sec_Type_Expr

19:37:02 HOL-MicroJava: theory HOL-MicroJava.TranslCompTp

19:37:02 HOL-IMP: theory HOL-IMP.Sem_Equiv

19:37:02 HOL-IMP: theory HOL-IMP.Sec_Typing

19:37:02 HOL-IMP: theory HOL-IMP.Sec_TypingT

19:37:03 HOL-IMP: theory HOL-IMP.Vars

19:37:03 HOL-IMP: theory HOL-IMP.Procs

19:37:03 HOL-MicroJava: theory HOL-MicroJava.TranslComp

19:37:03 HOL-MicroJava: theory HOL-MicroJava.LemmasComp

19:37:04 HOL-IMP: theory HOL-IMP.Def_Init

19:37:04 HOL-IMP: theory HOL-IMP.Def_Init_Exp

19:37:04 HOL-MicroJava: theory HOL-MicroJava.CorrComp

19:37:04 HOL-IMP: theory HOL-IMP.Def_Init_Big

19:37:04 HOL-IMP: theory HOL-IMP.Fold

19:37:05 HOL-IMP: theory HOL-IMP.Live

19:37:05 HOL-IMP: theory HOL-IMP.Procs_Dyn_Vars_Dyn

19:37:05 HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Dyn

19:37:05 HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Stat

19:37:07 HOL-IMP: theory HOL-IMP.Collecting

19:37:07 HOL-IMP: theory HOL-IMP.Collecting1

19:37:08 HOL-IMP: theory HOL-IMP.Collecting_Examples

19:37:08 HOL-IMP: theory HOL-IMP.Star

19:37:08 HOL-IMP: theory HOL-IMP.Compiler

19:37:12 HOL-IMP: theory HOL-IMP.Def_Init_Small

19:37:12 HOL-IMP: theory HOL-IMP.Small_Step

19:37:13 HOL-IMP: theory HOL-IMP.Compiler2

19:37:13 HOL-IMP: theory HOL-IMP.Finite_Reachable

19:37:13 HOL-IMP: theory HOL-IMP.Abs_Int_init

19:37:13 HOL-IMP: theory HOL-IMP.Live_True

19:37:14 HOL-IMP: theory HOL-IMP.Abs_Int0

19:37:14 HOL-IMP: theory HOL-IMP.Types

19:37:16 HOL-IMP: theory HOL-IMP.Abs_State

19:37:17 HOL-IMP: theory HOL-IMP.Abs_Int1

19:37:18 HOL-IMP: theory HOL-IMP.Abs_Int1_const

19:37:19 HOL-IMP: theory HOL-IMP.Abs_Int1_parity

19:37:19 HOL-IMP: theory HOL-IMP.Abs_Int2

19:37:20 HOL-IMP: theory HOL-IMP.Poly_Types

19:37:21 HOL-IMP: theory HOL-IMP.Abs_Int2_ivl

19:37:23 HOL-IMP: theory HOL-IMP.Abs_Int3

19:37:26 HOL-MicroJava: theory HOL-MicroJava.BVSpec

19:37:27 HOL-MicroJava: theory HOL-MicroJava.Altern

19:37:27 HOL-MicroJava: theory HOL-MicroJava.Correct

19:37:27 HOL-MicroJava: theory HOL-MicroJava.EffectMono

19:37:27 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_JVM

19:37:27 HOL-MicroJava: theory HOL-MicroJava.BVSpecTypeSafe

19:37:28 HOL-MicroJava: theory HOL-MicroJava.JVM

19:37:28 HOL-MicroJava: theory HOL-MicroJava.CorrCompTp

19:37:28 HOL-MicroJava: theory HOL-MicroJava.BVNoTypeError

19:37:29 HOL-MicroJava: theory HOL-MicroJava.BVExample

19:37:30 HOL-MicroJava: theory HOL-MicroJava.LBVJVM

19:37:30 HOL-MicroJava: theory HOL-MicroJava.MicroJava

19:38:17 Timing HOL-Nitpick_Examples (2 threads, 292.444s elapsed time, 145.368s cpu time, 2.860s GC time, factor 0.50)

19:38:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nitpick_Examples

19:38:17 Finished HOL-Nitpick_Examples (0:04:54 elapsed time, 0:11:03 cpu time, factor 2.25)

19:38:17 Running HOL-Proofs-Lambda ...

19:38:18 HOL-Proofs-Lambda: theory HOL-Library.Code_Target_Int

19:38:18 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Commutation

19:38:18 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Lambda

19:38:18 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListOrder

19:38:21 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListApplication

19:38:22 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.LambdaType

19:38:23 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ParRed

19:38:24 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListBeta

19:38:24 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Eta

19:38:25 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.InductTermi

19:38:26 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.StrongNorm

19:38:27 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.NormalForm

19:38:28 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Standardization

19:38:28 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.WeakNorm

19:39:42 Timing HOL-IMP (2 threads, 169.875s elapsed time, 290.560s cpu time, 16.332s GC time, factor 1.71)

19:39:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP

19:39:42 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP/document.pdf

19:39:42 Finished HOL-IMP (0:02:57 elapsed time, 0:04:59 cpu time, factor 1.69)

19:39:42 Running HOL-Quickcheck_Examples ...

19:39:43 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Completeness

19:39:43 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Interfaces

19:39:43 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples

19:39:43 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting

19:39:44 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Examples

19:39:44 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting_Example

19:39:44 Timing HOL-MicroJava (2 threads, 176.476s elapsed time, 297.360s cpu time, 11.908s GC time, factor 1.68)

19:39:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava

19:39:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/document.pdf

19:39:44 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/outline.pdf

19:39:44 Finished HOL-MicroJava (0:03:03 elapsed time, 0:05:09 cpu time, factor 1.68)

19:39:44 Running HOL-Bali ...

19:39:46 HOL-Bali: theory HOL-Bali.Basis

19:39:47 HOL-Bali: theory HOL-Bali.Name

19:39:47 HOL-Bali: theory HOL-Bali.Table

19:39:49 HOL-Bali: theory HOL-Bali.Type

19:39:51 HOL-Bali: theory HOL-Bali.Value

19:39:52 HOL-Bali: theory HOL-Bali.Term

19:40:14 HOL-Bali: theory HOL-Bali.Decl

19:40:19 HOL-Bali: theory HOL-Bali.TypeRel

19:40:20 HOL-Bali: theory HOL-Bali.DeclConcepts

19:40:22 HOL-Bali: theory HOL-Bali.State

19:40:22 HOL-Bali: theory HOL-Bali.WellType

19:40:24 HOL-Bali: theory HOL-Bali.Conform

19:40:25 HOL-Bali: theory HOL-Bali.Eval

19:40:27 HOL-Bali: theory HOL-Bali.DefiniteAssignment

19:40:34 HOL-Bali: theory HOL-Bali.WellForm

19:40:35 HOL-Bali: theory HOL-Bali.DefiniteAssignmentCorrect

19:40:36 HOL-Bali: theory HOL-Bali.Example

19:40:37 HOL-Bali: theory HOL-Bali.TypeSafe

19:40:39 HOL-Bali: theory HOL-Bali.Evaln

19:40:42 HOL-Bali: theory HOL-Bali.AxSem

19:40:42 HOL-Bali: theory HOL-Bali.Trans

19:40:46 HOL-Bali: theory HOL-Bali.AxCompl

19:40:46 HOL-Bali: theory HOL-Bali.AxSound

19:40:47 HOL-Bali: theory HOL-Bali.AxExample

19:40:53 Timing HOL-Proofs-Lambda (2 threads, 149.985s elapsed time, 175.392s cpu time, 7.100s GC time, factor 1.17)

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

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

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

19:40:53 Finished HOL-Proofs-Lambda (0:02:36 elapsed time, 0:03:05 cpu time, factor 1.18)

19:40:53 Running HOL-Predicate_Compile_Examples ...

19:40:55 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_1

19:40:55 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_2

19:40:55 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Hotel_Example

19:40:55 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Narrowing_Examples

19:40:56 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_3

19:40:56 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_4

19:40:57 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Quickcheck_Examples

19:40:57 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Tests

19:41:03 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Examples

19:41:20 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Specialisation_Examples

19:42:15 Timing HOL-Quickcheck_Examples (2 threads, 150.518s elapsed time, 168.036s cpu time, 6.292s GC time, factor 1.12)

19:42:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quickcheck_Examples

19:42:15 Finished HOL-Quickcheck_Examples (0:02:32 elapsed time, 0:04:26 cpu time, factor 1.75)

19:42:15 Running HOL-Proofs-Extraction ...

19:42:16 HOL-Proofs-Extraction: theory HOL-Library.Code_Abstract_Nat

19:42:16 HOL-Proofs-Extraction: theory HOL-Library.Cancellation

19:42:16 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Nat

19:42:17 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Int

19:42:17 HOL-Proofs-Extraction: theory HOL-Library.Multiset

19:42:17 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Numeral

19:42:18 HOL-Proofs-Extraction: theory HOL-Library.Open_State_Syntax

19:42:18 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Warshall

19:42:22 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman

19:42:23 Timing HOL-Bali (2 threads, 143.253s elapsed time, 233.752s cpu time, 15.632s GC time, factor 1.63)

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

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

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

19:42:23 Finished HOL-Bali (0:02:38 elapsed time, 0:04:16 cpu time, factor 1.62)

19:42:23 Running HOL-Imperative_HOL ...

19:42:24 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman_Extraction

19:42:24 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Sorted_List

19:42:24 HOL-Imperative_HOL: theory HOL-Imperative_HOL.List_Sublist

19:42:25 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap

19:42:27 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad

19:42:29 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Array

19:42:30 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Ref

19:42:30 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL

19:42:31 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Linked_Lists

19:42:32 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Overview

19:42:32 HOL-Imperative_HOL: theory HOL-Imperative_HOL.SatChecker

19:42:40 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Context_Free_Grammar_Example

19:42:40 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Code_Prolog_Examples

19:42:41 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Lambda_Example

19:42:43 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example

19:42:43 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.List_Examples

19:42:44 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Subarray

19:42:45 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Factorial_Ring

19:42:45 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort

19:42:46 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Util

19:42:46 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Pigeonhole

19:42:47 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example_Prolog

19:42:52 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Reg_Exp_Example

19:42:58 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Euclidean_Algorithm

19:43:00 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse

19:43:03 Timing HOL-Predicate_Compile_Examples (2 threads, 127.302s elapsed time, 200.136s cpu time, 13.076s GC time, factor 1.57)

19:43:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Predicate_Compile_Examples

19:43:03 Finished HOL-Predicate_Compile_Examples (0:02:09 elapsed time, 0:04:54 cpu time, factor 2.27)

19:43:03 Running HOL-Word-SMT_Examples ...

19:43:04 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.Boogie

19:43:04 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Word_Examples

19:43:04 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Examples

19:43:05 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Tests

19:43:10 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Primes

19:43:22 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Euclid

19:43:29 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.QuotRem

19:43:30 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL_ex

19:43:33 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Greatest_Common_Divisor

19:44:02 Timing HOL-Imperative_HOL (2 threads, 93.724s elapsed time, 74.972s cpu time, 2.476s GC time, factor 0.80)

19:44:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL

19:44:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/document.pdf

19:44:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/outline.pdf

19:44:02 Finished HOL-Imperative_HOL (0:01:38 elapsed time, 0:04:10 cpu time, factor 2.54)

19:44:02 Running HOL-UNITY ...

19:44:03 HOL-UNITY: theory HOL-UNITY.ListOrder

19:44:03 HOL-UNITY: theory HOL-UNITY.UNITY

19:44:04 HOL-UNITY: theory HOL-UNITY.Constrains

19:44:04 HOL-UNITY: theory HOL-UNITY.Deadlock

19:44:04 HOL-UNITY: theory HOL-UNITY.FP

19:44:04 HOL-UNITY: theory HOL-UNITY.Network

19:44:05 HOL-UNITY: theory HOL-UNITY.WFair

19:44:06 HOL-UNITY: theory HOL-UNITY.SubstAx

19:44:06 HOL-UNITY: theory HOL-UNITY.Token

19:44:06 HOL-UNITY: theory HOL-UNITY.Detects

19:44:06 HOL-UNITY: theory HOL-UNITY.Follows

19:44:07 HOL-UNITY: theory HOL-UNITY.Union

19:44:07 HOL-UNITY: theory HOL-UNITY.Comp

19:44:08 HOL-UNITY: theory HOL-UNITY.Guar

19:44:08 HOL-UNITY: theory HOL-UNITY.Transformers

19:44:08 HOL-UNITY: theory HOL-UNITY.Extend

19:44:09 HOL-UNITY: theory HOL-UNITY.ProgressSets

19:44:10 HOL-UNITY: theory HOL-UNITY.Project

19:44:10 HOL-UNITY: theory HOL-UNITY.Rename

19:44:10 HOL-UNITY: theory HOL-UNITY.Lift_prog

19:44:10 HOL-UNITY: theory HOL-UNITY.ELT

19:44:10 HOL-UNITY: theory HOL-UNITY.PPROD

19:44:10 HOL-UNITY: theory HOL-UNITY.UNITY_Main

19:44:10 Timing HOL-Proofs-Extraction (2 threads, 110.529s elapsed time, 200.700s cpu time, 12.588s GC time, factor 1.82)

19:44:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction

19:44:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/document.pdf

19:44:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/outline.pdf

19:44:10 Finished HOL-Proofs-Extraction (0:01:55 elapsed time, 0:03:28 cpu time, factor 1.81)

19:44:10 Running HOL-SET_Protocol ...

19:44:11 HOL-UNITY: theory HOL-UNITY.AllocBase

19:44:11 HOL-UNITY: theory HOL-UNITY.Channel

19:44:11 HOL-UNITY: theory HOL-UNITY.Common

19:44:11 HOL-UNITY: theory HOL-UNITY.Counter

19:44:11 HOL-UNITY: theory HOL-UNITY.Alloc

19:44:12 HOL-SET_Protocol: theory HOL-SET_Protocol.Message_SET

19:44:12 HOL-UNITY: theory HOL-UNITY.AllocImpl

19:44:14 HOL-UNITY: theory HOL-UNITY.Client

19:44:15 HOL-SET_Protocol: theory HOL-SET_Protocol.Event_SET

19:44:15 HOL-UNITY: theory HOL-UNITY.Counterc

19:44:15 HOL-UNITY: theory HOL-UNITY.Handshake

19:44:15 HOL-UNITY: theory HOL-UNITY.Lift

19:44:16 HOL-SET_Protocol: theory HOL-SET_Protocol.Public_SET

19:44:16 HOL-UNITY: theory HOL-UNITY.Mutex

19:44:16 HOL-UNITY: theory HOL-UNITY.NSP_Bad

19:44:16 HOL-SET_Protocol: theory HOL-SET_Protocol.Cardholder_Registration

19:44:16 HOL-SET_Protocol: theory HOL-SET_Protocol.Merchant_Registration

19:44:17 HOL-UNITY: theory HOL-UNITY.PriorityAux

19:44:17 HOL-UNITY: theory HOL-UNITY.Priority

19:44:17 HOL-UNITY: theory HOL-UNITY.Progress

19:44:17 HOL-UNITY: theory HOL-UNITY.Reach

19:44:17 HOL-UNITY: theory HOL-UNITY.TimerArray

19:44:17 HOL-UNITY: theory HOL-UNITY.Reachability

19:44:18 HOL-SET_Protocol: theory HOL-SET_Protocol.Purchase

19:44:19 Timing HOL-Word-SMT_Examples (2 threads, 73.507s elapsed time, 93.076s cpu time, 0.900s GC time, factor 1.27)

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

19:44:19 Finished HOL-Word-SMT_Examples (0:01:15 elapsed time, 0:01:36 cpu time, factor 1.28)

19:44:19 Running Corec ...

19:44:20 HOL-SET_Protocol: theory HOL-SET_Protocol.SET_Protocol

19:44:20 Corec: theory Datatypes.Setup

19:44:20 Corec: theory Corec.Corec

19:45:16 Timing HOL-SET_Protocol (2 threads, 59.821s elapsed time, 97.916s cpu time, 2.952s GC time, factor 1.64)

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

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

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

19:45:16 Finished HOL-SET_Protocol (0:01:05 elapsed time, 0:01:46 cpu time, factor 1.64)

19:45:16 Running Datatypes ...

19:45:17 Datatypes: theory Datatypes.Setup

19:45:18 Datatypes: theory Datatypes.Datatypes

19:45:20 Timing HOL-UNITY (2 threads, 71.218s elapsed time, 107.264s cpu time, 8.384s GC time, factor 1.51)

19:45:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY

19:45:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/document.pdf

19:45:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/outline.pdf

19:45:20 Finished HOL-UNITY (0:01:18 elapsed time, 0:01:58 cpu time, factor 1.52)

19:45:20 Running HOL-Probability-ex ...

19:45:22 HOL-Probability-ex: theory HOL-Library.Permutation

19:45:22 HOL-Probability-ex: theory HOL-Probability-ex.Dining_Cryptographers

19:45:22 HOL-Probability-ex: theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure

19:45:22 HOL-Probability-ex: theory HOL-Probability-ex.Measure_Not_CCC

19:45:23 Timing Corec (2 threads, 57.775s elapsed time, 84.004s cpu time, 5.728s GC time, factor 1.45)

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

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

19:45:23 Finished Corec (0:01:03 elapsed time, 0:01:30 cpu time, factor 1.42)

19:45:23 Running HOL-Metis_Examples ...

19:45:24 HOL-Metis_Examples: theory HOL-Metis_Examples.Abstraction

19:45:24 HOL-Metis_Examples: theory HOL-Decision_Procs.Dense_Linear_Order

19:45:24 HOL-Metis_Examples: theory HOL-Metis_Examples.Binary_Tree

19:45:25 HOL-Metis_Examples: theory HOL-Metis_Examples.Message

19:45:27 HOL-Metis_Examples: theory HOL-Metis_Examples.Big_O

19:45:28 HOL-Metis_Examples: theory HOL-Metis_Examples.Sets

19:45:28 HOL-Metis_Examples: theory HOL-Metis_Examples.Tarski

19:45:28 HOL-Metis_Examples: theory HOL-Metis_Examples.Trans_Closure

19:45:29 HOL-Metis_Examples: theory HOL-Metis_Examples.Type_Encodings

19:45:30 HOL-Metis_Examples: theory HOL-Metis_Examples.Proxies

19:45:30 HOL-Metis_Examples: theory HOL-Metis_Examples.Clausification

19:46:07 Timing HOL-Metis_Examples (2 threads, 42.289s elapsed time, 64.568s cpu time, 3.260s GC time, factor 1.53)

19:46:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Metis_Examples

19:46:07 Finished HOL-Metis_Examples (0:00:44 elapsed time, 0:01:22 cpu time, factor 1.85)

19:46:07 Timing HOL-Probability-ex (2 threads, 44.604s elapsed time, 54.308s cpu time, 1.768s GC time, factor 1.22)

19:46:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability-ex

19:46:07 Finished HOL-Probability-ex (0:00:47 elapsed time, 0:00:56 cpu time, factor 1.20)

19:46:07 Running HOL-Analysis-ex ...

19:46:07 Running HOL-Quotient_Examples ...

19:46:09 HOL-Analysis-ex: theory HOL-Analysis-ex.Approximations

19:46:09 HOL-Quotient_Examples: theory HOL-Quotient_Examples.DList

19:46:09 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Int

19:46:10 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_FSet

19:46:10 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Int_Pow

19:46:10 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_DList

19:46:11 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_FSet

19:46:11 Timing Datatypes (2 threads, 48.696s elapsed time, 68.804s cpu time, 5.292s GC time, factor 1.41)

19:46:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes

19:46:11 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes/datatypes.pdf

19:46:11 Finished Datatypes (0:00:54 elapsed time, 0:01:15 cpu time, factor 1.38)

19:46:11 Running Tutorial ...

19:46:12 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Fun

19:46:12 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Set

19:46:12 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lifting_Code_Dt_Test

19:46:12 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Message

19:46:12 Tutorial: theory Tutorial.ToyList_Test

19:46:13 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Rat

19:46:13 Tutorial: theory Tutorial.AB

19:46:13 Tutorial: theory Tutorial.ABexpr

19:46:14 Tutorial: theory Tutorial.AdvancedInd

19:46:14 Tutorial: theory Tutorial.Base

19:46:14 Tutorial: theory Tutorial.CTL

19:46:16 Tutorial: theory Tutorial.CTLind

19:46:16 Tutorial: theory Tutorial.PDL

19:46:16 Tutorial: theory Tutorial.CodeGen

19:46:17 Tutorial: theory Tutorial.Nested

19:46:19 Tutorial: theory Tutorial.Even

19:46:19 Tutorial: theory Tutorial.Advanced

19:46:19 Tutorial: theory Tutorial.Fundata

19:46:20 Tutorial: theory Tutorial.Ifexpr

19:46:21 Tutorial: theory Tutorial.Itrev

19:46:22 Tutorial: theory Tutorial.Mutual

19:46:22 Tutorial: theory Tutorial.Option2

19:46:23 Tutorial: theory Tutorial.Plus

19:46:23 Tutorial: theory Tutorial.Star

19:46:23 Tutorial: theory Tutorial.ToyList

19:46:23 Tutorial: theory Tutorial.Tree

19:46:24 Tutorial: theory Tutorial.Trie

19:46:24 Tutorial: theory Tutorial.Tree2

19:46:24 Tutorial: theory Tutorial.appendix

19:46:24 Tutorial: theory Tutorial.case_exprs

19:46:24 Tutorial: theory Tutorial.fakenat

19:46:25 Tutorial: theory Tutorial.fun0

19:46:26 Tutorial: theory Tutorial.natsum

19:46:26 Tutorial: theory Tutorial.pairs2

19:46:26 Tutorial: theory Tutorial.prime_def

19:46:26 Tutorial: theory Tutorial.simp

19:46:26 Tutorial: theory Tutorial.simp2

19:46:26 Tutorial: theory Tutorial.types

19:46:26 Tutorial: theory Tutorial.unfoldnested

19:46:40 Tutorial: theory Tutorial.Documents

19:46:40 Tutorial: theory Tutorial.Message

19:46:43 Tutorial: theory Tutorial.Event

19:46:44 Tutorial: theory Tutorial.Public

19:46:44 Tutorial: theory Tutorial.NS_Public

19:46:45 Tutorial: theory Tutorial.Setup

19:46:45 Tutorial: theory Tutorial.Numbers

19:46:45 Tutorial: theory Tutorial.Basic

19:46:45 Tutorial: theory Tutorial.Blast

19:46:45 Tutorial: theory Tutorial.Force

19:46:45 Tutorial: theory Tutorial.Pairs

19:46:46 Tutorial: theory Tutorial.Records

19:46:46 Tutorial: theory Tutorial.Overloading

19:46:46 Tutorial: theory Tutorial.Axioms

19:46:46 Tutorial: theory Tutorial.Typedefs

19:46:47 Tutorial: theory Tutorial.Examples

19:46:47 Tutorial: theory Tutorial.Functions

19:46:47 Tutorial: theory Tutorial.Recur

19:46:47 Tutorial: theory Tutorial.Relations

19:46:47 Tutorial: theory Tutorial.TPrimes

19:46:47 Tutorial: theory Tutorial.Tacticals

19:46:48 Tutorial: theory Tutorial.find2

19:46:48 Tutorial: theory Tutorial.Forward

19:46:51 Timing HOL-Quotient_Examples (2 threads, 40.878s elapsed time, 49.112s cpu time, 3.736s GC time, factor 1.20)

19:46:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quotient_Examples

19:46:51 Finished HOL-Quotient_Examples (0:00:44 elapsed time, 0:01:28 cpu time, factor 2.00)

19:46:51 Running HOL-Hoare ...

19:46:52 HOL-Hoare: theory HOL-Hoare.Heap

19:46:52 HOL-Hoare: theory HOL-Hoare.Arith2

19:46:52 HOL-Hoare: theory HOL-Hoare.Hoare_Logic

19:46:53 Timing HOL-Analysis-ex (2 threads, 43.193s elapsed time, 53.440s cpu time, 0.616s GC time, factor 1.24)

19:46:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis-ex

19:46:53 Finished HOL-Analysis-ex (0:00:45 elapsed time, 0:00:55 cpu time, factor 1.22)

19:46:53 Running HOL-Cardinals ...

19:46:53 HOL-Hoare: theory HOL-Hoare.Hoare_Logic_Abort

19:46:54 HOL-Hoare: theory HOL-Hoare.Examples

19:46:54 HOL-Cardinals: theory HOL-Cardinals.Fun_More

19:46:54 HOL-Cardinals: theory HOL-Cardinals.Order_Relation_More

19:46:55 HOL-Cardinals: theory HOL-Cardinals.Order_Union

19:46:55 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Extension

19:46:55 HOL-Cardinals: theory HOL-Cardinals.Wellfounded_More

19:46:55 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Relation

19:46:55 HOL-Hoare: theory HOL-Hoare.HeapSyntax

19:46:55 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Embedding

19:46:55 HOL-Hoare: theory HOL-Hoare.Pointer_Examples

19:46:55 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Constructions

19:46:55 HOL-Hoare: theory HOL-Hoare.SchorrWaite

19:46:56 Timing Tutorial (2 threads, 35.803s elapsed time, 67.192s cpu time, 9.992s GC time, factor 1.88)

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

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

19:46:56 Finished Tutorial (0:00:43 elapsed time, 0:01:15 cpu time, factor 1.71)

19:46:56 Running HOL-Induct ...

19:46:57 HOL-Hoare: theory HOL-Hoare.Pointers0

19:46:57 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Order_Relation

19:46:57 HOL-Induct: theory HOL-Induct.Common_Patterns

19:46:57 HOL-Cardinals: theory HOL-Cardinals.Ordinal_Arithmetic

19:46:57 HOL-Hoare: theory HOL-Hoare.ExamplesAbort

19:46:57 HOL-Hoare: theory HOL-Hoare.HeapSyntaxAbort

19:46:58 HOL-Hoare: theory HOL-Hoare.Pointer_ExamplesAbort

19:46:58 HOL-Hoare: theory HOL-Hoare.SepLogHeap

19:46:58 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Arithmetic

19:46:58 HOL-Hoare: theory HOL-Hoare.Separation

19:46:58 HOL-Cardinals: theory HOL-Cardinals.Cardinals

19:46:58 HOL-Hoare: theory HOL-Hoare.Hoare

19:46:59 HOL-Cardinals: theory HOL-Cardinals.Bounded_Set

19:46:59 HOL-Induct: theory HOL-Induct.ABexp

19:46:59 HOL-Induct: theory HOL-Induct.Com

19:47:03 HOL-Induct: theory HOL-Induct.Comb

19:47:03 HOL-Induct: theory HOL-Induct.Infinitely_Branching_Tree

19:47:04 HOL-Induct: theory HOL-Induct.Nested_Datatype

19:47:06 HOL-Induct: theory HOL-Induct.Ordinals

19:47:06 HOL-Induct: theory HOL-Induct.PropLog

19:47:06 HOL-Induct: theory HOL-Induct.QuoDataType

19:47:07 HOL-Induct: theory HOL-Induct.QuoNestedDataType

19:47:09 HOL-Induct: theory HOL-Induct.Sigma_Algebra

19:47:09 HOL-Induct: theory HOL-Induct.Term

19:47:10 HOL-Induct: theory HOL-Induct.Sexp

19:47:10 HOL-Induct: theory HOL-Induct.SList

19:47:23 Timing HOL-Induct (2 threads, 21.240s elapsed time, 39.908s cpu time, 6.876s GC time, factor 1.88)

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

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

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

19:47:23 Finished HOL-Induct (0:00:27 elapsed time, 0:00:48 cpu time, factor 1.80)

19:47:23 Running HOL-SPARK-Examples ...

19:47:24 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Lemmas

19:47:24 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD

19:47:24 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Greatest_Common_Divisor

19:47:25 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Longest_Increasing_Subsequence

19:47:25 Timing HOL-Hoare (2 threads, 27.532s elapsed time, 50.428s cpu time, 1.644s GC time, factor 1.83)

19:47:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare

19:47:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/document.pdf

19:47:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/outline.pdf

19:47:25 Finished HOL-Hoare (0:00:33 elapsed time, 0:00:59 cpu time, factor 1.78)

19:47:25 Timing HOL-Cardinals (2 threads, 23.701s elapsed time, 44.496s cpu time, 1.812s GC time, factor 1.88)

19:47:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals

19:47:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals/document.pdf

19:47:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals/outline.pdf

19:47:25 Finished HOL-Cardinals (0:00:31 elapsed time, 0:00:55 cpu time, factor 1.77)

19:47:25 Running HOL-Statespace ...

19:47:25 Running HOL-Matrix_LP ...

19:47:25 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification

19:47:25 HOL-SPARK-Examples: theory HOL-SPARK-Examples.F

19:47:26 HOL-Statespace: theory HOL-Statespace.DistinctTreeProver

19:47:26 HOL-Matrix_LP: theory HOL-Matrix_LP.Compute_Oracle

19:47:26 HOL-Matrix_LP: theory HOL-Matrix_LP.LP

19:47:26 HOL-Matrix_LP: theory HOL-Matrix_LP.Matrix

19:47:27 HOL-Statespace: theory HOL-Statespace.StateFun

19:47:27 HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeFloat

19:47:27 HOL-Statespace: theory HOL-Statespace.StateSpaceLocale

19:47:28 HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeHOL

19:47:28 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Hash

19:47:28 HOL-Statespace: theory HOL-Statespace.StateSpaceSyntax

19:47:28 HOL-Statespace: theory HOL-Statespace.StateSpaceEx

19:47:28 HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeNumeral

19:47:28 HOL-Matrix_LP: theory HOL-Matrix_LP.SparseMatrix

19:47:30 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_L

19:47:30 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_R

19:47:30 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_L

19:47:31 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_R

19:47:31 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Round

19:47:32 HOL-Matrix_LP: theory HOL-Matrix_LP.Cplex

19:47:32 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_L

19:47:33 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_R

19:47:33 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Sqrt

19:47:44 Timing HOL-SPARK-Examples (2 threads, 18.876s elapsed time, 32.028s cpu time, 1.052s GC time, factor 1.70)

19:47:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Examples

19:47:44 Finished HOL-SPARK-Examples (0:00:20 elapsed time, 0:00:33 cpu time, factor 1.62)

19:47:44 Running HOL-TLA-Memory ...

19:47:45 HOL-TLA-Memory: theory HOL-TLA-Memory.RPCMemoryParams

19:47:45 HOL-TLA-Memory: theory HOL-TLA-Memory.MemoryParameters

19:47:45 HOL-TLA-Memory: theory HOL-TLA-Memory.ProcedureInterface

19:47:46 HOL-TLA-Memory: theory HOL-TLA-Memory.RPCParameters

19:47:46 HOL-TLA-Memory: theory HOL-TLA-Memory.Memory

19:47:46 Timing HOL-Matrix_LP (2 threads, 14.894s elapsed time, 28.864s cpu time, 1.436s GC time, factor 1.94)

19:47:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP

19:47:46 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/document.pdf

19:47:46 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/outline.pdf

19:47:46 Finished HOL-Matrix_LP (0:00:20 elapsed time, 0:00:38 cpu time, factor 1.85)

19:47:46 Running HOLCF-Tutorial ...

19:47:47 HOL-TLA-Memory: theory HOL-TLA-Memory.MemClerkParameters

19:47:47 HOL-TLA-Memory: theory HOL-TLA-Memory.RPC

19:47:47 HOLCF-Tutorial: theory HOLCF-Tutorial.Domain_ex

19:47:47 HOLCF-Tutorial: theory HOLCF-Tutorial.Fixrec_ex

19:47:47 HOL-TLA-Memory: theory HOL-TLA-Memory.MemClerk

19:47:47 Timing HOL-Statespace (2 threads, 18.020s elapsed time, 20.760s cpu time, 0.796s GC time, factor 1.15)

19:47:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace

19:47:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/document.pdf

19:47:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/outline.pdf

19:47:47 Finished HOL-Statespace (0:00:22 elapsed time, 0:00:28 cpu time, factor 1.25)

19:47:47 Running Isar_Ref ...

19:47:48 HOL-TLA-Memory: theory HOL-TLA-Memory.MemoryImplementation

19:47:49 Isar_Ref: theory Isar_Ref.Base

19:47:49 Isar_Ref: theory Isar_Ref.Document_Preparation

19:47:49 Isar_Ref: theory Isar_Ref.First_Order_Logic

19:47:49 Isar_Ref: theory Isar_Ref.Framework

19:47:49 Isar_Ref: theory Isar_Ref.Generic

19:47:49 Isar_Ref: theory Isar_Ref.HOL_Specific

19:47:49 HOLCF-Tutorial: theory HOLCF-Tutorial.New_Domain

19:47:50 Isar_Ref: theory Isar_Ref.Inner_Syntax

19:47:50 Isar_Ref: theory Isar_Ref.Outer_Syntax

19:47:51 Isar_Ref: theory Isar_Ref.Preface

19:47:51 Isar_Ref: theory Isar_Ref.Proof

19:47:51 Isar_Ref: theory Isar_Ref.Proof_Script

19:47:51 Isar_Ref: theory Isar_Ref.Quick_Reference

19:47:51 Isar_Ref: theory Isar_Ref.Spec

19:47:52 Isar_Ref: theory Isar_Ref.Symbols

19:47:52 Isar_Ref: theory Isar_Ref.Synopsis

19:48:00 Timing HOL-TLA-Memory (2 threads, 13.722s elapsed time, 24.276s cpu time, 0.844s GC time, factor 1.77)

19:48:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Memory

19:48:00 Finished HOL-TLA-Memory (0:00:15 elapsed time, 0:00:25 cpu time, factor 1.66)

19:48:00 Running Codegen ...

19:48:01 Codegen: theory Codegen.Adaptation

19:48:01 Codegen: theory Codegen.Computations

19:48:02 Codegen: theory Codegen.Evaluation

19:48:02 Codegen: theory Codegen.Further

19:48:02 Codegen: theory Codegen.Inductive_Predicate

19:48:03 Codegen: theory Codegen.Introduction

19:48:04 Codegen: theory Codegen.Foundations

19:48:05 Codegen: theory Codegen.Refinement

19:48:05 Timing HOLCF-Tutorial (2 threads, 14.566s elapsed time, 18.752s cpu time, 0.504s GC time, factor 1.29)

19:48:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial

19:48:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/document.pdf

19:48:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/outline.pdf

19:48:05 Finished HOLCF-Tutorial (0:00:19 elapsed time, 0:00:25 cpu time, factor 1.36)

19:48:05 Running IOA-NTP ...

19:48:06 IOA-NTP: theory IOA-NTP.Lemmas

19:48:06 IOA-NTP: theory IOA-NTP.Multiset

19:48:06 IOA-NTP: theory IOA-NTP.Packet

19:48:06 IOA-NTP: theory IOA-NTP.Action

19:48:08 IOA-NTP: theory IOA-NTP.Abschannel

19:48:08 IOA-NTP: theory IOA-NTP.Receiver

19:48:09 IOA-NTP: theory IOA-NTP.Sender

19:48:10 Timing Isar_Ref (2 threads, 10.361s elapsed time, 16.476s cpu time, 1.236s GC time, factor 1.59)

19:48:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref

19:48:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref/isar-ref.pdf

19:48:10 Finished Isar_Ref (0:00:21 elapsed time, 0:00:28 cpu time, factor 1.30)

19:48:10 Running HOL-TPTP ...

19:48:10 IOA-NTP: theory IOA-NTP.Spec

19:48:10 IOA-NTP: theory IOA-NTP.Impl

19:48:11 IOA-NTP: theory IOA-NTP.Correctness

19:48:11 HOL-TPTP: theory HOL-TPTP.TPTP_Parser

19:48:11 HOL-TPTP: theory HOL-TPTP.MaSh_Export_Base

19:48:12 HOL-TPTP: theory HOL-TPTP.MaSh_Eval

19:48:12 HOL-TPTP: theory HOL-TPTP.ATP_Theory_Export

19:48:12 HOL-TPTP: theory HOL-TPTP.THF_Arith

19:48:15 Timing IOA-NTP (2 threads, 7.632s elapsed time, 14.288s cpu time, 0.804s GC time, factor 1.87)

19:48:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-NTP

19:48:15 Finished IOA-NTP (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.66)

19:48:15 Running HOL-NanoJava ...

19:48:15 Timing Codegen (2 threads, 8.104s elapsed time, 15.632s cpu time, 0.872s GC time, factor 1.93)

19:48:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen

19:48:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen/codegen.pdf

19:48:15 Finished Codegen (0:00:14 elapsed time, 0:00:22 cpu time, factor 1.55)

19:48:15 Running HOLCF-IMP ...

19:48:15 HOL-NanoJava: theory HOL-NanoJava.Term

19:48:16 HOL-TPTP: theory HOL-TPTP.TPTP_Interpret

19:48:16 HOLCF-IMP: theory HOL-IMP.AExp

19:48:17 HOL-TPTP: theory HOL-TPTP.TPTP_Proof_Reconstruction

19:48:18 HOLCF-IMP: theory HOL-IMP.BExp

19:48:18 HOL-NanoJava: theory HOL-NanoJava.Decl

19:48:18 HOL-NanoJava: theory HOL-NanoJava.TypeRel

19:48:19 HOL-NanoJava: theory HOL-NanoJava.State

19:48:19 HOL-TPTP: theory HOL-TPTP.ATP_Problem_Import

19:48:19 HOL-NanoJava: theory HOL-NanoJava.AxSem

19:48:19 HOL-NanoJava: theory HOL-NanoJava.OpSem

19:48:20 HOLCF-IMP: theory HOL-IMP.Com

19:48:20 HOL-NanoJava: theory HOL-NanoJava.Equivalence

19:48:21 HOLCF-IMP: theory HOL-IMP.Big_Step

19:48:21 Timing HOL-TPTP (2 threads, 8.294s elapsed time, 9.564s cpu time, 0.408s GC time, factor 1.15)

19:48:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TPTP

19:48:21 Finished HOL-TPTP (0:00:10 elapsed time, 0:00:11 cpu time, factor 1.08)

19:48:21 Running HOL-Unix ...

19:48:21 HOL-NanoJava: theory HOL-NanoJava.Example

19:48:21 HOLCF-IMP: theory HOLCF-IMP.Denotational

19:48:22 HOL-Unix: theory HOL-Unix.Nested_Environment

19:48:22 HOLCF-IMP: theory HOLCF-IMP.HoareEx

19:48:24 HOL-Unix: theory HOL-Unix.Unix

19:48:26 Timing HOL-NanoJava (2 threads, 6.730s elapsed time, 11.884s cpu time, 0.796s GC time, factor 1.77)

19:48:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava

19:48:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/document.pdf

19:48:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/outline.pdf

19:48:26 Finished HOL-NanoJava (0:00:11 elapsed time, 0:00:18 cpu time, factor 1.67)

19:48:26 Running Prog_Prove ...

19:48:27 Timing HOLCF-IMP (2 threads, 6.567s elapsed time, 12.140s cpu time, 0.656s GC time, factor 1.85)

19:48:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP

19:48:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP/document.pdf

19:48:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP/outline.pdf

19:48:27 Finished HOLCF-IMP (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.71)

19:48:27 Running IOA-ABP ...

19:48:27 Prog_Prove: theory Prog_Prove.Bool_nat_list

19:48:27 Prog_Prove: theory Prog_Prove.Basics

19:48:27 Prog_Prove: theory Prog_Prove.LaTeXsugar

19:48:27 Prog_Prove: theory Prog_Prove.Isar

19:48:28 Prog_Prove: theory Prog_Prove.Logic

19:48:28 IOA-ABP: theory IOA-ABP.Packet

19:48:28 IOA-ABP: theory IOA-ABP.Lemmas

19:48:28 IOA-ABP: theory IOA-ABP.Action

19:48:29 Prog_Prove: theory Prog_Prove.MyList

19:48:29 Prog_Prove: theory Prog_Prove.Types_and_funs

19:48:30 IOA-ABP: theory IOA-ABP.Abschannel

19:48:30 IOA-ABP: theory IOA-ABP.Env

19:48:30 IOA-ABP: theory IOA-ABP.Receiver

19:48:31 IOA-ABP: theory IOA-ABP.Sender

19:48:31 IOA-ABP: theory IOA-ABP.Abschannel_finite

19:48:31 IOA-ABP: theory IOA-ABP.Impl

19:48:32 IOA-ABP: theory IOA-ABP.Impl_finite

19:48:32 IOA-ABP: theory IOA-ABP.Spec

19:48:32 IOA-ABP: theory IOA-ABP.Correctness

19:48:33 Timing HOL-Unix (2 threads, 6.750s elapsed time, 10.020s cpu time, 0.488s GC time, factor 1.48)

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

19:48:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/document.pdf

19:48:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/outline.pdf

19:48:33 Finished HOL-Unix (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.49)

19:48:33 Running HOL-Mirabelle-ex ...

19:48:34 HOL-Mirabelle-ex: theory HOL-Mirabelle-ex.Ex

19:48:35 Timing IOA-ABP (2 threads, 6.035s elapsed time, 10.340s cpu time, 0.224s GC time, factor 1.71)

19:48:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ABP

19:48:35 Finished IOA-ABP (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.49)

19:48:35 Running HOL-Isar_Examples ...

19:48:36 HOL-Isar_Examples: theory HOL-Isar_Examples.First_Order_Logic

19:48:36 HOL-Isar_Examples: theory HOL-Isar_Examples.Higher_Order_Logic

19:48:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Basic_Logic

19:48:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Cantor

19:48:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Drinker

19:48:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Expr_Compiler

19:48:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Group

19:48:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Group_Context

19:48:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Group_Notepad

19:48:37 HOL-Isar_Examples: theory HOL-Isar_Examples.Hoare

19:48:38 Timing Prog_Prove (2 threads, 6.151s elapsed time, 11.796s cpu time, 0.884s GC time, factor 1.92)

19:48:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove

19:48:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove/prog-prove.pdf

19:48:38 Finished Prog_Prove (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.52)

19:48:38 Running HOLCF-ex ...

19:48:39 HOL-Isar_Examples: theory HOL-Isar_Examples.Knaster_Tarski

19:48:39 HOL-Isar_Examples: theory HOL-Isar_Examples.Hoare_Ex

19:48:39 HOL-Isar_Examples: theory HOL-Isar_Examples.Mutilated_Checkerboard

19:48:39 HOLCF-ex: theory HOLCF-ex.Focus_ex

19:48:39 HOLCF-ex: theory HOLCF-ex.Dagstuhl

19:48:39 HOL-Isar_Examples: theory HOL-Isar_Examples.Peirce

19:48:39 HOL-Isar_Examples: theory HOL-Isar_Examples.Puzzle

19:48:39 HOL-Isar_Examples: theory HOL-Isar_Examples.Structured_Statements

19:48:39 HOLCF-ex: theory HOLCF-ex.Concurrency_Monad

19:48:39 HOL-Isar_Examples: theory HOL-Isar_Examples.Summation

19:48:39 HOL-Isar_Examples: theory HOL-Isar_Examples.Fibonacci

19:48:39 HOLCF-ex: theory HOLCF-ex.Dnat

19:48:40 HOLCF-ex: theory HOLCF-ex.Domain_Proofs

19:48:40 Timing HOL-Mirabelle-ex (2 threads, 5.974s elapsed time, 0.032s cpu time, 0.000s GC time, factor 0.01)

19:48:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle-ex

19:48:40 Finished HOL-Mirabelle-ex (0:00:07 elapsed time, 0:00:08 cpu time, factor 1.18)

19:48:40 Running HOL-SPARK-Manual ...

19:48:41 HOLCF-ex: theory HOLCF-ex.Fix2

19:48:41 HOLCF-ex: theory HOLCF-ex.Hoare

19:48:42 HOL-SPARK-Manual: theory HOL-SPARK-Examples.Greatest_Common_Divisor

19:48:42 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Complex_Types

19:48:42 HOLCF-ex: theory HOLCF-ex.Letrec

19:48:42 HOLCF-ex: theory HOLCF-ex.Loop

19:48:42 HOLCF-ex: theory HOLCF-ex.Pattern_Match

19:48:42 HOLCF-ex: theory HOLCF-ex.Powerdomain_ex

19:48:42 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Proc1

19:48:42 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Proc2

19:48:42 HOL-SPARK-Manual: theory HOL-SPARK-Manual.VC_Principles

19:48:42 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Reference

19:48:43 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Simple_Greatest_Common_Divisor

19:48:43 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Example_Verification

19:48:46 Timing HOLCF-ex (2 threads, 5.618s elapsed time, 10.784s cpu time, 0.348s GC time, factor 1.92)

19:48:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-ex

19:48:46 Finished HOLCF-ex (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.62)

19:48:46 Running HOLCF-FOCUS ...

19:48:47 Timing HOL-Isar_Examples (2 threads, 5.789s elapsed time, 10.776s cpu time, 0.824s GC time, factor 1.86)

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

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

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

19:48:47 Finished HOL-Isar_Examples (0:00:11 elapsed time, 0:00:20 cpu time, factor 1.70)

19:48:47 Running HOL-IMPP ...

19:48:47 HOLCF-FOCUS: theory HOLCF-FOCUS.Fstream

19:48:47 HOLCF-FOCUS: theory HOLCF-FOCUS.Fstreams

19:48:47 HOLCF-FOCUS: theory HOLCF-FOCUS.FOCUS

19:48:47 HOLCF-FOCUS: theory HOLCF-FOCUS.Buffer

19:48:48 HOLCF-FOCUS: theory HOLCF-FOCUS.Stream_adm

19:48:48 HOL-IMPP: theory HOL-IMPP.Com

19:48:49 HOLCF-FOCUS: theory HOLCF-FOCUS.Buffer_adm

19:48:50 HOL-IMPP: theory HOL-IMPP.Natural

19:48:51 HOL-IMPP: theory HOL-IMPP.Hoare

19:48:52 HOL-IMPP: theory HOL-IMPP.Misc

19:48:52 Timing HOL-SPARK-Manual (2 threads, 4.799s elapsed time, 8.008s cpu time, 0.176s GC time, factor 1.67)

19:48:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual

19:48:52 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/document.pdf

19:48:52 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/outline.pdf

19:48:52 Finished HOL-SPARK-Manual (0:00:10 elapsed time, 0:00:18 cpu time, factor 1.66)

19:48:52 Running HOL-ZF ...

19:48:52 HOL-IMPP: theory HOL-IMPP.EvenOdd

19:48:53 Timing HOLCF-FOCUS (2 threads, 4.701s elapsed time, 8.860s cpu time, 0.236s GC time, factor 1.88)

19:48:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-FOCUS

19:48:53 Finished HOLCF-FOCUS (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.56)

19:48:53 Running Implementation ...

19:48:53 HOL-ZF: theory HOL-ZF.LProd

19:48:53 HOL-ZF: theory HOL-ZF.HOLZF

19:48:54 Implementation: theory Implementation.Base

19:48:54 Implementation: theory Implementation.Eq

19:48:54 Implementation: theory Implementation.Integration

19:48:54 Timing HOL-IMPP (2 threads, 4.727s elapsed time, 7.696s cpu time, 0.316s GC time, factor 1.63)

19:48:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMPP

19:48:54 Finished HOL-IMPP (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.40)

19:48:54 Running HOL-Hahn_Banach ...

19:48:54 Implementation: theory Implementation.Isar

19:48:54 HOL-ZF: theory HOL-ZF.Zet

19:48:54 Implementation: theory Implementation.Local_Theory

19:48:54 Implementation: theory Implementation.ML

19:48:54 HOL-ZF: theory HOL-ZF.MainZF

19:48:54 Implementation: theory Implementation.Prelim

19:48:54 HOL-ZF: theory HOL-ZF.Games

19:48:54 Implementation: theory Implementation.Proof

19:48:54 Implementation: theory Implementation.Syntax

19:48:55 Implementation: theory Implementation.Tactic

19:48:55 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Zorn_Lemma

19:48:55 HOL-Hahn_Banach: theory HOL-Analysis.Continuum_Not_Denumerable

19:48:55 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Bounds

19:48:55 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Vector_Space

19:48:56 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Linearform

19:48:56 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Subspace

19:48:57 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Function_Order

19:48:57 Implementation: theory Implementation.Logic

19:48:57 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Normed_Space

19:48:57 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Function_Norm

19:48:58 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Ext_Lemmas

19:48:58 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Sup_Lemmas

19:48:58 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Lemmas

19:48:58 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach

19:49:02 Timing HOL-ZF (2 threads, 4.684s elapsed time, 8.564s cpu time, 0.304s GC time, factor 1.83)

19:49:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF

19:49:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/document.pdf

19:49:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/outline.pdf

19:49:02 Finished HOL-ZF (0:00:10 elapsed time, 0:00:16 cpu time, factor 1.65)

19:49:02 Running Functions ...

19:49:03 Functions: theory Functions.Functions

19:49:03 Timing Implementation (2 threads, 3.903s elapsed time, 6.832s cpu time, 0.128s GC time, factor 1.75)

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

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

19:49:03 Finished Implementation (0:00:10 elapsed time, 0:00:13 cpu time, factor 1.29)

19:49:03 Running HOL-Nonstandard_Analysis-Examples ...

19:49:04 Timing HOL-Hahn_Banach (2 threads, 4.306s elapsed time, 7.736s cpu time, 0.296s GC time, factor 1.80)

19:49:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach

19:49:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/document.pdf

19:49:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/outline.pdf

19:49:04 Finished HOL-Hahn_Banach (0:00:09 elapsed time, 0:00:16 cpu time, factor 1.69)

19:49:04 Running HOL-IOA ...

19:49:05 HOL-IOA: theory HOL-IOA.Asig

19:49:05 HOL-IOA: theory HOL-IOA.IOA

19:49:05 HOL-Nonstandard_Analysis-Examples: theory HOL-Nonstandard_Analysis-Examples.NSPrimes

19:49:06 HOL-IOA: theory HOL-IOA.Solve

19:49:08 Timing HOL-IOA (2 threads, 2.706s elapsed time, 3.932s cpu time, 0.124s GC time, factor 1.45)

19:49:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IOA

19:49:08 Finished HOL-IOA (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.18)

19:49:08 Running HOL-TLA-Inc ...

19:49:09 Timing HOL-Nonstandard_Analysis-Examples (2 threads, 2.987s elapsed time, 3.696s cpu time, 0.168s GC time, factor 1.24)

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

19:49:09 Finished HOL-Nonstandard_Analysis-Examples (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.04)

19:49:09 Running HOL-Lattice ...

19:49:09 HOL-TLA-Inc: theory HOL-TLA-Inc.Inc

19:49:09 Timing Functions (2 threads, 3.363s elapsed time, 4.528s cpu time, 0.320s GC time, factor 1.35)

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

19:49:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions/functions.pdf

19:49:09 Finished Functions (0:00:07 elapsed time, 0:00:08 cpu time, factor 1.20)

19:49:09 Running Classes ...

19:49:10 HOL-Lattice: theory HOL-Lattice.Orders

19:49:10 Classes: theory Classes.Setup

19:49:11 Classes: theory Classes.Classes

19:49:11 HOL-Lattice: theory HOL-Lattice.Bounds

19:49:11 HOL-Lattice: theory HOL-Lattice.Lattice

19:49:11 HOL-Lattice: theory HOL-Lattice.CompleteLattice

19:49:13 Timing HOL-TLA-Inc (2 threads, 2.329s elapsed time, 4.048s cpu time, 0.148s GC time, factor 1.74)

19:49:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Inc

19:49:13 Finished HOL-TLA-Inc (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.33)

19:49:13 Running HOL-Proofs-ex ...

19:49:13 HOL-Proofs-ex: theory HOL-Isar_Examples.Drinker

19:49:13 HOL-Proofs-ex: theory HOL-Proofs-ex.Hilbert_Classical

19:49:13 HOL-Proofs-ex: theory HOL-Proofs-ex.XML_Data

19:49:14 HOL-Proofs-ex: theory HOL-Proofs-ex.Proof_Terms

19:49:16 Timing HOL-Lattice (2 threads, 2.066s elapsed time, 3.600s cpu time, 0.000s GC time, factor 1.74)

19:49:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice

19:49:16 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/document.pdf

19:49:16 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/outline.pdf

19:49:16 Finished HOL-Lattice (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.68)

19:49:16 Running Eisbach ...

19:49:16 Timing HOL-Proofs-ex (2 threads, 1.657s elapsed time, 2.308s cpu time, 0.000s GC time, factor 1.39)

19:49:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-ex

19:49:16 Finished HOL-Proofs-ex (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.06)

19:49:16 Running IOA-Storage ...

19:49:16 Eisbach: theory Eisbach.Base

19:49:17 Timing Classes (2 threads, 1.956s elapsed time, 2.252s cpu time, 0.000s GC time, factor 1.15)

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

19:49:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes/classes.pdf

19:49:17 Finished Classes (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.05)

19:49:17 Running Main ...

19:49:17 Eisbach: theory Eisbach.Manual

19:49:17 Eisbach: theory Eisbach.Preface

19:49:17 IOA-Storage: theory IOA-Storage.Action

19:49:18 Main: theory Main.Main_Doc

19:49:18 IOA-Storage: theory IOA-Storage.Impl

19:49:18 IOA-Storage: theory IOA-Storage.Spec

19:49:18 IOA-Storage: theory IOA-Storage.Correctness

19:49:20 Timing IOA-Storage (2 threads, 1.619s elapsed time, 2.400s cpu time, 0.000s GC time, factor 1.48)

19:49:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-Storage

19:49:20 Finished IOA-Storage (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.08)

19:49:20 Running Locales ...

19:49:21 Locales: theory Locales.Examples

19:49:21 Locales: theory Locales.Examples1

19:49:21 Locales: theory Locales.Examples2

19:49:21 Locales: theory Locales.Examples3

19:49:22 Timing Eisbach (2 threads, 1.699s elapsed time, 2.240s cpu time, 0.000s GC time, factor 1.32)

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

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

19:49:22 Finished Eisbach (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.16)

19:49:22 Timing Main (2 threads, 1.339s elapsed time, 1.424s cpu time, 0.000s GC time, factor 1.06)

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

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

19:49:22 Finished Main (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.11)

19:49:22 Running HOL-Import ...

19:49:22 Running Sugar ...

19:49:23 Sugar: theory HOL-Library.LaTeXsugar

19:49:23 HOL-Import: theory HOL-Import.Import_Setup

19:49:23 Sugar: theory HOL-Library.OptionalSugar

19:49:23 HOL-Import: theory HOL-Import.HOL_Light_Maps

19:49:24 Sugar: theory Sugar.Sugar

19:49:25 Skipping theories "HOL_Light_Import" (undefined HOL_LIGHT_BUNDLE)

19:49:25 Timing HOL-Import (2 threads, 0.938s elapsed time, 1.684s cpu time, 0.000s GC time, factor 1.80)

19:49:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Import

19:49:25 Finished HOL-Import (0:00:02 elapsed time)

19:49:25 Running HOL-Types_To_Sets ...

19:49:26 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Prerequisites

19:49:26 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Types_To_Sets

19:49:26 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Finite

19:49:26 HOL-Types_To_Sets: theory HOL-Types_To_Sets.T2_Spaces

19:49:26 Timing Locales (2 threads, 1.282s elapsed time, 2.364s cpu time, 0.000s GC time, factor 1.84)

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

19:49:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales/locales.pdf

19:49:26 Finished Locales (0:00:05 elapsed time, 0:00:07 cpu time, factor 1.27)

19:49:26 Running IOA-ex ...

19:49:27 IOA-ex: theory IOA-ex.TrivEx

19:49:27 IOA-ex: theory IOA-ex.TrivEx2

19:49:27 Timing Sugar (2 threads, 0.892s elapsed time, 0.988s cpu time, 0.000s GC time, factor 1.11)

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

19:49:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar/sugar.pdf

19:49:27 Finished Sugar (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.10)

19:49:27 Timing HOL-Types_To_Sets (2 threads, 0.925s elapsed time, 1.488s cpu time, 0.000s GC time, factor 1.61)

19:49:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Types_To_Sets

19:49:27 Finished HOL-Types_To_Sets (0:00:02 elapsed time)

19:49:27 Running HOL-TLA-Buffer ...

19:49:27 Running HOL-Mutabelle ...

19:49:28 HOL-TLA-Buffer: theory HOL-TLA-Buffer.Buffer

19:49:28 HOL-TLA-Buffer: theory HOL-TLA-Buffer.DBuffer

19:49:28 Timing IOA-ex (2 threads, 0.826s elapsed time, 1.740s cpu time, 0.000s GC time, factor 2.11)

19:49:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ex

19:49:28 Finished IOA-ex (0:00:02 elapsed time)

19:49:28 Running JEdit ...

19:49:29 HOL-Mutabelle: theory HOL-Mutabelle.MutabelleExtra

19:49:29 JEdit: theory JEdit.Base

19:49:29 JEdit: theory JEdit.JEdit

19:49:30 Timing HOL-TLA-Buffer (2 threads, 0.572s elapsed time, 1.088s cpu time, 0.000s GC time, factor 1.90)

19:49:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Buffer

19:49:30 Finished HOL-TLA-Buffer (0:00:02 elapsed time)

19:49:30 Running How_to_Prove_it ...

19:49:31 Timing HOL-Mutabelle (2 threads, 0.621s elapsed time, 0.716s cpu time, 0.000s GC time, factor 1.15)

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

19:49:31 Finished HOL-Mutabelle (0:00:02 elapsed time)

19:49:31 Running HOL-Prolog ...

19:49:31 How_to_Prove_it: theory How_to_Prove_it.How_to_Prove_it

19:49:31 HOL-Prolog: theory HOL-Prolog.HOHH

19:49:31 HOL-Prolog: theory HOL-Prolog.Func

19:49:31 HOL-Prolog: theory HOL-Prolog.Test

19:49:32 HOL-Prolog: theory HOL-Prolog.Type

19:49:33 Timing HOL-Prolog (2 threads, 0.266s elapsed time, 0.432s cpu time, 0.000s GC time, factor 1.62)

19:49:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Prolog

19:49:33 Finished HOL-Prolog (0:00:01 elapsed time)

19:49:33 Running Typeclass_Hierarchy ...

19:49:34 Typeclass_Hierarchy: theory Typeclass_Hierarchy.Typeclass_Hierarchy

19:49:35 Timing How_to_Prove_it (2 threads, 0.358s elapsed time, 0.512s cpu time, 0.000s GC time, factor 1.43)

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

19:49:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it/how_to_prove_it.pdf

19:49:35 Finished How_to_Prove_it (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.14)

19:49:38 Timing Typeclass_Hierarchy (2 threads, 0.253s elapsed time, 0.360s cpu time, 0.000s GC time, factor 1.42)

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

19:49:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy/typeclass_hierarchy.pdf

19:49:38 Finished Typeclass_Hierarchy (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.13)

19:49:41 Timing JEdit (2 threads, 0.540s elapsed time, 0.616s cpu time, 0.000s GC time, factor 1.14)

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

19:49:41 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit/jedit.pdf

19:49:41 Finished JEdit (0:00:11 elapsed time, 0:00:12 cpu time, factor 1.04)

19:49:41

19:49:41 === TIMING ===

19:49:41

19:49:41 Group main: 0:39:05 elapsed time, 1:06:57 cpu time, factor 1.71

19:49:41 Group doc: 0:04:59 elapsed time, 0:06:50 cpu time, factor 1.37

19:49:41 Group timing: 2:15:42 elapsed time, 3:52:30 cpu time, factor 1.71

19:49:41 Overall: 0:59:21 elapsed time, 4:59:25 cpu time, factor 5.04

19:49:41 Archiving artifacts

19:49:41 Started calculate disk usage of build

19:49:41 Finished Calculation of disk usage of build in 0 seconds

19:49:45 Started calculate disk usage of workspace

19:49:45 Finished Calculation of disk usage of workspace in 0 seconds

19:49:46 No emails were triggered.

19:49:46 Finished: SUCCESS