Console Output

12:10:14 Started by upstream project "isabelle-repo" build number 484
12:10:14 originally caused by:
12:10:14  Started by an SCM change
12:10:14 [EnvInject] - Loading node environment variables.
12:10:14 Building remotely on workermta4 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-repo-makeall
12:10:14 [isabelle-repo-makeall] $ hg showconfig paths.default
12:10:14 [isabelle-repo-makeall] $ hg pull --rev ec0fb01c6d50d3699521ded75720946272f04a2a
12:10:14 pulling from http://isabelle.in.tum.de/repos/isabelle/
12:10:14 searching for changes
12:10:14 adding changesets
12:10:14 adding manifests
12:10:14 adding file changes
12:10:14 added 2 changesets with 2 changes to 2 files
12:10:14 (run 'hg update' to get a working copy)
12:10:14 [isabelle-repo-makeall] $ hg update --clean --rev ec0fb01c6d50d3699521ded75720946272f04a2a
12:10:14 2 files updated, 0 files merged, 0 files removed, 0 files unresolved
12:10:14 [isabelle-repo-makeall] $ hg --config extensions.purge= clean --all
12:10:15 [isabelle-repo-makeall] $ hg log --rev . --template {node}
12:10:15 [isabelle-repo-makeall] $ hg log --rev . --template {rev}
12:10:15 [isabelle-repo-makeall] $ hg id --branch
12:10:15 No emails were triggered.
12:10:15 [isabelle-repo-makeall] $ /bin/sh -xe /tmp/hudson6929257456871830513.sh
12:10:15 + Admin/jenkins/run_build makeall
12:10:15 + set -e
12:10:15 + PROFILE=makeall
12:10:15 + shift
12:10:15 + bin/isabelle components -a
12:10:15 + bin/isabelle jedit -bf
12:10:15 ### Building graph browser ...
12:10:16 warning: [options] bootstrap class path not set in conjunction with -source 1.4
12:10:16 warning: [options] source value 1.4 is obsolete and will be removed in a future release
12:10:16 warning: [options] target value 1.4 is obsolete and will be removed in a future release
12:10:16 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
12:10:17 Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.
12:10:17 Note: Recompile with -Xlint:deprecation for details.
12:10:17 4 warnings
12:10:18 ### Building Isabelle/Scala ...
12:10:56 ### Building Isabelle/jEdit ...
12:11:22 + bin/isabelle ci_build_makeall
12:11:27 
12:11:27 === CONFIGURATION ===
12:11:27 
12:11:27 ML_PLATFORM="x86_64-linux"
12:11:27 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"
12:11:27 ML_SYSTEM="polyml-5.6"
12:11:27 ML_OPTIONS="-H 4000 --gcthreads 2 --maxheap 8G"
12:11:27 
12:11:27 === BUILD ===
12:11:27 
12:11:27 Build started at Sat, 1 Oct 2016 10:11:26 GMT
12:11:27 Isabelle id ec0fb01c6d50
12:11:27 
12:11:27 === LOG ===
12:11:27 
12:11:27 Session Pure/Pure
12:11:28 Session CCL/CCL
12:11:28 Session CTT/CTT
12:11:28 Session Cube/Cube
12:11:28 Session FOL/FOL
12:11:28 Session FOL/FOL-ex
12:11:28 Session FOLP/FOLP
12:11:28 Session FOLP/FOLP-ex
12:11:28 Session HOL/HOL (main)
12:11:29 Session Doc/Classes (doc)
12:11:29 Session Doc/Codegen_Basics
12:11:29 Session Doc/Codegen (doc)
12:11:29 Session Doc/Corec (doc)
12:11:29 Session Doc/Datatypes (doc)
12:11:29 Session Doc/Functions (doc)
12:11:29 Session HOL/HOL-Algebra (main timing)
12:11:29 Session HOL/HOL-Analysis (main timing)
12:11:29 Session HOL/HOL-Analysis-ex
12:11:29 Session HOL/HOL-Probability (timing)
12:11:29 Session HOL/HOL-Probability-ex (timing)
12:11:29 Session HOL/HOL-Auth (timing)
12:11:29 Session HOL/HOL-UNITY (timing)
12:11:30 Session HOL/HOL-Bali (timing)
12:11:30 Session HOL/HOL-Cardinals (timing)
12:11:30 Session HOL/HOL-Corec_Examples (timing)
12:11:30 Session HOL/HOL-Data_Structures (timing)
12:11:30 Session HOL/HOL-Datatype_Examples (timing)
12:11:30 Session HOL/HOL-Decision_Procs (timing)
12:11:30 Session HOL/HOL-Eisbach
12:11:30 Session Doc/Eisbach (doc)
12:11:31 Session HOL/HOL-Hahn_Banach
12:11:31 Session HOL/HOL-Hoare
12:11:31 Session HOL/HOL-Hoare_Parallel (timing)
12:11:31 Session HOL/HOL-IMP (timing)
12:11:31 Session HOL/HOL-IMPP
12:11:31 Session HOL/HOL-IOA
12:11:31 Session HOL/HOL-Imperative_HOL
12:11:31 Session HOL/HOL-Import
12:11:31 Session HOL/HOL-Induct
12:11:31 Session HOL/HOL-Isar_Examples
12:11:31 Session HOL/HOL-Lattice
12:11:31 Session HOL/HOL-Library (main timing)
12:11:31 Session HOL/HOL-Codegenerator_Test
12:11:31 Session HOL/HOL-Matrix_LP
12:11:31 Session HOL/HOL-Metis_Examples (timing)
12:11:31 Session HOL/HOL-MicroJava (timing)
12:11:32 Session HOL/HOL-Mirabelle
12:11:32 Session HOL/HOL-Mirabelle-ex
12:11:32 Session HOL/HOL-Mutabelle
12:11:32 Session HOL/HOL-NanoJava
12:11:32 Session HOL/HOL-Nitpick_Examples
12:11:32 Session HOL/HOL-Nominal
12:11:32 Session HOL/HOL-Nominal-Examples (timing)
12:11:32 Session HOL/HOL-Nonstandard_Analysis (timing)
12:11:32 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
12:11:32 Session HOL/HOL-Number_Theory (timing)
12:11:32 Session HOL/HOL-Old_Number_Theory
12:11:32 Session HOL/HOL-Predicate_Compile_Examples (timing)
12:11:32 Session HOL/HOL-Prolog
12:11:32 Session HOL/HOL-Quickcheck_Examples (timing)
12:11:33 Session HOL/HOL-Quotient_Examples (timing)
12:11:33 Session HOL/HOL-SET_Protocol (timing)
12:11:33 Session HOL/HOL-Statespace
12:11:33 Session HOL/HOL-TLA
12:11:33 Session HOL/HOL-TLA-Buffer
12:11:33 Session HOL/HOL-TLA-Inc
12:11:33 Session HOL/HOL-TLA-Memory
12:11:33 Session HOL/HOL-TPTP
12:11:33 Session HOL/HOL-Unix
12:11:33 Session HOL/HOL-Word (main timing)
12:11:33 Session HOL/HOL-SPARK (main)
12:11:33 Session HOL/HOL-SPARK-Examples
12:11:33 Session HOL/HOL-SPARK-Manual
12:11:33 Session HOL/HOL-Word-Examples
12:11:33 Session HOL/HOL-Word-SMT_Examples (timing)
12:11:33 Session HOL/HOL-ZF
12:11:33 Session HOL/HOL-ex
12:11:34 Session HOL/HOLCF (main timing)
12:11:34 Session HOL/HOLCF-FOCUS
12:11:34 Session HOL/HOLCF-IMP
12:11:34 Session HOL/HOLCF-Library
12:11:34 Session HOL/HOLCF-Tutorial
12:11:34 Session HOL/HOLCF-ex
12:11:34 Session HOL/IOA (timing)
12:11:34 Session HOL/IOA-ABP
12:11:34 Session HOL/IOA-NTP
12:11:34 Session HOL/IOA-Storage
12:11:34 Session HOL/IOA-ex
12:11:34 Session Doc/How_to_Prove_it
12:11:34 Session Doc/Implementation (doc)
12:11:34 Session Doc/Isar_Ref (doc)
12:11:34 Session Doc/JEdit (doc)
12:11:34 Session Doc/Locales (doc)
12:11:34 Session Doc/Main (doc)
12:11:34 Session Doc/Prog_Prove (doc)
12:11:34 Session Doc/Sugar (doc)
12:11:34 Session Doc/Tutorial (doc)
12:11:34 Session Doc/Typeclass_Hierarchy_Basics
12:11:34 Session Doc/Typeclass_Hierarchy (doc)
12:11:34 Session HOL/HOL-Proofs (timing)
12:11:35 Session HOL/HOL-Proofs-Extraction (timing)
12:11:35 Session HOL/HOL-Proofs-Lambda (timing)
12:11:35 Session HOL/HOL-Proofs-ex
12:11:35 Session Doc/Intro (doc)
12:11:35 Session LCF/LCF
12:11:35 Session Doc/Logics (doc)
12:11:35 Session Doc/Nitpick (doc)
12:11:35 Session Unsorted/SML
12:11:35 Session Sequents/Sequents
12:11:35 Session Doc/Sledgehammer (doc)
12:11:35 Session Unsorted/Spec_Check
12:11:35 Session Doc/System (doc)
12:11:35 Session ZF/ZF (main timing ZF)
12:11:35 Session Doc/Logics_ZF (doc)
12:11:35 Session ZF/ZF-AC (ZF)
12:11:35 Session ZF/ZF-Coind (ZF)
12:11:35 Session ZF/ZF-Constructible (ZF)
12:11:35 Session ZF/ZF-IMP (ZF)
12:11:35 Session ZF/ZF-Induct (ZF)
12:11:35 Session ZF/ZF-Resid (ZF)
12:11:35 Session ZF/ZF-UNITY (timing ZF)
12:11:35 Session ZF/ZF-ex (ZF)
12:11:35 Building Pure ...
12:11:46 Pure: theory Pure
12:11:47 Pure: theory ML_Bootstrap
12:11:49 Warning: missing document directory
12:11:49 Timing Pure (2 threads, 0.729s elapsed time, 0.760s cpu time, 0.000s GC time, factor 1.04)
12:11:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Pure/Pure
12:11:49 Finished Pure (0:00:13 elapsed time, 0:00:14 cpu time, factor 1.08)
12:11:49 Building HOL ...
12:11:49 Building ZF ...
12:11:49 Building HOL-Proofs ...
12:11:50 HOL-Proofs: theory Proofs
12:11:50 ZF: theory IFOL
12:11:50 HOL-Proofs: theory Code_Generator
12:11:50 HOL: theory Code_Generator
12:11:51 ZF: theory FOL
12:11:52 ZF: theory ZF
12:11:52 ZF: theory upair
12:11:53 HOL: theory HOL
12:11:53 ZF: theory pair
12:11:53 HOL-Proofs: theory HOL
12:11:53 ZF: theory Bool
12:11:53 ZF: theory equalities
12:11:54 ZF: theory Fixedpt
12:11:54 ZF: theory Sum
12:11:54 ZF: theory func
12:11:54 ZF: theory Perm
12:11:54 ZF: theory QPair
12:11:55 ZF: theory Trancl
12:11:55 ZF: theory EquivClass
12:11:55 ZF: theory WF
12:11:55 ZF: theory Order
12:11:55 ZF: theory Ordinal
12:11:55 ZF: theory OrdQuant
12:11:55 ZF: theory OrderArith
12:11:56 ZF: theory Nat_ZF
12:11:56 ZF: theory Epsilon
12:11:56 ZF: theory OrderType
12:11:56 ZF: theory Inductive_ZF
12:11:57 ZF: theory Finite
12:11:57 HOL: theory Argo
12:11:57 HOL: theory Ctr_Sugar
12:11:57 ZF: theory Cardinal
12:11:57 HOL-Proofs: theory Argo
12:11:57 HOL-Proofs: theory Ctr_Sugar
12:11:57 ZF: theory Univ
12:11:58 ZF: theory Arith
12:11:58 ZF: theory QUniv
12:11:58 ZF: theory Datatype_ZF
12:11:58 ZF: theory ArithSimp
12:11:58 HOL: theory Orderings
12:11:58 HOL-Proofs: theory Orderings
12:11:58 ZF: theory Int_ZF
12:11:58 ZF: theory CardinalArith
12:11:59 HOL: theory SAT
12:11:59 ZF: theory List_ZF
12:11:59 HOL-Proofs: theory SAT
12:11:59 ZF: theory Bin
12:11:59 HOL: theory Groups
12:12:00 ZF: theory IntDiv_ZF
12:12:00 HOL-Proofs: theory Groups
12:12:00 ZF: theory Main_ZF
12:12:00 ZF: theory AC
12:12:00 ZF: theory Main
12:12:00 ZF: theory Zorn
12:12:01 ZF: theory Cardinal_AC
12:12:01 ZF: theory InfDatatype
12:12:01 ZF: theory Main_ZFC
12:12:02 HOL: theory Lattices
12:12:04 HOL-Proofs: theory Lattices
12:12:04 HOL: theory Set
12:12:06 HOL: theory Fun
12:12:06 HOL: theory Typedef
12:12:06 HOL: theory Rings
12:12:06 HOL-Proofs: theory Set
12:12:07 HOL: theory Complete_Lattices
12:12:08 HOL-Proofs: theory Fun
12:12:08 HOL-Proofs: theory Typedef
12:12:08 HOL-Proofs: theory Rings
12:12:09 HOL-Proofs: theory Complete_Lattices
12:12:09 HOL: theory Inductive
12:12:11 HOL: theory Product_Type
12:12:12 HOL-Proofs: theory Inductive
12:12:12 HOL: theory Complete_Partial_Order
12:12:12 HOL: theory Sum_Type
12:12:13 HOL-Proofs: theory Product_Type
12:12:15 HOL-Proofs: theory Complete_Partial_Order
12:12:15 HOL: theory Nat
12:12:16 HOL-Proofs: theory Sum_Type
12:12:17 HOL: theory Fields
12:12:17 HOL: theory Meson
12:12:17 HOL: theory ATP
12:12:19 HOL-Proofs: theory Nat
12:12:20 HOL: theory Metis
12:12:21 Timing ZF (2 threads, 18.350s elapsed time, 34.040s cpu time, 2.148s GC time, factor 1.86)
12:12:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF
12:12:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/document.pdf
12:12:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/outline.pdf
12:12:21 Finished ZF (0:00:30 elapsed time, 0:00:54 cpu time, factor 1.78)
12:12:21 Building FOL ...
12:12:21 FOL: theory IFOL
12:12:21 HOL-Proofs: theory Fields
12:12:21 HOL: theory Finite_Set
12:12:22 FOL: theory FOL
12:12:23 HOL: theory Relation
12:12:24 HOL-Proofs: theory Meson
12:12:24 HOL: theory Transitive_Closure
12:12:24 HOL-Proofs: theory ATP
12:12:25 HOL: theory Wellfounded
12:12:26 HOL: theory Fun_Def_Base
12:12:26 HOL: theory Hilbert_Choice
12:12:26 HOL-Proofs: theory Finite_Set
12:12:26 HOL: theory Wfrec
12:12:26 HOL: theory Order_Relation
12:12:26 Timing FOL (2 threads, 2.853s elapsed time, 3.228s cpu time, 0.128s GC time, factor 1.13)
12:12:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL
12:12:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/document.pdf
12:12:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/outline.pdf
12:12:26 Finished FOL (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.26)
12:12:26 Building FOLP ...
12:12:26 FOLP: theory IFOLP
12:12:26 HOL: theory BNF_Wellorder_Relation
12:12:27 HOL: theory Zorn
12:12:27 HOL: theory BNF_Wellorder_Embedding
12:12:27 HOL-Proofs: theory Metis
12:12:27 FOLP: theory FOLP
12:12:27 HOL: theory BNF_Wellorder_Constructions
12:12:27 HOL-Proofs: theory Relation
12:12:28 HOL: theory BNF_Cardinal_Order_Relation
12:12:28 Timing FOLP (2 threads, 1.004s elapsed time, 1.004s cpu time, 0.000s GC time, factor 1.00)
12:12:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP
12:12:28 Finished FOLP (0:00:01 elapsed time)
12:12:28 Running CCL ...
12:12:29 HOL: theory BNF_Cardinal_Arithmetic
12:12:29 CCL: theory IFOL
12:12:29 HOL-Proofs: theory Transitive_Closure
12:12:29 HOL: theory BNF_Def
12:12:30 CCL: theory FOL
12:12:30 HOL-Proofs: theory Wellfounded
12:12:31 HOL: theory BNF_Composition
12:12:31 HOL: theory Basic_BNFs
12:12:31 HOL-Proofs: theory Fun_Def_Base
12:12:31 CCL: theory Set
12:12:31 HOL-Proofs: theory Hilbert_Choice
12:12:32 HOL-Proofs: theory Wfrec
12:12:32 CCL: theory Lfp
12:12:32 CCL: theory Gfp
12:12:32 CCL: theory CCL
12:12:32 HOL-Proofs: theory Order_Relation
12:12:32 HOL: theory BNF_Fixpoint_Base
12:12:32 HOL-Proofs: theory BNF_Wellorder_Relation
12:12:32 CCL: theory Term
12:12:32 CCL: theory Trancl
12:12:32 HOL-Proofs: theory Zorn
12:12:32 HOL-Proofs: theory BNF_Wellorder_Embedding
12:12:32 CCL: theory Type
12:12:33 HOL-Proofs: theory BNF_Wellorder_Constructions
12:12:33 CCL: theory Fix
12:12:33 CCL: theory Hered
12:12:33 CCL: theory Wfd
12:12:33 HOL-Proofs: theory BNF_Cardinal_Order_Relation
12:12:34 CCL: theory Nat
12:12:34 CCL: theory List
12:12:34 CCL: theory Flag
12:12:34 CCL: theory Stream
12:12:34 HOL-Proofs: theory BNF_Cardinal_Arithmetic
12:12:35 HOL: theory BNF_Least_Fixpoint
12:12:35 Timing CCL (2 threads, 5.633s elapsed time, 8.212s cpu time, 0.504s GC time, factor 1.46)
12:12:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CCL/CCL
12:12:35 Finished CCL (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.41)
12:12:35 Running CTT ...
12:12:35 CTT: theory CTT
12:12:35 HOL-Proofs: theory BNF_Def
12:12:36 CTT: theory Bool
12:12:36 CTT: theory Elimination
12:12:36 CTT: theory Arith
12:12:36 CTT: theory Equality
12:12:36 CTT: theory Typechecking
12:12:36 CTT: theory Synthesis
12:12:36 CTT: theory Main
12:12:37 HOL-Proofs: theory BNF_Composition
12:12:37 HOL: theory Basic_BNF_LFPs
12:12:37 HOL: theory Num
12:12:37 HOL: theory Transfer
12:12:37 HOL-Proofs: theory Basic_BNFs
12:12:38 HOL-Proofs: theory BNF_Fixpoint_Base
12:12:38 Timing CTT (2 threads, 0.930s elapsed time, 1.324s cpu time, 0.000s GC time, factor 1.42)
12:12:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT
12:12:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/document.pdf
12:12:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/outline.pdf
12:12:38 Finished CTT (0:00:02 elapsed time, 0:00:03 cpu time)
12:12:38 Running Cube ...
12:12:38 Cube: theory Cube
12:12:38 Cube: theory Example
12:12:39 Timing Cube (2 threads, 0.358s elapsed time, 0.360s cpu time, 0.000s GC time, factor 1.00)
12:12:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Cube/Cube
12:12:39 Finished Cube (0:00:00 elapsed time)
12:12:39 Running FOL-ex ...
12:12:39 FOL-ex: theory Classical
12:12:39 FOL-ex: theory If
12:12:39 FOL-ex: theory Intro
12:12:39 FOL-ex: theory Miniscope
12:12:39 FOL-ex: theory Nat
12:12:39 FOL-ex: theory Nat_Class
12:12:40 FOL-ex: theory Natural_Numbers
12:12:40 FOL-ex: theory Prolog
12:12:40 FOL-ex: theory Propositional_Cla
12:12:40 FOL-ex: theory Quantifiers_Cla
12:12:40 FOL-ex: theory Foundation
12:12:40 FOL-ex: theory Intuitionistic
12:12:40 FOL-ex: theory Propositional_Int
12:12:40 FOL-ex: theory Quantifiers_Int
12:12:40 HOL: theory Power
12:12:41 HOL-Proofs: theory BNF_Least_Fixpoint
12:12:42 FOL-ex: theory Locale_Test1
12:12:42 HOL: theory Groups_Big
12:12:43 HOL-Proofs: theory Basic_BNF_LFPs
12:12:44 HOL-Proofs: theory Num
12:12:44 HOL-Proofs: theory Transfer
12:12:44 HOL: theory Equiv_Relations
12:12:45 HOL: theory Lifting
12:12:45 FOL-ex: theory Locale_Test2
12:12:45 FOL-ex: theory Locale_Test3
12:12:45 FOL-ex: theory Locale_Test
12:12:46 HOL: theory Lifting_Set
12:12:46 HOL: theory Option
12:12:47 HOL: theory Quotient
12:12:47 HOL: theory Extraction
12:12:47 Timing FOL-ex (2 threads, 5.620s elapsed time, 8.000s cpu time, 0.176s GC time, factor 1.42)
12:12:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex
12:12:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/document.pdf
12:12:47 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/outline.pdf
12:12:47 Finished FOL-ex (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.42)
12:12:47 Running FOLP-ex ...
12:12:47 FOLP-ex: theory If
12:12:47 FOLP-ex: theory Classical
12:12:47 FOLP-ex: theory Intro
12:12:47 FOLP-ex: theory Nat
12:12:47 HOL-Proofs: theory Power
12:12:48 FOLP-ex: theory Propositional_Cla
12:12:48 HOL: theory Lattices_Big
12:12:48 FOLP-ex: theory Quantifiers_Cla
12:12:48 FOLP-ex: theory Foundation
12:12:48 FOLP-ex: theory Intuitionistic
12:12:49 HOL: theory Partial_Function
12:12:49 FOLP-ex: theory Propositional_Int
12:12:50 FOLP-ex: theory Quantifiers_Int
12:12:50 HOL: theory Fun_Def
12:12:50 HOL-Proofs: theory Groups_Big
12:12:51 HOL: theory Int
12:12:52 Timing FOLP-ex (2 threads, 3.603s elapsed time, 6.180s cpu time, 0.128s GC time, factor 1.72)
12:12:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP-ex
12:12:52 Finished FOLP-ex (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.62)
12:12:52 Running Intro ...
12:12:53 HOL-Proofs: theory Equiv_Relations
12:12:53 HOL-Proofs: theory Lifting
12:12:53 HOL: theory Nat_Transfer
12:12:54 HOL: theory Parity
12:12:54 Timing Intro (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)
12:12:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro
12:12:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro/intro.pdf
12:12:54 Finished Intro (0:00:02 elapsed time)
12:12:54 Running LCF ...
12:12:54 LCF: theory IFOL
12:12:55 HOL-Proofs: theory Lifting_Set
12:12:55 HOL-Proofs: theory Option
12:12:55 HOL-Proofs: theory Quotient
12:12:55 LCF: theory FOL
12:12:56 HOL: theory Divides
12:12:56 HOL-Proofs: theory Lattices_Big
12:12:57 HOL-Proofs: theory Partial_Function
12:12:57 LCF: theory LCF
12:12:57 LCF: theory Ex1
12:12:57 LCF: theory Ex2
12:12:57 LCF: theory Ex3
12:12:57 LCF: theory Ex4
12:12:57 HOL-Proofs: theory Fun_Def
12:12:58 Timing LCF (2 threads, 3.007s elapsed time, 3.448s cpu time, 0.152s GC time, factor 1.15)
12:12:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/LCF/LCF
12:12:58 Finished LCF (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.10)
12:12:58 Running Logics ...
12:12:59 HOL-Proofs: theory Int
12:13:00 Timing Logics (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)
12:13:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics
12:13:00 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics/logics.pdf
12:13:00 Finished Logics (0:00:02 elapsed time)
12:13:00 Running Logics_ZF ...
12:13:00 Logics_ZF: theory FOL_examples
12:13:00 Logics_ZF: theory If
12:13:00 Logics_ZF: theory ZF_Isar
12:13:00 HOL: theory Code_Numeral
12:13:00 Logics_ZF: theory ZF_examples
12:13:01 Logics_ZF: theory IFOL_examples
12:13:01 HOL: theory Numeral_Simprocs
12:13:02 HOL-Proofs: theory Nat_Transfer
12:13:02 HOL-Proofs: theory Parity
12:13:02 HOL: theory SMT
12:13:04 Timing Logics_ZF (2 threads, 0.419s elapsed time, 0.736s cpu time, 0.000s GC time, factor 1.76)
12:13:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF
12:13:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF/logics-ZF.pdf
12:13:04 Finished Logics_ZF (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.00)
12:13:04 Running Nitpick ...
12:13:04 HOL: theory Semiring_Normalization
12:13:04 HOL-Proofs: theory Divides
12:13:06 HOL: theory Groebner_Basis
12:13:06 Timing Nitpick (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)
12:13:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick
12:13:06 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick/nitpick.pdf
12:13:06 Finished Nitpick (0:00:02 elapsed time)
12:13:06 Running SML ...
12:13:06 SML: theory Examples
12:13:06 HOL: theory Set_Interval
12:13:07 Warning: missing document directory
12:13:07 Timing SML (2 threads, 0.019s elapsed time, 0.016s cpu time, 0.000s GC time, factor 0.86)
12:13:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/SML
12:13:07 Finished SML (0:00:00 elapsed time)
12:13:07 Running Sequents ...
12:13:07 Sequents: theory Sequents
12:13:07 Sequents: theory ILL
12:13:07 Sequents: theory LK0
12:13:07 Sequents: theory ILL_predlog
12:13:07 Sequents: theory Washing
12:13:07 Sequents: theory LK
12:13:07 Sequents: theory Modal0
12:13:07 Sequents: theory S4
12:13:08 Sequents: theory S43
12:13:08 Sequents: theory Hard_Quantifiers
12:13:08 Sequents: theory Nat
12:13:08 Sequents: theory Propositional
12:13:08 Sequents: theory Quantifiers
12:13:08 Sequents: theory T
12:13:09 HOL: theory Conditionally_Complete_Lattices
12:13:10 HOL: theory Filter
12:13:10 HOL-Proofs: theory Code_Numeral
12:13:11 HOL: theory Presburger
12:13:11 HOL-Proofs: theory Numeral_Simprocs
12:13:11 Timing Sequents (2 threads, 3.801s elapsed time, 7.308s cpu time, 0.144s GC time, factor 1.92)
12:13:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Sequents/Sequents
12:13:11 Finished Sequents (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.82)
12:13:11 Running Sledgehammer ...
12:13:12 HOL-Proofs: theory SMT
12:13:13 HOL: theory Sledgehammer
12:13:14 Timing Sledgehammer (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)
12:13:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer
12:13:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer/sledgehammer.pdf
12:13:14 Finished Sledgehammer (0:00:02 elapsed time)
12:13:14 Running Spec_Check ...
12:13:14 HOL-Proofs: theory Semiring_Normalization
12:13:14 Spec_Check: theory Spec_Check
12:13:14 Spec_Check: theory Examples
12:13:15 HOL: theory List
12:13:16 HOL-Proofs: theory Groebner_Basis
12:13:16 Warning: missing document directory
12:13:16 Timing Spec_Check (2 threads, 2.049s elapsed time, 3.352s cpu time, 0.012s GC time, factor 1.64)
12:13:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/Spec_Check
12:13:16 Finished Spec_Check (0:00:02 elapsed time, 0:00:03 cpu time)
12:13:16 Running System ...
12:13:17 System: theory Base
12:13:17 System: theory Environment
12:13:17 System: theory Misc
12:13:17 System: theory Presentation
12:13:17 System: theory Scala
12:13:17 System: theory Sessions
12:13:17 HOL-Proofs: theory Set_Interval
12:13:19 Timing System (2 threads, 0.355s elapsed time, 0.468s cpu time, 0.000s GC time, factor 1.32)
12:13:19 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System
12:13:19 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System/system.pdf
12:13:19 Finished System (0:00:02 elapsed time)
12:13:19 Running ZF-AC ...
12:13:20 ZF-AC: theory AC_Equiv
12:13:20 ZF-AC: theory AC18_AC19
12:13:20 ZF-AC: theory AC7_AC9
12:13:20 ZF-AC: theory Cardinal_aux
12:13:20 ZF-AC: theory Hartog
12:13:20 ZF-AC: theory WO6_WO1
12:13:20 ZF-AC: theory AC16_lemmas
12:13:20 ZF-AC: theory AC16_WO4
12:13:20 HOL-Proofs: theory Presburger
12:13:20 ZF-AC: theory DC
12:13:21 ZF-AC: theory HH
12:13:21 ZF-AC: theory AC15_WO6
12:13:21 ZF-AC: theory AC17_AC1
12:13:21 ZF-AC: theory WO1_AC
12:13:21 ZF-AC: theory WO1_WO7
12:13:21 ZF-AC: theory WO2_AC16
12:13:23 HOL-Proofs: theory Sledgehammer
12:13:23 HOL: theory Groups_List
12:13:23 HOL: theory Map
12:13:24 HOL: theory Enum
12:13:24 HOL: theory Random
12:13:25 HOL-Proofs: theory List
12:13:26 HOL: theory String
12:13:27 HOL: theory BNF_Greatest_Fixpoint
12:13:27 HOL: theory Predicate
12:13:27 Timing ZF-AC (2 threads, 4.942s elapsed time, 9.632s cpu time, 0.416s GC time, factor 1.95)
12:13:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC
12:13:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/document.pdf
12:13:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/outline.pdf
12:13:27 Finished ZF-AC (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.76)
12:13:27 Running ZF-Coind ...
12:13:27 ZF-Coind: theory Language
12:13:27 ZF-Coind: theory Map
12:13:27 ZF-Coind: theory Types
12:13:27 ZF-Coind: theory Values
12:13:27 ZF-Coind: theory Dynamic
12:13:27 ZF-Coind: theory Static
12:13:28 ZF-Coind: theory ECR
12:13:28 HOL: theory Lazy_Sequence
12:13:28 Timing ZF-Coind (2 threads, 0.743s elapsed time, 1.416s cpu time, 0.000s GC time, factor 1.91)
12:13:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Coind
12:13:28 Finished ZF-Coind (0:00:01 elapsed time)
12:13:28 Running ZF-Constructible ...
12:13:29 ZF-Constructible: theory Formula
12:13:29 ZF-Constructible: theory MetaExists
12:13:29 ZF-Constructible: theory Normal
12:13:29 ZF-Constructible: theory Reflection
12:13:29 HOL: theory Limited_Sequence
12:13:30 ZF-Constructible: theory Relative
12:13:30 HOL: theory Typerep
12:13:31 HOL: theory Code_Evaluation
12:13:31 ZF-Constructible: theory L_axioms
12:13:31 ZF-Constructible: theory Wellorderings
12:13:32 ZF-Constructible: theory WFrec
12:13:32 HOL: theory Quickcheck_Random
12:13:33 ZF-Constructible: theory WF_absolute
12:13:33 ZF-Constructible: theory Datatype_absolute
12:13:33 ZF-Constructible: theory Rank
12:13:34 ZF-Constructible: theory Separation
12:13:34 HOL: theory Quickcheck_Exhaustive
12:13:34 HOL: theory Quickcheck_Narrowing
12:13:34 ZF-Constructible: theory Internalize
12:13:35 ZF-Constructible: theory AC_in_L
12:13:36 ZF-Constructible: theory Rec_Separation
12:13:36 ZF-Constructible: theory Rank_Separation
12:13:36 ZF-Constructible: theory Satisfies_absolute
12:13:37 ZF-Constructible: theory DPow_absolute
12:13:38 HOL: theory Random_Pred
12:13:39 HOL: theory Record
12:13:39 HOL: theory Random_Sequence
12:13:40 HOL: theory Predicate_Compile
12:13:40 HOL: theory Nitpick
12:13:46 HOL: theory Main
12:13:47 HOL: theory Archimedean_Field
12:13:47 HOL: theory Binomial
12:13:48 Timing ZF-Constructible (2 threads, 14.988s elapsed time, 30.000s cpu time, 5.264s GC time, factor 2.00)
12:13:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible
12:13:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/document.pdf
12:13:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/outline.pdf
12:13:48 Finished ZF-Constructible (0:00:19 elapsed time, 0:00:37 cpu time, factor 1.93)
12:13:48 Running ZF-IMP ...
12:13:48 HOL: theory GCD
12:13:48 ZF-IMP: theory Com
12:13:49 ZF-IMP: theory Denotation
12:13:49 ZF-IMP: theory Equiv
12:13:50 Timing ZF-IMP (2 threads, 1.067s elapsed time, 1.332s cpu time, 0.000s GC time, factor 1.25)
12:13:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP
12:13:50 Finished ZF-IMP (0:00:01 elapsed time)
12:13:50 Running ZF-Induct ...
12:13:50 ZF-Induct: theory Acc
12:13:50 ZF-Induct: theory Binary_Trees
12:13:50 ZF-Induct: theory Comb
12:13:50 ZF-Induct: theory Datatypes
12:13:50 ZF-Induct: theory FoldSet
12:13:50 ZF-Induct: theory ListN
12:13:50 ZF-Induct: theory Mutil
12:13:50 ZF-Induct: theory Multiset
12:13:50 ZF-Induct: theory Ntree
12:13:51 ZF-Induct: theory Primrec
12:13:51 ZF-Induct: theory PropLog
12:13:51 ZF-Induct: theory Rmap
12:13:51 ZF-Induct: theory Term
12:13:51 ZF-Induct: theory Tree_Forest
12:13:51 ZF-Induct: theory Brouwer
12:13:52 HOL: theory Topological_Spaces
12:13:53 HOL: theory Rat
12:13:56 HOL: theory Real
12:13:59 Timing ZF-Induct (2 threads, 5.900s elapsed time, 10.836s cpu time, 0.572s GC time, factor 1.84)
12:13:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct
12:13:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/document.pdf
12:13:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/outline.pdf
12:13:59 Finished ZF-Induct (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.72)
12:13:59 Running ZF-Resid ...
12:13:59 ZF-Resid: theory Redex
12:13:59 HOL: theory Real_Vector_Spaces
12:13:59 ZF-Resid: theory Substitution
12:13:59 ZF-Resid: theory Residuals
12:14:00 ZF-Resid: theory Reduction
12:14:00 ZF-Resid: theory Confluence
12:14:01 Timing ZF-Resid (2 threads, 1.563s elapsed time, 2.852s cpu time, 0.124s GC time, factor 1.82)
12:14:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Resid
12:14:01 Finished ZF-Resid (0:00:01 elapsed time, 0:00:03 cpu time)
12:14:01 Running ZF-UNITY ...
12:14:01 ZF-UNITY: theory Acc
12:14:01 ZF-UNITY: theory FoldSet
12:14:01 ZF-UNITY: theory GenPrefix
12:14:02 ZF-UNITY: theory Multiset
12:14:02 ZF-UNITY: theory State
12:14:02 ZF-UNITY: theory UNITY
12:14:02 ZF-UNITY: theory Constrains
12:14:03 ZF-UNITY: theory MultisetSum
12:14:03 ZF-UNITY: theory Monotonicity
12:14:03 ZF-UNITY: theory FP
12:14:03 ZF-UNITY: theory WFair
12:14:03 ZF-UNITY: theory Increasing
12:14:03 ZF-UNITY: theory SubstAx
12:14:03 ZF-UNITY: theory Follows
12:14:04 ZF-UNITY: theory Mutex
12:14:04 ZF-UNITY: theory Union
12:14:04 ZF-UNITY: theory Comp
12:14:05 ZF-UNITY: theory Guar
12:14:05 ZF-UNITY: theory AllocBase
12:14:06 ZF-UNITY: theory ClientImpl
12:14:06 ZF-UNITY: theory Distributor
12:14:06 ZF-UNITY: theory Merge
12:14:06 ZF-UNITY: theory AllocImpl
12:14:10 HOL: theory Inequalities
12:14:10 HOL: theory Limits
12:14:14 HOL: theory Deriv
12:14:14 HOL: theory Series
12:14:15 HOL: theory NthRoot
12:14:16 HOL: theory Transcendental
12:14:19 Timing ZF-UNITY (2 threads, 16.550s elapsed time, 32.452s cpu time, 1.244s GC time, factor 1.96)
12:14:19 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-UNITY
12:14:19 Finished ZF-UNITY (0:00:17 elapsed time, 0:00:32 cpu time, factor 1.92)
12:14:19 Running ZF-ex ...
12:14:19 ZF-ex: theory BinEx
12:14:19 ZF-ex: theory CoUnit
12:14:19 ZF-ex: theory Commutation
12:14:19 ZF-ex: theory Group
12:14:19 ZF-ex: theory LList
12:14:19 ZF-ex: theory Limit
12:14:20 ZF-ex: theory Ring
12:14:20 HOL: theory Complex
12:14:20 ZF-ex: theory NatSum
12:14:20 ZF-ex: theory Primes
12:14:20 HOL: theory MacLaurin
12:14:21 ZF-ex: theory Ramsey
12:14:21 ZF-ex: theory misc
12:14:22 HOL: theory Complex_Main
12:14:27 Timing ZF-ex (2 threads, 7.745s elapsed time, 15.440s cpu time, 0.664s GC time, factor 1.99)
12:14:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-ex
12:14:27 Finished ZF-ex (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.93)
12:18:02 Timing HOL (2 threads, 273.455s elapsed time, 535.760s cpu time, 46.620s GC time, factor 1.96)
12:18:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL
12:18:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/document.pdf
12:18:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/outline.pdf
12:18:02 Finished HOL (0:06:12 elapsed time, 0:11:35 cpu time, factor 1.87)
12:18:04 Building HOLCF ...
12:18:04 Building HOL-TLA ...
12:18:05 HOL-TLA: theory Intensional
12:18:05 HOLCF: theory Nat_Bijection
12:18:05 HOLCF: theory Old_Datatype
12:18:06 HOL-TLA: theory Stfun
12:18:06 HOL-TLA: theory Action
12:18:06 HOL-TLA: theory Init
12:18:06 HOL-TLA: theory TLA
12:18:07 HOLCF: theory Countable
12:18:09 HOLCF: theory Porder
12:18:10 HOLCF: theory Pcpo
12:18:12 HOLCF: theory Cont
12:18:12 HOLCF: theory Adm
12:18:12 HOLCF: theory Discrete
12:18:12 HOLCF: theory Cpodef
12:18:12 HOLCF: theory Fun_Cpo
12:18:13 HOLCF: theory Product_Cpo
12:18:13 HOLCF: theory Cfun
12:18:14 HOLCF: theory Cprod
12:18:14 HOLCF: theory Fix
12:18:14 HOLCF: theory Sfun
12:18:14 HOLCF: theory Sprod
12:18:14 HOLCF: theory Up
12:18:15 HOLCF: theory Lift
12:18:16 HOLCF: theory One
12:18:16 HOLCF: theory Tr
12:18:16 HOLCF: theory Ssum
12:18:16 HOLCF: theory Plain_HOLCF
12:18:17 HOLCF: theory Completion
12:18:17 HOLCF: theory Deflation
12:18:17 HOLCF: theory Map_Functions
12:18:17 HOLCF: theory Fixrec
12:18:18 HOLCF: theory Bifinite
12:18:18 HOLCF: theory Domain_Aux
12:18:19 HOLCF: theory Universal
12:18:20 HOLCF: theory Algebraic
12:18:20 HOLCF: theory Compact_Basis
12:18:20 HOLCF: theory LowerPD
12:18:20 HOLCF: theory UpperPD
12:18:21 HOLCF: theory Representable
12:18:21 HOLCF: theory ConvexPD
12:18:21 Timing HOL-TLA (2 threads, 2.268s elapsed time, 4.032s cpu time, 0.140s GC time, factor 1.78)
12:18:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA
12:18:21 Finished HOL-TLA (0:00:16 elapsed time, 0:00:24 cpu time, factor 1.48)
12:18:21 Building HOL-Word ...
12:18:23 HOL-Word: theory Bit
12:18:23 HOL-Word: theory Bits
12:18:23 HOL-Word: theory Boolean_Algebra
12:18:23 HOL-Word: theory Bits_Bit
12:18:23 HOL-Word: theory Misc_Numeric
12:18:24 HOL-Word: theory Bit_Representation
12:18:24 HOLCF: theory Domain
12:18:24 HOL-Word: theory Misc_Typedef
12:18:24 HOL-Word: theory Phantom_Type
12:18:24 HOL-Word: theory Bits_Int
12:18:25 HOL-Word: theory Cardinality
12:18:25 HOLCF: theory Powerdomains
12:18:26 HOL-Word: theory Bool_List_Representation
12:18:26 HOL-Word: theory Numeral_Type
12:18:26 HOLCF: theory HOLCF
12:18:28 HOL-Word: theory Type_Length
12:18:28 HOL-Word: theory Word_Miscellaneous
12:18:28 HOL-Word: theory Word
12:18:57 Timing HOLCF (2 threads, 25.616s elapsed time, 50.012s cpu time, 2.200s GC time, factor 1.95)
12:18:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF
12:18:57 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/document.pdf
12:18:57 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/outline.pdf
12:18:57 Finished HOLCF (0:00:52 elapsed time, 0:01:30 cpu time, factor 1.73)
12:18:57 Building IOA ...
12:18:59 IOA: theory Asig
12:18:59 IOA: theory Seq
12:18:59 IOA: theory Automata
12:19:00 IOA: theory Sequence
12:19:00 IOA: theory Pred
12:19:01 IOA: theory Traces
12:19:01 IOA: theory TL
12:19:02 IOA: theory CompoExecs
12:19:02 IOA: theory RefMappings
12:19:03 IOA: theory RefCorrectness
12:19:03 IOA: theory CompoScheds
12:19:04 IOA: theory Simulations
12:19:04 IOA: theory SimCorrectness
12:19:04 IOA: theory Deadlock
12:19:04 IOA: theory ShortExecutions
12:19:05 IOA: theory CompoTraces
12:19:06 IOA: theory Compositionality
12:19:06 IOA: theory IOA
12:19:06 IOA: theory TLS
12:19:07 IOA: theory LiveIOA
12:19:07 IOA: theory Abstraction
12:19:10 Timing HOL-Word (2 threads, 23.681s elapsed time, 47.188s cpu time, 1.724s GC time, factor 1.99)
12:19:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word
12:19:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/document.pdf
12:19:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/outline.pdf
12:19:10 Finished HOL-Word (0:00:48 elapsed time, 0:01:24 cpu time, factor 1.75)
12:19:10 Building HOL-Analysis ...
12:19:13 HOL-Analysis: theory Disjoint_Sets
12:19:13 HOL-Analysis: theory FuncSet
12:19:14 HOL-Analysis: theory Infinite_Set
12:19:14 HOL-Analysis: theory Multiset
12:19:15 HOL-Analysis: theory Nat_Bijection
12:19:15 HOL-Analysis: theory Old_Datatype
12:19:17 HOL-Analysis: theory Countable
12:19:19 HOL-Analysis: theory Countable_Set
12:19:19 HOL-Analysis: theory Countable_Complete_Lattices
12:19:20 HOL-Analysis: theory Permutations
12:19:21 HOL-Analysis: theory Phantom_Type
12:19:22 HOL-Analysis: theory Cardinality
12:19:23 HOL-Analysis: theory Product_Plus
12:19:23 HOL-Analysis: theory Product_Order
12:19:23 HOL-Analysis: theory Set_Algebras
12:19:24 HOL-Analysis: theory Numeral_Type
12:19:24 HOL-Analysis: theory L2_Norm
12:19:24 HOL-Analysis: theory Continuum_Not_Denumerable
12:19:24 HOL-Analysis: theory Indicator_Function
12:19:24 HOL-Analysis: theory Inner_Product
12:19:25 HOL-Analysis: theory Liminf_Limsup
12:19:26 HOL-Analysis: theory Product_Vector
12:19:26 HOL-Analysis: theory Nonpos_Ints
12:19:26 HOL-Analysis: theory Operator_Norm
12:19:27 HOL-Analysis: theory Euclidean_Space
12:19:27 HOL-Analysis: theory Order_Continuity
12:19:27 HOL-Analysis: theory Extended_Nat
12:19:29 HOL-Analysis: theory Finite_Cartesian_Product
12:19:29 HOL-Analysis: theory Linear_Algebra
12:19:30 HOL-Analysis: theory Extended_Real
12:19:32 HOL-Analysis: theory Periodic_Fun
12:19:33 HOL-Analysis: theory Poly_Roots
12:19:33 HOL-Analysis: theory Sum_of_Squares
12:19:35 HOL-Analysis: theory Extended_Nonnegative_Real
12:19:36 HOL-Analysis: theory Norm_Arith
12:19:36 HOL-Analysis: theory Topology_Euclidean_Space
12:19:37 Timing IOA (2 threads, 18.812s elapsed time, 36.904s cpu time, 1.360s GC time, factor 1.96)
12:19:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA
12:19:37 Finished IOA (0:00:39 elapsed time, 0:01:08 cpu time, factor 1.71)
12:19:37 Building HOL-SPARK ...
12:19:37 HOL-Analysis: theory Sigma_Algebra
12:19:39 HOL-SPARK: theory Bit_Comparison
12:19:39 HOL-SPARK: theory SPARK_Setup
12:19:40 HOL-Analysis: theory Measurable
12:19:41 HOL-Analysis: theory Measure_Space
12:19:42 HOL-SPARK: theory SPARK
12:19:45 HOL-Analysis: theory Caratheodory
12:19:45 HOL-Analysis: theory Summation_Tests
12:19:47 HOL-Analysis: theory Bounded_Linear_Function
12:19:47 HOL-Analysis: theory Convex_Euclidean_Space
12:19:48 HOL-Analysis: theory Extended_Real_Limits
12:19:49 HOL-Analysis: theory Tagged_Division
12:19:51 HOL-Analysis: theory Uniform_Limit
12:19:53 HOL-Analysis: theory Continuous_Extension
12:19:54 HOL-Analysis: theory Path_Connected
12:19:56 Timing HOL-SPARK (2 threads, 3.465s elapsed time, 7.332s cpu time, 0.060s GC time, factor 2.12)
12:19:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK
12:19:56 Finished HOL-SPARK (0:00:18 elapsed time, 0:00:29 cpu time, factor 1.56)
12:19:56 Building Codegen_Basics ...
12:19:58 Codegen_Basics: theory Dlist
12:19:58 Codegen_Basics: theory IArray
12:19:58 HOL-Analysis: theory Homeomorphism
12:19:58 HOL-Analysis: theory Brouwer_Fixpoint
12:19:59 Codegen_Basics: theory Mapping
12:19:59 Codegen_Basics: theory RBT_Impl
12:20:00 HOL-Analysis: theory Derivative
12:20:03 HOL-Analysis: theory Cartesian_Euclidean_Space
12:20:03 HOL-Analysis: theory Weierstrass_Theorems
12:20:05 HOL-Analysis: theory Determinants
12:20:06 HOL-Analysis: theory Fashoda_Theorem
12:20:06 HOL-Analysis: theory Ordered_Euclidean_Space
12:20:07 HOL-Analysis: theory Polytope
12:20:11 HOL-Analysis: theory Borel_Space
12:20:14 HOL-Analysis: theory Nonnegative_Lebesgue_Integration
12:20:15 HOL-Analysis: theory Regularity
12:20:17 HOL-Analysis: theory Binary_Product_Measure
12:20:18 HOL-Analysis: theory Embed_Measure
12:20:18 HOL-Analysis: theory Finite_Product_Measure
12:20:20 HOL-Analysis: theory Bochner_Integration
12:20:22 HOL-Analysis: theory Complete_Measure
12:20:22 HOL-Analysis: theory Radon_Nikodym
12:20:23 HOL-Analysis: theory Set_Integral
12:20:23 HOL-Analysis: theory Lebesgue_Measure
12:20:25 HOL-Analysis: theory Henstock_Kurzweil_Integration
12:20:29 HOL-Analysis: theory Bounded_Continuous_Function
12:20:29 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration
12:20:29 HOL-Analysis: theory Integral_Test
12:20:30 HOL-Analysis: theory Complex_Analysis_Basics
12:20:30 HOL-Analysis: theory Interval_Integral
12:20:31 HOL-Analysis: theory Lebesgue_Integral_Substitution
12:20:32 HOL-Analysis: theory Complex_Transcendental
12:20:34 Codegen_Basics: theory RBT
12:20:34 HOL-Analysis: theory Generalised_Binomial_Theorem
12:20:34 HOL-Analysis: theory Harmonic_Numbers
12:20:34 HOL-Analysis: theory Cauchy_Integral_Theorem
12:20:35 HOL-Analysis: theory Gamma_Function
12:20:35 Codegen_Basics: theory Setup
12:20:39 HOL-Analysis: theory Conformal_Mappings
12:20:41 HOL-Analysis: theory Analysis
12:21:33 Timing Codegen_Basics (2 threads, 57.592s elapsed time, 114.412s cpu time, 3.840s GC time, factor 1.99)
12:21:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen_Basics
12:21:33 Finished Codegen_Basics (0:01:36 elapsed time, 0:02:55 cpu time, factor 1.82)
12:21:34 Building HOL-Auth ...
12:21:35 HOL-Auth: theory Message
12:21:35 HOL-Auth: theory Nat_Bijection
12:21:36 HOL-Auth: theory Simps_Case_Conv
12:21:39 HOL-Auth: theory All_Symmetric
12:21:39 HOL-Auth: theory Event
12:21:39 HOL-Auth: theory EventSC
12:21:40 HOL-Auth: theory Extensions
12:21:40 HOL-Auth: theory Analz
12:21:41 HOL-Auth: theory List_Msg
12:21:41 HOL-Auth: theory Guard
12:21:41 HOL-Auth: theory GuardK
12:21:42 HOL-Auth: theory Public
12:21:43 HOL-Auth: theory Shared
12:21:43 HOL-Auth: theory CertifiedEmail
12:21:43 HOL-Auth: theory Guard_Public
12:21:44 HOL-Auth: theory Guard_NS_Public
12:21:44 HOL-Auth: theory P2
12:21:44 HOL-Auth: theory Proto
12:21:46 HOL-Auth: theory KerberosIV
12:21:48 HOL-Auth: theory KerberosIV_Gets
12:21:48 HOL-Auth: theory KerberosV
12:21:49 HOL-Auth: theory Kerberos_BAN
12:21:50 HOL-Auth: theory Kerberos_BAN_Gets
12:21:50 HOL-Auth: theory NS_Public
12:21:51 HOL-Auth: theory NS_Public_Bad
12:21:51 HOL-Auth: theory NS_Shared
12:21:51 HOL-Auth: theory OtwayRees
12:21:51 HOL-Auth: theory OtwayReesBella
12:21:52 HOL-Auth: theory OtwayRees_AN
12:21:52 HOL-Auth: theory OtwayRees_Bad
12:21:53 HOL-Auth: theory P1
12:21:53 HOL-Auth: theory Recur
12:21:54 HOL-Auth: theory WooLam
12:21:54 HOL-Auth: theory Yahalom
12:21:56 HOL-Auth: theory Yahalom2
12:21:56 HOL-Auth: theory Yahalom_Bad
12:21:57 HOL-Auth: theory ZhouGollmann
12:21:58 HOL-Auth: theory Auth_Shared
12:21:59 HOL-Auth: theory Auth_Guard_Public
12:21:59 HOL-Auth: theory Guard_Shared
12:21:59 HOL-Auth: theory Guard_OtwayRees
12:21:59 HOL-Auth: theory Guard_Yahalom
12:22:00 HOL-Auth: theory TLS
12:22:00 HOL-Auth: theory Auth_Guard_Shared
12:22:00 HOL-Auth: theory Smartcard
12:22:01 HOL-Auth: theory ShoupRubin
12:22:02 HOL-Auth: theory Auth_Public
12:22:02 HOL-Auth: theory ShoupRubinBella
12:22:05 HOL-Auth: theory Auth_Smartcard
12:24:48 Timing HOL-Auth (2 threads, 153.573s elapsed time, 302.572s cpu time, 8.456s GC time, factor 1.97)
12:24:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth
12:24:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/document.pdf
12:24:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/outline.pdf
12:24:48 Finished HOL-Auth (0:03:13 elapsed time, 0:06:06 cpu time, factor 1.89)
12:24:48 Building HOL-Eisbach ...
12:24:49 HOL-Eisbach: theory Eisbach
12:24:49 HOL-Eisbach: theory IFOL
12:24:50 HOL-Eisbach: theory Eisbach_Old_Appl_Syntax
12:24:50 HOL-Eisbach: theory Eisbach_Tools
12:24:50 HOL-Eisbach: theory Examples
12:24:51 HOL-Eisbach: theory Tests
12:24:51 HOL-Eisbach: theory FOL
12:24:53 HOL-Eisbach: theory Examples_FOL
12:25:08 Warning: missing document directory
12:25:08 Timing HOL-Eisbach (2 threads, 4.630s elapsed time, 8.556s cpu time, 0.084s GC time, factor 1.85)
12:25:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Eisbach
12:25:08 Finished HOL-Eisbach (0:00:19 elapsed time, 0:00:29 cpu time, factor 1.53)
12:25:08 Building HOL-Library ...
12:25:10 HOL-Library: theory Adhoc_Overloading
12:25:10 HOL-Library: theory Lattice_Syntax
12:25:10 HOL-Library: theory AList
12:25:10 HOL-Library: theory BNF_Axiomatization
12:25:10 HOL-Library: theory BNF_Corec
12:25:12 HOL-Library: theory DAList
12:25:14 HOL-Library: theory Stirling
12:25:15 HOL-Library: theory Bit
12:25:15 HOL-Library: theory Bits
12:25:15 HOL-Library: theory Bits_Bit
12:25:16 HOL-Library: theory Boolean_Algebra
12:25:16 HOL-Library: theory Cardinal_Notations
12:25:16 HOL-Library: theory Char_ord
12:25:16 HOL-Library: theory Code_Abstract_Nat
12:25:16 HOL-Library: theory Code_Binary_Nat
12:25:17 HOL-Library: theory Code_Target_Nat
12:25:17 HOL-Library: theory Code_Char
12:25:17 HOL-Library: theory Code_Prolog
12:25:18 HOL-Library: theory Code_Test
12:25:18 HOL-Library: theory Combine_PER
12:25:18 HOL-Library: theory Complete_Partial_Order2
12:25:18 HOL-Library: theory Debug
12:25:19 HOL-Library: theory Discrete
12:25:19 HOL-Library: theory Disjoint_Sets
12:25:19 HOL-Library: theory Dlist
12:25:20 HOL-Library: theory FSet
12:25:22 HOL-Library: theory Fraction_Field
12:25:23 HOL-Library: theory Fun_Lexorder
12:25:23 HOL-Library: theory FuncSet
12:25:24 HOL-Library: theory Function_Algebras
12:25:24 HOL-Library: theory Finite_Map
12:25:24 HOL-Library: theory Function_Division
12:25:24 HOL-Library: theory Code_Target_Int
12:25:24 HOL-Library: theory Code_Target_Numeral
12:25:24 HOL-Library: theory Groups_Big_Fun
12:25:25 HOL-Library: theory IArray
12:25:26 HOL-Library: theory Infinite_Set
12:25:26 HOL-Library: theory LaTeXsugar
12:25:26 HOL-Library: theory Omega_Words_Fun
12:25:26 HOL-Library: theory Lattice_Constructions
12:25:27 HOL-Library: theory ListVector
12:25:27 HOL-Library: theory List_lexord
12:25:27 HOL-Library: theory Mapping
12:25:29 HOL-Library: theory AList_Mapping
12:25:29 HOL-Library: theory Misc_Numeric
12:25:29 HOL-Library: theory Bit_Representation
12:25:29 HOL-Library: theory Misc_Typedef
12:25:29 HOL-Library: theory Monad_Syntax
12:25:29 HOL-Library: theory More_List
12:25:30 HOL-Library: theory Bits_Int
12:25:30 HOL-Library: theory Multiset
12:25:31 HOL-Library: theory Nat_Bijection
12:25:32 HOL-Library: theory Stream
12:25:33 HOL-Library: theory Old_Datatype
12:25:34 HOL-Library: theory Countable
12:25:35 HOL-Library: theory DAList_Multiset
12:25:35 HOL-Library: theory Factorial_Ring
12:25:36 HOL-Library: theory Multiset_Order
12:25:36 HOL-Library: theory Permutation
12:25:37 HOL-Library: theory Permutations
12:25:38 HOL-Library: theory Countable_Set
12:25:38 HOL-Library: theory Countable_Complete_Lattices
12:25:41 HOL-Library: theory Countable_Set_Type
12:25:43 HOL-Library: theory Euclidean_Algorithm
12:25:43 HOL-Library: theory Old_Recdef
12:25:44 HOL-Library: theory Option_ord
12:25:45 HOL-Library: theory Parallel
12:25:45 HOL-Library: theory Perm
12:25:47 HOL-Library: theory Phantom_Type
12:25:48 HOL-Library: theory Cardinality
12:25:49 HOL-Library: theory FinFun
12:25:51 HOL-Library: theory Numeral_Type
12:25:53 HOL-Library: theory Normalized_Fraction
12:25:53 HOL-Library: theory Type_Length
12:25:53 HOL-Library: theory Saturated
12:25:53 HOL-Library: theory Predicate_Compile_Alternative_Defs
12:25:53 HOL-Library: theory Product_Lexorder
12:25:53 HOL-Library: theory Product_Plus
12:25:54 HOL-Library: theory Predicate_Compile_Quickcheck
12:25:54 HOL-Library: theory Product_Order
12:25:54 HOL-Library: theory Quotient_Syntax
12:25:54 HOL-Library: theory Finite_Lattice
12:25:54 HOL-Library: theory Quotient_Option
12:25:54 HOL-Library: theory Quotient_Product
12:25:54 HOL-Library: theory Quotient_Set
12:25:55 HOL-Library: theory Quotient_List
12:25:55 HOL-Library: theory Quotient_Sum
12:25:55 HOL-Library: theory Quotient_Type
12:25:55 HOL-Library: theory RBT_Impl
12:25:57 HOL-Library: theory Ramsey
12:25:58 HOL-Library: theory Reflection
12:25:58 HOL-Library: theory Refute
12:25:58 HOL-Library: theory Rewrite
12:25:59 HOL-Library: theory Set_Algebras
12:25:59 HOL-Library: theory Simps_Case_Conv
12:25:59 HOL-Library: theory Extended
12:26:01 HOL-Library: theory State_Monad
12:26:01 HOL-Library: theory Sublist
12:26:02 HOL-Library: theory Prefix_Order
12:26:02 HOL-Library: theory Sublist_Order
12:26:02 HOL-Library: theory Polynomial
12:26:08 HOL-Library: theory BigO
12:26:09 HOL-Library: theory Bool_List_Representation
12:26:10 HOL-Library: theory Code_Real_Approx_By_Float
12:26:11 HOL-Library: theory Diagonal_Subsequence
12:26:11 HOL-Library: theory Formal_Power_Series
12:26:15 HOL-Library: theory Polynomial_FPS
12:26:16 HOL-Library: theory Fundamental_Theorem_Algebra
12:26:17 HOL-Library: theory Indicator_Function
12:26:18 HOL-Library: theory Lattice_Algebras
12:26:24 HOL-Library: theory Liminf_Limsup
12:26:24 HOL-Library: theory Log_Nat
12:26:25 HOL-Library: theory Float
12:26:28 HOL-Library: theory Lub_Glb
12:26:28 HOL-Library: theory Multiset_Permutations
12:26:29 HOL-Library: theory Nonpos_Ints
12:26:30 HOL-Library: theory OptionalSugar
12:26:30 HOL-Library: theory Order_Continuity
12:26:31 HOL-Library: theory RBT
12:26:31 HOL-Library: theory Extended_Nat
12:26:32 HOL-Library: theory RBT_Mapping
12:26:32 HOL-Library: theory RBT_Set
12:26:32 HOL-Library: theory Extended_Real
12:26:33 HOL-Library: theory Linear_Temporal_Logic_on_Streams
12:26:35 HOL-Library: theory Periodic_Fun
12:26:35 HOL-Library: theory Polynomial_Factorial
12:26:37 HOL-Library: theory Extended_Nonnegative_Real
12:26:39 HOL-Library: theory Quadratic_Discriminant
12:26:39 HOL-Library: theory Sum_of_Squares
12:26:40 HOL-Library: theory Transitive_Closure_Table
12:26:40 HOL-Library: theory Tree
12:26:43 HOL-Library: theory While_Combinator
12:26:43 HOL-Library: theory Bourbaki_Witt_Fixpoint
12:26:44 HOL-Library: theory Word_Miscellaneous
12:26:44 HOL-Library: theory Tree_Multiset
12:26:44 HOL-Library: theory Word
12:26:45 HOL-Library: theory Preorder
12:26:45 HOL-Library: theory Function_Growth
12:26:46 HOL-Library: theory Library
12:26:51 HOL-Library: theory Old_SMT
12:27:48 HOL-Proofs: theory Extraction
12:27:48 HOL-Proofs: theory Conditionally_Complete_Lattices
12:27:51 HOL-Proofs: theory Filter
12:27:52 HOL-Proofs: theory Groups_List
12:27:52 HOL-Proofs: theory Map
12:27:53 HOL-Proofs: theory Random
12:27:53 HOL-Proofs: theory Enum
12:27:56 HOL-Proofs: theory String
12:27:57 HOL-Proofs: theory BNF_Greatest_Fixpoint
12:27:57 HOL-Proofs: theory Predicate
12:27:59 HOL-Proofs: theory Lazy_Sequence
12:28:01 HOL-Proofs: theory Limited_Sequence
12:28:01 HOL-Proofs: theory Typerep
12:28:03 HOL-Proofs: theory Code_Evaluation
12:28:04 HOL-Proofs: theory Quickcheck_Random
12:28:07 HOL-Proofs: theory Quickcheck_Exhaustive
12:28:07 HOL-Proofs: theory Quickcheck_Narrowing
12:28:12 HOL-Proofs: theory Random_Pred
12:28:12 HOL-Proofs: theory Record
12:28:13 HOL-Proofs: theory Random_Sequence
12:28:15 HOL-Proofs: theory Nitpick
12:28:15 HOL-Proofs: theory Predicate_Compile
12:28:22 HOL-Proofs: theory Main
12:28:24 HOL-Proofs: theory Old_Datatype
12:33:33 Timing HOL-Library (2 threads, 367.547s elapsed time, 722.540s cpu time, 55.572s GC time, factor 1.97)
12:33:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library
12:33:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/document.pdf
12:33:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/outline.pdf
12:33:33 Finished HOL-Library (0:08:24 elapsed time, 0:15:47 cpu time, factor 1.88)
12:33:35 Building HOL-Mirabelle ...
12:33:36 HOL-Mirabelle: theory Mirabelle
12:33:36 HOL-Mirabelle: theory Mirabelle_Test
12:33:49 Timing HOL-Mirabelle (2 threads, 1.126s elapsed time, 1.696s cpu time, 0.000s GC time, factor 1.51)
12:33:49 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle
12:33:49 Finished HOL-Mirabelle (0:00:14 elapsed time, 0:00:20 cpu time, factor 1.45)
12:33:50 Building HOL-Nominal ...
12:33:51 HOL-Nominal: theory Old_Datatype
12:33:51 HOL-Nominal: theory Infinite_Set
12:33:52 HOL-Nominal: theory Nominal
12:34:00 Timing HOL-Proofs (2 threads, 1262.192s elapsed time, 2305.252s cpu time, 158.660s GC time, factor 1.83)
12:34:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs
12:34:00 Finished HOL-Proofs (0:22:09 elapsed time, 0:40:13 cpu time, factor 1.81)
12:34:02 Building HOL-Nonstandard_Analysis ...
12:34:03 HOL-Nonstandard_Analysis: theory Infinite_Set
12:34:03 HOL-Nonstandard_Analysis: theory Lub_Glb
12:34:04 HOL-Nonstandard_Analysis: theory Free_Ultrafilter
12:34:04 HOL-Nonstandard_Analysis: theory StarDef
12:34:05 HOL-Nonstandard_Analysis: theory HyperNat
12:34:06 HOL-Nonstandard_Analysis: theory HyperDef
12:34:07 HOL-Nonstandard_Analysis: theory NSA
12:34:09 HOL-Nonstandard_Analysis: theory NSComplex
12:34:09 HOL-Nonstandard_Analysis: theory Star
12:34:10 HOL-Nonstandard_Analysis: theory HLim
12:34:10 HOL-Nonstandard_Analysis: theory NatStar
12:34:11 HOL-Nonstandard_Analysis: theory HDeriv
12:34:11 HOL-Nonstandard_Analysis: theory HSEQ
12:34:12 HOL-Nonstandard_Analysis: theory HSeries
12:34:12 HOL-Nonstandard_Analysis: theory HTranscendental
12:34:13 HOL-Nonstandard_Analysis: theory HLog
12:34:13 HOL-Nonstandard_Analysis: theory NSCA
12:34:14 HOL-Nonstandard_Analysis: theory Hyperreal
12:34:14 HOL-Nonstandard_Analysis: theory CStar
12:34:15 HOL-Nonstandard_Analysis: theory CLim
12:34:15 HOL-Nonstandard_Analysis: theory Hypercomplex
12:34:16 HOL-Nonstandard_Analysis: theory Nonstandard_Analysis
12:34:19 Timing HOL-Nominal (2 threads, 12.194s elapsed time, 25.252s cpu time, 0.988s GC time, factor 2.07)
12:34:19 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal
12:34:19 Finished HOL-Nominal (0:00:29 elapsed time, 0:00:50 cpu time, factor 1.71)
12:34:19 Building Typeclass_Hierarchy_Basics ...
12:34:20 Typeclass_Hierarchy_Basics: theory Lattice_Syntax
12:34:20 Typeclass_Hierarchy_Basics: theory Multiset
12:34:26 Typeclass_Hierarchy_Basics: theory Setup
12:34:42 Timing HOL-Nonstandard_Analysis (2 threads, 18.447s elapsed time, 36.960s cpu time, 1.304s GC time, factor 2.00)
12:34:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis
12:34:42 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/document.pdf
12:34:42 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/outline.pdf
12:34:42 Finished HOL-Nonstandard_Analysis (0:00:39 elapsed time, 0:01:08 cpu time, factor 1.74)
12:34:42 Running HOL-Mirabelle-ex ...
12:34:43 HOL-Mirabelle-ex: theory Ex
12:34:50 Timing Typeclass_Hierarchy_Basics (2 threads, 13.413s elapsed time, 26.964s cpu time, 0.784s GC time, factor 2.01)
12:34:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy_Basics
12:34:50 Finished Typeclass_Hierarchy_Basics (0:00:30 elapsed time, 0:00:52 cpu time, factor 1.73)
12:34:50 Running Classes ...
12:34:50 Timing HOL-Mirabelle-ex (2 threads, 6.869s elapsed time, 0.036s cpu time, 0.000s GC time, factor 0.01)
12:34:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle-ex
12:34:50 Finished HOL-Mirabelle-ex (0:00:08 elapsed time, 0:00:09 cpu time, factor 1.18)
12:34:50 Running Codegen ...
12:34:51 Classes: theory Setup
12:34:52 Codegen: theory Adaptation
12:34:52 Codegen: theory Evaluation
12:34:52 Classes: theory Classes
12:34:52 Codegen: theory Further
12:34:53 Codegen: theory Inductive_Predicate
12:34:54 Codegen: theory Introduction
12:34:55 Codegen: theory Refinement
12:34:55 Codegen: theory Foundations
12:34:57 Timing Classes (2 threads, 3.553s elapsed time, 4.704s cpu time, 0.048s GC time, factor 1.32)
12:34:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes
12:34:57 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes/classes.pdf
12:34:57 Finished Classes (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.13)
12:34:57 Running Corec ...
12:34:58 Corec: theory Setup
12:34:59 Corec: theory FSet
12:34:59 Corec: theory BNF_Corec
12:35:02 Timing Codegen (2 threads, 6.976s elapsed time, 14.784s cpu time, 0.568s GC time, factor 2.12)
12:35:02 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen
12:35:02 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen/codegen.pdf
12:35:02 Finished Codegen (0:00:11 elapsed time, 0:00:19 cpu time, factor 1.63)
12:35:02 Running Datatypes ...
12:35:04 Datatypes: theory Setup
12:35:05 Datatypes: theory BNF_Axiomatization
12:35:05 Datatypes: theory Cardinal_Notations
12:35:05 Datatypes: theory FSet
12:35:05 Datatypes: theory Nat_Bijection
12:35:06 Datatypes: theory Old_Datatype
12:35:06 Corec: theory Corec
12:35:08 Datatypes: theory Countable
12:35:09 Datatypes: theory Simps_Case_Conv
12:35:09 Datatypes: theory Datatypes
12:35:30 Timing HOL-Analysis (2 threads, 969.956s elapsed time, 1911.928s cpu time, 109.908s GC time, factor 1.97)
12:35:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis
12:35:30 HOL-Analysis FAILED
12:35:30 (see also /media/data/jenkins/workspace/isabelle-repo-makeall/heaps/polyml-5.6_x86_64-linux/log/HOL-Analysis)
12:35:30 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 rGamma[]weierstrass[]complex$\OT1/c
12:35:30 *** mr/m/n/10 :$ \OT1/cmr/m/it/10 rGamma[]series[]weierstrass z $[]$ rGamma
12:35:30 *** [1129] [1130]) (./Analysis.tex)) [1131] (./root.aux)
12:35:30 *** 
12:35:30 *** Package rerunfilecheck Warning: File `root.out' has changed.
12:35:30 *** (rerunfilecheck)                Rerun to get outlines right
12:35:30 *** (rerunfilecheck)                or use package `bookmark'.
12:35:30 *** 
12:35:30 *** 
12:35:30 *** LaTeX Font Warning: Some font shapes were not available, defaults substituted.
12:35:30 *** 
12:35:30 ***  )
12:35:30 *** (see the transcript file for additional information)</usr/share/texlive/texmf-d
12:35:30 *** ist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/f
12:35:30 *** onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/t
12:35:30 *** ype1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
12:35:30 *** ublic/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
12:35:30 *** amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
12:35:30 *** ts/cm/cmmi12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/
12:35:30 *** cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.p
12:35:30 *** fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></us
12:35:30 *** r/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share
12:35:30 *** /texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texliv
12:35:30 *** e/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-
12:35:30 *** dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fon
12:35:30 *** ts/type1/public/amsfonts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/typ
12:35:30 *** e1/public/amsfonts/cm/cmss10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
12:35:30 *** lic/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
12:35:30 *** sfonts/cm/cmsy5.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
12:35:30 *** cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy
12:35:30 *** 8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb>
12:35:30 *** </usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti12.pfb></usr/
12:35:30 *** share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/
12:35:30 *** texlive/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/share/t
12:35:30 *** exlive/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb>
12:35:30 *** Output written on root.pdf (1131 pages, 2405720 bytes).
12:35:30 *** Transcript written on root.log.
12:35:30 *** Document preparation failure in directory '/media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/outline'
12:35:30 *** 
12:35:30 *** Failed to build document "/media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/outline.pdf"
12:35:30 HOL-Probability CANCELLED
12:35:30 Running Eisbach ...
12:35:31 Eisbach: theory Base
12:35:32 Eisbach: theory Preface
12:35:32 Eisbach: theory Manual
12:35:36 Timing Eisbach (2 threads, 2.508s elapsed time, 4.188s cpu time, 0.040s GC time, factor 1.67)
12:35:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach
12:35:36 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach/eisbach.pdf
12:35:36 Finished Eisbach (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.22)
12:35:36 Running Functions ...
12:35:38 Functions: theory Functions
12:35:43 Timing Functions (2 threads, 2.977s elapsed time, 5.512s cpu time, 0.152s GC time, factor 1.85)
12:35:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions
12:35:43 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions/functions.pdf
12:35:43 Finished Functions (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.37)
12:35:43 Running HOL-Algebra ...
12:35:44 HOL-Algebra: theory FuncSet
12:35:44 HOL-Algebra: theory Multiset
12:35:50 HOL-Algebra: theory Factorial_Ring
12:35:50 HOL-Algebra: theory Permutation
12:35:58 HOL-Algebra: theory Euclidean_Algorithm
12:35:59 Timing Datatypes (2 threads, 52.281s elapsed time, 83.712s cpu time, 6.276s GC time, factor 1.60)
12:35:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes
12:35:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes/datatypes.pdf
12:35:59 Finished Datatypes (0:00:57 elapsed time, 0:01:28 cpu time, factor 1.55)
12:35:59 HOL-Analysis-ex CANCELLED
12:35:59 Running HOL-Bali ...
12:36:01 HOL-Bali: theory Old_Recdef
12:36:02 HOL-Bali: theory Basis
12:36:04 HOL-Bali: theory Name
12:36:04 HOL-Bali: theory Table
12:36:06 HOL-Bali: theory Type
12:36:07 HOL-Algebra: theory Primes
12:36:07 HOL-Bali: theory Value
12:36:08 HOL-Bali: theory Term
12:36:08 Timing Corec (2 threads, 67.721s elapsed time, 103.688s cpu time, 6.840s GC time, factor 1.53)
12:36:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec
12:36:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec/corec.pdf
12:36:08 Finished Corec (0:01:11 elapsed time, 0:01:47 cpu time, factor 1.50)
12:36:09 Running HOL-Cardinals ...
12:36:10 HOL-Cardinals: theory Order_Union
12:36:10 HOL-Cardinals: theory Cardinal_Notations
12:36:10 HOL-Cardinals: theory Fun_More
12:36:10 HOL-Cardinals: theory Order_Relation_More
12:36:10 HOL-Cardinals: theory Wellorder_Extension
12:36:11 HOL-Cardinals: theory Wellfounded_More
12:36:11 HOL-Cardinals: theory Wellorder_Relation
12:36:11 HOL-Cardinals: theory Wellorder_Embedding
12:36:11 HOL-Cardinals: theory Wellorder_Constructions
12:36:12 HOL-Cardinals: theory Cardinal_Order_Relation
12:36:12 HOL-Cardinals: theory Ordinal_Arithmetic
12:36:14 HOL-Cardinals: theory Cardinal_Arithmetic
12:36:14 HOL-Cardinals: theory Cardinals
12:36:14 HOL-Cardinals: theory Bounded_Set
12:36:23 HOL-Algebra: theory Congruence
12:36:23 HOL-Algebra: theory Exponent
12:36:24 HOL-Algebra: theory Lattice
12:36:26 HOL-Algebra: theory Group
12:36:28 HOL-Algebra: theory Bij
12:36:28 HOL-Algebra: theory Coset
12:36:29 HOL-Algebra: theory FiniteProduct
12:36:30 HOL-Bali: theory Decl
12:36:30 HOL-Algebra: theory Ring
12:36:31 HOL-Algebra: theory Sylow
12:36:32 HOL-Algebra: theory Divisibility
12:36:34 HOL-Algebra: theory AbelCoset
12:36:35 HOL-Bali: theory TypeRel
12:36:35 HOL-Bali: theory DeclConcepts
12:36:36 HOL-Algebra: theory Module
12:36:38 HOL-Bali: theory State
12:36:38 HOL-Bali: theory WellType
12:36:40 HOL-Bali: theory Conform
12:36:40 HOL-Bali: theory Eval
12:36:41 HOL-Algebra: theory Ideal
12:36:43 HOL-Bali: theory DefiniteAssignment
12:36:47 HOL-Algebra: theory RingHom
12:36:48 HOL-Algebra: theory QuotRing
12:36:49 HOL-Algebra: theory UnivPoly
12:36:49 HOL-Algebra: theory IntRing
12:36:50 HOL-Bali: theory WellForm
12:36:51 HOL-Bali: theory DefiniteAssignmentCorrect
12:36:51 HOL-Bali: theory Example
12:36:52 HOL-Bali: theory TypeSafe
12:36:56 HOL-Bali: theory Evaln
12:36:59 HOL-Bali: theory AxSem
12:36:59 HOL-Bali: theory Trans
12:37:03 HOL-Bali: theory AxCompl
12:37:03 HOL-Bali: theory AxSound
12:37:04 HOL-Bali: theory AxExample
12:37:45 Timing HOL-Algebra (2 threads, 115.567s elapsed time, 231.312s cpu time, 9.720s GC time, factor 2.00)
12:37:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra
12:37:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/document.pdf
12:37:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline.pdf
12:37:45 Finished HOL-Algebra (0:02:01 elapsed time, 0:03:59 cpu time, factor 1.97)
12:37:45 Running HOL-Codegenerator_Test ...
12:37:49 HOL-Codegenerator_Test: theory Less_False
12:37:49 HOL-Codegenerator_Test: theory Cmp
12:37:49 HOL-Codegenerator_Test: theory Sorted_Less
12:37:49 HOL-Codegenerator_Test: theory AList_Upd_Del
12:37:49 HOL-Codegenerator_Test: theory List_Ins_Del
12:37:50 HOL-Codegenerator_Test: theory Map_by_Ordered
12:37:50 HOL-Codegenerator_Test: theory Set_by_Ordered
12:37:50 HOL-Codegenerator_Test: theory Primes
12:37:50 HOL-Codegenerator_Test: theory Records
12:37:51 HOL-Codegenerator_Test: theory Eratosthenes
12:37:51 HOL-Codegenerator_Test: theory Tree_Set
12:37:52 HOL-Codegenerator_Test: theory Tree_Map
12:37:55 HOL-Codegenerator_Test: theory Candidates
12:37:58 HOL-Codegenerator_Test: theory Generate
12:37:58 HOL-Codegenerator_Test: theory Generate_Binary_Nat
12:39:01 Timing HOL-Bali (2 threads, 168.151s elapsed time, 330.440s cpu time, 13.220s GC time, factor 1.97)
12:39:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali
12:39:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/document.pdf
12:39:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/outline.pdf
12:39:01 Finished HOL-Bali (0:03:00 elapsed time, 0:05:47 cpu time, factor 1.92)
12:39:01 Running HOL-Corec_Examples ...
12:39:02 HOL-Corec_Examples: theory FSet
12:39:02 HOL-Corec_Examples: theory BNF_Corec
12:39:06 HOL-Corec_Examples: theory Nat_Bijection
12:39:07 HOL-Corec_Examples: theory Stream
12:39:09 HOL-Corec_Examples: theory LFilter
12:39:09 HOL-Corec_Examples: theory Simple_Nesting
12:39:13 HOL-Corec_Examples: theory Stream_Processor
12:39:27 HOL-Corec_Examples: theory Paper_Examples
12:40:32 HOL-Corec_Examples: theory GPV_Bare_Bones
12:40:32 HOL-Corec_Examples: theory Merge_A
12:40:38 HOL-Corec_Examples: theory Merge_B
12:40:42 HOL-Corec_Examples: theory Merge_C
12:40:47 HOL-Corec_Examples: theory Merge_Poly
12:40:48 HOL-Corec_Examples: theory Merge_D
12:40:57 HOL-Corec_Examples: theory Misc_Mono
12:41:42 HOL-Corec_Examples: theory Misc_Poly
12:42:41 HOL-Codegenerator_Test: theory Generate_Efficient_Datastructures
12:42:41 HOL-Codegenerator_Test: theory Generate_Pretty_Char
12:43:15 HOL-Corec_Examples: theory Small_Concrete
12:43:48 HOL-Corec_Examples: theory Stream_Friends
12:43:57 HOL-Corec_Examples: theory TLList_Friends
12:44:01 Timing HOL-Cardinals (2 threads, 470.174s elapsed time, 468.612s cpu time, 8.172s GC time, factor 1.00)
12:44:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals
12:44:01 Finished HOL-Cardinals (0:07:51 elapsed time, 0:07:50 cpu time, factor 1.00)
12:44:01 Running HOL-Data_Structures ...
12:44:02 HOL-Data_Structures: theory Less_False
12:44:02 HOL-Data_Structures: theory Multiset
12:44:02 HOL-Data_Structures: theory Lattice_Algebras
12:44:08 HOL-Data_Structures: theory Log_Nat
12:44:09 HOL-Data_Structures: theory Float
12:44:17 HOL-Corec_Examples: theory Type_Class
12:44:33 HOL-Data_Structures: theory Cmp
12:44:33 HOL-Data_Structures: theory Fib
12:44:33 HOL-Data_Structures: theory Sorted_Less
12:44:34 HOL-Data_Structures: theory Tree
12:44:34 HOL-Data_Structures: theory AList_Upd_Del
12:44:34 HOL-Data_Structures: theory Map_by_Ordered
12:44:35 HOL-Data_Structures: theory List_Ins_Del
12:44:35 HOL-Data_Structures: theory Set_by_Ordered
12:44:35 HOL-Data_Structures: theory Brother12_Set
12:44:37 HOL-Data_Structures: theory Balance
12:44:38 HOL-Data_Structures: theory Splay_Set
12:44:40 HOL-Data_Structures: theory Splay_Map
12:44:42 HOL-Data_Structures: theory Tree_Set
12:44:43 HOL-Data_Structures: theory Tree_Map
12:44:44 HOL-Data_Structures: theory Tree2
12:44:45 HOL-Data_Structures: theory Isin2
12:44:45 HOL-Data_Structures: theory AA_Set
12:44:47 HOL-Data_Structures: theory AVL_Set
12:44:48 HOL-Data_Structures: theory Leftist_Heap
12:44:50 HOL-Data_Structures: theory Lookup2
12:44:51 HOL-Data_Structures: theory AA_Map
12:44:51 Timing HOL-Corec_Examples (2 threads, 347.583s elapsed time, 571.184s cpu time, 58.348s GC time, factor 1.64)
12:44:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Corec_Examples
12:44:51 Finished HOL-Corec_Examples (0:05:49 elapsed time, 0:09:33 cpu time, factor 1.64)
12:44:51 Running HOL-Datatype_Examples ...
12:44:51 HOL-Data_Structures: theory AVL_Map
12:44:54 HOL-Data_Structures: theory RBT
12:44:54 HOL-Datatype_Examples: theory BNF_Axiomatization
12:44:54 HOL-Datatype_Examples: theory FSet
12:44:54 HOL-Datatype_Examples: theory Infinite_Set
12:44:56 HOL-Datatype_Examples: theory Lift_BNF
12:45:01 HOL-Datatype_Examples: theory Milner_Tofte
12:45:01 HOL-Datatype_Examples: theory Lambda_Term
12:45:04 HOL-Datatype_Examples: theory Misc_Codatatype
12:45:06 HOL-Datatype_Examples: theory Prelim
12:45:06 HOL-Datatype_Examples: theory DTree
12:45:07 HOL-Data_Structures: theory RBT_Set
12:45:07 HOL-Datatype_Examples: theory Parallel
12:45:08 HOL-Datatype_Examples: theory TreeFsetI
12:45:09 HOL-Datatype_Examples: theory Gram_Lang
12:45:11 HOL-Datatype_Examples: theory Nat_Bijection
12:45:12 HOL-Datatype_Examples: theory Stream
12:45:12 HOL-Data_Structures: theory RBT_Map
12:45:14 HOL-Datatype_Examples: theory Process
12:45:17 HOL-Data_Structures: theory Tree23
12:45:20 HOL-Data_Structures: theory Tree23_Set
12:45:24 HOL-Datatype_Examples: theory Stream_Processor
12:45:33 HOL-Data_Structures: theory Tree23_Map
12:45:34 HOL-Datatype_Examples: theory Old_Datatype
12:45:36 HOL-Datatype_Examples: theory Compat
12:45:39 HOL-Data_Structures: theory Tree234
12:45:43 HOL-Data_Structures: theory Tree234_Set
12:45:54 HOL-Codegenerator_Test: theory Generate_Target_Nat
12:46:18 HOL-Data_Structures: theory Tree234_Map
12:46:20 HOL-Datatype_Examples: theory Countable
12:46:21 HOL-Datatype_Examples: theory Misc_Datatype
12:46:38 HOL-Datatype_Examples: theory Misc_Primcorec
12:46:39 HOL-Data_Structures: theory Brother12_Map
12:46:41 HOL-Datatype_Examples: theory TreeFI
12:46:41 HOL-Datatype_Examples: theory Koenig
12:48:04 HOL-Datatype_Examples: theory Misc_Primrec
12:49:00 Timing HOL-Datatype_Examples (2 threads, 244.516s elapsed time, 370.228s cpu time, 44.364s GC time, factor 1.51)
12:49:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Datatype_Examples
12:49:00 Finished HOL-Datatype_Examples (0:04:08 elapsed time, 0:06:29 cpu time, factor 1.57)
12:49:00 Running HOL-Decision_Procs ...
12:49:01 HOL-Decision_Procs: theory Code_Abstract_Nat
12:49:01 HOL-Decision_Procs: theory Commutative_Ring
12:49:02 HOL-Decision_Procs: theory Code_Target_Nat
12:49:02 HOL-Decision_Procs: theory DP_Library
12:49:03 HOL-Decision_Procs: theory Dense_Linear_Order
12:49:08 HOL-Decision_Procs: theory Dense_Linear_Order_Ex
12:49:09 HOL-Decision_Procs: theory Code_Target_Int
12:49:09 HOL-Decision_Procs: theory Code_Target_Numeral
12:49:10 HOL-Decision_Procs: theory Old_Recdef
12:49:11 HOL-Decision_Procs: theory Cooper
12:49:11 HOL-Decision_Procs: theory Commutative_Ring_Complete
12:49:12 HOL-Decision_Procs: theory Commutative_Ring_Ex
12:49:12 HOL-Decision_Procs: theory Ferrack
12:49:36 HOL-Decision_Procs: theory Lattice_Algebras
12:49:42 HOL-Decision_Procs: theory Log_Nat
12:49:42 HOL-Decision_Procs: theory Float
12:49:44 HOL-Decision_Procs: theory MIR
12:49:45 HOL-Decision_Procs: theory Approximation
12:50:37 HOL-Codegenerator_Test: theory Code_Test_GHC
12:50:39 HOL-Codegenerator_Test: theory Code_Test_MLton
12:50:41 HOL-Decision_Procs: theory Polynomial_List
12:50:44 HOL-Codegenerator_Test: theory Code_Test_OCaml
12:50:45 HOL-Codegenerator_Test: theory Code_Test_PolyML
12:50:46 HOL-Codegenerator_Test: theory Code_Test_Scala
12:50:53 HOL-Decision_Procs: theory Approximation_Ex
12:50:54 HOL-Decision_Procs: theory Approximation_Quickcheck_Ex
12:50:54 HOL-Decision_Procs: theory Rat_Pair
12:51:00 HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial
12:51:14 HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff
12:51:17 HOL-Codegenerator_Test: theory Code_Test_SMLNJ
12:51:18 Timing HOL-Codegenerator_Test (2 threads, 809.079s elapsed time, 651.660s cpu time, 18.616s GC time, factor 0.81)
12:51:18 Finished HOL-Codegenerator_Test (0:13:33 elapsed time, 0:36:09 cpu time, factor 2.67)
12:51:18 Running HOL-Hahn_Banach ...
12:51:20 HOL-Hahn_Banach: theory Infinite_Set
12:51:20 HOL-Hahn_Banach: theory Nat_Bijection
12:51:21 HOL-Hahn_Banach: theory Old_Datatype
12:51:21 HOL-Hahn_Banach: theory Set_Algebras
12:51:22 HOL-Hahn_Banach: theory Zorn_Lemma
12:51:22 HOL-Hahn_Banach: theory Countable
12:51:24 HOL-Hahn_Banach: theory Countable_Set
12:51:25 HOL-Hahn_Banach: theory Continuum_Not_Denumerable
12:51:25 HOL-Hahn_Banach: theory Bounds
12:51:25 HOL-Hahn_Banach: theory Vector_Space
12:51:26 HOL-Hahn_Banach: theory Linearform
12:51:26 HOL-Hahn_Banach: theory Subspace
12:51:27 HOL-Hahn_Banach: theory Function_Order
12:51:27 HOL-Hahn_Banach: theory Normed_Space
12:51:27 HOL-Hahn_Banach: theory Function_Norm
12:51:27 HOL-Hahn_Banach: theory Hahn_Banach_Ext_Lemmas
12:51:28 HOL-Hahn_Banach: theory Hahn_Banach_Sup_Lemmas
12:51:28 HOL-Hahn_Banach: theory Hahn_Banach_Lemmas
12:51:28 HOL-Hahn_Banach: theory Hahn_Banach
12:51:45 Timing HOL-Hahn_Banach (2 threads, 23.192s elapsed time, 45.920s cpu time, 1.020s GC time, factor 1.98)
12:51:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach
12:51:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/document.pdf
12:51:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/outline.pdf
12:51:45 Finished HOL-Hahn_Banach (0:00:26 elapsed time, 0:00:50 cpu time, factor 1.88)
12:51:45 Running HOL-Hoare ...
12:51:47 HOL-Hoare: theory Arith2
12:51:47 HOL-Hoare: theory Heap
12:51:47 HOL-Hoare: theory Hoare_Logic
12:51:48 HOL-Hoare: theory Hoare_Logic_Abort
12:51:49 HOL-Hoare: theory Examples
12:51:50 HOL-Hoare: theory HeapSyntax
12:51:50 HOL-Hoare: theory Pointer_Examples
12:51:50 HOL-Hoare: theory SchorrWaite
12:51:52 HOL-Decision_Procs: theory Decision_Procs
12:51:52 HOL-Hoare: theory Pointers0
12:51:52 HOL-Hoare: theory ExamplesAbort
12:51:52 HOL-Hoare: theory HeapSyntaxAbort
12:51:52 HOL-Hoare: theory Pointer_ExamplesAbort
12:51:52 HOL-Hoare: theory SepLogHeap
12:51:53 HOL-Hoare: theory Separation
12:51:53 HOL-Hoare: theory Hoare
12:52:15 Timing HOL-Hoare (2 threads, 26.188s elapsed time, 52.092s cpu time, 1.316s GC time, factor 1.99)
12:52:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare
12:52:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/document.pdf
12:52:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/outline.pdf
12:52:15 Finished HOL-Hoare (0:00:29 elapsed time, 0:00:56 cpu time, factor 1.90)
12:52:15 Running HOL-Hoare_Parallel ...
12:52:17 HOL-Hoare_Parallel: theory Graph
12:52:17 HOL-Hoare_Parallel: theory OG_Com
12:52:18 HOL-Hoare_Parallel: theory Quote_Antiquote
12:52:18 HOL-Hoare_Parallel: theory RG_Com
12:52:20 HOL-Hoare_Parallel: theory RG_Tran
12:52:21 HOL-Hoare_Parallel: theory OG_Tran
12:52:22 HOL-Hoare_Parallel: theory RG_Hoare
12:52:23 HOL-Hoare_Parallel: theory OG_Hoare
12:52:23 HOL-Hoare_Parallel: theory RG_Syntax
12:52:24 HOL-Hoare_Parallel: theory OG_Tactics
12:52:24 HOL-Hoare_Parallel: theory RG_Examples
12:52:24 HOL-Hoare_Parallel: theory OG_Syntax
12:52:24 HOL-Hoare_Parallel: theory Gar_Coll
12:52:26 HOL-Hoare_Parallel: theory Mul_Gar_Coll
12:52:26 HOL-Hoare_Parallel: theory OG_Examples
12:52:30 HOL-Hoare_Parallel: theory Hoare_Parallel
12:54:45 Timing HOL-Data_Structures (2 threads, 639.612s elapsed time, 1093.344s cpu time, 39.964s GC time, factor 1.71)
12:54:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures
12:54:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures/document.pdf
12:54:45 Finished HOL-Data_Structures (0:10:44 elapsed time, 0:18:17 cpu time, factor 1.70)
12:54:46 Running HOL-IMP ...
12:54:47 HOL-IMP: theory Char_ord
12:54:47 HOL-IMP: theory List_lexord
12:54:47 HOL-IMP: theory Quotient_Syntax
12:54:47 HOL-IMP: theory Simps_Case_Conv
12:54:47 HOL-IMP: theory Quotient_Option
12:54:47 HOL-IMP: theory Quotient_Product
12:54:48 HOL-IMP: theory Quotient_Set
12:54:48 HOL-IMP: theory Extended
12:54:48 HOL-IMP: theory Quotient_List
12:54:48 HOL-IMP: theory While_Combinator
12:54:54 HOL-IMP: theory AExp
12:54:54 HOL-IMP: theory C_like
12:54:55 HOL-IMP: theory ASM
12:54:56 HOL-IMP: theory BExp
12:54:58 HOL-IMP: theory Com
12:54:58 HOL-IMP: theory Procs
12:54:59 HOL-IMP: theory ACom
12:55:00 HOL-IMP: theory ACom_ITP
12:55:02 HOL-IMP: theory Abs_Int_Tests
12:55:03 HOL-IMP: theory Big_Step
12:55:03 HOL-IMP: theory Vars
12:55:03 HOL-IMP: theory Denotational
12:55:04 HOL-IMP: theory Hoare
12:55:04 HOL-IMP: theory Sec_Type_Expr
12:55:04 HOL-IMP: theory Hoare_Examples
12:55:04 HOL-IMP: theory Hoare_Sound_Complete
12:55:04 HOL-IMP: theory Hoare_Total
12:55:04 HOL-IMP: theory Hoare_Total_EX
12:55:04 HOL-IMP: theory VCG
12:55:05 HOL-IMP: theory VCG_Total_EX
12:55:06 HOL-IMP: theory Sec_Typing
12:55:06 HOL-IMP: theory Sec_TypingT
12:55:06 HOL-IMP: theory Sem_Equiv
12:55:07 HOL-IMP: theory Def_Init
12:55:07 HOL-IMP: theory Def_Init_Exp
12:55:07 HOL-IMP: theory Fold
12:55:07 HOL-IMP: theory Def_Init_Big
12:55:07 HOL-IMP: theory Live
12:55:07 HOL-IMP: theory Procs_Dyn_Vars_Dyn
12:55:08 HOL-IMP: theory Procs_Stat_Vars_Dyn
12:55:08 HOL-IMP: theory Procs_Stat_Vars_Stat
12:55:09 HOL-IMP: theory Complete_Lattice
12:55:09 HOL-IMP: theory Collecting
12:55:10 HOL-IMP: theory Collecting1
12:55:11 HOL-IMP: theory Collecting_Examples
12:55:11 HOL-IMP: theory Complete_Lattice_ix
12:55:11 HOL-IMP: theory Collecting_ITP
12:55:14 HOL-IMP: theory OO
12:55:16 HOL-IMP: theory Star
12:55:16 HOL-IMP: theory Compiler
12:55:21 HOL-IMP: theory Compiler2
12:55:22 HOL-IMP: theory Def_Init_Small
12:55:22 HOL-IMP: theory Small_Step
12:55:23 HOL-IMP: theory Finite_Reachable
12:55:23 HOL-IMP: theory Types
12:55:25 HOL-IMP: theory Abs_Int0_ITP
12:55:27 Timing HOL-Hoare_Parallel (2 threads, 185.336s elapsed time, 359.280s cpu time, 4.512s GC time, factor 1.94)
12:55:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel
12:55:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/document.pdf
12:55:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/outline.pdf
12:55:27 Finished HOL-Hoare_Parallel (0:03:10 elapsed time, 0:06:06 cpu time, factor 1.92)
12:55:27 Running HOL-IMPP ...
12:55:28 HOL-IMP: theory Poly_Types
12:55:28 HOL-IMPP: theory Com
12:55:29 HOL-IMP: theory Abs_Int_init
12:55:30 HOL-IMP: theory Abs_Int0
12:55:30 HOL-IMPP: theory Natural
12:55:31 HOL-IMP: theory Abs_State_ITP
12:55:31 HOL-IMPP: theory Hoare
12:55:32 HOL-IMP: theory Abs_State
12:55:32 HOL-IMPP: theory Misc
12:55:32 HOL-IMPP: theory EvenOdd
12:55:32 HOL-IMP: theory Abs_Int1_ITP
12:55:33 HOL-IMP: theory Abs_Int1
12:55:33 HOL-IMP: theory Abs_Int1_const_ITP
12:55:33 HOL-IMP: theory Abs_Int1_parity_ITP
12:55:34 Timing HOL-IMPP (2 threads, 5.090s elapsed time, 9.028s cpu time, 0.148s GC time, factor 1.77)
12:55:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMPP
12:55:34 Finished HOL-IMPP (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.57)
12:55:34 Running HOL-IOA ...
12:55:35 HOL-IMP: theory Abs_Int2_ITP
12:55:35 HOL-IMP: theory Abs_Int1_const
12:55:35 HOL-IOA: theory Asig
12:55:36 HOL-IMP: theory Abs_Int1_parity
12:55:36 HOL-IOA: theory IOA
12:55:37 HOL-IOA: theory Solve
12:55:37 HOL-IMP: theory Abs_Int2
12:55:37 HOL-IMP: theory Abs_Int2_ivl_ITP
12:55:39 HOL-IMP: theory Abs_Int2_ivl
12:55:39 Timing HOL-IOA (2 threads, 2.984s elapsed time, 5.016s cpu time, 0.072s GC time, factor 1.68)
12:55:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IOA
12:55:39 Finished HOL-IOA (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.43)
12:55:39 Running HOL-Imperative_HOL ...
12:55:39 HOL-IMP: theory Abs_Int3_ITP
12:55:40 HOL-IMP: theory Abs_Int3
12:55:41 HOL-Imperative_HOL: theory Adhoc_Overloading
12:55:41 HOL-Imperative_HOL: theory LaTeXsugar
12:55:41 HOL-Imperative_HOL: theory Monad_Syntax
12:55:41 HOL-Imperative_HOL: theory Nat_Bijection
12:55:41 HOL-Imperative_HOL: theory Old_Datatype
12:55:43 HOL-IMP: theory Live_True
12:55:43 HOL-Imperative_HOL: theory Countable
12:55:45 HOL-Imperative_HOL: theory Code_Abstract_Nat
12:55:45 HOL-Imperative_HOL: theory Code_Target_Int
12:55:45 HOL-Imperative_HOL: theory Code_Target_Nat
12:55:46 HOL-Imperative_HOL: theory Multiset
12:55:46 HOL-Imperative_HOL: theory Code_Target_Numeral
12:55:46 HOL-Imperative_HOL: theory Heap
12:55:48 HOL-Imperative_HOL: theory Heap_Monad
12:55:51 HOL-Imperative_HOL: theory Array
12:55:52 HOL-Imperative_HOL: theory Ref
12:55:52 HOL-Imperative_HOL: theory List_Sublist
12:55:52 HOL-Imperative_HOL: theory Imperative_HOL
12:55:52 HOL-Imperative_HOL: theory Subarray
12:55:52 HOL-Imperative_HOL: theory Linked_Lists
12:55:53 HOL-Imperative_HOL: theory Overview
12:55:53 HOL-Imperative_HOL: theory Imperative_Quicksort
12:56:29 HOL-Imperative_HOL: theory Imperative_Reverse
12:56:36 HOL-Imperative_HOL: theory RBT_Impl
12:57:05 HOL-Imperative_HOL: theory Sorted_List
12:57:18 HOL-Imperative_HOL: theory SatChecker
12:57:28 HOL-Imperative_HOL: theory Imperative_HOL_ex
12:57:31 Timing HOL-Decision_Procs (2 threads, 508.764s elapsed time, 908.804s cpu time, 28.164s GC time, factor 1.79)
12:57:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Decision_Procs
12:57:31 Finished HOL-Decision_Procs (0:08:30 elapsed time, 0:15:10 cpu time, factor 1.78)
12:57:31 Running HOL-Import ...
12:57:32 HOL-Import: theory Import_Setup
12:57:33 HOL-Import: theory HOL_Light_Maps
12:57:35 Warning: missing document directory
12:57:35 Skipping theories "HOL_Light_Import" (undefined HOL_LIGHT_BUNDLE)
12:57:35 Timing HOL-Import (2 threads, 2.036s elapsed time, 3.000s cpu time, 0.056s GC time, factor 1.47)
12:57:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Import
12:57:35 Finished HOL-Import (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.17)
12:57:35 Running HOL-Induct ...
12:57:36 HOL-Induct: theory Old_Datatype
12:57:40 HOL-Induct: theory Common_Patterns
12:57:42 HOL-Induct: theory ABexp
12:57:42 HOL-Induct: theory Com
12:57:47 HOL-Induct: theory Comb
12:57:48 HOL-Induct: theory Nested_Datatype
12:57:50 HOL-Induct: theory Sexp
12:57:51 HOL-Induct: theory SList
12:57:51 HOL-Induct: theory Ordinals
12:57:51 HOL-Induct: theory PropLog
12:57:52 HOL-Induct: theory QuoDataType
12:57:53 HOL-Induct: theory QuoNestedDataType
12:57:55 HOL-Induct: theory Sigma_Algebra
12:57:55 HOL-Induct: theory Term
12:57:57 HOL-Induct: theory Tree
12:58:09 Timing HOL-Induct (2 threads, 29.877s elapsed time, 44.212s cpu time, 6.284s GC time, factor 1.48)
12:58:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct
12:58:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/document.pdf
12:58:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/outline.pdf
12:58:09 Finished HOL-Induct (0:00:33 elapsed time, 0:00:49 cpu time, factor 1.46)
12:58:09 Running HOL-Isar_Examples ...
12:58:10 HOL-Isar_Examples: theory Lattice_Syntax
12:58:10 HOL-Isar_Examples: theory Multiset
12:58:17 HOL-Isar_Examples: theory Factorial_Ring
12:58:25 HOL-Isar_Examples: theory Euclidean_Algorithm
12:58:35 HOL-Isar_Examples: theory Primes
12:58:50 HOL-Isar_Examples: theory First_Order_Logic
12:58:50 HOL-Isar_Examples: theory Basic_Logic
12:58:50 Timing HOL-Imperative_HOL (2 threads, 187.993s elapsed time, 225.972s cpu time, 7.336s GC time, factor 1.20)
12:58:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL
12:58:50 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/document.pdf
12:58:50 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/outline.pdf
12:58:50 Finished HOL-Imperative_HOL (0:03:11 elapsed time, 0:08:26 cpu time, factor 2.65)
12:58:50 Running HOL-Lattice ...
12:58:50 HOL-Isar_Examples: theory Cantor
12:58:50 HOL-Isar_Examples: theory Drinker
12:58:51 HOL-Isar_Examples: theory Expr_Compiler
12:58:51 HOL-Isar_Examples: theory Group
12:58:51 HOL-Isar_Examples: theory Group_Context
12:58:51 HOL-Isar_Examples: theory Group_Notepad
12:58:52 HOL-Lattice: theory Orders
12:58:52 HOL-Isar_Examples: theory Hoare
12:58:52 HOL-Isar_Examples: theory Knaster_Tarski
12:58:52 HOL-Isar_Examples: theory Fibonacci
12:58:52 HOL-Isar_Examples: theory Mutilated_Checkerboard
12:58:53 HOL-Isar_Examples: theory Peirce
12:58:53 HOL-Lattice: theory Bounds
12:58:53 HOL-Isar_Examples: theory Puzzle
12:58:53 HOL-Isar_Examples: theory Schroeder_Bernstein
12:58:53 HOL-Lattice: theory Lattice
12:58:53 HOL-Isar_Examples: theory Hoare_Ex
12:58:53 HOL-Isar_Examples: theory Structured_Statements
12:58:54 HOL-Lattice: theory CompleteLattice
12:58:54 HOL-Isar_Examples: theory Summation
12:58:54 HOL-Isar_Examples: theory Higher_Order_Logic
12:59:00 Timing HOL-Lattice (2 threads, 6.037s elapsed time, 12.116s cpu time, 0.164s GC time, factor 2.01)
12:59:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice
12:59:00 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/document.pdf
12:59:00 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/outline.pdf
12:59:00 Finished HOL-Lattice (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.73)
12:59:00 Running HOL-Matrix_LP ...
12:59:01 HOL-Matrix_LP: theory Compute_Oracle
12:59:01 HOL-Matrix_LP: theory Lattice_Algebras
12:59:02 HOL-Matrix_LP: theory ComputeHOL
12:59:04 Timing HOL-Isar_Examples (2 threads, 50.453s elapsed time, 100.572s cpu time, 2.752s GC time, factor 1.99)
12:59:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples
12:59:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/document.pdf
12:59:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/outline.pdf
12:59:04 Finished HOL-Isar_Examples (0:00:54 elapsed time, 0:01:45 cpu time, factor 1.94)
12:59:04 Running HOL-Metis_Examples ...
12:59:05 HOL-Metis_Examples: theory Binary_Tree
12:59:05 HOL-Metis_Examples: theory Dense_Linear_Order
12:59:07 HOL-Metis_Examples: theory FuncSet
12:59:08 HOL-Metis_Examples: theory Abstraction
12:59:08 HOL-Metis_Examples: theory Function_Algebras
12:59:08 HOL-Metis_Examples: theory Message
12:59:08 HOL-Metis_Examples: theory Set_Algebras
12:59:09 HOL-Metis_Examples: theory Big_O
12:59:09 HOL-Matrix_LP: theory ComputeFloat
12:59:09 HOL-Matrix_LP: theory ComputeNumeral
12:59:09 HOL-Matrix_LP: theory LP
12:59:10 HOL-Matrix_LP: theory Matrix
12:59:10 HOL-Metis_Examples: theory Sets
12:59:10 HOL-Metis_Examples: theory Tarski
12:59:11 HOL-Metis_Examples: theory Clausification
12:59:12 HOL-Metis_Examples: theory Trans_Closure
12:59:12 HOL-Matrix_LP: theory SparseMatrix
12:59:12 HOL-Metis_Examples: theory Type_Encodings
12:59:12 HOL-Metis_Examples: theory Proxies
12:59:15 HOL-Matrix_LP: theory Cplex
12:59:31 Timing HOL-Matrix_LP (2 threads, 26.401s elapsed time, 50.480s cpu time, 1.472s GC time, factor 1.91)
12:59:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP
12:59:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/document.pdf
12:59:31 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/outline.pdf
12:59:31 Finished HOL-Matrix_LP (0:00:30 elapsed time, 0:00:55 cpu time, factor 1.82)
12:59:31 Running HOL-MicroJava ...
12:59:32 HOL-MicroJava: theory While_Combinator
12:59:35 HOL-MicroJava: theory Transitive_Closure_Table
12:59:35 HOL-MicroJava: theory Eisbach
12:59:35 HOL-MicroJava: theory Semilat
12:59:35 HOL-MicroJava: theory JBasis
12:59:36 HOL-MicroJava: theory AuxLemmas
12:59:36 HOL-MicroJava: theory Type
12:59:36 HOL-MicroJava: theory Err
12:59:38 HOL-MicroJava: theory Listn
12:59:38 HOL-MicroJava: theory Typing_Framework
12:59:38 HOL-MicroJava: theory Opt
12:59:39 HOL-MicroJava: theory Product
12:59:39 HOL-MicroJava: theory SemilatAlg
12:59:39 HOL-MicroJava: theory Decl
12:59:39 HOL-MicroJava: theory SystemClasses
12:59:39 HOL-MicroJava: theory TypeRel
12:59:39 HOL-MicroJava: theory Value
12:59:40 HOL-MicroJava: theory WellForm
12:59:40 HOL-MicroJava: theory State
12:59:41 HOL-MicroJava: theory Exceptions
12:59:41 HOL-MicroJava: theory Term
12:59:41 HOL-MicroJava: theory Kildall
12:59:41 HOL-MicroJava: theory LBVSpec
12:59:42 HOL-MicroJava: theory LBVComplete
12:59:43 HOL-MicroJava: theory LBVCorrect
12:59:43 HOL-MicroJava: theory Typing_Framework_err
12:59:43 HOL-MicroJava: theory Abstract_BV
12:59:44 HOL-MicroJava: theory Semilattices
12:59:44 HOL-MicroJava: theory JType
12:59:45 HOL-MicroJava: theory JVMType
12:59:45 HOL-MicroJava: theory WellType
12:59:46 HOL-MicroJava: theory Conform
12:59:46 HOL-MicroJava: theory Eval
12:59:46 HOL-MicroJava: theory JVMState
12:59:46 HOL-MicroJava: theory JVMInstructions
12:59:48 HOL-MicroJava: theory JVMExceptions
12:59:48 HOL-MicroJava: theory JVMExecInstr
12:59:49 HOL-MicroJava: theory JVMExec
12:59:49 HOL-MicroJava: theory DefsComp
12:59:49 HOL-MicroJava: theory Index
12:59:50 HOL-MicroJava: theory JVMDefensive
12:59:50 Timing HOL-IMP (2 threads, 297.555s elapsed time, 514.144s cpu time, 24.484s GC time, factor 1.73)
12:59:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP
12:59:50 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP/document.pdf
12:59:50 Finished HOL-IMP (0:05:04 elapsed time, 0:08:41 cpu time, factor 1.72)
12:59:50 Running HOL-Mutabelle ...
12:59:50 HOL-MicroJava: theory JVMListExample
12:59:51 HOL-MicroJava: theory Example
12:59:51 HOL-MicroJava: theory JListExample
12:59:51 HOL-Mutabelle: theory Refute
12:59:52 HOL-MicroJava: theory JTypeSafe
12:59:52 HOL-Mutabelle: theory MutabelleExtra
12:59:53 HOL-MicroJava: theory TypeInf
12:59:53 HOL-MicroJava: theory Effect
12:59:53 HOL-MicroJava: theory TranslCompTp
12:59:54 HOL-MicroJava: theory TranslComp
12:59:54 Timing HOL-Mutabelle (2 threads, 1.661s elapsed time, 3.200s cpu time, 0.028s GC time, factor 1.93)
12:59:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mutabelle
12:59:54 Finished HOL-Mutabelle (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.46)
12:59:54 Running HOL-NanoJava ...
12:59:54 HOL-MicroJava: theory LemmasComp
12:59:54 Timing HOL-Metis_Examples (2 threads, 48.088s elapsed time, 80.624s cpu time, 3.468s GC time, factor 1.68)
12:59:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Metis_Examples
12:59:54 Finished HOL-Metis_Examples (0:00:49 elapsed time, 0:01:35 cpu time, factor 1.92)
12:59:54 Running HOL-Nitpick_Examples ...
12:59:54 HOL-MicroJava: theory CorrComp
12:59:55 HOL-NanoJava: theory Term
12:59:55 HOL-Nitpick_Examples: theory Core_Nits
12:59:55 HOL-Nitpick_Examples: theory Datatype_Nits
12:59:57 HOL-Nitpick_Examples: theory Hotel_Nits
12:59:57 HOL-Nitpick_Examples: theory Induct_Nits
12:59:57 HOL-Nitpick_Examples: theory Integer_Nits
12:59:58 HOL-NanoJava: theory Decl
12:59:58 HOL-Nitpick_Examples: theory Mini_Nits
12:59:58 HOL-NanoJava: theory TypeRel
12:59:59 HOL-Nitpick_Examples: theory Mono_Nits
12:59:59 HOL-NanoJava: theory State
12:59:59 HOL-Nitpick_Examples: theory Pattern_Nits
12:59:59 HOL-Nitpick_Examples: theory Quotient_Syntax
13:00:00 HOL-Nitpick_Examples: theory Quotient_Product
13:00:00 HOL-Nitpick_Examples: theory Record_Nits
13:00:00 HOL-NanoJava: theory AxSem
13:00:00 HOL-NanoJava: theory OpSem
13:00:00 HOL-Nitpick_Examples: theory Manual_Nits
13:00:01 HOL-Nitpick_Examples: theory Refute_Nits
13:00:01 HOL-NanoJava: theory Equivalence
13:00:01 HOL-NanoJava: theory Example
13:00:04 Timing HOL-NanoJava (2 threads, 7.169s elapsed time, 12.748s cpu time, 0.580s GC time, factor 1.78)
13:00:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava
13:00:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/document.pdf
13:00:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/outline.pdf
13:00:04 Finished HOL-NanoJava (0:00:10 elapsed time, 0:00:16 cpu time, factor 1.61)
13:00:04 Running HOL-Nominal-Examples ...
13:00:06 HOL-Nitpick_Examples: theory Special_Nits
13:00:06 HOL-Nominal-Examples: theory CK_Machine
13:00:06 HOL-Nominal-Examples: theory CR_Takahashi
13:00:06 HOL-Nitpick_Examples: theory Tests_Nits
13:00:08 HOL-Nitpick_Examples: theory Typedef_Nits
13:00:11 HOL-Nominal-Examples: theory Class1
13:00:13 HOL-Nitpick_Examples: theory Nitpick_Examples
13:00:17 HOL-MicroJava: theory BVSpec
13:00:18 HOL-MicroJava: theory EffectMono
13:00:18 HOL-MicroJava: theory Altern
13:00:18 HOL-MicroJava: theory Correct
13:00:18 HOL-MicroJava: theory Typing_Framework_JVM
13:00:18 HOL-MicroJava: theory BVSpecTypeSafe
13:00:19 HOL-MicroJava: theory JVM
13:00:19 HOL-MicroJava: theory CorrCompTp
13:00:20 HOL-MicroJava: theory BVNoTypeError
13:00:20 HOL-MicroJava: theory BVExample
13:00:21 HOL-MicroJava: theory LBVJVM
13:00:21 HOL-MicroJava: theory MicroJava
13:00:22 HOL-Nominal-Examples: theory Compile
13:00:46 HOL-Nominal-Examples: theory Contexts
13:00:50 HOL-Nominal-Examples: theory Crary
13:00:56 HOL-Nominal-Examples: theory Fsub
13:01:05 HOL-Nominal-Examples: theory Height
13:01:08 HOL-Nominal-Examples: theory Lam_Funs
13:01:12 HOL-Nominal-Examples: theory CR
13:01:12 HOL-Nominal-Examples: theory SN
13:01:14 HOL-Nominal-Examples: theory Lambda_mu
13:01:19 HOL-Nominal-Examples: theory LocalWeakening
13:01:22 HOL-Nominal-Examples: theory Pattern
13:01:33 HOL-Nominal-Examples: theory SOS
13:01:37 HOL-Nominal-Examples: theory Standardization
13:01:41 HOL-Nominal-Examples: theory Support
13:01:41 HOL-Nominal-Examples: theory Type_Preservation
13:01:46 HOL-Nominal-Examples: theory W
13:01:54 HOL-Nominal-Examples: theory Weakening
13:02:39 Timing HOL-MicroJava (2 threads, 181.808s elapsed time, 349.152s cpu time, 9.484s GC time, factor 1.92)
13:02:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava
13:02:39 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/document.pdf
13:02:39 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/outline.pdf
13:02:39 Finished HOL-MicroJava (0:03:07 elapsed time, 0:05:56 cpu time, factor 1.90)
13:02:39 Running HOL-Nonstandard_Analysis-Examples ...
13:02:41 HOL-Nonstandard_Analysis-Examples: theory Multiset
13:02:48 HOL-Nonstandard_Analysis-Examples: theory Factorial_Ring
13:02:58 HOL-Nonstandard_Analysis-Examples: theory Euclidean_Algorithm
13:03:07 HOL-Nonstandard_Analysis-Examples: theory Primes
13:03:08 HOL-Nonstandard_Analysis-Examples: theory NSPrimes
13:03:24 Timing HOL-Nonstandard_Analysis-Examples (2 threads, 42.759s elapsed time, 77.556s cpu time, 2.080s GC time, factor 1.81)
13:03:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis-Examples
13:03:24 Finished HOL-Nonstandard_Analysis-Examples (0:00:44 elapsed time, 0:01:19 cpu time, factor 1.78)
13:03:24 Running HOL-Number_Theory ...
13:03:25 HOL-Number_Theory: theory Congruence
13:03:25 HOL-Number_Theory: theory FuncSet
13:03:27 HOL-Number_Theory: theory Multiset
13:03:27 HOL-Number_Theory: theory Lattice
13:03:28 HOL-Nominal-Examples: theory Class2
13:03:30 HOL-Number_Theory: theory Group
13:03:31 HOL-Nominal-Examples: theory Class3
13:03:32 HOL-Number_Theory: theory FiniteProduct
13:03:33 HOL-Number_Theory: theory Ring
13:04:01 HOL-Number_Theory: theory MiscAlgebra
13:04:01 HOL-Number_Theory: theory Fib
13:04:01 HOL-Number_Theory: theory Factorial_Ring
13:04:09 HOL-Number_Theory: theory Euclidean_Algorithm
13:04:19 HOL-Number_Theory: theory Primes
13:04:20 HOL-Number_Theory: theory Cong
13:04:20 HOL-Number_Theory: theory Eratosthenes
13:04:21 HOL-Number_Theory: theory Residues
13:04:23 HOL-Number_Theory: theory Gauss
13:04:23 HOL-Number_Theory: theory Pocklington
13:04:23 HOL-Number_Theory: theory Number_Theory
13:05:00 Timing HOL-Number_Theory (2 threads, 90.323s elapsed time, 170.040s cpu time, 4.448s GC time, factor 1.88)
13:05:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory
13:05:00 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/document.pdf
13:05:00 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/outline.pdf
13:05:00 Finished HOL-Number_Theory (0:01:35 elapsed time, 0:02:56 cpu time, factor 1.84)
13:05:00 Running HOL-Old_Number_Theory ...
13:05:01 HOL-Old_Number_Theory: theory Infinite_Set
13:05:01 HOL-Old_Number_Theory: theory Multiset
13:05:08 HOL-Old_Number_Theory: theory Permutation
13:05:18 HOL-Old_Number_Theory: theory BijectionRel
13:05:18 HOL-Old_Number_Theory: theory Legacy_GCD
13:05:19 HOL-Old_Number_Theory: theory Primes
13:05:19 HOL-Old_Number_Theory: theory Factorization
13:05:20 HOL-Old_Number_Theory: theory Fib
13:05:20 HOL-Old_Number_Theory: theory IntPrimes
13:05:20 HOL-Old_Number_Theory: theory Pocklington
13:05:21 HOL-Old_Number_Theory: theory Chinese
13:05:21 HOL-Old_Number_Theory: theory IntFact
13:05:21 HOL-Old_Number_Theory: theory EulerFermat
13:05:21 HOL-Old_Number_Theory: theory Finite2
13:05:22 HOL-Old_Number_Theory: theory WilsonBij
13:05:22 HOL-Old_Number_Theory: theory WilsonRuss
13:05:22 HOL-Old_Number_Theory: theory Int2
13:05:23 HOL-Old_Number_Theory: theory EvenOdd
13:05:23 HOL-Old_Number_Theory: theory Residues
13:05:23 HOL-Old_Number_Theory: theory Euler
13:05:24 HOL-Old_Number_Theory: theory Gauss
13:05:24 HOL-Old_Number_Theory: theory Quadratic_Reciprocity
13:05:32 Timing HOL-Nitpick_Examples (2 threads, 335.425s elapsed time, 134.800s cpu time, 2.788s GC time, factor 0.40)
13:05:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nitpick_Examples
13:05:32 Finished HOL-Nitpick_Examples (0:05:37 elapsed time, 0:11:46 cpu time, factor 2.10)
13:05:32 Running HOL-Predicate_Compile_Examples ...
13:05:33 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Alternative_Defs
13:05:34 HOL-Predicate_Compile_Examples: theory Examples
13:05:34 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck
13:05:34 HOL-Predicate_Compile_Examples: theory IMP_1
13:05:35 HOL-Predicate_Compile_Examples: theory IMP_2
13:05:36 HOL-Predicate_Compile_Examples: theory IMP_3
13:05:37 HOL-Predicate_Compile_Examples: theory IMP_4
13:05:39 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck_Examples
13:05:45 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Tests
13:05:52 HOL-Predicate_Compile_Examples: theory Specialisation_Examples
13:06:08 Timing HOL-Old_Number_Theory (2 threads, 61.866s elapsed time, 118.492s cpu time, 2.552s GC time, factor 1.92)
13:06:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Old_Number_Theory
13:06:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Old_Number_Theory/document.pdf
13:06:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Old_Number_Theory/outline.pdf
13:06:08 Finished HOL-Old_Number_Theory (0:01:07 elapsed time, 0:02:05 cpu time, factor 1.86)
13:06:08 HOL-Probability-ex CANCELLED
13:06:08 Running HOL-Prolog ...
13:06:10 HOL-Prolog: theory HOHH
13:06:10 HOL-Prolog: theory Func
13:06:10 HOL-Prolog: theory Test
13:06:10 HOL-Prolog: theory Type
13:06:11 Timing HOL-Prolog (2 threads, 0.412s elapsed time, 0.440s cpu time, 0.000s GC time, factor 1.07)
13:06:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Prolog
13:06:11 Finished HOL-Prolog (0:00:03 elapsed time)
13:06:11 Running HOL-Proofs-Extraction ...
13:06:13 HOL-Proofs-Extraction: theory Adhoc_Overloading
13:06:13 HOL-Proofs-Extraction: theory Binomial
13:06:13 HOL-Proofs-Extraction: theory Code_Abstract_Nat
13:06:14 HOL-Proofs-Extraction: theory Code_Target_Nat
13:06:15 HOL-Proofs-Extraction: theory GCD
13:06:52 HOL-Proofs-Extraction: theory Code_Target_Int
13:06:53 HOL-Proofs-Extraction: theory Code_Target_Numeral
13:06:53 HOL-Proofs-Extraction: theory Monad_Syntax
13:06:53 HOL-Proofs-Extraction: theory Multiset
13:06:55 HOL-Proofs-Extraction: theory State_Monad
13:07:27 HOL-Predicate_Compile_Examples: theory Hotel_Example
13:07:27 HOL-Predicate_Compile_Examples: theory Code_Prolog
13:07:27 HOL-Predicate_Compile_Examples: theory Code_Prolog_Examples
13:07:30 HOL-Predicate_Compile_Examples: theory Context_Free_Grammar_Example
13:07:31 HOL-Predicate_Compile_Examples: theory Lambda_Example
13:07:31 HOL-Predicate_Compile_Examples: theory Hotel_Example_Prolog
13:07:31 HOL-Predicate_Compile_Examples: theory List_Examples
13:07:37 HOL-Predicate_Compile_Examples: theory Reg_Exp_Example
13:07:45 Timing HOL-Predicate_Compile_Examples (2 threads, 131.697s elapsed time, 222.516s cpu time, 13.080s GC time, factor 1.69)
13:07:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Predicate_Compile_Examples
13:07:45 Finished HOL-Predicate_Compile_Examples (0:02:13 elapsed time, 0:05:18 cpu time, factor 2.38)
13:07:45 Running HOL-Proofs-Lambda ...
13:07:47 HOL-Proofs-Lambda: theory GCD
13:07:51 HOL-Proofs-Extraction: theory Factorial_Ring
13:08:11 HOL-Proofs-Lambda: theory Code_Target_Int
13:08:15 HOL-Proofs-Extraction: theory Euclidean_Algorithm
13:08:31 HOL-Proofs-Extraction: theory Primes
13:09:21 HOL-Proofs-Lambda: theory Lambda
13:09:21 HOL-Proofs-Lambda: theory Commutation
13:09:22 HOL-Proofs-Lambda: theory ListOrder
13:09:24 HOL-Proofs-Lambda: theory ListApplication
13:09:25 HOL-Proofs-Lambda: theory LambdaType
13:09:25 HOL-Proofs-Lambda: theory ParRed
13:09:26 HOL-Proofs-Lambda: theory Eta
13:09:27 HOL-Proofs-Lambda: theory ListBeta
13:09:29 HOL-Proofs-Lambda: theory InductTermi
13:09:29 HOL-Proofs-Lambda: theory StrongNorm
13:09:33 HOL-Proofs-Lambda: theory NormalForm
13:09:34 HOL-Proofs-Lambda: theory Standardization
13:09:36 HOL-Proofs-Lambda: theory WeakNorm
13:12:07 Timing HOL-Proofs-Lambda (2 threads, 256.747s elapsed time, 385.972s cpu time, 8.120s GC time, factor 1.50)
13:12:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda
13:12:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda/document.pdf
13:12:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Lambda/outline.pdf
13:12:07 Finished HOL-Proofs-Lambda (0:04:21 elapsed time, 0:06:31 cpu time, factor 1.50)
13:12:07 Running HOL-Proofs-ex ...
13:12:09 HOL-Proofs-ex: theory Drinker
13:12:09 HOL-Proofs-ex: theory Hilbert_Classical
13:12:09 HOL-Proofs-ex: theory XML_Data
13:12:09 HOL-Proofs-ex: theory Proof_Terms
13:12:11 Timing HOL-Proofs-ex (2 threads, 2.069s elapsed time, 3.984s cpu time, 0.000s GC time, factor 1.93)
13:12:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-ex
13:12:11 Finished HOL-Proofs-ex (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.46)
13:12:11 Running HOL-Quickcheck_Examples ...
13:12:12 HOL-Quickcheck_Examples: theory AList
13:12:12 HOL-Quickcheck_Examples: theory Completeness
13:12:13 HOL-Quickcheck_Examples: theory Dlist
13:12:14 HOL-Quickcheck_Examples: theory Multiset
13:12:15 HOL-Quickcheck_Examples: theory DAList
13:12:16 HOL-Quickcheck_Examples: theory Quickcheck_Interfaces
13:12:17 HOL-Quickcheck_Examples: theory Quickcheck_Lattice_Examples
13:12:17 HOL-Quickcheck_Examples: theory Quickcheck_Nesting
13:12:18 HOL-Quickcheck_Examples: theory Quickcheck_Nesting_Example
13:12:20 HOL-Quickcheck_Examples: theory DAList_Multiset
13:12:21 HOL-Quickcheck_Examples: theory Quickcheck_Examples
13:13:51 HOL-Quickcheck_Examples: theory Predicate_Compile_Alternative_Defs
13:13:51 HOL-Quickcheck_Examples: theory Quickcheck_Narrowing_Examples
13:13:51 HOL-Quickcheck_Examples: theory Predicate_Compile_Quickcheck
13:13:52 HOL-Quickcheck_Examples: theory Hotel_Example
13:13:59 HOL-Proofs-Extraction: theory Util
13:13:59 HOL-Proofs-Extraction: theory Higman
13:13:59 HOL-Proofs-Extraction: theory Euclid
13:14:01 HOL-Proofs-Extraction: theory Pigeonhole
13:14:43 HOL-Proofs-Extraction: theory QuotRem
13:14:47 HOL-Proofs-Extraction: theory Warshall
13:14:48 HOL-Proofs-Extraction: theory Greatest_Common_Divisor
13:14:55 HOL-Proofs-Extraction: theory Higman_Extraction
13:15:01 Timing HOL-Quickcheck_Examples (2 threads, 167.839s elapsed time, 226.224s cpu time, 6.148s GC time, factor 1.35)
13:15:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quickcheck_Examples
13:15:01 Finished HOL-Quickcheck_Examples (0:02:49 elapsed time, 0:05:20 cpu time, factor 1.89)
13:15:01 Running HOL-Quotient_Examples ...
13:15:03 HOL-Quotient_Examples: theory Congruence
13:15:03 HOL-Quotient_Examples: theory FuncSet
13:15:03 HOL-Quotient_Examples: theory Lift_DList
13:15:04 HOL-Quotient_Examples: theory Lattice
13:15:04 HOL-Quotient_Examples: theory Lift_FSet
13:15:04 HOL-Quotient_Examples: theory Lift_Set
13:15:05 HOL-Quotient_Examples: theory Lifting_Code_Dt_Test
13:15:06 HOL-Quotient_Examples: theory Group
13:15:08 HOL-Quotient_Examples: theory Int_Pow
13:15:08 HOL-Quotient_Examples: theory Multiset
13:15:13 Timing HOL-Proofs-Extraction (2 threads, 537.360s elapsed time, 1037.460s cpu time, 17.384s GC time, factor 1.93)
13:15:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction
13:15:13 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/document.pdf
13:15:13 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs-Extraction/outline.pdf
13:15:13 Finished HOL-Proofs-Extraction (0:09:01 elapsed time, 0:17:21 cpu time, factor 1.93)
13:15:13 Running HOL-SET_Protocol ...
13:15:13 HOL-Quotient_Examples: theory Quotient_Syntax
13:15:13 HOL-Quotient_Examples: theory Lift_Fun
13:15:14 HOL-Quotient_Examples: theory Quotient_Message
13:15:14 HOL-SET_Protocol: theory Nat_Bijection
13:15:15 HOL-Quotient_Examples: theory Quotient_Option
13:15:15 HOL-SET_Protocol: theory Message_SET
13:15:15 HOL-Quotient_Examples: theory Quotient_Product
13:15:16 HOL-Quotient_Examples: theory Quotient_Rat
13:15:16 HOL-Quotient_Examples: theory Quotient_Set
13:15:16 HOL-Quotient_Examples: theory Quotient_List
13:15:17 HOL-Quotient_Examples: theory DList
13:15:17 HOL-Quotient_Examples: theory Quotient_FSet
13:15:20 HOL-SET_Protocol: theory Event_SET
13:15:20 HOL-Quotient_Examples: theory Quotient_Int
13:15:20 HOL-SET_Protocol: theory Public_SET
13:15:21 HOL-SET_Protocol: theory Cardholder_Registration
13:15:21 HOL-SET_Protocol: theory Merchant_Registration
13:15:22 HOL-SET_Protocol: theory Purchase
13:15:24 HOL-SET_Protocol: theory SET_Protocol
13:16:14 Timing HOL-Quotient_Examples (2 threads, 70.245s elapsed time, 109.140s cpu time, 7.948s GC time, factor 1.55)
13:16:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quotient_Examples
13:16:14 Finished HOL-Quotient_Examples (0:01:12 elapsed time, 0:02:51 cpu time, factor 2.38)
13:16:14 Running HOL-SPARK-Examples ...
13:16:15 Timing HOL-SET_Protocol (2 threads, 58.627s elapsed time, 100.868s cpu time, 1.768s GC time, factor 1.72)
13:16:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol
13:16:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/document.pdf
13:16:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/outline.pdf
13:16:15 Finished HOL-SET_Protocol (0:01:02 elapsed time, 0:01:45 cpu time, factor 1.70)
13:16:15 Running HOL-SPARK-Manual ...
13:16:15 HOL-SPARK-Examples: theory RMD_Lemmas
13:16:15 HOL-SPARK-Examples: theory RMD
13:16:16 HOL-SPARK-Examples: theory Greatest_Common_Divisor
13:16:16 HOL-SPARK-Examples: theory Longest_Increasing_Subsequence
13:16:17 HOL-SPARK-Examples: theory RMD_Specification
13:16:17 HOL-SPARK-Manual: theory Complex_Types
13:16:17 HOL-SPARK-Manual: theory Greatest_Common_Divisor
13:16:17 HOL-SPARK-Examples: theory F
13:16:18 HOL-SPARK-Manual: theory Proc1
13:16:18 HOL-SPARK-Manual: theory Proc2
13:16:19 HOL-SPARK-Manual: theory VC_Principles
13:16:19 HOL-SPARK-Manual: theory Reference
13:16:19 HOL-SPARK-Manual: theory Simple_Greatest_Common_Divisor
13:16:19 HOL-SPARK-Manual: theory Example_Verification
13:16:21 HOL-SPARK-Examples: theory Hash
13:16:23 HOL-SPARK-Examples: theory K_L
13:16:24 HOL-SPARK-Examples: theory K_R
13:16:25 HOL-SPARK-Examples: theory R_L
13:16:26 Timing HOL-SPARK-Manual (2 threads, 5.750s elapsed time, 12.024s cpu time, 0.232s GC time, factor 2.09)
13:16:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual
13:16:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/document.pdf
13:16:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/outline.pdf
13:16:26 Finished HOL-SPARK-Manual (0:00:10 elapsed time, 0:00:18 cpu time, factor 1.75)
13:16:26 Running HOL-Statespace ...
13:16:26 HOL-SPARK-Examples: theory R_R
13:16:27 HOL-SPARK-Examples: theory Round
13:16:27 HOL-Statespace: theory DistinctTreeProver
13:16:27 HOL-SPARK-Examples: theory S_L
13:16:29 HOL-SPARK-Examples: theory S_R
13:16:29 HOL-Statespace: theory StateFun
13:16:29 HOL-Statespace: theory StateSpaceLocale
13:16:29 HOL-Statespace: theory StateSpaceSyntax
13:16:30 HOL-Statespace: theory StateSpaceEx
13:16:30 HOL-SPARK-Examples: theory Sqrt
13:16:40 Timing HOL-SPARK-Examples (2 threads, 24.259s elapsed time, 43.836s cpu time, 0.824s GC time, factor 1.81)
13:16:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Examples
13:16:40 Finished HOL-SPARK-Examples (0:00:26 elapsed time, 0:00:45 cpu time, factor 1.74)
13:16:40 Running HOL-TLA-Buffer ...
13:16:42 HOL-TLA-Buffer: theory Buffer
13:16:42 HOL-TLA-Buffer: theory DBuffer
13:16:43 Timing HOL-TLA-Buffer (2 threads, 1.209s elapsed time, 2.424s cpu time, 0.000s GC time, factor 2.00)
13:16:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Buffer
13:16:43 Finished HOL-TLA-Buffer (0:00:02 elapsed time, 0:00:03 cpu time)
13:16:43 Running HOL-TLA-Inc ...
13:16:45 HOL-TLA-Inc: theory Inc
13:16:48 Timing HOL-Statespace (2 threads, 18.375s elapsed time, 24.344s cpu time, 0.480s GC time, factor 1.32)
13:16:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace
13:16:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/document.pdf
13:16:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/outline.pdf
13:16:48 Finished HOL-Statespace (0:00:21 elapsed time, 0:00:28 cpu time, factor 1.31)
13:16:48 Timing HOL-TLA-Inc (2 threads, 2.359s elapsed time, 4.984s cpu time, 0.068s GC time, factor 2.11)
13:16:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Inc
13:16:48 Finished HOL-TLA-Inc (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.63)
13:16:48 Running HOL-TLA-Memory ...
13:16:48 Running HOL-TPTP ...
13:16:49 HOL-TPTP: theory ATP_Theory_Export
13:16:49 HOL-TPTP: theory MaSh_Export_Base
13:16:49 HOL-TLA-Memory: theory RPCMemoryParams
13:16:49 HOL-TLA-Memory: theory MemoryParameters
13:16:49 HOL-TLA-Memory: theory ProcedureInterface
13:16:50 HOL-TPTP: theory MaSh_Eval
13:16:50 HOL-TPTP: theory THF_Arith
13:16:50 HOL-TPTP: theory TPTP_Parser
13:16:50 HOL-TLA-Memory: theory RPCParameters
13:16:50 HOL-TLA-Memory: theory Memory
13:16:51 HOL-TLA-Memory: theory MemClerkParameters
13:16:51 HOL-TLA-Memory: theory RPC
13:16:52 HOL-TLA-Memory: theory MemClerk
13:16:52 HOL-TLA-Memory: theory MemoryImplementation
13:16:52 HOL-TPTP: theory TPTP_Interpret
13:16:53 HOL-TPTP: theory TPTP_Proof_Reconstruction
13:16:54 HOL-TPTP: theory Refute
13:16:55 HOL-TPTP: theory ATP_Problem_Import
13:16:56 Timing HOL-TPTP (2 threads, 6.606s elapsed time, 10.056s cpu time, 0.268s GC time, factor 1.52)
13:16:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TPTP
13:16:56 Finished HOL-TPTP (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.40)
13:16:56 Running HOL-UNITY ...
13:16:58 HOL-UNITY: theory ListOrder
13:16:58 HOL-UNITY: theory Multiset
13:16:59 HOL-UNITY: theory UNITY
13:17:00 HOL-UNITY: theory Constrains
13:17:01 HOL-UNITY: theory Deadlock
13:17:01 HOL-UNITY: theory FP
13:17:01 HOL-UNITY: theory Network
13:17:02 HOL-UNITY: theory WFair
13:17:03 HOL-UNITY: theory SubstAx
13:17:03 Timing HOL-TLA-Memory (2 threads, 13.328s elapsed time, 25.344s cpu time, 0.624s GC time, factor 1.90)
13:17:03 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Memory
13:17:03 Finished HOL-TLA-Memory (0:00:15 elapsed time, 0:00:27 cpu time, factor 1.79)
13:17:03 Running HOL-Unix ...
13:17:04 HOL-UNITY: theory Detects
13:17:04 HOL-UNITY: theory Union
13:17:04 HOL-UNITY: theory Comp
13:17:04 HOL-UNITY: theory Multiset_Order
13:17:05 HOL-UNITY: theory Follows
13:17:05 HOL-UNITY: theory Guar
13:17:05 HOL-Unix: theory Nested_Environment
13:17:05 HOL-Unix: theory Sublist
13:17:05 HOL-UNITY: theory Extend
13:17:05 HOL-UNITY: theory Transformers
13:17:06 HOL-UNITY: theory ProgressSets
13:17:07 HOL-UNITY: theory Project
13:17:07 HOL-UNITY: theory Rename
13:17:07 HOL-Unix: theory Unix
13:17:07 HOL-UNITY: theory Lift_prog
13:17:07 HOL-UNITY: theory ELT
13:17:08 HOL-UNITY: theory PPROD
13:17:08 HOL-UNITY: theory UNITY_Main
13:17:08 HOL-UNITY: theory Token
13:17:08 HOL-UNITY: theory AllocBase
13:17:09 HOL-UNITY: theory Alloc
13:17:09 HOL-UNITY: theory AllocImpl
13:17:12 HOL-UNITY: theory Client
13:17:13 HOL-UNITY: theory Channel
13:17:13 HOL-UNITY: theory Common
13:17:13 HOL-UNITY: theory Counter
13:17:13 HOL-UNITY: theory Counterc
13:17:13 HOL-UNITY: theory Handshake
13:17:13 HOL-UNITY: theory Lift
13:17:14 HOL-UNITY: theory Mutex
13:17:16 HOL-UNITY: theory NSP_Bad
13:17:17 HOL-UNITY: theory PriorityAux
13:17:17 HOL-UNITY: theory Priority
13:17:17 HOL-UNITY: theory Progress
13:17:17 HOL-UNITY: theory Reach
13:17:18 HOL-UNITY: theory TimerArray
13:17:18 HOL-UNITY: theory Reachability
13:17:21 Timing HOL-Unix (2 threads, 14.102s elapsed time, 27.912s cpu time, 0.904s GC time, factor 1.98)
13:17:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix
13:17:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/document.pdf
13:17:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/outline.pdf
13:17:21 Finished HOL-Unix (0:00:17 elapsed time, 0:00:31 cpu time, factor 1.84)
13:17:21 Running HOL-Word-Examples ...
13:17:23 HOL-Word-Examples: theory WordBitwise
13:17:24 HOL-Word-Examples: theory WordExamples
13:17:26 Timing HOL-Word-Examples (2 threads, 2.766s elapsed time, 5.516s cpu time, 0.068s GC time, factor 1.99)
13:17:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-Examples
13:17:26 Finished HOL-Word-Examples (0:00:04 elapsed time, 0:00:07 cpu time, factor 1.56)
13:17:26 Running HOL-Word-SMT_Examples ...
13:17:28 HOL-Word-SMT_Examples: theory Boogie
13:17:28 HOL-Word-SMT_Examples: theory SMT_Examples
13:17:29 HOL-Word-SMT_Examples: theory SMT_Tests
13:17:31 HOL-Word-SMT_Examples: theory SMT_Word_Examples
13:18:06 HOL-Nominal-Examples: theory VC_Condition
13:18:09 Timing HOL-Nominal-Examples (2 threads, 1082.997s elapsed time, 2017.884s cpu time, 497.472s GC time, factor 1.86)
13:18:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal-Examples
13:18:09 Finished HOL-Nominal-Examples (0:18:05 elapsed time, 0:33:39 cpu time, factor 1.86)
13:18:10 Running HOL-ZF ...
13:18:11 Timing HOL-UNITY (2 threads, 67.543s elapsed time, 133.796s cpu time, 8.028s GC time, factor 1.98)
13:18:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY
13:18:11 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/document.pdf
13:18:11 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/outline.pdf
13:18:11 Finished HOL-UNITY (0:01:13 elapsed time, 0:02:22 cpu time, factor 1.93)
13:18:11 Running HOL-ex ...
13:18:11 HOL-ZF: theory Multiset
13:18:11 HOL-ZF: theory HOLZF
13:18:12 HOL-ZF: theory Zet
13:18:12 HOL-ex: theory Adhoc_Overloading
13:18:12 HOL-ex: theory Cartouche_Examples
13:18:12 HOL-ex: theory Chinese
13:18:13 HOL-ex: theory Code_Abstract_Nat
13:18:13 HOL-ex: theory Code_Binary_Nat
13:18:13 HOL-ex: theory FuncSet
13:18:14 HOL-ex: theory Hebrew
13:18:14 HOL-ex: theory Monad_Syntax
13:18:14 HOL-ex: theory Refute
13:18:15 HOL-ex: theory Serbian
13:18:17 HOL-ex: theory State_Monad
13:18:17 HOL-ZF: theory LProd
13:18:17 HOL-ex: theory Code_Binary_Nat_examples
13:18:17 HOL-ZF: theory MainZF
13:18:17 HOL-ex: theory Eval_Examples
13:18:17 HOL-ZF: theory Games
13:18:20 HOL-ex: theory Normalization_by_Evaluation
13:18:22 HOL-ex: theory Transitive_Closure_Table
13:18:33 Timing HOL-ZF (2 threads, 18.593s elapsed time, 38.244s cpu time, 1.328s GC time, factor 2.06)
13:18:33 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF
13:18:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/document.pdf
13:18:33 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/outline.pdf
13:18:33 Finished HOL-ZF (0:00:23 elapsed time, 0:00:44 cpu time, factor 1.91)
13:18:33 Running HOLCF-FOCUS ...
13:18:35 HOLCF-FOCUS: theory Infinite_Set
13:18:36 HOLCF-FOCUS: theory Countable_Set
13:18:36 HOLCF-FOCUS: theory Countable_Complete_Lattices
13:18:38 Timing HOL-Word-SMT_Examples (2 threads, 69.399s elapsed time, 93.328s cpu time, 0.668s GC time, factor 1.34)
13:18:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-SMT_Examples
13:18:38 Finished HOL-Word-SMT_Examples (0:01:11 elapsed time, 0:01:38 cpu time, factor 1.38)
13:18:38 Running HOLCF-IMP ...
13:18:39 HOLCF-FOCUS: theory Order_Continuity
13:18:40 HOLCF-IMP: theory AExp
13:18:40 HOLCF-FOCUS: theory Extended_Nat
13:18:41 HOLCF-IMP: theory BExp
13:18:42 HOLCF-FOCUS: theory Stream
13:18:43 HOLCF-IMP: theory Com
13:18:43 HOL-ex: theory Groebner_Examples
13:18:43 HOL-ex: theory PresburgerEx
13:18:43 HOLCF-FOCUS: theory Fstream
13:18:44 HOL-ex: theory AList
13:18:44 HOL-ex: theory Abstract_NAT
13:18:44 HOL-ex: theory Antiquote
13:18:44 HOLCF-FOCUS: theory FOCUS
13:18:44 HOLCF-FOCUS: theory Fstreams
13:18:44 HOL-ex: theory Arith_Examples
13:18:44 HOLCF-FOCUS: theory Buffer
13:18:44 HOL-ex: theory CTL
13:18:44 HOL-ex: theory Classical
13:18:44 HOLCF-FOCUS: theory Stream_adm
13:18:45 HOLCF-IMP: theory Big_Step
13:18:45 HOL-ex: theory Code_Target_Nat
13:18:45 HOLCF-IMP: theory Denotational
13:18:45 HOL-ex: theory Coercion_Examples
13:18:45 HOLCF-FOCUS: theory Buffer_adm
13:18:45 HOL-ex: theory Coherent
13:18:46 HOLCF-IMP: theory HoareEx
13:18:46 HOL-ex: theory Commands
13:18:46 HOL-ex: theory Debug
13:18:46 HOL-ex: theory Dlist
13:18:47 HOL-ex: theory Erdoes_Szekeres
13:18:47 HOL-ex: theory Executable_Relation
13:18:48 HOL-ex: theory FSet
13:18:48 HOL-ex: theory Birthday_Paradox
13:18:48 HOL-ex: theory Code_Target_Int
13:18:48 HOL-ex: theory Code_Target_Numeral
13:18:48 Timing HOLCF-IMP (2 threads, 8.423s elapsed time, 15.536s cpu time, 0.768s GC time, factor 1.84)
13:18:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP
13:18:48 Finished HOLCF-IMP (0:00:10 elapsed time, 0:00:17 cpu time, factor 1.67)
13:18:48 Running HOLCF-Library ...
13:18:49 HOL-ex: theory Transfer_Int_Nat
13:18:49 HOL-ex: theory Guess
13:18:49 HOL-ex: theory Hex_Bin_Examples
13:18:49 HOL-ex: theory IArray
13:18:50 HOLCF-Library: theory Infinite_Set
13:18:50 HOLCF-Library: theory Bool_Discrete
13:18:50 HOL-ex: theory IArray_Examples
13:18:50 HOLCF-Library: theory Char_Discrete
13:18:51 HOLCF-Library: theory Int_Discrete
13:18:51 HOL-ex: theory Iff_Oracle
13:18:51 HOL-ex: theory Induction_Schema
13:18:51 HOLCF-Library: theory Countable_Set
13:18:51 HOLCF-Library: theory Defl_Bifinite
13:18:51 HOL-ex: theory Infinite_Set
13:18:51 HOL-ex: theory Intuitionistic
13:18:52 HOL-ex: theory LaTeXsugar
13:18:52 HOL-ex: theory Adhoc_Overloading_Examples
13:18:52 HOL-ex: theory Lagrange
13:18:52 HOL-ex: theory List_to_Set_Comprehension_Examples
13:18:52 HOLCF-Library: theory Countable_Complete_Lattices
13:18:52 HOL-ex: theory LocaleTest2
13:18:52 HOLCF-Library: theory List_Cpo
13:18:53 HOLCF-Library: theory Nat_Discrete
13:18:53 HOLCF-Library: theory Sum_Cpo
13:18:53 HOL-ex: theory ML
13:18:53 HOL-ex: theory Mapping
13:18:53 HOLCF-Library: theory List_Predomain
13:18:54 Timing HOLCF-FOCUS (2 threads, 18.181s elapsed time, 36.288s cpu time, 1.012s GC time, factor 2.00)
13:18:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-FOCUS
13:18:54 Finished HOLCF-FOCUS (0:00:20 elapsed time, 0:00:38 cpu time, factor 1.89)
13:18:54 Running HOLCF-Tutorial ...
13:18:54 HOL-ex: theory Functions
13:18:54 HOL-ex: theory AList_Mapping
13:18:55 HOL-ex: theory Execute_Choice
13:18:55 HOLCF-Library: theory Option_Cpo
13:18:55 HOL-ex: theory MonoidGroup
13:18:55 HOLCF-Library: theory Order_Continuity
13:18:55 HOL-ex: theory Multiquote
13:18:56 HOL-ex: theory Multiset
13:18:56 HOLCF-Tutorial: theory Fixrec_ex
13:18:56 HOLCF-Tutorial: theory Domain_ex
13:18:56 HOLCF-Library: theory Extended_Nat
13:18:58 HOLCF-Library: theory Stream
13:18:59 HOLCF-Tutorial: theory New_Domain
13:18:59 HOLCF-Library: theory HOLCF_Library
13:19:01 HOL-ex: theory NatSum
13:19:01 HOL-ex: theory PER
13:19:01 HOL-ex: theory Parallel
13:19:01 HOL-ex: theory Bubblesort
13:19:02 HOL-ex: theory Factorial_Ring
13:19:02 HOL-ex: theory MergeSort
13:19:03 HOL-ex: theory Quicksort
13:19:04 HOL-ex: theory Perm
13:19:05 HOL-ex: theory Perm_Fragments
13:19:06 HOL-ex: theory Phantom_Type
13:19:07 HOL-ex: theory Cardinality
13:19:08 HOL-ex: theory FinFun
13:19:09 HOL-ex: theory Euclidean_Algorithm
13:19:10 HOL-ex: theory FinFunPred
13:19:10 Timing HOLCF-Library (2 threads, 19.547s elapsed time, 37.588s cpu time, 1.128s GC time, factor 1.92)
13:19:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Library
13:19:10 Finished HOLCF-Library (0:00:21 elapsed time, 0:00:39 cpu time, factor 1.83)
13:19:10 Running HOLCF-ex ...
13:19:11 HOL-ex: theory Primrec
13:19:11 HOL-ex: theory Records
13:19:12 HOLCF-ex: theory Infinite_Set
13:19:12 HOLCF-ex: theory Concurrency_Monad
13:19:12 Timing HOLCF-Tutorial (2 threads, 14.996s elapsed time, 20.520s cpu time, 0.460s GC time, factor 1.37)
13:19:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial
13:19:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/document.pdf
13:19:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/outline.pdf
13:19:12 Finished HOLCF-Tutorial (0:00:18 elapsed time, 0:00:24 cpu time, factor 1.33)
13:19:12 Running How_to_Prove_it ...
13:19:13 HOLCF-ex: theory Countable_Set
13:19:13 HOLCF-ex: theory Countable_Complete_Lattices
13:19:14 How_to_Prove_it: theory How_to_Prove_it
13:19:14 HOLCF-ex: theory Dnat
13:19:15 HOLCF-ex: theory Domain_Proofs
13:19:16 HOL-ex: theory Reflection
13:19:16 HOL-ex: theory Refute_Examples
13:19:17 HOLCF-ex: theory Fix2
13:19:17 HOLCF-ex: theory Hoare
13:19:17 HOLCF-ex: theory Letrec
13:19:17 HOLCF-ex: theory Loop
13:19:17 HOLCF-ex: theory Pattern_Match
13:19:17 HOLCF-ex: theory Powerdomain_ex
13:19:17 Timing How_to_Prove_it (2 threads, 1.857s elapsed time, 2.100s cpu time, 0.000s GC time, factor 1.13)
13:19:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it
13:19:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it/how_to_prove_it.pdf
13:19:17 Finished How_to_Prove_it (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.97)
13:19:17 Running IOA-ABP ...
13:19:18 HOLCF-ex: theory Order_Continuity
13:19:18 HOL-ex: theory Primes
13:19:19 HOLCF-ex: theory Extended_Nat
13:19:19 HOL-ex: theory Rewrite
13:19:19 IOA-ABP: theory Lemmas
13:19:19 IOA-ABP: theory Packet
13:19:19 HOL-ex: theory Eratosthenes
13:19:19 IOA-ABP: theory Action
13:19:19 HOL-ex: theory Rewrite_Examples
13:19:20 HOL-ex: theory Code_Timing
13:19:20 HOL-ex: theory SAT_Examples
13:19:20 HOLCF-ex: theory Stream
13:19:20 HOL-ex: theory Seq
13:19:21 HOL-ex: theory Set_Comprehension_Pointfree_Examples
13:19:22 HOL-ex: theory Set_Theory
13:19:22 IOA-ABP: theory Abschannel
13:19:22 IOA-ABP: theory Env
13:19:22 HOL-ex: theory Simproc_Tests
13:19:22 HOL-ex: theory Simps_Case_Conv
13:19:22 HOLCF-ex: theory Dagstuhl
13:19:22 IOA-ABP: theory Receiver
13:19:22 HOLCF-ex: theory Focus_ex
13:19:22 HOL-ex: theory Simps_Case_Conv_Examples
13:19:23 HOL-ex: theory Sudoku
13:19:23 IOA-ABP: theory Sender
13:19:23 IOA-ABP: theory Abschannel_finite
13:19:23 IOA-ABP: theory Impl
13:19:24 IOA-ABP: theory Impl_finite
13:19:24 HOL-ex: theory Tarski
13:19:24 IOA-ABP: theory Spec
13:19:24 IOA-ABP: theory Correctness
13:19:25 HOL-ex: theory Termination
13:19:27 Timing IOA-ABP (2 threads, 6.956s elapsed time, 13.880s cpu time, 0.512s GC time, factor 2.00)
13:19:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ABP
13:19:27 Finished IOA-ABP (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.75)
13:19:27 Running IOA-NTP ...
13:19:28 HOL-ex: theory ThreeDivides
13:19:29 HOL-ex: theory Argo_Examples
13:19:29 IOA-NTP: theory Lemmas
13:19:29 IOA-NTP: theory Multiset
13:19:29 IOA-NTP: theory Packet
13:19:29 IOA-NTP: theory Action
13:19:31 IOA-NTP: theory Abschannel
13:19:31 IOA-NTP: theory Receiver
13:19:32 HOL-ex: theory Ballot
13:19:32 IOA-NTP: theory Sender
13:19:32 Timing HOLCF-ex (2 threads, 20.037s elapsed time, 39.100s cpu time, 1.156s GC time, factor 1.95)
13:19:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-ex
13:19:32 Finished HOLCF-ex (0:00:22 elapsed time, 0:00:41 cpu time, factor 1.86)
13:19:32 Running IOA-Storage ...
13:19:33 HOL-ex: theory BinEx
13:19:33 IOA-NTP: theory Spec
13:19:33 HOL-ex: theory Cubic_Quartic
13:19:33 HOL-ex: theory Dedekind_Real
13:19:33 IOA-NTP: theory Impl
13:19:34 HOL-ex: theory Gauge_Integration
13:19:34 IOA-NTP: theory Correctness
13:19:34 HOL-ex: theory HarmonicSeries
13:19:34 IOA-Storage: theory Action
13:19:34 HOL-ex: theory Parallel_Example
13:19:35 HOL-ex: theory Pythagoras
13:19:35 HOL-ex: theory Reflection_Examples
13:19:35 IOA-Storage: theory Impl
13:19:35 IOA-Storage: theory Spec
13:19:36 IOA-Storage: theory Correctness
13:19:36 HOL-ex: theory Sqrt
13:19:36 HOL-ex: theory Sqrt_Script
13:19:37 HOL-ex: theory Sum_of_Powers
13:19:37 Timing IOA-Storage (2 threads, 2.362s elapsed time, 4.396s cpu time, 0.084s GC time, factor 1.86)
13:19:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-Storage
13:19:37 Finished IOA-Storage (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.44)
13:19:37 Running IOA-ex ...
13:19:37 HOL-ex: theory Sum_of_Squares
13:19:38 Timing IOA-NTP (2 threads, 8.288s elapsed time, 16.948s cpu time, 0.660s GC time, factor 2.04)
13:19:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-NTP
13:19:38 Finished IOA-NTP (0:00:10 elapsed time, 0:00:19 cpu time, factor 1.82)
13:19:38 Running Implementation ...
13:19:39 IOA-ex: theory TrivEx
13:19:39 IOA-ex: theory TrivEx2
13:19:39 Implementation: theory Base
13:19:39 Implementation: theory Eq
13:19:39 Implementation: theory Integration
13:19:39 Implementation: theory Isar
13:19:39 Implementation: theory Local_Theory
13:19:40 Implementation: theory ML
13:19:40 HOL-ex: theory SOS
13:19:40 Implementation: theory Prelim
13:19:40 Implementation: theory Proof
13:19:40 HOL-ex: theory SOS_Cert
13:19:40 Implementation: theory Syntax
13:19:41 Implementation: theory Tactic
13:19:41 HOL-ex: theory Transfer_Debug
13:19:41 HOL-ex: theory Transfer_Ex
13:19:41 HOL-ex: theory Transitive_Closure_Table_Ex
13:19:42 HOL-ex: theory Tree23
13:19:42 Timing IOA-ex (2 threads, 2.475s elapsed time, 4.124s cpu time, 0.096s GC time, factor 1.67)
13:19:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ex
13:19:42 Finished IOA-ex (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.35)
13:19:42 Running Isar_Ref ...
13:19:42 Implementation: theory Logic
13:19:44 Isar_Ref: theory Adhoc_Overloading
13:19:44 Isar_Ref: theory Base
13:19:44 Isar_Ref: theory Dlist
13:19:44 Isar_Ref: theory First_Order_Logic
13:19:44 Isar_Ref: theory Document_Preparation
13:19:44 Isar_Ref: theory FSet
13:19:45 Isar_Ref: theory Framework
13:19:46 Isar_Ref: theory Generic
13:19:46 Isar_Ref: theory Inner_Syntax
13:19:46 Isar_Ref: theory Old_Datatype
13:19:48 Timing Implementation (2 threads, 4.830s elapsed time, 8.684s cpu time, 0.036s GC time, factor 1.80)
13:19:48 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation
13:19:48 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation/implementation.pdf
13:19:48 Finished Implementation (0:00:09 elapsed time, 0:00:13 cpu time, factor 1.36)
13:19:48 Running JEdit ...
13:19:48 Isar_Ref: theory Old_Recdef
13:19:48 Isar_Ref: theory Outer_Syntax
13:19:49 Isar_Ref: theory Preface
13:19:49 Isar_Ref: theory Proof
13:19:49 JEdit: theory Base
13:19:49 JEdit: theory JEdit
13:19:49 Isar_Ref: theory Proof_Script
13:19:49 Isar_Ref: theory HOL_Specific
13:19:49 Isar_Ref: theory Quick_Reference
13:19:50 Isar_Ref: theory Spec
13:19:50 Isar_Ref: theory Symbols
13:19:50 Isar_Ref: theory Synopsis
13:19:59 Timing JEdit (2 threads, 1.344s elapsed time, 1.840s cpu time, 0.000s GC time, factor 1.37)
13:19:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit
13:19:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit/jedit.pdf
13:19:59 Finished JEdit (0:00:10 elapsed time, 0:00:11 cpu time, factor 1.02)
13:19:59 Running Locales ...
13:20:00 Locales: theory Examples
13:20:01 Locales: theory Examples1
13:20:01 Locales: theory Examples2
13:20:01 Locales: theory Examples3
13:20:02 HOL-ex: theory Unification
13:20:04 HOL-ex: theory While_Combinator
13:20:04 HOL-ex: theory While_Combinator_Example
13:20:05 Timing Locales (2 threads, 2.659s elapsed time, 6.048s cpu time, 0.108s GC time, factor 2.27)
13:20:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales
13:20:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales/locales.pdf
13:20:05 Finished Locales (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.48)
13:20:05 Running Main ...
13:20:06 Main: theory Main_Doc
13:20:10 Timing Main (2 threads, 1.832s elapsed time, 2.612s cpu time, 0.000s GC time, factor 1.43)
13:20:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main
13:20:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main/main.pdf
13:20:10 Finished Main (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.14)
13:20:10 Running Prog_Prove ...
13:20:11 Timing Isar_Ref (2 threads, 18.409s elapsed time, 35.508s cpu time, 1.620s GC time, factor 1.93)
13:20:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref
13:20:11 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref/isar-ref.pdf
13:20:11 Finished Isar_Ref (0:00:28 elapsed time, 0:00:44 cpu time, factor 1.60)
13:20:11 Running Sugar ...
13:20:11 Prog_Prove: theory Basics
13:20:11 Prog_Prove: theory Bool_nat_list
13:20:11 Prog_Prove: theory LaTeXsugar
13:20:11 Prog_Prove: theory Isar
13:20:12 Sugar: theory LaTeXsugar
13:20:12 Sugar: theory OptionalSugar
13:20:12 Prog_Prove: theory Logic
13:20:13 Prog_Prove: theory MyList
13:20:14 Sugar: theory Sugar
13:20:14 Prog_Prove: theory Types_and_funs
13:20:17 Timing Sugar (2 threads, 3.151s elapsed time, 3.964s cpu time, 0.032s GC time, factor 1.26)
13:20:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar
13:20:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar/sugar.pdf
13:20:17 Finished Sugar (0:00:06 elapsed time, 0:00:06 cpu time, factor 1.10)
13:20:17 Running Tutorial ...
13:20:19 Tutorial: theory ToyList_Test
13:20:20 Tutorial: theory AB
13:20:20 Tutorial: theory ABexpr
13:20:21 Tutorial: theory AdvancedInd
13:20:21 Tutorial: theory Base
13:20:21 Tutorial: theory CTL
13:20:21 Timing Prog_Prove (2 threads, 6.857s elapsed time, 14.272s cpu time, 0.736s GC time, factor 2.08)
13:20:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove
13:20:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove/prog-prove.pdf
13:20:21 Finished Prog_Prove (0:00:11 elapsed time, 0:00:18 cpu time, factor 1.64)
13:20:21 Running Typeclass_Hierarchy ...
13:20:22 Tutorial: theory CTLind
13:20:22 Tutorial: theory PDL
13:20:23 Typeclass_Hierarchy: theory Typeclass_Hierarchy
13:20:23 Tutorial: theory CodeGen
13:20:24 Tutorial: theory Nested
13:20:25 Tutorial: theory Even
13:20:25 Tutorial: theory Fundata
13:20:25 Tutorial: theory Advanced
13:20:26 Tutorial: theory Ifexpr
13:20:27 Timing Typeclass_Hierarchy (2 threads, 1.783s elapsed time, 2.012s cpu time, 0.000s GC time, factor 1.13)
13:20:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy
13:20:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy/typeclass_hierarchy.pdf
13:20:27 Finished Typeclass_Hierarchy (0:00:05 elapsed time, 0:00:05 cpu time, factor 0.99)
13:20:27 Tutorial: theory Itrev
13:20:28 Tutorial: theory Mutual
13:20:28 Tutorial: theory Option2
13:20:28 Tutorial: theory Plus
13:20:28 Tutorial: theory Star
13:20:28 Tutorial: theory ToyList
13:20:28 Tutorial: theory Tree
13:20:30 Tutorial: theory Trie
13:20:30 Tutorial: theory Tree2
13:20:30 Tutorial: theory appendix
13:20:30 Tutorial: theory case_exprs
13:20:30 Tutorial: theory fakenat
13:20:30 Tutorial: theory fun0
13:20:31 Tutorial: theory natsum
13:20:31 Tutorial: theory pairs2
13:20:31 Tutorial: theory prime_def
13:20:31 Tutorial: theory simp
13:20:31 Tutorial: theory simp2
13:20:31 Tutorial: theory types
13:20:31 Tutorial: theory unfoldnested
13:20:44 Tutorial: theory Documents
13:20:44 Tutorial: theory Message
13:20:46 Tutorial: theory Event
13:20:47 Tutorial: theory Public
13:20:47 Tutorial: theory NS_Public
13:20:49 Tutorial: theory Setup
13:20:50 Tutorial: theory Blast
13:20:50 Tutorial: theory Basic
13:20:50 Tutorial: theory Force
13:20:50 Tutorial: theory Pairs
13:20:50 Tutorial: theory Records
13:20:50 Tutorial: theory Overloading
13:20:50 Tutorial: theory Axioms
13:20:51 Tutorial: theory Numbers
13:20:51 Tutorial: theory Typedefs
13:20:52 Tutorial: theory Recur
13:20:52 Tutorial: theory Functions
13:20:52 Tutorial: theory Relations
13:20:52 Tutorial: theory TPrimes
13:20:53 Tutorial: theory Tacticals
13:20:53 Tutorial: theory Forward
13:20:53 Tutorial: theory Examples
13:20:53 Tutorial: theory find2
13:20:59 Timing Tutorial (2 threads, 35.237s elapsed time, 71.636s cpu time, 9.384s GC time, factor 2.03)
13:20:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial
13:20:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial/tutorial.pdf
13:20:59 Finished Tutorial (0:00:41 elapsed time, 0:01:17 cpu time, factor 1.87)
13:27:08 HOL-ex: theory Meson_Test
13:27:28 Timing HOL-ex (2 threads, 543.902s elapsed time, 1051.292s cpu time, 89.472s GC time, factor 1.93)
13:27:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex
13:27:28 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex/document.pdf
13:27:28 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex/outline.pdf
13:27:28 Finished HOL-ex (0:09:17 elapsed time, 0:18:34 cpu time, factor 2.00)
13:27:29 Unfinished session(s): HOL-Analysis, HOL-Analysis-ex, HOL-Probability, HOL-Probability-ex
13:27:29 
13:27:29 === TIMING ===
13:27:29 
13:27:29 Group timing: 2:31:44 elapsed time, 4:31:29 cpu time, factor 1.79
13:27:29 Group main: 0:35:27 elapsed time, 1:07:49 cpu time, factor 1.91
13:27:29 Group ZF: 0:01:35 elapsed time, 0:02:54 cpu time, factor 1.83
13:27:29 Group doc: 0:04:58 elapsed time, 0:07:24 cpu time, factor 1.49
13:27:29 Overall: 1:16:01 elapsed time, 6:30:24 cpu time, factor 5.14
13:27:29 
13:27:29 === FAILED SESSIONS ===
13:27:29 
13:27:29 Session HOL-Probability: CANCELLED
13:27:29 Session HOL-Probability-ex: CANCELLED
13:27:29 Session HOL-Analysis: FAILED 2
13:27:29 Session HOL-Analysis-ex: CANCELLED
13:27:29 Build step 'Execute shell' marked build as failure
13:27:29 Archiving artifacts
13:27:29 No emails were triggered.
13:27:29 Finished: FAILURE