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