Skip to content
Success

Console Output

15:05:25 Started by upstream project "isabelle-repo" build number 1682

15:05:25 originally caused by:

15:05:25 Started by an SCM change

15:05:25 [EnvInject] - Loading node environment variables.

15:05:26 Building remotely on workermta4 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-repo-makeall

15:05:26 [isabelle-repo-makeall] $ hg showconfig paths.default

15:05:26 [isabelle-repo-makeall] $ hg pull --rev 035c78bb0a6675e8b5e9c5b42daa6410b353c1a0

15:05:27 pulling from http://isabelle.in.tum.de/repos/isabelle/

15:05:27 searching for changes

15:05:27 adding changesets

15:05:27 adding manifests

15:05:27 adding file changes

15:05:27 added 70 changesets with 190 changes to 118 files

15:05:27 (run 'hg update' to get a working copy)

15:05:27 [isabelle-repo-makeall] $ hg update --clean --rev 035c78bb0a6675e8b5e9c5b42daa6410b353c1a0

15:05:27 117 files updated, 0 files merged, 3 files removed, 0 files unresolved

15:05:27 [isabelle-repo-makeall] $ hg log --rev . --template {node}

15:05:27 [isabelle-repo-makeall] $ hg log --rev . --template {rev}

15:05:28 [isabelle-repo-makeall] $ hg id --branch

15:05:28 No emails were triggered.

15:05:28 [isabelle-repo-makeall] $ /bin/sh -xe /tmp/jenkins40489613051452615.sh

15:05:28 + Admin/jenkins/run_build makeall

15:05:28 + set -e

15:05:28 + PROFILE=makeall

15:05:28 + shift

15:05:28 + bin/isabelle components -a

15:05:28 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/cvc4-1.5-4"

15:05:28 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/e-2.0-2"

15:05:28 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/scala-2.12.6"

15:05:28 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/spass-3.8ds-1"

15:05:28 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/z3-4.4.0pre-2"

15:05:28 Getting "https://isabelle.in.tum.de/components/cvc4-1.5-4.tar.gz"

15:05:29 Unpacking "/media/data/jenkins/.isabelle/contrib/cvc4-1.5-4.tar.gz"

15:05:30 Getting "https://isabelle.in.tum.de/components/e-2.0-2.tar.gz"

15:05:30 Unpacking "/media/data/jenkins/.isabelle/contrib/e-2.0-2.tar.gz"

15:05:30 Getting "https://isabelle.in.tum.de/components/scala-2.12.6.tar.gz"

15:05:31 Unpacking "/media/data/jenkins/.isabelle/contrib/scala-2.12.6.tar.gz"

15:05:31 Getting "https://isabelle.in.tum.de/components/spass-3.8ds-1.tar.gz"

15:05:31 Unpacking "/media/data/jenkins/.isabelle/contrib/spass-3.8ds-1.tar.gz"

15:05:31 Getting "https://isabelle.in.tum.de/components/z3-4.4.0pre-2.tar.gz"

15:05:32 Unpacking "/media/data/jenkins/.isabelle/contrib/z3-4.4.0pre-2.tar.gz"

15:05:32 + bin/isabelle jedit -bf

15:05:33 ### Building Isabelle/Scala ...

15:06:07 ### Building Isabelle/jEdit ...

15:06:28 + bin/isabelle ci_build_makeall

15:06:34

15:06:34 === CONFIGURATION ===

15:06:34

15:06:34 ISABELLE_BUILD_OPTIONS=""

15:06:34

15:06:34 ML_PLATFORM="x86_64-linux"

15:06:34 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7.1-5/x86_64-linux"

15:06:34 ML_SYSTEM="polyml-5.7.1"

15:06:34 ML_OPTIONS="-H 4000 --maxheap 8G"

15:06:34

15:06:34 === BUILD ===

15:06:34

15:06:34 Build started at Thu, 24 May 2018 13:06:33 GMT

15:06:34 Isabelle id 035c78bb0a66

15:06:34

15:06:34 === LOG ===

15:06:34

15:06:34 Session Pure/Pure

15:06:35 Session CTT/CTT

15:06:35 Session Cube/Cube

15:06:35 Session FOL/FOL

15:06:35 Session CCL/CCL

15:06:35 Session FOL/FOL-ex

15:06:35 Session FOLP/FOLP

15:06:35 Session FOLP/FOLP-ex

15:06:35 Session HOL/HOL (main)

15:06:36 Session Doc/Classes (doc)

15:06:36 Session Doc/Functions (doc)

15:06:36 Session HOL/HOL-Eisbach

15:06:36 Session Doc/Eisbach (doc)

15:06:37 Session HOL/HOL-Hoare

15:06:37 Session HOL/HOL-Hoare_Parallel (timing)

15:06:37 Session HOL/HOL-IMPP

15:06:37 Session HOL/HOL-IOA

15:06:37 Session HOL/HOL-Import

15:06:37 Session HOL/HOL-Lattice

15:06:37 Session HOL/HOL-Library (main timing)

15:06:37 Session Doc/Codegen_Basics

15:06:38 Session Doc/Codegen (doc)

15:06:38 Session Doc/Datatypes (doc)

15:06:38 Session Doc/Corec (doc)

15:06:38 Session HOL/HOL-Auth (timing)

15:06:38 Session HOL/HOL-UNITY (timing)

15:06:38 Session HOL/HOL-Bali (timing)

15:06:38 Session HOL/HOL-Cardinals (timing)

15:06:38 Session HOL/HOL-Computational_Algebra (main timing)

15:06:39 Session HOL/HOL-Algebra (main timing)

15:06:39 Session HOL/HOL-Decision_Procs (timing)

15:06:39 Session HOL/HOL-Quotient_Examples (timing)

15:06:39 Session HOL/HOL-Analysis (main timing)

15:06:40 Session HOL/HOL-Analysis-ex

15:06:40 Session HOL/HOL-Probability (main timing)

15:06:40 Session HOL/HOL-Probability-ex (timing)

15:06:40 Session HOL/HOL-Isar_Examples

15:06:41 Session HOL/HOL-Nonstandard_Analysis (timing)

15:06:41 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)

15:06:41 Session HOL/HOL-Number_Theory (main timing)

15:06:41 Session HOL/HOL-Data_Structures (timing)

15:06:41 Session HOL/HOL-ex (timing)

15:06:42 Session HOL/HOL-Codegenerator_Test

15:06:42 Session HOL/HOL-Corec_Examples (timing)

15:06:42 Session HOL/HOL-Datatype_Examples (timing)

15:06:42 Session HOL/HOL-Hahn_Banach

15:06:42 Session HOL/HOL-IMP (timing)

15:06:42 Session HOL/HOL-Imperative_HOL (timing)

15:06:42 Session HOL/HOL-Induct

15:06:42 Session HOL/HOL-Matrix_LP

15:06:43 Session HOL/HOL-Metis_Examples (timing)

15:06:43 Session HOL/HOL-MicroJava (timing)

15:06:43 Session HOL/HOL-Mutabelle

15:06:43 Session HOL/HOL-Nitpick_Examples

15:06:43 Session HOL/HOL-Nominal

15:06:43 Session HOL/HOL-Nominal-Examples (timing)

15:06:43 Session HOL/HOL-Predicate_Compile_Examples (timing)

15:06:43 Session HOL/HOL-Quickcheck_Examples (timing)

15:06:44 Session HOL/HOL-SET_Protocol (timing)

15:06:44 Session HOL/HOL-TPTP

15:06:44 Session HOL/HOL-Unix

15:06:44 Session HOL/HOL-ZF

15:06:44 Session Doc/Isar_Ref (doc)

15:06:44 Session Doc/Typeclass_Hierarchy_Basics

15:06:44 Session Doc/Typeclass_Hierarchy (doc)

15:06:44 Session HOL/HOL-Mirabelle

15:06:44 Session HOL/HOL-Mirabelle-ex

15:06:44 Session HOL/HOL-NanoJava

15:06:44 Session HOL/HOL-Prolog

15:06:44 Session HOL/HOL-Statespace

15:06:44 Session HOL/HOL-TLA

15:06:44 Session HOL/HOL-TLA-Buffer

15:06:44 Session HOL/HOL-TLA-Inc

15:06:44 Session HOL/HOL-TLA-Memory

15:06:44 Session HOL/HOL-Types_To_Sets

15:06:44 Session HOL/HOL-Word (main timing)

15:06:45 Session HOL/HOL-SPARK (main)

15:06:45 Session HOL/HOL-SPARK-Examples

15:06:45 Session HOL/HOL-SPARK-Manual

15:06:45 Session HOL/HOL-Word-SMT_Examples (timing)

15:06:45 Session HOL/HOLCF (main timing)

15:06:45 Session HOL/HOLCF-IMP

15:06:45 Session HOL/HOLCF-Library

15:06:46 Session HOL/HOLCF-FOCUS

15:06:46 Session HOL/HOLCF-ex

15:06:46 Session HOL/HOLCF-Tutorial

15:06:46 Session HOL/IOA (timing)

15:06:46 Session HOL/IOA-ABP

15:06:46 Session HOL/IOA-NTP

15:06:46 Session HOL/IOA-Storage

15:06:46 Session HOL/IOA-ex

15:06:46 Session Doc/How_to_Prove_it

15:06:46 Session Doc/Implementation (doc)

15:06:46 Session Doc/JEdit (doc)

15:06:47 Session Doc/Locales (doc)

15:06:47 Session Doc/Main (doc)

15:06:47 Session Doc/Prog_Prove (doc)

15:06:47 Session Doc/Sugar (doc)

15:06:47 Session Doc/Tutorial (doc)

15:06:47 Session HOL/HOL-Proofs (timing)

15:06:47 Session HOL/HOL-Proofs-Extraction (timing)

15:06:48 Session HOL/HOL-Proofs-Lambda (timing)

15:06:48 Session HOL/HOL-Proofs-ex

15:06:48 Session Doc/Intro (doc)

15:06:48 Session LCF/LCF

15:06:48 Session Doc/Logics (doc)

15:06:48 Session Doc/Nitpick (doc)

15:06:48 Session Unsorted/SML

15:06:48 Session Sequents/Sequents

15:06:48 Session Doc/Sledgehammer (doc)

15:06:48 Session Unsorted/Spec_Check

15:06:48 Session Doc/System (doc)

15:06:48 Session ZF/ZF (main timing)

15:06:48 Session Doc/Logics_ZF (doc)

15:06:48 Session ZF/ZF-AC

15:06:48 Session ZF/ZF-Coind

15:06:48 Session ZF/ZF-Constructible

15:06:48 Session ZF/ZF-IMP

15:06:48 Session ZF/ZF-Induct

15:06:48 Session ZF/ZF-UNITY (timing)

15:06:49 Session ZF/ZF-Resid

15:06:49 Session ZF/ZF-ex

15:06:51 Cleaned Pure

15:06:51 Cleaned SML

15:06:51 Cleaned Sequents

15:06:51 Cleaned Sledgehammer

15:06:51 Cleaned Spec_Check

15:06:51 Cleaned System

15:06:51 Cleaned ZF

15:06:51 Cleaned ZF-AC

15:06:51 Cleaned ZF-Coind

15:06:51 Cleaned ZF-Constructible

15:06:51 Cleaned ZF-IMP

15:06:51 Cleaned ZF-Induct

15:06:51 Cleaned ZF-UNITY

15:06:51 Cleaned ZF-Resid

15:06:51 Cleaned ZF-ex

15:06:51 Cleaned Nitpick

15:06:51 Cleaned Logics_ZF

15:06:51 Cleaned Logics

15:06:51 Cleaned LCF

15:06:51 Cleaned Intro

15:06:51 Cleaned HOL-Proofs

15:06:51 Cleaned HOL-Proofs-Extraction

15:06:51 Cleaned HOL-Proofs-Lambda

15:06:51 Cleaned HOL-Proofs-ex

15:06:51 Cleaned HOL

15:06:51 Cleaned HOL-Analysis

15:06:51 Cleaned HOL-Analysis-ex

15:06:51 Cleaned HOL-Probability

15:06:51 Cleaned HOL-Probability-ex

15:06:51 Cleaned HOL-Data_Structures

15:06:51 Cleaned HOL-Eisbach

15:06:51 Cleaned HOL-Hoare

15:06:51 Cleaned HOL-Hoare_Parallel

15:06:51 Cleaned HOL-IMPP

15:06:51 Cleaned HOL-IOA

15:06:51 Cleaned HOL-Import

15:06:51 Cleaned HOL-Lattice

15:06:51 Cleaned HOL-Library

15:06:51 Cleaned HOL-Auth

15:06:51 Cleaned HOL-UNITY

15:06:51 Cleaned HOL-Bali

15:06:51 Cleaned HOL-Cardinals

15:06:51 Cleaned HOL-Computational_Algebra

15:06:51 Cleaned HOL-Algebra

15:06:51 Cleaned HOL-Decision_Procs

15:06:51 Cleaned HOL-Quotient_Examples

15:06:51 Cleaned HOL-Isar_Examples

15:06:51 Cleaned HOL-Nonstandard_Analysis

15:06:51 Cleaned HOL-Nonstandard_Analysis-Examples

15:06:51 Cleaned HOL-Number_Theory

15:06:51 Cleaned HOL-Codegenerator_Test

15:06:51 Cleaned HOL-ex

15:06:51 Cleaned HOL-Corec_Examples

15:06:51 Cleaned HOL-Datatype_Examples

15:06:51 Cleaned HOL-Hahn_Banach

15:06:51 Cleaned HOL-IMP

15:06:51 Cleaned HOL-Imperative_HOL

15:06:51 Cleaned HOL-Induct

15:06:51 Cleaned HOL-Matrix_LP

15:06:51 Cleaned HOL-Metis_Examples

15:06:51 Cleaned HOL-MicroJava

15:06:51 Cleaned HOL-Mutabelle

15:06:51 Cleaned HOL-Nitpick_Examples

15:06:51 Cleaned HOL-Nominal

15:06:51 Cleaned HOL-Nominal-Examples

15:06:51 Cleaned HOL-Predicate_Compile_Examples

15:06:51 Cleaned HOL-Quickcheck_Examples

15:06:51 Cleaned HOL-SET_Protocol

15:06:51 Cleaned HOL-TPTP

15:06:51 Cleaned HOL-Unix

15:06:51 Cleaned HOL-ZF

15:06:51 Cleaned Isar_Ref

15:06:51 Cleaned Typeclass_Hierarchy_Basics

15:06:51 Cleaned Typeclass_Hierarchy

15:06:51 Cleaned HOL-Mirabelle

15:06:51 Cleaned HOL-Mirabelle-ex

15:06:51 Cleaned HOL-NanoJava

15:06:51 Cleaned HOL-Prolog

15:06:51 Cleaned HOL-Statespace

15:06:51 Cleaned HOL-TLA

15:06:51 Cleaned HOL-TLA-Buffer

15:06:51 Cleaned HOL-TLA-Inc

15:06:51 Cleaned HOL-TLA-Memory

15:06:51 Cleaned HOL-Types_To_Sets

15:06:51 Cleaned HOL-Word

15:06:51 Cleaned HOL-SPARK

15:06:51 Cleaned HOL-SPARK-Examples

15:06:51 Cleaned HOL-SPARK-Manual

15:06:51 Cleaned HOL-Word-SMT_Examples

15:06:51 Cleaned HOLCF

15:06:51 Cleaned HOLCF-IMP

15:06:51 Cleaned HOLCF-Library

15:06:51 Cleaned HOLCF-FOCUS

15:06:51 Cleaned HOLCF-ex

15:06:51 Cleaned HOLCF-Tutorial

15:06:51 Cleaned IOA

15:06:51 Cleaned IOA-ABP

15:06:51 Cleaned IOA-NTP

15:06:51 Cleaned IOA-Storage

15:06:51 Cleaned IOA-ex

15:06:51 Cleaned How_to_Prove_it

15:06:51 Cleaned Implementation

15:06:51 Cleaned JEdit

15:06:51 Cleaned Locales

15:06:51 Cleaned Main

15:06:51 Cleaned Prog_Prove

15:06:51 Cleaned Sugar

15:06:51 Cleaned Tutorial

15:06:51 Cleaned Functions

15:06:51 Cleaned FOLP

15:06:51 Cleaned FOLP-ex

15:06:51 Cleaned FOL

15:06:51 Cleaned FOL-ex

15:06:51 Cleaned Eisbach

15:06:51 Cleaned Datatypes

15:06:51 Cleaned Cube

15:06:51 Cleaned Corec

15:06:51 Cleaned Codegen_Basics

15:06:51 Cleaned Codegen

15:06:51 Cleaned Classes

15:06:51 Cleaned CTT

15:06:51 Cleaned CCL

15:06:51 Building Pure ...

15:07:10 Pure: theory Pure

15:07:11 Pure: theory ML_Bootstrap

15:07:11 Pure: theory Pure.Sessions

15:07:14 Timing Pure (1 threads, 0.920s elapsed time, 0.920s cpu time, 0.000s GC time, factor 1.00)

15:07:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Pure/Pure

15:07:14 Finished Pure (0:00:21 elapsed time, 0:00:21 cpu time, factor 0.98)

15:07:14 Building HOL ...

15:07:14 Building ZF ...

15:07:15 Building HOL-Proofs ...

15:07:16 ZF: theory IFOL

15:07:17 ZF: theory FOL

15:07:17 HOL-Proofs: theory HOL.Code_Generator

15:07:18 HOL: theory HOL.Code_Generator

15:07:19 ZF: theory ZF.ZF_Base

15:07:19 ZF: theory ZF.upair

15:07:20 ZF: theory ZF.pair

15:07:20 ZF: theory ZF.Bool

15:07:20 ZF: theory ZF.equalities

15:07:21 HOL-Proofs: theory HOL.HOL

15:07:21 ZF: theory ZF.Fixedpt

15:07:21 ZF: theory ZF.Sum

15:07:21 ZF: theory ZF.func

15:07:21 HOL: theory HOL.HOL

15:07:22 ZF: theory ZF.Perm

15:07:22 ZF: theory ZF.QPair

15:07:22 ZF: theory ZF.Trancl

15:07:22 ZF: theory ZF.EquivClass

15:07:22 ZF: theory ZF.WF

15:07:22 ZF: theory ZF.Order

15:07:22 ZF: theory ZF.Ordinal

15:07:22 ZF: theory ZF.OrdQuant

15:07:22 ZF: theory ZF.OrderArith

15:07:23 ZF: theory ZF.Nat_ZF

15:07:23 ZF: theory ZF.Epsilon

15:07:23 ZF: theory ZF.OrderType

15:07:23 ZF: theory ZF.Inductive_ZF

15:07:24 ZF: theory ZF.Finite

15:07:24 ZF: theory ZF.Cardinal

15:07:25 ZF: theory ZF.Univ

15:07:25 ZF: theory ZF.Arith

15:07:25 ZF: theory ZF.QUniv

15:07:25 ZF: theory ZF.Datatype_ZF

15:07:25 ZF: theory ZF.ArithSimp

15:07:26 ZF: theory ZF.Int_ZF

15:07:26 ZF: theory ZF.CardinalArith

15:07:26 HOL: theory HOL.Ctr_Sugar

15:07:26 HOL: theory HOL.Argo

15:07:26 ZF: theory ZF.List_ZF

15:07:26 HOL-Proofs: theory HOL.Ctr_Sugar

15:07:26 HOL-Proofs: theory HOL.Argo

15:07:27 ZF: theory ZF.Bin

15:07:27 ZF: theory ZF.IntDiv_ZF

15:07:28 HOL: theory HOL.Orderings

15:07:28 HOL-Proofs: theory HOL.Orderings

15:07:28 ZF: theory ZF

15:07:28 HOL-Proofs: theory HOL.SAT

15:07:29 HOL: theory HOL.SAT

15:07:29 ZF: theory ZF.AC

15:07:29 ZF: theory ZF.Zorn

15:07:29 ZF: theory ZF.Cardinal_AC

15:07:29 ZF: theory ZF.InfDatatype

15:07:29 ZF: theory ZFC

15:07:29 HOL: theory HOL.Groups

15:07:30 HOL-Proofs: theory HOL.Groups

15:07:32 HOL: theory HOL.Lattices

15:07:34 HOL-Proofs: theory HOL.Lattices

15:07:34 HOL: theory HOL.Set

15:07:36 HOL: theory HOL.Fun

15:07:36 HOL: theory HOL.Typedef

15:07:37 HOL: theory HOL.Rings

15:07:37 HOL: theory HOL.Complete_Lattices

15:07:38 HOL-Proofs: theory HOL.Set

15:07:40 HOL: theory HOL.Inductive

15:07:43 HOL: theory HOL.Product_Type

15:07:44 HOL: theory HOL.Complete_Partial_Order

15:07:45 HOL: theory HOL.Sum_Type

15:07:47 HOL-Proofs: theory HOL.Fun

15:07:48 HOL: theory HOL.Nat

15:07:48 HOL-Proofs: theory HOL.Typedef

15:07:49 HOL-Proofs: theory HOL.Rings

15:07:50 HOL: theory HOL.Fields

15:07:50 HOL: theory HOL.Meson

15:07:50 HOL-Proofs: theory HOL.Complete_Lattices

15:07:50 HOL: theory HOL.ATP

15:07:54 HOL: theory HOL.Metis

15:07:55 HOL: theory HOL.Finite_Set

15:07:55 Timing ZF (2 threads, 26.312s elapsed time, 42.060s cpu time, 2.596s GC time, factor 1.60)

15:07:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF

15:07:55 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/document.pdf

15:07:55 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/outline.pdf

15:07:55 Finished ZF (0:00:40 elapsed time, 0:01:05 cpu time, factor 1.63)

15:07:55 Building ZF-Induct ...

15:07:56 ZF-Induct: theory ZF-Induct.Binary_Trees

15:07:56 ZF-Induct: theory ZF-Induct.Acc

15:07:56 ZF-Induct: theory ZF-Induct.Comb

15:07:56 ZF-Induct: theory ZF-Induct.Datatypes

15:07:56 ZF-Induct: theory ZF-Induct.FoldSet

15:07:56 ZF-Induct: theory ZF-Induct.ListN

15:07:56 ZF-Induct: theory ZF-Induct.Mutil

15:07:56 HOL: theory HOL.Relation

15:07:56 ZF-Induct: theory ZF-Induct.Ntree

15:07:56 ZF-Induct: theory ZF-Induct.Multiset

15:07:56 ZF-Induct: theory ZF-Induct.Primrec

15:07:56 ZF-Induct: theory ZF-Induct.PropLog

15:07:57 ZF-Induct: theory ZF-Induct.Rmap

15:07:57 ZF-Induct: theory ZF-Induct.Term

15:07:57 ZF-Induct: theory ZF-Induct.Tree_Forest

15:07:57 ZF-Induct: theory ZF-Induct.Brouwer

15:07:58 HOL: theory HOL.Transitive_Closure

15:07:58 HOL-Proofs: theory HOL.Inductive

15:07:59 HOL: theory HOL.Wellfounded

15:08:00 HOL: theory HOL.Fun_Def_Base

15:08:00 HOL: theory HOL.Hilbert_Choice

15:08:00 HOL: theory HOL.Wfrec

15:08:00 HOL: theory HOL.Order_Relation

15:08:01 HOL: theory HOL.BNF_Wellorder_Relation

15:08:01 HOL: theory HOL.BNF_Wellorder_Embedding

15:08:01 HOL: theory HOL.Zorn

15:08:01 HOL: theory HOL.BNF_Wellorder_Constructions

15:08:02 HOL-Proofs: theory HOL.Product_Type

15:08:02 HOL: theory HOL.BNF_Cardinal_Order_Relation

15:08:03 HOL: theory HOL.BNF_Cardinal_Arithmetic

15:08:03 HOL: theory HOL.BNF_Def

15:08:06 HOL-Proofs: theory HOL.Complete_Partial_Order

15:08:06 HOL-Proofs: theory HOL.Sum_Type

15:08:06 HOL: theory HOL.BNF_Composition

15:08:06 HOL: theory HOL.Basic_BNFs

15:08:07 HOL-Proofs: theory HOL.Nat

15:08:07 HOL: theory HOL.BNF_Fixpoint_Base

15:08:10 Timing ZF-Induct (2 threads, 7.375s elapsed time, 11.928s cpu time, 0.532s GC time, factor 1.62)

15:08:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct

15:08:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/document.pdf

15:08:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/outline.pdf

15:08:10 Finished ZF-Induct (0:00:14 elapsed time, 0:00:23 cpu time, factor 1.62)

15:08:10 Building FOL ...

15:08:11 FOL: theory IFOL

15:08:11 HOL-Proofs: theory HOL.Fields

15:08:11 HOL-Proofs: theory HOL.Meson

15:08:11 HOL: theory HOL.BNF_Least_Fixpoint

15:08:12 HOL-Proofs: theory HOL.ATP

15:08:12 FOL: theory FOL

15:08:14 HOL: theory HOL.Basic_BNF_LFPs

15:08:15 HOL: theory HOL.Transfer

15:08:15 HOL-Proofs: theory HOL.Metis

15:08:16 HOL: theory HOL.Num

15:08:19 HOL: theory HOL.Power

15:08:19 Timing FOL (2 threads, 3.513s elapsed time, 3.844s cpu time, 0.160s GC time, factor 1.09)

15:08:19 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL

15:08:19 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/document.pdf

15:08:19 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/outline.pdf

15:08:19 Finished FOL (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.37)

15:08:19 Building FOLP ...

15:08:19 FOLP: theory IFOLP

15:08:20 FOLP: theory FOLP

15:08:21 HOL-Proofs: theory HOL.Finite_Set

15:08:21 HOL: theory HOL.Groups_Big

15:08:22 Timing FOLP (2 threads, 1.205s elapsed time, 1.216s cpu time, 0.000s GC time, factor 1.01)

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

15:08:22 Finished FOLP (0:00:02 elapsed time)

15:08:22 Running ZF-UNITY ...

15:08:22 ZF-UNITY: theory ZF-UNITY.GenPrefix

15:08:22 ZF-UNITY: theory ZF-UNITY.MultisetSum

15:08:22 ZF-UNITY: theory ZF-UNITY.State

15:08:22 ZF-UNITY: theory ZF-UNITY.UNITY

15:08:22 ZF-UNITY: theory ZF-UNITY.Monotonicity

15:08:23 ZF-UNITY: theory ZF-UNITY.Constrains

15:08:23 ZF-UNITY: theory ZF-UNITY.FP

15:08:23 ZF-UNITY: theory ZF-UNITY.WFair

15:08:23 ZF-UNITY: theory ZF-UNITY.Increasing

15:08:23 HOL: theory HOL.Equiv_Relations

15:08:23 ZF-UNITY: theory ZF-UNITY.SubstAx

15:08:23 HOL: theory HOL.Lifting

15:08:24 ZF-UNITY: theory ZF-UNITY.Follows

15:08:24 ZF-UNITY: theory ZF-UNITY.Mutex

15:08:24 ZF-UNITY: theory ZF-UNITY.Union

15:08:24 ZF-UNITY: theory ZF-UNITY.Comp

15:08:25 ZF-UNITY: theory ZF-UNITY.Guar

15:08:25 ZF-UNITY: theory ZF-UNITY.AllocBase

15:08:25 HOL: theory HOL.Lifting_Set

15:08:26 ZF-UNITY: theory ZF-UNITY.ClientImpl

15:08:26 ZF-UNITY: theory ZF-UNITY.Distributor

15:08:26 HOL: theory HOL.Option

15:08:26 HOL: theory HOL.Quotient

15:08:26 ZF-UNITY: theory ZF-UNITY.Merge

15:08:26 ZF-UNITY: theory ZF-UNITY.AllocImpl

15:08:26 HOL: theory HOL.Extraction

15:08:28 HOL: theory HOL.Lattices_Big

15:08:29 HOL: theory HOL.Partial_Function

15:08:29 HOL-Proofs: theory HOL.Relation

15:08:30 HOL: theory HOL.Fun_Def

15:08:32 HOL: theory HOL.Int

15:08:33 HOL-Proofs: theory HOL.Transitive_Closure

15:08:35 HOL: theory HOL.Euclidean_Division

15:08:38 HOL-Proofs: theory HOL.Wellfounded

15:08:39 HOL: theory HOL.Parity

15:08:40 Timing ZF-UNITY (2 threads, 16.818s elapsed time, 31.056s cpu time, 1.140s GC time, factor 1.85)

15:08:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-UNITY

15:08:40 Finished ZF-UNITY (0:00:17 elapsed time, 0:00:31 cpu time, factor 1.78)

15:08:40 Running ZF-Constructible ...

15:08:40 ZF-Constructible: theory ZF-Constructible.MetaExists

15:08:40 ZF-Constructible: theory ZF-Constructible.Formula

15:08:40 ZF-Constructible: theory ZF-Constructible.Normal

15:08:40 ZF-Constructible: theory ZF-Constructible.Reflection

15:08:40 HOL-Proofs: theory HOL.Fun_Def_Base

15:08:41 ZF-Constructible: theory ZF-Constructible.Relative

15:08:41 HOL-Proofs: theory HOL.Hilbert_Choice

15:08:42 HOL: theory HOL.Divides

15:08:43 ZF-Constructible: theory ZF-Constructible.L_axioms

15:08:43 ZF-Constructible: theory ZF-Constructible.Wellorderings

15:08:43 ZF-Constructible: theory ZF-Constructible.WFrec

15:08:43 HOL-Proofs: theory HOL.Wfrec

15:08:44 ZF-Constructible: theory ZF-Constructible.WF_absolute

15:08:44 HOL-Proofs: theory HOL.Order_Relation

15:08:44 HOL: theory HOL.Code_Numeral

15:08:44 HOL: theory HOL.Numeral_Simprocs

15:08:45 ZF-Constructible: theory ZF-Constructible.Datatype_absolute

15:08:45 ZF-Constructible: theory ZF-Constructible.Rank

15:08:45 HOL-Proofs: theory HOL.BNF_Wellorder_Relation

15:08:45 HOL-Proofs: theory HOL.Zorn

15:08:46 HOL: theory HOL.SMT

15:08:46 HOL: theory HOL.Semiring_Normalization

15:08:46 ZF-Constructible: theory ZF-Constructible.Separation

15:08:46 ZF-Constructible: theory ZF-Constructible.Internalize

15:08:46 ZF-Constructible: theory ZF-Constructible.AC_in_L

15:08:48 HOL: theory HOL.Set_Interval

15:08:48 ZF-Constructible: theory ZF-Constructible.Rec_Separation

15:08:48 HOL: theory HOL.Groebner_Basis

15:08:48 ZF-Constructible: theory ZF-Constructible.Rank_Separation

15:08:48 ZF-Constructible: theory ZF-Constructible.Satisfies_absolute

15:08:49 HOL-Proofs: theory HOL.BNF_Wellorder_Embedding

15:08:50 ZF-Constructible: theory ZF-Constructible.DPow_absolute

15:08:51 HOL-Proofs: theory HOL.BNF_Wellorder_Constructions

15:08:52 HOL: theory HOL.Conditionally_Complete_Lattices

15:08:52 HOL: theory HOL.Filter

15:08:53 HOL: theory HOL.Presburger

15:08:56 HOL: theory HOL.Sledgehammer

15:08:57 HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation

15:08:58 HOL: theory HOL.List

15:09:05 Timing ZF-Constructible (2 threads, 18.026s elapsed time, 34.628s cpu time, 7.300s GC time, factor 1.92)

15:09:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible

15:09:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/document.pdf

15:09:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/outline.pdf

15:09:05 Finished ZF-Constructible (0:00:24 elapsed time, 0:00:46 cpu time, factor 1.87)

15:09:05 Running ZF-ex ...

15:09:05 ZF-ex: theory ZF-ex.BinEx

15:09:05 ZF-ex: theory ZF-ex.CoUnit

15:09:05 ZF-ex: theory ZF-ex.Commutation

15:09:05 ZF-ex: theory ZF-ex.Group

15:09:05 HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic

15:09:05 ZF-ex: theory ZF-ex.LList

15:09:05 ZF-ex: theory ZF-ex.Limit

15:09:06 ZF-ex: theory ZF-ex.Ring

15:09:06 HOL-Proofs: theory HOL.BNF_Def

15:09:07 ZF-ex: theory ZF-ex.NatSum

15:09:07 ZF-ex: theory ZF-ex.Primes

15:09:07 ZF-ex: theory ZF-ex.Ramsey

15:09:07 ZF-ex: theory ZF-ex.misc

15:09:08 HOL: theory HOL.Groups_List

15:09:08 HOL: theory HOL.Map

15:09:08 HOL: theory HOL.Factorial

15:09:08 HOL: theory HOL.GCD

15:09:09 HOL: theory HOL.Binomial

15:09:09 HOL: theory HOL.Enum

15:09:09 HOL-Proofs: theory HOL.BNF_Composition

15:09:09 HOL-Proofs: theory HOL.Basic_BNFs

15:09:11 HOL-Proofs: theory HOL.BNF_Fixpoint_Base

15:09:13 HOL: theory HOL.String

15:09:14 HOL: theory HOL.Random

15:09:14 HOL: theory HOL.BNF_Greatest_Fixpoint

15:09:15 HOL: theory HOL.Predicate

15:09:15 HOL-Proofs: theory HOL.BNF_Least_Fixpoint

15:09:16 HOL: theory HOL.Lazy_Sequence

15:09:17 HOL: theory HOL.Limited_Sequence

15:09:17 Timing ZF-ex (2 threads, 11.312s elapsed time, 16.588s cpu time, 0.536s GC time, factor 1.47)

15:09:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-ex

15:09:17 Finished ZF-ex (0:00:12 elapsed time, 0:00:17 cpu time, factor 1.39)

15:09:17 Running CCL ...

15:09:17 CCL: theory IFOL

15:09:18 HOL: theory HOL.Typerep

15:09:19 CCL: theory FOL

15:09:19 HOL: theory HOL.Code_Evaluation

15:09:20 HOL-Proofs: theory HOL.Basic_BNF_LFPs

15:09:20 HOL-Proofs: theory HOL.Transfer

15:09:20 HOL: theory HOL.Quickcheck_Random

15:09:21 CCL: theory CCL.Set

15:09:21 CCL: theory CCL.Lfp

15:09:21 CCL: theory CCL.Gfp

15:09:21 CCL: theory CCL.CCL

15:09:22 CCL: theory CCL.Term

15:09:22 CCL: theory CCL.Trancl

15:09:22 HOL-Proofs: theory HOL.Num

15:09:22 CCL: theory CCL.Type

15:09:23 CCL: theory CCL.Fix

15:09:23 CCL: theory CCL.Hered

15:09:23 CCL: theory CCL.Wfd

15:09:23 HOL: theory HOL.Quickcheck_Exhaustive

15:09:23 HOL: theory HOL.Quickcheck_Narrowing

15:09:23 CCL: theory CCL.Nat

15:09:23 CCL: theory CCL.List

15:09:24 CCL: theory CCL.Flag

15:09:24 CCL: theory CCL.Stream

15:09:25 Timing CCL (2 threads, 6.596s elapsed time, 9.292s cpu time, 0.652s GC time, factor 1.41)

15:09:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CCL/CCL

15:09:25 Finished CCL (0:00:07 elapsed time, 0:00:09 cpu time, factor 1.29)

15:09:25 Running ZF-AC ...

15:09:25 ZF-AC: theory ZF-AC.AC_Equiv

15:09:25 ZF-AC: theory ZF-AC.AC18_AC19

15:09:25 ZF-AC: theory ZF-AC.AC7_AC9

15:09:25 ZF-AC: theory ZF-AC.Cardinal_aux

15:09:25 ZF-AC: theory ZF-AC.Hartog

15:09:25 ZF-AC: theory ZF-AC.HH

15:09:25 ZF-AC: theory ZF-AC.WO6_WO1

15:09:26 ZF-AC: theory ZF-AC.AC16_lemmas

15:09:26 ZF-AC: theory ZF-AC.AC16_WO4

15:09:26 ZF-AC: theory ZF-AC.DC

15:09:26 HOL-Proofs: theory HOL.Power

15:09:26 ZF-AC: theory ZF-AC.AC15_WO6

15:09:26 ZF-AC: theory ZF-AC.AC17_AC1

15:09:26 ZF-AC: theory ZF-AC.WO1_AC

15:09:26 ZF-AC: theory ZF-AC.WO1_WO7

15:09:26 ZF-AC: theory ZF-AC.WO2_AC16

15:09:27 HOL: theory HOL.Random_Pred

15:09:27 HOL: theory HOL.Record

15:09:27 HOL: theory HOL.Random_Sequence

15:09:28 HOL: theory HOL.Predicate_Compile

15:09:30 HOL: theory HOL.Nitpick

15:09:30 HOL-Proofs: theory HOL.Groups_Big

15:09:36 Timing ZF-AC (2 threads, 6.589s elapsed time, 11.084s cpu time, 0.616s GC time, factor 1.68)

15:09:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC

15:09:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/document.pdf

15:09:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/outline.pdf

15:09:36 Finished ZF-AC (0:00:11 elapsed time, 0:00:18 cpu time, factor 1.65)

15:09:36 Running FOL-ex ...

15:09:37 FOL-ex: theory FOL-ex.If

15:09:37 FOL-ex: theory FOL-ex.Classical

15:09:37 FOL-ex: theory FOL-ex.Intro

15:09:37 FOL-ex: theory FOL-ex.Miniscope

15:09:37 FOL-ex: theory FOL-ex.Nat

15:09:37 FOL-ex: theory FOL-ex.Nat_Class

15:09:37 FOL-ex: theory FOL-ex.Natural_Numbers

15:09:37 FOL-ex: theory FOL-ex.Prolog

15:09:37 FOL-ex: theory FOL-ex.Propositional_Cla

15:09:37 FOL-ex: theory FOL-ex.Quantifiers_Cla

15:09:37 FOL-ex: theory FOL-ex.Foundation

15:09:37 FOL-ex: theory FOL-ex.Intuitionistic

15:09:37 FOL-ex: theory FOL-ex.Propositional_Int

15:09:37 FOL-ex: theory FOL-ex.Quantifiers_Int

15:09:37 HOL: theory HOL.Nunchaku

15:09:38 HOL-Proofs: theory HOL.Equiv_Relations

15:09:38 HOL: theory Main

15:09:40 FOL-ex: theory FOL-ex.Locale_Test1

15:09:40 HOL: theory HOL.Archimedean_Field

15:09:40 HOL: theory HOL.Hull

15:09:41 HOL: theory HOL.Modules

15:09:41 HOL-Proofs: theory HOL.Lifting

15:09:41 HOL: theory HOL.Vector_Spaces

15:09:42 FOL-ex: theory FOL-ex.Locale_Test2

15:09:42 FOL-ex: theory FOL-ex.Locale_Test3

15:09:42 FOL-ex: theory FOL-ex.Locale_Test

15:09:43 HOL: theory HOL.Topological_Spaces

15:09:45 HOL: theory HOL.Rat

15:09:46 HOL-Proofs: theory HOL.Lifting_Set

15:09:47 HOL: theory HOL.Real

15:09:47 HOL-Proofs: theory HOL.Option

15:09:47 HOL-Proofs: theory HOL.Quotient

15:09:47 Timing FOL-ex (2 threads, 5.994s elapsed time, 8.404s cpu time, 0.252s GC time, factor 1.40)

15:09:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex

15:09:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/document.pdf

15:09:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/outline.pdf

15:09:47 Finished FOL-ex (0:00:10 elapsed time, 0:00:16 cpu time, factor 1.50)

15:09:47 Running FOLP-ex ...

15:09:48 FOLP-ex: theory FOLP-ex.Classical

15:09:48 FOLP-ex: theory FOLP-ex.If

15:09:48 FOLP-ex: theory FOLP-ex.Intro

15:09:48 FOLP-ex: theory FOLP-ex.Nat

15:09:48 FOLP-ex: theory FOLP-ex.Propositional_Cla

15:09:48 FOLP-ex: theory FOLP-ex.Quantifiers_Cla

15:09:49 FOLP-ex: theory FOLP-ex.Foundation

15:09:49 FOLP-ex: theory FOLP-ex.Intuitionistic

15:09:50 FOLP-ex: theory FOLP-ex.Propositional_Int

15:09:50 HOL-Proofs: theory HOL.Extraction

15:09:50 FOLP-ex: theory FOLP-ex.Quantifiers_Int

15:09:51 HOL-Proofs: theory HOL.Lattices_Big

15:09:51 HOL: theory HOL.Real_Vector_Spaces

15:09:52 Timing FOLP-ex (2 threads, 3.963s elapsed time, 6.828s cpu time, 0.092s GC time, factor 1.72)

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

15:09:53 Finished FOLP-ex (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.49)

15:09:53 Running Sequents ...

15:09:53 Sequents: theory Sequents.Sequents

15:09:53 Sequents: theory Sequents.LK0

15:09:53 Sequents: theory Sequents.ILL

15:09:53 Sequents: theory Sequents.ILL_predlog

15:09:53 Sequents: theory Sequents.Washing

15:09:53 Sequents: theory Sequents.LK

15:09:53 Sequents: theory Sequents.Modal0

15:09:53 Sequents: theory Sequents.S4

15:09:53 Sequents: theory Sequents.Hard_Quantifiers

15:09:53 Sequents: theory Sequents.Nat

15:09:53 Sequents: theory Sequents.Propositional

15:09:53 Sequents: theory Sequents.Quantifiers

15:09:53 Sequents: theory Sequents.S43

15:09:53 Sequents: theory Sequents.T

15:09:55 HOL-Proofs: theory HOL.Partial_Function

15:09:57 HOL-Proofs: theory HOL.Fun_Def

15:09:58 Timing Sequents (2 threads, 3.746s elapsed time, 7.256s cpu time, 0.140s GC time, factor 1.94)

15:09:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Sequents/Sequents

15:09:58 Finished Sequents (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.67)

15:09:58 Running LCF ...

15:09:58 LCF: theory IFOL

15:09:59 LCF: theory FOL

15:09:59 HOL-Proofs: theory HOL.Int

15:10:01 LCF: theory LCF.LCF

15:10:01 LCF: theory LCF.Ex1

15:10:01 LCF: theory LCF.Ex2

15:10:01 LCF: theory LCF.Ex3

15:10:01 LCF: theory LCF.Ex4

15:10:02 HOL: theory HOL.Inequalities

15:10:02 HOL: theory HOL.Limits

15:10:03 Timing LCF (2 threads, 3.746s elapsed time, 4.224s cpu time, 0.152s GC time, factor 1.13)

15:10:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/LCF/LCF

15:10:03 Finished LCF (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.00)

15:10:03 Running Spec_Check ...

15:10:03 Spec_Check: theory Spec_Check.Spec_Check

15:10:03 Spec_Check: theory Spec_Check.Examples

15:10:06 Timing Spec_Check (2 threads, 1.942s elapsed time, 3.244s cpu time, 0.020s GC time, factor 1.67)

15:10:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/Spec_Check

15:10:06 Finished Spec_Check (0:00:02 elapsed time, 0:00:03 cpu time)

15:10:06 Running ZF-Resid ...

15:10:06 ZF-Resid: theory ZF-Resid.Redex

15:10:06 HOL-Proofs: theory HOL.Euclidean_Division

15:10:06 ZF-Resid: theory ZF-Resid.Substitution

15:10:06 ZF-Resid: theory ZF-Resid.Residuals

15:10:06 HOL: theory HOL.Deriv

15:10:07 ZF-Resid: theory ZF-Resid.Reduction

15:10:07 ZF-Resid: theory ZF-Resid.Confluence

15:10:08 HOL: theory HOL.NthRoot

15:10:09 Timing ZF-Resid (2 threads, 1.757s elapsed time, 2.832s cpu time, 0.000s GC time, factor 1.61)

15:10:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Resid

15:10:09 Finished ZF-Resid (0:00:02 elapsed time, 0:00:03 cpu time)

15:10:09 Running ZF-IMP ...

15:10:09 HOL: theory HOL.Series

15:10:09 ZF-IMP: theory ZF-IMP.Com

15:10:09 ZF-IMP: theory ZF-IMP.Denotation

15:10:09 ZF-IMP: theory ZF-IMP.Equiv

15:10:10 HOL: theory HOL.Transcendental

15:10:14 Timing ZF-IMP (2 threads, 1.146s elapsed time, 1.328s cpu time, 0.000s GC time, factor 1.16)

15:10:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP

15:10:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP/document.pdf

15:10:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP/outline.pdf

15:10:14 Finished ZF-IMP (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.59)

15:10:14 Running CTT ...

15:10:14 CTT: theory CTT.CTT

15:10:15 CTT: theory CTT.Elimination

15:10:15 CTT: theory CTT.Equality

15:10:15 CTT: theory CTT.Synthesis

15:10:15 CTT: theory CTT.Typechecking

15:10:15 HOL: theory HOL.Complex

15:10:15 HOL: theory HOL.MacLaurin

15:10:17 HOL: theory Complex_Main

15:10:17 HOL-Proofs: theory HOL.Parity

15:10:19 Timing CTT (2 threads, 1.031s elapsed time, 1.424s cpu time, 0.000s GC time, factor 1.38)

15:10:19 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT

15:10:19 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/document.pdf

15:10:19 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/outline.pdf

15:10:19 Finished CTT (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.63)

15:10:19 Running ZF-Coind ...

15:10:19 ZF-Coind: theory ZF-Coind.Language

15:10:19 ZF-Coind: theory ZF-Coind.Map

15:10:19 ZF-Coind: theory ZF-Coind.Types

15:10:19 ZF-Coind: theory ZF-Coind.Values

15:10:19 ZF-Coind: theory ZF-Coind.Dynamic

15:10:19 ZF-Coind: theory ZF-Coind.Static

15:10:19 ZF-Coind: theory ZF-Coind.ECR

15:10:20 Timing ZF-Coind (2 threads, 0.742s elapsed time, 1.432s cpu time, 0.000s GC time, factor 1.93)

15:10:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Coind

15:10:20 Finished ZF-Coind (0:00:01 elapsed time)

15:10:20 Running System ...

15:10:20 System: theory System.Base

15:10:21 System: theory System.Environment

15:10:21 System: theory System.Misc

15:10:21 System: theory System.Presentation

15:10:21 System: theory System.Scala

15:10:21 System: theory System.Server

15:10:21 System: theory System.Sessions

15:10:23 HOL-Proofs: theory HOL.Divides

15:10:25 Timing System (2 threads, 0.453s elapsed time, 0.692s cpu time, 0.000s GC time, factor 1.53)

15:10:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System

15:10:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System/system.pdf

15:10:25 Finished System (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.10)

15:10:25 Running Cube ...

15:10:25 Cube: theory Cube.Cube

15:10:26 Cube: theory Cube.Example

15:10:26 Timing Cube (2 threads, 0.334s elapsed time, 0.340s cpu time, 0.000s GC time, factor 1.02)

15:10:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Cube/Cube

15:10:26 Finished Cube (0:00:00 elapsed time)

15:10:26 Running Intro ...

15:10:30 Timing Intro (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

15:10:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro

15:10:30 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro/intro.pdf

15:10:30 Finished Intro (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.04)

15:10:30 Running Logics ...

15:10:35 Timing Logics (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

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

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

15:10:35 Finished Logics (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.01)

15:10:35 Running Logics_ZF ...

15:10:35 Logics_ZF: theory Logics_ZF.FOL_examples

15:10:35 Logics_ZF: theory Logics_ZF.If

15:10:35 Logics_ZF: theory Logics_ZF.ZF_Isar

15:10:35 Logics_ZF: theory Logics_ZF.ZF_examples

15:10:35 Logics_ZF: theory Logics_ZF.IFOL_examples

15:10:37 HOL-Proofs: theory HOL.Code_Numeral

15:10:37 HOL-Proofs: theory HOL.Numeral_Simprocs

15:10:40 Timing Logics_ZF (2 threads, 0.299s elapsed time, 0.564s cpu time, 0.000s GC time, factor 1.89)

15:10:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF

15:10:40 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF/logics-ZF.pdf

15:10:40 Finished Logics_ZF (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.09)

15:10:40 Running Nitpick ...

15:10:45 Timing Nitpick (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

15:10:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick

15:10:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick/nitpick.pdf

15:10:45 Finished Nitpick (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.07)

15:10:45 Running SML ...

15:10:45 SML: theory SML.Examples

15:10:45 HOL-Proofs: theory HOL.Semiring_Normalization

15:10:45 HOL-Proofs: theory HOL.SMT

15:10:46 Timing SML (2 threads, 0.023s elapsed time, 0.024s cpu time, 0.000s GC time, factor 1.05)

15:10:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/SML

15:10:46 Finished SML (0:00:00 elapsed time)

15:10:46 Running Sledgehammer ...

15:10:48 HOL-Proofs: theory HOL.Set_Interval

15:10:49 HOL-Proofs: theory HOL.Groebner_Basis

15:10:50 Timing Sledgehammer (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)

15:10:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer

15:10:50 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer/sledgehammer.pdf

15:10:50 Finished Sledgehammer (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.09)

15:11:02 HOL-Proofs: theory HOL.Conditionally_Complete_Lattices

15:11:02 HOL-Proofs: theory HOL.Filter

15:11:22 HOL-Proofs: theory HOL.Presburger

15:11:34 HOL-Proofs: theory HOL.Sledgehammer

15:11:36 HOL-Proofs: theory HOL.List

15:13:58 Timing HOL (2 threads, 307.300s elapsed time, 566.036s cpu time, 58.224s GC time, factor 1.84)

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

15:13:58 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/document.pdf

15:13:58 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/outline.pdf

15:13:58 Finished HOL (0:06:40 elapsed time, 0:11:50 cpu time, factor 1.77)

15:13:58 Building HOL-Library ...

15:13:59 Building HOLCF ...

15:14:00 HOLCF: theory HOL-Library.Old_Datatype

15:14:00 HOLCF: theory HOL-Library.Nat_Bijection

15:14:00 HOL-Library: theory HOL-Library.Lattice_Syntax

15:14:00 HOL-Library: theory HOL-Library.AList

15:14:00 HOL-Library: theory HOL-Library.Adhoc_Overloading

15:14:00 HOL-Library: theory HOL-Library.Monad_Syntax

15:14:00 HOL-Library: theory HOL-Library.State_Monad

15:14:00 HOLCF: theory HOLCF.Porder

15:14:01 HOLCF: theory HOL-Library.Countable

15:14:01 HOLCF: theory HOLCF.Pcpo

15:14:01 HOL-Library: theory HOL-Library.BNF_Axiomatization

15:14:02 HOL-Library: theory HOL-Library.BNF_Corec

15:14:02 HOL-Library: theory HOL-Library.DAList

15:14:02 HOLCF: theory HOLCF.Cont

15:14:03 HOLCF: theory HOLCF.Adm

15:14:03 HOLCF: theory HOLCF.Discrete

15:14:03 HOLCF: theory HOLCF.Cpodef

15:14:03 HOLCF: theory HOLCF.Fun_Cpo

15:14:03 HOLCF: theory HOLCF.Product_Cpo

15:14:03 HOLCF: theory HOLCF.Cfun

15:14:03 HOL-Library: theory HOL-Library.Bit

15:14:04 HOL-Library: theory HOL-Library.Boolean_Algebra

15:14:04 HOLCF: theory HOLCF.Completion

15:14:04 HOLCF: theory HOLCF.Cprod

15:14:04 HOLCF: theory HOLCF.Deflation

15:14:04 HOL-Library: theory HOL-Library.Cancellation

15:14:05 HOLCF: theory HOLCF.Fix

15:14:05 HOLCF: theory HOLCF.Sfun

15:14:05 HOLCF: theory HOLCF.Sprod

15:14:05 HOLCF: theory HOLCF.Up

15:14:05 HOL-Proofs: theory HOL.Groups_List

15:14:05 HOL-Library: theory HOL-Library.Multiset

15:14:06 HOLCF: theory HOLCF.Lift

15:14:07 HOLCF: theory HOLCF.One

15:14:07 HOLCF: theory HOLCF.Tr

15:14:07 HOLCF: theory HOLCF.Ssum

15:14:07 HOLCF: theory HOLCF.Fixrec

15:14:07 HOLCF: theory HOLCF.Map_Functions

15:14:07 HOL-Proofs: theory HOL.Factorial

15:14:08 HOLCF: theory HOLCF.Bifinite

15:14:08 HOLCF: theory HOLCF.Domain_Aux

15:14:09 HOLCF: theory HOLCF.Universal

15:14:10 HOL-Library: theory HOL-Library.Cardinal_Notations

15:14:10 HOL-Library: theory HOL-Library.Char_ord

15:14:10 HOL-Library: theory HOL-Library.Code_Abstract_Nat

15:14:10 HOL-Library: theory HOL-Library.Code_Binary_Nat

15:14:10 HOL-Library: theory HOL-Library.Code_Target_Nat

15:14:10 HOL-Library: theory HOL-Library.Code_Lazy

15:14:11 HOL-Proofs: theory HOL.Binomial

15:14:11 HOLCF: theory HOLCF.Algebraic

15:14:11 HOLCF: theory HOLCF.Compact_Basis

15:14:11 HOL-Library: theory HOL-Library.DAList_Multiset

15:14:11 HOLCF: theory HOLCF.LowerPD

15:14:11 HOLCF: theory HOLCF.UpperPD

15:14:11 HOL-Library: theory HOL-Library.Multiset_Order

15:14:11 HOLCF: theory HOLCF.Representable

15:14:11 HOLCF: theory HOLCF.ConvexPD

15:14:11 HOL-Library: theory HOL-Library.Permutation

15:14:12 HOL-Library: theory HOL-Library.Code_Prolog

15:14:12 HOL-Library: theory HOL-Library.Code_Target_Int

15:14:12 HOL-Library: theory HOL-Library.Code_Target_Numeral

15:14:12 HOL-Library: theory HOL-Library.Code_Test

15:14:12 HOL-Library: theory HOL-Library.Combine_PER

15:14:13 HOL-Library: theory HOL-Library.Complete_Partial_Order2

15:14:13 HOL-Library: theory HOL-Library.Conditional_Parametricity

15:14:13 HOL-Library: theory HOL-Library.Datatype_Records

15:14:14 HOL-Library: theory HOL-Library.Debug

15:14:14 HOL-Library: theory HOL-Library.Disjoint_Sets

15:14:14 HOLCF: theory HOLCF.Domain

15:14:14 HOL-Library: theory HOL-Library.Permutations

15:14:16 HOL-Library: theory HOL-Library.Dlist

15:14:16 HOLCF: theory HOLCF.Powerdomains

15:14:16 HOL-Library: theory HOL-Library.Fun_Lexorder

15:14:16 HOL-Library: theory HOL-Library.FuncSet

15:14:17 HOL-Library: theory HOL-Library.Function_Algebras

15:14:17 HOL-Library: theory HOL-Library.Groups_Big_Fun

15:14:17 HOL-Library: theory HOL-Library.Function_Division

15:14:17 HOL-Library: theory HOL-Library.IArray

15:14:17 HOLCF: theory HOLCF

15:14:17 HOL-Library: theory HOL-Library.Infinite_Set

15:14:18 HOL-Library: theory HOL-Library.Omega_Words_Fun

15:14:18 HOL-Library: theory HOL-Library.Ramsey

15:14:18 HOL-Library: theory HOL-Library.LaTeXsugar

15:14:18 HOL-Library: theory HOL-Library.Lattice_Constructions

15:14:18 HOL-Library: theory HOL-Library.ListVector

15:14:19 HOL-Library: theory HOL-Library.List_lexord

15:14:19 HOL-Library: theory HOL-Library.Mapping

15:14:22 HOL-Library: theory HOL-Library.AList_Mapping

15:14:22 HOL-Library: theory HOL-Library.More_List

15:14:23 HOL-Library: theory HOL-Library.Nat_Bijection

15:14:23 HOL-Library: theory HOL-Library.Old_Datatype

15:14:23 HOL-Library: theory HOL-Library.Stream

15:14:24 HOL-Library: theory HOL-Library.Old_Recdef

15:14:25 HOL-Library: theory HOL-Library.Open_State_Syntax

15:14:25 HOL-Library: theory HOL-Library.Option_ord

15:14:25 HOL-Library: theory HOL-Library.Parallel

15:14:25 HOL-Library: theory HOL-Library.Pattern_Aliases

15:14:26 HOL-Library: theory HOL-Library.Perm

15:14:26 HOL-Library: theory HOL-Library.Phantom_Type

15:14:26 HOL-Proofs: theory HOL.GCD

15:14:27 HOL-Library: theory HOL-Library.Cardinality

15:14:28 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs

15:14:28 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck

15:14:28 HOL-Library: theory HOL-Library.Numeral_Type

15:14:28 HOL-Library: theory HOL-Library.Preorder

15:14:29 HOL-Library: theory HOL-Library.Product_Lexorder

15:14:29 HOL-Library: theory HOL-Library.Product_Plus

15:14:29 HOL-Library: theory HOL-Library.Product_Order

15:14:29 HOL-Library: theory HOL-Library.Finite_Lattice

15:14:29 HOL-Library: theory HOL-Library.Type_Length

15:14:29 HOL-Library: theory HOL-Library.Saturated

15:14:30 HOL-Library: theory HOL-Library.Quotient_Syntax

15:14:30 HOL-Library: theory HOL-Library.Quotient_Option

15:14:30 HOL-Library: theory HOL-Library.Quotient_Product

15:14:30 HOL-Library: theory HOL-Library.Quotient_Set

15:14:30 HOL-Library: theory HOL-Library.Quotient_List

15:14:31 HOL-Library: theory HOL-Library.Quotient_Sum

15:14:31 HOL-Library: theory HOL-Library.Quotient_Type

15:14:31 HOL-Library: theory HOL-Library.RBT_Impl

15:14:32 HOL-Library: theory HOL-Library.Realizers

15:14:32 HOL-Library: theory HOL-Library.Reflection

15:14:33 HOL-Library: theory HOL-Library.Refute

15:14:34 HOL-Library: theory HOL-Library.Rewrite

15:14:34 HOL-Library: theory HOL-Library.Set_Algebras

15:14:34 HOL-Library: theory HOL-Library.Simps_Case_Conv

15:14:35 HOL-Library: theory HOL-Library.Extended

15:14:37 HOL-Library: theory HOL-Library.Stirling

15:14:37 HOL-Library: theory HOL-Library.Sublist

15:14:42 HOL-Library: theory HOL-Library.Prefix_Order

15:14:42 HOL-Library: theory HOL-Library.Subseq_Order

15:14:42 HOL-Library: theory HOL-Library.Transitive_Closure_Table

15:14:42 HOL-Library: theory HOL-Library.Tree

15:14:43 Timing HOLCF (2 threads, 19.440s elapsed time, 38.020s cpu time, 2.452s GC time, factor 1.96)

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

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

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

15:14:43 Finished HOLCF (0:00:43 elapsed time, 0:01:12 cpu time, factor 1.67)

15:14:43 Building IOA ...

15:14:44 IOA: theory IOA.Asig

15:14:44 IOA: theory IOA.Seq

15:14:44 IOA: theory IOA.Automata

15:14:45 IOA: theory IOA.Sequence

15:14:45 IOA: theory IOA.Pred

15:14:45 HOL-Library: theory HOL-Library.Tree_Multiset

15:14:46 HOL-Library: theory HOL-Library.Uprod

15:14:46 IOA: theory IOA.Traces

15:14:46 IOA: theory IOA.TL

15:14:47 HOL-Library: theory HOL-Library.While_Combinator

15:14:47 IOA: theory IOA.CompoExecs

15:14:48 IOA: theory IOA.RefMappings

15:14:48 IOA: theory IOA.RefCorrectness

15:14:48 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint

15:14:48 IOA: theory IOA.CompoScheds

15:14:48 IOA: theory IOA.Simulations

15:14:48 HOL-Library: theory HOL-Library.Countable

15:14:48 IOA: theory IOA.SimCorrectness

15:14:49 IOA: theory IOA.ShortExecutions

15:14:49 IOA: theory IOA.Deadlock

15:14:49 IOA: theory IOA.CompoTraces

15:14:49 HOL-Library: theory HOL-Library.Countable_Set

15:14:50 HOL-Library: theory HOL-Library.Countable_Complete_Lattices

15:14:50 IOA: theory IOA.Compositionality

15:14:51 IOA: theory IOA.IOA

15:14:51 IOA: theory IOA.TLS

15:14:52 IOA: theory IOA.LiveIOA

15:14:52 IOA: theory IOA.Abstraction

15:14:52 HOL-Library: theory HOL-Library.Countable_Set_Type

15:14:54 HOL-Proofs: theory HOL.Map

15:14:55 HOL-Library: theory HOL-Library.FSet

15:14:58 HOL-Proofs: theory HOL.Enum

15:14:59 HOL-Library: theory HOL-Library.Finite_Map

15:15:02 HOL-Library: theory HOL-Library.BigO

15:15:03 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float

15:15:04 HOL-Library: theory HOL-Library.Diagonal_Subsequence

15:15:04 HOL-Library: theory HOL-Library.Discrete

15:15:04 HOL-Library: theory HOL-Library.Going_To_Filter

15:15:04 HOL-Library: theory HOL-Library.Indicator_Function

15:15:05 HOL-Library: theory HOL-Library.Landau_Symbols

15:15:08 HOL-Library: theory HOL-Library.Lattice_Algebras

15:15:13 HOL-Library: theory HOL-Library.Liminf_Limsup

15:15:13 HOL-Library: theory HOL-Library.Log_Nat

15:15:13 HOL-Library: theory HOL-Library.RBT

15:15:14 HOL-Library: theory HOL-Library.Float

15:15:14 HOL-Library: theory HOL-Library.RBT_Mapping

15:15:14 HOL-Library: theory HOL-Library.RBT_Set

15:15:15 HOL-Library: theory HOL-Library.Lub_Glb

15:15:16 HOL-Library: theory HOL-Library.Multiset_Permutations

15:15:16 HOL-Library: theory HOL-Library.Nonpos_Ints

15:15:17 HOL-Library: theory HOL-Library.OptionalSugar

15:15:17 HOL-Library: theory HOL-Library.Order_Continuity

15:15:17 HOL-Library: theory HOL-Library.Periodic_Fun

15:15:17 HOL-Library: theory HOL-Library.Quadratic_Discriminant

15:15:17 HOL-Library: theory HOL-Library.Sum_of_Squares

15:15:18 HOL-Library: theory HOL-Library.Extended_Nat

15:15:18 Timing IOA (2 threads, 18.722s elapsed time, 34.888s cpu time, 1.488s GC time, factor 1.86)

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

15:15:18 Finished IOA (0:00:35 elapsed time, 0:00:56 cpu time, factor 1.60)

15:15:18 Building HOL-TLA ...

15:15:19 HOL-Library: theory HOL-Library.Extended_Real

15:15:19 HOL-TLA: theory HOL-TLA.Intensional

15:15:20 HOL-TLA: theory HOL-TLA.Stfun

15:15:20 HOL-TLA: theory HOL-TLA.Action

15:15:20 HOL-TLA: theory HOL-TLA.Init

15:15:20 HOL-TLA: theory HOL-TLA.TLA

15:15:20 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams

15:15:22 HOL-Library: theory HOL-Library.Tree_Real

15:15:23 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real

15:15:25 HOL-Library: theory HOL-Library.Library

15:15:32 Timing HOL-TLA (2 threads, 1.879s elapsed time, 2.968s cpu time, 0.000s GC time, factor 1.58)

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

15:15:32 Finished HOL-TLA (0:00:13 elapsed time, 0:00:17 cpu time, factor 1.27)

15:15:32 Building HOL-Analysis ...

15:15:34 HOL-Analysis: theory HOL-Library.Disjoint_Sets

15:15:34 HOL-Analysis: theory HOL-Library.Cancellation

15:15:34 HOL-Analysis: theory HOL-Library.FuncSet

15:15:35 HOL-Analysis: theory HOL-Library.Multiset

15:15:35 HOL-Analysis: theory HOL-Library.Infinite_Set

15:15:35 HOL-Analysis: theory HOL-Library.Nat_Bijection

15:15:36 HOL-Analysis: theory HOL-Library.Old_Datatype

15:15:37 HOL-Analysis: theory HOL-Library.Phantom_Type

15:15:38 HOL-Analysis: theory HOL-Library.Cardinality

15:15:39 HOL-Analysis: theory HOL-Library.Numeral_Type

15:15:40 HOL-Analysis: theory HOL-Library.Product_Plus

15:15:40 HOL-Analysis: theory HOL-Library.Product_Order

15:15:41 HOL-Analysis: theory HOL-Library.Set_Algebras

15:15:41 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring

15:15:41 HOL-Analysis: theory HOL-Library.Permutations

15:15:42 HOL-Analysis: theory HOL-Library.Countable

15:15:44 HOL-Analysis: theory HOL-Library.Countable_Set

15:15:44 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices

15:15:47 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable

15:15:47 HOL-Analysis: theory HOL-Analysis.Infinite_Products

15:15:47 HOL-Analysis: theory HOL-Analysis.Inner_Product

15:15:48 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm

15:15:49 HOL-Analysis: theory HOL-Analysis.Product_Vector

15:15:50 HOL-Analysis: theory HOL-Analysis.L2_Norm

15:15:50 HOL-Analysis: theory HOL-Analysis.Euclidean_Space

15:15:52 HOL-Analysis: theory HOL-Analysis.Linear_Algebra

15:15:53 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product

15:15:55 HOL-Analysis: theory HOL-Computational_Algebra.Primes

15:15:55 HOL-Analysis: theory HOL-Analysis.Operator_Norm

15:15:55 HOL-Analysis: theory HOL-Analysis.Poly_Roots

15:15:56 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series

15:15:56 HOL-Analysis: theory HOL-Analysis.Cartesian_Space

15:15:57 HOL-Analysis: theory HOL-Library.Discrete

15:15:58 HOL-Analysis: theory HOL-Library.Indicator_Function

15:15:58 HOL-Analysis: theory HOL-Library.Liminf_Limsup

15:15:59 HOL-Analysis: theory HOL-Library.Nonpos_Ints

15:15:59 HOL-Analysis: theory HOL-Library.Order_Continuity

15:16:00 HOL-Analysis: theory HOL-Library.Extended_Nat

15:16:01 HOL-Analysis: theory HOL-Library.Periodic_Fun

15:16:01 HOL-Analysis: theory HOL-Library.Sum_of_Squares

15:16:01 HOL-Analysis: theory HOL-Library.Extended_Real

15:16:04 HOL-Analysis: theory HOL-Analysis.Norm_Arith

15:16:04 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space

15:16:06 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real

15:16:09 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra

15:16:12 HOL-Analysis: theory HOL-Analysis.Connected

15:16:12 HOL-Analysis: theory HOL-Analysis.Measurable

15:16:13 HOL-Analysis: theory HOL-Analysis.Measure_Space

15:16:15 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space

15:16:16 HOL-Analysis: theory HOL-Analysis.Caratheodory

15:16:17 HOL-Analysis: theory HOL-Analysis.Tagged_Division

15:16:18 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits

15:16:18 HOL-Analysis: theory HOL-Analysis.Starlike

15:16:23 HOL-Analysis: theory HOL-Analysis.Summation_Tests

15:16:24 HOL-Analysis: theory HOL-Analysis.Uniform_Limit

15:16:25 HOL-Analysis: theory HOL-Analysis.Continuous_Extension

15:16:26 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function

15:16:26 HOL-Analysis: theory HOL-Analysis.Path_Connected

15:16:30 HOL-Analysis: theory HOL-Analysis.Homeomorphism

15:16:31 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint

15:16:34 HOL-Analysis: theory HOL-Analysis.Derivative

15:16:36 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space

15:16:36 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems

15:16:38 HOL-Analysis: theory HOL-Analysis.Determinants

15:16:38 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem

15:16:38 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space

15:16:39 HOL-Analysis: theory HOL-Analysis.Polytope

15:16:42 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected

15:16:42 HOL-Analysis: theory HOL-Analysis.Borel_Space

15:16:46 HOL-Analysis: theory HOL-Analysis.Lipschitz

15:16:46 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration

15:16:46 HOL-Analysis: theory HOL-Analysis.Regularity

15:16:48 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure

15:16:49 HOL-Analysis: theory HOL-Analysis.Embed_Measure

15:16:49 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure

15:16:50 HOL-Analysis: theory HOL-Analysis.Bochner_Integration

15:16:50 HOL-Analysis: theory HOL-Analysis.Function_Topology

15:16:53 HOL-Analysis: theory HOL-Analysis.Complete_Measure

15:16:53 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym

15:16:54 HOL-Analysis: theory HOL-Analysis.Set_Integral

15:16:54 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure

15:16:54 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum

15:16:56 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration

15:17:00 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function

15:17:00 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration

15:17:01 HOL-Analysis: theory HOL-Analysis.Integral_Test

15:17:03 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics

15:17:04 HOL-Analysis: theory HOL-Analysis.Improper_Integral

15:17:04 HOL-Analysis: theory HOL-Analysis.Interval_Integral

15:17:05 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution

15:17:05 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental

15:17:08 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem

15:17:08 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers

15:17:09 HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem

15:17:13 HOL-Analysis: theory HOL-Analysis.Conformal_Mappings

15:17:15 HOL-Analysis: theory HOL-Analysis.FPS_Convergence

15:17:17 HOL-Analysis: theory HOL-Analysis.Gamma_Function

15:17:21 HOL-Analysis: theory HOL-Analysis.Ball_Volume

15:17:22 HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem

15:17:23 HOL-Analysis: theory HOL-Analysis.Change_Of_Vars

15:17:24 HOL-Analysis: theory HOL-Analysis.Further_Topology

15:17:28 HOL-Analysis: theory HOL-Analysis.Great_Picard

15:17:29 HOL-Analysis: theory HOL-Analysis.Riemann_Mapping

15:17:29 HOL-Analysis: theory HOL-Analysis.Jordan_Curve

15:17:30 HOL-Analysis: theory HOL-Analysis.Winding_Numbers

15:17:31 HOL-Analysis: theory HOL-Analysis.Analysis

15:18:57 Timing HOL-Library (2 threads, 220.059s elapsed time, 413.200s cpu time, 29.360s GC time, factor 1.88)

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

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

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

15:18:57 Finished HOL-Library (0:04:56 elapsed time, 0:08:47 cpu time, factor 1.78)

15:18:57 Building HOL-Computational_Algebra ...

15:18:58 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field

15:18:58 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure

15:18:59 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring

15:19:07 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm

15:19:14 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction

15:19:15 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes

15:19:15 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers

15:19:16 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree

15:19:16 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial

15:19:25 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring

15:19:27 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series

15:19:30 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra

15:19:31 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial

15:19:31 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS

15:19:46 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra

15:20:51 Timing HOL-Computational_Algebra (2 threads, 84.875s elapsed time, 153.376s cpu time, 6.636s GC time, factor 1.81)

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

15:20:51 Finished HOL-Computational_Algebra (0:01:53 elapsed time, 0:03:09 cpu time, factor 1.67)

15:20:51 Building HOL-Number_Theory ...

15:20:53 HOL-Number_Theory: theory HOL-Algebra.Congruence

15:20:53 HOL-Number_Theory: theory HOL-Number_Theory.Cong

15:20:54 HOL-Number_Theory: theory HOL-Algebra.Order

15:20:55 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes

15:20:55 HOL-Number_Theory: theory HOL-Number_Theory.Fib

15:20:55 HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers

15:20:56 HOL-Number_Theory: theory HOL-Algebra.Lattice

15:20:56 HOL-Number_Theory: theory HOL-Number_Theory.Totient

15:20:57 HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice

15:20:58 HOL-Number_Theory: theory HOL-Algebra.Group

15:21:00 HOL-Number_Theory: theory HOL-Algebra.Coset

15:21:00 HOL-Number_Theory: theory HOL-Algebra.FiniteProduct

15:21:00 HOL-Number_Theory: theory HOL-Algebra.Ring

15:21:04 HOL-Number_Theory: theory HOL-Algebra.AbelCoset

15:21:04 HOL-Number_Theory: theory HOL-Algebra.Module

15:21:05 HOL-Number_Theory: theory HOL-Algebra.More_Group

15:21:06 HOL-Number_Theory: theory HOL-Algebra.More_Finite_Product

15:21:06 HOL-Number_Theory: theory HOL-Algebra.More_Ring

15:21:08 HOL-Number_Theory: theory HOL-Algebra.Ideal

15:21:13 HOL-Number_Theory: theory HOL-Algebra.RingHom

15:21:13 HOL-Number_Theory: theory HOL-Algebra.UnivPoly

15:21:24 HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group

15:21:27 HOL-Number_Theory: theory HOL-Number_Theory.Residues

15:21:30 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion

15:21:30 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington

15:21:30 HOL-Number_Theory: theory HOL-Number_Theory.Gauss

15:21:30 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity

15:21:31 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory

15:22:05 HOL-Proofs: theory HOL.Random

15:23:20 HOL-Proofs: theory HOL.String

15:23:45 Timing HOL-Number_Theory (2 threads, 115.039s elapsed time, 204.964s cpu time, 12.808s GC time, factor 1.78)

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

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

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

15:23:45 Finished HOL-Number_Theory (0:02:52 elapsed time, 0:04:39 cpu time, factor 1.62)

15:23:45 Building HOL-Algebra ...

15:23:46 HOL-Algebra: theory HOL-Algebra.Exponent

15:23:46 HOL-Algebra: theory HOL-Algebra.Congruence

15:23:48 HOL-Algebra: theory HOL-Algebra.Order

15:23:49 HOL-Algebra: theory HOL-Algebra.Lattice

15:23:50 HOL-Algebra: theory HOL-Algebra.Complete_Lattice

15:23:52 HOL-Algebra: theory HOL-Algebra.Galois_Connection

15:23:53 HOL-Algebra: theory HOL-Algebra.Group

15:23:54 HOL-Algebra: theory HOL-Algebra.Bij

15:23:55 HOL-Algebra: theory HOL-Algebra.Coset

15:23:55 HOL-Algebra: theory HOL-Algebra.FiniteProduct

15:23:56 HOL-Algebra: theory HOL-Algebra.Sylow

15:23:56 HOL-Algebra: theory HOL-Algebra.Divisibility

15:23:57 HOL-Algebra: theory HOL-Algebra.Ring

15:24:00 HOL-Algebra: theory HOL-Algebra.AbelCoset

15:24:05 HOL-Algebra: theory HOL-Algebra.Module

15:24:06 HOL-Algebra: theory HOL-Algebra.Ideal

15:24:07 HOL-Algebra: theory HOL-Algebra.More_Group

15:24:07 HOL-Algebra: theory HOL-Algebra.More_Finite_Product

15:24:07 HOL-Algebra: theory HOL-Algebra.More_Ring

15:24:09 HOL-Algebra: theory HOL-Algebra.RingHom

15:24:10 HOL-Algebra: theory HOL-Algebra.QuotRing

15:24:10 HOL-Algebra: theory HOL-Algebra.UnivPoly

15:24:10 HOL-Algebra: theory HOL-Algebra.IntRing

15:24:18 HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint

15:24:23 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group

15:24:26 HOL-Proofs: theory HOL.Predicate

15:24:28 HOL-Proofs: theory HOL.Typerep

15:24:30 HOL-Proofs: theory HOL.Lazy_Sequence

15:24:31 HOL-Proofs: theory HOL.Limited_Sequence

15:24:32 HOL-Proofs: theory HOL.Code_Evaluation

15:24:34 HOL-Proofs: theory HOL.Quickcheck_Random

15:24:37 HOL-Proofs: theory HOL.Quickcheck_Exhaustive

15:24:37 HOL-Proofs: theory HOL.Quickcheck_Narrowing

15:24:45 HOL-Proofs: theory HOL.Record

15:24:45 HOL-Proofs: theory HOL.Random_Pred

15:24:47 HOL-Proofs: theory HOL.Random_Sequence

15:24:59 HOL-Proofs: theory HOL.Predicate_Compile

15:25:00 HOL-Proofs: theory HOL.Nitpick

15:25:08 HOL-Proofs: theory HOL.Nunchaku

15:25:09 HOL-Proofs: theory Main

15:25:11 HOL-Proofs: theory HOL-Library.Realizers

15:26:22 Timing HOL-Algebra (2 threads, 91.163s elapsed time, 159.620s cpu time, 16.960s GC time, factor 1.75)

15:26:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra

15:26:22 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/document.pdf

15:26:22 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline.pdf

15:26:22 Finished HOL-Algebra (0:02:36 elapsed time, 0:04:02 cpu time, factor 1.55)

15:26:22 Building HOL-Word ...

15:26:23 HOL-Word: theory HOL-Library.Bit

15:26:23 HOL-Word: theory HOL-Library.Boolean_Algebra

15:26:24 HOL-Word: theory HOL-Library.Phantom_Type

15:26:24 HOL-Word: theory HOL-Word.Bits

15:26:24 HOL-Word: theory HOL-Word.Bits_Bit

15:26:24 HOL-Word: theory HOL-Word.Misc_Numeric

15:26:24 HOL-Word: theory HOL-Word.Bit_Representation

15:26:25 HOL-Word: theory HOL-Library.Cardinality

15:26:25 HOL-Word: theory HOL-Word.Bits_Int

15:26:26 HOL-Word: theory HOL-Library.Numeral_Type

15:26:27 HOL-Word: theory HOL-Word.Bit_Comparison

15:26:27 HOL-Word: theory HOL-Library.Type_Length

15:26:27 HOL-Word: theory HOL-Word.Bool_List_Representation

15:26:27 HOL-Word: theory HOL-Word.Word_Miscellaneous

15:26:28 HOL-Word: theory HOL-Word.Misc_Typedef

15:26:28 HOL-Word: theory HOL-Word.Word

15:26:34 HOL-Word: theory HOL-Word.WordBitwise

15:26:35 HOL-Word: theory HOL-Word.WordExamples

15:27:07 Timing HOL-Proofs (2 threads, 1079.978s elapsed time, 1971.972s cpu time, 167.168s GC time, factor 1.83)

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

15:27:07 Finished HOL-Proofs (0:19:49 elapsed time, 0:35:24 cpu time, factor 1.79)

15:27:07 Building HOLCF-Library ...

15:27:08 HOLCF-Library: theory HOL-Library.Infinite_Set

15:27:08 HOLCF-Library: theory HOLCF-Library.Bool_Discrete

15:27:08 HOLCF-Library: theory HOLCF-Library.Char_Discrete

15:27:08 Timing HOL-Word (2 threads, 24.387s elapsed time, 46.736s cpu time, 2.288s GC time, factor 1.92)

15:27:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word

15:27:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/document.pdf

15:27:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/outline.pdf

15:27:08 Finished HOL-Word (0:00:45 elapsed time, 0:01:18 cpu time, factor 1.73)

15:27:08 Building HOL-SPARK ...

15:27:08 HOLCF-Library: theory HOLCF-Library.Int_Discrete

15:27:08 HOLCF-Library: theory HOL-Library.Countable_Set

15:27:08 HOLCF-Library: theory HOLCF-Library.Defl_Bifinite

15:27:09 HOLCF-Library: theory HOL-Library.Countable_Complete_Lattices

15:27:09 HOL-SPARK: theory HOL-SPARK.SPARK_Setup

15:27:09 HOLCF-Library: theory HOLCF-Library.List_Cpo

15:27:10 HOLCF-Library: theory HOLCF-Library.Nat_Discrete

15:27:10 HOLCF-Library: theory HOLCF-Library.Sum_Cpo

15:27:11 HOLCF-Library: theory HOLCF-Library.List_Predomain

15:27:11 HOL-SPARK: theory HOL-SPARK.SPARK

15:27:12 HOLCF-Library: theory HOL-Library.Order_Continuity

15:27:12 HOLCF-Library: theory HOLCF-Library.Option_Cpo

15:27:12 HOLCF-Library: theory HOLCF-Library.HOL_Cpo

15:27:12 HOLCF-Library: theory HOL-Library.Extended_Nat

15:27:14 HOLCF-Library: theory HOLCF-Library.Stream

15:27:15 HOLCF-Library: theory HOLCF-Library.HOLCF_Library

15:27:23 Timing HOL-SPARK (2 threads, 2.592s elapsed time, 3.488s cpu time, 0.156s GC time, factor 1.35)

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

15:27:23 Finished HOL-SPARK (0:00:14 elapsed time, 0:00:18 cpu time, factor 1.27)

15:27:23 Building HOL-Auth ...

15:27:24 HOL-Auth: theory HOL-Auth.Message

15:27:28 HOL-Auth: theory HOL-Auth.All_Symmetric

15:27:28 HOL-Auth: theory HOL-Auth.Event

15:27:28 HOL-Auth: theory HOL-Auth.EventSC

15:27:28 HOL-Auth: theory HOL-Auth.Extensions

15:27:29 HOL-Auth: theory HOL-Auth.Analz

15:27:30 HOL-Auth: theory HOL-Auth.Guard

15:27:30 HOL-Auth: theory HOL-Auth.GuardK

15:27:31 HOL-Auth: theory HOL-Auth.List_Msg

15:27:31 HOL-Auth: theory HOL-Auth.Public

15:27:31 HOL-Auth: theory HOL-Auth.CertifiedEmail

15:27:32 HOL-Auth: theory HOL-Auth.Guard_Public

15:27:32 HOL-Auth: theory HOL-Auth.Guard_NS_Public

15:27:33 HOL-Auth: theory HOL-Auth.P2

15:27:33 HOL-Auth: theory HOL-Auth.Proto

15:27:34 HOL-Auth: theory HOL-Auth.KerberosIV

15:27:36 HOL-Auth: theory HOL-Auth.KerberosIV_Gets

15:27:36 HOL-Auth: theory HOL-Auth.KerberosV

15:27:38 HOL-Auth: theory HOL-Auth.Kerberos_BAN

15:27:38 Timing HOLCF-Library (2 threads, 16.184s elapsed time, 29.828s cpu time, 1.364s GC time, factor 1.84)

15:27:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Library

15:27:38 Finished HOLCF-Library (0:00:30 elapsed time, 0:00:48 cpu time, factor 1.57)

15:27:38 Building HOL-Nonstandard_Analysis ...

15:27:38 HOL-Auth: theory HOL-Auth.Kerberos_BAN_Gets

15:27:38 HOL-Auth: theory HOL-Auth.NS_Public

15:27:39 HOL-Auth: theory HOL-Auth.NS_Public_Bad

15:27:39 HOL-Auth: theory HOL-Auth.NS_Shared

15:27:39 HOL-Auth: theory HOL-Auth.OtwayRees

15:27:40 HOL-Auth: theory HOL-Auth.OtwayReesBella

15:27:40 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Free_Ultrafilter

15:27:40 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.StarDef

15:27:40 HOL-Auth: theory HOL-Auth.OtwayRees_AN

15:27:40 HOL-Auth: theory HOL-Auth.OtwayRees_Bad

15:27:40 HOL-Auth: theory HOL-Auth.P1

15:27:41 HOL-Auth: theory HOL-Auth.Recur

15:27:41 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperNat

15:27:42 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HyperDef

15:27:42 HOL-Auth: theory HOL-Auth.WooLam

15:27:42 HOL-Auth: theory HOL-Auth.Yahalom

15:27:43 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSA

15:27:43 HOL-Auth: theory HOL-Auth.Yahalom2

15:27:44 HOL-Auth: theory HOL-Auth.Yahalom_Bad

15:27:44 HOL-Auth: theory HOL-Auth.ZhouGollmann

15:27:45 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSComplex

15:27:45 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Star

15:27:45 HOL-Auth: theory HOL-Auth.Auth_Shared

15:27:45 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLim

15:27:45 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HDeriv

15:27:45 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NatStar

15:27:46 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSEQ

15:27:46 HOL-Auth: theory HOL-Auth.Auth_Guard_Public

15:27:46 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HSeries

15:27:46 HOL-Auth: theory HOL-Auth.Shared

15:27:47 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HTranscendental

15:27:47 HOL-Auth: theory HOL-Auth.Guard_Shared

15:27:47 HOL-Auth: theory HOL-Auth.Guard_OtwayRees

15:27:47 HOL-Auth: theory HOL-Auth.Guard_Yahalom

15:27:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.HLog

15:27:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.NSCA

15:27:48 HOL-Auth: theory HOL-Auth.TLS

15:27:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hyperreal

15:27:48 HOL-Auth: theory HOL-Auth.Auth_Guard_Shared

15:27:48 HOL-Auth: theory HOL-Auth.Smartcard

15:27:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CStar

15:27:48 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.CLim

15:27:49 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Hypercomplex

15:27:49 HOL-Auth: theory HOL-Auth.ShoupRubin

15:27:49 HOL-Nonstandard_Analysis: theory HOL-Nonstandard_Analysis.Nonstandard_Analysis

15:27:50 HOL-Auth: theory HOL-Auth.Auth_Public

15:27:50 HOL-Auth: theory HOL-Auth.ShoupRubinBella

15:27:52 HOL-Auth: theory HOL-Auth.Auth_Smartcard

15:28:16 Timing HOL-Nonstandard_Analysis (2 threads, 11.620s elapsed time, 21.824s cpu time, 1.264s GC time, factor 1.88)

15:28:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis

15:28:16 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/document.pdf

15:28:16 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/outline.pdf

15:28:16 Finished HOL-Nonstandard_Analysis (0:00:37 elapsed time, 0:01:00 cpu time, factor 1.59)

15:28:16 Building HOL-Nominal ...

15:28:18 HOL-Nominal: theory HOL-Nominal.Nominal

15:28:44 Timing HOL-Nominal (2 threads, 7.759s elapsed time, 13.768s cpu time, 0.764s GC time, factor 1.77)

15:28:44 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal

15:28:44 Finished HOL-Nominal (0:00:27 elapsed time, 0:00:39 cpu time, factor 1.47)

15:28:44 Building HOL-Eisbach ...

15:28:45 HOL-Eisbach: theory HOL-Eisbach.Eisbach

15:28:45 HOL-Eisbach: theory IFOL

15:28:46 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Old_Appl_Syntax

15:28:46 HOL-Eisbach: theory HOL-Eisbach.Eisbach_Tools

15:28:46 HOL-Eisbach: theory HOL-Eisbach.Examples

15:28:46 HOL-Eisbach: theory HOL-Eisbach.Tests

15:28:47 HOL-Eisbach: theory FOL

15:28:49 HOL-Eisbach: theory HOL-Eisbach.Examples_FOL

15:29:00 Timing HOL-Eisbach (2 threads, 4.068s elapsed time, 7.972s cpu time, 0.192s GC time, factor 1.96)

15:29:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Eisbach

15:29:00 Finished HOL-Eisbach (0:00:15 elapsed time, 0:00:22 cpu time, factor 1.48)

15:29:00 Building Codegen_Basics ...

15:29:01 Codegen_Basics: theory Codegen_Basics.Setup

15:29:18 Timing Codegen_Basics (2 threads, 1.516s elapsed time, 1.640s cpu time, 0.000s GC time, factor 1.08)

15:29:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen_Basics

15:29:18 Finished Codegen_Basics (0:00:18 elapsed time, 0:00:23 cpu time, factor 1.27)

15:29:18 Building Typeclass_Hierarchy_Basics ...

15:29:20 Typeclass_Hierarchy_Basics: theory Typeclass_Hierarchy_Basics.Setup

15:29:37 Timing Typeclass_Hierarchy_Basics (2 threads, 0.854s elapsed time, 0.976s cpu time, 0.000s GC time, factor 1.14)

15:29:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy_Basics

15:29:37 Finished Typeclass_Hierarchy_Basics (0:00:18 elapsed time, 0:00:23 cpu time, factor 1.28)

15:29:37 Building HOL-Mirabelle ...

15:29:38 HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle

15:29:38 HOL-Mirabelle: theory HOL-Mirabelle.Mirabelle_Test

15:29:47 Timing HOL-Mirabelle (2 threads, 0.555s elapsed time, 0.656s cpu time, 0.000s GC time, factor 1.18)

15:29:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle

15:29:47 Finished HOL-Mirabelle (0:00:10 elapsed time, 0:00:12 cpu time, factor 1.23)

15:29:47 Running HOL-Nominal-Examples ...

15:29:49 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR_Takahashi

15:29:49 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CK_Machine

15:29:52 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class1

15:30:02 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Compile

15:30:20 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Contexts

15:30:26 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Crary

15:30:32 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Fsub

15:30:40 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Height

15:30:43 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lam_Funs

15:30:46 HOL-Nominal-Examples: theory HOL-Nominal-Examples.CR

15:30:47 HOL-Nominal-Examples: theory HOL-Nominal-Examples.SN

15:30:48 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Lambda_mu

15:30:52 HOL-Nominal-Examples: theory HOL-Nominal-Examples.LocalWeakening

15:30:55 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Pattern

15:31:03 Timing HOL-Auth (2 threads, 185.189s elapsed time, 296.272s cpu time, 12.404s GC time, factor 1.60)

15:31:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth

15:31:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/document.pdf

15:31:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/outline.pdf

15:31:03 Finished HOL-Auth (0:03:39 elapsed time, 0:05:47 cpu time, factor 1.58)

15:31:03 Running HOL-Data_Structures ...

15:31:04 HOL-Data_Structures: theory HOL-Data_Structures.Less_False

15:31:04 HOL-Data_Structures: theory HOL-Data_Structures.Sorted_Less

15:31:04 HOL-Data_Structures: theory HOL-Data_Structures.Cmp

15:31:05 HOL-Data_Structures: theory HOL-Data_Structures.AList_Upd_Del

15:31:05 HOL-Data_Structures: theory HOL-Data_Structures.List_Ins_Del

15:31:05 HOL-Data_Structures: theory HOL-Data_Structures.Map_Specs

15:31:05 HOL-Nominal-Examples: theory HOL-Nominal-Examples.SOS

15:31:05 HOL-Data_Structures: theory HOL-Data_Structures.Tree2

15:31:05 HOL-Data_Structures: theory HOL-Data_Structures.Set_Specs

15:31:06 HOL-Data_Structures: theory HOL-Data_Structures.Tree23

15:31:07 HOL-Data_Structures: theory HOL-Data_Structures.Isin2

15:31:08 HOL-Data_Structures: theory HOL-Data_Structures.Lookup2

15:31:08 HOL-Data_Structures: theory HOL-Data_Structures.AA_Set

15:31:08 HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join

15:31:09 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Standardization

15:31:10 HOL-Data_Structures: theory HOL-Data_Structures.AA_Map

15:31:10 HOL-Data_Structures: theory HOL-Data_Structures.RBT

15:31:11 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Set

15:31:12 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Support

15:31:13 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Type_Preservation

15:31:14 HOL-Data_Structures: theory HOL-Data_Structures.Tree234

15:31:17 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Set

15:31:17 HOL-Nominal-Examples: theory HOL-Nominal-Examples.W

15:31:19 HOL-Data_Structures: theory HOL-Data_Structures.Tree23_Map

15:31:24 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening

15:31:25 HOL-Data_Structures: theory HOL-Library.Cancellation

15:31:26 HOL-Data_Structures: theory HOL-Library.Multiset

15:31:30 HOL-Data_Structures: theory HOL-Data_Structures.Priority_Queue

15:31:31 HOL-Data_Structures: theory HOL-Library.Pattern_Aliases

15:31:31 HOL-Data_Structures: theory HOL-Data_Structures.Base_FDS

15:31:31 HOL-Data_Structures: theory HOL-Library.Tree

15:31:34 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Set

15:31:34 HOL-Data_Structures: theory HOL-Data_Structures.Tree_Map

15:31:35 HOL-Data_Structures: theory HOL-Data_Structures.Binomial_Heap

15:31:42 HOL-Data_Structures: theory HOL-Data_Structures.Leftist_Heap

15:31:45 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Set

15:31:47 HOL-Data_Structures: theory HOL-Data_Structures.RBT_Map

15:31:51 HOL-Data_Structures: theory HOL-Data_Structures.Set2_Join_RBT

15:31:53 HOL-Data_Structures: theory HOL-Data_Structures.Sorting

15:31:54 HOL-Data_Structures: theory HOL-Data_Structures.Tree234_Map

15:31:56 HOL-Data_Structures: theory HOL-Library.Tree_Real

15:31:56 HOL-Data_Structures: theory HOL-Data_Structures.Balance

15:31:56 HOL-Data_Structures: theory HOL-Number_Theory.Fib

15:31:57 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Set

15:31:59 HOL-Data_Structures: theory HOL-Data_Structures.AVL_Map

15:31:59 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Set

15:32:21 Timing HOL-Analysis (2 threads, 899.753s elapsed time, 1551.364s cpu time, 61.112s GC time, factor 1.72)

15:32:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis

15:32:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/document.pdf

15:32:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/manual.pdf

15:32:21 Finished HOL-Analysis (0:16:47 elapsed time, 0:28:13 cpu time, factor 1.68)

15:32:21 Building HOL-Probability ...

15:32:23 HOL-Probability: theory HOL-Library.Lattice_Syntax

15:32:23 HOL-Probability: theory HOL-Library.AList

15:32:23 HOL-Probability: theory HOL-Library.Adhoc_Overloading

15:32:23 HOL-Probability: theory HOL-Library.Monad_Syntax

15:32:23 HOL-Probability: theory HOL-Library.Complete_Partial_Order2

15:32:25 HOL-Probability: theory HOL-Library.Mapping

15:32:26 HOL-Probability: theory HOL-Library.AList_Mapping

15:32:26 HOL-Probability: theory HOL-Library.Stream

15:32:27 HOL-Probability: theory HOL-Library.Rewrite

15:32:27 HOL-Probability: theory HOL-Library.Sublist

15:32:28 HOL-Probability: theory HOL-Library.Tree

15:32:29 HOL-Probability: theory HOL-Library.FSet

15:32:32 HOL-Probability: theory HOL-Library.Diagonal_Subsequence

15:32:32 HOL-Probability: theory HOL-Library.Multiset_Permutations

15:32:33 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2

15:32:33 HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams

15:32:34 HOL-Probability: theory HOL-Library.Finite_Map

15:32:35 HOL-Probability: theory HOL-Probability.Discrete_Topology

15:32:35 HOL-Probability: theory HOL-Probability.Essential_Supremum

15:32:35 HOL-Probability: theory HOL-Probability.Probability_Measure

15:32:36 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3

15:32:36 HOL-Probability: theory HOL-Probability.Fin_Map

15:32:38 HOL-Probability: theory HOL-Probability.Conditional_Expectation

15:32:39 HOL-Probability: theory HOL-Probability.Distribution_Functions

15:32:39 HOL-Probability: theory HOL-Probability.Giry_Monad

15:32:39 HOL-Probability: theory HOL-Probability.Weak_Convergence

15:32:39 HOL-Probability: theory HOL-Probability.Helly_Selection

15:32:43 HOL-Probability: theory HOL-Probability.Stopping_Time

15:32:43 HOL-Probability: theory HOL-Probability.Probability_Mass_Function

15:32:43 HOL-Probability: theory HOL-Probability.Projective_Family

15:32:44 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure

15:32:45 HOL-Probability: theory HOL-Probability.Independent_Family

15:32:46 HOL-Probability: theory HOL-Probability.PMF_Impl

15:32:47 HOL-Probability: theory HOL-Probability.Random_Permutations

15:32:48 HOL-Probability: theory HOL-Probability.SPMF

15:32:48 HOL-Probability: theory HOL-Probability.Convolution

15:32:49 HOL-Probability: theory HOL-Probability.Information

15:32:51 HOL-Probability: theory HOL-Probability.Distributions

15:32:52 HOL-Probability: theory HOL-Probability.Projective_Limit

15:32:53 HOL-Probability: theory HOL-Probability.Characteristic_Functions

15:32:54 HOL-Probability: theory HOL-Probability.Sinc_Integral

15:32:54 HOL-Probability: theory HOL-Probability.Stream_Space

15:32:54 HOL-Probability: theory HOL-Probability.Levy

15:32:55 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem

15:32:55 HOL-Probability: theory HOL-Probability.Tree_Space

15:32:57 HOL-Probability: theory HOL-Probability.Probability

15:33:36 HOL-Data_Structures: theory HOL-Data_Structures.Brother12_Map

15:36:01 Timing HOL-Probability (2 threads, 174.049s elapsed time, 319.852s cpu time, 22.156s GC time, factor 1.84)

15:36:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability

15:36:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/document.pdf

15:36:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/outline.pdf

15:36:01 Finished HOL-Probability (0:03:38 elapsed time, 0:06:25 cpu time, factor 1.76)

15:36:01 Running HOL-Decision_Procs ...

15:36:04 HOL-Decision_Procs: theory HOL-Decision_Procs.DP_Library

15:36:04 HOL-Decision_Procs: theory HOL-Decision_Procs.Conversions

15:36:04 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order

15:36:04 HOL-Decision_Procs: theory HOL-Decision_Procs.Algebra_Aux

15:36:05 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring

15:36:06 HOL-Decision_Procs: theory HOL-Decision_Procs.Dense_Linear_Order_Ex

15:36:07 HOL-Decision_Procs: theory HOL-Decision_Procs.Cooper

15:36:16 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Complete

15:36:17 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflective_Field

15:36:31 HOL-Decision_Procs: theory HOL-Decision_Procs.Commutative_Ring_Ex

15:36:32 HOL-Decision_Procs: theory HOL-Decision_Procs.Ferrack

15:37:37 HOL-Decision_Procs: theory HOL-Decision_Procs.MIR

15:38:20 HOL-Decision_Procs: theory HOL-Decision_Procs.Polynomial_List

15:38:30 HOL-Decision_Procs: theory HOL-Decision_Procs.Rat_Pair

15:38:31 HOL-Decision_Procs: theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial

15:38:42 HOL-Decision_Procs: theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff

15:39:57 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Bounds

15:40:02 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation

15:40:51 HOL-Nominal-Examples: theory HOL-Nominal-Examples.VC_Condition

15:40:55 Timing HOL-Nominal-Examples (2 threads, 664.676s elapsed time, 1237.128s cpu time, 135.128s GC time, factor 1.86)

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

15:40:55 Finished HOL-Nominal-Examples (0:11:07 elapsed time, 0:20:39 cpu time, factor 1.86)

15:40:55 Running HOL-ex ...

15:40:57 HOL-ex: theory HOL-ex.Computations

15:40:57 HOL-ex: theory HOL-ex.Bubblesort

15:40:58 HOL-ex: theory HOL-ex.MergeSort

15:40:59 HOL-ex: theory HOL-ex.Quicksort

15:40:59 HOL-ex: theory HOL-ex.Conditional_Parametricity_Examples

15:40:59 HOL-ex: theory HOL-ex.Datatype_Record_Examples

15:41:00 HOL-ex: theory HOL-ex.IArray_Examples

15:41:00 HOL-ex: theory HOL-ex.Perm_Fragments

15:41:00 HOL-ex: theory HOL-ex.Refute_Examples

15:41:03 HOL-ex: theory HOL-ex.Simps_Case_Conv_Examples

15:41:03 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Ex

15:41:03 HOL-Decision_Procs: theory HOL-Decision_Procs.Approximation_Quickcheck_Ex

15:41:03 HOL-ex: theory HOL-ex.Radix_Sort

15:41:04 HOL-ex: theory HOL-ex.Transitive_Closure_Table_Ex

15:41:04 HOL-ex: theory HOL-ex.While_Combinator_Example

15:41:04 HOL-ex: theory HOL-ex.Code_Timing

15:41:05 HOL-ex: theory HOL-ex.Adhoc_Overloading_Examples

15:41:05 HOL-ex: theory HOL-ex.Antiquote

15:41:05 HOL-ex: theory HOL-ex.Arith_Examples

15:41:06 HOL-ex: theory HOL-ex.Birthday_Paradox

15:41:06 HOL-ex: theory HOL-ex.Bit_Lists

15:41:06 HOL-ex: theory HOL-ex.CTL

15:41:07 HOL-ex: theory HOL-ex.Cartouche_Examples

15:41:07 HOL-ex: theory HOL-ex.Case_Product

15:41:07 HOL-ex: theory HOL-ex.Chinese

15:41:08 HOL-ex: theory HOL-ex.Classical

15:41:09 HOL-ex: theory HOL-ex.Coercion_Examples

15:41:09 HOL-ex: theory HOL-ex.Coherent

15:41:09 HOL-ex: theory HOL-ex.Commands

15:41:09 HOL-ex: theory HOL-ex.Erdoes_Szekeres

15:41:09 HOL-ex: theory HOL-ex.Executable_Relation

15:41:09 HOL-ex: theory HOL-ex.Execute_Choice

15:41:09 HOL-ex: theory HOL-ex.Functions

15:41:10 HOL-ex: theory HOL-ex.Groebner_Examples

15:41:10 HOL-ex: theory HOL-ex.Guess

15:41:10 HOL-ex: theory HOL-ex.Hebrew

15:41:13 HOL-ex: theory HOL-ex.Hex_Bin_Examples

15:41:13 HOL-ex: theory HOL-ex.Iff_Oracle

15:41:13 HOL-ex: theory HOL-ex.Induction_Schema

15:41:13 HOL-ex: theory HOL-ex.Intuitionistic

15:41:13 HOL-ex: theory HOL-ex.Lagrange

15:41:13 HOL-ex: theory HOL-ex.List_to_Set_Comprehension_Examples

15:41:15 HOL-ex: theory HOL-ex.LocaleTest2

15:41:16 HOL-ex: theory HOL-ex.ML

15:41:17 HOL-ex: theory HOL-ex.MonoidGroup

15:41:18 HOL-ex: theory HOL-ex.Multiquote

15:41:18 HOL-ex: theory HOL-ex.NatSum

15:41:18 HOL-ex: theory HOL-ex.PER

15:41:18 HOL-ex: theory HOL-ex.Peano_Axioms

15:41:18 HOL-ex: theory HOL-ex.PresburgerEx

15:41:18 HOL-ex: theory HOL-ex.Primrec

15:41:19 HOL-ex: theory HOL-ex.Records

15:41:19 HOL-ex: theory HOL-ex.Residue_Ring

15:41:20 HOL-ex: theory HOL-ex.Rewrite_Examples

15:41:20 HOL-ex: theory HOL-ex.Seq

15:41:21 HOL-ex: theory HOL-ex.Serbian

15:41:24 Timing HOL-Data_Structures (2 threads, 613.511s elapsed time, 944.932s cpu time, 34.716s GC time, factor 1.54)

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

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

15:41:24 Finished HOL-Data_Structures (0:10:20 elapsed time, 0:15:51 cpu time, factor 1.53)

15:41:24 Running HOL-Codegenerator_Test ...

15:41:24 HOL-ex: theory HOL-ex.Set_Comprehension_Pointfree_Examples

15:41:25 HOL-ex: theory HOL-ex.Set_Theory

15:41:25 HOL-ex: theory HOL-ex.Simproc_Tests

15:41:26 HOL-Codegenerator_Test: theory HOL-Data_Structures.Less_False

15:41:26 HOL-Codegenerator_Test: theory HOL-Data_Structures.Cmp

15:41:26 HOL-Codegenerator_Test: theory HOL-Data_Structures.Sorted_Less

15:41:26 HOL-Codegenerator_Test: theory HOL-Data_Structures.AList_Upd_Del

15:41:27 HOL-Codegenerator_Test: theory HOL-Data_Structures.List_Ins_Del

15:41:27 HOL-Codegenerator_Test: theory HOL-Data_Structures.Map_Specs

15:41:27 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Lazy_Test

15:41:27 HOL-Codegenerator_Test: theory HOL-Data_Structures.Set_Specs

15:41:27 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Set

15:41:29 HOL-Codegenerator_Test: theory HOL-Data_Structures.Tree_Map

15:41:30 HOL-Codegenerator_Test: theory HOL-ex.Records

15:41:30 HOL-Decision_Procs: theory HOL-Decision_Procs.Decision_Procs

15:41:33 HOL-ex: theory HOL-ex.Sudoku

15:41:35 HOL-ex: theory HOL-ex.Tarski

15:41:35 HOL-ex: theory HOL-ex.Termination

15:41:36 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Candidates

15:41:36 HOL-ex: theory HOL-ex.ThreeDivides

15:41:36 HOL-ex: theory HOL-ex.Transfer_Int_Nat

15:41:36 HOL-ex: theory HOL-ex.Tree23

15:41:40 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_PolyML

15:41:40 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_Scala

15:41:40 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate

15:41:40 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Binary_Nat

15:41:43 HOL-ex: theory HOL-ex.Unification

15:41:45 HOL-ex: theory HOL-ex.Word_Type

15:41:47 HOL-ex: theory HOL-ex.veriT_Preprocessing

15:41:47 HOL-ex: theory HOL-ex.Transfer_Debug

15:41:47 HOL-ex: theory HOL-ex.Function_Growth

15:41:49 HOL-ex: theory HOL-ex.SOS

15:41:49 HOL-ex: theory HOL-ex.SOS_Cert

15:41:49 HOL-ex: theory HOL-ex.Argo_Examples

15:41:52 HOL-ex: theory HOL-ex.Ballot

15:41:53 HOL-ex: theory HOL-ex.BinEx

15:41:54 HOL-ex: theory HOL-ex.Code_Binary_Nat_examples

15:41:54 HOL-ex: theory HOL-ex.Cubic_Quartic

15:41:54 HOL-ex: theory HOL-ex.Dedekind_Real

15:41:56 HOL-ex: theory HOL-ex.Eval_Examples

15:41:58 HOL-ex: theory HOL-ex.Gauge_Integration

15:41:58 HOL-ex: theory HOL-ex.HarmonicSeries

15:41:58 HOL-ex: theory HOL-ex.Normalization_by_Evaluation

15:42:00 HOL-ex: theory HOL-ex.Parallel_Example

15:42:00 HOL-ex: theory HOL-ex.Pythagoras

15:42:00 HOL-ex: theory HOL-ex.Reflection_Examples

15:42:20 HOL-ex: theory HOL-ex.Sqrt

15:42:20 HOL-ex: theory HOL-ex.Sqrt_Script

15:42:21 HOL-ex: theory HOL-ex.Sum_of_Powers

15:44:57 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Efficient_Datastructures

15:44:58 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Generate_Target_Nat

15:47:31 Timing HOL-Decision_Procs (2 threads, 685.088s elapsed time, 1247.732s cpu time, 102.500s GC time, factor 1.82)

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

15:47:31 Finished HOL-Decision_Procs (0:11:28 elapsed time, 0:20:50 cpu time, factor 1.82)

15:47:31 Running HOL-Nitpick_Examples ...

15:47:35 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Core_Nits

15:47:35 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Datatype_Nits

15:47:37 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Hotel_Nits

15:47:38 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Induct_Nits

15:47:38 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Integer_Nits

15:47:39 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Mini_Nits

15:47:41 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Mono_Nits

15:47:42 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Pattern_Nits

15:47:43 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Record_Nits

15:47:44 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Refute_Nits

15:48:01 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Special_Nits

15:48:02 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Tests_Nits

15:48:04 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Manual_Nits

15:48:11 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Typedef_Nits

15:48:47 HOL-Nitpick_Examples: theory HOL-Nitpick_Examples.Nitpick_Examples

15:48:48 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_GHC

15:48:50 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_MLton

15:48:57 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_OCaml

15:48:58 HOL-Codegenerator_Test: theory HOL-Codegenerator_Test.Code_Test_SMLNJ

15:49:00 Timing HOL-Codegenerator_Test (2 threads, 452.915s elapsed time, 420.048s cpu time, 16.304s GC time, factor 0.93)

15:49:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Codegenerator_Test

15:49:00 Finished HOL-Codegenerator_Test (0:07:36 elapsed time, 0:18:09 cpu time, factor 2.39)

15:49:00 Running HOL-Corec_Examples ...

15:49:02 HOL-Corec_Examples: theory HOL-Corec_Examples.Iterate_GPV

15:49:02 HOL-Corec_Examples: theory HOL-Corec_Examples.LFilter

15:49:06 HOL-Corec_Examples: theory HOL-Corec_Examples.Simple_Nesting

15:49:14 HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Processor

15:49:29 HOL-Corec_Examples: theory HOL-Corec_Examples.Paper_Examples

15:49:55 HOL-ex: theory HOL-ex.Meson_Test

15:49:55 HOL-ex: theory HOL-ex.SAT_Examples

15:50:07 Timing HOL-ex (2 threads, 548.302s elapsed time, 931.712s cpu time, 45.472s GC time, factor 1.70)

15:50:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex

15:50:07 Finished HOL-ex (0:09:11 elapsed time, 0:16:01 cpu time, factor 1.74)

15:50:07 Running HOL-Hoare_Parallel ...

15:50:08 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Graph

15:50:08 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Com

15:50:09 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Quote_Antiquote

15:50:09 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Com

15:50:11 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Tran

15:50:12 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tran

15:50:13 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Hoare

15:50:14 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Hoare

15:50:15 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Tactics

15:50:15 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Syntax

15:50:15 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.RG_Examples

15:50:15 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Syntax

15:50:15 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Gar_Coll

15:50:17 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Mul_Gar_Coll

15:50:17 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.OG_Examples

15:50:21 HOL-Hoare_Parallel: theory HOL-Hoare_Parallel.Hoare_Parallel

15:50:23 HOL-Corec_Examples: theory HOL-Corec_Examples.GPV_Bare_Bones

15:50:23 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_A

15:50:28 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_B

15:50:32 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_C

15:50:36 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_Poly

15:50:37 HOL-Corec_Examples: theory HOL-Corec_Examples.Merge_D

15:50:46 HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Mono

15:51:29 HOL-Corec_Examples: theory HOL-Corec_Examples.Misc_Poly

15:52:43 HOL-Corec_Examples: theory HOL-Corec_Examples.Small_Concrete

15:53:08 Timing HOL-Nitpick_Examples (2 threads, 331.983s elapsed time, 149.660s cpu time, 2.900s GC time, factor 0.45)

15:53:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nitpick_Examples

15:53:08 Finished HOL-Nitpick_Examples (0:05:36 elapsed time, 0:11:03 cpu time, factor 1.97)

15:53:08 Running HOL-Datatype_Examples ...

15:53:10 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Compat

15:53:10 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lift_BNF

15:53:13 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Milner_Tofte

15:53:16 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFI

15:53:17 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Koenig

15:53:17 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Process

15:53:19 HOL-Corec_Examples: theory HOL-Corec_Examples.Stream_Friends

15:53:22 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Stream_Processor

15:53:23 Timing HOL-Hoare_Parallel (2 threads, 188.130s elapsed time, 324.220s cpu time, 5.108s GC time, factor 1.72)

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

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

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

15:53:23 Finished HOL-Hoare_Parallel (0:03:15 elapsed time, 0:05:35 cpu time, factor 1.71)

15:53:23 Running HOL-MicroJava ...

15:53:24 HOL-MicroJava: theory HOL-Eisbach.Eisbach

15:53:24 HOL-MicroJava: theory HOL-MicroJava.Semilat

15:53:25 HOL-MicroJava: theory HOL-MicroJava.Err

15:53:25 HOL-MicroJava: theory HOL-MicroJava.JBasis

15:53:25 HOL-MicroJava: theory HOL-MicroJava.AuxLemmas

15:53:26 HOL-MicroJava: theory HOL-MicroJava.Type

15:53:26 HOL-MicroJava: theory HOL-MicroJava.Listn

15:53:26 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Lambda_Term

15:53:27 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework

15:53:27 HOL-MicroJava: theory HOL-MicroJava.Opt

15:53:27 HOL-MicroJava: theory HOL-MicroJava.Product

15:53:27 HOL-MicroJava: theory HOL-MicroJava.SemilatAlg

15:53:27 HOL-MicroJava: theory HOL-MicroJava.Kildall

15:53:27 HOL-MicroJava: theory HOL-MicroJava.LBVSpec

15:53:28 HOL-Corec_Examples: theory HOL-Corec_Examples.TLList_Friends

15:53:28 HOL-MicroJava: theory HOL-MicroJava.Decl

15:53:28 HOL-MicroJava: theory HOL-MicroJava.SystemClasses

15:53:28 HOL-MicroJava: theory HOL-MicroJava.TypeRel

15:53:28 HOL-MicroJava: theory HOL-MicroJava.Value

15:53:29 HOL-MicroJava: theory HOL-MicroJava.WellForm

15:53:29 HOL-MicroJava: theory HOL-MicroJava.State

15:53:30 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Codatatype

15:53:30 HOL-MicroJava: theory HOL-MicroJava.Term

15:53:30 HOL-MicroJava: theory HOL-MicroJava.Exceptions

15:53:30 HOL-MicroJava: theory HOL-MicroJava.LBVComplete

15:53:31 HOL-MicroJava: theory HOL-MicroJava.LBVCorrect

15:53:31 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_err

15:53:31 HOL-MicroJava: theory HOL-MicroJava.Abstract_BV

15:53:31 HOL-MicroJava: theory HOL-MicroJava.Semilattices

15:53:32 HOL-MicroJava: theory HOL-MicroJava.JType

15:53:32 HOL-MicroJava: theory HOL-MicroJava.JVMType

15:53:34 HOL-MicroJava: theory HOL-MicroJava.WellType

15:53:35 HOL-MicroJava: theory HOL-MicroJava.Conform

15:53:36 HOL-MicroJava: theory HOL-MicroJava.JVMState

15:53:36 HOL-MicroJava: theory HOL-MicroJava.JVMInstructions

15:53:36 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Datatype

15:53:36 HOL-MicroJava: theory HOL-MicroJava.Eval

15:53:37 HOL-MicroJava: theory HOL-MicroJava.JVMExceptions

15:53:37 HOL-MicroJava: theory HOL-MicroJava.JVMExecInstr

15:53:38 HOL-MicroJava: theory HOL-MicroJava.JVMExec

15:53:38 HOL-MicroJava: theory HOL-MicroJava.DefsComp

15:53:38 HOL-MicroJava: theory HOL-MicroJava.Index

15:53:39 HOL-MicroJava: theory HOL-MicroJava.JVMDefensive

15:53:40 HOL-MicroJava: theory HOL-MicroJava.JVMListExample

15:53:40 HOL-MicroJava: theory HOL-MicroJava.Example

15:53:41 HOL-MicroJava: theory HOL-MicroJava.JListExample

15:53:42 HOL-MicroJava: theory HOL-MicroJava.JTypeSafe

15:53:42 HOL-MicroJava: theory HOL-MicroJava.TypeInf

15:53:42 HOL-MicroJava: theory HOL-MicroJava.Effect

15:53:42 HOL-MicroJava: theory HOL-MicroJava.TranslCompTp

15:53:43 HOL-MicroJava: theory HOL-MicroJava.TranslComp

15:53:43 HOL-MicroJava: theory HOL-MicroJava.LemmasComp

15:53:44 HOL-MicroJava: theory HOL-MicroJava.CorrComp

15:53:48 HOL-Corec_Examples: theory HOL-Corec_Examples.Type_Class

15:54:05 HOL-MicroJava: theory HOL-MicroJava.BVSpec

15:54:06 HOL-MicroJava: theory HOL-MicroJava.Altern

15:54:06 HOL-MicroJava: theory HOL-MicroJava.Correct

15:54:07 HOL-MicroJava: theory HOL-MicroJava.EffectMono

15:54:07 HOL-MicroJava: theory HOL-MicroJava.BVSpecTypeSafe

15:54:07 HOL-MicroJava: theory HOL-MicroJava.Typing_Framework_JVM

15:54:07 HOL-MicroJava: theory HOL-MicroJava.BVNoTypeError

15:54:08 HOL-MicroJava: theory HOL-MicroJava.JVM

15:54:08 HOL-MicroJava: theory HOL-MicroJava.BVExample

15:54:08 HOL-MicroJava: theory HOL-MicroJava.CorrCompTp

15:54:09 HOL-MicroJava: theory HOL-MicroJava.LBVJVM

15:54:10 HOL-MicroJava: theory HOL-MicroJava.MicroJava

15:54:21 Timing HOL-Corec_Examples (2 threads, 317.436s elapsed time, 572.264s cpu time, 58.216s GC time, factor 1.80)

15:54:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Corec_Examples

15:54:21 Finished HOL-Corec_Examples (0:05:19 elapsed time, 0:09:34 cpu time, factor 1.79)

15:54:21 Running HOL-IMP ...

15:54:22 HOL-IMP: theory HOL-IMP.AExp

15:54:22 HOL-IMP: theory HOL-IMP.C_like

15:54:24 HOL-IMP: theory HOL-IMP.ASM

15:54:25 HOL-IMP: theory HOL-IMP.BExp

15:54:26 HOL-IMP: theory HOL-IMP.Complete_Lattice

15:54:26 HOL-IMP: theory HOL-IMP.OO

15:54:27 HOL-IMP: theory HOL-IMP.Com

15:54:28 HOL-IMP: theory HOL-IMP.ACom

15:54:31 HOL-IMP: theory HOL-IMP.Abs_Int_Tests

15:54:31 HOL-IMP: theory HOL-IMP.Big_Step

15:54:32 HOL-IMP: theory HOL-IMP.Denotational

15:54:32 HOL-IMP: theory HOL-IMP.Hoare

15:54:33 HOL-IMP: theory HOL-IMP.Hoare_Examples

15:54:33 HOL-IMP: theory HOL-IMP.Hoare_Total

15:54:33 HOL-IMP: theory HOL-IMP.Hoare_Sound_Complete

15:54:33 HOL-IMP: theory HOL-IMP.Hoare_Total_EX

15:54:33 HOL-IMP: theory HOL-IMP.VCG_Total_EX

15:54:35 HOL-IMP: theory HOL-IMP.Hoare_Total_EX2

15:54:35 HOL-IMP: theory HOL-IMP.VCG_Total_EX2

15:54:39 HOL-IMP: theory HOL-IMP.VCG

15:54:40 HOL-IMP: theory HOL-IMP.Sec_Type_Expr

15:54:40 HOL-IMP: theory HOL-IMP.Sem_Equiv

15:54:40 HOL-IMP: theory HOL-IMP.Vars

15:54:40 HOL-IMP: theory HOL-IMP.Sec_Typing

15:54:41 HOL-IMP: theory HOL-IMP.Sec_TypingT

15:54:41 HOL-IMP: theory HOL-IMP.Procs

15:54:41 HOL-IMP: theory HOL-IMP.Def_Init

15:54:41 HOL-IMP: theory HOL-IMP.Def_Init_Exp

15:54:41 HOL-IMP: theory HOL-IMP.Def_Init_Big

15:54:42 HOL-IMP: theory HOL-IMP.Fold

15:54:42 HOL-IMP: theory HOL-IMP.Live

15:54:43 HOL-IMP: theory HOL-IMP.Procs_Dyn_Vars_Dyn

15:54:44 HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Dyn

15:54:44 HOL-IMP: theory HOL-IMP.Procs_Stat_Vars_Stat

15:54:45 HOL-IMP: theory HOL-IMP.Collecting

15:54:46 HOL-IMP: theory HOL-IMP.Collecting1

15:54:46 HOL-IMP: theory HOL-IMP.Collecting_Examples

15:54:46 HOL-IMP: theory HOL-IMP.Star

15:54:46 HOL-IMP: theory HOL-IMP.Compiler

15:54:47 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primcorec

15:54:49 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Prelim

15:54:49 HOL-Datatype_Examples: theory HOL-Datatype_Examples.DTree

15:54:50 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Gram_Lang

15:54:50 HOL-IMP: theory HOL-IMP.Def_Init_Small

15:54:51 HOL-IMP: theory HOL-IMP.Small_Step

15:54:51 HOL-IMP: theory HOL-IMP.Compiler2

15:54:52 HOL-IMP: theory HOL-IMP.Abs_Int_init

15:54:52 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Parallel_Composition

15:54:52 HOL-Datatype_Examples: theory HOL-Datatype_Examples.TreeFsetI

15:54:52 HOL-IMP: theory HOL-IMP.Finite_Reachable

15:54:52 HOL-IMP: theory HOL-IMP.Live_True

15:54:52 HOL-IMP: theory HOL-IMP.Abs_Int0

15:54:53 HOL-IMP: theory HOL-IMP.Types

15:54:54 HOL-IMP: theory HOL-IMP.Abs_State

15:54:55 HOL-IMP: theory HOL-IMP.Abs_Int1

15:54:56 HOL-IMP: theory HOL-IMP.Abs_Int1_const

15:54:57 HOL-IMP: theory HOL-IMP.Abs_Int1_parity

15:54:58 HOL-IMP: theory HOL-IMP.Abs_Int2

15:54:58 HOL-IMP: theory HOL-IMP.Poly_Types

15:55:00 HOL-IMP: theory HOL-IMP.Abs_Int2_ivl

15:55:02 HOL-IMP: theory HOL-IMP.Abs_Int3

15:55:13 HOL-Datatype_Examples: theory HOL-Datatype_Examples.Misc_Primrec

15:56:05 Timing HOL-Datatype_Examples (2 threads, 173.496s elapsed time, 340.924s cpu time, 43.260s GC time, factor 1.97)

15:56:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Datatype_Examples

15:56:05 Finished HOL-Datatype_Examples (0:02:56 elapsed time, 0:05:42 cpu time, factor 1.95)

15:56:05 Running HOL-Proofs-Lambda ...

15:56:07 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Commutation

15:56:07 HOL-Proofs-Lambda: theory HOL-Library.Code_Target_Int

15:56:08 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Lambda

15:56:08 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListOrder

15:56:10 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListApplication

15:56:11 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.LambdaType

15:56:12 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ParRed

15:56:14 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Eta

15:56:17 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListBeta

15:56:18 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.InductTermi

15:56:19 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.StrongNorm

15:56:20 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.NormalForm

15:56:21 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Standardization

15:56:22 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.WeakNorm

15:56:25 Timing HOL-MicroJava (2 threads, 174.468s elapsed time, 298.344s cpu time, 11.420s GC time, factor 1.71)

15:56:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava

15:56:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/document.pdf

15:56:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/outline.pdf

15:56:25 Finished HOL-MicroJava (0:03:01 elapsed time, 0:05:10 cpu time, factor 1.71)

15:56:25 Running HOL-Quickcheck_Examples ...

15:56:27 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Interfaces

15:56:27 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Completeness

15:56:27 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples

15:56:27 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting

15:56:27 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Examples

15:56:28 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Nesting_Example

15:57:03 Timing HOL-IMP (2 threads, 154.156s elapsed time, 261.984s cpu time, 14.248s GC time, factor 1.70)

15:57:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP

15:57:03 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP/document.pdf

15:57:03 Finished HOL-IMP (0:02:41 elapsed time, 0:04:31 cpu time, factor 1.68)

15:57:03 Running HOL-Bali ...

15:57:04 HOL-Bali: theory HOL-Bali.Basis

15:57:06 HOL-Bali: theory HOL-Bali.Name

15:57:06 HOL-Bali: theory HOL-Bali.Table

15:57:08 HOL-Bali: theory HOL-Bali.Type

15:57:09 HOL-Bali: theory HOL-Bali.Value

15:57:10 HOL-Bali: theory HOL-Bali.Term

15:57:33 HOL-Bali: theory HOL-Bali.Decl

15:57:34 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Hotel_Example

15:57:34 HOL-Quickcheck_Examples: theory HOL-Quickcheck_Examples.Quickcheck_Narrowing_Examples

15:57:39 HOL-Bali: theory HOL-Bali.TypeRel

15:57:40 HOL-Bali: theory HOL-Bali.DeclConcepts

15:57:42 HOL-Bali: theory HOL-Bali.State

15:57:42 HOL-Bali: theory HOL-Bali.WellType

15:57:45 HOL-Bali: theory HOL-Bali.Conform

15:57:45 HOL-Bali: theory HOL-Bali.Eval

15:57:48 HOL-Bali: theory HOL-Bali.DefiniteAssignment

15:57:54 HOL-Bali: theory HOL-Bali.WellForm

15:57:56 HOL-Bali: theory HOL-Bali.DefiniteAssignmentCorrect

15:57:56 HOL-Bali: theory HOL-Bali.Example

15:57:57 HOL-Bali: theory HOL-Bali.TypeSafe

15:57:59 HOL-Bali: theory HOL-Bali.Evaln

15:58:02 HOL-Bali: theory HOL-Bali.AxSem

15:58:03 HOL-Bali: theory HOL-Bali.Trans

15:58:07 HOL-Bali: theory HOL-Bali.AxCompl

15:58:07 HOL-Bali: theory HOL-Bali.AxSound

15:58:07 HOL-Bali: theory HOL-Bali.AxExample

15:58:40 Timing HOL-Proofs-Lambda (2 threads, 148.674s elapsed time, 170.488s cpu time, 5.968s GC time, factor 1.15)

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

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

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

15:58:40 Finished HOL-Proofs-Lambda (0:02:35 elapsed time, 0:03:00 cpu time, factor 1.16)

15:58:40 Running HOL-Predicate_Compile_Examples ...

15:58:42 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_1

15:58:42 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_2

15:58:43 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_3

15:58:43 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.IMP_4

15:58:44 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Quickcheck_Examples

15:58:44 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Predicate_Compile_Tests

15:58:45 Timing HOL-Quickcheck_Examples (2 threads, 137.072s elapsed time, 157.596s cpu time, 5.620s GC time, factor 1.15)

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

15:58:45 Finished HOL-Quickcheck_Examples (0:02:19 elapsed time, 0:04:18 cpu time, factor 1.86)

15:58:45 Running HOL-Proofs-Extraction ...

15:58:46 HOL-Proofs-Extraction: theory HOL-Library.Cancellation

15:58:46 HOL-Proofs-Extraction: theory HOL-Library.Code_Abstract_Nat

15:58:46 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Nat

15:58:47 HOL-Proofs-Extraction: theory HOL-Library.Multiset

15:58:47 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Int

15:58:49 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Numeral

15:58:49 HOL-Proofs-Extraction: theory HOL-Library.Open_State_Syntax

15:58:49 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Warshall

15:58:50 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Examples

15:59:06 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman

15:59:07 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Specialisation_Examples

15:59:07 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman_Extraction

15:59:16 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Factorial_Ring

15:59:31 Timing HOL-Bali (2 threads, 127.749s elapsed time, 229.032s cpu time, 15.340s GC time, factor 1.79)

15:59:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali

15:59:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/document.pdf

15:59:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/outline.pdf

15:59:31 Finished HOL-Bali (0:02:27 elapsed time, 0:04:11 cpu time, factor 1.71)

15:59:31 Running HOL-Imperative_HOL ...

15:59:31 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Util

15:59:31 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Pigeonhole

15:59:32 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Sorted_List

15:59:32 HOL-Imperative_HOL: theory HOL-Imperative_HOL.List_Sublist

15:59:33 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap

15:59:38 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Heap_Monad

15:59:42 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Array

15:59:44 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Ref

15:59:44 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL

15:59:45 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Linked_Lists

15:59:45 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Overview

15:59:46 HOL-Imperative_HOL: theory HOL-Imperative_HOL.SatChecker

15:59:58 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Subarray

15:59:59 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Quicksort

16:00:12 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Euclidean_Algorithm

16:00:20 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_Reverse

16:00:25 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.QuotRem

16:00:26 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Primes

16:00:31 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Greatest_Common_Divisor

16:00:33 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Code_Prolog_Examples

16:00:33 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Context_Free_Grammar_Example

16:00:35 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Lambda_Example

16:00:37 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example

16:00:38 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.List_Examples

16:00:43 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Hotel_Example_Prolog

16:00:46 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Euclid

16:00:49 HOL-Predicate_Compile_Examples: theory HOL-Predicate_Compile_Examples.Reg_Exp_Example

16:00:53 HOL-Imperative_HOL: theory HOL-Imperative_HOL.Imperative_HOL_ex

16:00:59 Timing HOL-Predicate_Compile_Examples (2 threads, 135.971s elapsed time, 202.868s cpu time, 13.024s GC time, factor 1.49)

16:00:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Predicate_Compile_Examples

16:00:59 Finished HOL-Predicate_Compile_Examples (0:02:18 elapsed time, 0:04:56 cpu time, factor 2.14)

16:00:59 Running HOL-Word-SMT_Examples ...

16:01:00 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.Boogie

16:01:00 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Word_Examples

16:01:00 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Examples

16:01:01 HOL-Word-SMT_Examples: theory HOL-Word-SMT_Examples.SMT_Tests

16:01:22 Timing HOL-Imperative_HOL (2 threads, 105.538s elapsed time, 78.992s cpu time, 2.684s GC time, factor 0.75)

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

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

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

16:01:22 Finished HOL-Imperative_HOL (0:01:50 elapsed time, 0:04:31 cpu time, factor 2.45)

16:01:22 Running HOL-UNITY ...

16:01:24 HOL-UNITY: theory HOL-UNITY.ListOrder

16:01:24 HOL-UNITY: theory HOL-UNITY.UNITY

16:01:24 HOL-UNITY: theory HOL-UNITY.Constrains

16:01:24 HOL-UNITY: theory HOL-UNITY.Deadlock

16:01:24 HOL-UNITY: theory HOL-UNITY.FP

16:01:24 HOL-UNITY: theory HOL-UNITY.Network

16:01:25 HOL-UNITY: theory HOL-UNITY.WFair

16:01:26 HOL-UNITY: theory HOL-UNITY.SubstAx

16:01:26 HOL-UNITY: theory HOL-UNITY.Token

16:01:26 HOL-UNITY: theory HOL-UNITY.Detects

16:01:27 HOL-UNITY: theory HOL-UNITY.Follows

16:01:27 HOL-UNITY: theory HOL-UNITY.Union

16:01:27 HOL-UNITY: theory HOL-UNITY.Comp

16:01:28 HOL-UNITY: theory HOL-UNITY.Guar

16:01:28 HOL-UNITY: theory HOL-UNITY.Extend

16:01:29 HOL-UNITY: theory HOL-UNITY.Transformers

16:01:30 HOL-UNITY: theory HOL-UNITY.Project

16:01:30 HOL-UNITY: theory HOL-UNITY.Rename

16:01:30 HOL-UNITY: theory HOL-UNITY.Lift_prog

16:01:30 HOL-UNITY: theory HOL-UNITY.ELT

16:01:30 HOL-UNITY: theory HOL-UNITY.PPROD

16:01:31 HOL-UNITY: theory HOL-UNITY.ProgressSets

16:01:31 HOL-UNITY: theory HOL-UNITY.UNITY_Main

16:01:32 HOL-UNITY: theory HOL-UNITY.AllocBase

16:01:32 HOL-UNITY: theory HOL-UNITY.Channel

16:01:32 HOL-UNITY: theory HOL-UNITY.Common

16:01:32 HOL-UNITY: theory HOL-UNITY.Counter

16:01:32 HOL-UNITY: theory HOL-UNITY.Alloc

16:01:33 HOL-UNITY: theory HOL-UNITY.AllocImpl

16:01:35 Timing HOL-Proofs-Extraction (2 threads, 164.999s elapsed time, 247.408s cpu time, 12.508s GC time, factor 1.50)

16:01:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction

16:01:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/document.pdf

16:01:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/outline.pdf

16:01:35 Finished HOL-Proofs-Extraction (0:02:50 elapsed time, 0:04:15 cpu time, factor 1.50)

16:01:35 Running HOL-SET_Protocol ...

16:01:36 HOL-UNITY: theory HOL-UNITY.Client

16:01:36 HOL-UNITY: theory HOL-UNITY.Counterc

16:01:37 HOL-UNITY: theory HOL-UNITY.Handshake

16:01:37 HOL-UNITY: theory HOL-UNITY.Lift

16:01:37 HOL-SET_Protocol: theory HOL-SET_Protocol.Message_SET

16:01:37 HOL-UNITY: theory HOL-UNITY.Mutex

16:01:37 HOL-UNITY: theory HOL-UNITY.NSP_Bad

16:01:38 HOL-UNITY: theory HOL-UNITY.PriorityAux

16:01:38 HOL-UNITY: theory HOL-UNITY.Priority

16:01:38 HOL-UNITY: theory HOL-UNITY.Progress

16:01:38 HOL-UNITY: theory HOL-UNITY.Reach

16:01:38 HOL-UNITY: theory HOL-UNITY.TimerArray

16:01:38 HOL-UNITY: theory HOL-UNITY.Reachability

16:01:40 HOL-SET_Protocol: theory HOL-SET_Protocol.Event_SET

16:01:41 HOL-SET_Protocol: theory HOL-SET_Protocol.Public_SET

16:01:42 HOL-SET_Protocol: theory HOL-SET_Protocol.Cardholder_Registration

16:01:42 HOL-SET_Protocol: theory HOL-SET_Protocol.Merchant_Registration

16:01:43 HOL-SET_Protocol: theory HOL-SET_Protocol.Purchase

16:01:45 HOL-SET_Protocol: theory HOL-SET_Protocol.SET_Protocol

16:02:09 Timing HOL-Word-SMT_Examples (2 threads, 67.969s elapsed time, 91.508s cpu time, 0.984s GC time, factor 1.35)

16:02:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-SMT_Examples

16:02:09 Finished HOL-Word-SMT_Examples (0:01:09 elapsed time, 0:01:36 cpu time, factor 1.37)

16:02:09 Running Corec ...

16:02:11 Corec: theory Datatypes.Setup

16:02:11 Corec: theory Corec.Corec

16:02:39 Timing HOL-SET_Protocol (2 threads, 56.899s elapsed time, 96.976s cpu time, 3.064s GC time, factor 1.70)

16:02:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol

16:02:39 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/document.pdf

16:02:39 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/outline.pdf

16:02:39 Finished HOL-SET_Protocol (0:01:02 elapsed time, 0:01:45 cpu time, factor 1.69)

16:02:39 Running Datatypes ...

16:02:40 Datatypes: theory Datatypes.Setup

16:02:40 Datatypes: theory Datatypes.Datatypes

16:02:40 Timing HOL-UNITY (2 threads, 69.749s elapsed time, 107.856s cpu time, 8.540s GC time, factor 1.55)

16:02:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY

16:02:40 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/document.pdf

16:02:40 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/outline.pdf

16:02:40 Finished HOL-UNITY (0:01:18 elapsed time, 0:02:00 cpu time, factor 1.54)

16:02:40 Running HOL-Probability-ex ...

16:02:43 HOL-Probability-ex: theory HOL-Library.Permutation

16:02:43 HOL-Probability-ex: theory HOL-Probability-ex.Dining_Cryptographers

16:02:43 HOL-Probability-ex: theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure

16:02:43 HOL-Probability-ex: theory HOL-Probability-ex.Measure_Not_CCC

16:03:13 Timing Corec (2 threads, 57.447s elapsed time, 84.432s cpu time, 6.000s GC time, factor 1.47)

16:03:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec

16:03:13 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec/corec.pdf

16:03:13 Finished Corec (0:01:03 elapsed time, 0:01:30 cpu time, factor 1.43)

16:03:13 Running HOL-Metis_Examples ...

16:03:15 HOL-Metis_Examples: theory HOL-Decision_Procs.Dense_Linear_Order

16:03:15 HOL-Metis_Examples: theory HOL-Metis_Examples.Abstraction

16:03:15 HOL-Metis_Examples: theory HOL-Metis_Examples.Binary_Tree

16:03:16 HOL-Metis_Examples: theory HOL-Metis_Examples.Message

16:03:17 HOL-Metis_Examples: theory HOL-Metis_Examples.Big_O

16:03:18 HOL-Metis_Examples: theory HOL-Metis_Examples.Sets

16:03:18 HOL-Metis_Examples: theory HOL-Metis_Examples.Tarski

16:03:19 HOL-Metis_Examples: theory HOL-Metis_Examples.Trans_Closure

16:03:20 HOL-Metis_Examples: theory HOL-Metis_Examples.Type_Encodings

16:03:20 HOL-Metis_Examples: theory HOL-Metis_Examples.Proxies

16:03:20 HOL-Metis_Examples: theory HOL-Metis_Examples.Clausification

16:03:28 Timing HOL-Probability-ex (2 threads, 43.863s elapsed time, 53.708s cpu time, 1.700s GC time, factor 1.22)

16:03:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability-ex

16:03:28 Finished HOL-Probability-ex (0:00:47 elapsed time, 0:00:55 cpu time, factor 1.18)

16:03:28 Running HOL-Analysis-ex ...

16:03:29 HOL-Analysis-ex: theory HOL-Analysis-ex.Approximations

16:03:32 Timing Datatypes (2 threads, 46.667s elapsed time, 67.628s cpu time, 5.368s GC time, factor 1.45)

16:03:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes

16:03:32 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes/datatypes.pdf

16:03:32 Finished Datatypes (0:00:53 elapsed time, 0:01:14 cpu time, factor 1.40)

16:03:32 Running HOL-Quotient_Examples ...

16:03:35 HOL-Quotient_Examples: theory HOL-Quotient_Examples.DList

16:03:35 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Int

16:03:35 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_FSet

16:03:36 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Int_Pow

16:03:36 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_DList

16:03:36 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_FSet

16:03:37 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Fun

16:03:37 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lift_Set

16:03:38 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Lifting_Code_Dt_Test

16:03:38 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Message

16:03:39 HOL-Quotient_Examples: theory HOL-Quotient_Examples.Quotient_Rat

16:03:58 Timing HOL-Metis_Examples (2 threads, 42.276s elapsed time, 65.200s cpu time, 3.916s GC time, factor 1.54)

16:03:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Metis_Examples

16:03:58 Finished HOL-Metis_Examples (0:00:44 elapsed time, 0:01:22 cpu time, factor 1.86)

16:03:58 Running Tutorial ...

16:03:59 Tutorial: theory Tutorial.ToyList_Test

16:04:00 Tutorial: theory Tutorial.AB

16:04:00 Tutorial: theory Tutorial.ABexpr

16:04:01 Tutorial: theory Tutorial.AdvancedInd

16:04:01 Tutorial: theory Tutorial.Base

16:04:01 Tutorial: theory Tutorial.CTL

16:04:02 Tutorial: theory Tutorial.CTLind

16:04:02 Tutorial: theory Tutorial.PDL

16:04:03 Tutorial: theory Tutorial.CodeGen

16:04:03 Tutorial: theory Tutorial.Nested

16:04:05 Tutorial: theory Tutorial.Even

16:04:06 Tutorial: theory Tutorial.Fundata

16:04:06 Tutorial: theory Tutorial.Advanced

16:04:06 Tutorial: theory Tutorial.Ifexpr

16:04:08 Tutorial: theory Tutorial.Itrev

16:04:08 Tutorial: theory Tutorial.Mutual

16:04:09 Tutorial: theory Tutorial.Option2

16:04:09 Tutorial: theory Tutorial.Plus

16:04:09 Tutorial: theory Tutorial.Star

16:04:09 Tutorial: theory Tutorial.ToyList

16:04:09 Tutorial: theory Tutorial.Tree

16:04:10 Tutorial: theory Tutorial.Tree2

16:04:10 Tutorial: theory Tutorial.Trie

16:04:10 Tutorial: theory Tutorial.appendix

16:04:10 Tutorial: theory Tutorial.case_exprs

16:04:10 Tutorial: theory Tutorial.fakenat

16:04:10 Tutorial: theory Tutorial.fun0

16:04:11 Timing HOL-Analysis-ex (2 threads, 40.568s elapsed time, 49.720s cpu time, 0.496s GC time, factor 1.23)

16:04:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis-ex

16:04:11 Finished HOL-Analysis-ex (0:00:42 elapsed time, 0:00:51 cpu time, factor 1.20)

16:04:11 Running HOL-Hoare ...

16:04:12 Tutorial: theory Tutorial.natsum

16:04:12 Tutorial: theory Tutorial.pairs2

16:04:12 Tutorial: theory Tutorial.prime_def

16:04:12 Tutorial: theory Tutorial.simp

16:04:12 Tutorial: theory Tutorial.simp2

16:04:12 HOL-Hoare: theory HOL-Hoare.Arith2

16:04:12 HOL-Hoare: theory HOL-Hoare.Heap

16:04:12 Tutorial: theory Tutorial.types

16:04:12 Tutorial: theory Tutorial.unfoldnested

16:04:12 HOL-Hoare: theory HOL-Hoare.Hoare_Logic

16:04:13 HOL-Hoare: theory HOL-Hoare.Hoare_Logic_Abort

16:04:14 HOL-Hoare: theory HOL-Hoare.Examples

16:04:15 HOL-Hoare: theory HOL-Hoare.HeapSyntax

16:04:15 Timing HOL-Quotient_Examples (2 threads, 38.846s elapsed time, 45.932s cpu time, 3.032s GC time, factor 1.18)

16:04:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quotient_Examples

16:04:15 Finished HOL-Quotient_Examples (0:00:42 elapsed time, 0:01:24 cpu time, factor 1.99)

16:04:15 Running HOL-Cardinals ...

16:04:15 HOL-Hoare: theory HOL-Hoare.Pointer_Examples

16:04:15 HOL-Hoare: theory HOL-Hoare.SchorrWaite

16:04:16 HOL-Hoare: theory HOL-Hoare.Pointers0

16:04:16 HOL-Cardinals: theory HOL-Cardinals.Order_Relation_More

16:04:16 HOL-Cardinals: theory HOL-Cardinals.Fun_More

16:04:17 HOL-Cardinals: theory HOL-Cardinals.Order_Union

16:04:17 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Extension

16:04:17 HOL-Cardinals: theory HOL-Cardinals.Wellfounded_More

16:04:17 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Relation

16:04:17 HOL-Hoare: theory HOL-Hoare.ExamplesAbort

16:04:17 HOL-Hoare: theory HOL-Hoare.HeapSyntaxAbort

16:04:17 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Embedding

16:04:17 HOL-Hoare: theory HOL-Hoare.Pointer_ExamplesAbort

16:04:17 HOL-Hoare: theory HOL-Hoare.SepLogHeap

16:04:17 HOL-Cardinals: theory HOL-Cardinals.Wellorder_Constructions

16:04:17 HOL-Hoare: theory HOL-Hoare.Separation

16:04:18 HOL-Hoare: theory HOL-Hoare.Hoare

16:04:19 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Order_Relation

16:04:19 HOL-Cardinals: theory HOL-Cardinals.Ordinal_Arithmetic

16:04:20 HOL-Cardinals: theory HOL-Cardinals.Cardinal_Arithmetic

16:04:21 HOL-Cardinals: theory HOL-Cardinals.Cardinals

16:04:21 HOL-Cardinals: theory HOL-Cardinals.Bounded_Set

16:04:24 Tutorial: theory Tutorial.Message

16:04:24 Tutorial: theory Tutorial.Documents

16:04:27 Tutorial: theory Tutorial.Event

16:04:28 Tutorial: theory Tutorial.Public

16:04:28 Tutorial: theory Tutorial.NS_Public

16:04:29 Tutorial: theory Tutorial.Setup

16:04:29 Tutorial: theory Tutorial.Numbers

16:04:29 Tutorial: theory Tutorial.Basic

16:04:29 Tutorial: theory Tutorial.Blast

16:04:29 Tutorial: theory Tutorial.Force

16:04:29 Tutorial: theory Tutorial.Pairs

16:04:29 Tutorial: theory Tutorial.Records

16:04:30 Tutorial: theory Tutorial.Overloading

16:04:30 Tutorial: theory Tutorial.Axioms

16:04:30 Tutorial: theory Tutorial.Typedefs

16:04:31 Tutorial: theory Tutorial.Examples

16:04:31 Tutorial: theory Tutorial.Functions

16:04:31 Tutorial: theory Tutorial.Recur

16:04:31 Tutorial: theory Tutorial.Relations

16:04:32 Tutorial: theory Tutorial.TPrimes

16:04:32 Tutorial: theory Tutorial.Tacticals

16:04:32 Tutorial: theory Tutorial.find2

16:04:32 Tutorial: theory Tutorial.Forward

16:04:39 Timing Tutorial (2 threads, 33.316s elapsed time, 62.344s cpu time, 9.060s GC time, factor 1.87)

16:04:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial

16:04:39 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial/tutorial.pdf

16:04:39 Finished Tutorial (0:00:40 elapsed time, 0:01:09 cpu time, factor 1.71)

16:04:39 Running HOL-Induct ...

16:04:40 HOL-Induct: theory HOL-Induct.Common_Patterns

16:04:42 Timing HOL-Hoare (2 threads, 25.895s elapsed time, 46.696s cpu time, 1.464s GC time, factor 1.80)

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

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

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

16:04:42 Finished HOL-Hoare (0:00:31 elapsed time, 0:00:55 cpu time, factor 1.77)

16:04:42 Running HOL-SPARK-Examples ...

16:04:43 HOL-Induct: theory HOL-Induct.ABexp

16:04:43 HOL-Induct: theory HOL-Induct.Com

16:04:43 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD

16:04:43 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Lemmas

16:04:43 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Greatest_Common_Divisor

16:04:44 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Longest_Increasing_Subsequence

16:04:44 HOL-SPARK-Examples: theory HOL-SPARK-Examples.RMD_Specification

16:04:44 HOL-SPARK-Examples: theory HOL-SPARK-Examples.F

16:04:45 Timing HOL-Cardinals (2 threads, 22.031s elapsed time, 39.540s cpu time, 1.736s GC time, factor 1.79)

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

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

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

16:04:45 Finished HOL-Cardinals (0:00:29 elapsed time, 0:00:50 cpu time, factor 1.71)

16:04:45 Running HOL-Statespace ...

16:04:46 HOL-Statespace: theory HOL-Statespace.DistinctTreeProver

16:04:46 HOL-Induct: theory HOL-Induct.Comb

16:04:46 HOL-Induct: theory HOL-Induct.Infinitely_Branching_Tree

16:04:47 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Hash

16:04:47 HOL-Statespace: theory HOL-Statespace.StateFun

16:04:47 HOL-Induct: theory HOL-Induct.Nested_Datatype

16:04:47 HOL-Statespace: theory HOL-Statespace.StateSpaceLocale

16:04:48 HOL-Statespace: theory HOL-Statespace.StateSpaceSyntax

16:04:48 HOL-Statespace: theory HOL-Statespace.StateSpaceEx

16:04:48 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_L

16:04:49 HOL-Induct: theory HOL-Induct.Ordinals

16:04:49 HOL-Induct: theory HOL-Induct.PropLog

16:04:49 HOL-SPARK-Examples: theory HOL-SPARK-Examples.K_R

16:04:49 HOL-Induct: theory HOL-Induct.QuoDataType

16:04:49 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_L

16:04:50 HOL-Induct: theory HOL-Induct.QuoNestedDataType

16:04:50 HOL-SPARK-Examples: theory HOL-SPARK-Examples.R_R

16:04:50 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Round

16:04:51 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_L

16:04:51 HOL-Induct: theory HOL-Induct.Sigma_Algebra

16:04:52 HOL-Induct: theory HOL-Induct.Term

16:04:52 HOL-SPARK-Examples: theory HOL-SPARK-Examples.S_R

16:04:53 HOL-Induct: theory HOL-Induct.Sexp

16:04:53 HOL-Induct: theory HOL-Induct.SList

16:04:53 HOL-SPARK-Examples: theory HOL-SPARK-Examples.Sqrt

16:05:04 Timing HOL-SPARK-Examples (2 threads, 19.396s elapsed time, 32.140s cpu time, 0.972s GC time, factor 1.66)

16:05:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Examples

16:05:04 Finished HOL-SPARK-Examples (0:00:21 elapsed time, 0:00:33 cpu time, factor 1.58)

16:05:04 Running HOLCF-Tutorial ...

16:05:05 Timing HOL-Induct (2 threads, 19.771s elapsed time, 37.712s cpu time, 6.728s GC time, factor 1.91)

16:05:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct

16:05:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/document.pdf

16:05:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/outline.pdf

16:05:05 Finished HOL-Induct (0:00:25 elapsed time, 0:00:46 cpu time, factor 1.86)

16:05:05 Running HOL-Matrix_LP ...

16:05:05 HOLCF-Tutorial: theory HOLCF-Tutorial.Domain_ex

16:05:05 HOLCF-Tutorial: theory HOLCF-Tutorial.Fixrec_ex

16:05:06 HOL-Matrix_LP: theory HOL-Matrix_LP.Compute_Oracle

16:05:06 HOL-Matrix_LP: theory HOL-Matrix_LP.LP

16:05:06 HOL-Matrix_LP: theory HOL-Matrix_LP.Matrix

16:05:07 HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeFloat

16:05:07 Timing HOL-Statespace (2 threads, 17.989s elapsed time, 20.908s cpu time, 0.812s GC time, factor 1.16)

16:05:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace

16:05:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/document.pdf

16:05:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/outline.pdf

16:05:07 Finished HOL-Statespace (0:00:22 elapsed time, 0:00:28 cpu time, factor 1.27)

16:05:07 Running HOL-TLA-Memory ...

16:05:08 HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeHOL

16:05:08 HOLCF-Tutorial: theory HOLCF-Tutorial.New_Domain

16:05:08 HOL-Matrix_LP: theory HOL-Matrix_LP.ComputeNumeral

16:05:08 HOL-Matrix_LP: theory HOL-Matrix_LP.SparseMatrix

16:05:08 HOL-TLA-Memory: theory HOL-TLA-Memory.RPCMemoryParams

16:05:08 HOL-TLA-Memory: theory HOL-TLA-Memory.MemoryParameters

16:05:08 HOL-TLA-Memory: theory HOL-TLA-Memory.ProcedureInterface

16:05:09 HOL-TLA-Memory: theory HOL-TLA-Memory.RPCParameters

16:05:09 HOL-TLA-Memory: theory HOL-TLA-Memory.Memory

16:05:10 HOL-TLA-Memory: theory HOL-TLA-Memory.MemClerkParameters

16:05:10 HOL-TLA-Memory: theory HOL-TLA-Memory.RPC

16:05:11 HOL-TLA-Memory: theory HOL-TLA-Memory.MemClerk

16:05:11 HOL-TLA-Memory: theory HOL-TLA-Memory.MemoryImplementation

16:05:12 HOL-Matrix_LP: theory HOL-Matrix_LP.Cplex

16:05:24 Timing HOL-TLA-Memory (2 threads, 14.845s elapsed time, 25.764s cpu time, 0.912s GC time, factor 1.74)

16:05:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Memory

16:05:24 Finished HOL-TLA-Memory (0:00:16 elapsed time, 0:00:26 cpu time, factor 1.63)

16:05:24 Running Isar_Ref ...

16:05:25 Timing HOLCF-Tutorial (2 threads, 16.666s elapsed time, 21.116s cpu time, 0.740s GC time, factor 1.27)

16:05:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial

16:05:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/document.pdf

16:05:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/outline.pdf

16:05:25 Finished HOLCF-Tutorial (0:00:21 elapsed time, 0:00:27 cpu time, factor 1.31)

16:05:25 Running IOA-NTP ...

16:05:26 Isar_Ref: theory Isar_Ref.Base

16:05:26 Timing HOL-Matrix_LP (2 threads, 15.018s elapsed time, 29.064s cpu time, 1.460s GC time, factor 1.94)

16:05:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP

16:05:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/document.pdf

16:05:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/outline.pdf

16:05:26 Finished HOL-Matrix_LP (0:00:20 elapsed time, 0:00:37 cpu time, factor 1.82)

16:05:26 Running Codegen ...

16:05:26 Isar_Ref: theory Isar_Ref.Document_Preparation

16:05:26 Isar_Ref: theory Isar_Ref.First_Order_Logic

16:05:26 Isar_Ref: theory Isar_Ref.Framework

16:05:26 Isar_Ref: theory Isar_Ref.Generic

16:05:27 IOA-NTP: theory IOA-NTP.Lemmas

16:05:27 Isar_Ref: theory Isar_Ref.HOL_Specific

16:05:27 IOA-NTP: theory IOA-NTP.Multiset

16:05:27 IOA-NTP: theory IOA-NTP.Packet

16:05:27 IOA-NTP: theory IOA-NTP.Action

16:05:27 Isar_Ref: theory Isar_Ref.Inner_Syntax

16:05:27 Isar_Ref: theory Isar_Ref.Outer_Syntax

16:05:28 Codegen: theory Codegen.Computations

16:05:28 Codegen: theory Codegen.Adaptation

16:05:28 Isar_Ref: theory Isar_Ref.Preface

16:05:28 Codegen: theory Codegen.Evaluation

16:05:28 Codegen: theory Codegen.Further

16:05:28 Isar_Ref: theory Isar_Ref.Proof

16:05:28 Isar_Ref: theory Isar_Ref.Proof_Script

16:05:28 Codegen: theory Codegen.Inductive_Predicate

16:05:29 Isar_Ref: theory Isar_Ref.Quick_Reference

16:05:29 Isar_Ref: theory Isar_Ref.Spec

16:05:29 IOA-NTP: theory IOA-NTP.Abschannel

16:05:29 IOA-NTP: theory IOA-NTP.Receiver

16:05:29 Codegen: theory Codegen.Introduction

16:05:29 Isar_Ref: theory Isar_Ref.Symbols

16:05:29 IOA-NTP: theory IOA-NTP.Sender

16:05:30 Isar_Ref: theory Isar_Ref.Synopsis

16:05:30 IOA-NTP: theory IOA-NTP.Spec

16:05:30 IOA-NTP: theory IOA-NTP.Impl

16:05:31 Codegen: theory Codegen.Foundations

16:05:31 Codegen: theory Codegen.Refinement

16:05:31 IOA-NTP: theory IOA-NTP.Correctness

16:05:35 Timing IOA-NTP (2 threads, 7.541s elapsed time, 14.232s cpu time, 0.748s GC time, factor 1.89)

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

16:05:35 Finished IOA-NTP (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.65)

16:05:35 Running HOL-TPTP ...

16:05:37 HOL-TPTP: theory HOL-TPTP.TPTP_Parser

16:05:37 HOL-TPTP: theory HOL-TPTP.MaSh_Export_Base

16:05:37 HOL-TPTP: theory HOL-TPTP.MaSh_Eval

16:05:37 HOL-TPTP: theory HOL-TPTP.ATP_Theory_Export

16:05:37 HOL-TPTP: theory HOL-TPTP.THF_Arith

16:05:41 HOL-TPTP: theory HOL-TPTP.TPTP_Interpret

16:05:41 Timing Codegen (2 threads, 8.180s elapsed time, 15.992s cpu time, 0.656s GC time, factor 1.96)

16:05:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen

16:05:41 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen/codegen.pdf

16:05:41 Finished Codegen (0:00:14 elapsed time, 0:00:22 cpu time, factor 1.54)

16:05:41 Running HOL-Mirabelle-ex ...

16:05:41 HOL-TPTP: theory HOL-TPTP.TPTP_Proof_Reconstruction

16:05:42 HOL-Mirabelle-ex: theory HOL-Mirabelle-ex.Ex

16:05:43 HOL-TPTP: theory HOL-TPTP.ATP_Problem_Import

16:05:45 Timing HOL-TPTP (2 threads, 7.197s elapsed time, 8.368s cpu time, 0.312s GC time, factor 1.16)

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

16:05:45 Finished HOL-TPTP (0:00:09 elapsed time, 0:00:10 cpu time, factor 1.07)

16:05:45 Running HOL-NanoJava ...

16:05:45 HOL-NanoJava: theory HOL-NanoJava.Term

16:05:47 Timing Isar_Ref (2 threads, 10.337s elapsed time, 16.580s cpu time, 1.172s GC time, factor 1.60)

16:05:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref

16:05:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref/isar-ref.pdf

16:05:47 Finished Isar_Ref (0:00:22 elapsed time, 0:00:28 cpu time, factor 1.30)

16:05:47 Running HOL-Unix ...

16:05:48 HOL-Unix: theory HOL-Unix.Nested_Environment

16:05:48 HOL-NanoJava: theory HOL-NanoJava.Decl

16:05:49 HOL-NanoJava: theory HOL-NanoJava.TypeRel

16:05:49 HOL-NanoJava: theory HOL-NanoJava.State

16:05:50 Timing HOL-Mirabelle-ex (2 threads, 6.585s elapsed time, 0.044s cpu time, 0.000s GC time, factor 0.01)

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

16:05:50 Finished HOL-Mirabelle-ex (0:00:08 elapsed time, 0:00:09 cpu time, factor 1.20)

16:05:50 Running HOLCF-IMP ...

16:05:50 HOL-NanoJava: theory HOL-NanoJava.AxSem

16:05:50 HOL-NanoJava: theory HOL-NanoJava.OpSem

16:05:50 HOL-Unix: theory HOL-Unix.Unix

16:05:50 HOL-NanoJava: theory HOL-NanoJava.Equivalence

16:05:51 HOLCF-IMP: theory HOL-IMP.AExp

16:05:51 HOL-NanoJava: theory HOL-NanoJava.Example

16:05:52 HOLCF-IMP: theory HOL-IMP.BExp

16:05:54 HOLCF-IMP: theory HOL-IMP.Com

16:05:55 HOLCF-IMP: theory HOL-IMP.Big_Step

16:05:56 HOLCF-IMP: theory HOLCF-IMP.Denotational

16:05:57 HOLCF-IMP: theory HOLCF-IMP.HoareEx

16:05:57 Timing HOL-NanoJava (2 threads, 6.918s elapsed time, 12.024s cpu time, 0.832s GC time, factor 1.74)

16:05:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava

16:05:57 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/document.pdf

16:05:57 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/outline.pdf

16:05:57 Finished HOL-NanoJava (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.66)

16:05:57 Running Prog_Prove ...

16:05:58 Prog_Prove: theory Prog_Prove.Basics

16:05:58 Prog_Prove: theory Prog_Prove.Bool_nat_list

16:05:58 Prog_Prove: theory Prog_Prove.LaTeXsugar

16:05:58 Prog_Prove: theory Prog_Prove.Isar

16:05:58 Prog_Prove: theory Prog_Prove.Logic

16:05:59 Timing HOL-Unix (2 threads, 6.822s elapsed time, 10.908s cpu time, 0.668s GC time, factor 1.60)

16:05:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix

16:05:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/document.pdf

16:05:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/outline.pdf

16:05:59 Finished HOL-Unix (0:00:11 elapsed time, 0:00:18 cpu time, factor 1.59)

16:05:59 Running IOA-ABP ...

16:05:59 Prog_Prove: theory Prog_Prove.MyList

16:06:00 Prog_Prove: theory Prog_Prove.Types_and_funs

16:06:00 IOA-ABP: theory IOA-ABP.Lemmas

16:06:00 IOA-ABP: theory IOA-ABP.Packet

16:06:00 IOA-ABP: theory IOA-ABP.Action

16:06:01 Timing HOLCF-IMP (2 threads, 6.511s elapsed time, 11.068s cpu time, 0.520s GC time, factor 1.70)

16:06:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP

16:06:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP/document.pdf

16:06:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP/outline.pdf

16:06:01 Finished HOLCF-IMP (0:00:10 elapsed time, 0:00:17 cpu time, factor 1.64)

16:06:01 Running HOL-Isar_Examples ...

16:06:01 IOA-ABP: theory IOA-ABP.Abschannel

16:06:01 IOA-ABP: theory IOA-ABP.Env

16:06:02 IOA-ABP: theory IOA-ABP.Receiver

16:06:02 HOL-Isar_Examples: theory HOL-Isar_Examples.Higher_Order_Logic

16:06:02 HOL-Isar_Examples: theory HOL-Isar_Examples.First_Order_Logic

16:06:02 HOL-Isar_Examples: theory HOL-Isar_Examples.Basic_Logic

16:06:03 HOL-Isar_Examples: theory HOL-Isar_Examples.Cantor

16:06:03 HOL-Isar_Examples: theory HOL-Isar_Examples.Drinker

16:06:03 IOA-ABP: theory IOA-ABP.Sender

16:06:03 HOL-Isar_Examples: theory HOL-Isar_Examples.Expr_Compiler

16:06:03 HOL-Isar_Examples: theory HOL-Isar_Examples.Group

16:06:03 HOL-Isar_Examples: theory HOL-Isar_Examples.Group_Context

16:06:03 HOL-Isar_Examples: theory HOL-Isar_Examples.Group_Notepad

16:06:03 IOA-ABP: theory IOA-ABP.Abschannel_finite

16:06:03 HOL-Isar_Examples: theory HOL-Isar_Examples.Hoare

16:06:03 IOA-ABP: theory IOA-ABP.Impl

16:06:03 IOA-ABP: theory IOA-ABP.Impl_finite

16:06:04 IOA-ABP: theory IOA-ABP.Spec

16:06:04 IOA-ABP: theory IOA-ABP.Correctness

16:06:05 HOL-Isar_Examples: theory HOL-Isar_Examples.Knaster_Tarski

16:06:05 HOL-Isar_Examples: theory HOL-Isar_Examples.Hoare_Ex

16:06:05 HOL-Isar_Examples: theory HOL-Isar_Examples.Mutilated_Checkerboard

16:06:05 HOL-Isar_Examples: theory HOL-Isar_Examples.Peirce

16:06:05 HOL-Isar_Examples: theory HOL-Isar_Examples.Puzzle

16:06:05 HOL-Isar_Examples: theory HOL-Isar_Examples.Structured_Statements

16:06:05 HOL-Isar_Examples: theory HOL-Isar_Examples.Summation

16:06:05 HOL-Isar_Examples: theory HOL-Isar_Examples.Fibonacci

16:06:06 Timing IOA-ABP (2 threads, 5.729s elapsed time, 10.568s cpu time, 0.276s GC time, factor 1.84)

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

16:06:06 Finished IOA-ABP (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.58)

16:06:06 Running HOLCF-ex ...

16:06:07 HOLCF-ex: theory HOLCF-ex.Focus_ex

16:06:07 HOLCF-ex: theory HOLCF-ex.Dagstuhl

16:06:08 HOLCF-ex: theory HOLCF-ex.Concurrency_Monad

16:06:08 HOLCF-ex: theory HOLCF-ex.Dnat

16:06:08 HOLCF-ex: theory HOLCF-ex.Domain_Proofs

16:06:08 Timing Prog_Prove (2 threads, 5.999s elapsed time, 11.404s cpu time, 0.764s GC time, factor 1.90)

16:06:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove

16:06:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove/prog-prove.pdf

16:06:08 Finished Prog_Prove (0:00:11 elapsed time, 0:00:16 cpu time, factor 1.48)

16:06:08 Running HOL-SPARK-Manual ...

16:06:09 HOL-SPARK-Manual: theory HOL-SPARK-Examples.Greatest_Common_Divisor

16:06:09 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Complex_Types

16:06:10 HOLCF-ex: theory HOLCF-ex.Fix2

16:06:10 HOLCF-ex: theory HOLCF-ex.Hoare

16:06:10 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Proc1

16:06:10 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Proc2

16:06:10 HOLCF-ex: theory HOLCF-ex.Letrec

16:06:10 HOLCF-ex: theory HOLCF-ex.Loop

16:06:10 HOLCF-ex: theory HOLCF-ex.Pattern_Match

16:06:10 HOL-SPARK-Manual: theory HOL-SPARK-Manual.VC_Principles

16:06:10 HOLCF-ex: theory HOLCF-ex.Powerdomain_ex

16:06:10 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Reference

16:06:11 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Simple_Greatest_Common_Divisor

16:06:11 HOL-SPARK-Manual: theory HOL-SPARK-Manual.Example_Verification

16:06:13 Timing HOL-Isar_Examples (2 threads, 5.578s elapsed time, 10.280s cpu time, 0.668s GC time, factor 1.84)

16:06:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples

16:06:13 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/document.pdf

16:06:13 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/outline.pdf

16:06:13 Finished HOL-Isar_Examples (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.70)

16:06:13 Running HOL-ZF ...

16:06:14 Timing HOLCF-ex (2 threads, 5.563s elapsed time, 10.700s cpu time, 0.240s GC time, factor 1.92)

16:06:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-ex

16:06:14 Finished HOLCF-ex (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.62)

16:06:14 Running HOL-IMPP ...

16:06:14 HOL-ZF: theory HOL-ZF.LProd

16:06:14 HOL-ZF: theory HOL-ZF.HOLZF

16:06:15 HOL-IMPP: theory HOL-IMPP.Com

16:06:15 HOL-ZF: theory HOL-ZF.Zet

16:06:15 HOL-ZF: theory HOL-ZF.MainZF

16:06:16 HOL-ZF: theory HOL-ZF.Games

16:06:17 HOL-IMPP: theory HOL-IMPP.Natural

16:06:18 HOL-IMPP: theory HOL-IMPP.Hoare

16:06:18 HOL-IMPP: theory HOL-IMPP.Misc

16:06:19 HOL-IMPP: theory HOL-IMPP.EvenOdd

16:06:20 Timing HOL-SPARK-Manual (2 threads, 5.184s elapsed time, 8.152s cpu time, 0.212s GC time, factor 1.57)

16:06:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual

16:06:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/document.pdf

16:06:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/outline.pdf

16:06:20 Finished HOL-SPARK-Manual (0:00:11 elapsed time, 0:00:17 cpu time, factor 1.61)

16:06:20 Running HOLCF-FOCUS ...

16:06:20 Timing HOL-IMPP (2 threads, 4.660s elapsed time, 7.308s cpu time, 0.212s GC time, factor 1.57)

16:06:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMPP

16:06:20 Finished HOL-IMPP (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.35)

16:06:20 Running HOL-Hahn_Banach ...

16:06:21 HOLCF-FOCUS: theory HOLCF-FOCUS.Fstream

16:06:21 HOLCF-FOCUS: theory HOLCF-FOCUS.Fstreams

16:06:21 HOLCF-FOCUS: theory HOLCF-FOCUS.FOCUS

16:06:21 HOLCF-FOCUS: theory HOLCF-FOCUS.Buffer

16:06:21 HOLCF-FOCUS: theory HOLCF-FOCUS.Stream_adm

16:06:22 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Zorn_Lemma

16:06:22 HOL-Hahn_Banach: theory HOL-Analysis.Continuum_Not_Denumerable

16:06:22 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Bounds

16:06:22 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Vector_Space

16:06:23 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Linearform

16:06:23 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Subspace

16:06:23 HOLCF-FOCUS: theory HOLCF-FOCUS.Buffer_adm

16:06:23 Timing HOL-ZF (2 threads, 4.646s elapsed time, 8.144s cpu time, 0.224s GC time, factor 1.75)

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

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

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

16:06:23 Finished HOL-ZF (0:00:09 elapsed time, 0:00:16 cpu time, factor 1.68)

16:06:23 Running Implementation ...

16:06:23 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Function_Order

16:06:23 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Normed_Space

16:06:24 Implementation: theory Implementation.Base

16:06:24 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Function_Norm

16:06:24 Implementation: theory Implementation.Eq

16:06:24 Implementation: theory Implementation.Integration

16:06:24 Implementation: theory Implementation.Isar

16:06:24 Implementation: theory Implementation.Local_Theory

16:06:24 Implementation: theory Implementation.ML

16:06:24 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Ext_Lemmas

16:06:24 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Sup_Lemmas

16:06:25 Implementation: theory Implementation.Prelim

16:06:25 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach_Lemmas

16:06:25 Implementation: theory Implementation.Proof

16:06:25 Implementation: theory Implementation.Syntax

16:06:25 HOL-Hahn_Banach: theory HOL-Hahn_Banach.Hahn_Banach

16:06:25 Implementation: theory Implementation.Tactic

16:06:27 Timing HOLCF-FOCUS (2 threads, 4.599s elapsed time, 8.956s cpu time, 0.224s GC time, factor 1.95)

16:06:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-FOCUS

16:06:27 Finished HOLCF-FOCUS (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.60)

16:06:27 Running Functions ...

16:06:27 Implementation: theory Implementation.Logic

16:06:27 Functions: theory Functions.Functions

16:06:31 Timing HOL-Hahn_Banach (2 threads, 3.994s elapsed time, 7.676s cpu time, 0.224s GC time, factor 1.92)

16:06:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach

16:06:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/document.pdf

16:06:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/outline.pdf

16:06:31 Finished HOL-Hahn_Banach (0:00:09 elapsed time, 0:00:16 cpu time, factor 1.71)

16:06:31 Running HOL-Nonstandard_Analysis-Examples ...

16:06:32 HOL-Nonstandard_Analysis-Examples: theory HOL-Nonstandard_Analysis-Examples.NSPrimes

16:06:33 Timing Implementation (2 threads, 3.856s elapsed time, 6.636s cpu time, 0.084s GC time, factor 1.72)

16:06:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation

16:06:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation/implementation.pdf

16:06:33 Finished Implementation (0:00:09 elapsed time, 0:00:12 cpu time, factor 1.32)

16:06:33 Running HOL-IOA ...

16:06:34 HOL-IOA: theory HOL-IOA.Asig

16:06:34 Timing Functions (2 threads, 3.291s elapsed time, 4.272s cpu time, 0.348s GC time, factor 1.30)

16:06:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions

16:06:34 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions/functions.pdf

16:06:34 Finished Functions (0:00:07 elapsed time, 0:00:08 cpu time, factor 1.18)

16:06:34 Running HOL-TLA-Inc ...

16:06:34 HOL-IOA: theory HOL-IOA.IOA

16:06:35 HOL-IOA: theory HOL-IOA.Solve

16:06:35 HOL-TLA-Inc: theory HOL-TLA-Inc.Inc

16:06:37 Timing HOL-Nonstandard_Analysis-Examples (2 threads, 3.008s elapsed time, 3.812s cpu time, 0.192s GC time, factor 1.27)

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

16:06:37 Finished HOL-Nonstandard_Analysis-Examples (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.05)

16:06:37 Running HOL-Lattice ...

16:06:37 HOL-Lattice: theory HOL-Lattice.Orders

16:06:38 Timing HOL-IOA (2 threads, 2.847s elapsed time, 4.136s cpu time, 0.188s GC time, factor 1.45)

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

16:06:38 Finished HOL-IOA (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.19)

16:06:38 Running Classes ...

16:06:38 Timing HOL-TLA-Inc (2 threads, 2.337s elapsed time, 4.092s cpu time, 0.124s GC time, factor 1.75)

16:06:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Inc

16:06:38 Finished HOL-TLA-Inc (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.33)

16:06:38 Running Eisbach ...

16:06:38 HOL-Lattice: theory HOL-Lattice.Bounds

16:06:39 Classes: theory Classes.Setup

16:06:39 HOL-Lattice: theory HOL-Lattice.Lattice

16:06:39 Classes: theory Classes.Classes

16:06:39 HOL-Lattice: theory HOL-Lattice.CompleteLattice

16:06:39 Eisbach: theory Eisbach.Base

16:06:39 Eisbach: theory Eisbach.Preface

16:06:39 Eisbach: theory Eisbach.Manual

16:06:43 Timing HOL-Lattice (2 threads, 2.072s elapsed time, 3.548s cpu time, 0.000s GC time, factor 1.71)

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

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

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

16:06:43 Finished HOL-Lattice (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.68)

16:06:43 Running IOA-Storage ...

16:06:44 IOA-Storage: theory IOA-Storage.Action

16:06:45 Timing Classes (2 threads, 2.041s elapsed time, 2.432s cpu time, 0.000s GC time, factor 1.19)

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

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

16:06:45 Finished Classes (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.02)

16:06:45 Running HOL-Proofs-ex ...

16:06:45 IOA-Storage: theory IOA-Storage.Impl

16:06:45 IOA-Storage: theory IOA-Storage.Spec

16:06:45 IOA-Storage: theory IOA-Storage.Correctness

16:06:45 Timing Eisbach (2 threads, 1.672s elapsed time, 2.124s cpu time, 0.000s GC time, factor 1.27)

16:06:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach

16:06:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach/eisbach.pdf

16:06:45 Finished Eisbach (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.06)

16:06:45 Running Locales ...

16:06:46 HOL-Proofs-ex: theory HOL-Isar_Examples.Drinker

16:06:46 HOL-Proofs-ex: theory HOL-Proofs-ex.Hilbert_Classical

16:06:46 HOL-Proofs-ex: theory HOL-Proofs-ex.Proof_Terms

16:06:46 HOL-Proofs-ex: theory HOL-Proofs-ex.XML_Data

16:06:46 Locales: theory Locales.Examples

16:06:47 Locales: theory Locales.Examples1

16:06:47 Locales: theory Locales.Examples2

16:06:47 Locales: theory Locales.Examples3

16:06:47 Timing IOA-Storage (2 threads, 1.589s elapsed time, 2.332s cpu time, 0.000s GC time, factor 1.47)

16:06:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-Storage

16:06:47 Finished IOA-Storage (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.09)

16:06:47 Running Main ...

16:06:48 Main: theory Main.Main_Doc

16:06:48 Timing HOL-Proofs-ex (2 threads, 1.516s elapsed time, 2.504s cpu time, 0.000s GC time, factor 1.65)

16:06:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-ex

16:06:48 Finished HOL-Proofs-ex (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.16)

16:06:48 Running HOL-Import ...

16:06:49 HOL-Import: theory HOL-Import.Import_Setup

16:06:50 HOL-Import: theory HOL-Import.HOL_Light_Maps

16:06:51 Skipping theories "HOL_Light_Import" (undefined HOL_LIGHT_BUNDLE)

16:06:51 Timing HOL-Import (2 threads, 0.970s elapsed time, 1.712s cpu time, 0.000s GC time, factor 1.77)

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

16:06:51 Finished HOL-Import (0:00:02 elapsed time)

16:06:51 Running HOL-Types_To_Sets ...

16:06:51 Timing Locales (2 threads, 1.341s elapsed time, 2.424s cpu time, 0.000s GC time, factor 1.81)

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

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

16:06:51 Finished Locales (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.27)

16:06:51 Running Sugar ...

16:06:52 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Prerequisites

16:06:52 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Types_To_Sets

16:06:52 HOL-Types_To_Sets: theory HOL-Types_To_Sets.Finite

16:06:52 HOL-Types_To_Sets: theory HOL-Types_To_Sets.T2_Spaces

16:06:52 Timing Main (2 threads, 1.348s elapsed time, 1.432s cpu time, 0.000s GC time, factor 1.06)

16:06:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main

16:06:52 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main/main.pdf

16:06:52 Finished Main (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.07)

16:06:52 Running IOA-ex ...

16:06:52 Sugar: theory HOL-Library.LaTeXsugar

16:06:52 Sugar: theory HOL-Library.OptionalSugar

16:06:53 Sugar: theory Sugar.Sugar

16:06:53 IOA-ex: theory IOA-ex.TrivEx

16:06:53 IOA-ex: theory IOA-ex.TrivEx2

16:06:53 Timing HOL-Types_To_Sets (2 threads, 1.001s elapsed time, 1.572s cpu time, 0.000s GC time, factor 1.57)

16:06:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Types_To_Sets

16:06:53 Finished HOL-Types_To_Sets (0:00:02 elapsed time)

16:06:53 Running HOL-TLA-Buffer ...

16:06:54 HOL-TLA-Buffer: theory HOL-TLA-Buffer.Buffer

16:06:54 Timing IOA-ex (2 threads, 0.843s elapsed time, 1.788s cpu time, 0.000s GC time, factor 2.12)

16:06:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ex

16:06:54 Finished IOA-ex (0:00:02 elapsed time)

16:06:54 Running HOL-Mutabelle ...

16:06:55 HOL-TLA-Buffer: theory HOL-TLA-Buffer.DBuffer

16:06:56 HOL-Mutabelle: theory HOL-Mutabelle.MutabelleExtra

16:06:56 Timing HOL-TLA-Buffer (2 threads, 0.579s elapsed time, 1.024s cpu time, 0.000s GC time, factor 1.77)

16:06:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Buffer

16:06:56 Finished HOL-TLA-Buffer (0:00:02 elapsed time)

16:06:56 Running JEdit ...

16:06:57 Timing Sugar (2 threads, 0.962s elapsed time, 1.108s cpu time, 0.000s GC time, factor 1.15)

16:06:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar

16:06:57 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar/sugar.pdf

16:06:57 Finished Sugar (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.11)

16:06:57 Running How_to_Prove_it ...

16:06:57 JEdit: theory JEdit.Base

16:06:57 JEdit: theory JEdit.JEdit

16:06:57 How_to_Prove_it: theory How_to_Prove_it.How_to_Prove_it

16:06:58 Timing HOL-Mutabelle (2 threads, 0.614s elapsed time, 0.720s cpu time, 0.000s GC time, factor 1.17)

16:06:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mutabelle

16:06:58 Finished HOL-Mutabelle (0:00:02 elapsed time)

16:06:58 Running HOL-Prolog ...

16:06:58 HOL-Prolog: theory HOL-Prolog.HOHH

16:06:59 HOL-Prolog: theory HOL-Prolog.Func

16:06:59 HOL-Prolog: theory HOL-Prolog.Test

16:06:59 HOL-Prolog: theory HOL-Prolog.Type

16:07:00 Timing HOL-Prolog (2 threads, 0.309s elapsed time, 0.472s cpu time, 0.000s GC time, factor 1.53)

16:07:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Prolog

16:07:00 Finished HOL-Prolog (0:00:01 elapsed time)

16:07:00 Running Typeclass_Hierarchy ...

16:07:01 Typeclass_Hierarchy: theory Typeclass_Hierarchy.Typeclass_Hierarchy

16:07:01 Timing How_to_Prove_it (2 threads, 0.371s elapsed time, 0.520s cpu time, 0.000s GC time, factor 1.40)

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

16:07:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it/how_to_prove_it.pdf

16:07:01 Finished How_to_Prove_it (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.11)

16:07:05 Timing Typeclass_Hierarchy (2 threads, 0.264s elapsed time, 0.384s cpu time, 0.000s GC time, factor 1.45)

16:07:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy

16:07:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy/typeclass_hierarchy.pdf

16:07:05 Finished Typeclass_Hierarchy (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.09)

16:07:08 Timing JEdit (2 threads, 0.627s elapsed time, 0.696s cpu time, 0.000s GC time, factor 1.11)

16:07:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit

16:07:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit/jedit.pdf

16:07:08 Finished JEdit (0:00:11 elapsed time, 0:00:11 cpu time, factor 1.01)

16:07:08

16:07:08 === TIMING ===

16:07:08

16:07:08 Group main: 0:41:49 elapsed time, 1:11:01 cpu time, factor 1.70

16:07:08 Group doc: 0:04:54 elapsed time, 0:06:42 cpu time, factor 1.37

16:07:08 Group timing: 2:19:58 elapsed time, 4:01:45 cpu time, factor 1.73

16:07:08 Overall: 1:00:34 elapsed time, 5:05:44 cpu time, factor 5.05

16:07:09 Archiving artifacts

16:07:11 Started calculate disk usage of build

16:07:11 Finished Calculation of disk usage of build in 0 seconds

16:07:45 Started calculate disk usage of workspace

16:07:48 Finished Calculation of disk usage of workspace in 2 second

16:07:48 No emails were triggered.

16:07:48 Finished: SUCCESS