Console Output

11:57:14 Started by upstream project "isabelle-repo" build number 441
11:57:14 originally caused by:
11:57:14  Started by an SCM change
11:57:14 [EnvInject] - Loading node environment variables.
11:57:14 Building remotely on workermta4 (mta_small) in workspace /media/data/jenkins/workspace/isabelle-repo-makeall
11:57:14 [isabelle-repo-makeall] $ hg showconfig paths.default
11:57:14 [isabelle-repo-makeall] $ hg pull --rev default
11:57:16 pulling from http://isabelle.in.tum.de/repos/isabelle/
11:57:16 searching for changes
11:57:16 adding changesets
11:57:16 adding manifests
11:57:16 adding file changes
11:57:16 added 1 changesets with 1 changes to 1 files
11:57:16 (run 'hg update' to get a working copy)
11:57:16 [isabelle-repo-makeall] $ hg update --clean --rev default
11:57:16 1 files updated, 0 files merged, 0 files removed, 0 files unresolved
11:57:16 [isabelle-repo-makeall] $ hg --config extensions.purge= clean --all
11:57:16 [isabelle-repo-makeall] $ hg log --rev . --template {node}
11:57:16 [isabelle-repo-makeall] $ hg log --rev . --template {rev}
11:57:16 No emails were triggered.
11:57:16 [EnvInject] - Executing scripts and injecting environment variables after the SCM step.
11:57:16 [EnvInject] - Injecting as environment variables the properties content 
11:57:16 ISABELLE_CI_PLATFORM=32
11:57:16 
11:57:16 [EnvInject] - Variables injected successfully.
11:57:16 [isabelle-repo-makeall] $ /bin/sh -xe /tmp/hudson5230080666219792610.sh
11:57:16 + Admin/jenkins/run_build makeall
11:57:16 + set -e
11:57:16 + PROFILE=makeall
11:57:16 + shift
11:57:16 + bin/isabelle components -a
11:57:17 + bin/isabelle jedit -bf
11:57:17 ### Building graph browser ...
11:57:17 warning: [options] bootstrap class path not set in conjunction with -source 1.4
11:57:17 warning: [options] source value 1.4 is obsolete and will be removed in a future release
11:57:17 warning: [options] target value 1.4 is obsolete and will be removed in a future release
11:57:17 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
11:57:18 Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.
11:57:18 Note: Recompile with -Xlint:deprecation for details.
11:57:18 4 warnings
11:57:19 ### Building Isabelle/Scala ...
11:58:03 ### Building Isabelle/jEdit ...
11:58:32 + bin/isabelle ci_build_makeall
11:58:38 
11:58:38 === CONFIGURATION ===
11:58:38 
11:58:38 ML_PLATFORM="x86-linux"
11:58:38 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86-linux"
11:58:38 ML_SYSTEM="polyml-5.6"
11:58:38 ML_OPTIONS="-H 1000 --gcthreads 2"
11:58:38 
11:58:38 === BUILD ===
11:58:38 
11:58:38 Build started at Thu, 15 Sep 2016 09:58:37 GMT
11:58:38 Isabelle id b4051d3f4e94
11:58:38 
11:58:38 === LOG ===
11:58:38 
11:58:38 Session Pure/Pure
11:58:39 Session CCL/CCL
11:58:39 Session CTT/CTT
11:58:39 Session Cube/Cube
11:58:39 Session FOL/FOL
11:58:39 Session FOL/FOL-ex
11:58:39 Session FOLP/FOLP
11:58:39 Session FOLP/FOLP-ex
11:58:39 Session HOL/HOL (main)
11:58:40 Session Doc/Classes (doc)
11:58:40 Session Doc/Codegen_Basics
11:58:40 Session Doc/Codegen (doc)
11:58:40 Session Doc/Corec (doc)
11:58:40 Session Doc/Datatypes (doc)
11:58:40 Session Doc/Functions (doc)
11:58:40 Session HOL/HOL-Algebra (main)
11:58:40 Session HOL/HOL-Analysis (main)
11:58:41 Session HOL/HOL-Analysis-ex
11:58:41 Session HOL/HOL-Probability
11:58:41 Session HOL/HOL-Probability-ex
11:58:41 Session HOL/HOL-Auth
11:58:41 Session HOL/HOL-UNITY
11:58:41 Session HOL/HOL-Bali
11:58:41 Session HOL/HOL-Cardinals
11:58:41 Session HOL/HOL-Corec_Examples
11:58:41 Session HOL/HOL-Data_Structures
11:58:41 Session HOL/HOL-Datatype_Examples
11:58:41 Session HOL/HOL-Decision_Procs
11:58:42 Session HOL/HOL-Eisbach
11:58:42 Session Doc/Eisbach (doc)
11:58:42 Session HOL/HOL-Hahn_Banach
11:58:42 Session HOL/HOL-Hoare
11:58:42 Session HOL/HOL-Hoare_Parallel
11:58:42 Session HOL/HOL-IMP
11:58:42 Session HOL/HOL-IMPP
11:58:42 Session HOL/HOL-IOA
11:58:42 Session HOL/HOL-Imperative_HOL
11:58:42 Session HOL/HOL-Import
11:58:42 Session HOL/HOL-Induct
11:58:42 Session HOL/HOL-Isar_Examples
11:58:43 Session HOL/HOL-Lattice
11:58:43 Session HOL/HOL-Library (main)
11:58:43 Session HOL/HOL-Codegenerator_Test
11:58:43 Session HOL/HOL-Matrix_LP
11:58:43 Session HOL/HOL-Metis_Examples
11:58:43 Session HOL/HOL-MicroJava
11:58:43 Session HOL/HOL-Mirabelle
11:58:43 Session HOL/HOL-Mirabelle-ex
11:58:43 Session HOL/HOL-Mutabelle
11:58:43 Session HOL/HOL-NanoJava
11:58:43 Session HOL/HOL-Nitpick_Examples
11:58:43 Session HOL/HOL-Nominal
11:58:43 Session HOL/HOL-Nominal-Examples
11:58:43 Session HOL/HOL-Nonstandard_Analysis
11:58:43 Session HOL/HOL-Nonstandard_Analysis-Examples
11:58:44 Session HOL/HOL-Number_Theory
11:58:44 Session HOL/HOL-Old_Number_Theory
11:58:44 Session HOL/HOL-Predicate_Compile_Examples
11:58:44 Session HOL/HOL-Prolog
11:58:44 Session HOL/HOL-Quickcheck_Examples
11:58:44 Session HOL/HOL-Quotient_Examples
11:58:44 Session HOL/HOL-SET_Protocol
11:58:44 Session HOL/HOL-Statespace
11:58:44 Session HOL/HOL-TLA
11:58:44 Session HOL/HOL-TLA-Buffer
11:58:44 Session HOL/HOL-TLA-Inc
11:58:44 Session HOL/HOL-TLA-Memory
11:58:44 Session HOL/HOL-TPTP
11:58:44 Session HOL/HOL-Unix
11:58:44 Session HOL/HOL-Word (main)
11:58:45 Session HOL/HOL-SPARK (main)
11:58:45 Session HOL/HOL-SPARK-Examples
11:58:45 Session HOL/HOL-SPARK-Manual
11:58:45 Session HOL/HOL-Word-Examples
11:58:45 Session HOL/HOL-Word-SMT_Examples
11:58:45 Session HOL/HOL-ZF
11:58:45 Session HOL/HOL-ex
11:58:45 Session HOL/HOLCF (main)
11:58:45 Session HOL/HOLCF-FOCUS
11:58:45 Session HOL/HOLCF-IMP
11:58:45 Session HOL/HOLCF-Library
11:58:45 Session HOL/HOLCF-Tutorial
11:58:45 Session HOL/HOLCF-ex
11:58:45 Session HOL/IOA
11:58:45 Session HOL/IOA-ABP
11:58:45 Session HOL/IOA-NTP
11:58:45 Session HOL/IOA-Storage
11:58:45 Session HOL/IOA-ex
11:58:45 Session Doc/How_to_Prove_it
11:58:45 Session Doc/Implementation (doc)
11:58:45 Session Doc/Isar_Ref (doc)
11:58:45 Session Doc/JEdit (doc)
11:58:45 Session Doc/Locales (doc)
11:58:45 Session Doc/Main (doc)
11:58:45 Session Doc/Prog_Prove (doc)
11:58:45 Session Doc/Sugar (doc)
11:58:45 Session Doc/Tutorial (doc)
11:58:45 Session Doc/Typeclass_Hierarchy_Basics
11:58:46 Session Doc/Typeclass_Hierarchy (doc)
11:58:46 Session HOL/HOL-Proofs
11:58:46 Session HOL/HOL-Proofs-Extraction
11:58:46 Session HOL/HOL-Proofs-Lambda
11:58:46 Session HOL/HOL-Proofs-ex
11:58:46 Session Doc/Intro (doc)
11:58:46 Session LCF/LCF
11:58:46 Session Doc/Logics (doc)
11:58:46 Session Doc/Nitpick (doc)
11:58:46 Session Unsorted/SML
11:58:46 Session Sequents/Sequents
11:58:46 Session Doc/Sledgehammer (doc)
11:58:46 Session Unsorted/Spec_Check
11:58:46 Session Doc/System (doc)
11:58:46 Session ZF/ZF (main ZF)
11:58:46 Session Doc/Logics_ZF (doc)
11:58:46 Session ZF/ZF-AC (ZF)
11:58:46 Session ZF/ZF-Coind (ZF)
11:58:46 Session ZF/ZF-Constructible (ZF)
11:58:46 Session ZF/ZF-IMP (ZF)
11:58:46 Session ZF/ZF-Induct (ZF)
11:58:46 Session ZF/ZF-Resid (ZF)
11:58:46 Session ZF/ZF-UNITY (ZF)
11:58:46 Session ZF/ZF-ex (ZF)
11:58:47 Building Pure ...
11:58:58 Pure: theory Pure
11:58:58 Pure: theory ML_Bootstrap
11:59:00 Warning: missing document directory
11:59:00 Timing Pure (2 threads, 0.658s elapsed time, 0.700s cpu time, 0.020s GC time, factor 1.06)
11:59:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Pure/Pure
11:59:00 Finished Pure (0:00:13 elapsed time, 0:00:14 cpu time, factor 1.08)
11:59:01 Building HOL ...
11:59:01 Building ZF ...
11:59:01 Building HOL-Proofs ...
11:59:01 ZF: theory IFOL
11:59:01 HOL-Proofs: theory Proofs
11:59:01 HOL: theory Code_Generator
11:59:01 HOL-Proofs: theory Code_Generator
11:59:02 ZF: theory FOL
11:59:03 ZF: theory ZF
11:59:03 ZF: theory upair
11:59:03 HOL: theory HOL
11:59:03 HOL-Proofs: theory HOL
11:59:04 ZF: theory pair
11:59:04 ZF: theory Bool
11:59:04 ZF: theory equalities
11:59:04 ZF: theory Fixedpt
11:59:04 ZF: theory Sum
11:59:04 ZF: theory func
11:59:05 ZF: theory Perm
11:59:05 ZF: theory QPair
11:59:05 ZF: theory Trancl
11:59:05 ZF: theory EquivClass
11:59:05 ZF: theory WF
11:59:05 ZF: theory Order
11:59:05 ZF: theory Ordinal
11:59:06 ZF: theory OrdQuant
11:59:06 ZF: theory OrderArith
11:59:06 ZF: theory Nat_ZF
11:59:06 ZF: theory Epsilon
11:59:06 ZF: theory OrderType
11:59:06 ZF: theory Inductive_ZF
11:59:06 HOL: theory Ctr_Sugar
11:59:06 HOL: theory Orderings
11:59:07 HOL-Proofs: theory Ctr_Sugar
11:59:07 HOL-Proofs: theory Orderings
11:59:07 ZF: theory Finite
11:59:07 ZF: theory Cardinal
11:59:07 ZF: theory Univ
11:59:07 HOL: theory SAT
11:59:07 HOL-Proofs: theory SAT
11:59:07 ZF: theory Arith
11:59:07 ZF: theory QUniv
11:59:07 ZF: theory Datatype_ZF
11:59:08 ZF: theory ArithSimp
11:59:08 ZF: theory Int_ZF
11:59:08 ZF: theory CardinalArith
11:59:08 HOL: theory Groups
11:59:08 ZF: theory List_ZF
11:59:08 HOL-Proofs: theory Groups
11:59:08 ZF: theory Bin
11:59:09 ZF: theory IntDiv_ZF
11:59:10 ZF: theory Main_ZF
11:59:10 ZF: theory AC
11:59:10 ZF: theory Zorn
11:59:10 ZF: theory Main
11:59:10 ZF: theory Cardinal_AC
11:59:10 ZF: theory InfDatatype
11:59:10 ZF: theory Main_ZFC
11:59:10 HOL: theory Lattices
11:59:11 HOL-Proofs: theory Lattices
11:59:12 HOL: theory Set
11:59:13 HOL: theory Fun
11:59:14 HOL: theory Typedef
11:59:14 HOL: theory Rings
11:59:14 HOL-Proofs: theory Set
11:59:14 HOL: theory Complete_Lattices
11:59:16 HOL-Proofs: theory Fun
11:59:16 HOL-Proofs: theory Typedef
11:59:16 HOL-Proofs: theory Rings
11:59:16 HOL-Proofs: theory Complete_Lattices
11:59:17 HOL: theory Inductive
11:59:18 HOL: theory Product_Type
11:59:19 HOL-Proofs: theory Inductive
11:59:20 HOL: theory Complete_Partial_Order
11:59:20 HOL: theory Sum_Type
11:59:21 HOL-Proofs: theory Product_Type
11:59:22 HOL-Proofs: theory Complete_Partial_Order
11:59:22 HOL: theory Nat
11:59:23 HOL-Proofs: theory Sum_Type
11:59:24 HOL: theory Fields
11:59:24 HOL: theory Meson
11:59:25 HOL: theory ATP
11:59:26 HOL-Proofs: theory Nat
11:59:27 HOL: theory Metis
11:59:28 HOL-Proofs: theory Fields
11:59:28 HOL: theory Finite_Set
11:59:30 HOL: theory Relation
11:59:30 Timing ZF (2 threads, 16.206s elapsed time, 30.216s cpu time, 1.920s GC time, factor 1.86)
11:59:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF
11:59:30 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/document.pdf
11:59:30 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF/outline.pdf
11:59:30 Finished ZF (0:00:28 elapsed time, 0:00:51 cpu time, factor 1.78)
11:59:30 Building FOL ...
11:59:30 FOL: theory IFOL
11:59:31 HOL: theory Transitive_Closure
11:59:31 FOL: theory FOL
11:59:31 HOL-Proofs: theory Meson
11:59:32 HOL-Proofs: theory ATP
11:59:32 HOL: theory Wellfounded
11:59:33 HOL-Proofs: theory Finite_Set
11:59:33 HOL: theory Fun_Def_Base
11:59:33 HOL: theory Hilbert_Choice
11:59:33 HOL: theory Wfrec
11:59:33 HOL: theory Order_Relation
11:59:33 HOL: theory BNF_Wellorder_Relation
11:59:33 HOL: theory Zorn
11:59:34 HOL: theory BNF_Wellorder_Embedding
11:59:34 HOL: theory BNF_Wellorder_Constructions
11:59:34 HOL-Proofs: theory Relation
11:59:35 HOL: theory BNF_Cardinal_Order_Relation
11:59:35 HOL-Proofs: theory Metis
11:59:35 Timing FOL (2 threads, 2.158s elapsed time, 2.432s cpu time, 0.064s GC time, factor 1.13)
11:59:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL
11:59:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/document.pdf
11:59:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL/outline.pdf
11:59:35 Finished FOL (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.32)
11:59:35 Building FOLP ...
11:59:35 FOLP: theory IFOLP
11:59:35 HOL: theory BNF_Cardinal_Arithmetic
11:59:36 HOL-Proofs: theory Transitive_Closure
11:59:36 FOLP: theory FOLP
11:59:36 HOL: theory BNF_Def
11:59:37 HOL-Proofs: theory Wellfounded
11:59:37 Timing FOLP (2 threads, 0.883s elapsed time, 0.884s cpu time, 0.000s GC time, factor 1.00)
11:59:37 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP
11:59:37 Finished FOLP (0:00:01 elapsed time)
11:59:37 Running CCL ...
11:59:37 CCL: theory IFOL
11:59:37 HOL: theory BNF_Composition
11:59:37 HOL: theory Basic_BNFs
11:59:37 HOL-Proofs: theory Fun_Def_Base
11:59:38 HOL-Proofs: theory Hilbert_Choice
11:59:38 CCL: theory FOL
11:59:38 HOL: theory BNF_Fixpoint_Base
11:59:38 HOL-Proofs: theory Wfrec
11:59:39 HOL-Proofs: theory Order_Relation
11:59:39 HOL-Proofs: theory BNF_Wellorder_Relation
11:59:39 HOL-Proofs: theory BNF_Wellorder_Embedding
11:59:39 HOL-Proofs: theory Zorn
11:59:39 HOL-Proofs: theory BNF_Wellorder_Constructions
11:59:39 CCL: theory Set
11:59:40 CCL: theory Lfp
11:59:40 CCL: theory Gfp
11:59:40 CCL: theory CCL
11:59:40 HOL-Proofs: theory BNF_Cardinal_Order_Relation
11:59:40 CCL: theory Term
11:59:40 CCL: theory Trancl
11:59:41 CCL: theory Type
11:59:41 CCL: theory Fix
11:59:41 CCL: theory Hered
11:59:41 HOL: theory BNF_Least_Fixpoint
11:59:41 CCL: theory Wfd
11:59:41 HOL-Proofs: theory BNF_Cardinal_Arithmetic
11:59:41 CCL: theory Nat
11:59:41 CCL: theory List
11:59:42 CCL: theory Flag
11:59:42 CCL: theory Stream
11:59:42 HOL-Proofs: theory BNF_Def
11:59:42 Timing CCL (2 threads, 4.407s elapsed time, 6.224s cpu time, 0.312s GC time, factor 1.41)
11:59:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CCL/CCL
11:59:42 Finished CCL (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.37)
11:59:42 Running CTT ...
11:59:42 CTT: theory CTT
11:59:43 CTT: theory Bool
11:59:43 CTT: theory Elimination
11:59:43 CTT: theory Arith
11:59:43 CTT: theory Equality
11:59:43 CTT: theory Typechecking
11:59:43 HOL: theory Basic_BNF_LFPs
11:59:43 CTT: theory Synthesis
11:59:43 CTT: theory Main
11:59:43 HOL: theory Num
11:59:43 HOL: theory Transfer
11:59:44 HOL-Proofs: theory BNF_Composition
11:59:44 HOL-Proofs: theory Basic_BNFs
11:59:45 HOL-Proofs: theory BNF_Fixpoint_Base
11:59:45 Timing CTT (2 threads, 0.751s elapsed time, 1.088s cpu time, 0.000s GC time, factor 1.45)
11:59:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT
11:59:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/document.pdf
11:59:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/CTT/CTT/outline.pdf
11:59:45 Finished CTT (0:00:02 elapsed time, 0:00:03 cpu time)
11:59:45 Running Cube ...
11:59:45 Cube: theory Cube
11:59:45 Cube: theory Example
11:59:45 Timing Cube (2 threads, 0.253s elapsed time, 0.256s cpu time, 0.000s GC time, factor 1.01)
11:59:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Cube/Cube
11:59:45 Finished Cube (0:00:00 elapsed time)
11:59:45 Running FOL-ex ...
11:59:46 FOL-ex: theory Classical
11:59:46 FOL-ex: theory If
11:59:46 FOL-ex: theory Intro
11:59:46 FOL-ex: theory Miniscope
11:59:46 FOL-ex: theory Nat
11:59:46 FOL-ex: theory Nat_Class
11:59:46 FOL-ex: theory Natural_Numbers
11:59:46 FOL-ex: theory Prolog
11:59:46 FOL-ex: theory Propositional_Cla
11:59:46 FOL-ex: theory Quantifiers_Cla
11:59:46 FOL-ex: theory Foundation
11:59:46 FOL-ex: theory Intuitionistic
11:59:46 FOL-ex: theory Propositional_Int
11:59:46 HOL: theory Power
11:59:46 FOL-ex: theory Quantifiers_Int
11:59:48 HOL-Proofs: theory BNF_Least_Fixpoint
11:59:48 FOL-ex: theory Locale_Test1
11:59:48 HOL: theory Groups_Big
11:59:50 FOL-ex: theory Locale_Test2
11:59:50 FOL-ex: theory Locale_Test3
11:59:50 FOL-ex: theory Locale_Test
11:59:50 HOL-Proofs: theory Basic_BNF_LFPs
11:59:50 HOL: theory Equiv_Relations
11:59:50 HOL-Proofs: theory Num
11:59:50 HOL-Proofs: theory Transfer
11:59:51 HOL: theory Lifting
11:59:52 Timing FOL-ex (2 threads, 4.204s elapsed time, 6.236s cpu time, 0.248s GC time, factor 1.48)
11:59:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex
11:59:52 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/document.pdf
11:59:52 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOL/FOL-ex/outline.pdf
11:59:52 Finished FOL-ex (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.50)
11:59:52 Running FOLP-ex ...
11:59:52 HOL: theory Lifting_Set
11:59:52 HOL: theory Option
11:59:52 FOLP-ex: theory Classical
11:59:52 FOLP-ex: theory If
11:59:52 FOLP-ex: theory Intro
11:59:52 FOLP-ex: theory Nat
11:59:52 HOL: theory Quotient
11:59:52 FOLP-ex: theory Propositional_Cla
11:59:53 FOLP-ex: theory Quantifiers_Cla
11:59:53 HOL: theory Extraction
11:59:53 FOLP-ex: theory Foundation
11:59:53 FOLP-ex: theory Intuitionistic
11:59:54 HOL: theory Lattices_Big
11:59:54 HOL-Proofs: theory Power
11:59:54 FOLP-ex: theory Propositional_Int
11:59:54 FOLP-ex: theory Quantifiers_Int
11:59:55 HOL: theory Partial_Function
11:59:55 Timing FOLP-ex (2 threads, 2.722s elapsed time, 4.808s cpu time, 0.148s GC time, factor 1.77)
11:59:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/FOLP/FOLP-ex
11:59:55 Finished FOLP-ex (0:00:02 elapsed time, 0:00:04 cpu time)
11:59:55 Running Intro ...
11:59:56 HOL: theory Fun_Def
11:59:57 HOL-Proofs: theory Groups_Big
11:59:57 HOL: theory Int
11:59:58 Timing Intro (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)
11:59:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro
11:59:58 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Intro/intro.pdf
11:59:58 Finished Intro (0:00:02 elapsed time)
11:59:58 Running LCF ...
11:59:58 LCF: theory IFOL
11:59:59 LCF: theory FOL
11:59:59 HOL: theory Nat_Transfer
11:59:59 HOL-Proofs: theory Equiv_Relations
11:59:59 HOL: theory Parity
12:00:00 LCF: theory LCF
12:00:00 LCF: theory Ex1
12:00:00 LCF: theory Ex2
12:00:00 LCF: theory Ex3
12:00:00 LCF: theory Ex4
12:00:01 Timing LCF (2 threads, 2.320s elapsed time, 2.652s cpu time, 0.064s GC time, factor 1.14)
12:00:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/LCF/LCF
12:00:01 Finished LCF (0:00:02 elapsed time)
12:00:01 Running Logics ...
12:00:01 HOL: theory Divides
12:00:02 HOL-Proofs: theory Lifting
12:00:04 HOL-Proofs: theory Lifting_Set
12:00:04 HOL-Proofs: theory Option
12:00:04 Timing Logics (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)
12:00:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics
12:00:04 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics/logics.pdf
12:00:04 Finished Logics (0:00:02 elapsed time)
12:00:04 Running Logics_ZF ...
12:00:04 Logics_ZF: theory FOL_examples
12:00:04 Logics_ZF: theory If
12:00:04 Logics_ZF: theory ZF_Isar
12:00:04 Logics_ZF: theory ZF_examples
12:00:04 HOL-Proofs: theory Quotient
12:00:04 Logics_ZF: theory IFOL_examples
12:00:05 HOL-Proofs: theory Lattices_Big
12:00:06 HOL-Proofs: theory Partial_Function
12:00:06 HOL: theory Code_Numeral
12:00:06 HOL-Proofs: theory Fun_Def
12:00:07 HOL: theory Numeral_Simprocs
12:00:08 Timing Logics_ZF (2 threads, 0.341s elapsed time, 0.580s cpu time, 0.000s GC time, factor 1.70)
12:00:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF
12:00:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Logics_ZF/logics-ZF.pdf
12:00:08 Finished Logics_ZF (0:00:03 elapsed time, 0:00:03 cpu time, factor 0.99)
12:00:08 Running Nitpick ...
12:00:08 HOL-Proofs: theory Int
12:00:08 HOL: theory SMT
12:00:10 HOL: theory Semiring_Normalization
12:00:10 Timing Nitpick (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)
12:00:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick
12:00:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Nitpick/nitpick.pdf
12:00:10 Finished Nitpick (0:00:02 elapsed time)
12:00:10 Running SML ...
12:00:10 SML: theory Examples
12:00:10 HOL-Proofs: theory Nat_Transfer
12:00:11 HOL-Proofs: theory Parity
12:00:11 Warning: missing document directory
12:00:11 Timing SML (2 threads, 0.011s elapsed time, 0.012s cpu time, 0.000s GC time, factor 1.12)
12:00:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/SML
12:00:11 Finished SML (0:00:00 elapsed time)
12:00:11 Running Sequents ...
12:00:11 Sequents: theory Sequents
12:00:11 Sequents: theory ILL
12:00:11 Sequents: theory LK0
12:00:11 Sequents: theory ILL_predlog
12:00:11 Sequents: theory Washing
12:00:11 Sequents: theory LK
12:00:11 Sequents: theory Modal0
12:00:11 Sequents: theory S4
12:00:11 Sequents: theory Hard_Quantifiers
12:00:11 Sequents: theory Nat
12:00:11 Sequents: theory Propositional
12:00:11 Sequents: theory Quantifiers
12:00:11 Sequents: theory S43
12:00:11 Sequents: theory T
12:00:12 HOL: theory Groebner_Basis
12:00:12 HOL: theory Set_Interval
12:00:13 HOL-Proofs: theory Divides
12:00:14 Timing Sequents (2 threads, 2.770s elapsed time, 5.360s cpu time, 0.116s GC time, factor 1.93)
12:00:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Sequents/Sequents
12:00:14 Finished Sequents (0:00:02 elapsed time, 0:00:05 cpu time)
12:00:14 Running Sledgehammer ...
12:00:16 Timing Sledgehammer (2 threads, 0.000s elapsed time, 0.000s cpu time, 0.000s GC time, factor 0.00)
12:00:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer
12:00:16 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sledgehammer/sledgehammer.pdf
12:00:16 Finished Sledgehammer (0:00:01 elapsed time)
12:00:16 Running Spec_Check ...
12:00:16 Spec_Check: theory Spec_Check
12:00:16 Spec_Check: theory Examples
12:00:18 Warning: missing document directory
12:00:18 Timing Spec_Check (2 threads, 1.631s elapsed time, 2.756s cpu time, 0.028s GC time, factor 1.69)
12:00:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Unsorted/Spec_Check
12:00:18 Finished Spec_Check (0:00:01 elapsed time)
12:00:18 Running System ...
12:00:18 System: theory Base
12:00:18 System: theory Environment
12:00:18 System: theory Misc
12:00:18 System: theory Presentation
12:00:18 System: theory Scala
12:00:18 System: theory Sessions
12:00:18 HOL-Proofs: theory Code_Numeral
12:00:19 HOL: theory Conditionally_Complete_Lattices
12:00:19 HOL-Proofs: theory Numeral_Simprocs
12:00:20 HOL-Proofs: theory SMT
12:00:20 HOL: theory Filter
12:00:21 Timing System (2 threads, 0.316s elapsed time, 0.308s cpu time, 0.000s GC time, factor 0.98)
12:00:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System
12:00:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/System/system.pdf
12:00:21 Finished System (0:00:02 elapsed time)
12:00:21 Running ZF-AC ...
12:00:21 HOL: theory Presburger
12:00:21 ZF-AC: theory AC_Equiv
12:00:21 ZF-AC: theory AC18_AC19
12:00:21 ZF-AC: theory AC7_AC9
12:00:21 ZF-AC: theory Cardinal_aux
12:00:21 ZF-AC: theory Hartog
12:00:21 ZF-AC: theory HH
12:00:21 ZF-AC: theory WO6_WO1
12:00:21 ZF-AC: theory AC16_lemmas
12:00:22 ZF-AC: theory AC16_WO4
12:00:22 ZF-AC: theory DC
12:00:22 HOL-Proofs: theory Semiring_Normalization
12:00:22 ZF-AC: theory AC15_WO6
12:00:22 ZF-AC: theory AC17_AC1
12:00:22 ZF-AC: theory WO1_AC
12:00:22 ZF-AC: theory WO1_WO7
12:00:22 ZF-AC: theory WO2_AC16
12:00:23 HOL: theory Sledgehammer
12:00:24 HOL-Proofs: theory Groebner_Basis
12:00:25 HOL-Proofs: theory Set_Interval
12:00:25 HOL: theory List
12:00:27 Timing ZF-AC (2 threads, 4.145s elapsed time, 8.056s cpu time, 0.412s GC time, factor 1.94)
12:00:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC
12:00:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/document.pdf
12:00:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-AC/outline.pdf
12:00:27 Finished ZF-AC (0:00:06 elapsed time, 0:00:11 cpu time, factor 1.77)
12:00:27 Running ZF-Coind ...
12:00:27 ZF-Coind: theory Map
12:00:27 ZF-Coind: theory Language
12:00:27 ZF-Coind: theory Types
12:00:28 ZF-Coind: theory Values
12:00:28 ZF-Coind: theory Dynamic
12:00:28 ZF-Coind: theory Static
12:00:28 HOL-Proofs: theory Presburger
12:00:28 ZF-Coind: theory ECR
12:00:28 Timing ZF-Coind (2 threads, 0.618s elapsed time, 1.176s cpu time, 0.048s GC time, factor 1.90)
12:00:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Coind
12:00:28 Finished ZF-Coind (0:00:00 elapsed time)
12:00:28 Running ZF-Constructible ...
12:00:29 ZF-Constructible: theory Formula
12:00:29 ZF-Constructible: theory MetaExists
12:00:29 ZF-Constructible: theory Normal
12:00:29 ZF-Constructible: theory Reflection
12:00:29 ZF-Constructible: theory Relative
12:00:30 HOL-Proofs: theory Sledgehammer
12:00:31 ZF-Constructible: theory L_axioms
12:00:31 ZF-Constructible: theory Wellorderings
12:00:31 ZF-Constructible: theory WFrec
12:00:31 ZF-Constructible: theory WF_absolute
12:00:32 HOL-Proofs: theory List
12:00:32 ZF-Constructible: theory Datatype_absolute
12:00:32 ZF-Constructible: theory Rank
12:00:33 HOL: theory Groups_List
12:00:33 HOL: theory Map
12:00:33 ZF-Constructible: theory Separation
12:00:33 ZF-Constructible: theory Internalize
12:00:33 ZF-Constructible: theory AC_in_L
12:00:33 HOL: theory Enum
12:00:34 HOL: theory Random
12:00:35 ZF-Constructible: theory Rec_Separation
12:00:35 ZF-Constructible: theory Rank_Separation
12:00:35 ZF-Constructible: theory Satisfies_absolute
12:00:36 HOL: theory String
12:00:36 HOL: theory BNF_Greatest_Fixpoint
12:00:36 ZF-Constructible: theory DPow_absolute
12:00:37 HOL: theory Predicate
12:00:38 HOL: theory Lazy_Sequence
12:00:39 HOL: theory Limited_Sequence
12:00:39 HOL: theory Typerep
12:00:40 HOL: theory Code_Evaluation
12:00:42 HOL: theory Quickcheck_Random
12:00:44 HOL: theory Quickcheck_Exhaustive
12:00:44 HOL: theory Quickcheck_Narrowing
12:00:45 Timing ZF-Constructible (2 threads, 11.986s elapsed time, 23.620s cpu time, 3.096s GC time, factor 1.97)
12:00:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible
12:00:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/document.pdf
12:00:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Constructible/outline.pdf
12:00:45 Finished ZF-Constructible (0:00:16 elapsed time, 0:00:31 cpu time, factor 1.91)
12:00:45 Running ZF-IMP ...
12:00:45 ZF-IMP: theory Com
12:00:45 ZF-IMP: theory Denotation
12:00:45 ZF-IMP: theory Equiv
12:00:46 Timing ZF-IMP (2 threads, 0.890s elapsed time, 1.136s cpu time, 0.048s GC time, factor 1.28)
12:00:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-IMP
12:00:46 Finished ZF-IMP (0:00:01 elapsed time)
12:00:46 Running ZF-Induct ...
12:00:47 ZF-Induct: theory Acc
12:00:47 ZF-Induct: theory Binary_Trees
12:00:47 ZF-Induct: theory Comb
12:00:47 ZF-Induct: theory Datatypes
12:00:47 ZF-Induct: theory FoldSet
12:00:47 ZF-Induct: theory ListN
12:00:47 ZF-Induct: theory Mutil
12:00:47 ZF-Induct: theory Ntree
12:00:47 ZF-Induct: theory Multiset
12:00:47 ZF-Induct: theory Primrec
12:00:47 ZF-Induct: theory PropLog
12:00:48 ZF-Induct: theory Rmap
12:00:48 ZF-Induct: theory Term
12:00:48 ZF-Induct: theory Tree_Forest
12:00:48 ZF-Induct: theory Brouwer
12:00:48 HOL: theory Record
12:00:48 HOL: theory Random_Pred
12:00:49 HOL: theory Random_Sequence
12:00:50 HOL: theory Nitpick
12:00:51 HOL: theory Predicate_Compile
12:00:54 Timing ZF-Induct (2 threads, 4.993s elapsed time, 9.264s cpu time, 0.464s GC time, factor 1.86)
12:00:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct
12:00:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/document.pdf
12:00:54 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Induct/outline.pdf
12:00:54 Finished ZF-Induct (0:00:07 elapsed time, 0:00:13 cpu time, factor 1.74)
12:00:54 Running ZF-Resid ...
12:00:55 ZF-Resid: theory Redex
12:00:55 ZF-Resid: theory Substitution
12:00:55 ZF-Resid: theory Residuals
12:00:55 ZF-Resid: theory Reduction
12:00:55 ZF-Resid: theory Confluence
12:00:56 Timing ZF-Resid (2 threads, 1.142s elapsed time, 2.096s cpu time, 0.052s GC time, factor 1.84)
12:00:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-Resid
12:00:56 Finished ZF-Resid (0:00:01 elapsed time)
12:00:56 Running ZF-UNITY ...
12:00:56 HOL: theory Main
12:00:56 ZF-UNITY: theory Acc
12:00:56 ZF-UNITY: theory FoldSet
12:00:56 ZF-UNITY: theory GenPrefix
12:00:56 ZF-UNITY: theory Multiset
12:00:57 ZF-UNITY: theory State
12:00:57 ZF-UNITY: theory UNITY
12:00:57 ZF-UNITY: theory Constrains
12:00:57 ZF-UNITY: theory MultisetSum
12:00:57 ZF-UNITY: theory Monotonicity
12:00:57 ZF-UNITY: theory FP
12:00:57 ZF-UNITY: theory Increasing
12:00:57 ZF-UNITY: theory WFair
12:00:58 ZF-UNITY: theory SubstAx
12:00:58 HOL: theory Archimedean_Field
12:00:58 HOL: theory Binomial
12:00:58 ZF-UNITY: theory Follows
12:00:58 ZF-UNITY: theory Mutex
12:00:58 ZF-UNITY: theory Union
12:00:59 ZF-UNITY: theory Comp
12:00:59 HOL: theory GCD
12:00:59 ZF-UNITY: theory Guar
12:00:59 ZF-UNITY: theory AllocBase
12:00:59 ZF-UNITY: theory ClientImpl
12:01:00 ZF-UNITY: theory AllocImpl
12:01:00 ZF-UNITY: theory Distributor
12:01:00 ZF-UNITY: theory Merge
12:01:03 HOL: theory Topological_Spaces
12:01:04 HOL: theory Rat
12:01:07 HOL: theory Real
12:01:11 Timing ZF-UNITY (2 threads, 14.613s elapsed time, 29.264s cpu time, 1.036s GC time, factor 2.00)
12:01:11 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-UNITY
12:01:11 Finished ZF-UNITY (0:00:14 elapsed time, 0:00:29 cpu time, factor 1.98)
12:01:11 Running ZF-ex ...
12:01:11 HOL: theory Real_Vector_Spaces
12:01:11 ZF-ex: theory BinEx
12:01:11 ZF-ex: theory CoUnit
12:01:11 ZF-ex: theory Commutation
12:01:11 ZF-ex: theory Group
12:01:11 ZF-ex: theory LList
12:01:12 ZF-ex: theory Limit
12:01:12 ZF-ex: theory Ring
12:01:13 ZF-ex: theory NatSum
12:01:13 ZF-ex: theory Primes
12:01:13 ZF-ex: theory Ramsey
12:01:13 ZF-ex: theory misc
12:01:18 Timing ZF-ex (2 threads, 7.110s elapsed time, 13.372s cpu time, 0.628s GC time, factor 1.88)
12:01:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/ZF/ZF-ex
12:01:18 Finished ZF-ex (0:00:07 elapsed time, 0:00:13 cpu time, factor 1.83)
12:01:27 HOL: theory Inequalities
12:01:27 HOL: theory Limits
12:01:31 HOL: theory Deriv
12:01:31 HOL: theory Series
12:01:33 HOL: theory NthRoot
12:01:34 HOL: theory Transcendental
12:01:38 HOL: theory Complex
12:01:38 HOL: theory MacLaurin
12:01:40 HOL: theory Complex_Main
12:05:20 Timing HOL (2 threads, 277.895s elapsed time, 548.164s cpu time, 42.976s GC time, factor 1.97)
12:05:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL
12:05:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/document.pdf
12:05:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL/outline.pdf
12:05:20 Finished HOL (0:06:19 elapsed time, 0:11:54 cpu time, factor 1.88)
12:05:21 Building HOLCF ...
12:05:21 Building HOL-TLA ...
12:05:23 HOL-TLA: theory Intensional
12:05:23 HOLCF: theory Nat_Bijection
12:05:23 HOLCF: theory Old_Datatype
12:05:23 HOL-TLA: theory Stfun
12:05:23 HOL-TLA: theory Action
12:05:24 HOL-TLA: theory Init
12:05:24 HOL-TLA: theory TLA
12:05:24 HOLCF: theory Countable
12:05:26 HOLCF: theory Porder
12:05:26 HOLCF: theory Pcpo
12:05:28 HOLCF: theory Cont
12:05:28 HOLCF: theory Adm
12:05:28 HOLCF: theory Discrete
12:05:28 HOLCF: theory Cpodef
12:05:29 HOLCF: theory Fun_Cpo
12:05:29 HOLCF: theory Product_Cpo
12:05:29 HOLCF: theory Cfun
12:05:29 HOLCF: theory Cprod
12:05:29 HOLCF: theory Fix
12:05:29 HOLCF: theory Sfun
12:05:30 HOLCF: theory Sprod
12:05:30 HOLCF: theory Up
12:05:30 HOLCF: theory Lift
12:05:31 HOLCF: theory One
12:05:31 HOLCF: theory Tr
12:05:31 HOLCF: theory Ssum
12:05:31 HOLCF: theory Plain_HOLCF
12:05:32 HOLCF: theory Deflation
12:05:32 HOLCF: theory Completion
12:05:32 HOLCF: theory Map_Functions
12:05:32 HOLCF: theory Fixrec
12:05:33 HOLCF: theory Bifinite
12:05:33 HOLCF: theory Domain_Aux
12:05:34 HOLCF: theory Universal
12:05:35 HOLCF: theory Algebraic
12:05:35 HOLCF: theory Compact_Basis
12:05:35 HOLCF: theory LowerPD
12:05:35 HOLCF: theory UpperPD
12:05:35 Timing HOL-TLA (2 threads, 1.658s elapsed time, 2.876s cpu time, 0.032s GC time, factor 1.74)
12:05:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA
12:05:35 Finished HOL-TLA (0:00:13 elapsed time, 0:00:20 cpu time, factor 1.46)
12:05:35 Building HOL-Word ...
12:05:36 HOLCF: theory Representable
12:05:36 HOLCF: theory ConvexPD
12:05:37 HOL-Word: theory Bit
12:05:37 HOL-Word: theory Bits
12:05:37 HOL-Word: theory Boolean_Algebra
12:05:38 HOL-Word: theory Bits_Bit
12:05:38 HOL-Word: theory Misc_Numeric
12:05:38 HOL-Word: theory Bit_Representation
12:05:38 HOL-Word: theory Misc_Typedef
12:05:38 HOL-Word: theory Phantom_Type
12:05:38 HOLCF: theory Domain
12:05:38 HOL-Word: theory Bits_Int
12:05:39 HOL-Word: theory Cardinality
12:05:39 HOLCF: theory Powerdomains
12:05:40 HOL-Word: theory Bool_List_Representation
12:05:40 HOL-Word: theory Numeral_Type
12:05:40 HOLCF: theory HOLCF
12:05:41 HOL-Word: theory Type_Length
12:05:41 HOL-Word: theory Word_Miscellaneous
12:05:41 HOL-Word: theory Word
12:06:06 Timing HOLCF (2 threads, 21.049s elapsed time, 40.648s cpu time, 1.640s GC time, factor 1.93)
12:06:06 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF
12:06:06 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/document.pdf
12:06:06 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/outline.pdf
12:06:06 Finished HOLCF (0:00:44 elapsed time, 0:01:15 cpu time, factor 1.72)
12:06:06 Building IOA ...
12:06:08 IOA: theory Asig
12:06:08 IOA: theory Seq
12:06:08 IOA: theory Automata
12:06:09 IOA: theory Sequence
12:06:09 IOA: theory Pred
12:06:10 IOA: theory Traces
12:06:10 IOA: theory TL
12:06:11 IOA: theory CompoExecs
12:06:11 IOA: theory RefMappings
12:06:11 IOA: theory RefCorrectness
12:06:11 IOA: theory CompoScheds
12:06:11 IOA: theory Simulations
12:06:12 IOA: theory SimCorrectness
12:06:12 IOA: theory Deadlock
12:06:12 IOA: theory ShortExecutions
12:06:12 IOA: theory CompoTraces
12:06:13 IOA: theory Compositionality
12:06:13 IOA: theory IOA
12:06:14 IOA: theory TLS
12:06:14 IOA: theory LiveIOA
12:06:15 IOA: theory Abstraction
12:06:15 Timing HOL-Word (2 threads, 19.585s elapsed time, 38.788s cpu time, 1.300s GC time, factor 1.98)
12:06:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word
12:06:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/document.pdf
12:06:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word/outline.pdf
12:06:15 Finished HOL-Word (0:00:39 elapsed time, 0:01:09 cpu time, factor 1.74)
12:06:15 Building HOL-Analysis ...
12:06:17 HOL-Analysis: theory Disjoint_Sets
12:06:17 HOL-Analysis: theory FuncSet
12:06:17 HOL-Analysis: theory Infinite_Set
12:06:18 HOL-Analysis: theory Multiset
12:06:18 HOL-Analysis: theory Nat_Bijection
12:06:18 HOL-Analysis: theory Old_Datatype
12:06:20 HOL-Analysis: theory Countable
12:06:21 HOL-Analysis: theory Countable_Set
12:06:22 HOL-Analysis: theory Countable_Complete_Lattices
12:06:22 HOL-Analysis: theory Permutations
12:06:23 HOL-Analysis: theory Phantom_Type
12:06:24 HOL-Analysis: theory Cardinality
12:06:24 HOL-Analysis: theory Product_plus
12:06:25 HOL-Analysis: theory Numeral_Type
12:06:25 HOL-Analysis: theory Product_Order
12:06:25 HOL-Analysis: theory Set_Algebras
12:06:25 HOL-Analysis: theory L2_Norm
12:06:25 HOL-Analysis: theory Indicator_Function
12:06:26 HOL-Analysis: theory Inner_Product
12:06:26 HOL-Analysis: theory Liminf_Limsup
12:06:27 HOL-Analysis: theory Nonpos_Ints
12:06:27 HOL-Analysis: theory Product_Vector
12:06:27 HOL-Analysis: theory Operator_Norm
12:06:27 HOL-Analysis: theory Order_Continuity
12:06:27 HOL-Analysis: theory Convex
12:06:28 HOL-Analysis: theory Euclidean_Space
12:06:28 HOL-Analysis: theory Extended_Nat
12:06:29 HOL-Analysis: theory Extended_Real
12:06:29 HOL-Analysis: theory Finite_Cartesian_Product
12:06:30 HOL-Analysis: theory Linear_Algebra
12:06:33 HOL-Analysis: theory Extended_Nonnegative_Real
12:06:33 HOL-Analysis: theory Periodic_Fun
12:06:33 HOL-Analysis: theory Poly_Roots
12:06:33 HOL-Analysis: theory Sum_of_Squares
12:06:35 HOL-Analysis: theory Sigma_Algebra
12:06:36 HOL-Analysis: theory Norm_Arith
12:06:36 HOL-Analysis: theory Topology_Euclidean_Space
12:06:38 HOL-Analysis: theory Measurable
12:06:38 HOL-Analysis: theory Measure_Space
12:06:39 Timing IOA (2 threads, 14.834s elapsed time, 29.172s cpu time, 0.868s GC time, factor 1.97)
12:06:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA
12:06:39 Finished IOA (0:00:32 elapsed time, 0:00:55 cpu time, factor 1.69)
12:06:39 Building HOL-SPARK ...
12:06:41 HOL-SPARK: theory Bit_Comparison
12:06:41 HOL-SPARK: theory SPARK_Setup
12:06:41 HOL-Analysis: theory Caratheodory
12:06:41 HOL-Analysis: theory Summation_Tests
12:06:43 HOL-SPARK: theory SPARK
12:06:45 HOL-Analysis: theory Bounded_Linear_Function
12:06:45 HOL-Analysis: theory Convex_Euclidean_Space
12:06:46 HOL-Analysis: theory Extended_Real_Limits
12:06:47 HOL-Analysis: theory Uniform_Limit
12:06:50 HOL-Analysis: theory Continuous_Extension
12:06:50 HOL-Analysis: theory Path_Connected
12:06:53 HOL-Analysis: theory Homeomorphism
12:06:53 HOL-Analysis: theory Weierstrass_Theorems
12:06:54 HOL-Analysis: theory Brouwer_Fixpoint
12:06:55 HOL-Analysis: theory Derivative
12:06:56 Timing HOL-SPARK (2 threads, 2.855s elapsed time, 5.672s cpu time, 0.104s GC time, factor 1.99)
12:06:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK
12:06:56 Finished HOL-SPARK (0:00:16 elapsed time, 0:00:25 cpu time, factor 1.51)
12:06:56 Building Codegen_Basics ...
12:06:57 Codegen_Basics: theory Dlist
12:06:57 Codegen_Basics: theory IArray
12:06:58 HOL-Analysis: theory Henstock_Kurzweil_Integration
12:06:58 Codegen_Basics: theory Mapping
12:06:58 Codegen_Basics: theory RBT_Impl
12:07:02 HOL-Analysis: theory Bounded_Continuous_Function
12:07:02 HOL-Analysis: theory Cartesian_Euclidean_Space
12:07:03 HOL-Analysis: theory Integral_Test
12:07:05 HOL-Analysis: theory Complex_Analysis_Basics
12:07:05 HOL-Analysis: theory Determinants
12:07:06 HOL-Analysis: theory Fashoda_Theorem
12:07:07 HOL-Analysis: theory Ordered_Euclidean_Space
12:07:07 HOL-Analysis: theory Complex_Transcendental
12:07:08 HOL-Analysis: theory Generalised_Binomial_Theorem
12:07:09 HOL-Analysis: theory Polytope
12:07:10 HOL-Analysis: theory Harmonic_Numbers
12:07:10 HOL-Analysis: theory Gamma_Function
12:07:12 HOL-Analysis: theory Borel_Space
12:07:14 HOL-Analysis: theory Cauchy_Integral_Theorem
12:07:15 HOL-Analysis: theory Nonnegative_Lebesgue_Integration
12:07:17 HOL-Analysis: theory Binary_Product_Measure
12:07:18 HOL-Analysis: theory Embed_Measure
12:07:18 HOL-Analysis: theory Finite_Product_Measure
12:07:19 HOL-Analysis: theory Regularity
12:07:20 HOL-Analysis: theory Conformal_Mappings
12:07:20 HOL-Analysis: theory Bochner_Integration
12:07:22 HOL-Analysis: theory Complete_Measure
12:07:22 HOL-Analysis: theory Radon_Nikodym
12:07:23 HOL-Analysis: theory Lebesgue_Measure
12:07:27 Codegen_Basics: theory RBT
12:07:27 HOL-Analysis: theory Set_Integral
12:07:27 Codegen_Basics: theory Setup
12:07:27 HOL-Analysis: theory Interval_Integral
12:07:28 HOL-Analysis: theory Lebesgue_Integral_Substitution
12:07:29 HOL-Analysis: theory Analysis
12:08:15 Timing Codegen_Basics (2 threads, 46.836s elapsed time, 92.504s cpu time, 2.864s GC time, factor 1.98)
12:08:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen_Basics
12:08:15 Finished Codegen_Basics (0:01:18 elapsed time, 0:02:22 cpu time, factor 1.80)
12:08:15 Building HOL-Auth ...
12:08:17 HOL-Auth: theory Message
12:08:17 HOL-Auth: theory Nat_Bijection
12:08:17 HOL-Auth: theory Simps_Case_Conv
12:08:19 HOL-Auth: theory All_Symmetric
12:08:20 HOL-Auth: theory Event
12:08:20 HOL-Auth: theory EventSC
12:08:20 HOL-Auth: theory Extensions
12:08:21 HOL-Auth: theory Analz
12:08:21 HOL-Auth: theory List_Msg
12:08:21 HOL-Auth: theory Guard
12:08:22 HOL-Auth: theory GuardK
12:08:22 HOL-Auth: theory Public
12:08:23 HOL-Auth: theory Shared
12:08:23 HOL-Auth: theory CertifiedEmail
12:08:23 HOL-Auth: theory Guard_Public
12:08:24 HOL-Auth: theory Guard_NS_Public
12:08:24 HOL-Auth: theory P2
12:08:24 HOL-Auth: theory Proto
12:08:25 HOL-Auth: theory KerberosIV
12:08:27 HOL-Auth: theory KerberosIV_Gets
12:08:27 HOL-Auth: theory KerberosV
12:08:28 HOL-Auth: theory Kerberos_BAN
12:08:28 HOL-Auth: theory Kerberos_BAN_Gets
12:08:29 HOL-Auth: theory NS_Public
12:08:29 HOL-Auth: theory NS_Public_Bad
12:08:29 HOL-Auth: theory NS_Shared
12:08:29 HOL-Auth: theory OtwayRees
12:08:30 HOL-Auth: theory OtwayReesBella
12:08:30 HOL-Auth: theory OtwayRees_AN
12:08:30 HOL-Auth: theory OtwayRees_Bad
12:08:31 HOL-Auth: theory P1
12:08:31 HOL-Auth: theory Recur
12:08:32 HOL-Auth: theory WooLam
12:08:32 HOL-Auth: theory Yahalom
12:08:33 HOL-Auth: theory Yahalom2
12:08:33 HOL-Auth: theory Yahalom_Bad
12:08:34 HOL-Auth: theory ZhouGollmann
12:08:34 HOL-Auth: theory Auth_Shared
12:08:35 HOL-Auth: theory Auth_Guard_Public
12:08:36 HOL-Auth: theory Guard_Shared
12:08:36 HOL-Auth: theory Guard_OtwayRees
12:08:36 HOL-Auth: theory Guard_Yahalom
12:08:36 HOL-Auth: theory TLS
12:08:37 HOL-Auth: theory Auth_Guard_Shared
12:08:37 HOL-Auth: theory Smartcard
12:08:37 HOL-Auth: theory ShoupRubin
12:08:38 HOL-Auth: theory Auth_Public
12:08:38 HOL-Auth: theory ShoupRubinBella
12:08:40 HOL-Auth: theory Auth_Smartcard
12:11:01 Timing HOL-Auth (2 threads, 132.576s elapsed time, 260.916s cpu time, 7.944s GC time, factor 1.97)
12:11:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth
12:11:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/document.pdf
12:11:01 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Auth/outline.pdf
12:11:01 Finished HOL-Auth (0:02:45 elapsed time, 0:05:12 cpu time, factor 1.89)
12:11:01 Building HOL-Eisbach ...
12:11:02 HOL-Eisbach: theory Eisbach
12:11:02 HOL-Eisbach: theory IFOL
12:11:03 HOL-Eisbach: theory Eisbach_Old_Appl_Syntax
12:11:03 HOL-Eisbach: theory Eisbach_Tools
12:11:03 HOL-Eisbach: theory Examples
12:11:03 HOL-Eisbach: theory Tests
12:11:04 HOL-Eisbach: theory FOL
12:11:05 HOL-Eisbach: theory Examples_FOL
12:11:17 Warning: missing document directory
12:11:17 Timing HOL-Eisbach (2 threads, 3.809s elapsed time, 7.032s cpu time, 0.224s GC time, factor 1.85)
12:11:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Eisbach
12:11:17 Finished HOL-Eisbach (0:00:15 elapsed time, 0:00:24 cpu time, factor 1.52)
12:11:17 Building HOL-Library ...
12:11:19 HOL-Library: theory Adhoc_Overloading
12:11:19 HOL-Library: theory Lattice_Syntax
12:11:19 HOL-Library: theory Preorder
12:11:19 HOL-Library: theory AList
12:11:19 HOL-Library: theory BNF_Axiomatization
12:11:19 HOL-Library: theory BNF_Corec
12:11:21 HOL-Library: theory DAList
12:11:22 HOL-Library: theory Stirling
12:11:22 HOL-Library: theory Bit
12:11:23 HOL-Library: theory Bits
12:11:23 HOL-Library: theory Bits_Bit
12:11:23 HOL-Library: theory Boolean_Algebra
12:11:24 HOL-Library: theory Cardinal_Notations
12:11:24 HOL-Library: theory Char_ord
12:11:24 HOL-Library: theory Code_Abstract_Nat
12:11:24 HOL-Library: theory Code_Binary_Nat
12:11:24 HOL-Library: theory Code_Target_Nat
12:11:24 HOL-Library: theory Code_Char
12:11:24 HOL-Library: theory Code_Prolog
12:11:24 HOL-Library: theory Code_Test
12:11:25 HOL-Library: theory Combine_PER
12:11:25 HOL-Library: theory Complete_Partial_Order2
12:11:25 HOL-Library: theory Debug
12:11:25 HOL-Library: theory Discrete
12:11:25 HOL-Library: theory Disjoint_Sets
12:11:26 HOL-Library: theory Dlist
12:11:26 HOL-Library: theory FSet
12:11:28 HOL-Library: theory Fraction_Field
12:11:29 HOL-Library: theory Fun_Lexorder
12:11:29 HOL-Library: theory FuncSet
12:11:29 HOL-Library: theory Function_Algebras
12:11:29 HOL-Library: theory Function_Growth
12:11:30 HOL-Library: theory Function_Division
12:11:30 HOL-Library: theory Code_Target_Int
12:11:30 HOL-Library: theory Code_Target_Numeral
12:11:30 HOL-Library: theory Groups_Big_Fun
12:11:30 HOL-Library: theory IArray
12:11:31 HOL-Library: theory Infinite_Set
12:11:31 HOL-Library: theory Omega_Words_Fun
12:11:31 HOL-Library: theory LaTeXsugar
12:11:31 HOL-Library: theory Lattice_Constructions
12:11:31 HOL-Library: theory ListVector
12:11:32 HOL-Library: theory List_lexord
12:11:32 HOL-Library: theory Mapping
12:11:33 HOL-Library: theory AList_Mapping
12:11:33 HOL-Library: theory Misc_Numeric
12:11:33 HOL-Library: theory Bit_Representation
12:11:34 HOL-Library: theory Misc_Typedef
12:11:34 HOL-Library: theory Monad_Syntax
12:11:34 HOL-Library: theory More_List
12:11:34 HOL-Library: theory Bits_Int
12:11:34 HOL-Library: theory Multiset
12:11:35 HOL-Library: theory Nat_Bijection
12:11:36 HOL-Library: theory Stream
12:11:37 HOL-Library: theory Old_Datatype
12:11:38 HOL-Library: theory DAList_Multiset
12:11:38 HOL-Library: theory Factorial_Ring
12:11:38 HOL-Library: theory Multiset_Order
12:11:39 HOL-Library: theory Permutation
12:11:39 HOL-Library: theory Permutations
12:11:40 HOL-Library: theory Countable
12:11:41 HOL-Library: theory Countable_Set
12:11:42 HOL-Library: theory Countable_Complete_Lattices
12:11:44 HOL-Library: theory Countable_Set_Type
12:11:44 HOL-Library: theory Euclidean_Algorithm
12:11:46 HOL-Library: theory Old_Recdef
12:11:47 HOL-Library: theory Option_ord
12:11:47 HOL-Library: theory Parallel
12:11:48 HOL-Library: theory Perm
12:11:49 HOL-Library: theory Phantom_Type
12:11:50 HOL-Library: theory Cardinality
12:11:51 HOL-Library: theory FinFun
12:11:52 HOL-Library: theory Normalized_Fraction
12:11:53 HOL-Library: theory Numeral_Type
12:11:53 HOL-Library: theory Predicate_Compile_Alternative_Defs
12:11:54 HOL-Library: theory Predicate_Compile_Quickcheck
12:11:54 HOL-Library: theory Product_Lexorder
12:11:54 HOL-Library: theory Product_plus
12:11:54 HOL-Library: theory Type_Length
12:11:54 HOL-Library: theory Product_Order
12:11:54 HOL-Library: theory Saturated
12:11:54 HOL-Library: theory Finite_Lattice
12:11:54 HOL-Library: theory Quotient_Syntax
12:11:55 HOL-Library: theory Quotient_Option
12:11:55 HOL-Library: theory Quotient_Product
12:11:55 HOL-Library: theory Quotient_Set
12:11:55 HOL-Library: theory Quotient_List
12:11:55 HOL-Library: theory Quotient_Sum
12:11:55 HOL-Library: theory Quotient_Type
12:11:56 HOL-Library: theory RBT_Impl
12:11:57 HOL-Library: theory Ramsey
12:11:57 HOL-Library: theory Reflection
12:11:58 HOL-Library: theory Refute
12:11:58 HOL-Library: theory Rewrite
12:11:58 HOL-Library: theory Set_Algebras
12:11:59 HOL-Library: theory Simps_Case_Conv
12:11:59 HOL-Library: theory Extended
12:12:01 HOL-Library: theory State_Monad
12:12:01 HOL-Library: theory Sublist
12:12:02 HOL-Library: theory Prefix_Order
12:12:02 HOL-Library: theory Sublist_Order
12:12:02 HOL-Library: theory Polynomial
12:12:07 HOL-Library: theory BigO
12:12:08 HOL-Library: theory Bool_List_Representation
12:12:09 HOL-Library: theory Code_Real_Approx_By_Float
12:12:09 HOL-Library: theory Continuum_Not_Denumerable
12:12:10 HOL-Library: theory Diagonal_Subsequence
12:12:10 HOL-Library: theory Formal_Power_Series
12:12:17 HOL-Library: theory Polynomial_FPS
12:12:18 HOL-Library: theory Fundamental_Theorem_Algebra
12:12:18 HOL-Library: theory Indicator_Function
12:12:19 HOL-Library: theory Inner_Product
12:12:20 HOL-Library: theory Product_Vector
12:12:20 HOL-Library: theory Convex
12:12:21 HOL-Library: theory Lattice_Algebras
12:12:26 HOL-Library: theory Liminf_Limsup
12:12:26 HOL-Library: theory Log_Nat
12:12:27 HOL-Library: theory Float
12:12:29 HOL-Library: theory Lub_Glb
12:12:29 HOL-Library: theory RBT
12:12:29 HOL-Library: theory Nonpos_Ints
12:12:30 HOL-Library: theory OptionalSugar
12:12:30 HOL-Library: theory RBT_Mapping
12:12:30 HOL-Library: theory RBT_Set
12:12:30 HOL-Library: theory Order_Continuity
12:12:31 HOL-Library: theory Extended_Nat
12:12:31 HOL-Library: theory Periodic_Fun
12:12:31 HOL-Library: theory Polynomial_Factorial
12:12:32 HOL-Library: theory Extended_Real
12:12:34 HOL-Library: theory Linear_Temporal_Logic_on_Streams
12:12:35 HOL-Library: theory Extended_Nonnegative_Real
12:12:36 HOL-Library: theory Quadratic_Discriminant
12:12:36 HOL-Library: theory Set_Permutations
12:12:37 HOL-Library: theory Sum_of_Squares
12:12:37 HOL-Library: theory Transitive_Closure_Table
12:12:38 HOL-Library: theory Tree
12:12:39 HOL-Library: theory While_Combinator
12:12:39 HOL-Library: theory Bourbaki_Witt_Fixpoint
12:12:40 HOL-Library: theory Word_Miscellaneous
12:12:40 HOL-Library: theory Word
12:12:40 HOL-Library: theory Tree_Multiset
12:12:41 HOL-Library: theory Library
12:12:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Proofs
12:12:42 HOL-Proofs FAILED
12:12:42 (see also /media/data/jenkins/workspace/isabelle-repo-makeall/heaps/polyml-5.6_x86-linux/log/HOL-Proofs)
12:12:42 ### Linear arithmetic should have refuted the assumptions.
12:12:42 ### Please inform Tobias Nipkow.
12:12:42 Assumptions:
12:12:42 Suc (k + (k + k * k)) \<le> n
12:12:42 m = Suc k
12:12:42 n < Suc k  [n < Suc k]
12:12:42 
12:12:42 Proved:
12:12:42 Suc (Suc (Suc (k + k + 2 * m))) \<le> m + (2 + 2 * k) + m  [n < Suc k]
12:12:42 
12:12:42 ### Linear arithmetic should have refuted the assumptions.
12:12:42 ### Please inform Tobias Nipkow.
12:12:42 Assumptions:
12:12:42 m = Suc k
12:12:42 n < Suc k
12:12:42 Suc (k + (k + k * k)) \<le> n
12:12:42 
12:12:42 Proved:
12:12:42 Suc (Suc (Suc (k + k + 2 * m))) \<le> m + (2 + 2 * k) + m
12:12:42 
12:12:42 ### Linear arithmetic should have refuted the assumptions.
12:12:42 ### Please inform Tobias Nipkow.
12:12:42 Assumptions:
12:12:42 Suc (k + (k + k * k)) \<le> n
12:12:42 True
12:12:42 n < Suc k
12:12:42 
12:12:42 Proved:
12:12:42 Suc (k + k + 2 * n) \<le> n + 2 * k + n
12:12:42 
12:12:42 ### Linear arithmetic should have refuted the assumptions.
12:12:42 ### Please inform Tobias Nipkow.
12:12:42 ### Metis: Unused theorems: "Fun.map_fun_apply"
12:12:42 ### Rule already declared as introduction (intro)
12:12:42 ### ?P ?x \<Longrightarrow> \<exists>x. ?P x
12:12:42 ### Rule already declared as introduction (intro)
12:12:42 ### ?P ?x \<Longrightarrow> \<exists>x. ?P x
12:12:42 ### Rule already declared as introduction (intro)
12:12:42 ### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
12:12:42 *** exception Fail raised (line 83 of "./basis/PolyMLException.sml"): Insufficient memory
12:12:42 Building HOL-Mirabelle ...
12:12:43 HOL-Mirabelle: theory Mirabelle
12:12:44 HOL-Mirabelle: theory Mirabelle_Test
12:12:45 HOL-Library: theory Old_SMT
12:12:52 Timing HOL-Mirabelle (2 threads, 0.721s elapsed time, 1.196s cpu time, 0.008s GC time, factor 1.66)
12:12:52 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle
12:12:52 Finished HOL-Mirabelle (0:00:10 elapsed time, 0:00:14 cpu time, factor 1.38)
12:12:52 Building HOL-Nominal ...
12:12:54 HOL-Nominal: theory Infinite_Set
12:12:54 HOL-Nominal: theory Old_Datatype
12:12:55 HOL-Nominal: theory Nominal
12:13:12 Timing HOL-Nominal (2 threads, 7.038s elapsed time, 14.424s cpu time, 0.588s GC time, factor 2.05)
12:13:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal
12:13:12 Finished HOL-Nominal (0:00:18 elapsed time, 0:00:30 cpu time, factor 1.65)
12:13:12 Building HOL-Nonstandard_Analysis ...
12:13:13 HOL-Nonstandard_Analysis: theory Infinite_Set
12:13:13 HOL-Nonstandard_Analysis: theory Lub_Glb
12:13:14 HOL-Nonstandard_Analysis: theory Free_Ultrafilter
12:13:14 HOL-Nonstandard_Analysis: theory StarDef
12:13:15 HOL-Nonstandard_Analysis: theory HyperNat
12:13:15 HOL-Nonstandard_Analysis: theory HyperDef
12:13:16 HOL-Nonstandard_Analysis: theory NSA
12:13:18 HOL-Nonstandard_Analysis: theory NSComplex
12:13:18 HOL-Nonstandard_Analysis: theory Star
12:13:18 HOL-Nonstandard_Analysis: theory HLim
12:13:19 HOL-Nonstandard_Analysis: theory NatStar
12:13:19 HOL-Nonstandard_Analysis: theory HDeriv
12:13:19 HOL-Nonstandard_Analysis: theory HSEQ
12:13:20 HOL-Nonstandard_Analysis: theory HSeries
12:13:20 HOL-Nonstandard_Analysis: theory HTranscendental
12:13:21 HOL-Nonstandard_Analysis: theory HLog
12:13:21 HOL-Nonstandard_Analysis: theory NSCA
12:13:22 HOL-Nonstandard_Analysis: theory Hyperreal
12:13:22 HOL-Nonstandard_Analysis: theory CStar
12:13:22 HOL-Nonstandard_Analysis: theory CLim
12:13:23 HOL-Nonstandard_Analysis: theory Hypercomplex
12:13:23 HOL-Nonstandard_Analysis: theory Nonstandard_Analysis
12:13:43 Timing HOL-Nonstandard_Analysis (2 threads, 14.131s elapsed time, 28.132s cpu time, 0.760s GC time, factor 1.99)
12:13:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis
12:13:43 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/document.pdf
12:13:43 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis/outline.pdf
12:13:43 Finished HOL-Nonstandard_Analysis (0:00:30 elapsed time, 0:00:52 cpu time, factor 1.71)
12:13:43 Building Typeclass_Hierarchy_Basics ...
12:13:44 Typeclass_Hierarchy_Basics: theory Lattice_Syntax
12:13:44 Typeclass_Hierarchy_Basics: theory Multiset
12:13:48 Typeclass_Hierarchy_Basics: theory Setup
12:14:04 Timing Typeclass_Hierarchy_Basics (2 threads, 8.825s elapsed time, 17.436s cpu time, 0.516s GC time, factor 1.98)
12:14:04 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy_Basics
12:14:04 Finished Typeclass_Hierarchy_Basics (0:00:21 elapsed time, 0:00:35 cpu time, factor 1.65)
12:14:04 Running HOL-Mirabelle-ex ...
12:14:06 HOL-Mirabelle-ex: theory Ex
12:14:12 Timing HOL-Mirabelle-ex (2 threads, 5.620s elapsed time, 0.020s cpu time, 0.000s GC time, factor 0.00)
12:14:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mirabelle-ex
12:14:12 Finished HOL-Mirabelle-ex (0:00:07 elapsed time, 0:00:08 cpu time, factor 1.19)
12:14:12 Running Classes ...
12:14:13 Classes: theory Setup
12:14:14 Classes: theory Classes
12:14:18 Timing Classes (2 threads, 2.377s elapsed time, 3.228s cpu time, 0.052s GC time, factor 1.36)
12:14:18 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes
12:14:18 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Classes/classes.pdf
12:14:18 Finished Classes (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.10)
12:14:18 Running Codegen ...
12:14:20 Codegen: theory Adaptation
12:14:20 Codegen: theory Evaluation
12:14:20 Codegen: theory Further
12:14:20 Codegen: theory Inductive_Predicate
12:14:21 Codegen: theory Introduction
12:14:22 Codegen: theory Refinement
12:14:22 Codegen: theory Foundations
12:14:28 Timing Codegen (2 threads, 4.888s elapsed time, 10.244s cpu time, 0.412s GC time, factor 2.10)
12:14:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen
12:14:28 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Codegen/codegen.pdf
12:14:28 Finished Codegen (0:00:09 elapsed time, 0:00:14 cpu time, factor 1.53)
12:14:28 Running Corec ...
12:14:29 Corec: theory Setup
12:14:30 Corec: theory BNF_Corec
12:14:30 Corec: theory FSet
12:14:34 Corec: theory Corec
12:15:23 Timing Corec (2 threads, 51.185s elapsed time, 76.388s cpu time, 4.280s GC time, factor 1.49)
12:15:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec
12:15:23 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Corec/corec.pdf
12:15:23 Finished Corec (0:00:54 elapsed time, 0:01:19 cpu time, factor 1.45)
12:15:23 Running Datatypes ...
12:15:24 Datatypes: theory Setup
12:15:25 Datatypes: theory BNF_Axiomatization
12:15:25 Datatypes: theory Cardinal_Notations
12:15:25 Datatypes: theory FSet
12:15:25 Datatypes: theory Nat_Bijection
12:15:26 Datatypes: theory Old_Datatype
12:15:27 Datatypes: theory Countable
12:15:28 Datatypes: theory Simps_Case_Conv
12:15:28 Datatypes: theory Datatypes
12:16:08 Timing Datatypes (2 threads, 40.761s elapsed time, 64.484s cpu time, 4.168s GC time, factor 1.58)
12:16:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes
12:16:08 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Datatypes/datatypes.pdf
12:16:08 Finished Datatypes (0:00:45 elapsed time, 0:01:08 cpu time, factor 1.52)
12:16:08 Running Eisbach ...
12:16:10 Eisbach: theory Base
12:16:11 Eisbach: theory Manual
12:16:11 Eisbach: theory Preface
12:16:14 Timing Eisbach (2 threads, 1.892s elapsed time, 2.936s cpu time, 0.024s GC time, factor 1.55)
12:16:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach
12:16:14 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Eisbach/eisbach.pdf
12:16:14 Finished Eisbach (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.14)
12:16:14 Running Functions ...
12:16:15 Functions: theory Functions
12:16:19 Timing Functions (2 threads, 2.456s elapsed time, 4.160s cpu time, 0.192s GC time, factor 1.69)
12:16:19 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions
12:16:19 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Functions/functions.pdf
12:16:19 Finished Functions (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.26)
12:16:19 Running HOL-Algebra ...
12:16:21 HOL-Algebra: theory FuncSet
12:16:21 HOL-Algebra: theory Multiset
12:16:25 HOL-Algebra: theory Factorial_Ring
12:16:25 HOL-Algebra: theory Permutation
12:16:31 HOL-Algebra: theory Euclidean_Algorithm
12:16:39 HOL-Algebra: theory Primes
12:16:47 HOL-Algebra: theory Congruence
12:16:47 HOL-Algebra: theory Exponent
12:16:48 HOL-Algebra: theory Lattice
12:16:50 HOL-Algebra: theory Group
12:16:51 HOL-Algebra: theory Bij
12:16:51 HOL-Algebra: theory Coset
12:16:52 HOL-Algebra: theory FiniteProduct
12:16:53 HOL-Algebra: theory Ring
12:16:53 HOL-Algebra: theory Sylow
12:16:54 HOL-Algebra: theory Divisibility
12:16:56 HOL-Algebra: theory AbelCoset
12:16:57 HOL-Algebra: theory Module
12:17:02 HOL-Algebra: theory Ideal
12:17:05 HOL-Algebra: theory RingHom
12:17:07 HOL-Algebra: theory QuotRing
12:17:07 HOL-Algebra: theory UnivPoly
12:17:08 HOL-Algebra: theory IntRing
12:17:15 Timing HOL-Library (2 threads, 257.318s elapsed time, 505.404s cpu time, 39.776s GC time, factor 1.96)
12:17:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library
12:17:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/document.pdf
12:17:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Library/outline.pdf
12:17:15 Finished HOL-Library (0:05:57 elapsed time, 0:11:06 cpu time, factor 1.86)
12:17:16 Running HOL-Bali ...
12:17:17 HOL-Bali: theory Old_Recdef
12:17:18 HOL-Bali: theory Basis
12:17:19 HOL-Bali: theory Name
12:17:19 HOL-Bali: theory Table
12:17:21 HOL-Bali: theory Type
12:17:22 HOL-Bali: theory Value
12:17:23 HOL-Bali: theory Term
12:17:39 HOL-Bali: theory Decl
12:17:43 HOL-Bali: theory TypeRel
12:17:43 HOL-Bali: theory DeclConcepts
12:17:45 HOL-Bali: theory State
12:17:45 HOL-Bali: theory WellType
12:17:46 Timing HOL-Algebra (2 threads, 81.377s elapsed time, 160.988s cpu time, 6.708s GC time, factor 1.98)
12:17:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra
12:17:46 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/document.pdf
12:17:46 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline.pdf
12:17:46 Finished HOL-Algebra (0:01:26 elapsed time, 0:02:48 cpu time, factor 1.94)
12:17:46 Running HOL-Cardinals ...
12:17:47 HOL-Bali: theory Conform
12:17:47 HOL-Bali: theory Eval
12:17:48 HOL-Cardinals: theory Order_Union
12:17:48 HOL-Cardinals: theory Cardinal_Notations
12:17:48 HOL-Cardinals: theory Fun_More
12:17:48 HOL-Cardinals: theory Order_Relation_More
12:17:48 HOL-Cardinals: theory Wellorder_Extension
12:17:48 HOL-Cardinals: theory Wellfounded_More
12:17:49 HOL-Cardinals: theory Wellorder_Relation
12:17:49 HOL-Cardinals: theory Wellorder_Embedding
12:17:49 HOL-Cardinals: theory Wellorder_Constructions
12:17:49 HOL-Bali: theory DefiniteAssignment
12:17:50 HOL-Cardinals: theory Cardinal_Order_Relation
12:17:50 HOL-Cardinals: theory Ordinal_Arithmetic
12:17:51 HOL-Cardinals: theory Cardinal_Arithmetic
12:17:51 HOL-Cardinals: theory Cardinals
12:17:51 HOL-Cardinals: theory Bounded_Set
12:17:55 HOL-Bali: theory WellForm
12:17:56 HOL-Bali: theory DefiniteAssignmentCorrect
12:17:56 HOL-Bali: theory Example
12:17:57 HOL-Bali: theory TypeSafe
12:18:00 HOL-Bali: theory Evaln
12:18:02 HOL-Bali: theory AxSem
12:18:02 HOL-Bali: theory Trans
12:18:06 HOL-Bali: theory AxCompl
12:18:06 HOL-Bali: theory AxSound
12:18:06 HOL-Bali: theory AxExample
12:19:21 Timing HOL-Analysis (2 threads, 683.642s elapsed time, 1338.476s cpu time, 133.732s GC time, factor 1.96)
12:19:21 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis
12:19:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/document.pdf
12:19:21 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis/outline.pdf
12:19:21 Finished HOL-Analysis (0:13:05 elapsed time, 0:24:55 cpu time, factor 1.90)
12:19:22 Building HOL-Probability ...
12:19:25 HOL-Probability: theory Permutation
12:19:25 HOL-Probability: theory Diagonal_Subsequence
12:19:26 HOL-Probability: theory Lattice_Syntax
12:19:26 HOL-Probability: theory Adhoc_Overloading
12:19:26 HOL-Probability: theory AList
12:19:26 HOL-Probability: theory Complete_Partial_Order2
12:19:27 Timing HOL-Bali (2 threads, 118.904s elapsed time, 230.596s cpu time, 19.132s GC time, factor 1.94)
12:19:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali
12:19:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/document.pdf
12:19:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Bali/outline.pdf
12:19:27 Finished HOL-Bali (0:02:10 elapsed time, 0:04:06 cpu time, factor 1.89)
12:19:27 Running HOL-Analysis-ex ...
12:19:27 HOL-Probability: theory Mapping
12:19:28 HOL-Probability: theory AList_Mapping
12:19:29 HOL-Probability: theory Monad_Syntax
12:19:29 HOL-Probability: theory Stream
12:19:29 HOL-Probability: theory Rewrite
12:19:29 HOL-Probability: theory Sublist
12:19:30 HOL-Analysis-ex: theory Approximations
12:19:30 HOL-Probability: theory Continuum_Not_Denumerable
12:19:30 HOL-Probability: theory Linear_Temporal_Logic_on_Streams
12:19:30 HOL-Probability: theory Set_Permutations
12:19:31 HOL-Probability: theory Fin_Map
12:19:31 HOL-Probability: theory Discrete_Topology
12:19:32 HOL-Probability: theory Probability_Measure
12:19:33 HOL-Probability: theory Distribution_Functions
12:19:33 HOL-Probability: theory Giry_Monad
12:19:34 HOL-Probability: theory Weak_Convergence
12:19:34 HOL-Probability: theory Helly_Selection
12:19:35 HOL-Probability: theory Probability_Mass_Function
12:19:35 HOL-Probability: theory Projective_Family
12:19:36 HOL-Probability: theory Infinite_Product_Measure
12:19:37 HOL-Probability: theory PMF_Impl
12:19:37 HOL-Probability: theory Random_Permutations
12:19:38 HOL-Probability: theory SPMF
12:19:38 HOL-Probability: theory Independent_Family
12:19:40 HOL-Probability: theory Convolution
12:19:40 HOL-Probability: theory Information
12:19:42 HOL-Probability: theory Projective_Limit
12:19:42 HOL-Probability: theory Distributions
12:19:43 HOL-Probability: theory Stream_Space
12:19:44 HOL-Probability: theory Characteristic_Functions
12:19:44 HOL-Probability: theory Sinc_Integral
12:19:44 HOL-Probability: theory Levy
12:19:45 HOL-Probability: theory Central_Limit_Theorem
12:19:45 HOL-Probability: theory Probability
12:19:53 Warning: missing document directory
12:19:53 Timing HOL-Analysis-ex (2 threads, 22.990s elapsed time, 40.212s cpu time, 0.392s GC time, factor 1.75)
12:19:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Analysis-ex
12:19:53 Finished HOL-Analysis-ex (0:00:26 elapsed time, 0:00:43 cpu time, factor 1.66)
12:19:53 Running HOL-Codegenerator_Test ...
12:19:57 HOL-Codegenerator_Test: theory Cmp
12:19:57 HOL-Codegenerator_Test: theory Less_False
12:19:57 HOL-Codegenerator_Test: theory Sorted_Less
12:19:57 HOL-Codegenerator_Test: theory AList_Upd_Del
12:19:58 HOL-Codegenerator_Test: theory List_Ins_Del
12:19:58 HOL-Codegenerator_Test: theory Map_by_Ordered
12:19:58 HOL-Codegenerator_Test: theory Set_by_Ordered
12:19:58 HOL-Codegenerator_Test: theory Primes
12:19:58 HOL-Codegenerator_Test: theory Records
12:19:59 HOL-Codegenerator_Test: theory Eratosthenes
12:19:59 HOL-Codegenerator_Test: theory Tree_Set
12:20:00 HOL-Codegenerator_Test: theory Tree_Map
12:20:02 HOL-Codegenerator_Test: theory Candidates
12:20:05 HOL-Codegenerator_Test: theory Generate
12:20:06 HOL-Codegenerator_Test: theory Generate_Binary_Nat
12:22:55 Timing HOL-Probability (2 threads, 149.565s elapsed time, 290.972s cpu time, 8.724s GC time, factor 1.95)
12:22:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability
12:22:55 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/document.pdf
12:22:55 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability/outline.pdf
12:22:55 Finished HOL-Probability (0:03:33 elapsed time, 0:06:07 cpu time, factor 1.73)
12:22:56 Running HOL-Corec_Examples ...
12:22:57 HOL-Corec_Examples: theory BNF_Corec
12:22:57 HOL-Corec_Examples: theory FSet
12:23:01 HOL-Corec_Examples: theory Nat_Bijection
12:23:01 HOL-Corec_Examples: theory Stream
12:23:03 HOL-Corec_Examples: theory LFilter
12:23:03 HOL-Corec_Examples: theory Simple_Nesting
12:23:06 HOL-Corec_Examples: theory Stream_Processor
12:23:18 HOL-Corec_Examples: theory Paper_Examples
12:24:18 HOL-Codegenerator_Test: theory Generate_Efficient_Datastructures
12:24:25 HOL-Codegenerator_Test: theory Generate_Pretty_Char
12:24:30 HOL-Corec_Examples: theory GPV_Bare_Bones
12:24:30 HOL-Corec_Examples: theory Merge_A
12:24:34 HOL-Corec_Examples: theory Merge_B
12:24:37 HOL-Corec_Examples: theory Merge_C
12:24:40 HOL-Corec_Examples: theory Merge_Poly
12:24:41 HOL-Corec_Examples: theory Merge_D
12:24:48 HOL-Corec_Examples: theory Misc_Mono
12:24:56 Timing HOL-Cardinals (2 threads, 427.412s elapsed time, 414.356s cpu time, 8.948s GC time, factor 0.97)
12:24:56 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Cardinals
12:24:56 Finished HOL-Cardinals (0:07:09 elapsed time, 0:06:55 cpu time, factor 0.97)
12:24:56 Running HOL-Data_Structures ...
12:24:57 HOL-Data_Structures: theory Less_False
12:24:57 HOL-Data_Structures: theory Multiset
12:24:57 HOL-Data_Structures: theory Lattice_Algebras
12:25:01 HOL-Data_Structures: theory Log_Nat
12:25:03 HOL-Data_Structures: theory Float
12:25:22 HOL-Data_Structures: theory Cmp
12:25:22 HOL-Data_Structures: theory Fib
12:25:22 HOL-Data_Structures: theory Sorted_Less
12:25:22 HOL-Data_Structures: theory Tree
12:25:23 HOL-Data_Structures: theory AList_Upd_Del
12:25:23 HOL-Data_Structures: theory Map_by_Ordered
12:25:23 HOL-Corec_Examples: theory Misc_Poly
12:25:23 HOL-Data_Structures: theory List_Ins_Del
12:25:24 HOL-Data_Structures: theory Set_by_Ordered
12:25:24 HOL-Data_Structures: theory Brother12_Set
12:25:26 HOL-Data_Structures: theory Balance
12:25:26 HOL-Data_Structures: theory Splay_Set
12:25:28 HOL-Data_Structures: theory Splay_Map
12:25:29 HOL-Data_Structures: theory Tree_Set
12:25:30 HOL-Data_Structures: theory Tree_Map
12:25:31 HOL-Data_Structures: theory Tree2
12:25:32 HOL-Data_Structures: theory Isin2
12:25:32 HOL-Data_Structures: theory AA_Set
12:25:34 HOL-Data_Structures: theory AVL_Set
12:25:35 HOL-Data_Structures: theory Leftist_Heap
12:25:37 HOL-Data_Structures: theory Lookup2
12:25:37 HOL-Data_Structures: theory AA_Map
12:25:38 HOL-Data_Structures: theory AVL_Map
12:25:39 HOL-Data_Structures: theory RBT
12:25:48 HOL-Data_Structures: theory RBT_Set
12:25:51 HOL-Data_Structures: theory RBT_Map
12:25:55 HOL-Data_Structures: theory Tree23
12:25:58 HOL-Data_Structures: theory Tree23_Set
12:26:09 HOL-Data_Structures: theory Tree23_Map
12:26:13 HOL-Data_Structures: theory Tree234
12:26:15 HOL-Data_Structures: theory Tree234_Set
12:26:35 HOL-Corec_Examples: theory Small_Concrete
12:26:48 HOL-Data_Structures: theory Tree234_Map
12:26:49 HOL-Data_Structures: theory Brother12_Map
12:27:15 HOL-Corec_Examples: theory Stream_Friends
12:27:27 HOL-Corec_Examples: theory TLList_Friends
12:27:32 HOL-Codegenerator_Test: theory Generate_Target_Nat
12:27:46 HOL-Corec_Examples: theory Type_Class
12:28:32 Timing HOL-Corec_Examples (2 threads, 333.702s elapsed time, 536.508s cpu time, 85.772s GC time, factor 1.61)
12:28:32 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Corec_Examples
12:28:32 Finished HOL-Corec_Examples (0:05:35 elapsed time, 0:08:58 cpu time, factor 1.60)
12:28:32 Running HOL-Datatype_Examples ...
12:28:33 HOL-Datatype_Examples: theory BNF_Axiomatization
12:28:33 HOL-Datatype_Examples: theory FSet
12:28:34 HOL-Datatype_Examples: theory Infinite_Set
12:28:35 HOL-Datatype_Examples: theory Lift_BNF
12:28:38 HOL-Datatype_Examples: theory Lambda_Term
12:28:38 HOL-Datatype_Examples: theory Misc_Codatatype
12:28:40 HOL-Datatype_Examples: theory Prelim
12:28:40 HOL-Datatype_Examples: theory DTree
12:28:40 HOL-Datatype_Examples: theory Parallel
12:28:41 HOL-Datatype_Examples: theory TreeFsetI
12:28:41 HOL-Datatype_Examples: theory Gram_Lang
12:28:43 HOL-Datatype_Examples: theory Milner_Tofte
12:28:47 HOL-Datatype_Examples: theory Nat_Bijection
12:28:48 HOL-Datatype_Examples: theory Stream
12:28:49 HOL-Datatype_Examples: theory Process
12:28:54 HOL-Datatype_Examples: theory Stream_Processor
12:28:59 HOL-Datatype_Examples: theory Old_Datatype
12:29:00 HOL-Datatype_Examples: theory Compat
12:29:33 HOL-Datatype_Examples: theory Countable
12:29:35 HOL-Datatype_Examples: theory Misc_Datatype
12:29:52 HOL-Datatype_Examples: theory Misc_Primcorec
12:29:56 HOL-Datatype_Examples: theory TreeFI
12:29:57 HOL-Datatype_Examples: theory Koenig
12:31:38 HOL-Datatype_Examples: theory Misc_Primrec
12:32:07 HOL-Codegenerator_Test: theory Code_Test_GHC
12:32:09 HOL-Codegenerator_Test: theory Code_Test_MLton
12:32:14 HOL-Codegenerator_Test: theory Code_Test_OCaml
12:32:15 HOL-Codegenerator_Test: theory Code_Test_PolyML
12:32:16 HOL-Codegenerator_Test: theory Code_Test_Scala
12:32:29 Timing HOL-Datatype_Examples (2 threads, 234.186s elapsed time, 349.464s cpu time, 67.252s GC time, factor 1.49)
12:32:29 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Datatype_Examples
12:32:29 Finished HOL-Datatype_Examples (0:03:56 elapsed time, 0:06:13 cpu time, factor 1.58)
12:32:29 Running HOL-Decision_Procs ...
12:32:33 HOL-Decision_Procs: theory Code_Abstract_Nat
12:32:33 HOL-Decision_Procs: theory Commutative_Ring
12:32:33 HOL-Decision_Procs: theory Code_Target_Nat
12:32:34 HOL-Decision_Procs: theory DP_Library
12:32:34 HOL-Decision_Procs: theory Dense_Linear_Order
12:32:37 HOL-Decision_Procs: theory Dense_Linear_Order_Ex
12:32:37 HOL-Decision_Procs: theory Code_Target_Int
12:32:37 HOL-Decision_Procs: theory Code_Target_Numeral
12:32:38 HOL-Decision_Procs: theory Old_Recdef
12:32:39 HOL-Decision_Procs: theory Cooper
12:32:39 HOL-Decision_Procs: theory Commutative_Ring_Complete
12:32:40 HOL-Decision_Procs: theory Commutative_Ring_Ex
12:32:40 HOL-Decision_Procs: theory Ferrack
12:32:48 HOL-Codegenerator_Test: theory Code_Test_SMLNJ
12:32:49 Timing HOL-Codegenerator_Test (2 threads, 771.545s elapsed time, 578.876s cpu time, 41.028s GC time, factor 0.75)
12:32:49 Finished HOL-Codegenerator_Test (0:12:55 elapsed time, 0:34:47 cpu time, factor 2.69)
12:32:49 Running HOL-Hahn_Banach ...
12:32:51 HOL-Hahn_Banach: theory Infinite_Set
12:32:51 HOL-Hahn_Banach: theory Nat_Bijection
12:32:51 HOL-Hahn_Banach: theory Old_Datatype
12:32:51 HOL-Hahn_Banach: theory Set_Algebras
12:32:52 HOL-Hahn_Banach: theory Zorn_Lemma
12:32:53 HOL-Hahn_Banach: theory Countable
12:32:54 HOL-Hahn_Banach: theory Countable_Set
12:32:55 HOL-Hahn_Banach: theory Continuum_Not_Denumerable
12:32:55 HOL-Hahn_Banach: theory Bounds
12:32:55 HOL-Hahn_Banach: theory Vector_Space
12:32:56 HOL-Hahn_Banach: theory Linearform
12:32:56 HOL-Hahn_Banach: theory Subspace
12:32:56 HOL-Hahn_Banach: theory Function_Order
12:32:57 HOL-Hahn_Banach: theory Normed_Space
12:32:57 HOL-Hahn_Banach: theory Function_Norm
12:32:57 HOL-Hahn_Banach: theory Hahn_Banach_Ext_Lemmas
12:32:57 HOL-Hahn_Banach: theory Hahn_Banach_Sup_Lemmas
12:32:58 HOL-Hahn_Banach: theory Hahn_Banach_Lemmas
12:32:58 HOL-Hahn_Banach: theory Hahn_Banach
12:33:01 HOL-Decision_Procs: theory Lattice_Algebras
12:33:06 HOL-Decision_Procs: theory Log_Nat
12:33:06 HOL-Decision_Procs: theory MIR
12:33:06 HOL-Decision_Procs: theory Float
12:33:09 HOL-Decision_Procs: theory Approximation
12:33:12 Timing HOL-Hahn_Banach (2 threads, 18.670s elapsed time, 36.944s cpu time, 0.872s GC time, factor 1.98)
12:33:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach
12:33:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/document.pdf
12:33:12 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hahn_Banach/outline.pdf
12:33:12 Finished HOL-Hahn_Banach (0:00:22 elapsed time, 0:00:41 cpu time, factor 1.86)
12:33:12 Running HOL-Hoare ...
12:33:13 HOL-Hoare: theory Heap
12:33:13 HOL-Hoare: theory Arith2
12:33:14 HOL-Hoare: theory Hoare_Logic
12:33:14 HOL-Hoare: theory Hoare_Logic_Abort
12:33:15 HOL-Hoare: theory Examples
12:33:16 HOL-Hoare: theory HeapSyntax
12:33:16 HOL-Hoare: theory Pointer_Examples
12:33:16 HOL-Hoare: theory SchorrWaite
12:33:17 HOL-Hoare: theory Pointers0
12:33:17 HOL-Hoare: theory ExamplesAbort
12:33:18 HOL-Hoare: theory HeapSyntaxAbort
12:33:18 HOL-Hoare: theory Pointer_ExamplesAbort
12:33:18 HOL-Hoare: theory SepLogHeap
12:33:18 HOL-Hoare: theory Separation
12:33:18 HOL-Hoare: theory Hoare
12:33:38 Timing HOL-Hoare (2 threads, 22.286s elapsed time, 44.568s cpu time, 1.064s GC time, factor 2.00)
12:33:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare
12:33:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/document.pdf
12:33:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare/outline.pdf
12:33:38 Finished HOL-Hoare (0:00:26 elapsed time, 0:00:49 cpu time, factor 1.90)
12:33:38 Running HOL-Hoare_Parallel ...
12:33:40 HOL-Hoare_Parallel: theory Graph
12:33:40 HOL-Hoare_Parallel: theory OG_Com
12:33:41 HOL-Hoare_Parallel: theory Quote_Antiquote
12:33:41 HOL-Hoare_Parallel: theory RG_Com
12:33:42 HOL-Hoare_Parallel: theory RG_Tran
12:33:43 HOL-Hoare_Parallel: theory OG_Tran
12:33:44 HOL-Hoare_Parallel: theory RG_Hoare
12:33:44 HOL-Hoare_Parallel: theory OG_Hoare
12:33:45 HOL-Hoare_Parallel: theory RG_Syntax
12:33:45 HOL-Hoare_Parallel: theory OG_Tactics
12:33:45 HOL-Hoare_Parallel: theory RG_Examples
12:33:45 HOL-Hoare_Parallel: theory OG_Syntax
12:33:46 HOL-Decision_Procs: theory Polynomial_List
12:33:46 HOL-Hoare_Parallel: theory Gar_Coll
12:33:48 HOL-Hoare_Parallel: theory Mul_Gar_Coll
12:33:48 HOL-Hoare_Parallel: theory OG_Examples
12:33:52 HOL-Hoare_Parallel: theory Hoare_Parallel
12:33:57 HOL-Decision_Procs: theory Rat_Pair
12:33:57 HOL-Decision_Procs: theory Approximation_Ex
12:33:57 HOL-Decision_Procs: theory Approximation_Quickcheck_Ex
12:33:57 HOL-Decision_Procs: theory Reflected_Multivariate_Polynomial
12:34:06 HOL-Decision_Procs: theory Parametric_Ferrante_Rackoff
12:34:30 Timing HOL-Data_Structures (2 threads, 569.064s elapsed time, 958.508s cpu time, 41.704s GC time, factor 1.68)
12:34:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures
12:34:30 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Data_Structures/document.pdf
12:34:30 Finished HOL-Data_Structures (0:09:33 elapsed time, 0:16:03 cpu time, factor 1.68)
12:34:30 Running HOL-IMP ...
12:34:32 HOL-IMP: theory List_lexord
12:34:32 HOL-IMP: theory Char_ord
12:34:32 HOL-IMP: theory Quotient_Syntax
12:34:32 HOL-IMP: theory Simps_Case_Conv
12:34:32 HOL-IMP: theory Quotient_Option
12:34:32 HOL-IMP: theory Quotient_Product
12:34:32 HOL-IMP: theory Quotient_Set
12:34:32 HOL-IMP: theory Extended
12:34:32 HOL-IMP: theory Quotient_List
12:34:33 HOL-IMP: theory While_Combinator
12:34:37 HOL-IMP: theory AExp
12:34:37 HOL-IMP: theory C_like
12:34:39 HOL-IMP: theory ASM
12:34:40 HOL-IMP: theory BExp
12:34:41 HOL-IMP: theory Complete_Lattice
12:34:41 HOL-IMP: theory Com
12:34:41 HOL-IMP: theory Procs
12:34:42 HOL-IMP: theory ACom
12:34:43 HOL-IMP: theory ACom_ITP
12:34:45 HOL-IMP: theory Abs_Int_Tests
12:34:46 HOL-IMP: theory Big_Step
12:34:46 HOL-IMP: theory Vars
12:34:46 HOL-IMP: theory Denotational
12:34:46 HOL-Decision_Procs: theory Decision_Procs
12:34:46 HOL-IMP: theory Hoare
12:34:47 HOL-IMP: theory Sec_Type_Expr
12:34:47 HOL-IMP: theory Hoare_Examples
12:34:47 HOL-IMP: theory Hoare_Total
12:34:47 HOL-IMP: theory Hoare_Sound_Complete
12:34:47 HOL-IMP: theory Hoare_Total_EX
12:34:47 HOL-IMP: theory VCG
12:34:47 HOL-IMP: theory VCG_Total_EX
12:34:49 HOL-IMP: theory Sec_Typing
12:34:49 HOL-IMP: theory Sec_TypingT
12:34:49 HOL-IMP: theory Sem_Equiv
12:34:49 HOL-IMP: theory Def_Init
12:34:49 HOL-IMP: theory Def_Init_Exp
12:34:49 HOL-IMP: theory Fold
12:34:49 HOL-IMP: theory Def_Init_Big
12:34:50 HOL-IMP: theory Live
12:34:50 HOL-IMP: theory Procs_Dyn_Vars_Dyn
12:34:51 HOL-IMP: theory Procs_Stat_Vars_Dyn
12:34:51 HOL-IMP: theory Procs_Stat_Vars_Stat
12:34:52 HOL-IMP: theory Collecting
12:34:53 HOL-IMP: theory Collecting1
12:34:53 HOL-IMP: theory Collecting_Examples
12:34:53 HOL-IMP: theory Complete_Lattice_ix
12:34:53 HOL-IMP: theory Collecting_ITP
12:34:56 HOL-IMP: theory OO
12:34:58 HOL-IMP: theory Star
12:34:58 HOL-IMP: theory Compiler
12:35:02 HOL-IMP: theory Compiler2
12:35:03 HOL-IMP: theory Def_Init_Small
12:35:04 HOL-IMP: theory Small_Step
12:35:05 HOL-IMP: theory Finite_Reachable
12:35:05 HOL-IMP: theory Types
12:35:07 HOL-IMP: theory Abs_Int0_ITP
12:35:09 HOL-IMP: theory Poly_Types
12:35:10 HOL-IMP: theory Abs_Int_init
12:35:11 HOL-IMP: theory Abs_Int0
12:35:12 HOL-IMP: theory Abs_State_ITP
12:35:13 HOL-IMP: theory Abs_State
12:35:13 HOL-IMP: theory Abs_Int1_ITP
12:35:13 HOL-IMP: theory Abs_Int1
12:35:14 HOL-IMP: theory Abs_Int1_const_ITP
12:35:14 HOL-IMP: theory Abs_Int1_parity_ITP
12:35:15 HOL-IMP: theory Abs_Int2_ITP
12:35:15 HOL-IMP: theory Abs_Int1_const
12:35:16 HOL-IMP: theory Abs_Int1_parity
12:35:17 HOL-IMP: theory Abs_Int2_ivl_ITP
12:35:17 HOL-IMP: theory Abs_Int2
12:35:19 HOL-IMP: theory Abs_Int2_ivl
12:35:19 HOL-IMP: theory Abs_Int3_ITP
12:35:21 HOL-IMP: theory Abs_Int3
12:35:23 HOL-IMP: theory Live_True
12:36:35 Timing HOL-Hoare_Parallel (2 threads, 170.822s elapsed time, 331.020s cpu time, 5.052s GC time, factor 1.94)
12:36:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel
12:36:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/document.pdf
12:36:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Hoare_Parallel/outline.pdf
12:36:35 Finished HOL-Hoare_Parallel (0:02:56 elapsed time, 0:05:38 cpu time, factor 1.92)
12:36:35 Running HOL-IMPP ...
12:36:36 HOL-IMPP: theory Com
12:36:38 HOL-IMPP: theory Natural
12:36:38 HOL-IMPP: theory Hoare
12:36:39 HOL-IMPP: theory Misc
12:36:40 HOL-IMPP: theory EvenOdd
12:36:41 Timing HOL-IMPP (2 threads, 4.031s elapsed time, 7.252s cpu time, 0.340s GC time, factor 1.80)
12:36:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMPP
12:36:41 Finished HOL-IMPP (0:00:05 elapsed time, 0:00:08 cpu time, factor 1.56)
12:36:41 Running HOL-IOA ...
12:36:42 HOL-IOA: theory Asig
12:36:42 HOL-IOA: theory IOA
12:36:43 HOL-IOA: theory Solve
12:36:45 Timing HOL-IOA (2 threads, 2.461s elapsed time, 4.136s cpu time, 0.084s GC time, factor 1.68)
12:36:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IOA
12:36:45 Finished HOL-IOA (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.39)
12:36:45 Running HOL-Imperative_HOL ...
12:36:47 HOL-Imperative_HOL: theory Adhoc_Overloading
12:36:47 HOL-Imperative_HOL: theory LaTeXsugar
12:36:47 HOL-Imperative_HOL: theory Monad_Syntax
12:36:47 HOL-Imperative_HOL: theory Nat_Bijection
12:36:47 HOL-Imperative_HOL: theory Old_Datatype
12:36:48 HOL-Imperative_HOL: theory Countable
12:36:50 HOL-Imperative_HOL: theory Code_Abstract_Nat
12:36:50 HOL-Imperative_HOL: theory Code_Target_Int
12:36:50 HOL-Imperative_HOL: theory Code_Target_Nat
12:36:51 HOL-Imperative_HOL: theory Multiset
12:36:51 HOL-Imperative_HOL: theory Code_Target_Numeral
12:36:51 HOL-Imperative_HOL: theory Heap
12:36:52 HOL-Imperative_HOL: theory Heap_Monad
12:36:55 HOL-Imperative_HOL: theory Array
12:36:55 HOL-Imperative_HOL: theory List_Sublist
12:36:55 HOL-Imperative_HOL: theory Ref
12:36:55 HOL-Imperative_HOL: theory Subarray
12:36:56 HOL-Imperative_HOL: theory Imperative_HOL
12:36:56 HOL-Imperative_HOL: theory RBT_Impl
12:36:56 HOL-Imperative_HOL: theory Linked_Lists
12:37:31 HOL-Imperative_HOL: theory Overview
12:37:32 HOL-Imperative_HOL: theory Imperative_Quicksort
12:37:32 HOL-Imperative_HOL: theory Imperative_Reverse
12:38:07 HOL-Imperative_HOL: theory Sorted_List
12:38:08 HOL-Imperative_HOL: theory SatChecker
12:38:19 HOL-Imperative_HOL: theory Imperative_HOL_ex
12:39:05 Timing HOL-IMP (2 threads, 268.022s elapsed time, 456.716s cpu time, 40.040s GC time, factor 1.70)
12:39:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP
12:39:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-IMP/document.pdf
12:39:05 Finished HOL-IMP (0:04:34 elapsed time, 0:07:44 cpu time, factor 1.69)
12:39:05 Running HOL-Import ...
12:39:06 HOL-Import: theory Import_Setup
12:39:07 HOL-Import: theory HOL_Light_Maps
12:39:08 Warning: missing document directory
12:39:08 Skipping theories "HOL_Light_Import" (undefined HOL_LIGHT_BUNDLE)
12:39:08 Timing HOL-Import (2 threads, 0.977s elapsed time, 2.080s cpu time, 0.020s GC time, factor 2.13)
12:39:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Import
12:39:08 Finished HOL-Import (0:00:02 elapsed time, 0:00:03 cpu time)
12:39:08 Running HOL-Induct ...
12:39:09 HOL-Induct: theory Old_Datatype
12:39:11 HOL-Induct: theory Common_Patterns
12:39:13 HOL-Induct: theory Com
12:39:13 HOL-Induct: theory ABexp
12:39:15 HOL-Induct: theory Comb
12:39:15 HOL-Induct: theory Nested_Datatype
12:39:16 HOL-Induct: theory Sexp
12:39:16 HOL-Induct: theory SList
12:39:17 HOL-Induct: theory Ordinals
12:39:17 HOL-Induct: theory PropLog
12:39:17 HOL-Induct: theory QuoDataType
12:39:18 HOL-Induct: theory QuoNestedDataType
12:39:19 HOL-Induct: theory Sigma_Algebra
12:39:19 HOL-Induct: theory Term
12:39:20 HOL-Induct: theory Tree
12:39:27 Timing HOL-Induct (2 threads, 15.666s elapsed time, 30.392s cpu time, 2.316s GC time, factor 1.94)
12:39:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct
12:39:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/document.pdf
12:39:27 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Induct/outline.pdf
12:39:27 Finished HOL-Induct (0:00:19 elapsed time, 0:00:35 cpu time, factor 1.82)
12:39:27 Running HOL-Isar_Examples ...
12:39:29 HOL-Isar_Examples: theory Lattice_Syntax
12:39:29 HOL-Isar_Examples: theory Multiset
12:39:33 HOL-Isar_Examples: theory Factorial_Ring
12:39:38 Timing HOL-Imperative_HOL (2 threads, 169.808s elapsed time, 186.288s cpu time, 6.124s GC time, factor 1.10)
12:39:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL
12:39:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/document.pdf
12:39:38 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Imperative_HOL/outline.pdf
12:39:38 Finished HOL-Imperative_HOL (0:02:52 elapsed time, 0:07:50 cpu time, factor 2.72)
12:39:38 Running HOL-Lattice ...
12:39:39 HOL-Isar_Examples: theory Euclidean_Algorithm
12:39:40 HOL-Lattice: theory Orders
12:39:41 HOL-Lattice: theory Bounds
12:39:41 HOL-Lattice: theory Lattice
12:39:41 HOL-Lattice: theory CompleteLattice
12:39:46 Timing HOL-Lattice (2 threads, 4.468s elapsed time, 8.828s cpu time, 0.044s GC time, factor 1.98)
12:39:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice
12:39:46 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/document.pdf
12:39:46 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Lattice/outline.pdf
12:39:46 Finished HOL-Lattice (0:00:07 elapsed time, 0:00:12 cpu time, factor 1.65)
12:39:46 Running HOL-Matrix_LP ...
12:39:48 HOL-Isar_Examples: theory Primes
12:39:48 HOL-Matrix_LP: theory Compute_Oracle
12:39:48 HOL-Matrix_LP: theory Lattice_Algebras
12:39:48 HOL-Matrix_LP: theory ComputeHOL
12:39:53 HOL-Matrix_LP: theory ComputeFloat
12:39:54 HOL-Matrix_LP: theory ComputeNumeral
12:39:54 HOL-Matrix_LP: theory LP
12:39:54 HOL-Matrix_LP: theory Matrix
12:39:56 HOL-Matrix_LP: theory SparseMatrix
12:39:58 Timing HOL-Decision_Procs (2 threads, 444.448s elapsed time, 809.444s cpu time, 41.472s GC time, factor 1.82)
12:39:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Decision_Procs
12:39:58 Finished HOL-Decision_Procs (0:07:28 elapsed time, 0:13:31 cpu time, factor 1.81)
12:39:58 Running HOL-Metis_Examples ...
12:39:58 HOL-Matrix_LP: theory Cplex
12:39:58 HOL-Isar_Examples: theory First_Order_Logic
12:39:58 HOL-Isar_Examples: theory Basic_Logic
12:39:58 HOL-Isar_Examples: theory Cantor
12:39:59 HOL-Isar_Examples: theory Drinker
12:39:59 HOL-Isar_Examples: theory Expr_Compiler
12:39:59 HOL-Isar_Examples: theory Group
12:39:59 HOL-Isar_Examples: theory Group_Context
12:39:59 HOL-Isar_Examples: theory Group_Notepad
12:39:59 HOL-Metis_Examples: theory Binary_Tree
12:39:59 HOL-Metis_Examples: theory Dense_Linear_Order
12:40:00 HOL-Isar_Examples: theory Hoare
12:40:00 HOL-Isar_Examples: theory Knaster_Tarski
12:40:00 HOL-Isar_Examples: theory Fibonacci
12:40:00 HOL-Isar_Examples: theory Mutilated_Checkerboard
12:40:01 HOL-Isar_Examples: theory Peirce
12:40:01 HOL-Isar_Examples: theory Puzzle
12:40:01 HOL-Isar_Examples: theory Hoare_Ex
12:40:01 HOL-Isar_Examples: theory Schroeder_Bernstein
12:40:01 HOL-Metis_Examples: theory FuncSet
12:40:01 HOL-Isar_Examples: theory Structured_Statements
12:40:01 HOL-Metis_Examples: theory Abstraction
12:40:01 HOL-Isar_Examples: theory Summation
12:40:01 HOL-Isar_Examples: theory Higher_Order_Logic
12:40:02 HOL-Metis_Examples: theory Function_Algebras
12:40:02 HOL-Metis_Examples: theory Message
12:40:02 HOL-Metis_Examples: theory Set_Algebras
12:40:02 HOL-Metis_Examples: theory Big_O
12:40:03 HOL-Metis_Examples: theory Sets
12:40:03 HOL-Metis_Examples: theory Tarski
12:40:04 HOL-Metis_Examples: theory Clausification
12:40:04 HOL-Metis_Examples: theory Trans_Closure
12:40:04 HOL-Metis_Examples: theory Type_Encodings
12:40:05 HOL-Metis_Examples: theory Proxies
12:40:09 Timing HOL-Isar_Examples (2 threads, 37.557s elapsed time, 74.976s cpu time, 1.848s GC time, factor 2.00)
12:40:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples
12:40:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/document.pdf
12:40:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Isar_Examples/outline.pdf
12:40:09 Finished HOL-Isar_Examples (0:00:41 elapsed time, 0:01:19 cpu time, factor 1.93)
12:40:09 Running HOL-MicroJava ...
12:40:10 HOL-MicroJava: theory While_Combinator
12:40:10 Timing HOL-Matrix_LP (2 threads, 19.919s elapsed time, 37.848s cpu time, 1.012s GC time, factor 1.90)
12:40:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP
12:40:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/document.pdf
12:40:10 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Matrix_LP/outline.pdf
12:40:10 Finished HOL-Matrix_LP (0:00:23 elapsed time, 0:00:42 cpu time, factor 1.80)
12:40:10 Running HOL-Mutabelle ...
12:40:12 HOL-Mutabelle: theory Refute
12:40:12 HOL-MicroJava: theory Eisbach
12:40:12 HOL-MicroJava: theory Transitive_Closure_Table
12:40:13 HOL-Mutabelle: theory MutabelleExtra
12:40:13 HOL-MicroJava: theory Semilat
12:40:13 HOL-MicroJava: theory JBasis
12:40:13 HOL-MicroJava: theory AuxLemmas
12:40:13 HOL-MicroJava: theory Type
12:40:13 HOL-MicroJava: theory Err
12:40:13 Timing HOL-Mutabelle (2 threads, 1.289s elapsed time, 2.296s cpu time, 0.048s GC time, factor 1.78)
12:40:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Mutabelle
12:40:13 Finished HOL-Mutabelle (0:00:02 elapsed time, 0:00:03 cpu time)
12:40:13 Running HOL-NanoJava ...
12:40:14 HOL-MicroJava: theory Listn
12:40:15 HOL-MicroJava: theory Typing_Framework
12:40:15 HOL-MicroJava: theory Opt
12:40:15 HOL-MicroJava: theory Product
12:40:15 HOL-NanoJava: theory Term
12:40:15 HOL-MicroJava: theory SemilatAlg
12:40:15 HOL-MicroJava: theory Decl
12:40:15 HOL-MicroJava: theory SystemClasses
12:40:15 HOL-MicroJava: theory TypeRel
12:40:15 HOL-MicroJava: theory Value
12:40:16 HOL-MicroJava: theory WellForm
12:40:16 HOL-MicroJava: theory State
12:40:17 HOL-MicroJava: theory Exceptions
12:40:17 HOL-MicroJava: theory Term
12:40:17 HOL-MicroJava: theory Kildall
12:40:17 HOL-NanoJava: theory Decl
12:40:17 HOL-MicroJava: theory LBVSpec
12:40:18 HOL-MicroJava: theory LBVComplete
12:40:18 HOL-NanoJava: theory TypeRel
12:40:18 HOL-NanoJava: theory State
12:40:18 HOL-MicroJava: theory LBVCorrect
12:40:19 HOL-MicroJava: theory Typing_Framework_err
12:40:19 HOL-MicroJava: theory Abstract_BV
12:40:19 HOL-NanoJava: theory AxSem
12:40:19 HOL-NanoJava: theory OpSem
12:40:19 HOL-MicroJava: theory Semilattices
12:40:19 HOL-MicroJava: theory JType
12:40:19 HOL-NanoJava: theory Equivalence
12:40:20 HOL-NanoJava: theory Example
12:40:20 HOL-MicroJava: theory JVMType
12:40:20 HOL-MicroJava: theory WellType
12:40:21 HOL-MicroJava: theory Conform
12:40:21 HOL-MicroJava: theory Eval
12:40:21 HOL-MicroJava: theory JVMState
12:40:21 HOL-MicroJava: theory JVMInstructions
12:40:23 Timing HOL-NanoJava (2 threads, 5.671s elapsed time, 10.296s cpu time, 0.528s GC time, factor 1.82)
12:40:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava
12:40:23 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/document.pdf
12:40:23 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-NanoJava/outline.pdf
12:40:23 Finished HOL-NanoJava (0:00:08 elapsed time, 0:00:14 cpu time, factor 1.61)
12:40:23 Running HOL-Nitpick_Examples ...
12:40:23 HOL-MicroJava: theory JVMExceptions
12:40:23 HOL-MicroJava: theory JVMExecInstr
12:40:23 HOL-MicroJava: theory JVMExec
12:40:24 HOL-MicroJava: theory DefsComp
12:40:24 HOL-Nitpick_Examples: theory Core_Nits
12:40:24 HOL-Nitpick_Examples: theory Datatype_Nits
12:40:24 HOL-MicroJava: theory Index
12:40:24 HOL-MicroJava: theory JVMDefensive
12:40:25 HOL-MicroJava: theory JVMListExample
12:40:25 HOL-Nitpick_Examples: theory Hotel_Nits
12:40:25 HOL-MicroJava: theory Example
12:40:25 HOL-Nitpick_Examples: theory Induct_Nits
12:40:26 HOL-MicroJava: theory JListExample
12:40:26 HOL-Nitpick_Examples: theory Integer_Nits
12:40:26 HOL-Nitpick_Examples: theory Mini_Nits
12:40:26 HOL-MicroJava: theory JTypeSafe
12:40:27 HOL-Nitpick_Examples: theory Mono_Nits
12:40:27 HOL-MicroJava: theory TypeInf
12:40:27 HOL-MicroJava: theory Effect
12:40:27 HOL-Nitpick_Examples: theory Pattern_Nits
12:40:27 HOL-MicroJava: theory TranslCompTp
12:40:27 HOL-Nitpick_Examples: theory Quotient_Syntax
12:40:27 HOL-Nitpick_Examples: theory Quotient_Product
12:40:27 HOL-Nitpick_Examples: theory Manual_Nits
12:40:27 HOL-Nitpick_Examples: theory Record_Nits
12:40:28 HOL-MicroJava: theory TranslComp
12:40:28 HOL-MicroJava: theory LemmasComp
12:40:28 HOL-Nitpick_Examples: theory Refute_Nits
12:40:28 HOL-MicroJava: theory CorrComp
12:40:32 HOL-Nitpick_Examples: theory Special_Nits
12:40:33 HOL-Nitpick_Examples: theory Tests_Nits
12:40:34 HOL-Nitpick_Examples: theory Typedef_Nits
12:40:38 HOL-Nitpick_Examples: theory Nitpick_Examples
12:40:40 Timing HOL-Metis_Examples (2 threads, 39.692s elapsed time, 61.240s cpu time, 3.064s GC time, factor 1.54)
12:40:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Metis_Examples
12:40:40 Finished HOL-Metis_Examples (0:00:41 elapsed time, 0:01:15 cpu time, factor 1.83)
12:40:40 Running HOL-Nominal-Examples ...
12:40:41 HOL-Nominal-Examples: theory CK_Machine
12:40:41 HOL-Nominal-Examples: theory CR_Takahashi
12:40:44 HOL-Nominal-Examples: theory Class1
12:40:49 HOL-MicroJava: theory BVSpec
12:40:49 HOL-MicroJava: theory EffectMono
12:40:49 HOL-MicroJava: theory Altern
12:40:49 HOL-MicroJava: theory Correct
12:40:49 HOL-MicroJava: theory Typing_Framework_JVM
12:40:50 HOL-MicroJava: theory BVSpecTypeSafe
12:40:50 HOL-MicroJava: theory JVM
12:40:50 HOL-MicroJava: theory CorrCompTp
12:40:51 HOL-MicroJava: theory BVNoTypeError
12:40:51 HOL-MicroJava: theory BVExample
12:40:52 HOL-MicroJava: theory LBVJVM
12:40:53 HOL-MicroJava: theory MicroJava
12:40:53 HOL-Nominal-Examples: theory Compile
12:41:09 HOL-Nominal-Examples: theory Contexts
12:41:12 HOL-Nominal-Examples: theory Crary
12:41:17 HOL-Nominal-Examples: theory Fsub
12:41:24 HOL-Nominal-Examples: theory Height
12:41:27 HOL-Nominal-Examples: theory Lam_Funs
12:41:30 HOL-Nominal-Examples: theory CR
12:41:30 HOL-Nominal-Examples: theory SN
12:41:32 HOL-Nominal-Examples: theory Lambda_mu
12:41:36 HOL-Nominal-Examples: theory LocalWeakening
12:41:38 HOL-Nominal-Examples: theory Pattern
12:41:47 HOL-Nominal-Examples: theory SOS
12:41:50 HOL-Nominal-Examples: theory Standardization
12:41:53 HOL-Nominal-Examples: theory Support
12:41:54 HOL-Nominal-Examples: theory Type_Preservation
12:41:57 HOL-Nominal-Examples: theory W
12:42:04 HOL-Nominal-Examples: theory Weakening
12:42:59 Timing HOL-MicroJava (2 threads, 164.371s elapsed time, 307.708s cpu time, 15.776s GC time, factor 1.87)
12:42:59 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava
12:42:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/document.pdf
12:42:59 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-MicroJava/outline.pdf
12:42:59 Finished HOL-MicroJava (0:02:50 elapsed time, 0:05:15 cpu time, factor 1.85)
12:42:59 Running HOL-Nonstandard_Analysis-Examples ...
12:43:01 HOL-Nonstandard_Analysis-Examples: theory Multiset
12:43:05 HOL-Nonstandard_Analysis-Examples: theory Factorial_Ring
12:43:13 HOL-Nonstandard_Analysis-Examples: theory Euclidean_Algorithm
12:43:21 HOL-Nonstandard_Analysis-Examples: theory Primes
12:43:22 HOL-Nonstandard_Analysis-Examples: theory NSPrimes
12:43:36 Timing HOL-Nonstandard_Analysis-Examples (2 threads, 34.228s elapsed time, 64.024s cpu time, 1.484s GC time, factor 1.87)
12:43:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nonstandard_Analysis-Examples
12:43:36 Finished HOL-Nonstandard_Analysis-Examples (0:00:36 elapsed time, 0:01:05 cpu time, factor 1.82)
12:43:36 Running HOL-Number_Theory ...
12:43:37 HOL-Number_Theory: theory Congruence
12:43:37 HOL-Number_Theory: theory FuncSet
12:43:38 HOL-Number_Theory: theory Multiset
12:43:38 HOL-Number_Theory: theory Lattice
12:43:38 HOL-Nominal-Examples: theory Class2
12:43:41 HOL-Number_Theory: theory Group
12:43:42 HOL-Number_Theory: theory FiniteProduct
12:43:43 HOL-Number_Theory: theory Ring
12:43:43 HOL-Nominal-Examples: theory Class3
12:44:05 HOL-Number_Theory: theory Fib
12:44:05 HOL-Number_Theory: theory MiscAlgebra
12:44:06 HOL-Number_Theory: theory Factorial_Ring
12:44:13 HOL-Number_Theory: theory Euclidean_Algorithm
12:44:21 HOL-Number_Theory: theory Primes
12:44:22 HOL-Number_Theory: theory Cong
12:44:22 HOL-Number_Theory: theory Eratosthenes
12:44:22 HOL-Number_Theory: theory Residues
12:44:24 HOL-Number_Theory: theory Gauss
12:44:24 HOL-Number_Theory: theory Pocklington
12:44:25 HOL-Number_Theory: theory Number_Theory
12:44:55 Timing HOL-Number_Theory (2 threads, 73.934s elapsed time, 140.908s cpu time, 3.308s GC time, factor 1.91)
12:44:55 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory
12:44:55 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/document.pdf
12:44:55 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/outline.pdf
12:44:55 Finished HOL-Number_Theory (0:01:18 elapsed time, 0:02:26 cpu time, factor 1.86)
12:44:55 Running HOL-Old_Number_Theory ...
12:44:56 HOL-Old_Number_Theory: theory Infinite_Set
12:44:56 HOL-Old_Number_Theory: theory Multiset
12:45:01 HOL-Old_Number_Theory: theory Permutation
12:45:09 HOL-Old_Number_Theory: theory BijectionRel
12:45:09 HOL-Old_Number_Theory: theory Legacy_GCD
12:45:09 HOL-Old_Number_Theory: theory Primes
12:45:10 HOL-Old_Number_Theory: theory Factorization
12:45:10 HOL-Old_Number_Theory: theory Fib
12:45:10 HOL-Old_Number_Theory: theory IntPrimes
12:45:11 HOL-Old_Number_Theory: theory Pocklington
12:45:11 HOL-Old_Number_Theory: theory Chinese
12:45:11 HOL-Old_Number_Theory: theory IntFact
12:45:12 HOL-Old_Number_Theory: theory EulerFermat
12:45:12 HOL-Old_Number_Theory: theory Finite2
12:45:12 HOL-Old_Number_Theory: theory WilsonBij
12:45:12 HOL-Old_Number_Theory: theory WilsonRuss
12:45:13 HOL-Old_Number_Theory: theory Int2
12:45:13 HOL-Old_Number_Theory: theory EvenOdd
12:45:14 HOL-Old_Number_Theory: theory Residues
12:45:14 HOL-Old_Number_Theory: theory Euler
12:45:14 HOL-Old_Number_Theory: theory Gauss
12:45:14 HOL-Old_Number_Theory: theory Quadratic_Reciprocity
12:45:47 Timing HOL-Nitpick_Examples (2 threads, 323.140s elapsed time, 114.496s cpu time, 2.200s GC time, factor 0.35)
12:45:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nitpick_Examples
12:45:47 Finished HOL-Nitpick_Examples (0:05:24 elapsed time, 0:11:13 cpu time, factor 2.07)
12:45:47 Running HOL-Predicate_Compile_Examples ...
12:45:49 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Alternative_Defs
12:45:49 HOL-Predicate_Compile_Examples: theory Examples
12:45:49 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck
12:45:50 HOL-Predicate_Compile_Examples: theory IMP_1
12:45:50 HOL-Predicate_Compile_Examples: theory IMP_2
12:45:51 Timing HOL-Old_Number_Theory (2 threads, 50.410s elapsed time, 93.140s cpu time, 1.732s GC time, factor 1.85)
12:45:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Old_Number_Theory
12:45:51 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Old_Number_Theory/document.pdf
12:45:51 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Old_Number_Theory/outline.pdf
12:45:51 Finished HOL-Old_Number_Theory (0:00:55 elapsed time, 0:01:40 cpu time, factor 1.80)
12:45:51 Running HOL-Probability-ex ...
12:45:51 HOL-Predicate_Compile_Examples: theory IMP_3
12:45:52 HOL-Predicate_Compile_Examples: theory IMP_4
12:45:53 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Quickcheck_Examples
12:45:55 HOL-Probability-ex: theory Dining_Cryptographers
12:45:55 HOL-Probability-ex: theory Koepf_Duermuth_Countermeasure
12:45:56 HOL-Probability-ex: theory Measure_Not_CCC
12:45:58 HOL-Predicate_Compile_Examples: theory Predicate_Compile_Tests
12:46:02 HOL-Predicate_Compile_Examples: theory Specialisation_Examples
12:46:43 Warning: missing document directory
12:46:43 Timing HOL-Probability-ex (2 threads, 47.629s elapsed time, 56.512s cpu time, 0.728s GC time, factor 1.19)
12:46:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Probability-ex
12:46:43 Finished HOL-Probability-ex (0:00:51 elapsed time, 0:01:00 cpu time, factor 1.17)
12:46:43 Running HOL-Prolog ...
12:46:45 HOL-Prolog: theory HOHH
12:46:45 HOL-Prolog: theory Func
12:46:45 HOL-Prolog: theory Test
12:46:45 HOL-Prolog: theory Type
12:46:45 Timing HOL-Prolog (2 threads, 0.217s elapsed time, 0.372s cpu time, 0.000s GC time, factor 1.72)
12:46:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Prolog
12:46:45 Finished HOL-Prolog (0:00:01 elapsed time)
12:46:45 HOL-Proofs-Extraction CANCELLED
12:46:45 HOL-Proofs-Lambda CANCELLED
12:46:45 HOL-Proofs-ex CANCELLED
12:46:45 Running HOL-Quickcheck_Examples ...
12:46:47 HOL-Quickcheck_Examples: theory AList
12:46:47 HOL-Quickcheck_Examples: theory Completeness
12:46:48 HOL-Quickcheck_Examples: theory Dlist
12:46:49 HOL-Quickcheck_Examples: theory Multiset
12:46:49 HOL-Quickcheck_Examples: theory DAList
12:46:51 HOL-Quickcheck_Examples: theory Quickcheck_Interfaces
12:46:51 HOL-Quickcheck_Examples: theory Quickcheck_Lattice_Examples
12:46:52 HOL-Quickcheck_Examples: theory Quickcheck_Nesting
12:46:52 HOL-Quickcheck_Examples: theory Quickcheck_Nesting_Example
12:46:54 HOL-Quickcheck_Examples: theory DAList_Multiset
12:46:55 HOL-Quickcheck_Examples: theory Quickcheck_Examples
12:47:31 HOL-Predicate_Compile_Examples: theory Hotel_Example
12:47:31 HOL-Predicate_Compile_Examples: theory Code_Prolog
12:47:31 HOL-Predicate_Compile_Examples: theory Code_Prolog_Examples
12:47:34 HOL-Predicate_Compile_Examples: theory Context_Free_Grammar_Example
12:47:35 HOL-Predicate_Compile_Examples: theory Lambda_Example
12:47:35 HOL-Predicate_Compile_Examples: theory Hotel_Example_Prolog
12:47:35 HOL-Predicate_Compile_Examples: theory List_Examples
12:47:44 HOL-Predicate_Compile_Examples: theory Reg_Exp_Example
12:47:51 Timing HOL-Predicate_Compile_Examples (2 threads, 121.924s elapsed time, 197.412s cpu time, 17.788s GC time, factor 1.62)
12:47:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Predicate_Compile_Examples
12:47:51 Finished HOL-Predicate_Compile_Examples (0:02:03 elapsed time, 0:05:02 cpu time, factor 2.44)
12:47:51 Running HOL-Quotient_Examples ...
12:47:53 HOL-Quotient_Examples: theory Congruence
12:47:53 HOL-Quotient_Examples: theory FuncSet
12:47:53 HOL-Quotient_Examples: theory Lift_DList
12:47:54 HOL-Quotient_Examples: theory Lattice
12:47:54 HOL-Quotient_Examples: theory Lift_FSet
12:47:55 HOL-Quotient_Examples: theory Lift_Set
12:47:55 HOL-Quotient_Examples: theory Lifting_Code_Dt_Test
12:47:56 HOL-Quotient_Examples: theory Group
12:47:57 HOL-Quotient_Examples: theory Int_Pow
12:47:57 HOL-Quotient_Examples: theory Multiset
12:48:03 HOL-Quotient_Examples: theory Quotient_Syntax
12:48:03 HOL-Quotient_Examples: theory Lift_Fun
12:48:03 HOL-Quotient_Examples: theory Quotient_Message
12:48:05 HOL-Quotient_Examples: theory Quotient_Option
12:48:05 HOL-Quotient_Examples: theory Quotient_Product
12:48:05 HOL-Quotient_Examples: theory Quotient_Int
12:48:06 HOL-Quotient_Examples: theory Quotient_Rat
12:48:06 HOL-Quotient_Examples: theory Quotient_Set
12:48:06 HOL-Quotient_Examples: theory Quotient_List
12:48:07 HOL-Quotient_Examples: theory DList
12:48:07 HOL-Quotient_Examples: theory FSet
12:48:13 HOL-Quickcheck_Examples: theory Predicate_Compile_Alternative_Defs
12:48:13 HOL-Quickcheck_Examples: theory Quickcheck_Narrowing_Examples
12:48:14 HOL-Quickcheck_Examples: theory Predicate_Compile_Quickcheck
12:48:14 HOL-Quickcheck_Examples: theory Hotel_Example
12:48:53 Timing HOL-Quotient_Examples (2 threads, 59.531s elapsed time, 90.472s cpu time, 5.448s GC time, factor 1.52)
12:48:53 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quotient_Examples
12:48:53 Finished HOL-Quotient_Examples (0:01:01 elapsed time, 0:02:31 cpu time, factor 2.48)
12:48:53 Running HOL-SET_Protocol ...
12:48:54 HOL-SET_Protocol: theory Nat_Bijection
12:48:55 HOL-SET_Protocol: theory Message_SET
12:48:58 HOL-SET_Protocol: theory Event_SET
12:48:59 HOL-SET_Protocol: theory Public_SET
12:48:59 HOL-SET_Protocol: theory Cardholder_Registration
12:48:59 HOL-SET_Protocol: theory Merchant_Registration
12:49:00 HOL-SET_Protocol: theory Purchase
12:49:02 HOL-SET_Protocol: theory SET_Protocol
12:49:30 Timing HOL-Quickcheck_Examples (2 threads, 163.022s elapsed time, 196.152s cpu time, 6.968s GC time, factor 1.20)
12:49:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Quickcheck_Examples
12:49:30 Finished HOL-Quickcheck_Examples (0:02:44 elapsed time, 0:04:49 cpu time, factor 1.76)
12:49:30 Running HOL-SPARK-Examples ...
12:49:32 HOL-SPARK-Examples: theory RMD_Lemmas
12:49:32 HOL-SPARK-Examples: theory RMD
12:49:32 HOL-SPARK-Examples: theory Greatest_Common_Divisor
12:49:33 HOL-SPARK-Examples: theory Longest_Increasing_Subsequence
12:49:33 HOL-SPARK-Examples: theory RMD_Specification
12:49:34 HOL-SPARK-Examples: theory F
12:49:37 HOL-SPARK-Examples: theory Hash
12:49:38 HOL-SPARK-Examples: theory K_L
12:49:39 HOL-SPARK-Examples: theory K_R
12:49:40 HOL-SPARK-Examples: theory R_L
12:49:40 Timing HOL-SET_Protocol (2 threads, 43.918s elapsed time, 85.988s cpu time, 1.512s GC time, factor 1.96)
12:49:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol
12:49:40 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/document.pdf
12:49:40 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SET_Protocol/outline.pdf
12:49:40 Finished HOL-SET_Protocol (0:00:47 elapsed time, 0:01:30 cpu time, factor 1.91)
12:49:40 Running HOL-SPARK-Manual ...
12:49:41 HOL-SPARK-Examples: theory R_R
12:49:41 HOL-SPARK-Examples: theory Round
12:49:42 HOL-SPARK-Manual: theory Complex_Types
12:49:42 HOL-SPARK-Manual: theory Greatest_Common_Divisor
12:49:42 HOL-SPARK-Examples: theory S_L
12:49:43 HOL-SPARK-Manual: theory Proc1
12:49:43 HOL-SPARK-Manual: theory Proc2
12:49:43 HOL-SPARK-Manual: theory VC_Principles
12:49:43 HOL-SPARK-Examples: theory S_R
12:49:44 HOL-SPARK-Manual: theory Reference
12:49:44 HOL-SPARK-Manual: theory Simple_Greatest_Common_Divisor
12:49:44 HOL-SPARK-Manual: theory Example_Verification
12:49:44 HOL-SPARK-Examples: theory Sqrt
12:49:50 Timing HOL-SPARK-Manual (2 threads, 4.579s elapsed time, 9.532s cpu time, 0.184s GC time, factor 2.08)
12:49:50 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual
12:49:50 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/document.pdf
12:49:50 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Manual/outline.pdf
12:49:50 Finished HOL-SPARK-Manual (0:00:09 elapsed time, 0:00:15 cpu time, factor 1.70)
12:49:50 Running HOL-Statespace ...
12:49:51 HOL-Statespace: theory DistinctTreeProver
12:49:53 HOL-Statespace: theory StateFun
12:49:53 HOL-Statespace: theory StateSpaceLocale
12:49:53 HOL-Statespace: theory StateSpaceSyntax
12:49:53 HOL-Statespace: theory StateSpaceEx
12:49:54 Timing HOL-SPARK-Examples (2 threads, 21.482s elapsed time, 37.792s cpu time, 0.712s GC time, factor 1.76)
12:49:54 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-SPARK-Examples
12:49:54 Finished HOL-SPARK-Examples (0:00:23 elapsed time, 0:00:39 cpu time, factor 1.69)
12:49:54 Running HOL-TLA-Buffer ...
12:49:55 HOL-TLA-Buffer: theory Buffer
12:49:56 HOL-TLA-Buffer: theory DBuffer
12:49:57 Timing HOL-TLA-Buffer (2 threads, 1.089s elapsed time, 1.860s cpu time, 0.028s GC time, factor 1.71)
12:49:57 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Buffer
12:49:57 Finished HOL-TLA-Buffer (0:00:02 elapsed time, 0:00:03 cpu time)
12:49:57 Running HOL-TLA-Inc ...
12:49:58 HOL-TLA-Inc: theory Inc
12:50:01 Timing HOL-TLA-Inc (2 threads, 2.064s elapsed time, 4.196s cpu time, 0.080s GC time, factor 2.03)
12:50:01 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Inc
12:50:01 Finished HOL-TLA-Inc (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.54)
12:50:01 Running HOL-TLA-Memory ...
12:50:02 HOL-TLA-Memory: theory RPCMemoryParams
12:50:02 HOL-TLA-Memory: theory MemoryParameters
12:50:02 HOL-TLA-Memory: theory ProcedureInterface
12:50:03 HOL-TLA-Memory: theory RPCParameters
12:50:03 HOL-TLA-Memory: theory Memory
12:50:04 HOL-TLA-Memory: theory MemClerkParameters
12:50:04 HOL-TLA-Memory: theory RPC
12:50:04 HOL-TLA-Memory: theory MemClerk
12:50:05 HOL-TLA-Memory: theory MemoryImplementation
12:50:09 Timing HOL-Statespace (2 threads, 15.818s elapsed time, 22.224s cpu time, 0.672s GC time, factor 1.40)
12:50:09 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace
12:50:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/document.pdf
12:50:09 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Statespace/outline.pdf
12:50:09 Finished HOL-Statespace (0:00:18 elapsed time, 0:00:26 cpu time, factor 1.38)
12:50:09 Running HOL-TPTP ...
12:50:10 HOL-TPTP: theory MaSh_Export_Base
12:50:10 HOL-TPTP: theory ATP_Theory_Export
12:50:11 HOL-TPTP: theory THF_Arith
12:50:11 HOL-TPTP: theory MaSh_Eval
12:50:11 HOL-TPTP: theory TPTP_Parser
12:50:13 HOL-TPTP: theory TPTP_Interpret
12:50:13 HOL-TPTP: theory TPTP_Proof_Reconstruction
12:50:13 Timing HOL-TLA-Memory (2 threads, 10.384s elapsed time, 20.268s cpu time, 0.524s GC time, factor 1.95)
12:50:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TLA-Memory
12:50:13 Finished HOL-TLA-Memory (0:00:12 elapsed time, 0:00:21 cpu time, factor 1.81)
12:50:13 Running HOL-UNITY ...
12:50:14 HOL-TPTP: theory Refute
12:50:15 HOL-TPTP: theory ATP_Problem_Import
12:50:16 HOL-UNITY: theory ListOrder
12:50:16 HOL-UNITY: theory Multiset
12:50:16 Timing HOL-TPTP (2 threads, 4.954s elapsed time, 8.084s cpu time, 0.236s GC time, factor 1.63)
12:50:16 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-TPTP
12:50:16 Finished HOL-TPTP (0:00:06 elapsed time, 0:00:09 cpu time, factor 1.46)
12:50:16 Running HOL-Unix ...
12:50:16 HOL-UNITY: theory UNITY
12:50:17 HOL-UNITY: theory Constrains
12:50:17 HOL-UNITY: theory Deadlock
12:50:17 HOL-UNITY: theory FP
12:50:17 HOL-UNITY: theory Network
12:50:17 HOL-Unix: theory Nested_Environment
12:50:17 HOL-Unix: theory Sublist
12:50:18 HOL-UNITY: theory WFair
12:50:19 HOL-UNITY: theory SubstAx
12:50:19 HOL-Unix: theory Unix
12:50:19 HOL-UNITY: theory Detects
12:50:20 HOL-UNITY: theory Union
12:50:20 HOL-UNITY: theory Multiset_Order
12:50:20 HOL-UNITY: theory Follows
12:50:20 HOL-UNITY: theory Comp
12:50:21 HOL-UNITY: theory Guar
12:50:21 HOL-UNITY: theory Transformers
12:50:21 HOL-UNITY: theory Extend
12:50:21 HOL-UNITY: theory ProgressSets
12:50:22 HOL-UNITY: theory Token
12:50:22 HOL-UNITY: theory Project
12:50:22 HOL-UNITY: theory ELT
12:50:22 HOL-UNITY: theory Rename
12:50:23 HOL-UNITY: theory Lift_prog
12:50:23 HOL-UNITY: theory PPROD
12:50:23 HOL-UNITY: theory UNITY_Main
12:50:24 HOL-UNITY: theory AllocBase
12:50:24 HOL-UNITY: theory Channel
12:50:24 HOL-UNITY: theory Common
12:50:24 HOL-UNITY: theory Alloc
12:50:24 HOL-UNITY: theory AllocImpl
12:50:27 HOL-UNITY: theory Client
12:50:27 HOL-UNITY: theory Counter
12:50:27 HOL-UNITY: theory Counterc
12:50:28 HOL-UNITY: theory Handshake
12:50:28 HOL-UNITY: theory Lift
12:50:28 HOL-UNITY: theory Mutex
12:50:28 HOL-UNITY: theory NSP_Bad
12:50:29 HOL-UNITY: theory PriorityAux
12:50:29 HOL-UNITY: theory Priority
12:50:29 HOL-UNITY: theory Progress
12:50:29 HOL-UNITY: theory Reach
12:50:29 HOL-UNITY: theory TimerArray
12:50:29 HOL-UNITY: theory Reachability
12:50:30 Timing HOL-Unix (2 threads, 10.511s elapsed time, 21.180s cpu time, 0.704s GC time, factor 2.01)
12:50:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix
12:50:30 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/document.pdf
12:50:30 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Unix/outline.pdf
12:50:30 Finished HOL-Unix (0:00:13 elapsed time, 0:00:25 cpu time, factor 1.83)
12:50:30 Running HOL-Word-Examples ...
12:50:32 HOL-Word-Examples: theory WordBitwise
12:50:32 HOL-Word-Examples: theory WordExamples
12:50:34 Timing HOL-Word-Examples (2 threads, 2.045s elapsed time, 4.452s cpu time, 0.064s GC time, factor 2.18)
12:50:34 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-Examples
12:50:34 Finished HOL-Word-Examples (0:00:04 elapsed time, 0:00:06 cpu time, factor 1.58)
12:50:34 Running HOL-Word-SMT_Examples ...
12:50:36 HOL-Word-SMT_Examples: theory SMT_Examples
12:50:36 HOL-Word-SMT_Examples: theory Boogie
12:50:37 HOL-Word-SMT_Examples: theory SMT_Tests
12:50:39 HOL-Word-SMT_Examples: theory SMT_Word_Examples
12:51:15 Timing HOL-UNITY (2 threads, 55.099s elapsed time, 109.568s cpu time, 3.928s GC time, factor 1.99)
12:51:15 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY
12:51:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/document.pdf
12:51:15 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-UNITY/outline.pdf
12:51:15 Finished HOL-UNITY (0:01:01 elapsed time, 0:01:58 cpu time, factor 1.93)
12:51:15 Running HOL-ZF ...
12:51:17 HOL-ZF: theory HOLZF
12:51:17 HOL-ZF: theory Multiset
12:51:17 HOL-ZF: theory Zet
12:51:21 HOL-ZF: theory LProd
12:51:21 HOL-ZF: theory MainZF
12:51:21 HOL-ZF: theory Games
12:51:35 Timing HOL-ZF (2 threads, 14.578s elapsed time, 29.964s cpu time, 0.980s GC time, factor 2.06)
12:51:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF
12:51:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/document.pdf
12:51:35 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ZF/outline.pdf
12:51:35 Finished HOL-ZF (0:00:19 elapsed time, 0:00:36 cpu time, factor 1.88)
12:51:35 Running HOL-ex ...
12:51:36 HOL-ex: theory Cartouche_Examples
12:51:36 HOL-ex: theory Adhoc_Overloading
12:51:36 HOL-ex: theory Chinese
12:51:37 HOL-ex: theory Code_Abstract_Nat
12:51:37 HOL-ex: theory Code_Binary_Nat
12:51:37 HOL-ex: theory FuncSet
12:51:37 HOL-ex: theory Hebrew
12:51:38 HOL-ex: theory Monad_Syntax
12:51:38 HOL-ex: theory Refute
12:51:38 HOL-ex: theory Serbian
12:51:39 HOL-ex: theory State_Monad
12:51:39 HOL-ex: theory Code_Binary_Nat_examples
12:51:40 HOL-ex: theory Eval_Examples
12:51:40 Timing HOL-Word-SMT_Examples (2 threads, 63.232s elapsed time, 83.168s cpu time, 0.632s GC time, factor 1.32)
12:51:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Word-SMT_Examples
12:51:40 Finished HOL-Word-SMT_Examples (0:01:05 elapsed time, 0:01:28 cpu time, factor 1.35)
12:51:40 Running HOLCF-FOCUS ...
12:51:42 HOLCF-FOCUS: theory Infinite_Set
12:51:42 HOL-ex: theory Normalization_by_Evaluation
12:51:42 HOLCF-FOCUS: theory Countable_Set
12:51:43 HOLCF-FOCUS: theory Countable_Complete_Lattices
12:51:43 HOL-ex: theory Transitive_Closure_Table
12:51:46 HOLCF-FOCUS: theory Order_Continuity
12:51:47 HOLCF-FOCUS: theory Extended_Nat
12:51:47 HOLCF-FOCUS: theory Stream
12:51:49 HOLCF-FOCUS: theory Fstream
12:51:49 HOLCF-FOCUS: theory Fstreams
12:51:49 HOLCF-FOCUS: theory FOCUS
12:51:49 HOLCF-FOCUS: theory Stream_adm
12:51:49 HOLCF-FOCUS: theory Buffer
12:51:51 HOLCF-FOCUS: theory Buffer_adm
12:51:58 Timing HOLCF-FOCUS (2 threads, 14.970s elapsed time, 29.476s cpu time, 0.752s GC time, factor 1.97)
12:51:58 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-FOCUS
12:51:58 Finished HOLCF-FOCUS (0:00:17 elapsed time, 0:00:31 cpu time, factor 1.85)
12:51:58 Running HOLCF-IMP ...
12:52:00 HOLCF-IMP: theory AExp
12:52:01 HOLCF-IMP: theory BExp
12:52:02 HOL-ex: theory PresburgerEx
12:52:02 HOL-ex: theory Groebner_Examples
12:52:03 HOL-ex: theory AList
12:52:03 HOL-ex: theory Abstract_NAT
12:52:03 HOLCF-IMP: theory Com
12:52:03 HOL-ex: theory Antiquote
12:52:03 HOL-ex: theory Arith_Examples
12:52:03 HOL-ex: theory CTL
12:52:03 HOL-ex: theory Classical
12:52:04 HOLCF-IMP: theory Big_Step
12:52:04 HOL-ex: theory Code_Target_Nat
12:52:04 HOLCF-IMP: theory Denotational
12:52:04 HOL-ex: theory Coercion_Examples
12:52:04 HOL-ex: theory Coherent
12:52:05 HOLCF-IMP: theory HoareEx
12:52:05 HOL-ex: theory Commands
12:52:05 HOL-ex: theory Debug
12:52:05 HOL-ex: theory Dlist
12:52:06 HOL-ex: theory Erdoes_Szekeres
12:52:06 HOL-ex: theory Executable_Relation
12:52:06 HOL-ex: theory FSet
12:52:06 HOL-ex: theory Birthday_Paradox
12:52:07 HOL-ex: theory Code_Target_Int
12:52:07 Timing HOLCF-IMP (2 threads, 6.703s elapsed time, 12.676s cpu time, 0.608s GC time, factor 1.89)
12:52:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-IMP
12:52:07 Finished HOLCF-IMP (0:00:08 elapsed time, 0:00:14 cpu time, factor 1.67)
12:52:07 Running HOLCF-Library ...
12:52:07 HOL-ex: theory Code_Target_Numeral
12:52:07 HOL-ex: theory Transfer_Int_Nat
12:52:07 HOL-ex: theory Guess
12:52:08 HOL-ex: theory Hex_Bin_Examples
12:52:08 HOL-ex: theory IArray
12:52:09 HOLCF-Library: theory Infinite_Set
12:52:09 HOLCF-Library: theory Bool_Discrete
12:52:09 HOLCF-Library: theory Char_Discrete
12:52:09 HOL-ex: theory IArray_Examples
12:52:09 HOLCF-Library: theory Countable_Set
12:52:09 HOLCF-Library: theory Defl_Bifinite
12:52:09 HOL-ex: theory Iff_Oracle
12:52:09 HOL-ex: theory Induction_Schema
12:52:09 HOL-ex: theory Infinite_Set
12:52:09 HOL-ex: theory Intuitionistic
12:52:10 HOLCF-Library: theory Countable_Complete_Lattices
12:52:10 HOL-ex: theory LaTeXsugar
12:52:10 HOL-ex: theory Adhoc_Overloading_Examples
12:52:10 HOL-ex: theory Lagrange
12:52:10 HOLCF-Library: theory Int_Discrete
12:52:10 HOL-ex: theory List_to_Set_Comprehension_Examples
12:52:10 HOLCF-Library: theory List_Cpo
12:52:10 HOL-ex: theory LocaleTest2
12:52:10 HOLCF-Library: theory Nat_Discrete
12:52:11 HOLCF-Library: theory Sum_Cpo
12:52:11 HOL-ex: theory ML
12:52:11 HOL-ex: theory Mapping
12:52:11 HOLCF-Library: theory List_Predomain
12:52:12 HOL-ex: theory AList_Mapping
12:52:12 HOL-ex: theory Functions
12:52:12 HOLCF-Library: theory Option_Cpo
12:52:12 HOL-ex: theory Execute_Choice
12:52:12 HOL-ex: theory MonoidGroup
12:52:12 HOLCF-Library: theory Order_Continuity
12:52:13 HOL-ex: theory Multiquote
12:52:13 HOL-ex: theory Multiset
12:52:13 HOLCF-Library: theory Extended_Nat
12:52:14 HOLCF-Library: theory Stream
12:52:16 HOLCF-Library: theory HOLCF_Library
12:52:18 HOL-ex: theory NatSum
12:52:18 HOL-ex: theory Bubblesort
12:52:18 HOL-ex: theory Factorial_Ring
12:52:19 HOL-ex: theory MergeSort
12:52:20 HOL-ex: theory Quicksort
12:52:20 HOL-ex: theory PER
12:52:21 HOL-ex: theory Parallel
12:52:21 HOL-ex: theory Perm
12:52:23 HOL-ex: theory Perm_Fragments
12:52:23 HOL-ex: theory Phantom_Type
12:52:24 HOL-ex: theory Cardinality
12:52:25 HOL-ex: theory FinFun
12:52:25 HOL-ex: theory Euclidean_Algorithm
12:52:26 Timing HOLCF-Library (2 threads, 16.780s elapsed time, 33.224s cpu time, 0.888s GC time, factor 1.98)
12:52:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Library
12:52:26 Finished HOLCF-Library (0:00:18 elapsed time, 0:00:35 cpu time, factor 1.87)
12:52:26 Running HOLCF-Tutorial ...
12:52:27 HOL-ex: theory FinFunPred
12:52:28 HOLCF-Tutorial: theory Domain_ex
12:52:28 HOLCF-Tutorial: theory Fixrec_ex
12:52:28 HOL-ex: theory Primrec
12:52:29 HOL-ex: theory Records
12:52:30 HOLCF-Tutorial: theory New_Domain
12:52:33 HOL-ex: theory Reflection
12:52:33 HOL-ex: theory Refute_Examples
12:52:34 HOL-ex: theory Primes
12:52:34 HOL-ex: theory Eratosthenes
12:52:35 HOL-ex: theory Code_Timing
12:52:35 HOL-ex: theory Rewrite
12:52:36 HOL-ex: theory Rewrite_Examples
12:52:36 HOL-ex: theory SAT_Examples
12:52:36 HOL-ex: theory Seq
12:52:36 HOL-ex: theory Set_Comprehension_Pointfree_Examples
12:52:37 HOL-ex: theory Set_Theory
12:52:37 HOL-ex: theory Simproc_Tests
12:52:37 HOL-ex: theory Simps_Case_Conv
12:52:37 HOL-ex: theory Simps_Case_Conv_Examples
12:52:38 HOL-ex: theory Sudoku
12:52:39 HOL-ex: theory Tarski
12:52:40 HOL-ex: theory Termination
12:52:41 Timing HOLCF-Tutorial (2 threads, 11.871s elapsed time, 16.520s cpu time, 0.376s GC time, factor 1.39)
12:52:41 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial
12:52:41 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/document.pdf
12:52:41 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-Tutorial/outline.pdf
12:52:41 Finished HOLCF-Tutorial (0:00:15 elapsed time, 0:00:20 cpu time, factor 1.34)
12:52:41 Running HOLCF-ex ...
12:52:43 HOL-ex: theory ThreeDivides
12:52:43 HOL-ex: theory Ballot
12:52:43 HOLCF-ex: theory Infinite_Set
12:52:43 HOLCF-ex: theory Concurrency_Monad
12:52:44 HOLCF-ex: theory Countable_Set
12:52:44 HOL-ex: theory BinEx
12:52:44 HOLCF-ex: theory Countable_Complete_Lattices
12:52:44 HOL-ex: theory Cubic_Quartic
12:52:45 HOL-ex: theory Dedekind_Real
12:52:45 HOLCF-ex: theory Dnat
12:52:46 HOLCF-ex: theory Domain_Proofs
12:52:46 HOL-ex: theory Gauge_Integration
12:52:46 HOL-ex: theory HarmonicSeries
12:52:46 HOL-ex: theory Parallel_Example
12:52:46 HOL-ex: theory Pythagoras
12:52:46 HOL-ex: theory Reflection_Examples
12:52:47 HOLCF-ex: theory Fix2
12:52:47 HOLCF-ex: theory Hoare
12:52:47 HOLCF-ex: theory Letrec
12:52:47 HOL-ex: theory Sqrt
12:52:47 HOLCF-ex: theory Loop
12:52:47 HOLCF-ex: theory Pattern_Match
12:52:47 HOLCF-ex: theory Powerdomain_ex
12:52:47 HOL-ex: theory Sqrt_Script
12:52:48 HOLCF-ex: theory Order_Continuity
12:52:48 HOL-ex: theory Sum_of_Powers
12:52:48 HOL-ex: theory Sum_of_Squares
12:52:49 HOLCF-ex: theory Extended_Nat
12:52:50 HOLCF-ex: theory Stream
12:52:51 HOL-ex: theory SOS
12:52:51 HOL-ex: theory SOS_Cert
12:52:51 HOLCF-ex: theory Dagstuhl
12:52:51 HOLCF-ex: theory Focus_ex
12:52:51 HOL-ex: theory Transfer_Debug
12:52:52 HOL-ex: theory Transfer_Ex
12:52:52 HOL-ex: theory Transitive_Closure_Table_Ex
12:52:52 HOL-ex: theory Tree23
12:53:00 Timing HOLCF-ex (2 threads, 16.979s elapsed time, 33.408s cpu time, 0.892s GC time, factor 1.97)
12:53:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF-ex
12:53:00 Finished HOLCF-ex (0:00:19 elapsed time, 0:00:35 cpu time, factor 1.86)
12:53:00 Running How_to_Prove_it ...
12:53:02 How_to_Prove_it: theory How_to_Prove_it
12:53:05 Timing How_to_Prove_it (2 threads, 1.339s elapsed time, 1.660s cpu time, 0.012s GC time, factor 1.24)
12:53:05 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it
12:53:05 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/How_to_Prove_it/how_to_prove_it.pdf
12:53:05 Finished How_to_Prove_it (0:00:04 elapsed time, 0:00:04 cpu time, factor 1.03)
12:53:05 Running IOA-ABP ...
12:53:07 IOA-ABP: theory Lemmas
12:53:07 IOA-ABP: theory Packet
12:53:07 IOA-ABP: theory Action
12:53:08 IOA-ABP: theory Abschannel
12:53:08 IOA-ABP: theory Env
12:53:09 IOA-ABP: theory Receiver
12:53:10 IOA-ABP: theory Sender
12:53:10 IOA-ABP: theory Abschannel_finite
12:53:10 IOA-ABP: theory Impl
12:53:10 IOA-ABP: theory Impl_finite
12:53:11 IOA-ABP: theory Spec
12:53:11 IOA-ABP: theory Correctness
12:53:11 HOL-ex: theory Unification
12:53:13 Timing IOA-ABP (2 threads, 5.676s elapsed time, 11.548s cpu time, 0.468s GC time, factor 2.03)
12:53:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ABP
12:53:13 Finished IOA-ABP (0:00:07 elapsed time, 0:00:13 cpu time, factor 1.74)
12:53:13 Running IOA-NTP ...
12:53:15 IOA-NTP: theory Lemmas
12:53:15 IOA-NTP: theory Multiset
12:53:15 IOA-NTP: theory Packet
12:53:15 IOA-NTP: theory Action
12:53:17 IOA-NTP: theory Abschannel
12:53:17 IOA-NTP: theory Receiver
12:53:18 HOL-ex: theory While_Combinator
12:53:18 IOA-NTP: theory Sender
12:53:19 HOL-ex: theory While_Combinator_Example
12:53:19 IOA-NTP: theory Spec
12:53:19 IOA-NTP: theory Impl
12:53:20 IOA-NTP: theory Correctness
12:53:22 Timing IOA-NTP (2 threads, 7.237s elapsed time, 14.244s cpu time, 0.496s GC time, factor 1.97)
12:53:22 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-NTP
12:53:22 Finished IOA-NTP (0:00:09 elapsed time, 0:00:16 cpu time, factor 1.74)
12:53:22 Running IOA-Storage ...
12:53:24 IOA-Storage: theory Action
12:53:25 IOA-Storage: theory Impl
12:53:25 IOA-Storage: theory Spec
12:53:25 IOA-Storage: theory Correctness
12:53:26 Timing IOA-Storage (2 threads, 1.783s elapsed time, 3.700s cpu time, 0.040s GC time, factor 2.08)
12:53:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-Storage
12:53:26 Finished IOA-Storage (0:00:03 elapsed time, 0:00:05 cpu time, factor 1.45)
12:53:26 Running IOA-ex ...
12:53:28 IOA-ex: theory TrivEx
12:53:28 IOA-ex: theory TrivEx2
12:53:31 Timing IOA-ex (2 threads, 1.835s elapsed time, 3.180s cpu time, 0.064s GC time, factor 1.73)
12:53:31 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/IOA-ex
12:53:31 Finished IOA-ex (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.31)
12:53:31 Running Implementation ...
12:53:32 Implementation: theory Base
12:53:33 Implementation: theory Eq
12:53:33 Implementation: theory Integration
12:53:33 Implementation: theory Isar
12:53:33 Implementation: theory Local_Theory
12:53:33 Implementation: theory ML
12:53:33 Implementation: theory Prelim
12:53:33 Implementation: theory Proof
12:53:34 Implementation: theory Syntax
12:53:34 Implementation: theory Tactic
12:53:35 Implementation: theory Logic
12:53:40 Timing Implementation (2 threads, 3.890s elapsed time, 7.036s cpu time, 0.060s GC time, factor 1.81)
12:53:40 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation
12:53:40 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Implementation/implementation.pdf
12:53:40 Finished Implementation (0:00:09 elapsed time, 0:00:11 cpu time, factor 1.32)
12:53:40 Running Isar_Ref ...
12:53:42 Isar_Ref: theory Base
12:53:42 Isar_Ref: theory Adhoc_Overloading
12:53:42 Isar_Ref: theory Dlist
12:53:42 Isar_Ref: theory First_Order_Logic
12:53:42 Isar_Ref: theory Document_Preparation
12:53:42 Isar_Ref: theory FSet
12:53:43 Isar_Ref: theory Framework
12:53:44 Isar_Ref: theory Generic
12:53:44 Isar_Ref: theory Inner_Syntax
12:53:45 Isar_Ref: theory Old_Datatype
12:53:46 Isar_Ref: theory Old_Recdef
12:53:46 Isar_Ref: theory Outer_Syntax
12:53:46 Isar_Ref: theory Preface
12:53:46 Isar_Ref: theory Proof
12:53:47 Isar_Ref: theory Proof_Script
12:53:47 Isar_Ref: theory HOL_Specific
12:53:47 Isar_Ref: theory Quick_Reference
12:53:47 Isar_Ref: theory Spec
12:53:47 Isar_Ref: theory Symbols
12:53:47 Isar_Ref: theory Synopsis
12:54:07 Timing Isar_Ref (2 threads, 16.588s elapsed time, 32.128s cpu time, 1.416s GC time, factor 1.94)
12:54:07 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref
12:54:07 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Isar_Ref/isar-ref.pdf
12:54:07 Finished Isar_Ref (0:00:26 elapsed time, 0:00:41 cpu time, factor 1.58)
12:54:07 Running JEdit ...
12:54:08 JEdit: theory Base
12:54:09 JEdit: theory JEdit
12:54:17 Timing JEdit (2 threads, 0.894s elapsed time, 1.284s cpu time, 0.016s GC time, factor 1.44)
12:54:17 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit
12:54:17 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/JEdit/jedit.pdf
12:54:17 Finished JEdit (0:00:10 elapsed time, 0:00:10 cpu time, factor 1.01)
12:54:17 Running Locales ...
12:54:19 Locales: theory Examples
12:54:20 Locales: theory Examples2
12:54:20 Locales: theory Examples1
12:54:20 Locales: theory Examples3
12:54:24 Timing Locales (2 threads, 2.529s elapsed time, 5.256s cpu time, 0.036s GC time, factor 2.08)
12:54:24 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales
12:54:24 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Locales/locales.pdf
12:54:24 Finished Locales (0:00:06 elapsed time, 0:00:08 cpu time, factor 1.41)
12:54:24 Running Main ...
12:54:26 Main: theory Main_Doc
12:54:28 Timing Main (2 threads, 1.282s elapsed time, 1.880s cpu time, 0.020s GC time, factor 1.47)
12:54:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main
12:54:28 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Main/main.pdf
12:54:28 Finished Main (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.11)
12:54:28 Running Prog_Prove ...
12:54:30 Prog_Prove: theory Basics
12:54:30 Prog_Prove: theory Bool_nat_list
12:54:30 Prog_Prove: theory LaTeXsugar
12:54:30 Prog_Prove: theory Isar
12:54:31 Prog_Prove: theory Logic
12:54:31 Prog_Prove: theory MyList
12:54:32 Prog_Prove: theory Types_and_funs
12:54:39 Timing Prog_Prove (2 threads, 5.923s elapsed time, 11.804s cpu time, 0.768s GC time, factor 1.99)
12:54:39 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove
12:54:39 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Prog_Prove/prog-prove.pdf
12:54:39 Finished Prog_Prove (0:00:10 elapsed time, 0:00:15 cpu time, factor 1.56)
12:54:39 Running Sugar ...
12:54:40 Sugar: theory LaTeXsugar
12:54:40 Sugar: theory OptionalSugar
12:54:41 Sugar: theory Sugar
12:54:45 Timing Sugar (2 threads, 2.479s elapsed time, 3.252s cpu time, 0.020s GC time, factor 1.31)
12:54:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar
12:54:45 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Sugar/sugar.pdf
12:54:45 Finished Sugar (0:00:05 elapsed time, 0:00:06 cpu time, factor 1.09)
12:54:45 Running Tutorial ...
12:54:46 Tutorial: theory ToyList_Test
12:54:47 Tutorial: theory AB
12:54:47 Tutorial: theory ABexpr
12:54:48 Tutorial: theory AdvancedInd
12:54:48 Tutorial: theory Base
12:54:48 Tutorial: theory CTL
12:54:49 Tutorial: theory CTLind
12:54:49 Tutorial: theory PDL
12:54:50 Tutorial: theory CodeGen
12:54:50 Tutorial: theory Nested
12:54:52 Tutorial: theory Even
12:54:52 Tutorial: theory Fundata
12:54:52 Tutorial: theory Advanced
12:54:53 Tutorial: theory Ifexpr
12:54:55 Tutorial: theory Itrev
12:54:55 Tutorial: theory Mutual
12:54:55 Tutorial: theory Option2
12:54:55 Tutorial: theory Plus
12:54:55 Tutorial: theory Star
12:54:55 Tutorial: theory ToyList
12:54:56 Tutorial: theory Tree
12:54:56 Tutorial: theory Trie
12:54:56 Tutorial: theory Tree2
12:54:56 Tutorial: theory appendix
12:54:56 Tutorial: theory case_exprs
12:54:57 Tutorial: theory fakenat
12:54:57 Tutorial: theory fun0
12:54:58 Tutorial: theory natsum
12:54:58 Tutorial: theory pairs2
12:54:58 Tutorial: theory prime_def
12:54:58 Tutorial: theory simp
12:54:58 Tutorial: theory simp2
12:54:58 Tutorial: theory types
12:54:58 Tutorial: theory unfoldnested
12:55:07 Tutorial: theory Message
12:55:07 Tutorial: theory Documents
12:55:09 Tutorial: theory Event
12:55:10 Tutorial: theory Public
12:55:10 Tutorial: theory NS_Public
12:55:11 Tutorial: theory Setup
12:55:12 Tutorial: theory Basic
12:55:12 Tutorial: theory Blast
12:55:12 Tutorial: theory Force
12:55:12 Tutorial: theory Pairs
12:55:12 Tutorial: theory Records
12:55:12 Tutorial: theory Overloading
12:55:12 Tutorial: theory Axioms
12:55:13 Tutorial: theory Numbers
12:55:13 Tutorial: theory Typedefs
12:55:14 Tutorial: theory Recur
12:55:14 Tutorial: theory Functions
12:55:14 Tutorial: theory Relations
12:55:14 Tutorial: theory TPrimes
12:55:14 Tutorial: theory Tacticals
12:55:14 Tutorial: theory Examples
12:55:14 Tutorial: theory Forward
12:55:14 Tutorial: theory find2
12:55:20 Timing Tutorial (2 threads, 29.208s elapsed time, 58.092s cpu time, 7.172s GC time, factor 1.99)
12:55:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial
12:55:20 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Tutorial/tutorial.pdf
12:55:20 Finished Tutorial (0:00:35 elapsed time, 0:01:03 cpu time, factor 1.81)
12:55:20 Running Typeclass_Hierarchy ...
12:55:22 Typeclass_Hierarchy: theory Typeclass_Hierarchy
12:55:25 Timing Typeclass_Hierarchy (2 threads, 1.222s elapsed time, 1.456s cpu time, 0.008s GC time, factor 1.19)
12:55:25 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy
12:55:25 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/Doc/Typeclass_Hierarchy/typeclass_hierarchy.pdf
12:55:25 Finished Typeclass_Hierarchy (0:00:04 elapsed time, 0:00:04 cpu time, factor 0.99)
12:56:43 HOL-Nominal-Examples: theory VC_Condition
12:56:47 Timing HOL-Nominal-Examples (2 threads, 965.182s elapsed time, 1775.892s cpu time, 485.080s GC time, factor 1.84)
12:56:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Nominal-Examples
12:56:47 Finished HOL-Nominal-Examples (0:16:07 elapsed time, 0:29:37 cpu time, factor 1.84)
13:00:01 HOL-ex: theory Meson_Test
13:00:26 Timing HOL-ex (2 threads, 514.676s elapsed time, 1000.768s cpu time, 78.520s GC time, factor 1.94)
13:00:26 Browser info at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex
13:00:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex/document.pdf
13:00:26 Document at /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-ex/outline.pdf
13:00:26 Finished HOL-ex (0:08:51 elapsed time, 0:17:43 cpu time, factor 2.00)
13:00:26 Unfinished session(s): HOL-Proofs, HOL-Proofs-Extraction, HOL-Proofs-Lambda, HOL-Proofs-ex
13:00:26 
13:00:26 === TIMING ===
13:00:26 
13:00:26 Group main: 0:28:57 elapsed time, 0:54:25 cpu time, factor 1.88
13:00:26 Group ZF: 0:01:25 elapsed time, 0:02:35 cpu time, factor 1.82
13:00:26 Group doc: 0:04:12 elapsed time, 0:06:03 cpu time, factor 1.44
13:00:26 Overall: 1:01:48 elapsed time, 5:18:25 cpu time, factor 5.15
13:00:26 
13:00:26 === FAILED SESSIONS ===
13:00:26 
13:00:26 Session HOL-Proofs-ex: CANCELLED
13:00:26 Session HOL-Proofs: FAILED 2
13:00:26 Session HOL-Proofs-Extraction: CANCELLED
13:00:26 Session HOL-Proofs-Lambda: CANCELLED
13:00:26 Build step 'Execute shell' marked build as failure
13:00:26 Archiving artifacts
13:00:27 Email was triggered for: Failure - Any
13:00:27 Sending email for trigger: Failure - Any
13:00:27 Sending email to: isabelle-ci@mail46.informatik.tu-muenchen.de
13:00:27 Finished: FAILURE