Skipping 41 KB.. Full Log

HOL: theory HOL.NthRoot
17:56:58 HOL: theory HOL.Transcendental
17:57:05 HOL: theory HOL.Complex
17:57:06 HOL: theory HOL.MacLaurin
17:57:07 HOL: theory Complex_Main
17:58:05 Preparing HOL/document ...
17:59:59 Finished HOL/document (0:01:54 elapsed time)
17:59:59 Preparing HOL/outline ...
18:01:06 Finished HOL/outline (0:01:06 elapsed time)
18:01:07 Timing HOL (8 threads, 305.292s elapsed time, 1194.139s cpu time, 50.415s GC time, factor 3.91)
18:01:07 Finished HOL (0:05:34 elapsed time, 0:21:04 cpu time, factor 3.78)
18:01:07 Building HOL-Analysis (on hpcisabelle/2) ...
18:01:11 HOL-Analysis: theory HOL-Combinatorics.Transposition
18:01:11 HOL-Analysis: theory HOL-Library.Cancellation
18:01:11 HOL-Analysis: theory HOL-Library.BNF_Corec
18:01:11 HOL-Analysis: theory HOL-Library.Infinite_Set
18:01:11 HOL-Analysis: theory HOL-Library.FuncSet
18:01:11 HOL-Analysis: theory HOL-Library.Old_Datatype
18:01:11 HOL-Analysis: theory HOL-Library.Nat_Bijection
18:01:11 HOL-Analysis: theory HOL-Library.Phantom_Type
18:01:11 HOL-Analysis: theory HOL-Library.Product_Plus
18:01:12 HOL-Analysis: theory HOL-Library.Product_Order
18:01:12 HOL-Analysis: theory HOL-Library.Set_Algebras
18:01:12 HOL-Analysis: theory HOL-Real_Asymp.Inst_Existentials
18:01:12 HOL-Analysis: theory HOL-Analysis.Metric_Arith
18:01:12 HOL-Analysis: theory HOL-Analysis.Inner_Product
18:01:12 HOL-Analysis: theory HOL-Library.Countable
18:01:13 HOL-Analysis: theory HOL-Library.Disjoint_Sets
18:01:13 HOL-Analysis: theory HOL-Analysis.L2_Norm
18:01:13 HOL-Analysis: theory HOL-Library.Multiset
18:01:13 HOL-Analysis: theory HOL-Library.Cardinality
18:01:13 HOL-Analysis: theory HOL-Analysis.Operator_Norm
18:01:13 HOL-Analysis: theory HOL-Analysis.Poly_Roots
18:01:13 HOL-Analysis: theory HOL-Analysis.Product_Vector
18:01:13 HOL-Analysis: theory HOL-Library.Complex_Order
18:01:13 HOL-Analysis: theory HOL-Library.Discrete
18:01:14 HOL-Analysis: theory HOL-Library.Indicator_Function
18:01:14 HOL-Analysis: theory HOL-Library.Numeral_Type
18:01:14 HOL-Analysis: theory HOL-Library.Landau_Symbols
18:01:14 HOL-Analysis: theory HOL-Library.Liminf_Limsup
18:01:14 HOL-Analysis: theory HOL-Library.Nonpos_Ints
18:01:14 HOL-Analysis: theory HOL-Library.Countable_Set
18:01:15 HOL-Analysis: theory HOL-Library.Periodic_Fun
18:01:15 HOL-Analysis: theory HOL-Library.Sum_of_Squares
18:01:15 HOL-Analysis: theory HOL-Real_Asymp.Eventuallize
18:01:16 HOL-Analysis: theory HOL-Real_Asymp.Lazy_Eval
18:01:16 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices
18:01:16 HOL-Analysis: theory HOL-Library.Equipollence
18:01:16 HOL-Analysis: theory HOL-Library.Set_Idioms
18:01:16 HOL-Analysis: theory HOL-Analysis.Abstract_Topology
18:01:17 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable
18:01:17 HOL-Analysis: theory HOL-Analysis.Elementary_Topology
18:01:17 HOL-Analysis: theory HOL-Analysis.Euclidean_Space
18:01:22 HOL-Analysis: theory HOL-Library.Order_Continuity
18:01:23 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
18:01:23 HOL-Analysis: theory HOL-Analysis.Linear_Algebra
18:01:24 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring
18:01:24 HOL-Analysis: theory HOL-Combinatorics.Permutations
18:01:24 HOL-Analysis: theory HOL-Library.Extended_Nat
18:01:24 HOL-Analysis: theory HOL-Analysis.Norm_Arith
18:01:25 HOL-Analysis: theory HOL-Analysis.Abstract_Limits
18:01:25 HOL-Analysis: theory HOL-Analysis.FSigma
18:01:27 HOL-Analysis: theory HOL-Analysis.Sum_Topology
18:01:27 HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2
18:01:27 HOL-Analysis: theory HOL-Analysis.Affine
18:01:27 HOL-Analysis: theory HOL-Library.Extended_Real
18:01:27 HOL-Analysis: theory HOL-Real_Asymp.Multiseries_Expansion
18:01:28 HOL-Analysis: theory HOL-Analysis.Convex
18:01:28 HOL-Analysis: theory HOL-Analysis.Cartesian_Space
18:01:30 HOL-Analysis: theory HOL-Analysis.Connected
18:01:30 HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces
18:01:31 HOL-Analysis: theory HOL-Analysis.Function_Topology
18:01:32 HOL-Analysis: theory HOL-Analysis.Determinants
18:01:33 HOL-Analysis: theory HOL-Analysis.Product_Topology
18:01:34 HOL-Analysis: theory HOL-Analysis.T1_Spaces
18:01:34 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real
18:01:34 HOL-Analysis: theory HOL-Analysis.Lindelof_Spaces
18:01:35 HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces
18:01:35 HOL-Analysis: theory HOL-Analysis.Function_Metric
18:01:35 HOL-Analysis: theory HOL-Analysis.Isolated
18:01:37 HOL-Analysis: theory HOL-Analysis.Infinite_Sum
18:01:37 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra
18:01:37 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space
18:01:38 HOL-Analysis: theory HOL-Analysis.Measurable
18:01:39 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits
18:01:39 HOL-Analysis: theory HOL-Analysis.Line_Segment
18:01:39 HOL-Analysis: theory HOL-Analysis.Tagged_Division
18:01:39 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm
18:01:39 HOL-Analysis: theory HOL-Analysis.Measure_Space
18:01:40 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space
18:01:41 HOL-Analysis: theory HOL-Analysis.Summation_Tests
18:01:42 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
18:01:42 HOL-Analysis: theory HOL-Analysis.Starlike
18:01:44 HOL-Analysis: theory HOL-Analysis.Caratheodory
18:01:45 HOL-Analysis: theory HOL-Analysis.Continuous_Extension
18:01:45 HOL-Analysis: theory HOL-Analysis.Path_Connected
18:01:47 HOL-Analysis: theory HOL-Analysis.Locally
18:01:47 HOL-Analysis: theory HOL-Analysis.Uncountable_Sets
18:01:47 HOL-Analysis: theory HOL-Analysis.Homotopy
18:01:49 HOL-Analysis: theory HOL-Analysis.Abstract_Euclidean_Space
18:01:49 HOL-Analysis: theory HOL-Analysis.Homeomorphism
18:01:49 HOL-Analysis: theory HOL-Analysis.Sparse_In
18:01:50 HOL-Analysis: theory HOL-Analysis.Abstract_Topological_Spaces
18:01:53 HOL-Analysis: theory HOL-Analysis.Abstract_Metric_Spaces
18:01:54 HOL-Analysis: theory HOL-Computational_Algebra.Primes
18:01:55 HOL-Analysis: theory HOL-Analysis.Uniform_Limit
18:01:57 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function
18:01:57 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function
18:01:59 HOL-Analysis: theory HOL-Analysis.Derivative
18:02:03 HOL-Analysis: theory HOL-Analysis.Borel_Space
18:02:03 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
18:02:03 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics
18:02:03 HOL-Analysis: theory HOL-Analysis.Cross3
18:02:04 HOL-Analysis: theory HOL-Analysis.Polytope
18:02:04 HOL-Analysis: theory HOL-Analysis.Lipschitz
18:02:04 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint
18:02:05 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series
18:02:05 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
18:02:06 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
18:02:06 HOL-Analysis: theory HOL-Analysis.Multivariate_Analysis
18:02:06 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
18:02:07 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
18:02:07 HOL-Analysis: theory HOL-Analysis.Regularity
18:02:08 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem
18:02:08 HOL-Analysis: theory HOL-Analysis.Retracts
18:02:08 HOL-Analysis: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
18:02:11 HOL-Analysis: theory HOL-Analysis.Urysohn
18:02:12 HOL-Analysis: theory HOL-Analysis.Smooth_Paths
18:02:13 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
18:02:13 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers
18:02:13 HOL-Analysis: theory HOL-Analysis.Infinite_Products
18:02:13 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
18:02:14 HOL-Analysis: theory HOL-Analysis.Embed_Measure
18:02:15 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
18:02:15 HOL-Analysis: theory HOL-Real_Asymp.Real_Asymp
18:02:17 HOL-Analysis: theory HOL-Analysis.FPS_Convergence
18:02:17 HOL-Analysis: theory HOL-Analysis.Bochner_Integration
18:02:20 HOL-Analysis: theory HOL-Analysis.Complete_Measure
18:02:20 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym
18:02:20 HOL-Analysis: theory HOL-Analysis.Set_Integral
18:02:21 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure
18:02:22 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum
18:02:23 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration
18:02:25 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
18:02:25 HOL-Analysis: theory HOL-Analysis.Integral_Test
18:02:25 HOL-Analysis: theory HOL-Analysis.Kronecker_Approximation_Theorem
18:02:28 HOL-Analysis: theory HOL-Analysis.Further_Topology
18:02:28 HOL-Analysis: theory HOL-Analysis.Gamma_Function
18:02:28 HOL-Analysis: theory HOL-Analysis.Improper_Integral
18:02:28 HOL-Analysis: theory HOL-Analysis.Interval_Integral
18:02:28 HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem
18:02:29 HOL-Analysis: theory HOL-Analysis.Equivalence_Measurable_On_Borel
18:02:29 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution
18:02:30 HOL-Analysis: theory HOL-Analysis.Change_Of_Vars
18:02:32 HOL-Analysis: theory HOL-Analysis.Simplex_Content
18:02:32 HOL-Analysis: theory HOL-Analysis.Jordan_Curve
18:02:33 HOL-Analysis: theory HOL-Analysis.Ball_Volume
18:02:34 HOL-Analysis: theory HOL-Analysis.Analysis
18:12:11 Preparing HOL-Analysis/document ...
18:15:17 Finished HOL-Analysis/document (0:03:05 elapsed time)
18:15:17 Preparing HOL-Analysis/manual ...
18:15:42 Finished HOL-Analysis/manual (0:00:25 elapsed time)
18:15:43 Timing HOL-Analysis (8 threads, 567.820s elapsed time, 3877.554s cpu time, 347.491s GC time, factor 6.83)
18:15:43 Finished HOL-Analysis (0:10:47 elapsed time, 1:07:57 cpu time, factor 6.30)
18:15:43 Building Ordinary_Differential_Equations (on hpcisabelle/3) ...
18:15:45 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order
18:15:45 Ordinary_Differential_Equations: theory HOL-Library.Code_Cardinality
18:15:45 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int
18:15:45 Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat
18:15:45 Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence
18:15:45 Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras
18:15:45 Ordinary_Differential_Equations: theory HOL-Library.Log_Nat
18:15:45 Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
18:15:46 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat
18:15:46 Ordinary_Differential_Equations: theory Triangle.Angles
18:15:46 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator
18:15:46 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Vector_Derivative_On
18:15:46 Ordinary_Differential_Equations: theory List-Index.List_Index
18:15:46 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral
18:15:46 Ordinary_Differential_Equations: theory Triangle.Triangle
18:15:47 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Gronwall
18:15:47 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Interval_Integral_HK
18:15:53 Ordinary_Differential_Equations: theory HOL-Library.Interval
18:15:53 Ordinary_Differential_Equations: theory HOL-Library.Float
18:15:56 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral_Float
18:15:56 Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space
18:15:56 Ordinary_Differential_Equations: theory HOL-Library.Interval_Float
18:15:58 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds
18:16:00 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities
18:16:02 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones
18:16:02 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem
18:16:03 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor
18:16:04 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation
18:16:05 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
18:16:06 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow
18:16:11 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map
18:16:11 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution
18:16:11 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE
18:16:14 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis
18:16:16 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow_Congs
18:16:55 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex
18:16:58 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis
18:18:29 Preparing Ordinary_Differential_Equations/document ...
18:18:46 Finished Ordinary_Differential_Equations/document (0:00:16 elapsed time)
18:18:46 Preparing Ordinary_Differential_Equations/outline ...
18:18:52 Finished Ordinary_Differential_Equations/outline (0:00:06 elapsed time)
18:18:52 Timing Ordinary_Differential_Equations (8 threads, 140.842s elapsed time, 711.359s cpu time, 11.885s GC time, factor 5.05)
18:18:52 Finished Ordinary_Differential_Equations (0:02:43 elapsed time, 0:12:36 cpu time, factor 4.62)
18:18:52 Building HOL-ODE-Numerics (on hpcisabelle/4) ...
18:18:55 HOL-ODE-Numerics: theory Automatic_Refinement.Foldi
18:18:55 HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach
18:18:55 HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List
18:18:55 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1
18:18:55 HOL-ODE-Numerics: theory Deriving.Derive_Manager
18:18:55 HOL-ODE-Numerics: theory Deriving.Generator_Aux
18:18:55 HOL-ODE-Numerics: theory Deriving.Comparator
18:18:55 HOL-ODE-Numerics: theory HOL-Library.AList
18:18:56 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot
18:18:56 HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot
18:18:56 HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading
18:18:56 HOL-ODE-Numerics: theory HOL-ex.Quicksort
18:18:56 HOL-ODE-Numerics: theory HOL-Library.Char_ord
18:18:56 HOL-ODE-Numerics: theory Deriving.Equality_Generator
18:18:56 HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax
18:18:56 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
18:18:56 HOL-ODE-Numerics: theory HOL-Combinatorics.List_Permutation
18:18:57 HOL-ODE-Numerics: theory HOL-Library.Option_ord
18:18:57 HOL-ODE-Numerics: theory HOL-Library.Parallel
18:18:57 HOL-ODE-Numerics: theory HOL-Library.Type_Length
18:18:57 HOL-ODE-Numerics: theory Deriving.Equality_Instances
18:18:58 HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
18:18:58 HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
18:18:58 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
18:18:58 HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
18:18:58 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp
18:18:58 HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver
18:18:58 HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms
18:18:58 HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve
18:18:58 HOL-ODE-Numerics: theory Automatic_Refinement.Misc
18:18:58 HOL-ODE-Numerics: theory HOL-Library.RBT_Impl
18:18:58 HOL-ODE-Numerics: theory HOL-Library.Signed_Division
18:18:58 HOL-ODE-Numerics: theory Deriving.Compare
18:18:58 HOL-ODE-Numerics: theory Deriving.Comparator_Generator
18:18:58 HOL-ODE-Numerics: theory HOL-Library.While_Combinator
18:18:59 HOL-ODE-Numerics: theory HOL-Library.Mapping
18:18:59 HOL-ODE-Numerics: theory HOL-Library.Word
18:18:59 HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
18:19:00 HOL-ODE-Numerics: theory Deriving.Countable_Generator
18:19:00 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
18:19:00 HOL-ODE-Numerics: theory Deriving.Compare_Generator
18:19:00 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise
18:19:00 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
18:19:00 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float
18:19:00 HOL-ODE-Numerics: theory Deriving.Compare_Instances
18:19:01 HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real
18:19:01 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
18:19:01 HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
18:19:01 HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
18:19:01 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector
18:19:01 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
18:19:01 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
18:19:02 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
18:19:02 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
18:19:03 HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
18:19:03 HOL-ODE-Numerics: theory Native_Word.Code_Int_Integer_Conversion
18:19:03 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
18:19:03 HOL-ODE-Numerics: theory Show.Show
18:19:03 HOL-ODE-Numerics: theory Word_Lib.More_Arithmetic
18:19:03 HOL-ODE-Numerics: theory Word_Lib.More_Bit_Ring
18:19:04 HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
18:19:05 HOL-ODE-Numerics: theory Show.Show_Instances
18:19:05 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
18:19:05 HOL-ODE-Numerics: theory Collections.SetIterator
18:19:06 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases
18:19:06 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging
18:19:06 HOL-ODE-Numerics: theory Automatic_Refinement.Relators
18:19:06 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
18:19:06 HOL-ODE-Numerics: theory Collections.SetIteratorOperations
18:19:07 HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
18:19:08 HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
18:19:10 HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
18:19:10 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
18:19:10 HOL-ODE-Numerics: theory Word_Lib.Bit_Comprehension
18:19:10 HOL-ODE-Numerics: theory Word_Lib.More_Divides
18:19:10 HOL-ODE-Numerics: theory Word_Lib.Signed_Division_Word
18:19:10 HOL-ODE-Numerics: theory Collections.Assoc_List
18:19:10 HOL-ODE-Numerics: theory Collections.Proper_Iterator
18:19:10 HOL-ODE-Numerics: theory Collections.SetIteratorGA
18:19:11 HOL-ODE-Numerics: theory Collections.Diff_Array
18:19:11 HOL-ODE-Numerics: theory Word_Lib.More_Word
18:19:11 HOL-ODE-Numerics: theory Collections.It_to_It
18:19:12 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
18:19:13 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
18:19:13 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
18:19:13 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
18:19:13 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
18:19:14 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
18:19:14 HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
18:19:14 HOL-ODE-Numerics: theory Word_Lib.Bit_Shifts_Infix_Syntax
18:19:14 HOL-ODE-Numerics: theory Word_Lib.Least_significant_bit
18:19:15 HOL-ODE-Numerics: theory Word_Lib.Most_significant_bit
18:19:15 HOL-ODE-Numerics: theory Word_Lib.Generic_set_bit
18:19:16 HOL-ODE-Numerics: theory Native_Word.Code_Target_Integer_Bit
18:19:16 HOL-ODE-Numerics: theory Native_Word.Word_Type_Copies
18:19:16 HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
18:19:16 HOL-ODE-Numerics: theory Collections.Intf_Comp
18:19:16 HOL-ODE-Numerics: theory Collections.Idx_Iterator
18:19:16 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
18:19:17 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
18:19:17 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
18:19:18 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
18:19:19 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
18:19:19 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
18:19:19 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
18:19:20 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
18:19:24 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
18:19:24 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
18:19:24 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
18:19:24 HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
18:19:24 HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
18:19:24 HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
18:19:27 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
18:19:27 HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
18:19:27 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
18:19:28 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
18:19:30 HOL-ODE-Numerics: theory Native_Word.Code_Target_Int_Bit
18:19:30 HOL-ODE-Numerics: theory Collections.Code_Target_ICF
18:19:31 HOL-ODE-Numerics: theory Native_Word.Uint
18:19:31 HOL-ODE-Numerics: theory Native_Word.Uint32
18:19:31 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
18:19:32 HOL-ODE-Numerics: theory Collections.Gen_Iterator
18:19:32 HOL-ODE-Numerics: theory Collections.Intf_Map
18:19:32 HOL-ODE-Numerics: theory Collections.Intf_Set
18:19:33 HOL-ODE-Numerics: theory Collections.HashCode
18:19:33 HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
18:19:33 HOL-ODE-Numerics: theory Collections.Iterator
18:19:34 HOL-ODE-Numerics: theory Collections.Intf_Hash
18:19:34 HOL-ODE-Numerics: theory Deriving.Hash_Generator
18:19:34 HOL-ODE-Numerics: theory Collections.Array_Iterator
18:19:34 HOL-ODE-Numerics: theory Collections.Gen_Map
18:19:34 HOL-ODE-Numerics: theory Collections.Gen_Map2Set
18:19:35 HOL-ODE-Numerics: theory Collections.Gen_Set
18:19:35 HOL-ODE-Numerics: theory Collections.Impl_List_Set
18:19:35 HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
18:19:35 HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
18:19:36 HOL-ODE-Numerics: theory Collections.Gen_Hash
18:19:36 HOL-ODE-Numerics: theory Deriving.Hash_Instances
18:19:36 HOL-ODE-Numerics: theory Deriving.Derive
18:19:36 HOL-ODE-Numerics: theory Collections.Impl_Array_Map
18:19:36 HOL-ODE-Numerics: theory Collections.Impl_List_Map
18:19:37 HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
18:20:10 HOL-ODE-Numerics: theory HOL-Library.RBT
18:20:10 HOL-ODE-Numerics: theory Collections.RBT_add
18:20:11 HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
18:20:12 HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
18:20:12 HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
18:20:22 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
18:20:23 HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
18:20:30 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
18:20:30 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
18:20:31 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
18:20:35 HOL-ODE-Numerics: theory Affine_Arithmetic.Print
18:20:37 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
18:20:37 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
18:20:38 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
18:20:39 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
18:20:39 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
18:20:39 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
18:20:39 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
18:20:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
18:20:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
18:20:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
18:20:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
18:20:57 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
18:20:57 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
18:21:02 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
18:21:04 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
18:21:05 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
18:21:05 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
18:21:07 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
18:21:26 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
18:21:50 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
18:21:50 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
18:22:07 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
18:22:07 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
18:22:07 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
18:22:08 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
18:22:22 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
18:22:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
18:22:34 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
18:23:01 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
18:23:52 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
18:31:55 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
18:32:30 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
18:33:48 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
18:35:30 Timing HOL-ODE-Numerics (8 threads, 912.954s elapsed time, 5015.882s cpu time, 299.393s GC time, factor 5.49)
18:35:30 Finished HOL-ODE-Numerics (0:16:30 elapsed time, 1:26:46 cpu time, factor 5.26)
18:35:30 Building ZFC_in_HOL (on hpcisabelle/5) ...
18:35:32 ZFC_in_HOL: theory HOL-Cardinals.Fun_More
18:35:32 ZFC_in_HOL: theory HOL-Cardinals.Order_Union
18:35:32 ZFC_in_HOL: theory HOL-Cardinals.Order_Relation_More
18:35:32 ZFC_in_HOL: theory HOL-Library.Nat_Bijection
18:35:32 ZFC_in_HOL: theory HOL-Library.FuncSet
18:35:32 ZFC_in_HOL: theory HOL-Library.Old_Datatype
18:35:32 ZFC_in_HOL: theory HOL-Library.Infinite_Set
18:35:33 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Extension
18:35:33 ZFC_in_HOL: theory HOL-Cardinals.Wellfounded_More
18:35:33 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Relation
18:35:33 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Embedding
18:35:33 ZFC_in_HOL: theory HOL-Library.Countable
18:35:34 ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Constructions
18:35:34 ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Order_Relation
18:35:34 ZFC_in_HOL: theory HOL-Cardinals.Ordinal_Arithmetic
18:35:35 ZFC_in_HOL: theory HOL-Library.Countable_Set
18:35:36 ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Arithmetic
18:35:36 ZFC_in_HOL: theory HOL-Cardinals.Cardinals
18:35:36 ZFC_in_HOL: theory HOL-Library.Equipollence
18:35:36 ZFC_in_HOL: theory HOL-Analysis.Continuum_Not_Denumerable
18:35:37 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Library
18:35:37 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_in_HOL
18:35:38 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Cardinals
18:35:40 ZFC_in_HOL: theory ZFC_in_HOL.Kirby
18:35:40 ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Typeclasses
18:35:41 ZFC_in_HOL: theory ZFC_in_HOL.Ordinal_Exp
18:35:41 ZFC_in_HOL: theory ZFC_in_HOL.Cantor_NF
18:35:42 ZFC_in_HOL: theory ZFC_in_HOL.General_Cardinals
18:36:22 Preparing ZFC_in_HOL/document ...
18:36:32 Finished ZFC_in_HOL/document (0:00:09 elapsed time)
18:36:32 Preparing ZFC_in_HOL/outline ...
18:36:37 Finished ZFC_in_HOL/outline (0:00:05 elapsed time)
18:36:37 Timing ZFC_in_HOL (8 threads, 39.326s elapsed time, 254.712s cpu time, 4.515s GC time, factor 6.48)
18:36:37 Finished ZFC_in_HOL (0:00:50 elapsed time, 0:04:35 cpu time, factor 5.50)
18:36:37 Building CZH_Foundations (on hpcisabelle/6) ...
18:36:39 CZH_Foundations: theory CZH_Foundations.CZH_Utilities
18:36:39 CZH_Foundations: theory CZH_Foundations.CZH_Sets_MIF
18:36:39 CZH_Foundations: theory HOL-Eisbach.Eisbach
18:36:39 CZH_Foundations: theory Conditional_Simplification.CS_Tools
18:36:39 CZH_Foundations: theory Cardinality_Continuum.Cardinality_Continuum_Library
18:36:39 CZH_Foundations: theory CZH_Foundations.CZH_Introduction
18:36:39 CZH_Foundations: theory HOL-Library.Rewrite
18:36:39 CZH_Foundations: theory Intro_Dest_Elim.IHOL_IDE
18:36:39 CZH_Foundations: theory Conditional_Simplification.IHOL_CS
18:36:40 CZH_Foundations: theory Cardinality_Continuum.Cardinality_Continuum
18:36:40 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Introduction
18:36:42 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Sets
18:36:43 CZH_Foundations: theory CZH_Foundations.CZH_Sets_BRelations
18:36:43 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Nat
18:36:46 CZH_Foundations: theory CZH_Foundations.CZH_Sets_IF
18:36:47 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Equipollence
18:36:47 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Cardinality
18:36:48 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Ordinals
18:36:48 CZH_Foundations: theory CZH_Foundations.CZH_Sets_FSequences
18:36:50 CZH_Foundations: theory CZH_Foundations.CZH_Sets_FBRelations
18:36:51 CZH_Foundations: theory CZH_Foundations.CZH_Sets_NOP
18:36:51 CZH_Foundations: theory CZH_Foundations.CZH_Sets_VNHS
18:36:53 CZH_Foundations: theory CZH_Foundations.CZH_DG_Introduction
18:36:53 CZH_Foundations: theory CZH_Foundations.CZH_Sets_ZQR
18:36:59 CZH_Foundations: theory CZH_Foundations.CZH_EX_Replacement
18:36:59 CZH_Foundations: theory CZH_Foundations.CZH_EX_TS
18:36:59 CZH_Foundations: theory CZH_Foundations.CZH_DG_Digraph
18:36:59 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Introduction
18:37:00 CZH_Foundations: theory CZH_Foundations.CZH_EX_Algebra
18:37:01 CZH_Foundations: theory CZH_Foundations.CZH_DG_DGHM
18:37:02 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_Digraph
18:37:02 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Semicategory
18:37:03 CZH_Foundations: theory CZH_Foundations.CZH_Sets_Conclusions
18:37:06 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_Semicategory
18:37:19 CZH_Foundations: theory CZH_Foundations.CZH_DG_TDGHM
18:37:19 CZH_Foundations: theory CZH_Foundations.CZH_DG_GRPH
18:37:19 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_DGHM
18:37:19 CZH_Foundations: theory CZH_Foundations.CZH_DG_Subdigraph
18:37:20 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Semifunctor
18:37:25 CZH_Foundations: theory CZH_Foundations.CZH_DG_Rel
18:37:27 CZH_Foundations: theory CZH_Foundations.CZH_DG_Par
18:37:28 CZH_Foundations: theory CZH_Foundations.CZH_DG_Simple
18:37:28 CZH_Foundations: theory CZH_Foundations.CZH_DG_PDigraph
18:37:28 CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_TDGHM
18:37:28 CZH_Foundations: theory CZH_Foundations.CZH_SMC_GRPH
18:37:29 CZH_Foundations: theory CZH_Foundations.CZH_DG_Set
18:37:36 CZH_Foundations: theory CZH_Foundations.CZH_DG_Conclusions
18:37:45 CZH_Foundations: theory CZH_Foundations.CZH_DG_SemiCAT
18:37:45 CZH_Foundations: theory CZH_Foundations.CZH_SMC_NTSMCF
18:37:45 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Subsemicategory
18:37:45 CZH_Foundations: theory CZH_Foundations.CZH_SMC_PSemicategory
18:37:46 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Rel
18:37:46 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_Semifunctor
18:37:58 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Simple
18:37:58 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_NTSMCF
18:37:59 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Par
18:37:59 CZH_Foundations: theory CZH_Foundations.CZH_SMC_SemiCAT
18:38:00 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Set
18:38:09 CZH_Foundations: theory CZH_Foundations.CZH_SMC_Conclusions
18:38:56 Preparing CZH_Foundations/document ...
18:40:18 Finished CZH_Foundations/document (0:01:22 elapsed time)
18:40:18 Preparing CZH_Foundations/outline ...
18:41:06 Finished CZH_Foundations/outline (0:00:47 elapsed time)
18:41:06 Timing CZH_Foundations (8 threads, 125.022s elapsed time, 807.635s cpu time, 89.967s GC time, factor 6.46)
18:41:06 Finished CZH_Foundations (0:02:16 elapsed time, 0:13:52 cpu time, factor 6.09)
18:41:06 Building CZH_Elementary_Categories (on hpcisabelle/7) ...
18:41:08 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Introduction
18:41:09 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Category
18:41:17 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Functor
18:41:17 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Category
18:41:20 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_GRPH
18:41:41 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_NTCF
18:41:42 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Order
18:41:42 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_DG_CAT
18:41:42 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Subcategory
18:41:42 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Rel
18:41:42 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Functor
18:41:52 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Parallel
18:41:52 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_SS
18:41:53 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Order
18:42:01 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Ordinal
18:42:02 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_CSimplicial
18:42:03 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Par
18:42:08 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_PCategory
18:42:08 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Simple
18:42:09 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_NTCF
18:42:10 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Comma
18:42:16 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Discrete
18:42:18 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_SemiCAT
18:42:22 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_SMC_CAT
18:42:23 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_CAT
18:42:28 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_DG_FUNCT
18:42:30 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Set
18:42:36 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Hom
18:42:37 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Structure_Example
18:42:45 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_SMC_FUNCT
18:42:49 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_FUNCT
18:43:03 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Cone
18:43:04 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Yoneda
18:43:22 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Cone
18:43:41 CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Conclusions
18:50:41 Preparing CZH_Elementary_Categories/document ...
18:52:42 Finished CZH_Elementary_Categories/document (0:02:00 elapsed time)
18:52:42 Preparing CZH_Elementary_Categories/outline ...
18:53:39 Finished CZH_Elementary_Categories/outline (0:00:56 elapsed time)
18:53:39 Timing CZH_Elementary_Categories (8 threads, 561.286s elapsed time, 2529.281s cpu time, 243.174s GC time, factor 4.51)
18:53:39 Finished CZH_Elementary_Categories (0:09:33 elapsed time, 0:42:34 cpu time, factor 4.46)
18:53:39 Building Lorenz_Approximation (on hpcisabelle/0) ...
18:53:43 Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
18:53:48 Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
18:54:08 Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
18:58:07 Timing Lorenz_Approximation (8 threads, 240.697s elapsed time, 608.994s cpu time, 24.651s GC time, factor 2.53)
18:58:07 Finished Lorenz_Approximation (0:04:26 elapsed time, 0:10:57 cpu time, factor 2.46)
18:58:07 Building HOL-Library (on hpcisabelle/1) ...
18:58:08 HOL-Library: theory HOL-Library.README
18:58:08 HOL-Library: theory HOL-Library.AList
18:58:08 HOL-Library: theory HOL-Library.Adhoc_Overloading
18:58:08 HOL-Library: theory HOL-Library.BNF_Axiomatization
18:58:08 HOL-Library: theory HOL-Library.BNF_Corec
18:58:08 HOL-Library: theory HOL-Library.Cancellation
18:58:08 HOL-Library: theory HOL-Library.Case_Converter
18:58:08 HOL-Library: theory HOL-Library.Char_ord
18:58:08 HOL-Library: theory HOL-Library.Centered_Division
18:58:09 HOL-Library: theory HOL-Library.Code_Abstract_Char
18:58:09 HOL-Library: theory HOL-Library.Code_Abstract_Nat
18:58:09 HOL-Library: theory HOL-Library.Code_Prolog
18:58:09 HOL-Library: theory HOL-Library.Monad_Syntax
18:58:09 HOL-Library: theory HOL-Library.Code_Binary_Nat
18:58:09 HOL-Library: theory HOL-Library.State_Monad
18:58:09 HOL-Library: theory HOL-Library.Code_Target_Nat
18:58:10 HOL-Library: theory HOL-Library.Code_Lazy
18:58:10 HOL-Library: theory HOL-Library.Simps_Case_Conv
18:58:10 HOL-Library: theory HOL-Library.Extended
18:58:10 HOL-Library: theory HOL-Library.Multiset
18:58:10 HOL-Library: theory HOL-Library.Code_Target_Int
18:58:11 HOL-Library: theory HOL-Library.Code_Test
18:58:11 HOL-Library: theory HOL-Library.Code_Target_Numeral
18:58:11 HOL-Library: theory HOL-Library.Combine_PER
18:58:11 HOL-Library: theory HOL-Library.Comparator
18:58:11 HOL-Library: theory HOL-Library.Complete_Partial_Order2
18:58:11 HOL-Library: theory HOL-Library.DAList
18:58:12 HOL-Library: theory HOL-Library.Conditional_Parametricity
18:58:12 HOL-Library: theory HOL-Library.Confluence
18:58:12 HOL-Library: theory HOL-Library.Confluent_Quotient
18:58:12 HOL-Library: theory HOL-Library.Datatype_Records
18:58:12 HOL-Library: theory HOL-Library.Debug
18:58:12 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
18:58:12 HOL-Library: theory HOL-Library.Dlist
18:58:12 HOL-Library: theory HOL-Library.Fun_Lexorder
18:58:13 HOL-Library: theory HOL-Library.FuncSet
18:58:13 HOL-Library: theory HOL-Library.Function_Algebras
18:58:13 HOL-Library: theory HOL-Library.Groups_Big_Fun
18:58:13 HOL-Library: theory HOL-Library.Function_Division
18:58:14 HOL-Library: theory HOL-Library.IArray
18:58:14 HOL-Library: theory HOL-Library.Infinite_Set
18:58:14 HOL-Library: theory HOL-Library.Disjoint_Sets
18:58:14 HOL-Library: theory HOL-Library.LaTeXsugar
18:58:14 HOL-Library: theory HOL-Library.Lattice_Constructions
18:58:14 HOL-Library: theory HOL-Library.Omega_Words_Fun
18:58:14 HOL-Library: theory HOL-Library.ListVector
18:58:15 HOL-Library: theory HOL-Library.List_Lenlexorder
18:58:15 HOL-Library: theory HOL-Library.List_Lexorder
18:58:15 HOL-Library: theory HOL-Library.Mapping
18:58:15 HOL-Library: theory HOL-Library.More_List
18:58:15 HOL-Library: theory HOL-Library.NList
18:58:15 HOL-Library: theory HOL-Library.Nat_Bijection
18:58:16 HOL-Library: theory HOL-Library.Poly_Mapping
18:58:16 HOL-Library: theory HOL-Library.Stream
18:58:19 HOL-Library: theory HOL-Library.Old_Datatype
18:58:19 HOL-Library: theory HOL-Library.AList_Mapping
18:58:20 HOL-Library: theory HOL-Library.Old_Recdef
18:58:20 HOL-Library: theory HOL-Library.Open_State_Syntax
18:58:20 HOL-Library: theory HOL-Library.Option_ord
18:58:21 HOL-Library: theory HOL-Library.Parallel
18:58:21 HOL-Library: theory HOL-Library.Pattern_Aliases
18:58:21 HOL-Library: theory HOL-Library.Phantom_Type
18:58:21 HOL-Library: theory HOL-Library.Power_By_Squaring
18:58:21 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
18:58:21 HOL-Library: theory HOL-Library.DAList_Multiset
18:58:21 HOL-Library: theory HOL-Library.Multiset_Order
18:58:21 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
18:58:21 HOL-Library: theory HOL-Library.Preorder
18:58:22 HOL-Library: theory HOL-Library.Cardinality
18:58:23 HOL-Library: theory HOL-Library.Product_Lexorder
18:58:23 HOL-Library: theory HOL-Library.Product_Plus
18:58:23 HOL-Library: theory HOL-Library.Quotient_Syntax
18:58:23 HOL-Library: theory HOL-Library.Quotient_Option
18:58:23 HOL-Library: theory HOL-Library.Quotient_Product
18:58:23 HOL-Library: theory HOL-Library.Quotient_Set
18:58:23 HOL-Library: theory HOL-Library.Quotient_Sum
18:58:23 HOL-Library: theory HOL-Library.Product_Order
18:58:23 HOL-Library: theory HOL-Library.Quotient_Type
18:58:23 HOL-Library: theory HOL-Library.RBT_Impl
18:58:23 HOL-Library: theory HOL-Library.Realizers
18:58:23 HOL-Library: theory HOL-Library.Quotient_List
18:58:24 HOL-Library: theory HOL-Library.Reflection
18:58:24 HOL-Library: theory HOL-Library.Finite_Lattice
18:58:24 HOL-Library: theory HOL-Library.Refute
18:58:24 HOL-Library: theory HOL-Library.Rewrite
18:58:25 HOL-Library: theory HOL-Library.Set_Algebras
18:58:25 HOL-Library: theory HOL-Library.Signed_Division
18:58:25 HOL-Library: theory HOL-Library.Code_Cardinality
18:58:26 HOL-Library: theory HOL-Library.Numeral_Type
18:58:26 HOL-Library: theory HOL-Library.Sorting_Algorithms
18:58:26 HOL-Library: theory HOL-Library.Sublist
18:58:27 HOL-Library: theory HOL-Library.Transitive_Closure_Table
18:58:27 HOL-Library: theory HOL-Library.Tree
18:58:27 HOL-Library: theory HOL-Library.Uprod
18:58:27 HOL-Library: theory HOL-Library.Type_Length
18:58:27 HOL-Library: theory HOL-Library.While_Combinator
18:58:28 HOL-Library: theory HOL-Library.Z2
18:58:28 HOL-Library: theory HOL-Library.Saturated
18:58:28 HOL-Library: theory HOL-Library.Word
18:58:28 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
18:58:28 HOL-Library: theory HOL-Library.Countable
18:58:28 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
18:58:28 HOL-Library: theory HOL-Library.Prefix_Order
18:58:28 HOL-Library: theory HOL-Library.Subseq_Order
18:58:28 HOL-Library: theory HOL-Library.Complex_Order
18:58:28 HOL-Library: theory HOL-Library.Diagonal_Subsequence
18:58:28 HOL-Library: theory HOL-Library.Discrete
18:58:28 HOL-Library: theory HOL-Library.Going_To_Filter
18:58:28 HOL-Library: theory HOL-Library.Indicator_Function
18:58:29 HOL-Library: theory HOL-Library.Infinite_Typeclass
18:58:29 HOL-Library: theory HOL-Library.Landau_Symbols
18:58:29 HOL-Library: theory HOL-Library.Lattice_Algebras
18:58:29 HOL-Library: theory HOL-Library.Countable_Set
18:58:29 HOL-Library: theory HOL-Library.FSet
18:58:29 HOL-Library: theory HOL-Library.Tree_Multiset
18:58:30 HOL-Library: theory HOL-Library.Liminf_Limsup
18:58:30 HOL-Library: theory HOL-Library.Countable_Complete_Lattices
18:58:30 HOL-Library: theory HOL-Library.Countable_Set_Type
18:58:32 HOL-Library: theory HOL-Library.Equipollence
18:58:32 HOL-Library: theory HOL-Library.Set_Idioms
18:58:33 HOL-Library: theory HOL-Library.Ramsey
18:58:33 HOL-Library: theory HOL-Library.Log_Nat
18:58:33 HOL-Library: theory HOL-Library.Lub_Glb
18:58:33 HOL-Library: theory HOL-Library.Nonpos_Ints
18:58:33 HOL-Library: theory HOL-Library.Finite_Map
18:58:33 HOL-Library: theory HOL-Library.OptionalSugar
18:58:33 HOL-Library: theory HOL-Library.Order_Continuity
18:58:33 HOL-Library: theory HOL-Library.Periodic_Fun
18:58:33 HOL-Library: theory HOL-Library.Quadratic_Discriminant
18:58:33 HOL-Library: theory HOL-Library.Real_Mod
18:58:34 HOL-Library: theory HOL-Library.Sum_of_Squares
18:58:34 HOL-Library: theory HOL-Library.Extended_Nat
18:58:34 HOL-Library: theory HOL-Library.Tree_Real
18:58:35 HOL-Library: theory HOL-Library.Extended_Real
18:58:35 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
18:58:35 HOL-Library: theory HOL-Library.Interval
18:58:37 HOL-Library: theory HOL-Library.Float
18:58:40 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
18:58:40 HOL-Library: theory HOL-Library.Code_Target_Numeral_Float
18:58:40 HOL-Library: theory HOL-Library.Interval_Float
18:58:49 HOL-Library: theory HOL-Library.Disjoint_FSets
18:58:49 HOL-Library: theory HOL-Library.Library
18:59:33 HOL-Library: theory HOL-Library.RBT
18:59:34 HOL-Library: theory HOL-Library.RBT_Mapping
18:59:34 HOL-Library: theory HOL-Library.RBT_Set
19:01:49 Preparing HOL-Library/document ...
19:02:53 Finished HOL-Library/document (0:01:04 elapsed time)
19:02:53 Preparing HOL-Library/outline ...
19:03:31 Finished HOL-Library/outline (0:00:37 elapsed time)
19:03:32 Timing HOL-Library (8 threads, 181.734s elapsed time, 1225.214s cpu time, 60.180s GC time, factor 6.74)
19:03:32 Finished HOL-Library (0:03:37 elapsed time, 0:21:49 cpu time, factor 6.03)
19:03:32 Running Lorenz_C0 (on hpcisabelle/2) ...
19:03:36 Lorenz_C0: theory Lorenz_C0.Lorenz_C0
19:28:08 Timing Lorenz_C0 (8 threads, 1471.911s elapsed time, 11610.545s cpu time, 23.801s GC time, factor 7.89)
19:28:08 Finished Lorenz_C0 (0:24:36 elapsed time, 3:13:36 cpu time, factor 7.87)
19:28:08 Building Simpl (on hpcisabelle/3) ...
19:28:10 Simpl: theory HOL-Library.LaTeXsugar
19:28:10 Simpl: theory HOL-Library.Cancellation
19:28:10 Simpl: theory HOL-Library.Old_Recdef
19:28:10 Simpl: theory HOL-Statespace.DistinctTreeProver
19:28:10 Simpl: theory Simpl.Simpl_Heap
19:28:10 Simpl: theory Simpl.HeapList
19:28:11 Simpl: theory HOL-Library.Multiset
19:28:12 Simpl: theory Simpl.Generalise
19:28:12 Simpl: theory HOL-Statespace.StateFun
19:28:13 Simpl: theory Simpl.Language
19:28:13 Simpl: theory HOL-Statespace.StateSpaceLocale
19:28:13 Simpl: theory HOL-Statespace.StateSpaceSyntax
19:28:20 Simpl: theory Simpl.Semantic
19:28:26 Simpl: theory Simpl.HoarePartialDef
19:28:26 Simpl: theory Simpl.Termination
19:28:27 Simpl: theory Simpl.HoarePartialProps
19:28:27 Simpl: theory Simpl.HoareTotalDef
19:28:27 Simpl: theory Simpl.SmallStep
19:28:28 Simpl: theory Simpl.HoarePartial
19:28:28 Simpl: theory Simpl.AlternativeSmallStep
19:28:30 Simpl: theory Simpl.HoareTotalProps
19:28:31 Simpl: theory Simpl.Compose
19:28:31 Simpl: theory Simpl.HoareTotal
19:28:34 Simpl: theory Simpl.Hoare
19:28:34 Simpl: theory Simpl.Closure
19:28:34 Simpl: theory Simpl.StateSpace
19:28:35 Simpl: theory Simpl.Vcg
19:28:43 Simpl: theory Simpl.ProcParEx
19:28:43 Simpl: theory Simpl.ProcParExSP
19:28:43 Simpl: theory Simpl.XVcg
19:28:43 Simpl: theory Simpl.XVcgEx
19:28:43 Simpl: theory Simpl.ClosureEx
19:28:43 Simpl: theory Simpl.ComposeEx
19:28:43 Simpl: theory Simpl.Quicksort
19:28:43 Simpl: theory Simpl.SyntaxTest
19:28:43 Simpl: theory Simpl.UserGuide
19:28:43 Simpl: theory Simpl.VcgEx
19:28:43 Simpl: theory Simpl.VcgExSP
19:28:43 Simpl: theory Simpl.VcgExTotal
19:28:48 Simpl: theory Simpl.Simpl
19:29:23 Preparing Simpl/document ...
19:29:59 Finished Simpl/document (0:00:35 elapsed time)
19:29:59 Preparing Simpl/outline ...
19:30:16 Finished Simpl/outline (0:00:17 elapsed time)
19:30:16 Timing Simpl (8 threads, 52.379s elapsed time, 337.398s cpu time, 12.827s GC time, factor 6.44)
19:30:16 Finished Simpl (0:01:11 elapsed time, 0:06:21 cpu time, factor 5.33)
19:30:17 Running CZH_Universal_Constructions (on hpcisabelle/4) ...
19:30:18 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Introduction
19:30:18 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Pointed
19:30:19 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Universal
19:30:33 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit
19:31:14 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Adjoints
19:31:14 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Equalizer
19:31:14 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_IT
19:31:15 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Product
19:31:15 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Limit_Pullback
19:31:15 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Representable
19:31:38 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Comma
19:32:04 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Kan
19:32:07 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Complete
19:32:11 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Set
19:32:48 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan
19:33:24 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_PWKan_Example
19:33:34 CZH_Universal_Constructions: theory CZH_Universal_Constructions.CZH_UCAT_Conclusions
19:52:30 Preparing CZH_Universal_Constructions/document ...
19:53:37 Finished CZH_Universal_Constructions/document (0:01:06 elapsed time)
19:53:37 Preparing CZH_Universal_Constructions/outline ...
19:54:02 Finished CZH_Universal_Constructions/outline (0:00:25 elapsed time)
19:54:02 Timing CZH_Universal_Constructions (8 threads, 1328.072s elapsed time, 5078.274s cpu time, 315.704s GC time, factor 3.82)
19:54:02 Finished CZH_Universal_Constructions (0:22:11 elapsed time, 1:24:48 cpu time, factor 3.82)
19:54:03 Building Echelon_Form (on hpcisabelle/5) ...
19:54:05 Echelon_Form: theory HOL-Library.Code_Abstract_Nat
19:54:05 Echelon_Form: theory HOL-Computational_Algebra.Fraction_Field
19:54:05 Echelon_Form: theory HOL-Library.Code_Target_Int
19:54:05 Echelon_Form: theory HOL-Library.Function_Algebras
19:54:05 Echelon_Form: theory HOL-Library.More_List
19:54:05 Echelon_Form: theory HOL-Library.IArray
19:54:05 Echelon_Form: theory HOL-Library.Code_Cardinality
19:54:05 Echelon_Form: theory HOL-Library.Z2
19:54:05 Echelon_Form: theory HOL-Library.Code_Target_Nat
19:54:05 Echelon_Form: theory HOL-Computational_Algebra.Field_as_Ring
19:54:06 Echelon_Form: theory Cayley_Hamilton.Square_Matrix
19:54:06 Echelon_Form: theory HOL-Computational_Algebra.Polynomial
19:54:06 Echelon_Form: theory HOL-Library.Code_Target_Numeral
19:54:06 Echelon_Form: theory Gauss_Jordan.Code_Set
19:54:06 Echelon_Form: theory Gauss_Jordan.Code_Z2
19:54:06 Echelon_Form: theory Rank_Nullity_Theorem.Dual_Order
19:54:06 Echelon_Form: theory Gauss_Jordan.IArray_Addenda
19:54:06 Echelon_Form: theory Rank_Nullity_Theorem.Mod_Type
19:54:07 Echelon_Form: theory HOL-Computational_Algebra.Normalized_Fraction
19:54:10 Echelon_Form: theory Rank_Nullity_Theorem.Miscellaneous
19:54:12 Echelon_Form: theory Gauss_Jordan.Code_Matrix
19:54:12 Echelon_Form: theory Gauss_Jordan.Rref
19:54:12 Echelon_Form: theory Rank_Nullity_Theorem.Fundamental_Subspaces
19:54:13 Echelon_Form: theory Rank_Nullity_Theorem.Dim_Formula
19:54:13 Echelon_Form: theory Gauss_Jordan.Elementary_Operations
19:54:13 Echelon_Form: theory Gauss_Jordan.Rank
19:54:14 Echelon_Form: theory Gauss_Jordan.Matrix_To_IArray
19:54:14 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan
19:54:16 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_IArrays
19:54:16 Echelon_Form: theory Gauss_Jordan.Linear_Maps
19:54:17 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA
19:54:18 Echelon_Form: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
19:54:18 Echelon_Form: theory Gauss_Jordan.Determinants2
19:54:18 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays
19:54:18 Echelon_Form: theory Gauss_Jordan.Inverse
19:54:18 Echelon_Form: theory Gauss_Jordan.System_Of_Equations
19:54:19 Echelon_Form: theory HOL-Computational_Algebra.Polynomial_Factorial
19:54:19 Echelon_Form: theory Cayley_Hamilton.Cayley_Hamilton
19:54:19 Echelon_Form: theory Gauss_Jordan.Inverse_IArrays
19:54:19 Echelon_Form: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
19:54:20 Echelon_Form: theory Echelon_Form.Rings2
19:54:56 Echelon_Form: theory Echelon_Form.Cayley_Hamilton_Compatible
19:54:58 Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton
19:54:58 Echelon_Form: theory Echelon_Form.Echelon_Form
19:55:00 Echelon_Form: theory Echelon_Form.Echelon_Form_Det
19:55:00 Echelon_Form: theory Echelon_Form.Echelon_Form_IArrays
19:55:01 Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse
19:55:01 Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_Abstract
19:55:02 Echelon_Form: theory Echelon_Form.Echelon_Form_Det_IArrays
19:55:03 Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton_IArrays
19:55:03 Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse_IArrays
19:55:04 Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_IArrays
19:56:50 Preparing Echelon_Form/document ...
19:56:55 Finished Echelon_Form/document (0:00:05 elapsed time)
19:56:55 Preparing Echelon_Form/outline ...
19:56:58 Finished Echelon_Form/outline (0:00:03 elapsed time)
19:56:59 Timing Echelon_Form (8 threads, 141.686s elapsed time, 885.522s cpu time, 31.330s GC time, factor 6.25)
19:56:59 Finished Echelon_Form (0:02:44 elapsed time, 0:15:32 cpu time, factor 5.66)
19:56:59 Building HOL-Computational_Algebra (on hpcisabelle/6) ...
19:57:01 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field
19:57:01 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring
19:57:01 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure
19:57:12 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm
19:57:26 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction
19:57:26 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring
19:57:26 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes
19:57:35 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree
19:57:35 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series
19:57:35 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers
19:57:35 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial
19:57:47 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
19:57:48 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS
19:57:48 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial
19:57:48 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Laurent_Series
19:57:53 HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra
19:58:23 Preparing HOL-Computational_Algebra/document ...
19:58:49 Finished HOL-Computational_Algebra/document (0:00:25 elapsed time)
19:58:49 Preparing HOL-Computational_Algebra/outline ...
19:59:02 Finished HOL-Computational_Algebra/outline (0:00:12 elapsed time)
19:59:02 Timing HOL-Computational_Algebra (8 threads, 66.747s elapsed time, 269.242s cpu time, 5.778s GC time, factor 4.03)
19:59:02 Finished HOL-Computational_Algebra (0:01:23 elapsed time, 0:05:01 cpu time, factor 3.63)
19:59:02 Building HOL-Probability (on hpcisabelle/7) ...
19:59:04 HOL-Probability: theory HOL-Library.Rewrite
19:59:04 HOL-Probability: theory HOL-Library.AList
19:59:04 HOL-Probability: theory HOL-Library.Complete_Partial_Order2
19:59:04 HOL-Probability: theory HOL-Library.Adhoc_Overloading
19:59:04 HOL-Probability: theory HOL-Library.Conditional_Parametricity
19:59:04 HOL-Probability: theory HOL-Library.Stream
19:59:04 HOL-Probability: theory HOL-Library.Tree
19:59:04 HOL-Probability: theory HOL-Library.Sublist
19:59:05 HOL-Probability: theory HOL-Library.Monad_Syntax
19:59:05 HOL-Probability: theory HOL-Library.FSet
19:59:06 HOL-Probability: theory HOL-Combinatorics.Multiset_Permutations
19:59:06 HOL-Probability: theory HOL-Library.Diagonal_Subsequence
19:59:06 HOL-Probability: theory HOL-Probability.Discrete_Topology
19:59:07 HOL-Probability: theory HOL-Probability.Essential_Supremum
19:59:07 HOL-Probability: theory HOL-Probability.Probability_Measure
19:59:07 HOL-Probability: theory HOL-Probability.Stopping_Time
19:59:08 HOL-Probability: theory HOL-Library.Mapping
19:59:09 HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams
19:59:10 HOL-Probability: theory HOL-Probability.Tree_Space
19:59:10 HOL-Probability: theory HOL-Library.AList_Mapping
19:59:11 HOL-Probability: theory HOL-Probability.Conditional_Expectation
19:59:11 HOL-Probability: theory HOL-Probability.Distribution_Functions
19:59:11 HOL-Probability: theory HOL-Probability.Giry_Monad
19:59:12 HOL-Probability: theory HOL-Probability.Weak_Convergence
19:59:12 HOL-Probability: theory HOL-Probability.Helly_Selection
19:59:12 HOL-Probability: theory HOL-Library.Finite_Map
19:59:13 HOL-Probability: theory HOL-Probability.Probability_Mass_Function
19:59:13 HOL-Probability: theory HOL-Probability.Projective_Family
19:59:14 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
19:59:15 HOL-Probability: theory HOL-Probability.Independent_Family
19:59:15 HOL-Probability: theory HOL-Probability.Stream_Space
19:59:16 HOL-Probability: theory HOL-Probability.PMF_Impl
19:59:16 HOL-Probability: theory HOL-Probability.Random_Permutations
19:59:16 HOL-Probability: theory HOL-Probability.SPMF
19:59:16 HOL-Probability: theory HOL-Probability.Convolution
19:59:16 HOL-Probability: theory HOL-Probability.Information
19:59:17 HOL-Probability: theory HOL-Probability.Product_PMF
19:59:18 HOL-Probability: theory HOL-Probability.Hoeffding
19:59:19 HOL-Probability: theory HOL-Probability.Distributions
19:59:21 HOL-Probability: theory HOL-Probability.Sinc_Integral
19:59:21 HOL-Probability: theory HOL-Probability.Characteristic_Functions
19:59:22 HOL-Probability: theory HOL-Probability.Levy
19:59:23 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
19:59:27 HOL-Probability: theory HOL-Probability.Fin_Map
19:59:28 HOL-Probability: theory HOL-Probability.Projective_Limit
19:59:31 HOL-Probability: theory HOL-Probability.Probability
20:00:42 Preparing HOL-Probability/document ...
20:01:03 Finished HOL-Probability/document (0:00:21 elapsed time)
20:01:03 Preparing HOL-Probability/outline ...
20:01:11 Finished HOL-Probability/outline (0:00:07 elapsed time)
20:01:12 Timing HOL-Probability (8 threads, 73.082s elapsed time, 493.894s cpu time, 14.242s GC time, factor 6.76)
20:01:12 Finished HOL-Probability (0:01:37 elapsed time, 0:09:04 cpu time, factor 5.60)
20:01:12 Building Automatic_Refinement (on hpcisabelle/0) ...
20:01:13 Automatic_Refinement: theory HOL-Eisbach.Eisbach
20:01:13 Automatic_Refinement: theory Automatic_Refinement.Foldi
20:01:13 Automatic_Refinement: theory Automatic_Refinement.Prio_List
20:01:13 Automatic_Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1
20:01:13 Automatic_Refinement: theory HOL-Library.Cancellation
20:01:13 Automatic_Refinement: theory HOL-Library.Infinite_Set
20:01:13 Automatic_Refinement: theory HOL-Library.Option_ord
20:01:13 Automatic_Refinement: theory Automatic_Refinement.Mk_Term_Antiquot
20:01:13 Automatic_Refinement: theory Automatic_Refinement.Mpat_Antiquot
20:01:14 Automatic_Refinement: theory Automatic_Refinement.Refine_Util
20:01:15 Automatic_Refinement: theory Automatic_Refinement.Attr_Comb
20:01:15 Automatic_Refinement: theory Automatic_Refinement.Anti_Unification
20:01:15 Automatic_Refinement: theory Automatic_Refinement.Indep_Vars
20:01:15 Automatic_Refinement: theory Automatic_Refinement.Mk_Record_Simp
20:01:15 Automatic_Refinement: theory Automatic_Refinement.Tagged_Solver
20:01:15 Automatic_Refinement: theory Automatic_Refinement.Select_Solve
20:01:15 Automatic_Refinement: theory HOL-Library.Multiset
20:01:15 Automatic_Refinement: theory Automatic_Refinement.Named_Sorted_Thms
20:01:21 Automatic_Refinement: theory HOL-ex.Quicksort
20:01:22 Automatic_Refinement: theory Automatic_Refinement.Misc
20:01:29 Automatic_Refinement: theory Automatic_Refinement.Refine_Lib
20:01:31 Automatic_Refinement: theory Automatic_Refinement.Param_Chapter
20:01:31 Automatic_Refinement: theory Automatic_Refinement.Relators
20:01:32 Automatic_Refinement: theory Automatic_Refinement.Param_Tool
20:01:32 Automatic_Refinement: theory Automatic_Refinement.Param_HOL
20:01:34 Automatic_Refinement: theory Automatic_Refinement.Parametricity
20:01:34 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tagging
20:01:34 Automatic_Refinement: theory Automatic_Refinement.Autoref_Phases
20:01:34 Automatic_Refinement: theory Automatic_Refinement.Autoref_Data
20:01:34 Automatic_Refinement: theory Automatic_Refinement.Autoref_Id_Ops
20:01:35 Automatic_Refinement: theory Automatic_Refinement.Autoref_Fix_Rel
20:01:36 Automatic_Refinement: theory Automatic_Refinement.Autoref_Translate
20:01:36 Automatic_Refinement: theory Automatic_Refinement.Autoref_Relator_Interface
20:01:36 Automatic_Refinement: theory Automatic_Refinement.Autoref_Gen_Algo
20:01:36 Automatic_Refinement: theory Automatic_Refinement.Autoref_Chapter
20:01:36 Automatic_Refinement: theory Automatic_Refinement.Autoref_Tool
20:01:37 Automatic_Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL
20:01:41 Automatic_Refinement: theory Automatic_Refinement.Automatic_Refinement
20:01:52 Preparing Automatic_Refinement/document ...
20:01:55 Finished Automatic_Refinement/document (0:00:03 elapsed time)
20:01:55 Preparing Automatic_Refinement/outline ...
20:01:57 Finished Automatic_Refinement/outline (0:00:02 elapsed time)
20:01:57 Timing Automatic_Refinement (8 threads, 28.338s elapsed time, 121.959s cpu time, 3.657s GC time, factor 4.30)
20:01:57 Finished Automatic_Refinement (0:00:38 elapsed time, 0:02:21 cpu time, factor 3.64)
20:01:58 Building AutoCorres2_Main (on hpcisabelle/1) ...
20:01:59 AutoCorres2_Main: theory AutoCorres2.ML_Fun_Cache
20:01:59 AutoCorres2_Main: theory AutoCorres2.MkTermAntiquote
20:01:59 AutoCorres2_Main: theory AutoCorres2.TermPatternAntiquote
20:01:59 AutoCorres2_Main: theory HOL-Eisbach.Eisbach
20:01:59 AutoCorres2_Main: theory AutoCorres2.Introduction_AutoCorres2
20:01:59 AutoCorres2_Main: theory AutoCorres2.ML_Infer_Instantiate
20:01:59 AutoCorres2_Main: theory AutoCorres2.ML_Record_Antiquotation
20:01:59 AutoCorres2_Main: theory AutoCorres2.MapExtra
20:01:59 AutoCorres2_Main: theory AutoCorres2.Misc_Antiquotation
20:02:00 AutoCorres2_Main: theory AutoCorres2.Named_Rules
20:02:00 AutoCorres2_Main: theory AutoCorres2.Padding
20:02:00 AutoCorres2_Main: theory AutoCorres2.Print_Annotated
20:02:00 AutoCorres2_Main: theory AutoCorres2.StaticFun
20:02:00 AutoCorres2_Main: theory AutoCorres2.Subgoals
20:02:00 AutoCorres2_Main: theory AutoCorres2.AutoCorres_Utils
20:02:00 AutoCorres2_Main: theory AutoCorres2.Option_Scanner
20:02:00 AutoCorres2_Main: theory AutoCorres2.Target_Architecture
20:02:00 AutoCorres2_Main: theory AutoCorres2.Tuple_Tools
20:02:00 AutoCorres2_Main: theory HOL-Library.Adhoc_Overloading
20:02:00 AutoCorres2_Main: theory HOL-Library.Code_Abstract_Nat
20:02:01 AutoCorres2_Main: theory HOL-Library.Complete_Partial_Order2
20:02:01 AutoCorres2_Main: theory HOL-Library.Code_Binary_Nat
20:02:01 AutoCorres2_Main: theory HOL-Library.Monad_Syntax
20:02:01 AutoCorres2_Main: theory AutoCorres2.MapExtraTrans
20:02:01 AutoCorres2_Main: theory HOL-Library.Phantom_Type
20:02:01 AutoCorres2_Main: theory AutoCorres2.Less_Monad_Syntax
20:02:01 AutoCorres2_Main: theory HOL-Library.Signed_Division
20:02:01 AutoCorres2_Main: theory HOL-Library.Sublist
20:02:02 AutoCorres2_Main: theory HOL-Eisbach.Eisbach_Tools
20:02:02 AutoCorres2_Main: theory AutoCorres2.Cong_Tactic
20:02:02 AutoCorres2_Main: theory AutoCorres2.Tagging
20:02:02 AutoCorres2_Main: theory AutoCorres2.Match_Cterm
20:02:02 AutoCorres2_Main: theory AutoCorres2.Simp_Trace
20:02:02 AutoCorres2_Main: theory HOL-Library.Cardinality
20:02:03 AutoCorres2_Main: theory AutoCorres2.PrettyProgs
20:02:03 AutoCorres2_Main: theory Word_Lib.Enumeration
20:02:03 AutoCorres2_Main: theory Word_Lib.Even_More_List
20:02:04 AutoCorres2_Main: theory AutoCorres2.IndirectCalls
20:02:04 AutoCorres2_Main: theory Word_Lib.More_Bit_Ring
20:02:04 AutoCorres2_Main: theory Word_Lib.More_Misc
20:02:04 AutoCorres2_Main: theory AutoCorres2.Basic_Runs_To_VCG
20:02:04 AutoCorres2_Main: theory HOL-Library.Numeral_Type
20:02:05 AutoCorres2_Main: theory HOL-Library.Prefix_Order
20:02:05 AutoCorres2_Main: theory Word_Lib.More_Sublist
20:02:05 AutoCorres2_Main: theory AutoCorres2.Arrays
20:02:05 AutoCorres2_Main: theory HOL-Library.Type_Length
20:02:05 AutoCorres2_Main: theory AutoCorres2.Runs_To_VCG
20:02:06 AutoCorres2_Main: theory HOL-Library.Word
20:02:06 AutoCorres2_Main: theory Word_Lib.More_Arithmetic
20:02:06 AutoCorres2_Main: theory AutoCorres2.Mutual_CCPO_Recursion
20:02:06 AutoCorres2_Main: theory AutoCorres2.Spec_Monad
20:02:13 AutoCorres2_Main: theory AutoCorres2.Synthesize
20:02:18 AutoCorres2_Main: theory Word_Lib.Bit_Comprehension
20:02:18 AutoCorres2_Main: theory Word_Lib.Hex_Words
20:02:18 AutoCorres2_Main: theory Word_Lib.Legacy_Aliases
20:02:18 AutoCorres2_Main: theory Word_Lib.More_Divides
20:02:18 AutoCorres2_Main: theory Word_Lib.Signed_Words
20:02:18 AutoCorres2_Main: theory Word_Lib.Syntax_Bundles
20:02:18 AutoCorres2_Main: theory Word_Lib.Type_Syntax
20:02:18 AutoCorres2_Main: theory Word_Lib.Word_Syntax
20:02:18 AutoCorres2_Main: theory AutoCorres2.Reaches
20:02:18 AutoCorres2_Main: theory Word_Lib.Signed_Division_Word
20:02:18 AutoCorres2_Main: theory Word_Lib.Norm_Words
20:02:18 AutoCorres2_Main: theory Word_Lib.Word_Names
20:02:18 AutoCorres2_Main: theory Word_Lib.More_Word
20:02:20 AutoCorres2_Main: theory Word_Lib.Bit_Comprehension_Int
20:02:20 AutoCorres2_Main: theory Word_Lib.Bit_Shifts_Infix_Syntax
20:02:20 AutoCorres2_Main: theory Word_Lib.Enumeration_Word
20:02:20 AutoCorres2_Main: theory Word_Lib.Least_significant_bit
20:02:20 AutoCorres2_Main: theory Word_Lib.Many_More
20:02:20 AutoCorres2_Main: theory Word_Lib.Strict_part_mono
20:02:20 AutoCorres2_Main: theory Word_Lib.Word_16
20:02:21 AutoCorres2_Main: theory AutoCorres2.Distinct_Prop
20:02:21 AutoCorres2_Main: theory AutoCorres2.Lens
20:02:22 AutoCorres2_Main: theory Word_Lib.Aligned
20:02:22 AutoCorres2_Main: theory Word_Lib.Singleton_Bit_Shifts
20:02:22 AutoCorres2_Main: theory Word_Lib.Most_significant_bit
20:02:22 AutoCorres2_Main: theory Word_Lib.Generic_set_bit
20:02:22 AutoCorres2_Main: theory Word_Lib.Sgn_Abs
20:02:22 AutoCorres2_Main: theory Word_Lib.Next_and_Prev
20:02:22 AutoCorres2_Main: theory Word_Lib.Word_EqI
20:02:23 AutoCorres2_Main: theory Word_Lib.Bits_Int
20:02:25 AutoCorres2_Main: theory Word_Lib.Boolean_Inequalities
20:02:27 AutoCorres2_Main: theory Word_Lib.Rsplit
20:02:27 AutoCorres2_Main: theory Word_Lib.Typedef_Morphisms
20:02:28 AutoCorres2_Main: theory Word_Lib.Reversed_Bit_Lists
20:02:29 AutoCorres2_Main: theory Word_Lib.Word_Lemmas
20:02:32 AutoCorres2_Main: theory Word_Lib.Bitwise
20:02:32 AutoCorres2_Main: theory Word_Lib.Word_8
20:02:32 AutoCorres2_Main: theory Word_Lib.More_Word_Operations
20:02:32 AutoCorres2_Main: theory Word_Lib.Bitwise_Signed
20:02:33 AutoCorres2_Main: theory AutoCorres2.Word_Lemmas_Internal
20:02:33 AutoCorres2_Main: theory Word_Lib.Word_32
20:02:33 AutoCorres2_Main: theory Word_Lib.Word_64
20:02:34 AutoCorres2_Main: theory Word_Lib.Machine_Word_64_Basics
20:02:35 AutoCorres2_Main: theory Word_Lib.Machine_Word_64
20:02:35 AutoCorres2_Main: theory Word_Lib.Machine_Word_32_Basics
20:02:35 AutoCorres2_Main: theory Word_Lib.Word_Lib_Sumo
20:02:35 AutoCorres2_Main: theory Word_Lib.Machine_Word_32
20:02:38 AutoCorres2_Main: theory AutoCorres2.More_Lib
20:02:38 AutoCorres2_Main: theory AutoCorres2.Word_Lemmas_32_Internal
20:02:38 AutoCorres2_Main: theory AutoCorres2.Word_Lemmas_64_Internal
20:02:38 AutoCorres2_Main: theory AutoCorres2.WordSetup
20:02:39 AutoCorres2_Main: theory AutoCorres2.Addr_Type_ARM
20:02:39 AutoCorres2_Main: theory AutoCorres2.Addr_Type_ARM64
20:02:39 AutoCorres2_Main: theory AutoCorres2.Addr_Type_ARM_HYP
20:02:39 AutoCorres2_Main: theory AutoCorres2.Addr_Type_RISCV64
20:02:40 AutoCorres2_Main: theory AutoCorres2.Addr_Type_X64
20:02:40 AutoCorres2_Main: theory AutoCorres2.Addr_Type
20:02:41 AutoCorres2_Main: theory AutoCorres2.NatBitwise
20:02:41 AutoCorres2_Main: theory AutoCorres2.Reader_Monad
20:02:41 AutoCorres2_Main: theory AutoCorres2.CTypesBase
20:02:42 AutoCorres2_Main: theory AutoCorres2.Option_MonadND
20:02:44 AutoCorres2_Main: theory AutoCorres2.CTypesDefs
20:02:59 AutoCorres2_Main: theory AutoCorres2.CTypes
20:03:03 AutoCorres2_Main: theory AutoCorres2.HeapRawState
20:03:03 AutoCorres2_Main: theory AutoCorres2.Vanilla32_Preliminaries
20:03:03 AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_ARM
20:03:03 AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_ARM64
20:03:03 AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_ARM_HYP
20:03:03 AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_RISCV64
20:03:03 AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_X64
20:03:03 AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding
20:03:04 AutoCorres2_Main: theory AutoCorres2.Vanilla32
20:03:05 AutoCorres2_Main: theory AutoCorres2.CompoundCTypes
20:03:11 AutoCorres2_Main: theory AutoCorres2.ArraysMemInstance
20:03:12 AutoCorres2_Main: theory AutoCorres2.ArchArraysMemInstance
20:03:15 AutoCorres2_Main: theory AutoCorres2.TypHeap
20:03:23 AutoCorres2_Main: theory AutoCorres2.Separation_UMM
20:03:24 AutoCorres2_Main: theory AutoCorres2.SepCode
20:03:26 AutoCorres2_Main: theory AutoCorres2.SepInv
20:03:27 AutoCorres2_Main: theory AutoCorres2.SepTactic
20:03:28 AutoCorres2_Main: theory AutoCorres2.SepFrame
20:03:29 AutoCorres2_Main: theory AutoCorres2.StructSupport
20:03:31 AutoCorres2_Main: theory AutoCorres2.ArrayAssertion
20:03:31 AutoCorres2_Main: theory AutoCorres2.CProof
20:03:41 AutoCorres2_Main: theory AutoCorres2.CLanguage
20:03:41 AutoCorres2_Main: theory AutoCorres2.Padding_Equivalence
20:03:41 AutoCorres2_Main: theory AutoCorres2.PackedTypes
20:03:48 AutoCorres2_Main: theory AutoCorres2.ModifiesProofs
20:03:51 AutoCorres2_Main: theory AutoCorres2.UMM
20:03:59 AutoCorres2_Main: theory AutoCorres2.CLocals
20:04:02 AutoCorres2_Main: theory AutoCorres2.CTranslationSetup
20:04:31 AutoCorres2_Main: theory AutoCorres2.Array_Selectors
20:04:31 AutoCorres2_Main: theory AutoCorres2.CTranslation
20:04:32 AutoCorres2_Main: theory AutoCorres2.TypHeapLib
20:04:33 AutoCorres2_Main: theory AutoCorres2.AbstractArrays
20:04:33 AutoCorres2_Main: theory AutoCorres2.LemmaBucket_C
20:04:34 AutoCorres2_Main: theory AutoCorres2.AutoCorres_Base
20:04:38 AutoCorres2_Main: theory AutoCorres2.TypHeapSimple
20:04:38 AutoCorres2_Main: theory AutoCorres2.SimplBucket
20:04:38 AutoCorres2_Main: theory AutoCorres2.AutoCorresSimpset
20:04:38 AutoCorres2_Main: theory AutoCorres2.CCorresE
20:04:39 AutoCorres2_Main: theory AutoCorres2.CorresXF
20:04:39 AutoCorres2_Main: theory AutoCorres2.L1Defs
20:04:42 AutoCorres2_Main: theory AutoCorres2.L1Peephole
20:04:42 AutoCorres2_Main: theory AutoCorres2.L1Valid
20:04:43 AutoCorres2_Main: theory AutoCorres2.ExceptionRewrite
20:04:43 AutoCorres2_Main: theory AutoCorres2.SimplConv
20:04:43 AutoCorres2_Main: theory AutoCorres2.L2Defs
20:04:48 AutoCorres2_Main: theory AutoCorres2.Split_Heap
20:04:51 AutoCorres2_Main: theory AutoCorres2.L2ExceptionRewrite
20:04:51 AutoCorres2_Main: theory AutoCorres2.L2Peephole
20:04:51 AutoCorres2_Main: theory AutoCorres2.LocalVarExtract
20:04:51 AutoCorres2_Main: theory AutoCorres2.Stack_Typing
20:04:51 AutoCorres2_Main: theory AutoCorres2.WordAbstract
20:04:54 AutoCorres2_Main: theory AutoCorres2.Refines_Spec
20:04:54 AutoCorres2_Main: theory AutoCorres2.In_Out_Parameters
20:04:55 AutoCorres2_Main: theory AutoCorres2.WordPolish
20:05:12 AutoCorres2_Main: theory AutoCorres2.HeapLift
20:05:12 AutoCorres2_Main: theory AutoCorres2.TypeStrengthen
20:05:36 AutoCorres2_Main: theory AutoCorres2.Polish
20:05:36 AutoCorres2_Main: theory AutoCorres2.Runs_To_VCG_StackPointer
20:05:45 AutoCorres2_Main: theory AutoCorres2.AutoCorres
20:06:11 AutoCorres2_Main: theory AutoCorres2_Main.AutoCorres_Main
20:06:11 AutoCorres2_Main: theory AutoCorres2_Main.AutoCorres_Nondet_Syntax
20:07:21 Timing AutoCorres2_Main (8 threads, 260.854s elapsed time, 1783.938s cpu time, 43.499s GC time, factor 6.84)
20:07:21 Finished AutoCorres2_Main (0:05:11 elapsed time, 0:31:51 cpu time, factor 6.14)
20:07:22 Building HOL-Algebra (on hpcisabelle/2) ...
20:07:24 HOL-Algebra: theory HOL-Algebra.README
20:07:24 HOL-Algebra: theory HOL-Cardinals.Fun_More
20:07:24 HOL-Algebra: theory HOL-Cardinals.Order_Union
20:07:24 HOL-Algebra: theory HOL-Cardinals.Order_Relation_More
20:07:24 HOL-Algebra: theory HOL-Algebra.Exponent
20:07:24 HOL-Algebra: theory HOL-Combinatorics.Transposition
20:07:24 HOL-Algebra: theory HOL-Algebra.Congruence
20:07:24 HOL-Algebra: theory HOL-Combinatorics.Permutations
20:07:25 HOL-Algebra: theory HOL-Cardinals.Wellfounded_More
20:07:25 HOL-Algebra: theory HOL-Cardinals.Wellorder_Relation
20:07:25 HOL-Algebra: theory HOL-Cardinals.Wellorder_Embedding
20:07:25 HOL-Algebra: theory HOL-Cardinals.Wellorder_Constructions
20:07:26 HOL-Algebra: theory HOL-Algebra.Order
20:07:26 HOL-Algebra: theory HOL-Combinatorics.Cycles
20:07:26 HOL-Algebra: theory HOL-Combinatorics.List_Permutation
20:07:26 HOL-Algebra: theory HOL-Cardinals.Cardinal_Order_Relation
20:07:27 HOL-Algebra: theory HOL-Algebra.Lattice
20:07:27 HOL-Algebra: theory HOL-Cardinals.Cardinal_Arithmetic
20:07:28 HOL-Algebra: theory HOL-Algebra.Complete_Lattice
20:07:30 HOL-Algebra: theory HOL-Algebra.Galois_Connection
20:07:30 HOL-Algebra: theory HOL-Algebra.Group
20:07:33 HOL-Algebra: theory HOL-Algebra.Bij
20:07:33 HOL-Algebra: theory HOL-Algebra.Coset
20:07:33 HOL-Algebra: theory HOL-Algebra.FiniteProduct
20:07:34 HOL-Algebra: theory HOL-Algebra.Ring
20:07:35 HOL-Algebra: theory HOL-Algebra.Group_Action
20:07:35 HOL-Algebra: theory HOL-Algebra.Left_Coset
20:07:35 HOL-Algebra: theory HOL-Algebra.SimpleGroups
20:07:35 HOL-Algebra: theory HOL-Algebra.SndIsomorphismGrp
20:07:35 HOL-Algebra: theory HOL-Algebra.Sylow
20:07:36 HOL-Algebra: theory HOL-Algebra.Generated_Groups
20:07:36 HOL-Algebra: theory HOL-Algebra.Divisibility
20:07:36 HOL-Algebra: theory HOL-Algebra.Zassenhaus
20:07:37 HOL-Algebra: theory HOL-Algebra.Solvable_Groups
20:07:37 HOL-Algebra: theory HOL-Algebra.Elementary_Groups
20:07:37 HOL-Algebra: theory HOL-Algebra.Sym_Groups
20:07:39 HOL-Algebra: theory HOL-Algebra.Exact_Sequence
20:07:39 HOL-Algebra: theory HOL-Algebra.Product_Groups
20:07:40 HOL-Algebra: theory HOL-Algebra.AbelCoset
20:07:40 HOL-Algebra: theory HOL-Algebra.Module
20:07:40 HOL-Algebra: theory HOL-Algebra.Free_Abelian_Groups
20:07:45 HOL-Algebra: theory HOL-Algebra.Ideal
20:07:48 HOL-Algebra: theory HOL-Algebra.Ideal_Product
20:07:48 HOL-Algebra: theory HOL-Algebra.RingHom
20:07:50 HOL-Algebra: theory HOL-Algebra.QuotRing
20:07:50 HOL-Algebra: theory HOL-Algebra.UnivPoly
20:07:54 HOL-Algebra: theory HOL-Algebra.IntRing
20:07:54 HOL-Algebra: theory HOL-Algebra.Weak_Morphisms
20:07:55 HOL-Algebra: theory HOL-Algebra.Chinese_Remainder
20:08:07 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group
20:08:11 HOL-Algebra: theory HOL-Algebra.Ring_Divisibility
20:08:12 HOL-Algebra: theory HOL-Algebra.Subrings
20:08:15 HOL-Algebra: theory HOL-Algebra.Embedded_Algebras
20:08:15 HOL-Algebra: theory HOL-Algebra.Generated_Rings
20:08:16 HOL-Algebra: theory HOL-Algebra.Generated_Fields
20:08:21 HOL-Algebra: theory HOL-Algebra.Polynomials
20:08:41 HOL-Algebra: theory HOL-Algebra.Polynomial_Divisibility
20:09:24 HOL-Algebra: theory HOL-Algebra.Finite_Extensions
20:09:24 HOL-Algebra: theory HOL-Algebra.Indexed_Polynomials
20:09:39 HOL-Algebra: theory HOL-Algebra.Algebraic_Closure
20:09:48 HOL-Algebra: theory HOL-Algebra.Algebraic_Closure_Type
20:09:48 HOL-Algebra: theory HOL-Algebra.Algebra
20:10:32 Preparing HOL-Algebra/document ...
20:11:01 Finished HOL-Algebra/document (0:00:28 elapsed time)
20:11:01 Preparing HOL-Algebra/outline ...
20:11:14 Finished HOL-Algebra/outline (0:00:13 elapsed time)
20:11:15 Timing HOL-Algebra (8 threads, 159.272s elapsed time, 797.848s cpu time, 91.079s GC time, factor 5.01)
20:11:15 Finished HOL-Algebra (0:03:07 elapsed time, 0:14:21 cpu time, factor 4.60)
20:11:15 Building Refine_Monadic (on hpcisabelle/3) ...
20:11:16 Refine_Monadic: theory Refine_Monadic.Refine_Chapter
20:11:16 Refine_Monadic: theory Refine_Monadic.Example_Chapter
20:11:16 Refine_Monadic: theory HOL-Library.Adhoc_Overloading
20:11:16 Refine_Monadic: theory HOL-Library.While_Combinator
20:11:16 Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover
20:11:16 Refine_Monadic: theory HOL-Library.Phantom_Type
20:11:17 Refine_Monadic: theory HOL-Library.Monad_Syntax
20:11:17 Refine_Monadic: theory Refine_Monadic.Refine_Misc
20:11:17 Refine_Monadic: theory HOL-Library.Cardinality
20:11:18 Refine_Monadic: theory Refine_Monadic.RefineG_Domain
20:11:18 Refine_Monadic: theory Refine_Monadic.RefineG_Transfer
20:11:18 Refine_Monadic: theory Refine_Monadic.RefineG_Assert
20:11:19 Refine_Monadic: theory HOL-Library.Numeral_Type
20:11:19 Refine_Monadic: theory Refine_Monadic.RefineG_Recursion
20:11:20 Refine_Monadic: theory Refine_Monadic.Refine_Basic
20:11:20 Refine_Monadic: theory Refine_Monadic.RefineG_While
20:11:20 Refine_Monadic: theory HOL-Library.Type_Length
20:11:20 Refine_Monadic: theory Refine_Monadic.Refine_Det
20:11:21 Refine_Monadic: theory HOL-Library.Word
20:11:24 Refine_Monadic: theory Refine_Monadic.Refine_Heuristics
20:11:24 Refine_Monadic: theory Refine_Monadic.Refine_Leof
20:11:24 Refine_Monadic: theory Refine_Monadic.Refine_More_Comb
20:11:25 Refine_Monadic: theory Refine_Monadic.Refine_Pfun
20:11:25 Refine_Monadic: theory Refine_Monadic.Refine_While
20:11:27 Refine_Monadic: theory Refine_Monadic.Refine_Transfer
20:11:27 Refine_Monadic: theory Refine_Monadic.Autoref_Monadic
20:11:27 Refine_Monadic: theory Refine_Monadic.Refine_Automation
20:11:27 Refine_Monadic: theory Refine_Monadic.Refine_Foreach
20:11:31 Refine_Monadic: theory Refine_Monadic.Refine_Monadic
20:11:32 Refine_Monadic: theory Refine_Monadic.Breadth_First_Search
20:11:32 Refine_Monadic: theory Refine_Monadic.WordRefine
20:11:33 Refine_Monadic: theory Refine_Monadic.Examples
20:12:07 Preparing Refine_Monadic/document ...
20:12:18 Finished Refine_Monadic/document (0:00:11 elapsed time)
20:12:18 Preparing Refine_Monadic/outline ...
20:12:26 Finished Refine_Monadic/outline (0:00:07 elapsed time)
20:12:26 Timing Refine_Monadic (8 threads, 38.991s elapsed time, 174.799s cpu time, 4.512s GC time, factor 4.48)
20:12:26 Finished Refine_Monadic (0:00:50 elapsed time, 0:03:18 cpu time, factor 3.90)
20:12:26 Building Hermite (on hpcisabelle/4) ...
20:12:28 Hermite: theory Hermite.Hermite
20:12:34 Hermite: theory Hermite.Hermite_IArrays
20:13:11 Preparing Hermite/document ...
20:13:14 Finished Hermite/document (0:00:03 elapsed time)
20:13:14 Preparing Hermite/outline ...
20:13:16 Finished Hermite/outline (0:00:02 elapsed time)
20:13:17 Timing Hermite (8 threads, 29.131s elapsed time, 113.898s cpu time, 1.420s GC time, factor 3.91)
20:13:17 Finished Hermite (0:00:45 elapsed time, 0:02:21 cpu time, factor 3.13)
20:13:17 Building Expander_Graphs (on hpcisabelle/5) ...
20:13:22 Expander_Graphs: theory Digit_Expansions.Bits_Digits
20:13:22 Expander_Graphs: theory HOL-Eisbach.Eisbach
20:13:22 Expander_Graphs: theory Graph_Theory.Rtrancl_On
20:13:22 Expander_Graphs: theory HOL-Decision_Procs.Dense_Linear_Order
20:13:22 Expander_Graphs: theory HOL-Library.Code_Abstract_Nat
20:13:22 Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
20:13:22 Expander_Graphs: theory HOL-Library.Code_Target_Int
20:13:22 Expander_Graphs: theory HOL-Algebra.Congruence
20:13:22 Expander_Graphs: theory HOL-Library.Code_Target_Nat
20:13:22 Expander_Graphs: theory Finite_Fields.Finite_Fields_More_Bijections
20:13:22 Expander_Graphs: theory HOL-Combinatorics.List_Permutation
20:13:22 Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
20:13:23 Expander_Graphs: theory HOL-Library.Code_Target_Numeral
20:13:23 Expander_Graphs: theory HOL-Library.Function_Algebras
20:13:23 Expander_Graphs: theory Abstract-Rewriting.Seq
20:13:23 Expander_Graphs: theory HOL-Library.More_List
20:13:23 Expander_Graphs: theory Perron_Frobenius.Bij_Nat
20:13:23 Expander_Graphs: theory HOL-Library.While_Combinator
20:13:23 Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
20:13:24 Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
20:13:24 Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
20:13:24 Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
20:13:24 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
20:13:24 Expander_Graphs: theory HOL-Algebra.Order
20:13:24 Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
20:13:24 Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
20:13:25 Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
20:13:25 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
20:13:25 Expander_Graphs: theory Jordan_Normal_Form.Conjugate
20:13:25 Expander_Graphs: theory HOL-Library.Lattice_Algebras
20:13:25 Expander_Graphs: theory HOL-Library.Log_Nat
20:13:25 Expander_Graphs: theory HOL-Algebra.Lattice
20:13:25 Expander_Graphs: theory Graph_Theory.Stuff
20:13:25 Expander_Graphs: theory Graph_Theory.Digraph
20:13:25 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families
20:13:26 Expander_Graphs: theory Ergodic_Theory.SG_Library_Complement
20:13:26 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
20:13:27 Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
20:13:27 Expander_Graphs: theory Matrix.Utility
20:13:27 Expander_Graphs: theory HOL-Algebra.Complete_Lattice
20:13:27 Expander_Graphs: theory Lp.Functional_Spaces
20:13:27 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
20:13:28 Expander_Graphs: theory Graph_Theory.Arc_Walk
20:13:28 Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
20:13:28 Expander_Graphs: theory HOL-Algebra.Group
20:13:29 Expander_Graphs: theory Regular-Sets.Regular_Set
20:13:30 Expander_Graphs: theory Graph_Theory.Pair_Digraph
20:13:30 Expander_Graphs: theory VectorSpace.FunctionLemmas
20:13:31 Expander_Graphs: theory HOL-Algebra.Coset
20:13:31 Expander_Graphs: theory HOL-Algebra.FiniteProduct
20:13:31 Expander_Graphs: theory Lp.Lp
20:13:31 Expander_Graphs: theory HOL-Algebra.Ring
20:13:32 Expander_Graphs: theory Concentration_Inequalities.Concentration_Inequalities_Preliminary
20:13:32 Expander_Graphs: theory HOL-Library.Interval
20:13:32 Expander_Graphs: theory HOL-Library.Float
20:13:32 Expander_Graphs: theory Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
20:13:33 Expander_Graphs: theory HOL-Algebra.Generated_Groups
20:13:33 Expander_Graphs: theory HOL-Algebra.Divisibility
20:13:37 Expander_Graphs: theory HOL-Algebra.Elementary_Groups
20:13:37 Expander_Graphs: theory Universal_Hash_Families.Pseudorandom_Objects
20:13:38 Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
20:13:38 Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
20:13:38 Expander_Graphs: theory HOL-Library.Interval_Float
20:13:38 Expander_Graphs: theory Regular-Sets.Regular_Exp
20:13:39 Expander_Graphs: theory HOL-Algebra.AbelCoset
20:13:39 Expander_Graphs: theory HOL-Algebra.Module
20:13:39 Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
20:13:39 Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
20:13:39 Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
20:13:39 Expander_Graphs: theory HOL-Decision_Procs.Approximation_Bounds
20:13:40 Expander_Graphs: theory Graph_Theory.Digraph_Component
20:13:40 Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
20:13:40 Expander_Graphs: theory VectorSpace.RingModuleFacts
20:13:41 Expander_Graphs: theory VectorSpace.MonoidSums
20:13:41 Expander_Graphs: theory Regular-Sets.NDerivative
20:13:42 Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
20:13:42 Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
20:13:42 Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
20:13:42 Expander_Graphs: theory Regular-Sets.Relation_Interpretation
20:13:42 Expander_Graphs: theory HOL-Algebra.Ideal
20:13:42 Expander_Graphs: theory VectorSpace.LinearCombinations
20:13:44 Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
20:13:44 Expander_Graphs: theory Jordan_Normal_Form.Matrix
20:13:45 Expander_Graphs: theory HOL-Decision_Procs.Approximation
20:13:46 Expander_Graphs: theory HOL-Algebra.RingHom
20:13:46 Expander_Graphs: theory Regular-Sets.Equivalence_Checking
20:13:47 Expander_Graphs: theory Regular-Sets.Regexp_Method
20:13:47 Expander_Graphs: theory HOL-Algebra.QuotRing
20:13:47 Expander_Graphs: theory HOL-Algebra.UnivPoly
20:13:48 Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
20:13:50 Expander_Graphs: theory VectorSpace.SumSpaces
20:13:51 Expander_Graphs: theory VectorSpace.VectorSpace
20:13:51 Expander_Graphs: theory Abstract-Rewriting.SN_Orders
20:13:52 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
20:13:52 Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
20:13:53 Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
20:13:54 Expander_Graphs: theory Jordan_Normal_Form.Determinant
20:13:54 Expander_Graphs: theory Matrix.Ordered_Semiring
20:13:55 Expander_Graphs: theory Matrix.Matrix_Legacy
20:13:57 Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
20:13:57 Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
20:13:57 Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
20:13:58 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
20:13:59 Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
20:14:00 Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
20:14:00 Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
20:14:01 Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
20:14:01 Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
20:14:02 Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
20:14:03 Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
20:14:04 Expander_Graphs: theory HOL-Algebra.Multiplicative_Group
20:14:09 Expander_Graphs: theory HOL-Algebra.Ring_Divisibility
20:14:09 Expander_Graphs: theory HOL-Algebra.Subrings
20:14:12 Expander_Graphs: theory HOL-Algebra.Embedded_Algebras
20:14:16 Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
20:14:18 Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
20:14:19 Expander_Graphs: theory HOL-Algebra.Polynomials
20:14:23 Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
20:14:29 Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
20:14:29 Expander_Graphs: theory QHLProver.Complex_Matrix
20:14:29 Expander_Graphs: theory Perron_Frobenius.HMA_Connect
20:14:35 Expander_Graphs: theory QHLProver.Gates
20:14:35 Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
20:14:43 Expander_Graphs: theory HOL-Algebra.Polynomial_Divisibility
20:14:45 Expander_Graphs: theory Projective_Measurements.Projective_Measurements
20:14:47 Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
20:14:48 Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
20:15:16 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
20:15:16 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
20:15:21 Expander_Graphs: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
20:15:25 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
20:15:28 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
20:15:29 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
20:15:30 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
20:15:33 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
20:15:44 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
20:15:44 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
20:15:47 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
20:15:51 Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
20:15:58 Expander_Graphs: theory Expander_Graphs.Pseudorandom_Objects_Expander_Walks
20:24:12 Preparing Expander_Graphs/document ...
20:24:25 Finished Expander_Graphs/document (0:00:12 elapsed time)
20:24:25 Preparing Expander_Graphs/outline ...
20:24:29 Finished Expander_Graphs/outline (0:00:04 elapsed time)
20:24:30 Timing Expander_Graphs (8 threads, 585.335s elapsed time, 2723.789s cpu time, 218.012s GC time, factor 4.65)
20:24:30 Finished Expander_Graphs (0:10:46 elapsed time, 0:47:52 cpu time, factor 4.44)
20:24:30 Building Smith_Normal_Form (on hpcisabelle/6) ...
20:24:33 Smith_Normal_Form: theory Deriving.Generator_Aux
20:24:33 Smith_Normal_Form: theory Deriving.Derive_Manager
20:24:33 Smith_Normal_Form: theory HOL-Eisbach.Eisbach
20:24:33 Smith_Normal_Form: theory HOL-Number_Theory.Cong
20:24:33 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
20:24:33 Smith_Normal_Form: theory HOL-Algebra.Congruence
20:24:33 Smith_Normal_Form: theory Perron_Frobenius.Bij_Nat
20:24:33 Smith_Normal_Form: theory HOL-Types_To_Sets.Types_To_Sets
20:24:34 Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
20:24:34 Smith_Normal_Form: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
20:24:34 Smith_Normal_Form: theory Jordan_Normal_Form.Conjugate
20:24:34 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
20:24:34 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
20:24:34 Smith_Normal_Form: theory Perron_Frobenius.Cancel_Card_Constraint
20:24:35 Smith_Normal_Form: theory Smith_Normal_Form.Rings2_Extended
20:24:35 Smith_Normal_Form: theory List-Index.List_Index
20:24:35 Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
20:24:35 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form
20:24:36 Smith_Normal_Form: theory HOL-Algebra.Order
20:24:36 Smith_Normal_Form: theory Show.Show
20:24:36 Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith
20:24:36 Smith_Normal_Form: theory HOL-Number_Theory.Totient
20:24:37 Smith_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
20:24:37 Smith_Normal_Form: theory HOL-Algebra.Lattice
20:24:37 Smith_Normal_Form: theory Subresultants.Binary_Exponentiation
20:24:37 Smith_Normal_Form: theory VectorSpace.FunctionLemmas
20:24:38 Smith_Normal_Form: theory Show.Show_Instances
20:24:38 Smith_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
20:24:38 Smith_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
20:24:38 Smith_Normal_Form: theory HOL-Algebra.Complete_Lattice
20:24:38 Smith_Normal_Form: theory Show.Show_Poly
20:24:39 Smith_Normal_Form: theory HOL-Algebra.Group
20:24:41 Smith_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
20:24:41 Smith_Normal_Form: theory HOL-Algebra.Coset
20:24:42 Smith_Normal_Form: theory HOL-Algebra.FiniteProduct
20:24:42 Smith_Normal_Form: theory HOL-Algebra.Ring
20:24:44 Smith_Normal_Form: theory HOL-Algebra.Generated_Groups
20:24:45 Smith_Normal_Form: theory HOL-Algebra.Elementary_Groups
20:24:47 Smith_Normal_Form: theory HOL-Algebra.AbelCoset
20:24:47 Smith_Normal_Form: theory HOL-Algebra.Module
20:24:47 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
20:24:50 Smith_Normal_Form: theory VectorSpace.RingModuleFacts
20:24:51 Smith_Normal_Form: theory VectorSpace.MonoidSums
20:24:51 Smith_Normal_Form: theory VectorSpace.LinearCombinations
20:24:52 Smith_Normal_Form: theory HOL-Algebra.Ideal
20:24:54 Smith_Normal_Form: theory Jordan_Normal_Form.Matrix
20:24:56 Smith_Normal_Form: theory HOL-Algebra.RingHom
20:24:57 Smith_Normal_Form: theory HOL-Algebra.UnivPoly
20:24:59 Smith_Normal_Form: theory VectorSpace.SumSpaces
20:25:00 Smith_Normal_Form: theory VectorSpace.VectorSpace
20:25:00 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
20:25:00 Smith_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
20:25:00 Smith_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
20:25:02 Smith_Normal_Form: theory Jordan_Normal_Form.Column_Operations
20:25:03 Smith_Normal_Form: theory Jordan_Normal_Form.Determinant
20:25:05 Smith_Normal_Form: theory Jordan_Normal_Form.Char_Poly
20:25:06 Smith_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
20:25:07 Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
20:25:10 Smith_Normal_Form: theory Jordan_Normal_Form.VS_Connect
20:25:14 Smith_Normal_Form: theory HOL-Algebra.Multiplicative_Group
20:25:19 Smith_Normal_Form: theory HOL-Number_Theory.Residues
20:25:23 Smith_Normal_Form: theory Berlekamp_Zassenhaus.Finite_Field
20:25:25 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank
20:25:25 Smith_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
20:25:27 Smith_Normal_Form: theory Smith_Normal_Form.Finite_Field_Mod_Type_Connection
20:25:27 Smith_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
20:25:32 Smith_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
20:25:34 Smith_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
20:25:37 Smith_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
20:25:37 Smith_Normal_Form: theory Perron_Frobenius.HMA_Connect
20:25:42 Smith_Normal_Form: theory Smith_Normal_Form.Mod_Type_Connect
20:25:44 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Missing_Lemmas
20:25:48 Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet
20:25:48 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Normal_Form_JNF
20:25:48 Smith_Normal_Form: theory Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring
20:25:48 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm
20:25:50 Smith_Normal_Form: theory Smith_Normal_Form.Cauchy_Binet_HOL_Analysis
20:25:52 Smith_Normal_Form: theory Smith_Normal_Form.Diagonal_To_Smith_JNF
20:25:53 Smith_Normal_Form: theory Smith_Normal_Form.Diagonalize
20:25:53 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Uniqueness
20:25:53 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps
20:25:56 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Two_Steps_JNF
20:26:00 Smith_Normal_Form: theory Smith_Normal_Form.Elementary_Divisor_Rings
20:26:02 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_HOL_Analysis
20:26:02 Smith_Normal_Form: theory Smith_Normal_Form.Alternative_Proofs
20:26:02 Smith_Normal_Form: theory Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain
20:26:10 Smith_Normal_Form: theory Smith_Normal_Form.Smith_Certified
20:31:12 Preparing Smith_Normal_Form/document ...
20:31:26 Finished Smith_Normal_Form/document (0:00:13 elapsed time)
20:31:26 Preparing Smith_Normal_Form/outline ...
20:31:31 Finished Smith_Normal_Form/outline (0:00:04 elapsed time)
20:31:31 Timing Smith_Normal_Form (8 threads, 347.815s elapsed time, 2066.558s cpu time, 113.521s GC time, factor 5.94)
20:31:31 Finished Smith_Normal_Form (0:06:37 elapsed time, 0:36:25 cpu time, factor 5.49)
20:31:31 Building Collections (on hpcisabelle/7) ...
20:31:33 Collections: theory Collections.ICF_Tools
20:31:33 Collections: theory Collections.Partial_Equivalence_Relation
20:31:33 Collections: theory Finger-Trees.FingerTree
20:31:33 Collections: theory Binomial-Heaps.BinomialHeap
20:31:33 Collections: theory Binomial-Heaps.SkewBinomialHeap
20:31:33 Collections: theory HOL-Library.AList
20:31:33 Collections: theory HOL-Library.Code_Abstract_Nat
20:31:33 Collections: theory HOL-Library.Code_Target_Int
20:31:33 Collections: theory HOL-Library.Code_Target_Nat
20:31:33 Collections: theory HOL-Library.Confluence
20:31:33 Collections: theory Collections.Ord_Code_Preproc
20:31:33 Collections: theory Collections.Locale_Code
20:31:33 Collections: theory Collections.Record_Intf
20:31:33 Collections: theory HOL-Library.Confluent_Quotient
20:31:34 Collections: theory HOL-Library.Code_Target_Numeral
20:31:34 Collections: theory Collections.SetIterator
20:31:34 Collections: theory Collections.Sorted_List_Operations
20:31:34 Collections: theory Word_Lib.Bit_Comprehension
20:31:34 Collections: theory HOL-Library.Dlist
20:31:35 Collections: theory Word_Lib.More_Divides
20:31:35 Collections: theory HOL-Library.RBT_Impl
20:31:35 Collections: theory HOL-Library.Signed_Division
20:31:36 Collections: theory Collections.DatRef
20:31:36 Collections: theory Collections.Idx_Iterator
20:31:36 Collections: theory Collections.SetAbstractionIterator
20:31:37 Collections: theory Collections.SetIteratorOperations
20:31:37 Collections: theory Native_Word.Code_Int_Integer_Conversion
20:31:37 Collections: theory Word_Lib.More_Arithmetic
20:31:37 Collections: theory Word_Lib.Signed_Division_Word
20:31:37 Collections: theory Word_Lib.More_Bit_Ring
20:31:38 Collections: theory Word_Lib.More_Word
20:31:41 Collections: theory Collections.Assoc_List
20:31:41 Collections: theory Collections.Dlist_add
20:31:42 Collections: theory Collections.Proper_Iterator
20:31:42 Collections: theory Collections.SetIteratorGA
20:31:42 Collections: theory Native_Word.Code_Target_Word_Base
20:31:42 Collections: theory Collections.Diff_Array
20:31:42 Collections: theory Collections.It_to_It
20:31:43 Collections: theory Collections.Gen_Iterator
20:31:43 Collections: theory Word_Lib.Bit_Shifts_Infix_Syntax
20:31:43 Collections: theory Word_Lib.Least_significant_bit
20:31:44 Collections: theory Collections.Iterator
20:31:44 Collections: theory Collections.ICF_Spec_Base
20:31:45 Collections: theory Collections.MapSpec
20:31:45 Collections: theory Word_Lib.Most_significant_bit
20:31:45 Collections: theory Word_Lib.Generic_set_bit
20:31:46 Collections: theory Native_Word.Code_Target_Integer_Bit
20:31:46 Collections: theory Native_Word.Word_Type_Copies
20:31:49 Collections: theory Collections.Robdd
20:32:02 Collections: theory Native_Word.Code_Target_Int_Bit
20:32:02 Collections: theory Native_Word.Uint32
20:32:02 Collections: theory Collections.Code_Target_ICF
20:32:03 Collections: theory Collections.Locale_Code_Ex
20:32:04 Collections: theory Collections.HashCode
20:32:49 Collections: theory Collections.RBT_add
20:33:25 Collections: theory Collections.GenCF_Chapter
20:33:25 Collections: theory Collections.GenCF_Gen_Chapter
20:33:25 Collections: theory Collections.GenCF_Impl_Chapter
20:33:25 Collections: theory Collections.GenCF_Intf_Chapter
20:33:25 Collections: theory Collections.Intf_Comp
20:33:25 Collections: theory Collections.Impl_Array_Stack
20:33:25 Collections: theory Collections.Array_Iterator
20:33:25 Collections: theory HOL-Library.Product_Lexorder
20:33:25 Collections: theory Collections.Intf_Map
20:33:25 Collections: theory Collections.Intf_Set
20:33:25 Collections: theory Collections.Intf_Hash
20:33:26 Collections: theory Collections.Gen_Set
20:33:26 Collections: theory Collections.Impl_Cfun_Set
20:33:26 Collections: theory Collections.Gen_Map
20:33:26 Collections: theory Collections.Impl_List_Set
20:33:27 Collections: theory Collections.Gen_Comp
20:33:27 Collections: theory Collections.Impl_Array_Map
20:33:27 Collections: theory Collections.Impl_List_Map
20:33:27 Collections: theory Collections.Impl_RBT_Map
20:33:27 Collections: theory Collections.Gen_Map2Set
20:33:29 Collections: theory Collections.Impl_Array_Hash_Map
20:33:40 Collections: theory Native_Word.Uint
20:33:40 Collections: theory Collections.Impl_Bit_Set
20:33:40 Collections: theory Collections.Gen_Hash
20:33:42 Collections: theory Collections.Impl_Uv_Set
20:33:57 Collections: theory Collections.GenCF
20:34:01 Collections: theory Collections.ICF_Chapter
20:34:01 Collections: theory Collections.ICF_Gen_Algo_Chapter
20:34:01 Collections: theory Collections.ICF_Impl_Chapter
20:34:01 Collections: theory Trie.Trie
20:34:01 Collections: theory Collections.ICF_Spec_Chapter
20:34:01 Collections: theory Collections.AnnotatedListSpec
20:34:01 Collections: theory HOL-Library.RBT
20:34:01 Collections: theory Collections.ListSpec
20:34:01 Collections: theory Collections.PrioSpec
20:34:01 Collections: theory Collections.PrioUniqueSpec
20:34:01 Collections: theory Collections.SetSpec
20:34:02 Collections: theory Collections.BinoPrioImpl
20:34:02 Collections: theory Collections.SkewPrioImpl
20:34:03 Collections: theory Collections.ListGA
20:34:03 Collections: theory Collections.Trie_Impl
20:34:03 Collections: theory Collections.FTAnnotatedListImpl
20:34:03 Collections: theory Collections.PrioByAnnotatedList
20:34:04 Collections: theory Collections.PrioUniqueByAnnotatedList
20:34:04 Collections: theory Collections.Fifo
20:34:04 Collections: theory Collections.Trie2
20:34:05 Collections: theory Collections.Algos
20:34:05 Collections: theory Collections.SetIndex
20:34:06 Collections: theory Collections.SetIteratorCollectionsGA
20:34:06 Collections: theory Collections.MapGA
20:34:06 Collections: theory Collections.SetGA
20:34:08 Collections: theory Collections.FTPrioImpl
20:34:08 Collections: theory Collections.FTPrioUniqueImpl
20:34:09 Collections: theory Collections.ArrayMapImpl
20:34:09 Collections: theory Collections.ListMapImpl
20:34:09 Collections: theory Collections.ListMapImpl_Invar
20:34:10 Collections: theory Collections.TrieMapImpl
20:34:12 Collections: theory Collections.ListSetImpl
20:34:13 Collections: theory Collections.ListSetImpl_Invar
20:34:13 Collections: theory Collections.ListSetImpl_NotDist
20:34:13 Collections: theory Collections.ListSetImpl_Sorted
20:34:14 Collections: theory Collections.SetByMap
20:34:15 Collections: theory Collections.RBTMapImpl
20:34:15 Collections: theory Collections.ArrayHashMap_Impl
20:34:17 Collections: theory Collections.ArraySetImpl
20:34:17 Collections: theory Collections.TrieSetImpl
20:34:19 Collections: theory Collections.ArrayHashMap
20:34:22 Collections: theory Collections.RBTSetImpl
20:34:22 Collections: theory Collections.HashMap_Impl
20:34:24 Collections: theory Collections.HashMap
20:34:25 Collections: theory Collections.ArrayHashSet
20:34:30 Collections: theory Collections.HashSet
20:34:30 Collections: theory Collections.MapStdImpl
20:34:39 Collections: theory Collections.SetStdImpl
20:34:45 Collections: theory Collections.ICF_Impl
20:34:49 Collections: theory Collections.ICF_Refine_Monadic
20:34:49 Collections: theory Collections.ICF_Autoref
20:34:54 Collections: theory Collections.Collections_Entrypoints_Chapter
20:34:54 Collections: theory Collections.ICF_Entrypoints_Chapter
20:34:54 Collections: theory Collections.Userguides_Chapter
20:34:54 Collections: theory Collections.Collections
20:34:54 Collections: theory Collections.Refine_Dflt
20:34:54 Collections: theory Collections.CollectionsV1
20:34:54 Collections: theory Collections.ICF_Userguide
20:34:54 Collections: theory Collections.Refine_Dflt_ICF
20:34:54 Collections: theory Collections.Refine_Dflt_Only_ICF
20:34:54 Collections: theory Collections.Refine_Monadic_Userguide
20:36:23 Preparing Collections/document ...
20:36:43 Finished Collections/document (0:00:19 elapsed time)
20:36:43 Preparing Collections/outline ...
20:36:55 Finished Collections/outline (0:00:12 elapsed time)
20:36:55 Preparing Collections/userguide ...
20:36:59 Finished Collections/userguide (0:00:03 elapsed time)
20:36:59 Timing Collections (8 threads, 227.293s elapsed time, 1013.393s cpu time, 76.110s GC time, factor 4.46)
20:36:59 Finished Collections (0:04:48 elapsed time, 0:19:27 cpu time, factor 4.05)
20:36:59 Building Core_SC_DOM (on hpcisabelle/0) ...
20:37:14 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Basic_Datatypes
20:37:14 Core_SC_DOM: theory Core_SC_DOM.Hiding_Type_Variables
20:37:14 Core_SC_DOM: theory Core_SC_DOM.Testing_Utils
20:37:15 Core_SC_DOM: theory Core_SC_DOM.Ref
20:37:15 Core_SC_DOM: theory Core_SC_DOM.Heap_Error_Monad
20:37:15 Core_SC_DOM: theory Core_SC_DOM.ObjectPointer
20:37:15 Core_SC_DOM: theory Core_SC_DOM.BaseClass
20:37:16 Core_SC_DOM: theory Core_SC_DOM.NodePointer
20:37:16 Core_SC_DOM: theory Core_SC_DOM.ObjectClass
20:37:16 Core_SC_DOM: theory Core_SC_DOM.ElementPointer
20:37:17 Core_SC_DOM: theory Core_SC_DOM.NodeClass
20:37:17 Core_SC_DOM: theory Core_SC_DOM.CharacterDataPointer
20:37:18 Core_SC_DOM: theory Core_SC_DOM.BaseMonad
20:37:19 Core_SC_DOM: theory Core_SC_DOM.DocumentPointer
20:37:20 Core_SC_DOM: theory Core_SC_DOM.ShadowRootPointer
20:37:20 Core_SC_DOM: theory Core_SC_DOM.ObjectMonad
20:37:21 Core_SC_DOM: theory Core_SC_DOM.ElementClass
20:37:21 Core_SC_DOM: theory Core_SC_DOM.NodeMonad
20:37:23 Core_SC_DOM: theory Core_SC_DOM.ElementMonad
20:37:23 Core_SC_DOM: theory Core_SC_DOM.CharacterDataClass
20:37:24 Core_SC_DOM: theory Core_SC_DOM.DocumentClass
20:37:24 Core_SC_DOM: theory Core_SC_DOM.CharacterDataMonad
20:37:25 Core_SC_DOM: theory Core_SC_DOM.DocumentMonad
20:37:27 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Functions
20:37:48 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Heap_WF
20:38:09 Core_SC_DOM: theory Core_SC_DOM.Core_DOM
20:38:09 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_BaseTest
20:38:16 Core_SC_DOM: theory Core_SC_DOM.Document_adoptNode
20:38:16 Core_SC_DOM: theory Core_SC_DOM.Document_getElementById
20:38:16 Core_SC_DOM: theory Core_SC_DOM.Node_insertBefore
20:38:17 Core_SC_DOM: theory Core_SC_DOM.Node_removeChild
20:38:19 Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Tests
20:40:35 Preparing Core_SC_DOM/document ...
20:40:52 Finished Core_SC_DOM/document (0:00:16 elapsed time)
20:40:52 Preparing Core_SC_DOM/outline ...
20:41:03 Finished Core_SC_DOM/outline (0:00:11 elapsed time)
20:41:03 Timing Core_SC_DOM (8 threads, 158.155s elapsed time, 856.207s cpu time, 60.569s GC time, factor 5.41)
20:41:03 Finished Core_SC_DOM (0:03:35 elapsed time, 0:16:35 cpu time, factor 4.63)
20:41:03 Building Jordan_Normal_Form (on hpcisabelle/1) ...
20:41:06 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Misc
20:41:06 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Ring
20:41:13 Jordan_Normal_Form: theory Containers.Equal
20:41:13 Jordan_Normal_Form: theory Containers.Extend_Partial_Order
20:41:13 Jordan_Normal_Form: theory Containers.List_Fusion
20:41:13 Jordan_Normal_Form: theory Deriving.Comparator
20:41:13 Jordan_Normal_Form: theory Deriving.Derive_Manager
20:41:13 Jordan_Normal_Form: theory Deriving.Generator_Aux
20:41:13 Jordan_Normal_Form: theory Containers.Containers_Auxiliary
20:41:13 Jordan_Normal_Form: theory Abstract-Rewriting.Seq
20:41:14 Jordan_Normal_Form: theory Containers.Closure_Set
20:41:14 Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Unsorted
20:41:14 Jordan_Normal_Form: theory Jordan_Normal_Form.Conjugate
20:41:14 Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom
20:41:14 Jordan_Normal_Form: theory Deriving.Equality_Generator
20:41:14 Jordan_Normal_Form: theory Containers.Containers_Generator
20:41:14 Jordan_Normal_Form: theory Regular-Sets.Regular_Set
20:41:15 Jordan_Normal_Form: theory Deriving.Equality_Instances
20:41:15 Jordan_Normal_Form: theory Show.Show
20:41:15 Jordan_Normal_Form: theory Containers.Collection_Enum
20:41:15 Jordan_Normal_Form: theory Deriving.Compare
20:41:15 Jordan_Normal_Form: theory Deriving.Comparator_Generator
20:41:16 Jordan_Normal_Form: theory Containers.Lexicographic_Order
20:41:16 Jordan_Normal_Form: theory Containers.Collection_Eq
20:41:16 Jordan_Normal_Form: theory Containers.RBT_ext
20:41:16 Jordan_Normal_Form: theory Containers.Set_Linorder
20:41:16 Jordan_Normal_Form: theory Deriving.RBT_Comparator_Impl
20:41:17 Jordan_Normal_Form: theory Deriving.Compare_Generator
20:41:17 Jordan_Normal_Form: theory Containers.DList_Set
20:41:17 Jordan_Normal_Form: theory Deriving.Compare_Instances
20:41:17 Jordan_Normal_Form: theory Polynomial_Interpolation.Missing_Polynomial
20:41:17 Jordan_Normal_Form: theory Show.Show_Instances
20:41:18 Jordan_Normal_Form: theory Regular-Sets.Regular_Exp
20:41:19 Jordan_Normal_Form: theory Show.Shows_Literal
20:41:19 Jordan_Normal_Form: theory VectorSpace.FunctionLemmas
20:41:19 Jordan_Normal_Form: theory VectorSpace.RingModuleFacts
20:41:19 Jordan_Normal_Form: theory Polynomial_Factorization.Order_Polynomial
20:41:19 Jordan_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
20:41:20 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix
20:41:20 Jordan_Normal_Form: theory Polynomial_Interpolation.Ring_Hom_Poly
20:41:20 Jordan_Normal_Form: theory VectorSpace.MonoidSums
20:41:20 Jordan_Normal_Form: theory VectorSpace.LinearCombinations
20:41:22 Jordan_Normal_Form: theory Regular-Sets.NDerivative
20:41:22 Jordan_Normal_Form: theory Regular-Sets.Relation_Interpretation
20:41:27 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
20:41:27 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm
20:41:28 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Matrix
20:41:28 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Matrix
20:41:28 Jordan_Normal_Form: theory Jordan_Normal_Form.Shows_Literal_Matrix
20:41:29 Jordan_Normal_Form: theory Regular-Sets.Equivalence_Checking
20:41:29 Jordan_Normal_Form: theory VectorSpace.SumSpaces
20:41:29 Jordan_Normal_Form: theory Jordan_Normal_Form.Column_Operations
20:41:29 Jordan_Normal_Form: theory Regular-Sets.Regexp_Method
20:41:30 Jordan_Normal_Form: theory VectorSpace.VectorSpace
20:41:30 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant
20:41:31 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm_Code
20:41:31 Jordan_Normal_Form: theory Abstract-Rewriting.Abstract_Rewriting
20:41:31 Jordan_Normal_Form: theory Containers.Collection_Order
20:41:33 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant_Impl
20:41:33 Jordan_Normal_Form: theory Jordan_Normal_Form.Char_Poly
20:41:33 Jordan_Normal_Form: theory Abstract-Rewriting.SN_Orders
20:41:33 Jordan_Normal_Form: theory Jordan_Normal_Form.Derivation_Bound
20:41:34 Jordan_Normal_Form: theory Containers.RBT_Mapping2
20:41:34 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form
20:41:35 Jordan_Normal_Form: theory Containers.RBT_Set2
20:41:36 Jordan_Normal_Form: theory Abstract-Rewriting.SN_Order_Carrier
20:41:36 Jordan_Normal_Form: theory Matrix.Ordered_Semiring
20:41:36 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace
20:41:37 Jordan_Normal_Form: theory Containers.Set_Impl
20:41:38 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Comparison
20:41:40 Jordan_Normal_Form: theory Jordan_Normal_Form.VS_Connect
20:41:41 Jordan_Normal_Form: theory Jordan_Normal_Form.Complexity_Carrier
20:41:41 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Arctic
20:41:46 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Complexity
20:41:54 Jordan_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt
20:41:54 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Kernel
20:41:56 Jordan_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition
20:41:57 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
20:42:00 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
20:42:00 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_IArray_Impl
20:42:03 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
20:42:06 Jordan_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius
20:42:06 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Impl
20:45:35 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List
20:45:35 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist
20:45:36 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank
20:45:36 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix
20:45:44 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix
20:46:28 Preparing Jordan_Normal_Form/document ...
20:46:55 Finished Jordan_Normal_Form/document (0:00:26 elapsed time)
20:46:55 Preparing Jordan_Normal_Form/outline ...
20:47:06 Finished Jordan_Normal_Form/outline (0:00:11 elapsed time)
20:47:06 Timing Jordan_Normal_Form (8 threads, 279.799s elapsed time, 1755.452s cpu time, 93.234s GC time, factor 6.27)
20:47:06 Finished Jordan_Normal_Form (0:05:21 elapsed time, 0:30:52 cpu time, factor 5.76)
20:47:07 Building HOL-Number_Theory (on hpcisabelle/2) ...
20:47:09 HOL-Number_Theory: theory HOL-Number_Theory.Cong
20:47:09 HOL-Number_Theory: theory HOL-Algebra.Congruence
20:47:09 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes
20:47:09 HOL-Number_Theory: theory HOL-Number_Theory.Fib
20:47:09 HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers
20:47:10 HOL-Number_Theory: theory HOL-Algebra.Order
20:47:11 HOL-Number_Theory: theory HOL-Number_Theory.Mod_Exp
20:47:11 HOL-Number_Theory: theory HOL-Number_Theory.Totient
20:47:12 HOL-Number_Theory: theory HOL-Algebra.Lattice
20:47:13 HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice
20:47:14 HOL-Number_Theory: theory HOL-Algebra.Group
20:47:17 HOL-Number_Theory: theory HOL-Algebra.Coset
20:47:17 HOL-Number_Theory: theory HOL-Algebra.FiniteProduct
20:47:18 HOL-Number_Theory: theory HOL-Algebra.Ring
20:47:20 HOL-Number_Theory: theory HOL-Algebra.Generated_Groups
20:47:22 HOL-Number_Theory: theory HOL-Algebra.Elementary_Groups
20:47:23 HOL-Number_Theory: theory HOL-Algebra.AbelCoset
20:47:23 HOL-Number_Theory: theory HOL-Algebra.Module
20:47:28 HOL-Number_Theory: theory HOL-Algebra.Ideal
20:47:31 HOL-Number_Theory: theory HOL-Algebra.RingHom
20:47:32 HOL-Number_Theory: theory HOL-Algebra.UnivPoly
20:47:46 HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group
20:47:51 HOL-Number_Theory: theory HOL-Number_Theory.Residues
20:47:54 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion
20:47:54 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington
20:47:54 HOL-Number_Theory: theory HOL-Number_Theory.Gauss
20:47:54 HOL-Number_Theory: theory HOL-Number_Theory.Residue_Primitive_Roots
20:47:54 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity
20:47:55 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory
20:48:25 Preparing HOL-Number_Theory/document ...
20:48:31 Finished HOL-Number_Theory/document (0:00:05 elapsed time)
20:48:31 Preparing HOL-Number_Theory/outline ...
20:48:34 Finished HOL-Number_Theory/outline (0:00:02 elapsed time)
20:48:34 Timing HOL-Number_Theory (8 threads, 59.275s elapsed time, 335.163s cpu time, 10.274s GC time, factor 5.65)
20:48:34 Finished HOL-Number_Theory (0:01:16 elapsed time, 0:06:10 cpu time, factor 4.81)
20:48:34 Building Bounded_Deducibility_Security (on hpcisabelle/3) ...
20:48:35 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Abstract_BD_Security
20:48:35 Bounded_Deducibility_Security: theory HOL-Library.Sublist
20:48:38 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Trivia
20:48:39 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Transition_System
20:48:39 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Filtermap
20:48:40 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_TS
20:48:40 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.IO_Automaton
20:48:41 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_Triggers
20:48:42 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_IO
20:48:43 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_Unwinding
20:48:43 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Compositional_Reasoning
20:48:44 Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Bounded_Deducibility_Security
20:48:53 Preparing Bounded_Deducibility_Security/document ...
20:48:57 Finished Bounded_Deducibility_Security/document (0:00:03 elapsed time)
20:48:57 Preparing Bounded_Deducibility_Security/outline ...
20:49:00 Finished Bounded_Deducibility_Security/outline (0:00:03 elapsed time)
20:49:00 Timing Bounded_Deducibility_Security (8 threads, 9.757s elapsed time, 44.382s cpu time, 1.234s GC time, factor 4.55)
20:49:00 Finished Bounded_Deducibility_Security (0:00:18 elapsed time, 0:01:00 cpu time, factor 3.26)
20:49:00 Running AutoCorres2_Test (on hpcisabelle/4) ...
20:49:03 AutoCorres2_Test: theory AutoCorres2_Test.Match_Cterm_Ex
20:49:03 AutoCorres2_Test: theory AutoCorres2_Test.DataStructures
20:49:03 AutoCorres2_Test: theory HOL-Computational_Algebra.Factorial_Ring
20:49:03 AutoCorres2_Test: theory HOL-Library.Product_Lexorder
20:49:03 AutoCorres2_Test: theory AutoCorres2_Test.Asm_Labels
20:49:03 AutoCorres2_Test: theory AutoCorres2_Test.AC_Rename
20:49:03 AutoCorres2_Test: theory AutoCorres2_Test.CList
20:49:03 AutoCorres2_Test: theory AutoCorres2_Test.Alloc_Ex
20:49:03 AutoCorres2_Test: theory AutoCorres2_Test.ConditionGuard
20:49:03 AutoCorres2_Test: theory AutoCorres2_Test.CustomWordAbs
20:49:04 AutoCorres2_Test: theory AutoCorres2_Test.BinarySearch
20:49:12 AutoCorres2_Test: theory AutoCorres2_Test.EvaluationOrder
20:49:13 AutoCorres2_Test: theory AutoCorres2_Test.Exception_Rewriting
20:49:13 AutoCorres2_Test: theory AutoCorres2_Test.FactorialTest
20:49:15 AutoCorres2_Test: theory HOL-Computational_Algebra.Euclidean_Algorithm
20:49:19 AutoCorres2_Test: theory AutoCorres2_Test.FibProof
20:49:24 AutoCorres2_Test: theory AutoCorres2_Test.FunctionInfoDemo
20:49:24 AutoCorres2_Test: theory AutoCorres2_Test.Global_Structs
20:49:25 AutoCorres2_Test: theory AutoCorres2_Test.Guard_Simp
20:49:26 AutoCorres2_Test: theory AutoCorres2_Test.HeapWrap
20:49:31 AutoCorres2_Test: theory HOL-Computational_Algebra.Primes
20:49:33 AutoCorres2_Test: theory AutoCorres2_Test.In_Out_Parameters_Slow
20:49:34 AutoCorres2_Test: theory AutoCorres2_Test.Incremental
20:49:41 AutoCorres2_Test: theory AutoCorres2_Test.Kmalloc
20:49:42 AutoCorres2_Test: theory AutoCorres2_Test.IsPrime_Ex
20:49:54 AutoCorres2_Test: theory AutoCorres2_Test.ListRev
20:50:05 AutoCorres2_Test: theory AutoCorres2_Test.Memcpy
20:50:07 AutoCorres2_Test: theory AutoCorres2_Test.Memset
20:50:20 AutoCorres2_Test: theory AutoCorres2_Test.MultByAdd
20:50:25 AutoCorres2_Test: theory AutoCorres2_Test.Mutual_Fixed_Points
20:50:28 AutoCorres2_Test: theory AutoCorres2_Test.Plus_Ex
20:50:31 AutoCorres2_Test: theory AutoCorres2_Test.Quicksort_Ex
20:50:41 AutoCorres2_Test: theory AutoCorres2_Test.SchorrWaite_Ex
20:50:45 poly: objsize.cpp:139: ProcessVisitAddresses::ProcessVisitAddresses(bool): Assertion `bm == nBitmaps' failed.
20:50:45 /tmp/isabelle-jenkins/bash_script18066552991993791909: Zeile 1: 1001570 Abgebrochen             (Speicherabzug geschrieben) numactl -m4 -N4 "$POLYML_EXE" -q -H 4000 --maxheap 16G --gcthreads 8 --exportstats --eval \(PolyML.SaveState.loadHierarchy\ \[\"/media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9.1_x86_64_32-linux/Pure\",\ \"/media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9.1_x86_64_32-linux/HOL\",\ \"/media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9.1_x86_64_32-linux/Simpl\",\ \"/media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9.1_x86_64_32-linux/AutoCorres2_Main\"\]\;\ PolyML.print_depth\ 0\) --eval Options.load_default\ \(\) --eval Resources.init_session_env\ \(\) --eval Command_Line.tool\ \(fn\ \(\)\ \=\>\ \(Isabelle_Process.init_build\ \(\)\)\)\;
20:50:45 AutoCorres2_Test FAILED (see also "isabelle build_log -H Error AutoCorres2_Test")
20:50:45 
20:50:45 Running Crypto_Standards (on hpcisabelle/5) ...
20:50:47 Crypto_Standards: theory Crypto_Standards.More_Bit_Operations_Nat
20:50:47 Crypto_Standards: theory HOL-Decision_Procs.Conversions
20:50:47 Crypto_Standards: theory HOL-Decision_Procs.Algebra_Aux
20:50:48 Crypto_Standards: theory Crypto_Standards.Words
20:50:49 Crypto_Standards: theory Crypto_Standards.More_Residues
20:50:49 Crypto_Standards: theory HOL-Decision_Procs.Commutative_Ring
20:50:51 Crypto_Standards: theory Crypto_Standards.FIPS180_4
20:50:51 Crypto_Standards: theory Crypto_Standards.PKCS1v2_2
20:50:57 Crypto_Standards: theory Crypto_Standards.FIPS180_4_Test_Vectors
20:51:01 Crypto_Standards: theory HOL-Decision_Procs.Reflective_Field
20:51:01 Crypto_Standards: theory Crypto_Standards.Efficient_Mod_Exp
20:51:01 Crypto_Standards: theory Crypto_Standards.PKCS1v2_2_Interpretations
20:51:05 Crypto_Standards: theory Crypto_Standards.FIPS198_1
20:51:05 Crypto_Standards: theory Crypto_Standards.FIPS198_1_Test_Vectors
20:51:07 Crypto_Standards: theory Crypto_Standards.PKCS1v2_2_Test_Vectors
20:51:14 Crypto_Standards: theory Elliptic_Curves_Group_Law.Elliptic_Locale
20:51:19 Crypto_Standards: theory Elliptic_Curves_Group_Law.Elliptic_Test
20:51:25 Crypto_Standards: theory Crypto_Standards.EC_Common
20:51:35 Crypto_Standards: theory Crypto_Standards.SEC1v2_0
20:51:52 Crypto_Standards: theory Crypto_Standards.Crypto_Standards
20:51:53 Crypto_Standards: theory Crypto_Standards.Efficient_SEC1
20:52:00 Crypto_Standards: theory Crypto_Standards.FIPS186_4_Curves
20:52:34 Crypto_Standards: theory Crypto_Standards.SEC1v2_0_Test_Vectors
20:58:12 Crypto_Standards: theory Crypto_Standards.Test_Vectors
21:05:13 Preparing Crypto_Standards/document ...
21:05:17 Finished Crypto_Standards/document (0:00:04 elapsed time)
21:05:17 Preparing Crypto_Standards/outline ...
21:05:19 Finished Crypto_Standards/outline (0:00:02 elapsed time)
21:05:20 Timing Crypto_Standards (8 threads, 861.072s elapsed time, 6436.189s cpu time, 580.756s GC time, factor 7.47)
21:05:20 Finished Crypto_Standards (0:14:24 elapsed time, 1:47:26 cpu time, factor 7.45)
21:05:20 Building Abstract-Rewriting (on hpcisabelle/6) ...
21:05:24 Abstract-Rewriting: theory Abstract-Rewriting.Seq
21:05:24 Abstract-Rewriting: theory Regular-Sets.Regular_Set
21:05:28 Abstract-Rewriting: theory Regular-Sets.Regular_Exp
21:05:31 Abstract-Rewriting: theory Regular-Sets.NDerivative
21:05:31 Abstract-Rewriting: theory Regular-Sets.Relation_Interpretation
21:05:35 Abstract-Rewriting: theory Regular-Sets.Equivalence_Checking
21:05:35 Abstract-Rewriting: theory Regular-Sets.Regexp_Method
21:05:36 Abstract-Rewriting: theory Abstract-Rewriting.Abstract_Rewriting
21:05:39 Abstract-Rewriting: theory Abstract-Rewriting.Relative_Rewriting
21:05:39 Abstract-Rewriting: theory Abstract-Rewriting.SN_Orders
21:05:42 Abstract-Rewriting: theory Abstract-Rewriting.SN_Order_Carrier
21:06:00 Preparing Abstract-Rewriting/document ...
21:06:08 Finished Abstract-Rewriting/document (0:00:08 elapsed time)
21:06:08 Preparing Abstract-Rewriting/outline ...
21:06:13 Finished Abstract-Rewriting/outline (0:00:04 elapsed time)
21:06:13 Timing Abstract-Rewriting (8 threads, 25.308s elapsed time, 86.783s cpu time, 2.477s GC time, factor 3.43)
21:06:13 Finished Abstract-Rewriting (0:00:39 elapsed time, 0:01:53 cpu time, factor 2.88)
21:06:13 Building BD_Security_Compositional (on hpcisabelle/7) ...
21:06:14 BD_Security_Compositional: theory BD_Security_Compositional.Trivial_Security
21:06:14 BD_Security_Compositional: theory BD_Security_Compositional.Composing_Security
21:06:14 BD_Security_Compositional: theory BD_Security_Compositional.Independent_Secrets
21:06:14 BD_Security_Compositional: theory BD_Security_Compositional.Transporting_Security
21:06:23 BD_Security_Compositional: theory BD_Security_Compositional.Composing_Security_Network
21:07:24 Preparing BD_Security_Compositional/document ...
21:07:29 Finished BD_Security_Compositional/document (0:00:05 elapsed time)
21:07:29 Preparing BD_Security_Compositional/outline ...
21:07:33 Finished BD_Security_Compositional/outline (0:00:03 elapsed time)
21:07:33 Timing BD_Security_Compositional (8 threads, 55.637s elapsed time, 196.499s cpu time, 5.535s GC time, factor 3.53)
21:07:33 Finished BD_Security_Compositional (0:01:10 elapsed time, 0:03:48 cpu time, factor 3.23)
21:07:33 Building First_Order_Terms (on hpcisabelle/0) ...
21:07:35 First_Order_Terms: theory First_Order_Terms.Transitive_Closure_More
21:07:35 First_Order_Terms: theory Fresh_Identifiers.Fresh
21:07:35 First_Order_Terms: theory First_Order_Terms.Lists_are_Infinite
21:07:35 First_Order_Terms: theory First_Order_Terms.Renaming2
21:07:36 First_Order_Terms: theory First_Order_Terms.Renaming2_String
21:07:36 First_Order_Terms: theory First_Order_Terms.Fun_More
21:07:36 First_Order_Terms: theory First_Order_Terms.Option_Monad
21:07:36 First_Order_Terms: theory First_Order_Terms.Seq_More
21:07:37 First_Order_Terms: theory First_Order_Terms.Term
21:07:39 First_Order_Terms: theory First_Order_Terms.Unifiers
21:07:39 First_Order_Terms: theory First_Order_Terms.Subsumption
21:07:39 First_Order_Terms: theory First_Order_Terms.Term_Pair_Multiset
21:07:39 First_Order_Terms: theory First_Order_Terms.Subterm_and_Context
21:07:40 First_Order_Terms: theory First_Order_Terms.Abstract_Matching
21:07:40 First_Order_Terms: theory First_Order_Terms.Abstract_Unification
21:07:41 First_Order_Terms: theory First_Order_Terms.Unification
21:07:43 First_Order_Terms: theory First_Order_Terms.Matching
21:07:43 First_Order_Terms: theory First_Order_Terms.Unification_String
21:07:45 First_Order_Terms: theory Deriving.Derive_Manager
21:07:45 First_Order_Terms: theory Matrix.Utility
21:07:45 First_Order_Terms: theory Deriving.Generator_Aux
21:07:46 First_Order_Terms: theory Show.Show
21:07:46 First_Order_Terms: theory Polynomial_Factorization.Missing_List
21:07:47 First_Order_Terms: theory Show.Show_Instances
21:07:48 First_Order_Terms: theory Show.Shows_Literal
21:07:49 First_Order_Terms: theory First_Order_Terms.Position
21:07:51 First_Order_Terms: theory First_Order_Terms.Term_More
21:08:18 Preparing First_Order_Terms/document ...
21:08:28 Finished First_Order_Terms/document (0:00:10 elapsed time)
21:08:28 Preparing First_Order_Terms/outline ...
21:08:34 Finished First_Order_Terms/outline (0:00:05 elapsed time)
21:08:34 Timing First_Order_Terms (8 threads, 26.464s elapsed time, 116.239s cpu time, 3.837s GC time, factor 4.39)
21:08:34 Finished First_Order_Terms (0:00:43 elapsed time, 0:02:30 cpu time, factor 3.43)
21:08:34 Building Shadow_SC_DOM (on hpcisabelle/1) ...
21:09:14 Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootClass
21:09:16 Shadow_SC_DOM: theory Shadow_SC_DOM.ShadowRootMonad
21:09:19 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM
21:10:41 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_BaseTest
21:10:52 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_adoptNode
21:10:53 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Document_getElementById
21:10:54 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_insertBefore
21:10:54 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Node_removeChild
21:10:54 Shadow_SC_DOM: theory Shadow_SC_DOM.slots
21:10:54 Shadow_SC_DOM: theory Shadow_SC_DOM.slots_fallback
21:11:06 Shadow_SC_DOM: theory Shadow_SC_DOM.Shadow_DOM_Tests
21:17:22 Preparing Shadow_SC_DOM/document ...
21:17:38 Finished Shadow_SC_DOM/document (0:00:16 elapsed time)
21:17:38 Preparing Shadow_SC_DOM/outline ...
21:17:48 Finished Shadow_SC_DOM/outline (0:00:10 elapsed time)
21:17:49 Timing Shadow_SC_DOM (8 threads, 436.127s elapsed time, 2679.363s cpu time, 193.456s GC time, factor 6.14)
21:17:49 Finished Shadow_SC_DOM (0:08:46 elapsed time, 0:48:36 cpu time, factor 5.54)
21:17:49 Running X86_Semantics (on hpcisabelle/2) ...
21:17:50 X86_Semantics: theory HOL-Eisbach.Eisbach
21:17:50 X86_Semantics: theory HOL-Library.Phantom_Type
21:17:50 X86_Semantics: theory Word_Lib.Even_More_List
21:17:50 X86_Semantics: theory HOL-Library.Sublist
21:17:50 X86_Semantics: theory Word_Lib.More_Bit_Ring
21:17:52 X86_Semantics: theory HOL-Library.Cardinality
21:17:52 X86_Semantics: theory HOL-Library.Numeral_Type
21:17:53 X86_Semantics: theory HOL-Library.Type_Length
21:17:54 X86_Semantics: theory Word_Lib.More_Arithmetic
21:17:54 X86_Semantics: theory HOL-Library.Word
21:18:04 X86_Semantics: theory Word_Lib.Bit_Comprehension
21:18:04 X86_Semantics: theory Word_Lib.Legacy_Aliases
21:18:04 X86_Semantics: theory Word_Lib.More_Divides
21:18:04 X86_Semantics: theory Word_Lib.Syntax_Bundles
21:18:04 X86_Semantics: theory Word_Lib.More_Word
21:18:06 X86_Semantics: theory Word_Lib.Bit_Shifts_Infix_Syntax
21:18:06 X86_Semantics: theory Word_Lib.Least_significant_bit
21:18:08 X86_Semantics: theory Word_Lib.Aligned
21:18:08 X86_Semantics: theory Word_Lib.Singleton_Bit_Shifts
21:18:08 X86_Semantics: theory Word_Lib.Most_significant_bit
21:18:09 X86_Semantics: theory Word_Lib.Generic_set_bit
21:18:10 X86_Semantics: theory Word_Lib.Bits_Int
21:18:14 X86_Semantics: theory Word_Lib.Typedef_Morphisms
21:18:15 X86_Semantics: theory Word_Lib.Reversed_Bit_Lists
21:18:18 X86_Semantics: theory Word_Lib.Bitwise
21:18:18 X86_Semantics: theory X86_Semantics.BitByte
21:18:19 X86_Semantics: theory X86_Semantics.Memory
21:18:19 X86_Semantics: theory X86_Semantics.State
21:18:27 X86_Semantics: theory X86_Semantics.StateCleanUp
21:18:27 X86_Semantics: theory X86_Semantics.X86_InstructionSemantics
21:18:40 X86_Semantics: theory X86_Semantics.SymbolicExecution
21:18:40 X86_Semantics: theory X86_Semantics.X86_Parse
21:18:41 X86_Semantics: theory X86_Semantics.Example_WC
21:18:41 X86_Semantics: theory X86_Semantics.Examples
21:31:27 Preparing X86_Semantics/document ...
21:31:35 Finished X86_Semantics/document (0:00:07 elapsed time)
21:31:35 Preparing X86_Semantics/outline ...
21:31:42 Finished X86_Semantics/outline (0:00:06 elapsed time)
21:31:42 Timing X86_Semantics (8 threads, 815.296s elapsed time, 1021.094s cpu time, 11.528s GC time, factor 1.25)
21:31:42 Finished X86_Semantics (0:13:37 elapsed time, 0:17:06 cpu time, factor 1.26)
21:31:42 Building CAVA_Base (on hpcisabelle/3) ...
21:31:45 CAVA_Base: theory CAVA_Base.Statistics
21:31:45 CAVA_Base: theory CAVA_Base.Lexord_List
21:31:45 CAVA_Base: theory Deriving.Comparator
21:31:45 CAVA_Base: theory Deriving.Derive_Manager
21:31:45 CAVA_Base: theory Deriving.Generator_Aux
21:31:45 CAVA_Base: theory HOL-Library.Char_ord
21:31:45 CAVA_Base: theory HOL-Library.Old_Datatype
21:31:45 CAVA_Base: theory HOL-Library.Nat_Bijection
21:31:45 CAVA_Base: theory CAVA_Base.Code_String
21:31:45 CAVA_Base: theory CAVA_Base.CAVA_Code_Target
21:31:45 CAVA_Base: theory CAVA_Base.CAVA_Base
21:31:45 CAVA_Base: theory Deriving.Equality_Generator
21:31:45 CAVA_Base: theory Deriving.Hash_Generator
21:31:46 CAVA_Base: theory HOL-Library.Countable
21:31:46 CAVA_Base: theory Deriving.Equality_Instances
21:31:46 CAVA_Base: theory Deriving.Hash_Instances
21:31:46 CAVA_Base: theory Deriving.Compare
21:31:46 CAVA_Base: theory Deriving.Comparator_Generator
21:31:46 CAVA_Base: theory CAVA_Base.All_Of_CAVA_Base
21:31:48 CAVA_Base: theory Deriving.Countable_Generator
21:31:48 CAVA_Base: theory Deriving.Compare_Generator
21:31:48 CAVA_Base: theory Deriving.Compare_Instances
21:31:49 CAVA_Base: theory Deriving.Derive
21:32:03 Timing CAVA_Base (8 threads, 6.028s elapsed time, 24.641s cpu time, 0.596s GC time, factor 4.09)
21:32:03 Finished CAVA_Base (0:00:20 elapsed time, 0:00:51 cpu time, factor 2.50)
21:32:03 Building CAVA_Automata (on hpcisabelle/4) ...
21:32:06 CAVA_Automata: theory CAVA_Automata.Step_Conv
21:32:06 CAVA_Automata: theory HOL-Library.Omega_Words_Fun
21:32:07 CAVA_Automata: theory CAVA_Automata.Digraph_Basic
21:32:07 CAVA_Automata: theory CAVA_Automata.Digraph
21:32:09 CAVA_Automata: theory CAVA_Automata.Automata
21:32:09 CAVA_Automata: theory CAVA_Automata.Digraph_Impl
21:32:16 CAVA_Automata: theory CAVA_Automata.Lasso
21:32:16 CAVA_Automata: theory CAVA_Automata.Simulation
21:32:16 CAVA_Automata: theory CAVA_Automata.Stuttering_Extension
21:32:31 CAVA_Automata: theory CAVA_Automata.Automata_Impl
21:33:13 CAVA_Automata: theory CAVA_Automata.All_Of_CAVA_Automata
21:33:29 Preparing CAVA_Automata/document ...
21:33:33 Finished CAVA_Automata/document (0:00:04 elapsed time)
21:33:34 Preparing CAVA_Automata/outline ...
21:33:37 Finished CAVA_Automata/outline (0:00:03 elapsed time)
21:33:37 Timing CAVA_Automata (8 threads, 68.555s elapsed time, 122.867s cpu time, 4.612s GC time, factor 1.79)
21:33:37 Finished CAVA_Automata (0:01:25 elapsed time, 0:02:35 cpu time, factor 1.82)
21:33:37 Building Stateful_Protocol_Composition_and_Typing (on hpcisabelle/5) ...
21:33:42 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Miscellaneous
21:33:43 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Messages
21:33:45 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.More_Unification
21:33:49 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Intruder_Deduction
21:33:51 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Strands_and_Constraints
21:34:01 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Strands
21:34:01 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Lazy_Intruder
21:34:01 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Strands
21:34:02 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typed_Model
21:34:10 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_TLS
21:34:10 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typing_Result
21:34:16 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Stateful_Strands
21:34:20 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Parallel_Compositionality
21:34:20 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Typing
21:34:39 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Compositionality
21:35:05 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_Keyserver
21:35:21 Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Examples
21:38:23 Preparing Stateful_Protocol_Composition_and_Typing/document ...
21:39:01 Finished Stateful_Protocol_Composition_and_Typing/document (0:00:37 elapsed time)
21:39:01 Preparing Stateful_Protocol_Composition_and_Typing/outline ...
21:39:17 Finished Stateful_Protocol_Composition_and_Typing/outline (0:00:16 elapsed time)
21:39:18 Timing Stateful_Protocol_Composition_and_Typing (8 threads, 236.802s elapsed time, 1393.137s cpu time, 47.026s GC time, factor 5.88)
21:39:18 Finished Stateful_Protocol_Composition_and_Typing (0:04:43 elapsed time, 0:25:06 cpu time, factor 5.32)
21:39:18 Running CoSMeDis (on hpcisabelle/6) ...
21:39:19 CoSMeDis: theory Fresh_Identifiers.Fresh
21:39:20 CoSMeDis: theory Fresh_Identifiers.Fresh_String
21:39:20 CoSMeDis: theory CoSMeDis.Prelim
21:39:27 CoSMeDis: theory CoSMeDis.System_Specification
21:39:48 CoSMeDis: theory CoSMeDis.API_Network
21:39:48 CoSMeDis: theory CoSMeDis.Automation_Setup
21:39:48 CoSMeDis: theory CoSMeDis.Safety_Properties
21:39:48 CoSMeDis: theory CoSMeDis.Friend_Intro
21:39:48 CoSMeDis: theory CoSMeDis.Friend_Observation_Setup
21:39:48 CoSMeDis: theory CoSMeDis.Friend_State_Indistinguishability
21:39:49 CoSMeDis: theory CoSMeDis.Friend_Openness
21:39:49 CoSMeDis: theory CoSMeDis.Outer_Friend_Intro
21:39:49 CoSMeDis: theory CoSMeDis.Friend_Value_Setup
21:39:49 CoSMeDis: theory CoSMeDis.Friend_Request_Intro
21:39:49 CoSMeDis: theory CoSMeDis.Friend_Request_Value_Setup
21:39:49 CoSMeDis: theory CoSMeDis.Outer_Friend
21:39:50 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Observation_Setup
21:39:50 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_Observation_Setup
21:39:51 CoSMeDis: theory CoSMeDis.Post_Intro
21:39:51 CoSMeDis: theory CoSMeDis.Post_Observation_Setup_ISSUER
21:39:51 CoSMeDis: theory CoSMeDis.Friend
21:39:52 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_State_Indistinguishability
21:39:52 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_State_Indistinguishability
21:39:52 CoSMeDis: theory CoSMeDis.Post_Observation_Setup_RECEIVER
21:39:52 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_Value_Setup
21:39:53 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Openness
21:39:53 CoSMeDis: theory CoSMeDis.Friend_Request
21:39:53 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Value_Setup
21:39:53 CoSMeDis: theory CoSMeDis.Independent_Post_Observation_Setup_ISSUER
21:39:53 CoSMeDis: theory CoSMeDis.Post_Unwinding_Helper_ISSUER
21:39:53 CoSMeDis: theory CoSMeDis.Independent_Post_Observation_Setup_RECEIVER
21:39:53 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_Value_Setup_ISSUER
21:39:54 CoSMeDis: theory CoSMeDis.Post_Unwinding_Helper_RECEIVER
21:39:55 CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_Value_Setup_ISSUER
21:39:55 CoSMeDis: theory CoSMeDis.Independent_Post_Value_Setup_RECEIVER
21:39:55 CoSMeDis: theory CoSMeDis.Post_Value_Setup_ISSUER
21:39:55 CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver
21:39:55 CoSMeDis: theory CoSMeDis.Friend_Network
21:39:56 CoSMeDis: theory CoSMeDis.Friend_Request_Network
21:39:56 CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer
21:39:56 CoSMeDis: theory CoSMeDis.Post_Value_Setup_RECEIVER
21:39:57 CoSMeDis: theory CoSMeDis.Outer_Friend_Network
21:39:58 CoSMeDis: theory CoSMeDis.Independent_Post_RECEIVER
21:39:59 CoSMeDis: theory CoSMeDis.Post_RECEIVER
21:40:00 CoSMeDis: theory CoSMeDis.Friend_All
21:40:00 CoSMeDis: theory CoSMeDis.Friend_Request_All
21:40:01 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_ISSUER
21:40:01 CoSMeDis: theory CoSMeDis.Post_ISSUER
21:40:02 CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_ISSUER
21:40:03 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_COMPOSE2
21:40:03 CoSMeDis: theory CoSMeDis.DYNAMIC_Post_Network
21:40:03 CoSMeDis: theory CoSMeDis.Post_COMPOSE2
21:40:04 CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_Network
21:40:04 CoSMeDis: theory CoSMeDis.Outer_Friend_All
21:40:04 CoSMeDis: theory CoSMeDis.Post_Network
21:40:11 CoSMeDis: theory CoSMeDis.Independent_Posts_Network
21:42:18 CoSMeDis: theory CoSMeDis.Post_All
21:52:35 Preparing CoSMeDis/document ...
21:52:52 Finished CoSMeDis/document (0:00:17 elapsed time)
21:52:52 Preparing CoSMeDis/outline ...
21:53:01 Finished CoSMeDis/outline (0:00:08 elapsed time)
21:53:01 Timing CoSMeDis (8 threads, 792.375s elapsed time, 4485.611s cpu time, 109.136s GC time, factor 5.66)
21:53:01 Finished CoSMeDis (0:13:15 elapsed time, 1:14:55 cpu time, factor 5.65)
21:53:01 Running Cook_Levin (on hpcisabelle/7) ...
21:53:04 Cook_Levin: theory Cook_Levin.Basics
21:53:04 Cook_Levin: theory HOL-Eisbach.Eisbach
21:53:07 Cook_Levin: theory Cook_Levin.Combinations
21:53:08 Cook_Levin: theory Cook_Levin.Elementary
21:53:10 Cook_Levin: theory Cook_Levin.Composing
21:53:10 Cook_Levin: theory Cook_Levin.Memorizing
21:53:11 Cook_Levin: theory Cook_Levin.Arithmetic
21:53:11 Cook_Levin: theory Cook_Levin.Oblivious
21:53:12 Cook_Levin: theory Cook_Levin.Oblivious_Polynomial
21:53:15 Cook_Levin: theory Cook_Levin.Lists_Lists
21:53:18 Cook_Levin: theory Cook_Levin.Two_Four_Symbols
21:53:19 Cook_Levin: theory Cook_Levin.Symbol_Ops
21:53:21 Cook_Levin: theory Cook_Levin.Wellformed
21:53:21 Cook_Levin: theory Cook_Levin.NP
21:53:22 Cook_Levin: theory Cook_Levin.Oblivious_2_Tape
21:53:23 Cook_Levin: theory Cook_Levin.Satisfiability
21:53:28 Cook_Levin: theory Cook_Levin.Reducing
21:53:29 Cook_Levin: theory Cook_Levin.Aux_TM_Reducing
21:53:34 Cook_Levin: theory Cook_Levin.Sat_TM_CNF
21:53:39 Cook_Levin: theory Cook_Levin.Reduction_TM
22:05:49 Preparing Cook_Levin/document ...
22:07:11 Finished Cook_Levin/document (0:01:21 elapsed time)
22:07:11 Preparing Cook_Levin/outline ...
22:07:45 Finished Cook_Levin/outline (0:00:34 elapsed time)
22:07:46 Timing Cook_Levin (8 threads, 759.949s elapsed time, 3916.436s cpu time, 32.002s GC time, factor 5.15)
22:07:46 Finished Cook_Levin (0:12:43 elapsed time, 1:05:25 cpu time, factor 5.14)
22:07:46 Building Frequency_Moments (on hpcisabelle/0) ...
22:07:51 Frequency_Moments: theory Digit_Expansions.Bits_Digits
22:07:51 Frequency_Moments: theory Flow_Networks.Graph
22:07:51 Frequency_Moments: theory HOL-Eisbach.Eisbach
22:07:51 Frequency_Moments: theory Graph_Theory.Rtrancl_On
22:07:51 Frequency_Moments: theory HOL-Combinatorics.Stirling
22:07:51 Frequency_Moments: theory HOL-Computational_Algebra.Fraction_Field
22:07:51 Frequency_Moments: theory HOL-Computational_Algebra.Group_Closure
22:07:51 Frequency_Moments: theory HOL-Decision_Procs.Dense_Linear_Order
22:07:52 Frequency_Moments: theory HOL-Computational_Algebra.Nth_Powers
22:07:52 Frequency_Moments: theory HOL-Computational_Algebra.Squarefree
22:07:52 Frequency_Moments: theory HOL-Number_Theory.Cong
22:07:52 Frequency_Moments: theory HOL-Library.Case_Converter
22:07:52 Frequency_Moments: theory HOL-Library.Code_Abstract_Nat
22:07:53 Frequency_Moments: theory Expander_Graphs.Extra_Congruence_Method
22:07:53 Frequency_Moments: theory HOL-Library.Code_Target_Nat
22:07:53 Frequency_Moments: theory HOL-Library.Code_Target_Int
22:07:54 Frequency_Moments: theory Finite_Fields.Finite_Fields_More_Bijections
22:07:54 Frequency_Moments: theory HOL-Library.Code_Lazy
22:07:54 Frequency_Moments: theory HOL-Library.Code_Target_Numeral
22:07:54 Frequency_Moments: theory HOL-Algebra.Congruence
22:07:55 Frequency_Moments: theory HOL-Computational_Algebra.Normalized_Fraction
22:07:55 Frequency_Moments: theory Card_Partitions.Injectivity_Solver
22:07:55 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
22:07:55 Frequency_Moments: theory Card_Partitions.Set_Partition
22:07:55 Frequency_Moments: theory Flow_Networks.Network
22:07:56 Frequency_Moments: theory HOL-Combinatorics.List_Permutation
22:07:56 Frequency_Moments: theory Card_Partitions.Card_Partitions
22:07:56 Frequency_Moments: theory Jordan_Normal_Form.Missing_Misc
22:07:56 Frequency_Moments: theory HOL-Library.Function_Algebras
22:07:56 Frequency_Moments: theory Abstract-Rewriting.Seq
22:07:56 Frequency_Moments: theory HOL-Library.List_Lexorder
22:07:56 Frequency_Moments: theory HOL-Library.More_List
22:07:57 Frequency_Moments: theory Perron_Frobenius.Bij_Nat
22:07:57 Frequency_Moments: theory HOL-Library.Power_By_Squaring
22:07:57 Frequency_Moments: theory HOL-Algebra.Order
22:07:57 Frequency_Moments: theory Bell_Numbers_Spivey.Bell_Numbers
22:07:57 Frequency_Moments: theory HOL-Library.Transitive_Closure_Table
22:07:57 Frequency_Moments: theory HOL-Library.While_Combinator
22:07:58 Frequency_Moments: theory HOL-Number_Theory.Mod_Exp
22:07:58 Frequency_Moments: theory HOL-Number_Theory.Eratosthenes
22:07:58 Frequency_Moments: theory Card_Equiv_Relations.Card_Equiv_Relations
22:07:58 Frequency_Moments: theory HOL-Types_To_Sets.Prerequisites
22:07:58 Frequency_Moments: theory Equivalence_Relation_Enumeration.Equivalence_Relation_Enumeration
22:07:58 Frequency_Moments: theory HOL-Types_To_Sets.Types_To_Sets
22:07:58 Frequency_Moments: theory Polynomial_Interpolation.Missing_Unsorted
22:07:58 Frequency_Moments: theory HOL-Library.Bourbaki_Witt_Fixpoint
22:07:59 Frequency_Moments: theory HOL-Computational_Algebra.Polynomial
22:07:59 Frequency_Moments: theory Jordan_Normal_Form.Conjugate
22:07:59 Frequency_Moments: theory Flow_Networks.Residual_Graph
22:07:59 Frequency_Moments: theory HOL-Types_To_Sets.Group_On_With
22:07:59 Frequency_Moments: theory Perron_Frobenius.Cancel_Card_Constraint
22:07:59 Frequency_Moments: theory HOL-Algebra.Lattice
22:08:00 Frequency_Moments: theory HOL-Library.Going_To_Filter
22:08:00 Frequency_Moments: theory Frequency_Moments.Landau_Ext
22:08:00 Frequency_Moments: theory HOL-Library.Lattice_Algebras
22:08:00 Frequency_Moments: theory HOL-Library.Log_Nat
22:08:00 Frequency_Moments: theory Graph_Theory.Stuff
22:08:00 Frequency_Moments: theory Executable_Randomized_Algorithms.Tau_Additivity
22:08:01 Frequency_Moments: theory Graph_Theory.Digraph
22:08:01 Frequency_Moments: theory HOL-Number_Theory.Fib
22:08:01 Frequency_Moments: theory HOL-Number_Theory.Prime_Powers
22:08:01 Frequency_Moments: theory HOL-Algebra.Complete_Lattice
22:08:01 Frequency_Moments: theory HOL-Number_Theory.Totient
22:08:03 Frequency_Moments: theory Flow_Networks.Augmenting_Flow
22:08:03 Frequency_Moments: theory Flow_Networks.Augmenting_Path
22:08:03 Frequency_Moments: theory HOL-Complex_Analysis.Contour_Integration
22:08:03 Frequency_Moments: theory Flow_Networks.Ford_Fulkerson
22:08:04 Frequency_Moments: theory Finite_Fields.Finite_Fields_More_PMF
22:08:04 Frequency_Moments: theory Graph_Theory.Arc_Walk
22:08:04 Frequency_Moments: theory HOL-Algebra.Group
22:08:04 Frequency_Moments: theory Graph_Theory.Bidirected_Digraph
22:08:04 Frequency_Moments: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
22:08:05 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families
22:08:06 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
22:08:06 Frequency_Moments: theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
22:08:07 Frequency_Moments: theory MFMC_Countable.MFMC_Finite
22:08:07 Frequency_Moments: theory Ergodic_Theory.SG_Library_Complement
22:08:07 Frequency_Moments: theory Graph_Theory.Pair_Digraph
22:08:07 Frequency_Moments: theory HOL-Complex_Analysis.Winding_Numbers
22:08:07 Frequency_Moments: theory Executable_Randomized_Algorithms.Coin_Space
22:08:08 Frequency_Moments: theory MFMC_Countable.MFMC_Misc
22:08:08 Frequency_Moments: theory HOL-Algebra.Coset
22:08:08 Frequency_Moments: theory HOL-Algebra.FiniteProduct
22:08:11 Frequency_Moments: theory HOL-Complex_Analysis.Cauchy_Integral_Formula
22:08:11 Frequency_Moments: theory HOL-Algebra.Ring
22:08:11 Frequency_Moments: theory MFMC_Countable.Matrix_For_Marginals
22:08:12 Frequency_Moments: theory HOL-Library.Interval
22:08:12 Frequency_Moments: theory HOL-Library.Float
22:08:13 Frequency_Moments: theory HOL-Algebra.Generated_Groups
22:08:13 Frequency_Moments: theory HOL-Algebra.Divisibility
22:08:14 Frequency_Moments: theory HOL-Algebra.Elementary_Groups
22:08:15 Frequency_Moments: theory HOL-Complex_Analysis.Conformal_Mappings
22:08:16 Frequency_Moments: theory HOL-Library.Code_Target_Numeral_Float
22:08:16 Frequency_Moments: theory HOL-Library.Interval_Float
22:08:16 Frequency_Moments: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
22:08:17 Frequency_Moments: theory HOL-Complex_Analysis.Complex_Singularities
22:08:17 Frequency_Moments: theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code
22:08:17 Frequency_Moments: theory HOL-Algebra.AbelCoset
22:08:17 Frequency_Moments: theory HOL-Algebra.Module
22:08:17 Frequency_Moments: theory Jordan_Normal_Form.Missing_Ring
22:08:18 Frequency_Moments: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
22:08:18 Frequency_Moments: theory HOL-Computational_Algebra.Polynomial_FPS
22:08:19 Frequency_Moments: theory HOL-Computational_Algebra.Polynomial_Factorial
22:08:19 Frequency_Moments: theory HOL-Decision_Procs.Approximation_Bounds
22:08:19 Frequency_Moments: theory Graph_Theory.Digraph_Component
22:08:19 Frequency_Moments: theory HOL-Computational_Algebra.Formal_Laurent_Series
22:08:22 Frequency_Moments: theory HOL-Complex_Analysis.Complex_Residues
22:08:22 Frequency_Moments: theory HOL-Complex_Analysis.Residue_Theorem
22:08:22 Frequency_Moments: theory Polynomial_Interpolation.Missing_Polynomial
22:08:23 Frequency_Moments: theory HOL-Complex_Analysis.Great_Picard
22:08:25 Frequency_Moments: theory HOL-Complex_Analysis.Riemann_Mapping
22:08:25 Frequency_Moments: theory HOL-Algebra.Ideal
22:08:27 Frequency_Moments: theory Polynomial_Factorization.Order_Polynomial
22:08:27 Frequency_Moments: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
22:08:28 Frequency_Moments: theory MFMC_Countable.Rel_PMF_Characterisation
22:08:28 Frequency_Moments: theory Median_Method.Median
22:08:28 Frequency_Moments: theory Probabilistic_While.While_SPMF
22:08:28 Frequency_Moments: theory Lp.Functional_Spaces
22:08:29 Frequency_Moments: theory HOL-Computational_Algebra.Computational_Algebra
22:08:29 Frequency_Moments: theory Graph_Theory.Digraph_Isomorphism
22:08:29 Frequency_Moments: theory HOL-Complex_Analysis.Laurent_Convergence
22:08:29 Frequency_Moments: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
22:08:30 Frequency_Moments: theory Matrix.Utility
22:08:30 Frequency_Moments: theory Polynomial_Interpolation.Ring_Hom
22:08:30 Frequency_Moments: theory Regular-Sets.Regular_Set
22:08:30 Frequency_Moments: theory VectorSpace.FunctionLemmas
22:08:30 Frequency_Moments: theory VectorSpace.RingModuleFacts
22:08:30 Frequency_Moments: theory HOL-Decision_Procs.Approximation
22:08:30 Frequency_Moments: theory HOL-Algebra.RingHom
22:08:31 Frequency_Moments: theory VectorSpace.MonoidSums
22:08:31 Frequency_Moments: theory Lp.Lp
22:08:31 Frequency_Moments: theory VectorSpace.LinearCombinations
22:08:31 Frequency_Moments: theory HOL-Algebra.QuotRing
22:08:31 Frequency_Moments: theory HOL-Algebra.UnivPoly
22:08:33 Frequency_Moments: theory Concentration_Inequalities.Concentration_Inequalities_Preliminary
22:08:33 Frequency_Moments: theory HOL-Complex_Analysis.Meromorphic
22:08:33 Frequency_Moments: theory Concentration_Inequalities.Bienaymes_Identity
22:08:33 Frequency_Moments: theory Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
22:08:34 Frequency_Moments: theory HOL-Complex_Analysis.Weierstrass_Factorization
22:08:34 Frequency_Moments: theory HOL-Complex_Analysis.Complex_Analysis
22:08:34 Frequency_Moments: theory Jordan_Normal_Form.Matrix
22:08:35 Frequency_Moments: theory Universal_Hash_Families.Pseudorandom_Objects
22:08:35 Frequency_Moments: theory HOL-Algebra.IntRing
22:08:35 Frequency_Moments: theory Expander_Graphs.Constructive_Chernoff_Bound
22:08:35 Frequency_Moments: theory Polynomial_Interpolation.Ring_Hom_Poly
22:08:36 Frequency_Moments: theory VectorSpace.SumSpaces
22:08:36 Frequency_Moments: theory VectorSpace.VectorSpace
22:08:37 Frequency_Moments: theory Commuting_Hermitian.Commuting_Hermitian_Misc
22:08:38 Frequency_Moments: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
22:08:38 Frequency_Moments: theory Jordan_Normal_Form.Column_Operations
22:08:39 Frequency_Moments: theory Jordan_Normal_Form.Determinant
22:08:39 Frequency_Moments: theory Regular-Sets.Regular_Exp
22:08:40 Frequency_Moments: theory Jordan_Normal_Form.Missing_VectorSpace
22:08:40 Frequency_Moments: theory Jordan_Normal_Form.Char_Poly
22:08:41 Frequency_Moments: theory Jordan_Normal_Form.Jordan_Normal_Form
22:08:41 Frequency_Moments: theory HOL-Algebra.Multiplicative_Group
22:08:41 Frequency_Moments: theory Isabelle_Marries_Dirac.Basics
22:08:41 Frequency_Moments: theory Isabelle_Marries_Dirac.Binary_Nat
22:08:41 Frequency_Moments: theory Isabelle_Marries_Dirac.Quantum
22:08:42 Frequency_Moments: theory Regular-Sets.NDerivative
22:08:42 Frequency_Moments: theory Regular-Sets.Relation_Interpretation
22:08:43 Frequency_Moments: theory Jordan_Normal_Form.VS_Connect
22:08:44 Frequency_Moments: theory Isabelle_Marries_Dirac.Complex_Vectors
22:08:45 Frequency_Moments: theory HOL-Algebra.Ring_Divisibility
22:08:45 Frequency_Moments: theory HOL-Algebra.Subrings
22:08:45 Frequency_Moments: theory HOL-Number_Theory.Residues
22:08:47 Frequency_Moments: theory Regular-Sets.Equivalence_Checking
22:08:47 Frequency_Moments: theory Regular-Sets.Regexp_Method
22:08:48 Frequency_Moments: theory Abstract-Rewriting.Abstract_Rewriting
22:08:48 Frequency_Moments: theory HOL-Number_Theory.Euler_Criterion
22:08:48 Frequency_Moments: theory HOL-Algebra.Embedded_Algebras
22:08:49 Frequency_Moments: theory HOL-Number_Theory.Gauss
22:08:49 Frequency_Moments: theory HOL-Number_Theory.Pocklington
22:08:49 Frequency_Moments: theory HOL-Number_Theory.Quadratic_Reciprocity
22:08:50 Frequency_Moments: theory HOL-Number_Theory.Residue_Primitive_Roots
22:08:51 Frequency_Moments: theory Lehmer.Lehmer
22:08:51 Frequency_Moments: theory HOL-Number_Theory.Number_Theory
22:08:51 Frequency_Moments: theory Pratt_Certificate.Pratt_Certificate
22:08:52 Frequency_Moments: theory Abstract-Rewriting.SN_Orders
22:08:52 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Misc
22:08:53 Frequency_Moments: theory Dirichlet_Series.Multiplicative_Function
22:08:53 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Product
22:08:54 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Series
22:08:54 Frequency_Moments: theory Dirichlet_Series.Euler_Products
22:08:54 Frequency_Moments: theory Bertrands_Postulate.Bertrand
22:08:55 Frequency_Moments: theory Matrix.Ordered_Semiring
22:08:55 Frequency_Moments: theory HOL-Algebra.Polynomials
22:08:56 Frequency_Moments: theory Matrix.Matrix_Legacy
22:08:57 Frequency_Moments: theory Jordan_Normal_Form.Gram_Schmidt
22:08:58 Frequency_Moments: theory Matrix_Tensor.Matrix_Tensor
22:09:00 Frequency_Moments: theory Dirichlet_Series.Moebius_Mu
22:09:00 Frequency_Moments: theory Dirichlet_Series.More_Totient
22:09:00 Frequency_Moments: theory Dirichlet_Series.Liouville_Lambda
22:09:00 Frequency_Moments: theory Dirichlet_Series.Divisor_Count
22:09:00 Frequency_Moments: theory Jordan_Normal_Form.Schur_Decomposition
22:09:00 Frequency_Moments: theory Dirichlet_Series.Arithmetic_Summatory
22:09:01 Frequency_Moments: theory Isabelle_Marries_Dirac.Tensor
22:09:01 Frequency_Moments: theory Dirichlet_Series.Partial_Summation
22:09:02 Frequency_Moments: theory Isabelle_Marries_Dirac.More_Tensor
22:09:02 Frequency_Moments: theory Dirichlet_Series.Dirichlet_Series_Analysis
22:09:05 Frequency_Moments: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
22:09:10 Frequency_Moments: theory Jordan_Normal_Form.Spectral_Radius
22:09:10 Frequency_Moments: theory Perron_Frobenius.HMA_Connect
22:09:11 Frequency_Moments: theory QHLProver.Complex_Matrix
22:09:13 Frequency_Moments: theory Zeta_Function.Zeta_Library
22:09:14 Frequency_Moments: theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
22:09:15 Frequency_Moments: theory HOL-Algebra.Polynomial_Divisibility
22:09:16 Frequency_Moments: theory QHLProver.Gates
22:09:17 Frequency_Moments: theory Projective_Measurements.Linear_Algebra_Complements
22:09:17 Frequency_Moments: theory Executable_Randomized_Algorithms.Randomized_Algorithm
22:09:17 Frequency_Moments: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
22:09:24 Frequency_Moments: theory Projective_Measurements.Projective_Measurements
22:09:26 Frequency_Moments: theory Commuting_Hermitian.Spectral_Theory_Complements
22:09:27 Frequency_Moments: theory Commuting_Hermitian.Commuting_Hermitian
22:09:47 Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results
22:09:47 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
22:09:49 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
22:09:54 Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
22:09:54 Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext
22:09:55 Frequency_Moments: theory Finite_Fields.Ring_Characteristic
22:09:57 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Definition
22:09:57 Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
22:09:57 Frequency_Moments: theory Frequency_Moments.K_Smallest
22:10:00 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_TTS
22:10:01 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_MGG
22:10:02 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Algebra
22:10:02 Frequency_Moments: theory Frequency_Moments.Probability_Ext
22:10:05 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Eigenvalues
22:10:05 Frequency_Moments: theory Finite_Fields.Finite_Fields_Mod_Ring_Code
22:10:05 Frequency_Moments: theory Finite_Fields.Formal_Polynomial_Derivatives
22:10:06 Frequency_Moments: theory Finite_Fields.Monic_Polynomial_Factorization
22:10:06 Frequency_Moments: theory Frequency_Moments.Frequency_Moments
22:10:07 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0
22:10:08 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2
22:10:08 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k
22:10:11 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Walks
22:10:13 Frequency_Moments: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
22:10:14 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Power_Construction
22:10:18 Frequency_Moments: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
22:10:20 Frequency_Moments: theory Finite_Fields.Finite_Fields_Poly_Ring_Code
22:10:20 Frequency_Moments: theory Finite_Fields.Rabin_Irreducibility_Test
22:10:20 Frequency_Moments: theory Finite_Fields.Card_Irreducible_Polynomials
22:10:25 Frequency_Moments: theory Expander_Graphs.Pseudorandom_Objects_Expander_Walks
22:10:27 Frequency_Moments: theory Finite_Fields.Rabin_Irreducibility_Test_Code
22:10:31 Frequency_Moments: theory Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code
22:10:39 Frequency_Moments: theory Finite_Fields.Find_Irreducible_Poly
22:10:48 Frequency_Moments: theory Universal_Hash_Families.Pseudorandom_Objects_Hash_Families
22:10:51 Frequency_Moments: theory Frequency_Moments.Tutorial_Pseudorandom_Objects
22:21:41 Preparing Frequency_Moments/document ...
22:21:50 Finished Frequency_Moments/document (0:00:08 elapsed time)
22:21:50 Preparing Frequency_Moments/outline ...
22:21:54 Finished Frequency_Moments/outline (0:00:03 elapsed time)
22:21:55 Timing Frequency_Moments (8 threads, 740.276s elapsed time, 4237.528s cpu time, 311.390s GC time, factor 5.72)
22:21:55 Finished Frequency_Moments (0:13:40 elapsed time, 1:13:45 cpu time, factor 5.40)
22:21:55 Building Padic_Ints (on hpcisabelle/1) ...
22:21:57 Padic_Ints: theory HOL-Number_Theory.Cong
22:21:57 Padic_Ints: theory Padic_Ints.Function_Ring
22:21:57 Padic_Ints: theory Padic_Ints.Supplementary_Ring_Facts
22:21:57 Padic_Ints: theory Padic_Ints.Extended_Int
22:22:00 Padic_Ints: theory HOL-Number_Theory.Totient
22:22:00 Padic_Ints: theory HOL-Number_Theory.Residues
22:22:04 Padic_Ints: theory Padic_Ints.Padic_Construction
22:22:05 Padic_Ints: theory Padic_Ints.Padic_Integers
22:22:07 Padic_Ints: theory Padic_Ints.Cring_Poly
22:23:08 Padic_Ints: theory Padic_Ints.Padic_Int_Topology
22:23:12 Padic_Ints: theory Padic_Ints.Zp_Compact
22:23:50 Padic_Ints: theory Padic_Ints.Padic_Int_Polynomials
22:23:54 Padic_Ints: theory Padic_Ints.Hensels_Lemma
22:24:32 Preparing Padic_Ints/document ...
22:25:02 Finished Padic_Ints/document (0:00:29 elapsed time)
22:25:02 Preparing Padic_Ints/outline ...
22:25:13 Finished Padic_Ints/outline (0:00:11 elapsed time)
22:25:14 Timing Padic_Ints (8 threads, 132.924s elapsed time, 551.751s cpu time, 61.486s GC time, factor 4.15)
22:25:14 Finished Padic_Ints (0:02:35 elapsed time, 0:09:58 cpu time, factor 3.85)
22:25:14 Building Sepref_Prereq (on hpcisabelle/2) ...
22:25:16 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Syntax_Match
22:25:16 Sepref_Prereq: theory HOL-Library.Nat_Bijection
22:25:16 Sepref_Prereq: theory HOL-Library.Old_Datatype
22:25:17 Sepref_Prereq: theory HOL-Library.Countable
22:25:19 Sepref_Prereq: theory HOL-Imperative_HOL.Heap
22:25:21 Sepref_Prereq: theory HOL-Imperative_HOL.Heap_Monad
22:25:23 Sepref_Prereq: theory HOL-Imperative_HOL.Array
22:25:24 Sepref_Prereq: theory HOL-Imperative_HOL.Ref
22:25:24 Sepref_Prereq: theory HOL-Imperative_HOL.Imperative_HOL
22:25:25 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
22:25:25 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Run
22:25:25 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Assertions
22:25:27 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hoare_Triple
22:25:27 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Automation
22:25:29 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Main
22:25:29 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Set_Spec
22:25:29 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_Map_Spec
22:25:29 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Imp_List_Spec
22:25:29 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Blit
22:25:29 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.List_Seg
22:25:29 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Union_Find
22:25:29 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Table
22:25:30 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Circ_List
22:25:31 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Open_List
22:25:33 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map
22:25:34 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Map_Impl
22:25:39 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Hash_Set_Impl
22:25:44 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Idioms
22:25:44 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.To_List_GA
22:25:46 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Set_Impl
22:25:46 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Array_Map_Impl
22:25:47 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.From_List_GA
22:25:48 Sepref_Prereq: theory Separation_Logic_Imperative_HOL.Sep_Examples
22:26:07 Timing Sepref_Prereq (8 threads, 34.691s elapsed time, 101.971s cpu time, 3.188s GC time, factor 2.94)
22:26:07 Finished Sepref_Prereq (0:00:52 elapsed time, 0:02:15 cpu time, factor 2.59)
22:26:07 Running MiniSail (on hpcisabelle/3) ...
22:26:09 MiniSail: theory HOL-Eisbach.Eisbach
22:26:09 MiniSail: theory FinFun.FinFun
22:26:10 MiniSail: theory HOL-Eisbach.Eisbach_Tools
22:26:11 MiniSail: theory Nominal2.Nominal2_Base
22:26:17 MiniSail: theory Nominal2.Nominal2_Abs
22:26:19 MiniSail: theory Nominal2.Nominal2_FCB
22:26:20 MiniSail: theory Nominal2.Nominal2
22:26:24 MiniSail: theory MiniSail.Nominal-Utils
22:26:25 MiniSail: theory MiniSail.Syntax
22:27:21 MiniSail: theory MiniSail.BTVSubst
22:27:21 MiniSail: theory MiniSail.IVSubst
22:27:27 MiniSail: theory MiniSail.Wellformed
22:27:27 MiniSail: theory MiniSail.SyntaxL
22:29:10 MiniSail: theory MiniSail.RCLogic
22:29:10 MiniSail: theory MiniSail.WellformedL
22:29:31 MiniSail: theory MiniSail.SubstMethods
22:29:37 MiniSail: theory MiniSail.RCLogicL
22:29:40 MiniSail: theory MiniSail.Typing
22:32:01 MiniSail: theory MiniSail.Operational
22:32:03 MiniSail: theory MiniSail.TypingL
22:32:15 MiniSail: theory MiniSail.ContextSubtypingL
22:32:18 MiniSail: theory MiniSail.BTVSubstTypingL
22:32:19 MiniSail: theory MiniSail.IVSubstTypingL
22:32:20 MiniSail: theory MiniSail.Safety
22:32:23 MiniSail: theory MiniSail.MiniSail
22:38:20 Preparing MiniSail/document ...
22:38:54 Finished MiniSail/document (0:00:33 elapsed time)
22:38:54 Preparing MiniSail/outline ...
22:39:07 Finished MiniSail/outline (0:00:13 elapsed time)
22:39:07 Timing MiniSail (8 threads, 726.216s elapsed time, 3674.566s cpu time, 222.896s GC time, factor 5.06)
22:39:07 Finished MiniSail (0:12:09 elapsed time, 1:01:23 cpu time, factor 5.05)
22:39:07 Running Modular_arithmetic_LLL_and_HNF_algorithms (on hpcisabelle/4) ...
22:39:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Equal
22:39:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Extend_Partial_Order
22:39:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.List_Fusion
22:39:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator
22:39:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Generator
22:39:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.AList
22:39:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Adhoc_Overloading
22:39:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Char_ord
22:39:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Closure_Set
22:39:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Combinatorics.List_Permutation
22:39:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.More_IArray
22:39:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Monad_Syntax
22:39:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Seq
22:39:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Auxiliary
22:39:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based
22:39:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Algebra.Divisibility
22:39:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Equality_Instances
22:39:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Type_Length
22:39:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Impl
22:39:15 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Containers_Generator
22:39:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare
22:39:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Comparator_Generator
22:39:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Lexicographic_Order
22:39:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Enum
22:39:16 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Mapping
22:39:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Eq
22:39:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Linorder
22:39:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Generator
22:39:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Word
22:39:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.Compare_Instances
22:39:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.DList_Set
22:39:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.Signed_Division
22:39:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.While_Combinator
22:39:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory Cauchy.CauchysMeanTheorem
22:39:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Improved_Code_Equations
22:39:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Neville_Aitken_Interpolation
22:39:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication
22:39:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Polynomial_Factorial
22:39:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Polynomial_Irreducibility
22:39:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Lagrange_Interpolation
22:39:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Coeff_Int
22:39:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Dichotomous_Lazard
22:39:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly
22:39:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
22:39:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.List_Representation
22:39:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Matrix.Utility
22:39:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Int_Integer_Conversion
22:39:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Divmod_Int
22:39:21 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Determinant_Impl
22:39:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gauss_Lemma
22:39:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_List
22:39:22 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Is_Rat_To_Rat
22:39:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Log_Impl
22:39:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.NthRoot_Impl
22:39:24 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Dvd_Int_Poly
22:39:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Gcd_Rat_Poly
22:39:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Sqrt_Babylonian.Sqrt_Babylonian
22:39:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Square_Free_Factorization
22:39:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Polynomial_Record_Based
22:39:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Explicit_Roots
22:39:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Missing_Multiset
22:39:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Newton_Interpolation
22:39:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.More_Missing_Multiset
22:39:26 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Sublist_Iteration
22:39:26 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Prime_Factorization
22:39:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization
22:39:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Root_Test
22:39:29 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.More_Homomorphisms
22:39:29 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Interpolation.Polynomial_Interpolation
22:39:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Resultant_Prelim
22:39:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Comprehension
22:39:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Divides
22:39:30 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Signed_Division_Word
22:39:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite
22:39:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Collection_Order
22:39:31 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Set
22:39:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory Show.Shows_Literal
22:39:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant
22:39:32 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF
22:39:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Shows_Literal_Matrix
22:39:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Kernel
22:39:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Arithmetic
22:39:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Bit_Ring
22:39:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.More_Word
22:39:35 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regular_Exp
22:39:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Word_Base
22:39:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Bit_Shifts_Infix_Syntax
22:39:37 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Least_significant_bit
22:39:38 Modular_arithmetic_LLL_and_HNF_algorithms: theory Subresultants.Subresultant_Gcd
22:39:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Most_significant_bit
22:39:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Word_Lib.Generic_set_bit
22:39:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.NDerivative
22:39:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Relation_Interpretation
22:39:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Integer_Bit
22:39:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Word_Type_Copies
22:39:41 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly
22:39:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Bivariate_Polynomials
22:39:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod
22:39:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Equivalence_Checking
22:39:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Regular-Sets.Regexp_Method
22:39:45 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.Abstract_Rewriting
22:39:46 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo
22:39:46 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
22:39:46 Modular_arithmetic_LLL_and_HNF_algorithms: theory Algebraic_Numbers.Resultant
22:39:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Orders
22:39:48 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based
22:39:51 Modular_arithmetic_LLL_and_HNF_algorithms: theory Abstract-Rewriting.SN_Order_Carrier
22:39:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Code_Target_Int_Bit
22:39:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint32
22:39:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Native_Word.Uint64
22:39:57 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization
22:39:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based
22:39:59 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization
22:40:05 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
22:40:08 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Hensel_Lifting
22:40:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_ext
22:40:33 Modular_arithmetic_LLL_and_HNF_algorithms: theory Deriving.RBT_Comparator_Impl
22:40:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT
22:40:34 Modular_arithmetic_LLL_and_HNF_algorithms: theory HOL-Library.RBT_Mapping
22:40:45 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Mapping2
22:40:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.RBT_Set2
22:40:49 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Precomputation
22:40:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory Containers.Set_Impl
22:40:50 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Kronecker_Factorization
22:40:52 Modular_arithmetic_LLL_and_HNF_algorithms: theory Polynomial_Factorization.Rational_Factorization
22:40:56 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
22:41:14 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_IArray_Impl
22:41:17 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
22:41:18 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row
22:41:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Matrix_Record_Based
22:41:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory Jordan_Normal_Form.Matrix_Impl
22:41:23 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
22:41:27 Modular_arithmetic_LLL_and_HNF_algorithms: theory Berlekamp_Zassenhaus.Berlekamp_Hensel
22:41:29 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Missing_Lemmas
22:41:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Norms
22:42:28 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Int_Rat_Operations
22:42:29 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_2
22:43:19 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.Gram_Schmidt_Int
22:43:20 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL
22:43:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Impl
22:43:53 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Number_Bounds
22:44:25 Modular_arithmetic_LLL_and_HNF_algorithms: theory LLL_Basis_Reduction.LLL_Certification
22:44:39 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm
22:44:40 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation
22:44:47 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann
22:44:51 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness
22:45:03 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl
22:45:44 Modular_arithmetic_LLL_and_HNF_algorithms: theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
22:48:33 Build timed out (after 300 minutes). Marking the build as failed.
22:48:33 Build was aborted
22:53:13 Started calculate disk usage of build
22:53:13 Finished Calculation of disk usage of build in 0 seconds
22:53:13 Started calculate disk usage of workspace
22:53:15 Finished Calculation of disk usage of workspace in  1 second
22:53:16 Email was triggered for: Failure - 1st
22:53:16 Trigger Failure - Any was overridden by another trigger and will not send an email.
22:53:16 Trigger Failure - Still was overridden by another trigger and will not send an email.
22:53:16 Sending email for trigger: Failure - 1st
22:53:16 Sending email to: isabelle-ci@mailman46.in.tum.de
22:53:16 Finished: FAILURE