Started by an SCM change [EnvInject] - Loading node environment variables. Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-all [isabelle-all] $ hg showconfig paths.default [isabelle-all] $ hg pull --rev default pulling from http://isabelle.in.tum.de/repos/isabelle/ searching for changes no changes found [isabelle-all] $ hg update --clean --rev default 6 files updated, 0 files merged, 0 files removed, 0 files unresolved [isabelle-all] $ hg log --rev . --template {node} [isabelle-all] $ hg log --rev . --template {rev} [isabelle-all] $ hg log --rev ab8aad4aa76e11e15da6b17a10de5e0cfa93eefc --template exists\n exists [isabelle-all] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(ab8aad4aa76e11e15da6b17a10de5e0cfa93eefc)" --encoding UTF-8 --encodingmode replace [afp] $ hg showconfig paths.default [afp] $ hg pull --rev default pulling from https://bitbucket.org/isa-afp/afp-devel/ no changes found [afp] $ hg update --clean --rev default 469 files updated, 0 files merged, 0 files removed, 0 files unresolved [afp] $ hg --config extensions.purge= clean --all [afp] $ hg log --rev . --template {node} [afp] $ hg log --rev . --template {rev} [afp] $ hg log --rev 08edeafdffe13606003e088c2f2f509ae5182fa9 --template exists\n exists [afp] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(08edeafdffe13606003e088c2f2f509ae5182fa9)" --encoding UTF-8 --encodingmode replace No emails were triggered. [isabelle-all] $ /bin/sh -xe /tmp/jenkins3446293230243963596.sh + Admin/jenkins/run_build all + set -e + PROFILE=all + shift + bin/isabelle components -a + bin/isabelle jedit -bf ### Building Isabelle/Scala ... ### Building Isabelle/jEdit ... + bin/isabelle ocaml_setup The following actions will be performed: ∗ install base-bigarray base ∗ install ocaml-base-compiler 4.05.0 [required by ocaml] ∗ install base-threads base ∗ install conf-gmp 1 ∗ install conf-perl 1 ∗ install base-unix base ∗ install conf-m4 1 ∗ install ocaml-config 1 [required by ocaml] ∗ install ocaml 4.05.0 [required by ocamlfind, zarith] ∗ install ocamlfind 1.8.0 ∗ install zarith 1.7 ===== ∗ 11 ===== <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [ocaml-base-compiler.4.05.0] found in cache [ocamlfind.1.8.0] found in cache [zarith.1.7] found in cache <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> ∗ installed base-bigarray.base ∗ installed base-threads.base ∗ installed base-unix.base ∗ installed conf-gmp.1 ∗ installed conf-m4.1 ∗ installed conf-perl.1 ∗ installed ocaml-base-compiler.4.05.0 ∗ installed ocaml-config.1 ∗ installed ocaml.4.05.0 ∗ installed ocamlfind.1.8.0 ∗ installed zarith.1.7 Done. # Run eval $(opam env) to update the current shell environment [NOTE] Package zarith is already installed (current version is 1.7). + bin/isabelle ghc_setup stack will use a sandboxed GHC it installed For more information on paths, see 'stack path' and 'stack exec env' To use this GHC and packages outside of a project, consider using: stack ghc, stack ghci, stack runghc, or stack exec The Glorious Glasgow Haskell Compilation System, version 8.4.4 + bin/isabelle ci_build_all === CONFIGURATION === ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64-linux" ML_SYSTEM="polyml-5.8" ML_OPTIONS="-H 4000 --maxheap 8G" jobs = 10, threads = 4, numa = false === BUILD === Build started at Fri, 22 Mar 2019 12:42:25 GMT Isabelle id 35ba13ac6e5c AFP id 08edeafdffe1 === LOG === Session Pure/Pure Session CTT/CTT Session Cube/Cube Session FOL/FOL Session CCL/CCL Session FOL/FOL-ex Session FOLP/FOLP Session FOLP/FOLP-ex Session HOL/HOL (main) Session AFP/AVL-Trees (AFP) Session AFP/AWN (AFP) Session AFP/Abortable_Linearizable_Modules (AFP) Session AFP/Abstract-Hoare-Logics (AFP) Session AFP/AnselmGod (AFP) Session AFP/AxiomaticCategoryTheory (AFP) Session AFP/BinarySearchTree (AFP) Session AFP/Binomial-Queues (AFP) Session AFP/Bondy (AFP) Session AFP/Bounded_Deducibility_Security (AFP) Session AFP/BytecodeLogicJmlTypes (AFP) Session AFP/CISC-Kernel (AFP) Session AFP/CYK (AFP) Session AFP/Cauchy (AFP) Session AFP/Sqrt_Babylonian (AFP) Session Doc/Classes (doc) Session AFP/ClockSynchInst (AFP) Session AFP/Compiling-Exceptions-Correctly (AFP) Session AFP/ComponentDependencies (AFP) Session AFP/Concurrent_Revisions (AFP) Session AFP/Constructor_Funs (AFP) Session AFP/CryptoBasedCompositionalProperties (AFP) Session AFP/DPT-SAT-Solver (AFP) Session AFP/Depth-First-Search (AFP) Session AFP/Diophantine_Eqns_Lin_Hom (AFP) Session AFP/DiskPaxos (AFP) Session AFP/Example-Submission (AFP) Session AFP/FFT (AFP) Session AFP/FLP (AFP) Session AFP/FeatherweightJava (AFP) Session AFP/Featherweight_OCL (AFP) Session AFP/FileRefinement (AFP) Session AFP/FocusStreamsCaseStudies (AFP) Session AFP/Free-Boolean-Algebra (AFP) Session AFP/FunWithFunctions (AFP) Session AFP/FunWithTilings (AFP) Session Doc/Functions (doc) Session AFP/GPU_Kernel_PL (AFP) Session AFP/Gauss-Jordan-Elim-Fun (AFP) Session AFP/GenClock (AFP) Session AFP/General-Triangle (AFP) Session AFP/Generic_Deriving (AFP) Session AFP/GewirthPGCProof (AFP) Session AFP/GoedelGod (AFP) Session HOL/HOL-Eisbach Session AFP/Allen_Calculus (AFP) Session AFP/Dependent_SIFUM_Type_Systems (AFP) Session AFP/Dependent_SIFUM_Refinement (AFP) Session Doc/Eisbach (doc) Session HOL/HOL-Hoare Session AFP/Case_Labeling (AFP) Session HOL/HOL-Hoare_Parallel (timing) Session HOL/HOL-IMPP Session HOL/HOL-IOA Session HOL/HOL-Import Session HOL/HOL-Lattice Session HOL/HOL-Library (main timing) Session AFP/ArrowImpossibilityGS (AFP) Session AFP/Auto2_HOL (AFP) Session AFP/BNF_CC (AFP) Session AFP/BNF_Operations (AFP) Session AFP/Binomial-Heaps (AFP) Session AFP/Boolean_Expression_Checkers (AFP) Session AFP/Buildings (AFP) Session AFP/CRDT (AFP) Session AFP/IMAP-CRDT (AFP) Session AFP/Card_Multisets (AFP) Session AFP/Card_Number_Partitions (AFP) Session AFP/Category (AFP) Session AFP/Category3 (AFP) Session AFP/MonoidalCategory (AFP) Session Doc/Codegen (doc) Session AFP/CofGroups (AFP) Session AFP/Completeness (AFP) Session AFP/ConcurrentIMP (AFP) Session AFP/Concurrent_Ref_Alg (AFP) Session AFP/CoreC++ (AFP) Session AFP/Core_DOM (AFP) Session Doc/Datatypes (doc) Session Doc/Corec (doc) Session AFP/Decl_Sem_Fun_PL (AFP) Session AFP/Derangements (AFP) Session AFP/Discrete_Summation (AFP) Session AFP/Card_Partitions (AFP) Session AFP/Bell_Numbers_Spivey (AFP) Session AFP/Card_Equiv_Relations (AFP) Session AFP/Efficient-Mergesort (AFP) Session AFP/Encodability_Process_Calculi (AFP) Session AFP/Epistemic_Logic (AFP) Session AFP/Euler_Partition (AFP) Session AFP/FOL-Fitting (AFP) Session AFP/FOL_Harrison (AFP) Session AFP/Factored_Transition_System_Bounding (AFP) Session AFP/Falling_Factorial_Sum (AFP) Session AFP/FinFun (AFP) Session AFP/Finger-Trees (AFP) Session AFP/Graph_Saturation (AFP) Session AFP/Graph_Theory (AFP) Session AFP/ShortestPath (AFP) Session AFP/Group-Ring-Module (AFP) Session AFP/Valuation (AFP) Session HOL/HOL-Auth (timing) Session HOL/HOL-UNITY (timing) Session HOL/HOL-Bali (timing) Session HOL/HOL-Cardinals (timing) Session AFP/Ordinals_and_Cardinals (AFP) Session AFP/Sort_Encodings (AFP) Session HOL/HOL-Computational_Algebra (main timing) Session AFP/Descartes_Sign_Rule (AFP) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Decision_Procs (timing) Session HOL/HOL-Quotient_Examples (timing) Session AFP/JNF-HOL-Lib (AFP) Session AFP/Localization_Ring (AFP) Session AFP/Orbit_Stabiliser (AFP) Session AFP/Perfect-Number-Thm (AFP) Session AFP/Secondary_Sylow (AFP) Session AFP/Jordan_Hoelder (AFP) Session AFP/VectorSpace (AFP) Session HOL/HOL-Analysis (main timing) Session AFP/Bernoulli (AFP) Session AFP/Cartan_FP (AFP) Session AFP/Cayley_Hamilton (AFP) Session AFP/Coinductive (AFP) Session AFP/DynamicArchitectures (AFP) Session AFP/Architectural_Design_Patterns (AFP) Session AFP/Lazy-Lists-II (AFP) Session AFP/Stream_Fusion_Code (AFP) Session AFP/Topology (AFP) Session AFP/First_Welfare_Theorem (AFP) Session AFP/Green (AFP) Session HOL/HOL-Analysis-ex Session HOL/HOL-Probability (main timing) Session AFP/Buffons_Needle (AFP) Session AFP/Density_Compiler (AFP) Session AFP/DiscretePricing (AFP) Session AFP/Ergodic_Theory (AFP) Session AFP/Gromov_Hyperbolicity (AFP) Session AFP/Fisher_Yates (AFP) Session AFP/Girth_Chromatic (AFP) Session AFP/Random_Graph_Subgraph_Threshold (AFP) Session HOL/HOL-Probability-ex (timing) Session AFP/Lp (AFP) Session AFP/Markov_Models (AFP) Session AFP/Monad_Normalisation (AFP) Session AFP/Monomorphic_Monad (AFP) Session AFP/Neumann_Morgenstern_Utility (AFP) Session AFP/Probabilistic_Noninterference (AFP) Session AFP/Probabilistic_System_Zoo (AFP) Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP) Session AFP/Source_Coding_Theorem (AFP) Session AFP/Irrationality_J_Hancl (AFP) Session AFP/Kuratowski_Closure_Complement (AFP) Session AFP/Lower_Semicontinuous (AFP) Session AFP/Minkowskis_Theorem (AFP) Session AFP/Octonions (AFP) Session AFP/Probabilistic_System_Zoo-BNFs (AFP) Session AFP/Ptolemys_Theorem (AFP) Session AFP/Quaternions (AFP) Session AFP/Rank_Nullity_Theorem (AFP) Session AFP/Gauss_Jordan (AFP) Session AFP/Echelon_Form (AFP) Session AFP/Hermite (AFP) Session AFP/Tarskis_Geometry (AFP) Session AFP/Triangle (AFP) Session AFP/Chord_Segments (AFP) Session AFP/Stewart_Apollonius (AFP) Session AFP/pGCL (AFP) Session HOL/HOL-Isar_Examples Session HOL/HOL-Nonstandard_Analysis (timing) Session HOL/HOL-Nonstandard_Analysis-Examples (timing) Session HOL/HOL-Number_Theory (main timing) Session AFP/E_Transcendental (AFP) Session AFP/Elliptic_Curves_Group_Law (AFP) Session AFP/Fermat3_4 (AFP) Session HOL/HOL-Data_Structures (timing) Session HOL/HOL-ex (timing) Session AFP/Automatic_Refinement (AFP) Session HOL/HOL-Codegenerator_Test Session AFP/Lehmer (AFP) Session AFP/Pratt_Certificate (AFP) Session AFP/Bertrands_Postulate (AFP) Session AFP/Prime_Harmonic_Series (AFP) Session AFP/RSAPSS (AFP) Session AFP/SumSquares (AFP) Session AFP/Liouville_Numbers (AFP) Session AFP/Mason_Stothers (AFP) Session AFP/Polynomial_Interpolation (AFP) Session AFP/Probabilistic_Prime_Tests (AFP) Session AFP/Rep_Fin_Groups (AFP) Session AFP/Sturm_Sequences (AFP) Session AFP/Special_Function_Bounds (AFP) Session AFP/Sturm_Tarski (AFP) Session AFP/Budan_Fourier (AFP) Session AFP/Winding_Number_Eval (AFP) Session AFP/Count_Complex_Roots (AFP) Session HOL/HOL-Corec_Examples (timing) Session HOL/HOL-Datatype_Examples (timing) Session HOL/HOL-Hahn_Banach Session HOL/HOL-IMP (timing) Session AFP/Abs_Int_ITP2012 (AFP) Session HOL/HOL-Imperative_HOL (timing) Session AFP/Auto2_Imperative_HOL (AFP) Session AFP/Imperative_Insertion_Sort (AFP) Session HOL/HOL-Induct Session HOL/HOL-Matrix_LP Session HOL/HOL-Metis_Examples (timing) Session HOL/HOL-MicroJava (timing) Session HOL/HOL-Mutabelle Session HOL/HOL-Nitpick_Examples Session HOL/HOL-Nominal Session AFP/CCS (AFP) Session HOL/HOL-Nominal-Examples (timing) Session AFP/Lam-ml-Normalization (AFP) Session AFP/Pi_Calculus (AFP) Session AFP/Psi_Calculi (AFP) Session AFP/SequentInvertibility (AFP) Session HOL/HOL-Predicate_Compile_Examples (timing) Session HOL/HOL-Quickcheck_Examples (timing) Session HOL/HOL-SET_Protocol (timing) Session HOL/HOL-TPTP Session HOL/HOL-Unix Session HOL/HOL-ZF Session AFP/Category2 (AFP) Session AFP/HereditarilyFinite (AFP) Session AFP/HyperCTL (AFP) Session AFP/Integration (AFP) Session AFP/Isabelle_Meta_Model (AFP) Session AFP/LTL (AFP) Session AFP/Stuttering_Equivalence (AFP) Session AFP/Lambda_Free_RPOs (AFP) Session AFP/Lambda_Free_EPO (AFP) Session AFP/Landau_Symbols (AFP) Session AFP/Akra_Bazzi (AFP) Session AFP/Catalan_Numbers (AFP) Session AFP/Error_Function (AFP) Session AFP/Euler_MacLaurin (AFP) Session AFP/Stirling_Formula (AFP) Session AFP/LightweightJava (AFP) Session AFP/LinearQuantifierElim (AFP) Session AFP/List-Infinite (AFP) Session AFP/Nat-Interval-Logic (AFP) Session AFP/AutoFocus-Stream (AFP) Session AFP/MuchAdoAboutTwo (AFP) Session AFP/Optics (AFP) Session AFP/UTP-Toolkit (AFP) Session AFP/UTP (AFP) Session AFP/Order_Lattice_Props (AFP) Session AFP/POPLmark-deBruijn (AFP) Session AFP/Pairing_Heap (AFP) Session AFP/Password_Authentication_Protocol (AFP) Session AFP/Pell (AFP) Session AFP/Presburger-Automata (AFP) Session AFP/Priority_Queue_Braun (AFP) Session AFP/Program-Conflict-Analysis (AFP) Session AFP/Regular-Sets (AFP) Session AFP/Abstract-Rewriting (AFP) Session AFP/Decreasing-Diagrams (AFP) Session AFP/First_Order_Terms (AFP) Session AFP/Matrix (AFP) Session AFP/Matrix_Tensor (AFP) Session AFP/Knot_Theory (AFP) Session AFP/Coinductive_Languages (AFP) Session AFP/Finite_Automata_HF (AFP) Session AFP/Functional-Automata (AFP) Session AFP/Posix-Lexing (AFP) Session AFP/Ribbon_Proofs (AFP) Session AFP/SATSolverVerification (AFP) Session AFP/Selection_Heap_Sort (AFP) Session AFP/Simplex (AFP) Session AFP/Farkas (AFP) Session AFP/Skew_Heap (AFP) Session AFP/Splay_Tree (AFP) Session AFP/Amortized_Complexity (AFP) Session AFP/Dynamic_Tables (AFP) Session AFP/Root_Balanced_Tree (AFP) Session AFP/Stable_Matching (AFP) Session AFP/SuperCalc (AFP) Session AFP/Tail_Recursive_Functions (AFP) Session AFP/TortoiseHare (AFP) Session AFP/Trie (AFP) Session AFP/Flyspeck-Tame (AFP) Session AFP/Twelvefold_Way (AFP) Session AFP/Vickrey_Clarke_Groves (AFP) Session HOL/HOL-Mirabelle Session HOL/HOL-Mirabelle-ex Session HOL/HOL-NanoJava Session HOL/HOL-Prolog Session HOL/HOL-Real_Asymp Session HOL/HOL-Real_Asymp-Manual Session HOL/HOL-Statespace Session HOL/HOL-TLA Session HOL/HOL-TLA-Buffer Session HOL/HOL-TLA-Inc Session HOL/HOL-TLA-Memory Session HOL/HOL-Types_To_Sets Session AFP/Smooth_Manifolds (AFP) Session HOL/HOL-Word (main timing) Session HOL/HOL-SPARK Session HOL/HOL-SPARK-Examples Session AFP/RIPEMD-160-SPARK (AFP) Session HOL/HOL-SPARK-Manual Session HOL/HOL-Word-SMT_Examples (timing) Session AFP/Kleene_Algebra (AFP) Session AFP/KAT_and_DRA (AFP) Session AFP/Multirelations (AFP) Session AFP/Quantales (AFP) Session AFP/Transformer_Semantics (AFP) Session AFP/Regular_Algebras (AFP) Session AFP/Relation_Algebra (AFP) Session AFP/Residuated_Lattices (AFP) Session AFP/LEM (AFP) Session AFP/Native_Word (AFP) Session AFP/WebAssembly (AFP) Session AFP/Refine_Monadic (AFP) Session AFP/Collections (AFP) Session AFP/Abstract_Completeness (AFP) Session AFP/Abstract_Soundness (AFP) Session AFP/Incredible_Proof_Machine (AFP) Session AFP/Deriving (AFP) Session AFP/CAVA_Base (AFP) Session AFP/CAVA_Automata (AFP) Session AFP/DFS_Framework (AFP) Session AFP/Gabow_SCC (AFP) Session AFP/LTL_to_GBA (AFP) Session AFP/Promela (AFP) Session AFP/Containers (AFP) Session AFP/Collections_Examples (AFP) Session AFP/Containers-Benchmarks (AFP) Session AFP/Datatype_Order_Generator (AFP) Session AFP/Old_Datatype_Show (AFP) Session AFP/Show (AFP) Session AFP/JNF-AFP-Lib (AFP) Session AFP/Real_Impl (AFP) Session AFP/QR_Decomposition (AFP) Session AFP/Dijkstra_Shortest_Path (AFP) Session AFP/Koenigsberg_Friendship (AFP) Session AFP/Transition_Systems_and_Automata (AFP) Session AFP/Buchi_Complementation (AFP) Session AFP/Partial_Order_Reduction (AFP) Session AFP/SM_Base (AFP) Session AFP/SM (AFP) Session AFP/CAVA_Setup (AFP) Session AFP/CAVA_LTL_Modelchecker (AFP) Session AFP/Transitive-Closure (AFP) Session AFP/KBPs (AFP) Session AFP/Tree-Automata (AFP) Session AFP/SPARCv8 (AFP) Session AFP/Separation_Algebra (AFP) Session AFP/Separata (AFP) Session AFP/Separation_Logic_Imperative_HOL (AFP) Session AFP/Sepref_Prereq (AFP) Session AFP/ROBDD (AFP) Session AFP/UpDown_Scheme (AFP) Session AFP/Word_Lib (AFP) Session AFP/Complx (AFP) Session AFP/IEEE_Floating_Point (AFP) Session AFP/CakeML (AFP) Session AFP/IP_Addresses (AFP) Session AFP/Simple_Firewall (AFP) Session AFP/Routing (AFP) Session AFP/Iptables_Semantics (AFP) Session AFP/Iptables_Semantics_Examples (AFP) Session AFP/LOFT (AFP) Session HOL/HOLCF (main timing) Session AFP/Circus (AFP) Session HOL/HOLCF-IMP Session HOL/HOLCF-Library Session HOL/HOLCF-FOCUS Session HOL/HOLCF-ex Session AFP/PCF (AFP) Session AFP/HOLCF-Prelude (AFP) Session HOL/HOLCF-Tutorial Session HOL/IOA (timing) Session HOL/IOA-ABP Session HOL/IOA-NTP Session HOL/IOA-Storage Session HOL/IOA-ex Session AFP/Shivers-CFA (AFP) Session AFP/Stream-Fusion (AFP) Session AFP/Tycon (AFP) Session AFP/WorkerWrapper (AFP) Session AFP/Heard_Of (AFP) Session AFP/Consensus_Refined (AFP) Session AFP/Hoare_Time (AFP) Session AFP/HotelKeyCards (AFP) Session Doc/How_to_Prove_it (no_doc) Session AFP/Huffman (AFP) Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP) Session AFP/IMP2 (AFP) Session Doc/Implementation (doc) Session AFP/Impossible_Geometry (AFP) Session AFP/Inductive_Confidentiality (AFP) Session AFP/InfPathElimination (AFP) Session Doc/Isar_Ref (doc) Session Doc/JEdit (doc) Session AFP/JiveDataStoreModel (AFP) Session AFP/KAD (AFP) Session AFP/Algebraic_VCs (AFP) Session AFP/Key_Agreement_Strong_Adversaries (AFP) Session AFP/LambdaMu (AFP) Session AFP/LatticeProperties (AFP) Session AFP/DataRefinementIBP (AFP) Session AFP/GraphMarkingIBP (AFP) Session AFP/Lazy_Case (AFP) Session AFP/Dict_Construction (AFP) Session AFP/Lifting_Definition_Option (AFP) Session AFP/List-Index (AFP) Session AFP/Affine_Arithmetic (AFP) Session AFP/Taylor_Models (AFP) Session AFP/Comparison_Sort_Lower_Bound (AFP) Session AFP/Formula_Derivatives (AFP) Session AFP/Formula_Derivatives-Examples (AFP) Session AFP/Higher_Order_Terms (AFP) Session AFP/Jinja (AFP) Session AFP/HRB-Slicing (AFP) Session AFP/InformationFlowSlicing_Inter (AFP) Session AFP/Slicing (AFP) Session AFP/Formal_SSA (AFP) Session AFP/Minimal_SSA (AFP) Session AFP/InformationFlowSlicing (AFP) Session AFP/LTL_to_DRA (AFP) Session AFP/List_Update (AFP) Session AFP/Ordinary_Differential_Equations (AFP) Session AFP/Differential_Dynamic_Logic (AFP) Session AFP/HOL-ODE-Numerics (AFP) Session AFP/HOL-ODE-ARCH-COMP (AFP) Session AFP/HOL-ODE-Examples (AFP large) Session AFP/Lorenz_Approximation (AFP) Session AFP/Lorenz_C0 (AFP large) Session AFP/Lorenz_C1 (AFP large) Session AFP/Quick_Sort_Cost (AFP) Session AFP/Random_BSTs (AFP) Session AFP/Randomised_BSTs (AFP) Session AFP/Treaps (AFP) Session AFP/Randomised_Social_Choice (AFP) Session AFP/Fishburn_Impossibility (AFP) Session AFP/SDS_Impossibility (AFP) Session AFP/Refine_Imperative_HOL (AFP) Session AFP/Floyd_Warshall (AFP) Session AFP/Sepref_Basic (AFP) Session AFP/Sepref_IICF (AFP) Session AFP/Flow_Networks (AFP) Session AFP/EdmondsKarp_Maxflow (AFP) Session AFP/MFMC_Countable (AFP) Session AFP/Prpu_Maxflow (AFP) Session AFP/Knuth_Morris_Pratt (AFP) Session AFP/VerifyThis2018 (AFP) Session AFP/List_Interleaving (AFP) Session AFP/List_Inversions (AFP) Session AFP/LocalLexing (AFP) Session Doc/Locales (doc) Session AFP/Lowe_Ontological_Argument (AFP) Session AFP/MSO_Regex_Equivalence (AFP) Session Doc/Main (doc) Session AFP/Marriage (AFP) Session AFP/Latin_Square (AFP) Session AFP/Matroids (AFP) Session AFP/Kruskal (AFP) Session AFP/Max-Card-Matching (AFP) Session AFP/Median_Of_Medians_Selection (AFP) Session AFP/Menger (AFP) Session AFP/MiniML (AFP) Session AFP/Modular_Assembly_Kit_Security (AFP) Session AFP/Monad_Memo_DP (AFP) Session AFP/Hidden_Markov_Models (AFP) Session AFP/Optimal_BST (AFP) Session AFP/MonoBoolTranAlgebra (AFP) Session AFP/Name_Carrying_Type_Inference (AFP) Session AFP/Network_Security_Policy_Verification (AFP) Session AFP/No_FTL_observers (AFP) Session AFP/Nominal2 (AFP) Session AFP/Incompleteness (AFP) Session AFP/Surprise_Paradox (AFP) Session AFP/Launchbury (AFP) Session AFP/Call_Arity (AFP) Session AFP/Modal_Logics_for_NTS (AFP) Session AFP/Rewriting_Z (AFP) Session AFP/Noninterference_CSP (AFP) Session AFP/Noninterference_Ipurge_Unwinding (AFP) Session AFP/Noninterference_Generic_Unwinding (AFP) Session AFP/Noninterference_Inductive_Unwinding (AFP) Session AFP/Noninterference_Sequential_Composition (AFP) Session AFP/Noninterference_Concurrent_Composition (AFP) Session AFP/NormByEval (AFP) Session AFP/OpSets (AFP) Session AFP/Open_Induction (AFP) Session AFP/Well_Quasi_Orders (AFP) Session AFP/Decreasing-Diagrams-II (AFP) Session AFP/Myhill-Nerode (AFP) Session AFP/Polynomials (AFP) Session AFP/Symmetric_Polynomials (AFP) Session AFP/Pi_Transcendental (AFP) Session AFP/Ordinal (AFP) Session AFP/Nested_Multisets_Ordinals (AFP) Session AFP/Lambda_Free_KBOs (AFP) Session AFP/Ordered_Resolution_Prover (AFP) Session AFP/PLM (AFP) Session AFP/PSemigroupsConvolution (AFP) Session AFP/Paraconsistency (AFP) Session AFP/Parity_Game (AFP) Session AFP/Partial_Function_MR (AFP) Session AFP/Certification_Monads (AFP) Session AFP/XML (AFP) Session AFP/Pre_Polynomial_Factorization (AFP) Session AFP/Polynomial_Factorization (AFP) Session AFP/Dirichlet_Series (AFP) Session AFP/Zeta_Function (AFP) Session AFP/Dirichlet_L (AFP) Session AFP/Prime_Number_Theorem (AFP) Session AFP/Prime_Distribution_Elementary (AFP) Session AFP/Functional_Ordered_Resolution_Prover (AFP) Session AFP/Jordan_Normal_Form (AFP) Session AFP/Deep_Learning (AFP) Session AFP/Groebner_Bases (AFP) Session AFP/Signature_Groebner (AFP) Session AFP/Linear_Recurrences (AFP) Session AFP/Perron_Frobenius (AFP) Session AFP/Stochastic_Matrices (AFP) Session AFP/Subresultants (AFP) Session AFP/Pre_BZ (AFP) Session AFP/Berlekamp_Zassenhaus (AFP) Session AFP/Algebraic_Numbers (AFP) Session AFP/LLL_Basis_Reduction (AFP) Session AFP/LLL_Factorization (AFP) Session AFP/Linear_Recurrences_Solver (AFP) Session AFP/Probabilistic_While (AFP) Session AFP/Pop_Refinement (AFP) Session AFP/Possibilistic_Noninterference (AFP) Session Doc/Prog_Prove (doc) Session AFP/Projective_Geometry (AFP) Session AFP/Proof_Strategy_Language (AFP) Session AFP/PropResPI (AFP) Session AFP/Propositional_Proof_Systems (AFP) Session AFP/PseudoHoops (AFP) Session AFP/Ramsey-Infinite (AFP) Session AFP/Recursion-Theory-I (AFP) Session AFP/Minsky_Machines (AFP) Session AFP/RefinementReactive (AFP) Session AFP/Resolution_FOL (AFP) Session AFP/Robbins-Conjecture (AFP) Session AFP/Roy_Floyd_Warshall (AFP) Session AFP/SIFPL (AFP) Session AFP/SIFUM_Type_Systems (AFP) Session AFP/Security_Protocol_Refinement (AFP) Session AFP/SenSocialChoice (AFP) Session AFP/Simpl (AFP) Session AFP/BDD (AFP) Session AFP/Planarity_Certificates (AFP) Session AFP/Statecharts (AFP) Session AFP/Stone_Algebras (AFP) Session AFP/Stone_Relation_Algebras (AFP) Session AFP/Stone_Kleene_Relation_Algebras (AFP) Session AFP/Aggregation_Algebras (AFP) Session AFP/Store_Buffer_Reduction (AFP) Session AFP/Strong_Security (AFP) Session Doc/Sugar (doc) Session AFP/TLA (AFP) Session AFP/Timed_Automata (AFP) Session AFP/Probabilistic_Timed_Automata (AFP) Session AFP/Transitive-Closure-II (AFP) Session AFP/Tree_Decomposition (AFP) Session Doc/Tutorial (doc) Session Doc/Typeclass_Hierarchy (doc) Session AFP/Types_Tableaus_and_Goedels_God (AFP) Session AFP/UPF (AFP) Session AFP/UPF_Firewall (AFP) Session AFP/Universal_Turing_Machine (AFP) Session AFP/Verified-Prover (AFP) Session AFP/VolpanoSmith (AFP) Session AFP/WHATandWHERE_Security (AFP) Session AFP/Weight_Balanced_Trees (AFP) Session HOL/HOL-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-Lambda (timing) Session AFP/Applicative_Lifting (AFP) Session AFP/CryptHOL (AFP) Session AFP/Constructive_Cryptography (AFP) Session AFP/Game_Based_Crypto (AFP) Session AFP/Free-Groups (AFP) Session AFP/Locally-Nameless-Sigma (AFP) Session AFP/Stern_Brocot (AFP) Session HOL/HOL-Proofs-ex Session Tools/Haskell Session Doc/Intro (doc) Session LCF/LCF Session Doc/Logics (doc) Session Doc/Nitpick (doc) Session Tools/SML Session Sequents/Sequents Session Doc/Sledgehammer (doc) Session Tools/Spec_Check Session AFP/Regex_Equivalence (AFP) Session Doc/System (doc) Session ZF/ZF (main timing) Session Doc/Logics_ZF (doc) Session ZF/ZF-AC Session ZF/ZF-Coind Session ZF/ZF-Constructible Session ZF/ZF-IMP Session ZF/ZF-Induct Session ZF/ZF-UNITY (timing) Session ZF/ZF-Resid Session ZF/ZF-ex Building HOL-Analysis ... Building LLL_Basis_Reduction ... Running Perron_Frobenius ... Building Coinductive ... Running Higher_Order_Terms ... Running Lambda_Free_EPO ... Running Lambda_Free_KBOs ... Running Lambda_Free_RPOs ... Running Functional_Ordered_Resolution_Prover ... Running Noninterference_Generic_Unwinding ... HOL-Analysis: theory HOL-Library.Cancellation HOL-Analysis: theory HOL-Library.Disjoint_Sets HOL-Analysis: theory HOL-Library.FuncSet HOL-Analysis: theory HOL-Library.Infinite_Set Higher_Order_Terms: theory HOL-Library.Adhoc_Overloading Higher_Order_Terms: theory HOL-Library.Conditional_Parametricity Higher_Order_Terms: theory HOL-Library.AList Higher_Order_Terms: theory HOL-Library.Nat_Bijection HOL-Analysis: theory HOL-Library.Nat_Bijection Coinductive: theory Coinductive.Resumption Coinductive: theory HOL-Analysis.Inner_Product Coinductive: theory HOL-Analysis.Abstract_Topology Coinductive: theory HOL-Analysis.L2_Norm Higher_Order_Terms: theory HOL-Library.Monad_Syntax HOL-Analysis: theory HOL-Library.Old_Datatype Higher_Order_Terms: theory HOL-Library.State_Monad Noninterference_Generic_Unwinding: theory Noninterference_Generic_Unwinding.GenericUnwinding Coinductive: theory HOL-Analysis.Product_Vector Lambda_Free_EPO: theory HOL-Cardinals.Order_Union Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Util Lambda_Free_RPOs: theory HOL-Cardinals.Order_Union Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Util Higher_Order_Terms: theory HOL-Library.Old_Datatype Lambda_Free_EPO: theory HOL-Cardinals.Wellorder_Extension HOL-Analysis: theory HOL-Library.Phantom_Type Higher_Order_Terms: theory List-Index.List_Index HOL-Analysis: theory HOL-Library.Multiset HOL-Analysis: theory HOL-Library.Product_Plus Lambda_Free_RPOs: theory HOL-Cardinals.Wellorder_Extension HOL-Analysis: theory HOL-Library.Product_Order HOL-Analysis: theory HOL-Library.Set_Algebras Perron_Frobenius: theory HOL-Eisbach.Eisbach Perron_Frobenius: theory HOL-Analysis.Continuum_Not_Denumerable Perron_Frobenius: theory HOL-Types_To_Sets.Types_To_Sets Perron_Frobenius: theory HOL-Analysis.Abstract_Topology HOL-Analysis: theory HOL-Library.Countable HOL-Analysis: theory HOL-Analysis.Inner_Product LLL_Basis_Reduction: theory LLL_Basis_Reduction.More_IArray LLL_Basis_Reduction: theory LLL_Basis_Reduction.Cost LLL_Basis_Reduction: theory LLL_Basis_Reduction.List_Representation LLL_Basis_Reduction: theory Algebraic_Numbers.Bivariate_Polynomials Higher_Order_Terms: theory HOL-Library.Countable Perron_Frobenius: theory HOL-Analysis.Inner_Product HOL-Analysis: theory HOL-Library.Cardinality Coinductive: theory Coinductive.Coinductive_Nat Perron_Frobenius: theory HOL-Analysis.L2_Norm Lambda_Free_EPO: theory Lambda_Free_RPOs.Infinite_Chain Coinductive: theory HOL-Analysis.Elementary_Topology Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Term Perron_Frobenius: theory HOL-Analysis.Operator_Norm Coinductive: theory HOL-Analysis.Euclidean_Space Lambda_Free_RPOs: theory Lambda_Free_RPOs.Infinite_Chain Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Term Lambda_Free_EPO: theory Lambda_Free_RPOs.Extension_Orders Lambda_Free_RPOs: theory Lambda_Free_RPOs.Extension_Orders Perron_Frobenius: theory HOL-Analysis.Product_Vector Perron_Frobenius: theory Polynomial_Factorization.Polynomial_Divisibility Perron_Frobenius: theory Sturm_Sequences.Misc_Polynomial Perron_Frobenius: theory Sturm_Sequences.Sturm_Library Perron_Frobenius: theory Sturm_Sequences.Sturm_Theorem LLL_Basis_Reduction: theory Algebraic_Numbers.Resultant Perron_Frobenius: theory HOL-Analysis.Norm_Arith Coinductive: theory Coinductive.Coinductive_List HOL-Analysis: theory HOL-Analysis.L2_Norm HOL-Analysis: theory HOL-Analysis.Operator_Norm HOL-Analysis: theory HOL-Library.Countable_Set HOL-Analysis: theory HOL-Analysis.Poly_Roots HOL-Analysis: theory HOL-Library.Numeral_Type HOL-Analysis: theory HOL-Analysis.Product_Vector Perron_Frobenius: theory Polynomial_Factorization.Square_Free_Factorization Higher_Order_Terms: theory HOL-Library.FSet Perron_Frobenius: theory HOL-Analysis.Elementary_Topology HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Fun_More Functional_Ordered_Resolution_Prover: theory Deriving.Generator_Aux Functional_Ordered_Resolution_Prover: theory Deriving.Comparator Functional_Ordered_Resolution_Prover: theory Deriving.Derive_Manager Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Transitive_Closure_More Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Order_Union Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Generator Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Wellorder_Extension Coinductive: theory HOL-Analysis.Linear_Algebra Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Option_Monad HOL-Analysis: theory HOL-Library.Set_Idioms HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable Perron_Frobenius: theory HOL-Analysis.Euclidean_Space Coinductive: theory HOL-Analysis.Norm_Arith HOL-Analysis: theory HOL-Analysis.Abstract_Topology Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Instances HOL-Analysis: theory HOL-Analysis.Elementary_Topology Functional_Ordered_Resolution_Prover: theory Nested_Multisets_Ordinals.Multiset_More Coinductive: theory HOL-Analysis.Abstract_Topology_2 Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Seq Functional_Ordered_Resolution_Prover: theory Deriving.Compare Functional_Ordered_Resolution_Prover: theory Deriving.Comparator_Generator Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Encoding Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_App Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Std Lambda_Free_EPO: theory Lambda_Free_EPO.Embeddings Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Seq_More Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Clausal_Logic Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unifiers Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term_Pair_Multiset LLL_Basis_Reduction: theory LLL_Basis_Reduction.Missing_Lemmas Perron_Frobenius: theory HOL-Analysis.Abstract_Limits Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Subsumption Lambda_Free_KBOs: theory HOL-Cardinals.Order_Union Lambda_Free_KBOs: theory Abstract-Rewriting.Seq Lambda_Free_KBOs: theory HOL-Library.While_Combinator Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Free_Util HOL-Analysis: theory HOL-Analysis.Euclidean_Space Perron_Frobenius: theory Sturm_Sequences.Sturm_Method Lambda_Free_KBOs: theory HOL-Cardinals.Wellorder_Extension Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Generator Lambda_Free_KBOs: theory Matrix.Utility Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Optim Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits_Bit Lambda_Free_KBOs: theory Regular-Sets.Regular_Set Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Herbrand_Interpretation HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_Numeric Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Instances Perron_Frobenius: theory HOL-Analysis.Abstract_Topology_2 Functional_Ordered_Resolution_Prover: theory HOL-Word.Bit_Representation Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Ground_Resolution_Model Coinductive: theory HOL-Analysis.Connected Coinductive: theory HOL-Analysis.Elementary_Metric_Spaces Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPOs Perron_Frobenius: theory Rank_Nullity_Theorem.Dual_Order Lambda_Free_KBOs: theory Lambda_Free_RPOs.Infinite_Chain Perron_Frobenius: theory HOL-Analysis.Finite_Cartesian_Product Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Inference_System Lambda_Free_KBOs: theory Lambda_Free_RPOs.Extension_Orders Perron_Frobenius: theory HOL-Analysis.Linear_Algebra Functional_Ordered_Resolution_Prover: theory HOL-Word.Word_Miscellaneous Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits_Int Lambda_Free_EPO: theory Lambda_Free_EPO.Chop Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Free_Term Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_Typedef Functional_Ordered_Resolution_Prover: theory Deriving.Countable_Generator Higher_Order_Terms: theory HOL-Library.Finite_Map Lambda_Free_EPO: theory Lambda_Free_EPO.Lambda_Free_EPO Functional_Ordered_Resolution_Prover: theory Coinductive.Coinductive_Nat HOL-Analysis: theory HOL-Library.Permutations Functional_Ordered_Resolution_Prover: theory Matrix.Utility Functional_Ordered_Resolution_Prover: theory Polynomial_Factorization.Missing_List Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Ordered_Ground_Resolution Perron_Frobenius: theory HOL-Analysis.Convex Perron_Frobenius: theory HOL-Analysis.Connected Perron_Frobenius: theory HOL-Analysis.Elementary_Metric_Spaces Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Unordered_Ground_Resolution Functional_Ordered_Resolution_Prover: theory HOL-Word.Bool_List_Representation Functional_Ordered_Resolution_Prover: theory Coinductive.Coinductive_List HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product Lambda_Free_KBOs: theory Regular-Sets.Regular_Exp Functional_Ordered_Resolution_Prover: theory Open_Induction.Restricted_Predicates Perron_Frobenius: theory HOL-Analysis.Cartesian_Space HOL-Analysis: theory HOL-Analysis.Linear_Algebra Functional_Ordered_Resolution_Prover: theory Native_Word.More_Bits_Int Functional_Ordered_Resolution_Prover: theory HOL-Word.Word HOL-Analysis: theory HOL-Analysis.Abstract_Limits Coinductive: theory HOL-Analysis.Elementary_Normed_Spaces Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Encoding HOL-Analysis: theory HOL-Library.Discrete HOL-Analysis: theory HOL-Library.Indicator_Function HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2 Perron_Frobenius: theory HOL-Analysis.Elementary_Normed_Spaces HOL-Analysis: theory HOL-Analysis.Convex Perron_Frobenius: theory HOL-Analysis.Determinants Coinductive: theory HOL-Analysis.Topology_Euclidean_Space Coinductive: theory Coinductive.Coinductive_List_Prefix Perron_Frobenius: theory HOL-Analysis.Topology_Euclidean_Space Coinductive: theory Coinductive.Hamming_Stream Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Map2 HOL-Analysis: theory HOL-Analysis.Cartesian_Space Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Abstract_Substitution Coinductive: theory Coinductive.Koenigslemma Lambda_Free_KBOs: theory Regular-Sets.NDerivative Lambda_Free_KBOs: theory Regular-Sets.Relation_Interpretation Coinductive: theory Coinductive.LMirror Coinductive: theory Coinductive.Lazy_LList Coinductive: theory Coinductive.Quotient_Coinductive_List HOL-Analysis: theory HOL-Analysis.Connected Functional_Ordered_Resolution_Prover: theory Native_Word.Bits_Integer Coinductive: theory Coinductive.TLList Coinductive: theory Coinductive.Coinductive_Stream HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces HOL-Analysis: theory HOL-Library.Liminf_Limsup HOL-Analysis: theory HOL-Analysis.Determinants HOL-Analysis: theory HOL-Library.Nonpos_Ints Coinductive: theory HOL-Analysis.Extended_Real_Limits HOL-Analysis: theory HOL-Library.Order_Continuity HOL-Analysis: theory HOL-Library.Periodic_Fun HOL-Analysis: theory HOL-Library.Sum_of_Squares HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm Perron_Frobenius: theory HOL-Analysis.Convex_Euclidean_Space Perron_Frobenius: theory HOL-Analysis.Extended_Real_Limits Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Set HOL-Analysis: theory HOL-Library.Extended_Nat HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/outline.pdf Lambda_Free_RPOs FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_RPOs) assumes "rpo_optim ground_heads_var (>\<^sub>s) extf arity_sym arity_var" Proofs for inductive predicate(s) "gt" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... locale rpo fixes ground_heads_var :: "'v \ 's set" and gt_sym :: "'s \ 's \ bool" (infix \>\<^sub>s\ 50) and extf :: "'s \ (('s, 'v) tm \ ('s, 'v) tm \ bool) \ ('s, 'v) tm list \ ('s, 'v) tm list \ bool" and arity_sym :: "'s \ enat" and arity_var :: "'v \ enat" assumes "rpo ground_heads_var (>\<^sub>s) extf arity_sym arity_var" ### theory "Lambda_Free_RPOs.Lambda_Free_RPO_Optim" ### 0.788s elapsed time, 2.928s cpu time, 0.000s GC time Loading theory "Lambda_Free_RPOs.Lambda_Free_RPOs" locale simple_rpo_instances ### theory "Lambda_Free_RPOs.Lambda_Free_RPOs" ### 1.133s elapsed time, 4.528s cpu time, 0.000s GC time isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/outline -o pdf -n outline -t /proof,/ML isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/document -o pdf -n document *** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy") Coinductive: theory Coinductive.CCPO_Topology Lambda_Free_KBOs: theory Regular-Sets.Equivalence_Checking Coinductive: theory Coinductive.Lazy_TLList Perron_Frobenius: theory HOL-Analysis.Function_Topology Lambda_Free_KBOs: theory Regular-Sets.Regexp_Method HOL-Analysis: theory HOL-Library.Extended_Real Coinductive: theory Coinductive.Quotient_TLList Perron_Frobenius: theory HOL-Analysis.Starlike Perron_Frobenius: theory HOL-Analysis.Summation_Tests Coinductive: theory Coinductive.TLList_CCPO Functional_Ordered_Resolution_Prover: theory Native_Word.Word_Misc Lambda_Free_KBOs: theory Abstract-Rewriting.Abstract_Rewriting Coinductive: theory Coinductive.LList_CCPO_Topology Coinductive: theory Coinductive.Coinductive Coinductive: theory Coinductive.TLList_CCPO_Examples Perron_Frobenius: theory HOL-Analysis.Uniform_Limit Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Exp HOL-Analysis: theory HOL-Analysis.Norm_Arith Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Lazy_List_Liminf Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Lazy_List_Chain Perron_Frobenius: theory HOL-Analysis.Bounded_Linear_Function HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space Coinductive: theory Coinductive.Coinductive_Examples Lambda_Free_KBOs: theory Abstract-Rewriting.SN_Orders Perron_Frobenius: theory HOL-Analysis.Continuous_Extension Perron_Frobenius: theory HOL-Analysis.Path_Connected Higher_Order_Terms: theory Higher_Order_Terms.Term_Utils Higher_Order_Terms: theory Higher_Order_Terms.Find_First Higher_Order_Terms: theory Higher_Order_Terms.Disjoint_Sets HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real Lambda_Free_KBOs: theory Polynomials.Polynomials Higher_Order_Terms: theory Deriving.Derive_Manager Higher_Order_Terms: theory HOL-Library.Cancellation Higher_Order_Terms: theory HOL-Library.Infinite_Set Higher_Order_Terms: theory HOL-ex.Unification Higher_Order_Terms: theory Datatype_Order_Generator.Derive_Aux Higher_Order_Terms: theory Datatype_Order_Generator.Order_Generator Higher_Order_Terms: theory HOL-Library.Countable_Set Functional_Ordered_Resolution_Prover: theory Regular-Sets.NDerivative Functional_Ordered_Resolution_Prover: theory Regular-Sets.Relation_Interpretation Higher_Order_Terms: theory Higher_Order_Terms.Fresh_Monad Higher_Order_Terms: theory HOL-Library.Multiset Higher_Order_Terms: theory Higher_Order_Terms.Name Higher_Order_Terms: theory HOL-Library.Countable_Complete_Lattices HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Function_Topology HOL-Analysis: theory HOL-Computational_Algebra.Primes Perron_Frobenius: theory HOL-Analysis.Homotopy Higher_Order_Terms: theory Higher_Order_Terms.Fresh_Class HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series HOL-Analysis: theory HOL-Analysis.Product_Topology Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding Noninterference_Generic_Unwinding FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Noninterference_Generic_Unwinding) Loading theory "Noninterference_Generic_Unwinding.GenericUnwinding" Proofs for inductive predicate(s) "rel_induct_auxp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... *** Failed to apply initial proof method (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"): *** goal (1 subgoal): *** 1. unaffected_domains I D {D y} (ys @ [y']) \ {} *** At command "proof" (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy") *** Failed to apply initial proof method (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"): *** goal (1 subgoal): *** 1. unaffected_domains I D {D y} (zs @ [z]) \ {} *** At command "proof" (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy") ### theory "Noninterference_Generic_Unwinding.GenericUnwinding" ### 2.071s elapsed time, 4.940s cpu time, 0.156s GC time isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/outline -o pdf -n outline -t /proof,/ML *** Failed to build document in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/outline" *** Failed to apply initial proof method (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"): *** goal (1 subgoal): *** 1. unaffected_domains I D {D y} (zs @ [z]) \ {} *** At command "proof" (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy") *** Failed to apply initial proof method (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"): *** goal (1 subgoal): *** 1. unaffected_domains I D {D y} (ys @ [y']) \ {} *** At command "proof" (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy") Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/outline.pdf Lambda_Free_EPO FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_EPO) Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "gt_chop" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "gt_diff" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "gt_same" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Lambda_Free_EPO.Lambda_Free_EPO" ### 1.224s elapsed time, 4.532s cpu time, 0.180s GC time \?X \ ?C; ?A \ ?X\ \ ?A \ \ ?C ?P ?a \ ?a \ {x. ?P x} isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/outline -o pdf -n outline -t /proof,/ML *** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy") HOL-Analysis: theory HOL-Analysis.Sigma_Algebra Higher_Order_Terms: theory Higher_Order_Terms.Term_Class HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits HOL-Analysis: theory HOL-Analysis.Starlike Higher_Order_Terms: theory HOL-Library.Order_Continuity HOL-Analysis: theory HOL-Analysis.Summation_Tests Higher_Order_Terms: theory HOL-Library.Extended_Nat Perron_Frobenius: theory HOL-Analysis.Homeomorphism LLL_Basis_Reduction: theory LLL_Basis_Reduction.Norms Functional_Ordered_Resolution_Prover: theory Native_Word.Uint32 Functional_Ordered_Resolution_Prover: theory Regular-Sets.Equivalence_Checking Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regexp_Method Perron_Frobenius: theory HOL-Analysis.Brouwer_Fixpoint HOL-Analysis: theory HOL-Analysis.Uniform_Limit HOL-Analysis: theory HOL-Analysis.Measurable Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Proving_Process Higher_Order_Terms: theory HOL-Library.Multiset_Order Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Abstract_Rewriting HOL-Analysis: theory HOL-Analysis.Continuous_Extension HOL-Analysis: theory HOL-Analysis.Path_Connected Higher_Order_Terms: theory Lambda_Free_RPOs.Lambda_Free_Util HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function HOL-Analysis: theory HOL-Analysis.Measure_Space Functional_Ordered_Resolution_Prover: theory Collections.HashCode Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Util Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Standard_Redundancy Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Generator Higher_Order_Terms: theory Lambda_Free_RPOs.Lambda_Free_Term Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.FO_Ordered_Resolution Perron_Frobenius: theory HOL-Analysis.Derivative HOL-Analysis: theory HOL-Analysis.T1_Spaces Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_App HOL-Analysis: theory HOL-Analysis.Tagged_Division Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Instances Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Matching Functional_Ordered_Resolution_Prover: theory Deriving.Derive Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Std Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Unification HOL-Analysis: theory HOL-Analysis.Homotopy Higher_Order_Terms: theory Higher_Order_Terms.Nterm Higher_Order_Terms: theory Higher_Order_Terms.Term HOL-Analysis: theory HOL-Analysis.Locally Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Basic Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unification Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover Higher_Order_Terms: theory Higher_Order_Terms.Unification_Compat Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Encoding_KBO Perron_Frobenius: theory HOL-Analysis.Cartesian_Euclidean_Space Higher_Order_Terms: theory Higher_Order_Terms.Pats HOL-Analysis: theory HOL-Analysis.Caratheodory Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Matching Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.IsaFoR_Term Higher_Order_Terms: theory Higher_Order_Terms.Lambda_Free_Compat Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs Higher_Order_Terms: theory Higher_Order_Terms.Term_to_Nterm Perron_Frobenius: theory Rank_Nullity_Theorem.Mod_Type HOL-Analysis: theory HOL-Analysis.Homeomorphism Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Executable_Subsumption Perron_Frobenius: theory Rank_Nullity_Theorem.Miscellaneous Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBOs HOL-Analysis: theory HOL-Analysis.Derivative Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems HOL-Analysis: theory HOL-Analysis.Cross3 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Polytope HOL-Analysis: theory HOL-Analysis.Arcwise_Connected HOL-Analysis: theory HOL-Analysis.Borel_Space HOL-Analysis: theory HOL-Analysis.Lipschitz HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration HOL-Analysis: theory HOL-Analysis.Regularity LLL_Basis_Reduction: theory LLL_Basis_Reduction.Int_Rat_Operations LLL_Basis_Reduction: theory HOL-Eisbach.Eisbach LLL_Basis_Reduction: theory Perron_Frobenius.Bij_Nat LLL_Basis_Reduction: theory Perron_Frobenius.Cancel_Card_Constraint LLL_Basis_Reduction: theory HOL-Analysis.Abstract_Topology LLL_Basis_Reduction: theory HOL-Analysis.Continuum_Not_Denumerable LLL_Basis_Reduction: theory HOL-Analysis.Inner_Product HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure LLL_Basis_Reduction: theory HOL-Analysis.L2_Norm LLL_Basis_Reduction: theory HOL-Analysis.Operator_Norm LLL_Basis_Reduction: theory HOL-Analysis.Product_Vector LLL_Basis_Reduction: theory HOL-Analysis.Norm_Arith Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/outline.pdf Higher_Order_Terms FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Higher_Order_Terms) ### Introduced fixed type variable(s): 'd, 'e in "f__" ### Introduced fixed type variable(s): 'd in "X__" ### Introduced fixed type variable(s): 'd, 'e, 'f in "R__" or "S__" ### Introduced fixed type variable(s): 'd, 'e in "R__" ### Ignoring duplicate rewrite rule: ### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1) ### Ignoring duplicate rewrite rule: ### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1) ### Introduced fixed type variable(s): 'd in "z__" ### Introduced fixed type variable(s): 'd in "P__" *** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy") ### Metis: Unused theorems: "Term_Class.list_comb_cond_inj_2" ### Metis: Unused theorems: "Term_Class.list_comb_cond_inj_1" ### Rule already declared as introduction (intro) ### \rel_option ?R ?x ?y; ### \a b. ?R a b \ rel_option ?R (?f a) (?g b)\ ### \ rel_option ?R (?x \ ?f) (?y \ ?g) isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/outline -o pdf -n outline -t /proof,/ML *** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy") HOL-Analysis: theory HOL-Analysis.Embed_Measure HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure LLL_Basis_Reduction: theory HOL-Analysis.Elementary_Topology LLL_Basis_Reduction: theory HOL-Analysis.Euclidean_Space HOL-Analysis: theory HOL-Analysis.Bochner_Integration LLL_Basis_Reduction: theory HOL-Analysis.Abstract_Limits LLL_Basis_Reduction: theory HOL-Analysis.Finite_Cartesian_Product LLL_Basis_Reduction: theory HOL-Analysis.Linear_Algebra LLL_Basis_Reduction: theory HOL-Analysis.Abstract_Topology_2 HOL-Analysis: theory HOL-Analysis.Complete_Measure HOL-Analysis: theory HOL-Analysis.Radon_Nikodym LLL_Basis_Reduction: theory HOL-Analysis.Convex HOL-Analysis: theory HOL-Analysis.Set_Integral HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure LLL_Basis_Reduction: theory HOL-Analysis.Connected HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum LLL_Basis_Reduction: theory HOL-Analysis.Cartesian_Space LLL_Basis_Reduction: theory HOL-Analysis.Elementary_Metric_Spaces HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration LLL_Basis_Reduction: theory HOL-Analysis.Determinants LLL_Basis_Reduction: theory HOL-Analysis.Elementary_Normed_Spaces LLL_Basis_Reduction: theory HOL-Analysis.Topology_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration HOL-Analysis: theory HOL-Analysis.Integral_Test LLL_Basis_Reduction: theory HOL-Analysis.Convex_Euclidean_Space LLL_Basis_Reduction: theory HOL-Analysis.Extended_Real_Limits LLL_Basis_Reduction: theory HOL-Analysis.Function_Topology HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics LLL_Basis_Reduction: theory HOL-Analysis.Starlike LLL_Basis_Reduction: theory HOL-Analysis.Summation_Tests HOL-Analysis: theory HOL-Analysis.Improper_Integral HOL-Analysis: theory HOL-Analysis.Interval_Integral HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution LLL_Basis_Reduction: theory HOL-Analysis.Uniform_Limit HOL-Analysis: theory HOL-Analysis.Complex_Transcendental LLL_Basis_Reduction: theory HOL-Analysis.Bounded_Linear_Function LLL_Basis_Reduction: theory HOL-Analysis.Continuous_Extension LLL_Basis_Reduction: theory HOL-Analysis.Path_Connected HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem HOL-Analysis: theory HOL-Analysis.Infinite_Products HOL-Analysis: theory HOL-Analysis.Further_Topology HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers LLL_Basis_Reduction: theory HOL-Analysis.Homotopy HOL-Analysis: theory HOL-Analysis.Jordan_Curve LLL_Basis_Reduction: theory HOL-Analysis.Homeomorphism HOL-Analysis: theory HOL-Analysis.Conformal_Mappings LLL_Basis_Reduction: theory HOL-Analysis.Brouwer_Fixpoint HOL-Analysis: theory HOL-Analysis.FPS_Convergence HOL-Analysis: theory HOL-Analysis.Great_Picard HOL-Analysis: theory HOL-Analysis.Gamma_Function LLL_Basis_Reduction: theory HOL-Analysis.Derivative HOL-Analysis: theory HOL-Analysis.Riemann_Mapping HOL-Analysis: theory HOL-Analysis.Winding_Numbers LLL_Basis_Reduction: theory HOL-Analysis.Cartesian_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Ball_Volume LLL_Basis_Reduction: theory Perron_Frobenius.HMA_Connect HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem HOL-Analysis: theory HOL-Analysis.Change_Of_Vars HOL-Analysis: theory HOL-Analysis.Simplex_Content HOL-Analysis: theory HOL-Analysis.Analysis LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_2 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/outline.pdf Lambda_Free_KBOs FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_KBOs) Proving the simplification rules ... Proofs for inductive predicate(s) "gt_diff" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "gt_same" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... consts subst_zpassign :: "('v \ ('s, 'v) tm) \ ('v pvar \ zhmultiset) \ 'v pvar \ zhmultiset" ### theory "Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs" ### 4.081s elapsed time, 8.380s cpu time, 0.344s GC time Loading theory "Lambda_Free_KBOs.Lambda_Free_KBOs" locale simple_kbo_instances ### theory "Lambda_Free_KBOs.Lambda_Free_KBOs" ### 1.424s elapsed time, 2.980s cpu time, 0.276s GC time Found termination order: "size <*mlex*> {}" "(>\<^sub>h\<^sub>d)" :: "('s, 'v) hd \ ('s, 'v) hd \ bool" isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/outline -o pdf -n outline -t /proof,/ML isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/document -o pdf -n document *** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy") Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/outline.pdf Functional_Ordered_Resolution_Prover FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Functional_Ordered_Resolution_Prover) compare_order: register types in class compare_order, options: (linorder) or () countable: register datatypes is class countable equality: generate an equality function, options are () and (eq) hash_code: generate a hash function, options are () and (hashcode) hashable: register types in class hashable linorder: register types in class linorder, options: (linorder) or () *** Failed to finish proof (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy") ### Ignoring duplicate rewrite rule: ### mset (filter ?P1 ?xs1) \ filter_mset ?P1 (mset ?xs1) Testing conjecture with Quickcheck-narrowing... [1 of 5] Compiling Data_Bits ( /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Data_Bits.hs.hs, /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Data_Bits.hs.o ) [2 of 5] Compiling Typerep ( /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Typerep.hs.hs, /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Typerep.hs.o ) [3 of 5] Compiling Generated_Code ( /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Generated_Code.hs, /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Generated_Code.o ) [4 of 5] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Narrowing_Engine.o ) [5 of 5] Compiling Main ( /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Main.hs, /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Main.o ) Linking /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/isabelle_quickcheck_narrowing ... Quickcheck found no counterexample. isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/outline -o pdf -n outline -t /proof,/ML isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/document -o pdf -n document *** Failed to finish proof (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy") Timing Coinductive (4 threads, 95.740s elapsed time, 334.604s cpu time, 15.216s GC time, factor 3.49) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Coinductive Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Coinductive/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Coinductive/outline.pdf Finished Coinductive (0:02:06 elapsed time, 0:06:40 cpu time, factor 3.18) Building DynamicArchitectures ... Running Stream_Fusion_Code ... Running Topology ... Running Lazy-Lists-II ... Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion DynamicArchitectures: theory DynamicArchitectures.Configuration_Traces Topology: theory Topology.Topology Topology: theory Lazy-Lists-II.LList2 Lazy-Lists-II: theory Lazy-Lists-II.LList2 Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_List DynamicArchitectures: theory DynamicArchitectures.Dynamic_Architecture_Calculus Topology: theory Topology.LList_Topology Timing Lazy-Lists-II (4 threads, 2.003s elapsed time, 5.212s cpu time, 0.236s GC time, factor 2.60) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lazy-Lists-II Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lazy-Lists-II/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lazy-Lists-II/outline.pdf Finished Lazy-Lists-II (0:00:07 elapsed time, 0:00:15 cpu time, factor 2.19) Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_LList Timing Topology (4 threads, 4.952s elapsed time, 17.164s cpu time, 0.700s GC time, factor 3.47) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Topology Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Topology/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Topology/outline.pdf Finished Topology (0:00:10 elapsed time, 0:00:27 cpu time, factor 2.71) Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_Examples LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_Int Timing Stream_Fusion_Code (4 threads, 11.653s elapsed time, 34.180s cpu time, 1.168s GC time, factor 2.93) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stream_Fusion_Code Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stream_Fusion_Code/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stream_Fusion_Code/outline.pdf Finished Stream_Fusion_Code (0:00:17 elapsed time, 0:00:45 cpu time, factor 2.61) Timing DynamicArchitectures (4 threads, 8.878s elapsed time, 30.092s cpu time, 0.624s GC time, factor 3.39) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DynamicArchitectures Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DynamicArchitectures/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DynamicArchitectures/outline.pdf Finished DynamicArchitectures (0:00:31 elapsed time, 0:01:09 cpu time, factor 2.21) Running Architectural_Design_Patterns ... Architectural_Design_Patterns: theory Architectural_Design_Patterns.Auxiliary Architectural_Design_Patterns: theory Architectural_Design_Patterns.Singleton Architectural_Design_Patterns: theory Architectural_Design_Patterns.RF_LTL Architectural_Design_Patterns: theory Architectural_Design_Patterns.Publisher_Subscriber Architectural_Design_Patterns: theory Architectural_Design_Patterns.Blockchain Architectural_Design_Patterns: theory Architectural_Design_Patterns.Blackboard Timing Architectural_Design_Patterns (4 threads, 23.787s elapsed time, 59.348s cpu time, 3.440s GC time, factor 2.50) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Architectural_Design_Patterns Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Architectural_Design_Patterns/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Architectural_Design_Patterns/outline.pdf Finished Architectural_Design_Patterns (0:00:31 elapsed time, 0:01:12 cpu time, factor 2.32) Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint Perron_Frobenius: theory Perron_Frobenius.Bij_Nat Perron_Frobenius: theory Perron_Frobenius.Roots_Unity Perron_Frobenius: theory Perron_Frobenius.Hom_Gauss_Jordan Perron_Frobenius: theory Perron_Frobenius.HMA_Connect Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Irreducible Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_General Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory_2 Perron_Frobenius: theory Perron_Frobenius.Check_Matrix_Growth Timing Perron_Frobenius (4 threads, 209.636s elapsed time, 716.348s cpu time, 27.796s GC time, factor 3.42) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perron_Frobenius Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perron_Frobenius/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perron_Frobenius/outline.pdf Finished Perron_Frobenius (0:03:37 elapsed time, 0:12:09 cpu time, factor 3.36) LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Impl LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Complexity LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Number_Bounds LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Certification LLL_Basis_Reduction: theory LLL_Basis_Reduction.FPLLL_Solver Timing LLL_Basis_Reduction (4 threads, 415.938s elapsed time, 1137.952s cpu time, 104.932s GC time, factor 2.74) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Basis_Reduction Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Basis_Reduction/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Basis_Reduction/outline.pdf Finished LLL_Basis_Reduction (0:07:52 elapsed time, 0:20:38 cpu time, factor 2.62) Running LLL_Factorization ... LLL_Factorization: theory LLL_Factorization.Sub_Sums LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly LLL_Factorization: theory LLL_Factorization.Factor_Bound_2 LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl LLL_Factorization: theory LLL_Factorization.LLL_Factorization LLL_Factorization: theory LLL_Factorization.Factorization_Algorithm_16_22 LLL_Factorization: theory LLL_Factorization.Modern_Computer_Algebra_Problem Timing LLL_Factorization (4 threads, 47.586s elapsed time, 124.564s cpu time, 5.576s GC time, factor 2.62) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Factorization Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Factorization/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Factorization/outline.pdf Finished LLL_Factorization (0:00:54 elapsed time, 0:02:16 cpu time, factor 2.50) Timing HOL-Analysis (4 threads, 509.795s elapsed time, 1728.152s cpu time, 58.160s GC time, factor 3.39) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis/manual.pdf Finished HOL-Analysis (0:09:56 elapsed time, 0:30:58 cpu time, factor 3.11) Building Ordinary_Differential_Equations ... Building HOL-Probability ... Running Smooth_Manifolds ... Building Affine_Arithmetic ... Building Echelon_Form ... Building Dirichlet_Series ... Building Count_Complex_Roots ... Building E_Transcendental ... Running QR_Decomposition ... Running Gromov_Hyperbolicity ... Smooth_Manifolds: theory HOL-Library.Function_Algebras Smooth_Manifolds: theory HOL-Library.Quotient_Syntax Smooth_Manifolds: theory HOL-Types_To_Sets.Prerequisites Smooth_Manifolds: theory HOL-Types_To_Sets.Types_To_Sets Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order Smooth_Manifolds: theory HOL-Library.Quotient_Set HOL-Probability: theory HOL-Library.AList Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int HOL-Probability: theory HOL-Library.Adhoc_Overloading Ordinary_Differential_Equations: theory HOL-Word.Bits HOL-Probability: theory HOL-Library.Conditional_Parametricity HOL-Probability: theory HOL-Library.Lattice_Syntax HOL-Probability: theory HOL-Library.Complete_Partial_Order2 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat Echelon_Form: theory HOL-Computational_Algebra.Fraction_Field Echelon_Form: theory HOL-Library.Bit Echelon_Form: theory HOL-Library.Code_Abstract_Nat Echelon_Form: theory HOL-Library.Code_Target_Int Affine_Arithmetic: theory Deriving.Comparator Affine_Arithmetic: theory Deriving.Derive_Manager Affine_Arithmetic: theory Deriving.Generator_Aux Affine_Arithmetic: theory HOL-Decision_Procs.Dense_Linear_Order Ordinary_Differential_Equations: theory HOL-Word.Misc_Numeric HOL-Probability: theory HOL-Library.Monad_Syntax Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading Echelon_Form: theory HOL-Library.Code_Target_Nat Count_Complex_Roots: theory HOL-Eisbach.Eisbach Count_Complex_Roots: theory HOL-Computational_Algebra.Fraction_Field Count_Complex_Roots: theory HOL-Library.More_List Count_Complex_Roots: theory HOL-Computational_Algebra.Field_as_Ring Ordinary_Differential_Equations: theory HOL-Word.Bit_Representation Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence HOL-Probability: theory HOL-Library.Mapping Gromov_Hyperbolicity: theory HOL-Cardinals.Fun_More Gromov_Hyperbolicity: theory HOL-Cardinals.Order_Relation_More Gromov_Hyperbolicity: theory HOL-Cardinals.Order_Union Gromov_Hyperbolicity: theory HOL-Decision_Procs.Dense_Linear_Order Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral Echelon_Form: theory HOL-Library.Function_Algebras Affine_Arithmetic: theory HOL-Library.Monad_Syntax Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras Smooth_Manifolds: theory HOL-Types_To_Sets.Group_On_With Gromov_Hyperbolicity: theory HOL-Library.Cardinal_Notations Echelon_Form: theory HOL-Library.Code_Target_Numeral Affine_Arithmetic: theory HOL-Library.Bit Affine_Arithmetic: theory Deriving.Equality_Generator Gromov_Hyperbolicity: theory HOL-Library.Code_Abstract_Nat Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Int E_Transcendental: theory HOL-Number_Theory.Cong E_Transcendental: theory HOL-Algebra.Congruence E_Transcendental: theory HOL-Library.More_List E_Transcendental: theory HOL-Library.Power_By_Squaring Ordinary_Differential_Equations: theory HOL-Library.Log_Nat Echelon_Form: theory HOL-Library.IArray Dirichlet_Series: theory HOL-Computational_Algebra.Fraction_Field Dirichlet_Series: theory HOL-Computational_Algebra.Group_Closure Dirichlet_Series: theory HOL-Library.Adhoc_Overloading Dirichlet_Series: theory HOL-Library.BNF_Corec Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Nat Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial Echelon_Form: theory HOL-Library.More_List HOL-Probability: theory HOL-Library.Stream Dirichlet_Series: theory HOL-Library.Monad_Syntax Gromov_Hyperbolicity: theory HOL-Library.Lattice_Algebras Gromov_Hyperbolicity: theory HOL-Cardinals.Wellfounded_More Dirichlet_Series: theory HOL-Computational_Algebra.Nth_Powers Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Relation Echelon_Form: theory Gauss_Jordan.Code_Bit Echelon_Form: theory Gauss_Jordan.Code_Set Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Numeral E_Transcendental: theory HOL-Number_Theory.Eratosthenes E_Transcendental: theory HOL-Computational_Algebra.Polynomial Echelon_Form: theory HOL-Computational_Algebra.Field_as_Ring Echelon_Form: theory HOL-Computational_Algebra.Polynomial Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator Gromov_Hyperbolicity: theory HOL-Library.Log_Nat Ordinary_Differential_Equations: theory HOL-Word.Bits_Int QR_Decomposition: theory Deriving.Derive_Manager QR_Decomposition: theory Deriving.Generator_Aux QR_Decomposition: theory HOL-Library.Bit QR_Decomposition: theory Real_Impl.Real_Impl_Auxiliary Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Embedding Affine_Arithmetic: theory Deriving.Equality_Instances QR_Decomposition: theory HOL-Library.Code_Abstract_Nat Dirichlet_Series: theory HOL-Computational_Algebra.Squarefree Affine_Arithmetic: theory HOL-Library.Boolean_Algebra QR_Decomposition: theory HOL-Library.Code_Target_Int Affine_Arithmetic: theory HOL-Library.Permutation QR_Decomposition: theory HOL-Library.Code_Target_Nat Count_Complex_Roots: theory HOL-Eisbach.Eisbach_Tools Count_Complex_Roots: theory Winding_Number_Eval.Missing_Analysis Affine_Arithmetic: theory Deriving.Compare Gromov_Hyperbolicity: theory Ergodic_Theory.Fekete QR_Decomposition: theory HOL-Library.Function_Algebras Affine_Arithmetic: theory Deriving.Comparator_Generator QR_Decomposition: theory HOL-Library.IArray E_Transcendental: theory HOL-Number_Theory.Fib Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On_With Affine_Arithmetic: theory HOL-Library.Char_ord Count_Complex_Roots: theory Winding_Number_Eval.Missing_Topology QR_Decomposition: theory HOL-Library.Code_Target_Numeral HOL-Probability: theory HOL-Library.Rewrite Dirichlet_Series: theory HOL-Number_Theory.Cong Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Constructions Dirichlet_Series: theory HOL-Library.Code_Abstract_Nat Dirichlet_Series: theory HOL-Library.Code_Target_Nat Echelon_Form: theory HOL-Computational_Algebra.Normalized_Fraction Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat QR_Decomposition: theory Gauss_Jordan.Code_Set Count_Complex_Roots: theory HOL-Computational_Algebra.Normalized_Fraction Echelon_Form: theory Gauss_Jordan.IArray_Addenda Affine_Arithmetic: theory HOL-Library.Code_Target_Nat QR_Decomposition: theory Cauchy.CauchysMeanTheorem Echelon_Form: theory Cayley_Hamilton.Square_Matrix E_Transcendental: theory HOL-Number_Theory.Prime_Powers QR_Decomposition: theory HOL-Library.Code_Real_Approx_By_Float QR_Decomposition: theory Gauss_Jordan.Code_Bit Dirichlet_Series: theory HOL-Library.Code_Target_Int QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary HOL-Probability: theory HOL-Library.AList_Mapping E_Transcendental: theory HOL-Number_Theory.Mod_Exp E_Transcendental: theory HOL-Algebra.Order Dirichlet_Series: theory HOL-Computational_Algebra.Normalized_Fraction Affine_Arithmetic: theory HOL-Library.Code_Target_Int HOL-Probability: theory HOL-Library.Sublist Affine_Arithmetic: theory HOL-Library.Mapping Dirichlet_Series: theory HOL-Library.Code_Target_Numeral QR_Decomposition: theory Rank_Nullity_Theorem.Dual_Order Dirichlet_Series: theory HOL-Algebra.Congruence Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral Echelon_Form: theory Rank_Nullity_Theorem.Dual_Order QR_Decomposition: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell QR_Decomposition: theory Rank_Nullity_Theorem.Mod_Type QR_Decomposition: theory QR_Decomposition.IArray_Addenda_QR HOL-Probability: theory HOL-Library.Tree QR_Decomposition: theory Show.Show QR_Decomposition: theory Sqrt_Babylonian.Log_Impl HOL-Probability: theory HOL-Library.FSet Affine_Arithmetic: theory HOL-Library.Type_Length Echelon_Form: theory Rank_Nullity_Theorem.Mod_Type Affine_Arithmetic: theory Deriving.Compare_Generator E_Transcendental: theory HOL-Number_Theory.Totient QR_Decomposition: theory Sqrt_Babylonian.NthRoot_Impl Affine_Arithmetic: theory HOL-Library.RBT_Impl Dirichlet_Series: theory HOL-Library.Function_Algebras Gromov_Hyperbolicity: theory HOL-Cardinals.Cardinal_Order_Relation Ordinary_Differential_Equations: theory HOL-Word.Bool_List_Representation Dirichlet_Series: theory HOL-Library.More_List Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Vector_Derivative_On Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On Dirichlet_Series: theory HOL-Library.Power_By_Squaring Ordinary_Differential_Equations: theory Triangle.Angles Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Gronwall Affine_Arithmetic: theory Deriving.Compare_Instances HOL-Probability: theory HOL-Library.Diagonal_Subsequence Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Interval_Integral_HK HOL-Probability: theory HOL-Library.Multiset_Permutations Ordinary_Differential_Equations: theory Triangle.Triangle Dirichlet_Series: theory HOL-Library.Stirling Dirichlet_Series: theory HOL-Number_Theory.Mod_Exp Ordinary_Differential_Equations: theory List-Index.List_Index Affine_Arithmetic: theory HOL-Word.Bits HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams Affine_Arithmetic: theory HOL-Word.Misc_Numeric E_Transcendental: theory HOL-Algebra.Lattice Affine_Arithmetic: theory HOL-Word.Bits_Bit Affine_Arithmetic: theory HOL-Word.Bit_Representation Dirichlet_Series: theory HOL-Algebra.Order QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian Dirichlet_Series: theory HOL-Number_Theory.Eratosthenes QR_Decomposition: theory Show.Show_Instances Affine_Arithmetic: theory HOL-Word.Word_Miscellaneous QR_Decomposition: theory Show.Show_Real Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Library_Complements Affine_Arithmetic: theory HOL-Word.Misc_Typedef Dirichlet_Series: theory HOL-Real_Asymp.Inst_Existentials Dirichlet_Series: theory Bernoulli.Bernoulli Affine_Arithmetic: theory Deriving.Countable_Generator Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial Affine_Arithmetic: theory HOL-Word.Bits_Int Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer QR_Decomposition: theory Real_Impl.Prime_Product Affine_Arithmetic: theory HOL-Library.Lattice_Algebras Dirichlet_Series: theory Bernoulli.Bernoulli_FPS QR_Decomposition: theory Real_Impl.Real_Impl HOL-Probability: theory HOL-Probability.Discrete_Topology QR_Decomposition: theory Rank_Nullity_Theorem.Miscellaneous Affine_Arithmetic: theory HOL-Library.Log_Nat HOL-Probability: theory HOL-Probability.Essential_Supremum E_Transcendental: theory HOL-Algebra.Complete_Lattice Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities HOL-Probability: theory HOL-Probability.Probability_Measure Ordinary_Differential_Equations: theory HOL-Library.Float Dirichlet_Series: theory HOL-Algebra.Lattice Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise HOL-Probability: theory HOL-Probability.Stopping_Time Echelon_Form: theory Rank_Nullity_Theorem.Miscellaneous HOL-Probability: theory HOL-Probability.Tree_Space Gromov_Hyperbolicity: theory HOL-Library.Float QR_Decomposition: theory Real_Impl.Real_Unique_Impl Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector Affine_Arithmetic: theory HOL-Word.Bool_List_Representation Dirichlet_Series: theory HOL-Library.Going_To_Filter E_Transcendental: theory HOL-Algebra.Group Dirichlet_Series: theory HOL-Library.Landau_Symbols Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict Dirichlet_Series: theory HOL-Algebra.Complete_Lattice Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Eexp_Eln Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Hausdorff_Distance Affine_Arithmetic: theory Native_Word.More_Bits_Int Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Isometries HOL-Probability: theory HOL-Library.Finite_Map HOL-Probability: theory HOL-Probability.Conditional_Expectation QR_Decomposition: theory Gauss_Jordan.Code_Matrix QR_Decomposition: theory Gauss_Jordan.Rref Affine_Arithmetic: theory HOL-Word.Word Echelon_Form: theory Gauss_Jordan.Code_Matrix Echelon_Form: theory Gauss_Jordan.Rref HOL-Probability: theory HOL-Probability.Distribution_Functions QR_Decomposition: theory Rank_Nullity_Theorem.Fundamental_Subspaces QR_Decomposition: theory Gauss_Jordan.Elementary_Operations QR_Decomposition: theory QR_Decomposition.Generalizations2 QR_Decomposition: theory Rank_Nullity_Theorem.Dim_Formula Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space HOL-Probability: theory HOL-Probability.Weak_Convergence Dirichlet_Series: theory HOL-Algebra.Group Echelon_Form: theory Rank_Nullity_Theorem.Fundamental_Subspaces HOL-Probability: theory HOL-Probability.Giry_Monad QR_Decomposition: theory Gauss_Jordan.Rank Echelon_Form: theory Gauss_Jordan.Elementary_Operations HOL-Probability: theory HOL-Probability.Helly_Selection Echelon_Form: theory Rank_Nullity_Theorem.Dim_Formula Echelon_Form: theory Gauss_Jordan.Rank Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation_Bounds E_Transcendental: theory HOL-Algebra.Coset QR_Decomposition: theory QR_Decomposition.Matrix_To_IArray_QR E_Transcendental: theory HOL-Algebra.FiniteProduct QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan Affine_Arithmetic: theory Native_Word.Bits_Integer Affine_Arithmetic: theory HOL-Library.Float Echelon_Form: theory Gauss_Jordan.Matrix_To_IArray Echelon_Form: theory Gauss_Jordan.Gauss_Jordan E_Transcendental: theory HOL-Algebra.Ring Count_Complex_Roots: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial_Factorial Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Metric_Completion Echelon_Form: theory HOL-Computational_Algebra.Polynomial_Factorial Echelon_Form: theory Cayley_Hamilton.Cayley_Hamilton Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Hyperbolicity E_Transcendental: theory HOL-Algebra.Generated_Groups Dirichlet_Series: theory Bernoulli.Periodic_Bernpoly QR_Decomposition: theory Gauss_Jordan.Linear_Maps Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin Dirichlet_Series: theory HOL-Number_Theory.Fib Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_IArrays Echelon_Form: theory Gauss_Jordan.Linear_Maps Dirichlet_Series: theory HOL-Algebra.Coset Dirichlet_Series: theory HOL-Algebra.FiniteProduct HOL-Probability: theory HOL-Probability.Probability_Mass_Function HOL-Probability: theory HOL-Probability.Projective_Family QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan_PA Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float Dirichlet_Series: theory HOL-Algebra.Ring Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation HOL-Probability: theory HOL-Probability.Infinite_Product_Measure Affine_Arithmetic: theory Affine_Arithmetic.Float_Real Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation QR_Decomposition: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces QR_Decomposition: theory Gauss_Jordan.Determinants2 Affine_Arithmetic: theory Native_Word.Word_Misc QR_Decomposition: theory Gauss_Jordan.Inverse Echelon_Form: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces QR_Decomposition: theory Gauss_Jordan.System_Of_Equations Echelon_Form: theory Gauss_Jordan.Determinants2 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays Dirichlet_Series: theory HOL-Number_Theory.Prime_Powers HOL-Probability: theory HOL-Probability.Independent_Family HOL-Probability: theory HOL-Probability.Stream_Space Dirichlet_Series: theory HOL-Algebra.Generated_Groups Echelon_Form: theory Gauss_Jordan.Inverse Echelon_Form: theory Gauss_Jordan.System_Of_Equations Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Boundary QR_Decomposition: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract Echelon_Form: theory Gauss_Jordan.Inverse_IArrays HOL-Probability: theory HOL-Probability.PMF_Impl Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary E_Transcendental: theory HOL-Algebra.AbelCoset E_Transcendental: theory HOL-Algebra.Module Echelon_Form: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract Smooth_Manifolds: theory Smooth_Manifolds.Analysis_More Dirichlet_Series: theory HOL-Number_Theory.Totient Dirichlet_Series: theory HOL-Real_Asymp.Eventuallize Dirichlet_Series: theory HOL-Real_Asymp.Lazy_Eval Dirichlet_Series: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities HOL-Probability: theory HOL-Probability.Random_Permutations HOL-Probability: theory HOL-Probability.SPMF Affine_Arithmetic: theory Affine_Arithmetic.Polygon Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_FPS QR_Decomposition: theory QR_Decomposition.Miscellaneous_QR Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_Factorial Dirichlet_Series: theory HOL-Real_Asymp.Multiseries_Expansion QR_Decomposition: theory QR_Decomposition.Projections Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor Affine_Arithmetic: theory List-Index.List_Index QR_Decomposition: theory QR_Decomposition.Gram_Schmidt HOL-Probability: theory HOL-Probability.Convolution Dirichlet_Series: theory HOL-Computational_Algebra.Formal_Laurent_Series HOL-Probability: theory HOL-Probability.Information QR_Decomposition: theory QR_Decomposition.QR_Decomposition Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Float Dirichlet_Series: theory HOL-Algebra.AbelCoset Affine_Arithmetic: theory HOL-Decision_Procs.Approximation Smooth_Manifolds: theory Smooth_Manifolds.Smooth Smooth_Manifolds: theory Smooth_Manifolds.Chart Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative QR_Decomposition: theory QR_Decomposition.Gram_Schmidt_IArrays Smooth_Manifolds: theory Smooth_Manifolds.Topological_Manifold QR_Decomposition: theory QR_Decomposition.Least_Squares_Approximation QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Symbolic HOL-Probability: theory HOL-Probability.Distributions QR_Decomposition: theory QR_Decomposition.QR_Decomposition_IArrays Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow E_Transcendental: theory HOL-Algebra.Ideal QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Float Smooth_Manifolds: theory Smooth_Manifolds.Bump_Function Smooth_Manifolds: theory Smooth_Manifolds.Differentiable_Manifold QR_Decomposition: theory QR_Decomposition.QR_Efficient HOL-Probability: theory HOL-Probability.Characteristic_Functions HOL-Probability: theory HOL-Probability.Sinc_Integral Smooth_Manifolds: theory Smooth_Manifolds.Partition_Of_Unity Dirichlet_Series: theory HOL-Algebra.Module Smooth_Manifolds: theory Smooth_Manifolds.Product_Manifold Affine_Arithmetic: theory Native_Word.Uint32 Smooth_Manifolds: theory Smooth_Manifolds.Projective_Space Smooth_Manifolds: theory Smooth_Manifolds.Sphere HOL-Probability: theory HOL-Probability.Fin_Map Smooth_Manifolds: theory Smooth_Manifolds.Tangent_Space HOL-Probability: theory HOL-Probability.Levy E_Transcendental: theory HOL-Algebra.RingHom Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map HOL-Probability: theory HOL-Probability.Central_Limit_Theorem Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form Dirichlet_Series: theory HOL-Algebra.Ideal HOL-Probability: theory HOL-Probability.Projective_Limit Affine_Arithmetic: theory Collections.HashCode Dirichlet_Series: theory Landau_Symbols.Group_Sort Affine_Arithmetic: theory Deriving.Hash_Generator E_Transcendental: theory HOL-Algebra.UnivPoly Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE Affine_Arithmetic: theory Deriving.Hash_Instances Dirichlet_Series: theory Landau_Symbols.Landau_Real_Products Affine_Arithmetic: theory Deriving.Derive HOL-Probability: theory HOL-Probability.Probability Affine_Arithmetic: theory Show.Show Dirichlet_Series: theory HOL-Algebra.RingHom Smooth_Manifolds: theory Smooth_Manifolds.Cotangent_Space QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Symbolic Affine_Arithmetic: theory Show.Show_Instances Affine_Arithmetic: theory Affine_Arithmetic.Intersection Dirichlet_Series: theory HOL-Algebra.UnivPoly Dirichlet_Series: theory Landau_Symbols.Landau_Simprocs Dirichlet_Series: theory Landau_Symbols.Landau_More Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin_Landau Echelon_Form: theory Echelon_Form.Rings2 Count_Complex_Roots: theory Sturm_Tarski.PolyMisc Count_Complex_Roots: theory Sturm_Tarski.Sturm_Tarski Dirichlet_Series: theory Matrix.Utility Dirichlet_Series: theory Polynomial_Factorization.Missing_List Count_Complex_Roots: theory Budan_Fourier.BF_Misc Count_Complex_Roots: theory Budan_Fourier.Sturm_Multiple_Roots Count_Complex_Roots: theory Winding_Number_Eval.Missing_Algebraic Dirichlet_Series: theory Polynomial_Factorization.Missing_Multiset Dirichlet_Series: theory Polynomial_Factorization.Prime_Factorization Count_Complex_Roots: theory Winding_Number_Eval.Missing_Transcendental Count_Complex_Roots: theory Count_Complex_Roots.More_Polynomials Count_Complex_Roots: theory Winding_Number_Eval.Cauchy_Index_Theorem E_Transcendental: theory HOL-Algebra.Multiplicative_Group Count_Complex_Roots: theory Count_Complex_Roots.Extended_Sturm Count_Complex_Roots: theory Winding_Number_Eval.Winding_Number_Eval Dirichlet_Series: theory HOL-Computational_Algebra.Computational_Algebra Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots E_Transcendental: theory HOL-Number_Theory.Residues Affine_Arithmetic: theory HOL-Library.RBT Dirichlet_Series: theory HOL-Algebra.Multiplicative_Group Affine_Arithmetic: theory HOL-Library.RBT_Mapping E_Transcendental: theory HOL-Number_Theory.Euler_Criterion E_Transcendental: theory HOL-Number_Theory.Pocklington E_Transcendental: theory HOL-Number_Theory.Gauss Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots_Examples E_Transcendental: theory HOL-Number_Theory.Residue_Primitive_Roots E_Transcendental: theory HOL-Number_Theory.Quadratic_Reciprocity E_Transcendental: theory HOL-Number_Theory.Number_Theory Dirichlet_Series: theory HOL-Number_Theory.Residues E_Transcendental: theory E_Transcendental.E_Transcendental Dirichlet_Series: theory HOL-Number_Theory.Euler_Criterion Dirichlet_Series: theory HOL-Number_Theory.Pocklington Dirichlet_Series: theory HOL-Number_Theory.Gauss Dirichlet_Series: theory HOL-Number_Theory.Residue_Primitive_Roots Dirichlet_Series: theory HOL-Number_Theory.Quadratic_Reciprocity Dirichlet_Series: theory HOL-Number_Theory.Number_Theory Dirichlet_Series: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Misc Dirichlet_Series: theory Dirichlet_Series.Multiplicative_Function Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Product Dirichlet_Series: theory Dirichlet_Series.Euler_Products Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series Dirichlet_Series: theory HOL-Real_Asymp.Real_Asymp Echelon_Form: theory Echelon_Form.Cayley_Hamilton_Compatible Dirichlet_Series: theory Dirichlet_Series.Moebius_Mu Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton Dirichlet_Series: theory Dirichlet_Series.More_Totient Dirichlet_Series: theory Dirichlet_Series.Liouville_Lambda Echelon_Form: theory Echelon_Form.Echelon_Form Dirichlet_Series: theory Dirichlet_Series.Divisor_Count Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Efficient_Code Dirichlet_Series: theory Dirichlet_Series.Partial_Summation Echelon_Form: theory Echelon_Form.Echelon_Form_Det Echelon_Form: theory Echelon_Form.Echelon_Form_IArrays Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series_Analysis Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_Abstract Echelon_Form: theory Echelon_Form.Echelon_Form_Det_IArrays Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton_IArrays Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse_IArrays Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Morse_Gromov_Theorem Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_IArrays Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Bonk_Schramm_Extension Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Boundary_Extension Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Busemann_Function Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Isometries_Classification Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program Timing E_Transcendental (4 threads, 123.489s elapsed time, 444.936s cpu time, 19.244s GC time, factor 3.60) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/E_Transcendental Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/E_Transcendental/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/E_Transcendental/outline.pdf Finished E_Transcendental (0:02:49 elapsed time, 0:08:44 cpu time, factor 3.09) Running Pi_Transcendental ... Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation Pi_Transcendental: theory HOL-Computational_Algebra.Fraction_Field Pi_Transcendental: theory HOL-Library.BNF_Corec Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree Pi_Transcendental: theory HOL-Library.Fun_Lexorder Pi_Transcendental: theory HOL-Library.Groups_Big_Fun Pi_Transcendental: theory HOL-Real_Asymp.Inst_Existentials Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Pi_Transcendental: theory Polynomials.Poly_Mapping Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_FPS Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial Pi_Transcendental: theory HOL-Computational_Algebra.Formal_Laurent_Series Pi_Transcendental: theory Polynomials.MPoly_Type Pi_Transcendental: theory Polynomials.More_MPoly_Type Pi_Transcendental: theory HOL-Library.Landau_Symbols Pi_Transcendental: theory HOL-Real_Asymp.Eventuallize Pi_Transcendental: theory HOL-Real_Asymp.Lazy_Eval Pi_Transcendental: theory HOL-Real_Asymp.Multiseries_Expansion Timing Gromov_Hyperbolicity (4 threads, 169.040s elapsed time, 567.752s cpu time, 15.772s GC time, factor 3.36) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gromov_Hyperbolicity Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gromov_Hyperbolicity/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gromov_Hyperbolicity/outline.pdf Finished Gromov_Hyperbolicity (0:03:01 elapsed time, 0:09:48 cpu time, factor 3.23) Running Gauss_Jordan ... Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code Gauss_Jordan: theory HOL-Library.Bit Gauss_Jordan: theory HOL-Library.Code_Abstract_Nat Gauss_Jordan: theory HOL-Library.Code_Target_Int Gauss_Jordan: theory HOL-Library.Function_Algebras Gauss_Jordan: theory HOL-Library.Code_Target_Nat Gauss_Jordan: theory HOL-Library.IArray Gauss_Jordan: theory Gauss_Jordan.Code_Set Gauss_Jordan: theory HOL-Library.Code_Real_Approx_By_Float Gauss_Jordan: theory HOL-Library.Code_Target_Numeral Gauss_Jordan: theory Rank_Nullity_Theorem.Dual_Order Gauss_Jordan: theory Gauss_Jordan.Code_Bit Gauss_Jordan: theory Rank_Nullity_Theorem.Mod_Type Gauss_Jordan: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell Gauss_Jordan: theory Gauss_Jordan.IArray_Addenda Affine_Arithmetic: theory Affine_Arithmetic.Print Gauss_Jordan: theory Rank_Nullity_Theorem.Miscellaneous Gauss_Jordan: theory Gauss_Jordan.Code_Matrix Gauss_Jordan: theory Gauss_Jordan.Rref Gauss_Jordan: theory Rank_Nullity_Theorem.Fundamental_Subspaces Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs Gauss_Jordan: theory Rank_Nullity_Theorem.Dim_Formula Gauss_Jordan: theory Gauss_Jordan.Rank Gauss_Jordan: theory Gauss_Jordan.Elementary_Operations Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter Gauss_Jordan: theory Gauss_Jordan.Matrix_To_IArray Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_IArrays Gauss_Jordan: theory Gauss_Jordan.Linear_Maps Timing Count_Complex_Roots (4 threads, 165.012s elapsed time, 461.184s cpu time, 11.000s GC time, factor 2.79) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Count_Complex_Roots Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Count_Complex_Roots/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Count_Complex_Roots/outline.pdf Finished Count_Complex_Roots (0:03:18 elapsed time, 0:08:34 cpu time, factor 2.60) Running Winding_Number_Eval ... Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_PA Gauss_Jordan: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces Winding_Number_Eval: theory HOL-Eisbach.Eisbach Winding_Number_Eval: theory HOL-Computational_Algebra.Fraction_Field Winding_Number_Eval: theory HOL-Library.More_List Winding_Number_Eval: theory HOL-Computational_Algebra.Field_as_Ring Gauss_Jordan: theory Gauss_Jordan.Determinants2 Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays Gauss_Jordan: theory Gauss_Jordan.Inverse Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial Gauss_Jordan: theory Gauss_Jordan.Determinants_IArrays Gauss_Jordan: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces_IArrays Gauss_Jordan: theory Gauss_Jordan.Inverse_IArrays Winding_Number_Eval: theory HOL-Eisbach.Eisbach_Tools Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract Winding_Number_Eval: theory Winding_Number_Eval.Missing_Analysis Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations_IArrays Winding_Number_Eval: theory Winding_Number_Eval.Missing_Topology Winding_Number_Eval: theory HOL-Computational_Algebra.Normalized_Fraction Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_IArrays Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_SML Gauss_Jordan: theory Gauss_Jordan.Code_Rational Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library Pi_Transcendental: theory Symmetric_Polynomials.Vieta Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_Haskell Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials Winding_Number_Eval: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial_Factorial Timing HOL-Probability (4 threads, 160.273s elapsed time, 538.168s cpu time, 21.296s GC time, factor 3.36) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability/outline.pdf Finished HOL-Probability (0:03:37 elapsed time, 0:11:33 cpu time, factor 3.18) Building Probabilistic_While ... Probabilistic_While: theory Flow_Networks.Graph Probabilistic_While: theory HOL-Library.Transitive_Closure_Table Probabilistic_While: theory HOL-Library.While_Combinator Probabilistic_While: theory HOL-Types_To_Sets.Types_To_Sets Probabilistic_While: theory Probabilistic_While.Bernoulli Probabilistic_While: theory HOL-Library.Bourbaki_Witt_Fixpoint Probabilistic_While: theory MFMC_Countable.MFMC_Misc Probabilistic_While: theory Flow_Networks.Network Probabilistic_While: theory Flow_Networks.Residual_Graph Probabilistic_While: theory Flow_Networks.Augmenting_Flow Probabilistic_While: theory Flow_Networks.Augmenting_Path Probabilistic_While: theory Flow_Networks.Ford_Fulkerson Probabilistic_While: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract Probabilistic_While: theory MFMC_Countable.MFMC_Finite Pi_Transcendental: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Probabilistic_While: theory MFMC_Countable.Matrix_For_Marginals Probabilistic_While: theory MFMC_Countable.Rel_PMF_Characterisation Probabilistic_While: theory Probabilistic_While.While_SPMF Probabilistic_While: theory Probabilistic_While.Resampling Probabilistic_While: theory Probabilistic_While.Fast_Dice_Roll Probabilistic_While: theory Probabilistic_While.Geometric Pi_Transcendental: theory HOL-Real_Asymp.Real_Asymp Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental Winding_Number_Eval: theory Sturm_Tarski.PolyMisc Winding_Number_Eval: theory Sturm_Tarski.Sturm_Tarski Timing QR_Decomposition (4 threads, 235.290s elapsed time, 838.768s cpu time, 23.908s GC time, factor 3.56) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/QR_Decomposition Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/QR_Decomposition/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/QR_Decomposition/outline.pdf Finished QR_Decomposition (0:04:02 elapsed time, 0:14:13 cpu time, factor 3.52) Building Markov_Models ... Winding_Number_Eval: theory Budan_Fourier.BF_Misc Winding_Number_Eval: theory Winding_Number_Eval.Missing_Algebraic Markov_Models: theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun Markov_Models: theory HOL-Computational_Algebra.Group_Closure Markov_Models: theory HOL-Library.Case_Converter Markov_Models: theory HOL-Library.Code_Abstract_Nat Markov_Models: theory HOL-Library.Code_Target_Nat Markov_Models: theory HOL-Library.Code_Target_Int Markov_Models: theory HOL-Library.Simps_Case_Conv Markov_Models: theory HOL-Library.IArray Markov_Models: theory HOL-Library.While_Combinator Winding_Number_Eval: theory Winding_Number_Eval.Missing_Transcendental Markov_Models: theory HOL-Library.Code_Target_Numeral Markov_Models: theory Coinductive.Coinductive_Nat Winding_Number_Eval: theory Winding_Number_Eval.Cauchy_Index_Theorem Markov_Models: theory Coinductive.Coinductive_List Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval_Examples Markov_Models: theory Coinductive.Coinductive_Stream Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic Markov_Models: theory Markov_Models.Markov_Models_Auxiliary Markov_Models: theory Markov_Models.Discrete_Time_Markov_Chain Markov_Models: theory Markov_Models.Discrete_Time_Markov_Process Markov_Models: theory Markov_Models.Classifying_Markov_Chain_States Markov_Models: theory Markov_Models.Crowds_Protocol Markov_Models: theory Markov_Models.Gossip_Broadcast Markov_Models: theory Markov_Models.Markov_Decision_Process Markov_Models: theory Markov_Models.PCTL Markov_Models: theory Markov_Models.Trace_Space_Equals_Markov_Processes Markov_Models: theory Markov_Models.Zeroconf_Analysis Markov_Models: theory Markov_Models.MDP_Reachability_Problem Timing Ordinary_Differential_Equations (4 threads, 219.626s elapsed time, 684.328s cpu time, 17.048s GC time, factor 3.12) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ordinary_Differential_Equations Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ordinary_Differential_Equations/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ordinary_Differential_Equations/outline.pdf Finished Ordinary_Differential_Equations (0:04:30 elapsed time, 0:12:51 cpu time, factor 2.85) Building HOL-ODE-Numerics ... Markov_Models: theory Markov_Models.Example_A Markov_Models: theory Markov_Models.Example_B Markov_Models: theory Markov_Models.MDP_RP_Certification Markov_Models: theory Markov_Models.PGCL Markov_Models: theory Markov_Models.Continuous_Time_Markov_Chain HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach HOL-ODE-Numerics: theory Automatic_Refinement.Foldi HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1 HOL-ODE-Numerics: theory Collections.ICF_Tools HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot HOL-ODE-Numerics: theory Collections.Ord_Code_Preproc HOL-ODE-Numerics: theory Deriving.Comparator HOL-ODE-Numerics: theory Collections.Locale_Code HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util HOL-ODE-Numerics: theory Deriving.Derive_Manager HOL-ODE-Numerics: theory Deriving.Generator_Aux HOL-ODE-Numerics: theory Deriving.Equality_Generator HOL-ODE-Numerics: theory HOL-Library.AList HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve HOL-ODE-Numerics: theory Deriving.Compare HOL-ODE-Numerics: theory Deriving.Comparator_Generator HOL-ODE-Numerics: theory Deriving.Equality_Instances Markov_Models: theory Markov_Models.Markov_Models HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax HOL-ODE-Numerics: theory HOL-Library.Bit HOL-ODE-Numerics: theory HOL-Library.Boolean_Algebra HOL-ODE-Numerics: theory HOL-Library.Permutation HOL-ODE-Numerics: theory HOL-ex.Quicksort HOL-ODE-Numerics: theory Deriving.Compare_Generator HOL-ODE-Numerics: theory HOL-Library.Char_ord HOL-ODE-Numerics: theory HOL-Library.Mapping HOL-ODE-Numerics: theory HOL-Library.Option_ord HOL-ODE-Numerics: theory Deriving.Compare_Instances HOL-ODE-Numerics: theory HOL-Library.Parallel HOL-ODE-Numerics: theory Automatic_Refinement.Misc HOL-ODE-Numerics: theory HOL-Library.Type_Length HOL-ODE-Numerics: theory HOL-Library.RBT_Impl HOL-ODE-Numerics: theory HOL-Library.While_Combinator HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets HOL-ODE-Numerics: theory HOL-Word.Bits_Bit HOL-ODE-Numerics: theory HOL-Word.Word_Miscellaneous HOL-ODE-Numerics: theory Native_Word.More_Bits_Int HOL-ODE-Numerics: theory HOL-Word.Misc_Typedef HOL-ODE-Numerics: theory HOL-Word.Word HOL-ODE-Numerics: theory Native_Word.Bits_Integer HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging HOL-ODE-Numerics: theory Automatic_Refinement.Relators HOL-ODE-Numerics: theory Collections.SetIterator HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool HOL-ODE-Numerics: theory Collections.SetIteratorOperations HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL Timing Probabilistic_While (4 threads, 40.700s elapsed time, 109.632s cpu time, 2.564s GC time, factor 2.69) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_While Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_While/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_While/outline.pdf Finished Probabilistic_While (0:01:13 elapsed time, 0:02:43 cpu time, factor 2.23) Building CryptHOL ... HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops Timing Pi_Transcendental (4 threads, 117.342s elapsed time, 376.584s cpu time, 18.776s GC time, factor 3.21) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Pi_Transcendental Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Pi_Transcendental/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Pi_Transcendental/outline.pdf Finished Pi_Transcendental (0:02:03 elapsed time, 0:06:27 cpu time, factor 3.15) Timing Gauss_Jordan (4 threads, 100.887s elapsed time, 362.824s cpu time, 8.472s GC time, factor 3.60) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gauss_Jordan Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gauss_Jordan/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gauss_Jordan/outline.pdf Finished Gauss_Jordan (0:01:51 elapsed time, 0:06:21 cpu time, factor 3.43) Running Differential_Dynamic_Logic ... Running Deep_Learning ... HOL-ODE-Numerics: theory Collections.Assoc_List HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel CryptHOL: theory HOL-Eisbach.Eisbach CryptHOL: theory Applicative_Lifting.Applicative CryptHOL: theory CryptHOL.Partial_Function_Set CryptHOL: theory HOL-Library.Cardinal_Notations CryptHOL: theory HOL-Library.Case_Converter HOL-ODE-Numerics: theory Collections.Diff_Array CryptHOL: theory HOL-Library.Simps_Case_Conv CryptHOL: theory HOL-Algebra.Congruence HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate CryptHOL: theory HOL-Library.Function_Algebras HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo CryptHOL: theory HOL-Library.Type_Length HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Ids Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Lib Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Syntax CryptHOL: theory HOL-Library.Countable_Set_Type CryptHOL: theory HOL-Library.Landau_Symbols Deep_Learning: theory Deep_Learning.DL_Missing_Finite_Set Deep_Learning: theory Deep_Learning.Tensor Deep_Learning: theory HOL-Computational_Algebra.Fraction_Field Deep_Learning: theory HOL-Library.Fun_Lexorder Deep_Learning: theory HOL-Algebra.Congruence Deep_Learning: theory HOL-Library.Groups_Big_Fun CryptHOL: theory Applicative_Lifting.Applicative_Environment Deep_Learning: theory HOL-Library.More_List CryptHOL: theory CryptHOL.Environment_Functor Deep_Learning: theory Deep_Learning.Tensor_Subtensor CryptHOL: theory Applicative_Lifting.Applicative_Set HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL CryptHOL: theory HOL-Algebra.Order Deep_Learning: theory Deep_Learning.Tensor_Plus Deep_Learning: theory Polynomials.Poly_Mapping CryptHOL: theory CryptHOL.Set_Applicative CryptHOL: theory Coinductive.Coinductive_Nat Deep_Learning: theory Deep_Learning.Tensor_Scalar_Mult Deep_Learning: theory Deep_Learning.Tensor_Product Deep_Learning: theory HOL-Computational_Algebra.Normalized_Fraction Deep_Learning: theory Deep_Learning.Tensor_Unit_Vec Deep_Learning: theory Deep_Learning.Tensor_Rank Deep_Learning: theory HOL-Algebra.Order Deep_Learning: theory Polynomial_Interpolation.Missing_Unsorted Deep_Learning: theory HOL-Computational_Algebra.Polynomial HOL-ODE-Numerics: theory Collections.Proper_Iterator CryptHOL: theory Coinductive.Coinductive_List CryptHOL: theory HOL-Algebra.Lattice CryptHOL: theory Applicative_Lifting.Applicative_PMF HOL-ODE-Numerics: theory Collections.It_to_It CryptHOL: theory Monad_Normalisation.Monad_Normalisation Deep_Learning: theory Polynomials.MPoly_Type Deep_Learning: theory HOL-Algebra.Lattice HOL-ODE-Numerics: theory Collections.SetIteratorGA Deep_Learning: theory Deep_Learning.Lebesgue_Functional Deep_Learning: theory Jordan_Normal_Form.DL_Missing_List CryptHOL: theory Monomorphic_Monad.Monomorphic_Monad Deep_Learning: theory Polynomials.More_MPoly_Type Deep_Learning: theory Jordan_Normal_Form.DL_Missing_Sublist HOL-ODE-Numerics: theory Native_Word.Code_Target_Bits_Int CryptHOL: theory HOL-Algebra.Complete_Lattice Deep_Learning: theory Polynomial_Interpolation.Ring_Hom HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement HOL-ODE-Numerics: theory Collections.Intf_Comp HOL-ODE-Numerics: theory Collections.Idx_Iterator Deep_Learning: theory VectorSpace.FunctionLemmas Deep_Learning: theory HOL-Algebra.Complete_Lattice HOL-ODE-Numerics: theory Collections.Code_Target_ICF HOL-ODE-Numerics: theory Native_Word.Word_Misc CryptHOL: theory HOL-Algebra.Group CryptHOL: theory CryptHOL.SPMF_Applicative Deep_Learning: theory HOL-Algebra.Group HOL-ODE-Numerics: theory Deriving.Countable_Generator HOL-ODE-Numerics: theory Native_Word.Uint CryptHOL: theory Landau_Symbols.Group_Sort HOL-ODE-Numerics: theory Native_Word.Uint32 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer CryptHOL: theory HOL-Algebra.Coset CryptHOL: theory Landau_Symbols.Landau_Real_Products Deep_Learning: theory HOL-Algebra.Coset HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float Timing Winding_Number_Eval (4 threads, 97.993s elapsed time, 256.672s cpu time, 7.340s GC time, factor 2.62) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Winding_Number_Eval Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Winding_Number_Eval/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Winding_Number_Eval/outline.pdf Finished Winding_Number_Eval (0:01:48 elapsed time, 0:04:34 cpu time, factor 2.53) Running Probabilistic_Prime_Tests ... Deep_Learning: theory HOL-Algebra.FiniteProduct HOL-ODE-Numerics: theory Collections.HashCode HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise HOL-ODE-Numerics: theory Collections.Intf_Hash Deep_Learning: theory HOL-Algebra.Ring HOL-ODE-Numerics: theory Collections.Impl_Array_Stack HOL-ODE-Numerics: theory Deriving.Hash_Generator HOL-ODE-Numerics: theory Collections.Gen_Hash HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict Probabilistic_Prime_Tests: theory HOL-Algebra.Exponent Probabilistic_Prime_Tests: theory HOL-Computational_Algebra.Squarefree Probabilistic_Prime_Tests: theory HOL-Number_Theory.Cong Probabilistic_Prime_Tests: theory HOL-Library.Permutation Probabilistic_Prime_Tests: theory HOL-Algebra.Congruence Probabilistic_Prime_Tests: theory HOL-Algebra.Cycles HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis Probabilistic_Prime_Tests: theory HOL-Library.Power_By_Squaring HOL-ODE-Numerics: theory Deriving.Hash_Instances HOL-ODE-Numerics: theory Deriving.Derive Probabilistic_Prime_Tests: theory HOL-Number_Theory.Eratosthenes HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form Probabilistic_Prime_Tests: theory HOL-Number_Theory.Fib Probabilistic_Prime_Tests: theory HOL-Number_Theory.Prime_Powers HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary CryptHOL: theory CryptHOL.Cyclic_Group Probabilistic_Prime_Tests: theory HOL-Algebra.Order Probabilistic_Prime_Tests: theory HOL-Number_Theory.Mod_Exp Probabilistic_Prime_Tests: theory HOL-Number_Theory.Totient HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression CryptHOL: theory CryptHOL.Cyclic_Group_SPMF Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Denotational_Semantics Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Pretty_Printer HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method Deep_Learning: theory Polynomials.MPoly_Type_Univariate CryptHOL: theory Coinductive.TLList HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta Probabilistic_Prime_Tests: theory HOL-Algebra.Lattice Deep_Learning: theory HOL-Computational_Algebra.Polynomial_Factorial Deep_Learning: theory Deep_Learning.Lebesgue_Zero_Set CryptHOL: theory Landau_Symbols.Landau_Simprocs Probabilistic_Prime_Tests: theory HOL-Algebra.Complete_Lattice CryptHOL: theory Landau_Symbols.Landau_More CryptHOL: theory CryptHOL.Negligible Probabilistic_Prime_Tests: theory HOL-Algebra.Galois_Connection Deep_Learning: theory HOL-Algebra.Module Probabilistic_Prime_Tests: theory HOL-Algebra.Group HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection Deep_Learning: theory Jordan_Normal_Form.Missing_Ring Deep_Learning: theory VectorSpace.RingModuleFacts Probabilistic_Prime_Tests: theory HOL-Algebra.Bij Probabilistic_Prime_Tests: theory HOL-Algebra.Coset Probabilistic_Prime_Tests: theory HOL-Algebra.FiniteProduct HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE Deep_Learning: theory VectorSpace.MonoidSums Probabilistic_Prime_Tests: theory HOL-Algebra.Ring Deep_Learning: theory Jordan_Normal_Form.Missing_Permutations Deep_Learning: theory Jordan_Normal_Form.Matrix Deep_Learning: theory VectorSpace.LinearCombinations HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter Probabilistic_Prime_Tests: theory HOL-Algebra.Group_Action HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Axioms Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Frechet_Correctness Probabilistic_Prime_Tests: theory HOL-Algebra.Sylow HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain Probabilistic_Prime_Tests: theory HOL-Algebra.Divisibility Probabilistic_Prime_Tests: theory HOL-Algebra.Zassenhaus Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Static_Semantics HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Groups HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion HOL-ODE-Numerics: theory Show.Show HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While Probabilistic_Prime_Tests: theory HOL-Algebra.Solvable_Groups Probabilistic_Prime_Tests: theory HOL-Algebra.Exact_Sequence Probabilistic_Prime_Tests: theory HOL-Algebra.Sym_Groups HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic Probabilistic_Prime_Tests: theory HOL-Algebra.AbelCoset Probabilistic_Prime_Tests: theory HOL-Algebra.Module Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Coincidence Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix Deep_Learning: theory Deep_Learning.DL_Network Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Bound_Effect Deep_Learning: theory Deep_Learning.Tensor_Matricization Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Axioms Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Uniform_Renaming Deep_Learning: theory Jordan_Normal_Form.DL_Submatrix HOL-ODE-Numerics: theory Show.Show_Instances Deep_Learning: theory Jordan_Normal_Form.Gauss_Jordan_Elimination HOL-ODE-Numerics: theory HOL-Library.RBT Markov_Models: theory Markov_Models.MDP_RP Deep_Learning: theory VectorSpace.SumSpaces HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof Deep_Learning: theory VectorSpace.VectorSpace HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb HOL-ODE-Numerics: theory Refine_Monadic.Refine_While Deep_Learning: theory Jordan_Normal_Form.Column_Operations Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal CryptHOL: theory CryptHOL.Misc_CryptHOL HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer Deep_Learning: theory Deep_Learning.DL_Shallow_Model HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal_Product Probabilistic_Prime_Tests: theory HOL-Algebra.RingHom HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic Probabilistic_Prime_Tests: theory HOL-Algebra.QuotRing Probabilistic_Prime_Tests: theory HOL-Algebra.UnivPoly HOL-ODE-Numerics: theory Collections.Gen_Iterator Deep_Learning: theory Jordan_Normal_Form.Missing_VectorSpace Deep_Learning: theory Jordan_Normal_Form.VS_Connect HOL-ODE-Numerics: theory Collections.Iterator HOL-ODE-Numerics: theory Collections.Intf_Map Timing Dirichlet_Series (4 threads, 266.857s elapsed time, 896.416s cpu time, 54.640s GC time, factor 3.36) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_Series Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_Series/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_Series/outline.pdf Finished Dirichlet_Series (0:05:44 elapsed time, 0:17:12 cpu time, factor 3.00) Building Zeta_Function ... HOL-ODE-Numerics: theory Collections.Intf_Set Deep_Learning: theory Jordan_Normal_Form.Determinant HOL-ODE-Numerics: theory Collections.Array_Iterator HOL-ODE-Numerics: theory Collections.RBT_add HOL-ODE-Numerics: theory Collections.Gen_Map HOL-ODE-Numerics: theory Collections.Gen_Map2Set Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst_Lemma CryptHOL: theory CryptHOL.Generat CryptHOL: theory CryptHOL.List_Bits CryptHOL: theory CryptHOL.Resumption HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program HOL-ODE-Numerics: theory Collections.Impl_Array_Map HOL-ODE-Numerics: theory Collections.Impl_List_Map Zeta_Function: theory Bernoulli.Bernoulli_Zeta Probabilistic_Prime_Tests: theory HOL-Algebra.IntRing Probabilistic_Prime_Tests: theory HOL-Algebra.Weak_Morphisms HOL-ODE-Numerics: theory Collections.Impl_RBT_Map HOL-ODE-Numerics: theory Collections.Gen_Set HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map Deep_Learning: theory Deep_Learning.DL_Deep_Model Probabilistic_Prime_Tests: theory HOL-Algebra.Chinese_Remainder Deep_Learning: theory Jordan_Normal_Form.DL_Rank HOL-ODE-Numerics: theory Collections.Impl_Bit_Set CryptHOL: theory CryptHOL.Generative_Probabilistic_Value Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Proof_Checker HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set HOL-ODE-Numerics: theory Collections.Impl_List_Set HOL-ODE-Numerics: theory Collections.Impl_Uv_Set Zeta_Function: theory HOL-Eisbach.Eisbach Zeta_Function: theory HOL-Computational_Algebra.Field_as_Ring Zeta_Function: theory Sturm_Tarski.PolyMisc Zeta_Function: theory Winding_Number_Eval.Missing_Analysis Zeta_Function: theory Winding_Number_Eval.Missing_Topology Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly Zeta_Function: theory HOL-Eisbach.Eisbach_Tools Zeta_Function: theory Sturm_Tarski.Sturm_Tarski Zeta_Function: theory Budan_Fourier.BF_Misc Probabilistic_Prime_Tests: theory HOL-Algebra.Multiplicative_Group Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental Deep_Learning: theory Jordan_Normal_Form.DL_Rank_Submatrix Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity Probabilistic_Prime_Tests: theory HOL-Algebra.Ring_Divisibility Probabilistic_Prime_Tests: theory HOL-Algebra.Subrings Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residues Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval Probabilistic_Prime_Tests: theory HOL-Algebra.Embedded_Algebras Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Rings Probabilistic_Prime_Tests: theory HOL-Number_Theory.Euler_Criterion Probabilistic_Prime_Tests: theory HOL-Number_Theory.Gauss Zeta_Function: theory Zeta_Function.Zeta_Function Probabilistic_Prime_Tests: theory HOL-Number_Theory.Quadratic_Reciprocity Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Fields Probabilistic_Prime_Tests: theory HOL-Number_Theory.Pocklington Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residue_Primitive_Roots Probabilistic_Prime_Tests: theory HOL-Number_Theory.Number_Theory CryptHOL: theory CryptHOL.Computational_Model CryptHOL: theory CryptHOL.GPV_Applicative CryptHOL: theory CryptHOL.GPV_Expectation HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Legendre_Symbol HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation CryptHOL: theory CryptHOL.GPV_Bisim CryptHOL: theory CryptHOL.CryptHOL Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomials HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code HOL-ODE-Numerics: theory Affine_Arithmetic.Print Probabilistic_Prime_Tests: theory HOL-Algebra.Algebra HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries Timing Markov_Models (4 threads, 93.518s elapsed time, 324.156s cpu time, 12.044s GC time, factor 3.47) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Markov_Models Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Markov_Models/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Markov_Models/outline.pdf Finished Markov_Models (0:02:39 elapsed time, 0:07:24 cpu time, factor 2.79) Running Stochastic_Matrices ... Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Generalized_Primality_Test Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Residues_Nat Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Jacobi_Symbol Stochastic_Matrices: theory HOL-Eisbach.Eisbach Stochastic_Matrices: theory HOL-Library.Bit Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field Stochastic_Matrices: theory HOL-Algebra.Congruence Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Carmichael_Numbers Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.QuadRes Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Euler_Witness Stochastic_Matrices: theory HOL-Library.Function_Algebras Stochastic_Matrices: theory HOL-Library.More_List Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Witness Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Solovay_Strassen_Test Stochastic_Matrices: theory HOL-Algebra.Order Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Test Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Miller_Rabin_Test Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial Stochastic_Matrices: theory HOL-Algebra.Lattice Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type Stochastic_Matrices: theory HOL-Algebra.Group Stochastic_Matrices: theory VectorSpace.FunctionLemmas Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous Stochastic_Matrices: theory HOL-Algebra.Coset Stochastic_Matrices: theory HOL-Algebra.FiniteProduct Stochastic_Matrices: theory HOL-Algebra.Ring Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations Stochastic_Matrices: theory HOL-Algebra.Module Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring Stochastic_Matrices: theory VectorSpace.RingModuleFacts Stochastic_Matrices: theory VectorSpace.MonoidSums Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Permutations Stochastic_Matrices: theory Jordan_Normal_Form.Matrix Stochastic_Matrices: theory VectorSpace.LinearCombinations Timing Echelon_Form (4 threads, 396.386s elapsed time, 1261.264s cpu time, 143.676s GC time, factor 3.18) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Echelon_Form Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Echelon_Form/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Echelon_Form/outline.pdf Finished Echelon_Form (0:07:13 elapsed time, 0:22:04 cpu time, factor 3.06) Running Probabilistic_Timed_Automata ... Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.MDP_Aux Probabilistic_Timed_Automata: theory Timed_Automata.Misc Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Basic Stochastic_Matrices: theory VectorSpace.SumSpaces Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Instantiate_Existentials Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.More_List Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence Probabilistic_Timed_Automata: theory Timed_Automata.Floyd_Warshall Stochastic_Matrices: theory VectorSpace.VectorSpace Probabilistic_Timed_Automata: theory Timed_Automata.Timed_Automata Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach_Tools Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Finiteness HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence_LTL Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Stream_More Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Graphs HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions Probabilistic_Timed_Automata: theory Timed_Automata.DBM Probabilistic_Timed_Automata: theory Timed_Automata.Paths_Cycles Probabilistic_Timed_Automata: theory Timed_Automata.Regions Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Basics Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial Stochastic_Matrices: theory Jordan_Normal_Form.Determinant HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Normalization Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Operations Probabilistic_Timed_Automata: theory Timed_Automata.Closure Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics Probabilistic_Timed_Automata: theory Timed_Automata.Regions_Beta Timing Zeta_Function (4 threads, 68.905s elapsed time, 220.008s cpu time, 4.332s GC time, factor 3.19) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Zeta_Function Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Zeta_Function/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Zeta_Function/outline.pdf Finished Zeta_Function (0:01:43 elapsed time, 0:04:36 cpu time, factor 2.67) Running List_Update ... Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly List_Update: theory HOL-Library.While_Combinator List_Update: theory List_Update.Prob_Theory List_Update: theory List_Update.Bit_Strings List_Update: theory List_Update.On_Off List_Update: theory List-Index.List_Index Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form List_Update: theory Regular-Sets.Regular_Set List_Update: theory List_Update.Inversion List_Update: theory List_Update.Swaps List_Update: theory List_Update.Competitive_Analysis Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness Probabilistic_Timed_Automata: theory Timed_Automata.Approx_Beta List_Update: theory List_Update.Move_to_Front List_Update: theory Regular-Sets.Regular_Exp HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom List_Update: theory Regular-Sets.NDerivative List_Update: theory List_Update.MTF2_Effects List_Update: theory List_Update.Partial_Cost_Model List_Update: theory List_Update.BIT List_Update: theory List_Update.List_Factoring HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect List_Update: theory Regular-Sets.Equivalence_Checking List_Update: theory List_Update.RExp_Var List_Update: theory List_Update.OPT2 List_Update: theory List_Update.BIT_pairwise List_Update: theory List_Update.Phase_Partitioning Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux List_Update: theory List_Update.BIT_2comp_on2 List_Update: theory List_Update.TS Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector List_Update: theory List_Update.Comb Timing Affine_Arithmetic (4 threads, 396.557s elapsed time, 1377.260s cpu time, 91.996s GC time, factor 3.47) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic/outline.pdf Finished Affine_Arithmetic (0:07:58 elapsed time, 0:26:27 cpu time, factor 3.32) Running Taylor_Models ... Taylor_Models: theory HOL-Decision_Procs.Rat_Pair Taylor_Models: theory HOL-Decision_Procs.Polynomial_List HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane Timing CryptHOL (4 threads, 122.828s elapsed time, 441.972s cpu time, 23.296s GC time, factor 3.60) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CryptHOL Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CryptHOL/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CryptHOL/outline.pdf Finished CryptHOL (0:03:08 elapsed time, 0:09:34 cpu time, factor 3.05) Running Constructive_Cryptography ... Constructive_Cryptography: theory Constructive_Cryptography.More_CryptHOL HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval Constructive_Cryptography: theory Constructive_Cryptography.Resource Constructive_Cryptography: theory Constructive_Cryptography.Converter Taylor_Models: theory Taylor_Models.Polynomial_Expression Timing Probabilistic_Prime_Tests (4 threads, 187.742s elapsed time, 688.448s cpu time, 48.584s GC time, factor 3.67) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Prime_Tests Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Prime_Tests/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Prime_Tests/outline.pdf Finished Probabilistic_Prime_Tests (0:03:14 elapsed time, 0:11:41 cpu time, factor 3.60) Running Hermite ... Hermite: theory Hermite.Hermite Hermite: theory Hermite.Hermite_IArrays Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite Constructive_Cryptography: theory Constructive_Cryptography.Random_System Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher Constructive_Cryptography: theory Constructive_Cryptography.Wiring Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography Constructive_Cryptography: theory Constructive_Cryptography.System_Construction Timing Deep_Learning (4 threads, 216.332s elapsed time, 740.084s cpu time, 31.556s GC time, factor 3.42) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Deep_Learning Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Deep_Learning/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Deep_Learning/outline.pdf Finished Deep_Learning (0:03:44 elapsed time, 0:12:33 cpu time, factor 3.36) Running Density_Compiler ... Density_Compiler: theory Density_Compiler.Density_Predicates Density_Compiler: theory Density_Compiler.PDF_Transformations Density_Compiler: theory Density_Compiler.PDF_Values Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad Density_Compiler: theory Density_Compiler.PDF_Semantics Taylor_Models: theory HOL-Library.Function_Algebras Taylor_Models: theory Taylor_Models.Float_Topology Taylor_Models: theory Taylor_Models.Interval Taylor_Models: theory Taylor_Models.Taylor_Models_Misc Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel Constructive_Cryptography: theory Constructive_Cryptography.Examples Taylor_Models: theory Taylor_Models.Horner_Eval Taylor_Models: theory Taylor_Models.Interval_Approximation Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional Density_Compiler: theory Density_Compiler.PDF_Density_Contexts Density_Compiler: theory Density_Compiler.PDF_Target_Semantics Density_Compiler: theory Density_Compiler.PDF_Compiler_Pred Taylor_Models: theory Taylor_Models.Taylor_Models Density_Compiler: theory Density_Compiler.PDF_Target_Density_Contexts Density_Compiler: theory Density_Compiler.PDF_Compiler Timing List_Update (4 threads, 105.239s elapsed time, 323.640s cpu time, 12.820s GC time, factor 3.08) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/List_Update Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/List_Update/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/List_Update/outline.pdf Finished List_Update (0:01:59 elapsed time, 0:05:56 cpu time, factor 2.98) Running Linear_Recurrences ... Linear_Recurrences: theory HOL-Library.BNF_Corec Linear_Recurrences: theory HOL-Computational_Algebra.Group_Closure Linear_Recurrences: theory HOL-Computational_Algebra.Nth_Powers Linear_Recurrences: theory HOL-Computational_Algebra.Squarefree Linear_Recurrences: theory HOL-Library.Code_Abstract_Nat Linear_Recurrences: theory HOL-Library.Code_Target_Int Linear_Recurrences: theory HOL-Library.Code_Target_Nat Linear_Recurrences: theory HOL-Library.Code_Target_Numeral Linear_Recurrences: theory HOL-Library.Stirling Linear_Recurrences: theory HOL-Library.Sublist Linear_Recurrences: theory HOL-Real_Asymp.Inst_Existentials Linear_Recurrences: theory Polynomial_Interpolation.Missing_Unsorted Linear_Recurrences: theory HOL-Computational_Algebra.Polynomial_FPS Linear_Recurrences: theory HOL-Computational_Algebra.Formal_Laurent_Series Linear_Recurrences: theory HOL-Library.Landau_Symbols HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics Linear_Recurrences: theory Polynomial_Interpolation.Missing_Polynomial Linear_Recurrences: theory Polynomial_Factorization.Order_Polynomial Linear_Recurrences: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Linear_Recurrences: theory Polynomial_Factorization.Polynomial_Divisibility Linear_Recurrences: theory HOL-Real_Asymp.Eventuallize Linear_Recurrences: theory HOL-Real_Asymp.Lazy_Eval Linear_Recurrences: theory Linear_Recurrences.Pochhammer_Polynomials Linear_Recurrences: theory Matrix.Utility Linear_Recurrences: theory HOL-Computational_Algebra.Computational_Algebra Linear_Recurrences: theory Polynomial_Interpolation.Ring_Hom Linear_Recurrences: theory Linear_Recurrences.Eulerian_Polynomials Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Common Linear_Recurrences: theory HOL-Real_Asymp.Multiseries_Expansion Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Misc Linear_Recurrences: theory Linear_Recurrences.RatFPS Linear_Recurrences: theory Linear_Recurrences.Factorizations Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition Taylor_Models: theory Taylor_Models.Experiments Linear_Recurrences: theory Polynomial_Interpolation.Ring_Hom_Poly Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver Linear_Recurrences: theory Polynomial_Factorization.Square_Free_Factorization Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences Timing Differential_Dynamic_Logic (4 threads, 291.706s elapsed time, 642.212s cpu time, 21.820s GC time, factor 2.20) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Dynamic_Logic Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Dynamic_Logic/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Dynamic_Logic/outline.pdf Finished Differential_Dynamic_Logic (0:05:03 elapsed time, 0:11:01 cpu time, factor 2.18) Building Girth_Chromatic ... Girth_Chromatic: theory HOL-Decision_Procs.Dense_Linear_Order Girth_Chromatic: theory HOL-Library.Code_Abstract_Nat Girth_Chromatic: theory HOL-Library.Code_Target_Int Girth_Chromatic: theory HOL-Library.Lattice_Algebras Girth_Chromatic: theory HOL-Library.Code_Target_Nat Girth_Chromatic: theory HOL-Library.Log_Nat Girth_Chromatic: theory HOL-Library.Code_Target_Numeral Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic_Misc Girth_Chromatic: theory Girth_Chromatic.Ugraphs Girth_Chromatic: theory HOL-Library.Float Girth_Chromatic: theory HOL-Decision_Procs.Approximation_Bounds Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA Timing Taylor_Models (4 threads, 123.531s elapsed time, 355.784s cpu time, 12.436s GC time, factor 2.88) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models/outline.pdf Finished Taylor_Models (0:02:10 elapsed time, 0:06:08 cpu time, factor 2.83) Running Probabilistic_Noninterference ... Probabilistic_Noninterference: theory HOL-Library.Case_Converter Probabilistic_Noninterference: theory HOL-Library.Prefix_Order Probabilistic_Noninterference: theory Coinductive.Coinductive_Nat Probabilistic_Noninterference: theory HOL-Library.Simps_Case_Conv Girth_Chromatic: theory HOL-Decision_Procs.Approximation Probabilistic_Noninterference: theory Coinductive.Coinductive_List HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics Linear_Recurrences: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Linear_Recurrences: theory HOL-Real_Asymp.Real_Asymp Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Asymptotics Probabilistic_Noninterference: theory Coinductive.Coinductive_Stream Timing Hermite (4 threads, 114.838s elapsed time, 265.576s cpu time, 23.308s GC time, factor 2.31) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hermite Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hermite/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hermite/outline.pdf Finished Hermite (0:02:01 elapsed time, 0:04:37 cpu time, factor 2.29) Running Hidden_Markov_Models ... Probabilistic_Noninterference: theory Markov_Models.Markov_Models_Auxiliary Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary Hidden_Markov_Models: theory HOL-Library.State_Monad Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc Probabilistic_Noninterference: theory Markov_Models.Discrete_Time_Markov_Chain Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad Hidden_Markov_Models: theory Monad_Memo_DP.Memory Probabilistic_Noninterference: theory Probabilistic_Noninterference.Interface Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability Hidden_Markov_Models: theory HOL-Imperative_HOL.Array Timing Density_Compiler (4 threads, 104.448s elapsed time, 287.576s cpu time, 5.540s GC time, factor 2.75) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Density_Compiler Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Density_Compiler/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Density_Compiler/outline.pdf Finished Density_Compiler (0:01:53 elapsed time, 0:05:03 cpu time, factor 2.68) Running Dirichlet_L ... Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order Dirichlet_L: theory HOL-Library.Lattice_Algebras Dirichlet_L: theory HOL-Library.Log_Nat Dirichlet_L: theory Lehmer.Lehmer Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd Hidden_Markov_Models: theory Monad_Memo_DP.State_Main Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics Dirichlet_L: theory HOL-Library.Float Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based Dirichlet_L: theory Bertrands_Postulate.Bertrand Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete Timing Linear_Recurrences (4 threads, 81.692s elapsed time, 313.620s cpu time, 18.504s GC time, factor 3.84) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences/outline.pdf Finished Linear_Recurrences (0:01:28 elapsed time, 0:05:25 cpu time, factor 3.70) Running Ergodic_Theory ... Ergodic_Theory: theory Ergodic_Theory.Fekete Ergodic_Theory: theory Ergodic_Theory.SG_Library_Complement Ergodic_Theory: theory Ergodic_Theory.Kohlberg_Neyman_Karlsson Ergodic_Theory: theory Ergodic_Theory.Asymptotic_Density Ergodic_Theory: theory Ergodic_Theory.Measure_Preserving_Transformations Timing Probabilistic_Timed_Automata (4 threads, 220.048s elapsed time, 638.392s cpu time, 18.040s GC time, factor 2.90) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Timed_Automata Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Timed_Automata/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Timed_Automata/outline.pdf Finished Probabilistic_Timed_Automata (0:03:47 elapsed time, 0:10:52 cpu time, factor 2.87) Building Applicative_Lifting ... Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation Applicative_Lifting: theory Applicative_Lifting.Applicative Applicative_Lifting: theory Applicative_Lifting.Joinable Applicative_Lifting: theory HOL-Library.State_Monad Applicative_Lifting: theory HOL-Library.Dlist Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic Applicative_Lifting: theory HOL-Library.Function_Algebras Applicative_Lifting: theory HOL-Library.Function_Division Applicative_Lifting: theory HOL-Nonstandard_Analysis.Free_Ultrafilter Applicative_Lifting: theory HOL-Nonstandard_Analysis.StarDef Ergodic_Theory: theory Ergodic_Theory.Recurrence Applicative_Lifting: theory HOL-Proofs-Lambda.Commutation Applicative_Lifting: theory HOL-Proofs-Lambda.Lambda Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment Applicative_Lifting: theory Applicative_Lifting.Applicative_List Applicative_Lifting: theory Applicative_Lifting.Applicative_Monoid Applicative_Lifting: theory Applicative_Lifting.Applicative_Open_State Applicative_Lifting: theory Applicative_Lifting.Applicative_Option Applicative_Lifting: theory Applicative_Lifting.Applicative_Set Ergodic_Theory: theory Ergodic_Theory.Invariants Applicative_Lifting: theory Applicative_Lifting.Applicative_Sum Applicative_Lifting: theory Applicative_Lifting.Applicative_State Applicative_Lifting: theory Applicative_Lifting.Applicative_DNEList Ergodic_Theory: theory Ergodic_Theory.Transfer_Operator Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment_Algebra Applicative_Lifting: theory Applicative_Lifting.Applicative_Star Applicative_Lifting: theory Applicative_Lifting.Applicative_Stream Ergodic_Theory: theory Ergodic_Theory.Ergodicity Ergodic_Theory: theory Ergodic_Theory.Normalizing_Sequences Applicative_Lifting: theory HOL-Proofs-Lambda.ParRed Applicative_Lifting: theory Applicative_Lifting.Applicative_Filter Applicative_Lifting: theory Applicative_Lifting.Applicative_Probability_List Applicative_Lifting: theory Applicative_Lifting.Stream_Algebra Applicative_Lifting: theory HOL-Proofs-Lambda.Eta Applicative_Lifting: theory Applicative_Lifting.Applicative_Vector Applicative_Lifting: theory Applicative_Lifting.Beta_Eta Applicative_Lifting: theory Applicative_Lifting.Applicative_PMF Applicative_Lifting: theory Applicative_Lifting.Combinators Applicative_Lifting: theory Applicative_Lifting.Idiomatic_Terms Ergodic_Theory: theory Ergodic_Theory.Kingman Applicative_Lifting: theory Applicative_Lifting.Applicative_Functor Applicative_Lifting: theory Applicative_Lifting.Tree_Relabelling Ergodic_Theory: theory Ergodic_Theory.Gouezel_Karlsson Applicative_Lifting: theory Applicative_Lifting.Applicative_Examples Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models Applicative_Lifting: theory Applicative_Lifting.Abstract_AF Applicative_Lifting: theory Applicative_Lifting.Applicative_Test Dirichlet_L: theory Dirichlet_L.Group_Adjoin Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions Timing Stochastic_Matrices (4 threads, 286.167s elapsed time, 780.220s cpu time, 31.132s GC time, factor 2.73) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stochastic_Matrices Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stochastic_Matrices/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stochastic_Matrices/outline.pdf Finished Stochastic_Matrices (0:04:51 elapsed time, 0:13:10 cpu time, factor 2.71) Timing Probabilistic_Noninterference (4 threads, 77.798s elapsed time, 254.244s cpu time, 7.160s GC time, factor 3.27) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference/outline.pdf Finished Probabilistic_Noninterference (0:01:24 elapsed time, 0:04:34 cpu time, factor 3.23) Running MFMC_Countable ... Running Green ... Green: theory Green.General_Utils Green: theory Green.Derivs Green: theory Green.Integrals MFMC_Countable: theory Flow_Networks.Graph MFMC_Countable: theory HOL-Library.Transitive_Closure_Table MFMC_Countable: theory HOL-Library.While_Combinator Green: theory Green.Paths Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example MFMC_Countable: theory HOL-Library.Bourbaki_Witt_Fixpoint MFMC_Countable: theory MFMC_Countable.MFMC_Misc MFMC_Countable: theory Flow_Networks.Network MFMC_Countable: theory MFMC_Countable.Max_Flow_Min_Cut_Countable Green: theory Green.Green MFMC_Countable: theory Flow_Networks.Residual_Graph Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem Green: theory Green.SymmetricR2Shapes Green: theory Green.CircExample Green: theory Green.DiamExample MFMC_Countable: theory Flow_Networks.Augmenting_Flow Timing Girth_Chromatic (4 threads, 71.074s elapsed time, 149.552s cpu time, 5.896s GC time, factor 2.10) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic/outline.pdf Finished Girth_Chromatic (0:01:44 elapsed time, 0:03:27 cpu time, factor 1.98) Running DiscretePricing ... MFMC_Countable: theory Flow_Networks.Augmenting_Path MFMC_Countable: theory Flow_Networks.Ford_Fulkerson MFMC_Countable: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract DiscretePricing: theory DiscretePricing.Filtration DiscretePricing: theory DiscretePricing.Generated_Subalgebra DiscretePricing: theory DiscretePricing.Disc_Cond_Expect MFMC_Countable: theory MFMC_Countable.MFMC_Finite MFMC_Countable: theory MFMC_Countable.Matrix_For_Marginals MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation DiscretePricing: theory DiscretePricing.Martingale DiscretePricing: theory DiscretePricing.Infinite_Coin_Toss_Space Timing Dirichlet_L (4 threads, 73.867s elapsed time, 233.440s cpu time, 7.408s GC time, factor 3.16) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_L Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_L/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_L/outline.pdf Finished Dirichlet_L (0:01:21 elapsed time, 0:04:06 cpu time, factor 3.04) Running Prime_Harmonic_Series ... DiscretePricing: theory DiscretePricing.Geometric_Random_Walk Prime_Harmonic_Series: theory HOL-Number_Theory.Cong Prime_Harmonic_Series: theory HOL-Algebra.Congruence Prime_Harmonic_Series: theory HOL-Library.Power_By_Squaring Prime_Harmonic_Series: theory HOL-Number_Theory.Eratosthenes Prime_Harmonic_Series: theory HOL-Number_Theory.Fib DiscretePricing: theory DiscretePricing.Fair_Price Prime_Harmonic_Series: theory HOL-Number_Theory.Prime_Powers Timing Hidden_Markov_Models (4 threads, 85.880s elapsed time, 149.320s cpu time, 10.180s GC time, factor 1.74) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hidden_Markov_Models Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hidden_Markov_Models/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hidden_Markov_Models/outline.pdf Finished Hidden_Markov_Models (0:01:32 elapsed time, 0:02:42 cpu time, factor 1.75) Running Akra_Bazzi ... Prime_Harmonic_Series: theory HOL-Algebra.Order Prime_Harmonic_Series: theory HOL-Number_Theory.Mod_Exp Prime_Harmonic_Series: theory HOL-Number_Theory.Totient Akra_Bazzi: theory HOL-Decision_Procs.Dense_Linear_Order Akra_Bazzi: theory HOL-Library.Code_Abstract_Nat Akra_Bazzi: theory HOL-Library.Code_Target_Int Akra_Bazzi: theory HOL-Library.Function_Algebras Akra_Bazzi: theory HOL-Library.Code_Target_Nat Akra_Bazzi: theory Akra_Bazzi.Eval_Numeral Akra_Bazzi: theory HOL-Library.Landau_Symbols Akra_Bazzi: theory HOL-Library.Code_Target_Numeral Akra_Bazzi: theory HOL-Library.Lattice_Algebras Akra_Bazzi: theory HOL-Library.Log_Nat Prime_Harmonic_Series: theory HOL-Algebra.Lattice Akra_Bazzi: theory Landau_Symbols.Group_Sort Prime_Harmonic_Series: theory HOL-Algebra.Complete_Lattice Prime_Harmonic_Series: theory HOL-Algebra.Group DiscretePricing: theory DiscretePricing.CRR_Model Akra_Bazzi: theory Landau_Symbols.Landau_Real_Products Prime_Harmonic_Series: theory HOL-Algebra.Coset Prime_Harmonic_Series: theory HOL-Algebra.FiniteProduct Akra_Bazzi: theory HOL-Library.Float HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1 Timing Applicative_Lifting (4 threads, 24.303s elapsed time, 76.648s cpu time, 4.860s GC time, factor 3.15) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Applicative_Lifting Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Applicative_Lifting/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Applicative_Lifting/outline.pdf Finished Applicative_Lifting (0:01:03 elapsed time, 0:02:21 cpu time, factor 2.25) Running Irrationality_J_Hancl ... Prime_Harmonic_Series: theory HOL-Algebra.Ring HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis Irrationality_J_Hancl: theory HOL-Library.Code_Abstract_Nat Irrationality_J_Hancl: theory HOL-Library.Code_Target_Int Irrationality_J_Hancl: theory HOL-Decision_Procs.Dense_Linear_Order Irrationality_J_Hancl: theory HOL-Library.Lattice_Algebras Irrationality_J_Hancl: theory HOL-Library.Code_Target_Nat Prime_Harmonic_Series: theory HOL-Algebra.Generated_Groups Irrationality_J_Hancl: theory HOL-Library.Log_Nat Irrationality_J_Hancl: theory HOL-Library.Code_Target_Numeral HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis Akra_Bazzi: theory Landau_Symbols.Landau_Simprocs Akra_Bazzi: theory Landau_Symbols.Landau_More Akra_Bazzi: theory HOL-Decision_Procs.Approximation_Bounds Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Library Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Asymptotics Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Real Prime_Harmonic_Series: theory HOL-Algebra.AbelCoset Prime_Harmonic_Series: theory HOL-Algebra.Module Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi Akra_Bazzi: theory Akra_Bazzi.Master_Theorem Irrationality_J_Hancl: theory HOL-Library.Float Akra_Bazzi: theory HOL-Decision_Procs.Approximation Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Method Prime_Harmonic_Series: theory HOL-Algebra.Ideal Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation_Bounds Prime_Harmonic_Series: theory HOL-Algebra.RingHom Prime_Harmonic_Series: theory HOL-Algebra.UnivPoly Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation Timing Ergodic_Theory (4 threads, 75.186s elapsed time, 255.236s cpu time, 5.324s GC time, factor 3.39) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ergodic_Theory Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ergodic_Theory/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ergodic_Theory/outline.pdf Finished Ergodic_Theory (0:01:30 elapsed time, 0:04:39 cpu time, factor 3.10) Running Stern_Brocot ... Stern_Brocot: theory HOL-Library.BNF_Corec Prime_Harmonic_Series: theory HOL-Algebra.Multiplicative_Group Stern_Brocot: theory Stern_Brocot.Cotree Prime_Harmonic_Series: theory HOL-Number_Theory.Residues Prime_Harmonic_Series: theory HOL-Number_Theory.Euler_Criterion Prime_Harmonic_Series: theory HOL-Number_Theory.Pocklington Prime_Harmonic_Series: theory HOL-Number_Theory.Gauss Prime_Harmonic_Series: theory HOL-Number_Theory.Residue_Primitive_Roots Prime_Harmonic_Series: theory HOL-Number_Theory.Quadratic_Reciprocity Prime_Harmonic_Series: theory HOL-Number_Theory.Number_Theory Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic_Misc Prime_Harmonic_Series: theory Prime_Harmonic_Series.Squarefree_Nat Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic Stern_Brocot: theory Stern_Brocot.Cotree_Algebra Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree Timing MFMC_Countable (4 threads, 75.971s elapsed time, 233.440s cpu time, 6.712s GC time, factor 3.07) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MFMC_Countable Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MFMC_Countable/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MFMC_Countable/outline.pdf Finished MFMC_Countable (0:01:25 elapsed time, 0:04:09 cpu time, factor 2.91) Running Probabilistic_System_Zoo ... Timing Green (4 threads, 77.891s elapsed time, 267.956s cpu time, 2.776s GC time, factor 3.44) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green/outline.pdf Finished Green (0:01:26 elapsed time, 0:04:48 cpu time, factor 3.34) Running Treaps ... Probabilistic_System_Zoo: theory HOL-Cardinals.Fun_More Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Relation_More Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Union Probabilistic_System_Zoo: theory HOL-Library.Cardinal_Notations Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Extension Probabilistic_System_Zoo: theory HOL-Cardinals.Wellfounded_More Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Relation Treaps: theory HOL-Data_Structures.Less_False Treaps: theory HOL-Data_Structures.Cmp Treaps: theory HOL-Library.Function_Algebras Treaps: theory HOL-Library.Landau_Symbols Treaps: theory HOL-Data_Structures.Sorted_Less Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Embedding Treaps: theory HOL-Data_Structures.List_Ins_Del Treaps: theory Landau_Symbols.Group_Sort Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Constructions Treaps: theory List-Index.List_Index Treaps: theory HOL-Data_Structures.Set_Specs Treaps: theory HOL-Data_Structures.Tree_Set Treaps: theory Comparison_Sort_Lower_Bound.Linorder_Relations Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Order_Relation Probabilistic_System_Zoo: theory HOL-Cardinals.Ordinal_Arithmetic Timing DiscretePricing (4 threads, 72.730s elapsed time, 244.448s cpu time, 9.108s GC time, factor 3.36) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DiscretePricing Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DiscretePricing/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DiscretePricing/outline.pdf Finished DiscretePricing (0:01:22 elapsed time, 0:04:20 cpu time, factor 3.15) Running Prime_Distribution_Elementary ... Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Arithmetic Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinals Treaps: theory Landau_Symbols.Landau_Real_Products Probabilistic_System_Zoo: theory HOL-Cardinals.Bounded_Set Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Approximation Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Nonempty_Bounded_Set Akra_Bazzi: theory Akra_Bazzi.Master_Theorem_Examples Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primes_Omega Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Number_Theorem_Library Prime_Distribution_Elementary: theory Stirling_Formula.Stirling_Formula Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions Treaps: theory Landau_Symbols.Landau_Simprocs Treaps: theory Landau_Symbols.Landau_More Treaps: theory Quick_Sort_Cost.Randomised_Quick_Sort Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc Treaps: theory Quick_Sort_Cost.Quick_Sort_Average_Case Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds Probabilistic_System_Zoo: theory HOL-Eisbach.Eisbach Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primorial Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Shapiro_Tauberian Irrationality_J_Hancl: theory Irrationality_J_Hancl.Irrationality_J_Hancl Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Probabilistic_Hierarchy Treaps: theory Random_BSTs.Random_BSTs Stern_Brocot: theory Stern_Brocot.Bird_Tree Timing Prime_Harmonic_Series (4 threads, 78.515s elapsed time, 282.956s cpu time, 13.984s GC time, factor 3.60) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series/outline.pdf Finished Prime_Harmonic_Series (0:01:23 elapsed time, 0:04:52 cpu time, factor 3.52) Timing Akra_Bazzi (4 threads, 73.360s elapsed time, 242.088s cpu time, 9.284s GC time, factor 3.30) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Akra_Bazzi Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Akra_Bazzi/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Akra_Bazzi/outline.pdf Finished Akra_Bazzi (0:01:19 elapsed time, 0:04:14 cpu time, factor 3.19) Building Randomised_Social_Choice ... Running Monomorphic_Monad ... Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula Monomorphic_Monad: theory HOL-Library.Cardinal_Notations Randomised_Social_Choice: theory Randomised_Social_Choice.Lotteries Randomised_Social_Choice: theory Randomised_Social_Choice.QSOpt_Exact Randomised_Social_Choice: theory List-Index.List_Index Monomorphic_Monad: theory HOL-Library.Countable_Set_Type Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences Randomised_Social_Choice: theory Randomised_Social_Choice.Order_Predicates Treaps: theory Treaps.Treap Treaps: theory Treaps.Probability_Misc Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profiles Treaps: theory Treaps.Random_List_Permutation Monomorphic_Monad: theory Monomorphic_Monad.Monomorphic_Monad Treaps: theory Treaps.Treap_Sort_and_BSTs Randomised_Social_Choice: theory Randomised_Social_Choice.Elections Randomised_Social_Choice: theory Randomised_Social_Choice.Utility_Functions Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profile_Cmd Timing Stern_Brocot (4 threads, 45.616s elapsed time, 72.616s cpu time, 3.920s GC time, factor 1.59) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stern_Brocot Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stern_Brocot/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stern_Brocot/outline.pdf Finished Stern_Brocot (0:00:51 elapsed time, 0:01:24 cpu time, factor 1.63) Running Probabilistic_System_Zoo-Non_BNFs ... Randomised_Social_Choice: theory Randomised_Social_Choice.Stochastic_Dominance Timing Irrationality_J_Hancl (4 threads, 72.123s elapsed time, 159.048s cpu time, 5.980s GC time, factor 2.21) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Irrationality_J_Hancl Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Irrationality_J_Hancl/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Irrationality_J_Hancl/outline.pdf Finished Irrationality_J_Hancl (0:01:17 elapsed time, 0:02:49 cpu time, factor 2.19) Randomised_Social_Choice: theory Randomised_Social_Choice.SD_Efficiency Building Quick_Sort_Cost ... Randomised_Social_Choice: theory Randomised_Social_Choice.Social_Decision_Schemes Probabilistic_System_Zoo-Non_BNFs: theory HOL-Eisbach.Eisbach Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Fun_More Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Order_Relation_More Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Order_Union Probabilistic_System_Zoo-Non_BNFs: theory HOL-Library.Cardinal_Notations Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Wellorder_Extension Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Wellfounded_More Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Wellorder_Relation Quick_Sort_Cost: theory HOL-Library.Function_Algebras Quick_Sort_Cost: theory HOL-Library.Landau_Symbols Quick_Sort_Cost: theory Landau_Symbols.Group_Sort Quick_Sort_Cost: theory List-Index.List_Index Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Wellorder_Embedding Treaps: theory Treaps.Random_Treap Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Wellorder_Constructions Quick_Sort_Cost: theory Comparison_Sort_Lower_Bound.Linorder_Relations Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Cardinal_Order_Relation Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Ordinal_Arithmetic Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Dictatorship Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Automation Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Lowering Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Serial_Dictatorship Randomised_Social_Choice: theory Randomised_Social_Choice.Randomised_Social_Choice Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Cardinal_Arithmetic Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Cardinals Quick_Sort_Cost: theory Landau_Symbols.Landau_Real_Products Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Bounded_Set Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Nonempty_Bounded_Set Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Probabilistic_Hierarchy Quick_Sort_Cost: theory Landau_Symbols.Landau_Simprocs Quick_Sort_Cost: theory Landau_Symbols.Landau_More Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case Timing Constructive_Cryptography (4 threads, 330.117s elapsed time, 629.760s cpu time, 7.508s GC time, factor 1.91) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography/outline.pdf Finished Constructive_Cryptography (0:05:40 elapsed time, 0:10:47 cpu time, factor 1.90) Running Game_Based_Crypto ... Timing Treaps (4 threads, 37.685s elapsed time, 122.260s cpu time, 3.700s GC time, factor 3.24) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Treaps Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Treaps/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Treaps/outline.pdf Finished Treaps (0:00:43 elapsed time, 0:02:12 cpu time, factor 3.08) Running Prime_Number_Theorem ... Game_Based_Crypto: theory HOL-Library.LaTeXsugar Game_Based_Crypto: theory Game_Based_Crypto.Diffie_Hellman Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2_sym Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK_Single Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Function Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Permutation Game_Based_Crypto: theory Game_Based_Crypto.Guessing_Many_One Game_Based_Crypto: theory Game_Based_Crypto.CryptHOL_Tutorial Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF Monomorphic_Monad: theory Monomorphic_Monad.Interpreter Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading Game_Based_Crypto: theory Game_Based_Crypto.RP_RF Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2 Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula Timing Probabilistic_System_Zoo (4 threads, 41.318s elapsed time, 98.840s cpu time, 3.856s GC time, factor 2.39) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo/outline.pdf Finished Probabilistic_System_Zoo (0:00:45 elapsed time, 0:01:47 cpu time, factor 2.35) Running Tarskis_Geometry ... Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA Game_Based_Crypto: theory Game_Based_Crypto.Elgamal Tarskis_Geometry: theory HOL-Algebra.Congruence Tarskis_Geometry: theory HOL-Library.Quadratic_Discriminant Tarskis_Geometry: theory Tarskis_Geometry.Metric Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Vardi Tarskis_Geometry: theory Tarskis_Geometry.Miscellany Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA Tarskis_Geometry: theory Tarskis_Geometry.Linear_Algebra2 Tarskis_Geometry: theory Tarskis_Geometry.Tarski Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA Tarskis_Geometry: theory Tarskis_Geometry.Euclid_Tarski Tarskis_Geometry: theory HOL-Algebra.Order Timing Prime_Distribution_Elementary (4 threads, 36.607s elapsed time, 138.704s cpu time, 3.108s GC time, factor 3.79) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary/outline.pdf Finished Prime_Distribution_Elementary (0:00:44 elapsed time, 0:02:31 cpu time, factor 3.44) Running UpDown_Scheme ... Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal UpDown_Scheme: theory HOL-Eisbach.Eisbach UpDown_Scheme: theory HOL-Library.Adhoc_Overloading UpDown_Scheme: theory HOL-ex.Quicksort UpDown_Scheme: theory HOL-Library.Option_ord UpDown_Scheme: theory HOL-Library.Monad_Syntax UpDown_Scheme: theory HOL-Imperative_HOL.Heap Tarskis_Geometry: theory HOL-Algebra.Lattice UpDown_Scheme: theory UpDown_Scheme.Grid_Point UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Syntax_Match Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems UpDown_Scheme: theory Automatic_Refinement.Misc Tarskis_Geometry: theory HOL-Algebra.Complete_Lattice Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec UpDown_Scheme: theory UpDown_Scheme.Grid UpDown_Scheme: theory HOL-Imperative_HOL.Heap_Monad Tarskis_Geometry: theory HOL-Algebra.Group Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Finitely_Bounded_Set_Counterexample Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Vardi_Counterexample UpDown_Scheme: theory UpDown_Scheme.UpDown_Scheme Timing Randomised_Social_Choice (4 threads, 12.879s elapsed time, 47.960s cpu time, 2.028s GC time, factor 3.72) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice/outline.pdf Finished Randomised_Social_Choice (0:00:39 elapsed time, 0:01:30 cpu time, factor 2.32) Running SDS_Impossibility ... UpDown_Scheme: theory UpDown_Scheme.Triangular_Function Tarskis_Geometry: theory Tarskis_Geometry.Action Tarskis_Geometry: theory Tarskis_Geometry.Projective UpDown_Scheme: theory HOL-Imperative_HOL.Array UpDown_Scheme: theory UpDown_Scheme.Down UpDown_Scheme: theory UpDown_Scheme.Up SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility UpDown_Scheme: theory HOL-Imperative_HOL.Ref UpDown_Scheme: theory UpDown_Scheme.Up_Down UpDown_Scheme: theory HOL-Imperative_HOL.Imperative_HOL UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Run UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Assertions Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto Timing Monomorphic_Monad (4 threads, 37.001s elapsed time, 65.080s cpu time, 2.872s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monomorphic_Monad Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monomorphic_Monad/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monomorphic_Monad/outline.pdf Finished Monomorphic_Monad (0:00:44 elapsed time, 0:01:20 cpu time, factor 1.80) Running Lp ... Tarskis_Geometry: theory Tarskis_Geometry.Hyperbolic_Tarski Lp: theory Ergodic_Theory.SG_Library_Complement UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Hoare_Triple Timing Probabilistic_System_Zoo-Non_BNFs (4 threads, 36.867s elapsed time, 114.276s cpu time, 4.684s GC time, factor 3.10) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs/outline.pdf Finished Probabilistic_System_Zoo-Non_BNFs (0:00:42 elapsed time, 0:02:04 cpu time, factor 2.95) Building Stirling_Formula ... UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Automation Lp: theory Lp.Functional_Spaces Stirling_Formula: theory HOL-Library.Function_Algebras Stirling_Formula: theory HOL-Library.Stirling Stirling_Formula: theory Bernoulli.Bernoulli Stirling_Formula: theory HOL-Library.Landau_Symbols Stirling_Formula: theory Landau_Symbols.Group_Sort UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Sep_Main UpDown_Scheme: theory UpDown_Scheme.Imperative Stirling_Formula: theory Bernoulli.Periodic_Bernpoly Stirling_Formula: theory Bernoulli.Bernoulli_FPS Lp: theory Lp.Lp Timing Quick_Sort_Cost (4 threads, 15.776s elapsed time, 58.192s cpu time, 2.172s GC time, factor 3.69) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quick_Sort_Cost Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quick_Sort_Cost/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quick_Sort_Cost/outline.pdf Finished Quick_Sort_Cost (0:00:44 elapsed time, 0:01:45 cpu time, factor 2.38) Running Quaternions ... Quaternions: theory Quaternions.Quaternions Stirling_Formula: theory Landau_Symbols.Landau_Real_Products Stirling_Formula: theory Landau_Symbols.Landau_Simprocs Stirling_Formula: theory Landau_Symbols.Landau_More Stirling_Formula: theory Stirling_Formula.Stirling_Formula Stirling_Formula: theory Stirling_Formula.Ln_Gamma_Asymptotics Timing Game_Based_Crypto (4 threads, 30.603s elapsed time, 115.368s cpu time, 2.956s GC time, factor 3.77) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Game_Based_Crypto Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Game_Based_Crypto/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Game_Based_Crypto/outline.pdf Finished Game_Based_Crypto (0:00:40 elapsed time, 0:02:14 cpu time, factor 3.31) Running pGCL ... pGCL: theory pGCL.Misc pGCL: theory pGCL.Expectations Timing Prime_Number_Theorem (4 threads, 33.076s elapsed time, 104.032s cpu time, 2.740s GC time, factor 3.15) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Number_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Number_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Number_Theorem/outline.pdf Finished Prime_Number_Theorem (0:00:40 elapsed time, 0:01:57 cpu time, factor 2.88) Running HOL-Analysis-ex ... pGCL: theory pGCL.Transformers Timing UpDown_Scheme (4 threads, 30.975s elapsed time, 120.084s cpu time, 3.628s GC time, factor 3.88) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UpDown_Scheme Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UpDown_Scheme/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UpDown_Scheme/outline.pdf Finished UpDown_Scheme (0:00:36 elapsed time, 0:02:10 cpu time, factor 3.57) Running Kuratowski_Closure_Complement ... HOL-Analysis-ex: theory HOL-Analysis-ex.Approximations Timing Tarskis_Geometry (4 threads, 31.424s elapsed time, 111.856s cpu time, 3.604s GC time, factor 3.56) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tarskis_Geometry Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tarskis_Geometry/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tarskis_Geometry/outline.pdf Finished Tarskis_Geometry (0:00:40 elapsed time, 0:02:06 cpu time, factor 3.16) Running Octonions ... pGCL: theory pGCL.Induction Kuratowski_Closure_Complement: theory Kuratowski_Closure_Complement.KuratowskiClosureComplementTheorem pGCL: theory pGCL.Embedding Octonions: theory Octonions.Cross_Product_7 pGCL: theory pGCL.Healthiness pGCL: theory pGCL.Continuity pGCL: theory pGCL.LoopInduction pGCL: theory pGCL.Sublinearity pGCL: theory pGCL.WellDefined pGCL: theory pGCL.Algebra pGCL: theory pGCL.Determinism pGCL: theory pGCL.Loops pGCL: theory pGCL.StructuredReasoning Octonions: theory Octonions.Octonions pGCL: theory pGCL.Automation pGCL: theory pGCL.Termination pGCL: theory pGCL.pGCL Timing Lp (4 threads, 26.668s elapsed time, 87.336s cpu time, 1.412s GC time, factor 3.27) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lp Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lp/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lp/outline.pdf Finished Lp (0:00:33 elapsed time, 0:01:40 cpu time, factor 2.98) Running Euler_MacLaurin ... pGCL: theory pGCL.LoopExamples pGCL: theory pGCL.Monty pGCL: theory pGCL.Primitives Euler_MacLaurin: theory HOL-Library.Function_Algebras Euler_MacLaurin: theory HOL-Library.Stirling Euler_MacLaurin: theory Bernoulli.Bernoulli Euler_MacLaurin: theory HOL-Library.Landau_Symbols Euler_MacLaurin: theory Landau_Symbols.Group_Sort Euler_MacLaurin: theory Bernoulli.Periodic_Bernpoly Euler_MacLaurin: theory Bernoulli.Bernoulli_FPS Timing Quaternions (4 threads, 24.837s elapsed time, 34.644s cpu time, 0.724s GC time, factor 1.39) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quaternions Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quaternions/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quaternions/outline.pdf Finished Quaternions (0:00:30 elapsed time, 0:00:45 cpu time, factor 1.51) Building Random_BSTs ... Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin Random_BSTs: theory HOL-Data_Structures.Cmp Random_BSTs: theory HOL-Data_Structures.Less_False Random_BSTs: theory HOL-Data_Structures.Sorted_Less Random_BSTs: theory HOL-Data_Structures.List_Ins_Del Random_BSTs: theory HOL-Data_Structures.Set_Specs Random_BSTs: theory HOL-Data_Structures.Tree_Set Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products Random_BSTs: theory Random_BSTs.Random_BSTs Timing SDS_Impossibility (4 threads, 39.951s elapsed time, 92.972s cpu time, 1.580s GC time, factor 2.33) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/SDS_Impossibility Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/SDS_Impossibility/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/SDS_Impossibility/outline.pdf Finished SDS_Impossibility (0:00:46 elapsed time, 0:01:44 cpu time, factor 2.26) Running Probabilistic_System_Zoo-BNFs ... Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Fun_More Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Order_Relation_More Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Order_Union Probabilistic_System_Zoo-BNFs: theory HOL-Library.Cardinal_Notations Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Wellorder_Extension Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Wellfounded_More Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Wellorder_Relation Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Wellorder_Embedding Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Wellorder_Constructions Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs Euler_MacLaurin: theory Landau_Symbols.Landau_More Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Cardinal_Order_Relation Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Ordinal_Arithmetic Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Cardinal_Arithmetic Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Cardinals Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Bounded_Set Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Bool_Bounded_Set Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Nonempty_Bounded_Set Timing HOL-Analysis-ex (4 threads, 23.276s elapsed time, 58.772s cpu time, 0.268s GC time, factor 2.53) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis-ex Finished HOL-Analysis-ex (0:00:24 elapsed time, 0:01:00 cpu time, factor 2.42) Running Cayley_Hamilton ... Cayley_Hamilton: theory HOL-Library.More_List Cayley_Hamilton: theory Cayley_Hamilton.Square_Matrix Cayley_Hamilton: theory HOL-Computational_Algebra.Polynomial Timing Octonions (4 threads, 20.002s elapsed time, 68.332s cpu time, 1.720s GC time, factor 3.42) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Octonions Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Octonions/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Octonions/outline.pdf Finished Octonions (0:00:25 elapsed time, 0:01:18 cpu time, factor 3.12) Running Neumann_Morgenstern_Utility ... Timing Stirling_Formula (4 threads, 22.907s elapsed time, 75.672s cpu time, 2.500s GC time, factor 3.30) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula/outline.pdf Finished Stirling_Formula (0:00:49 elapsed time, 0:02:01 cpu time, factor 2.44) Running Catalan_Numbers ... Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries Catalan_Numbers: theory HOL-Library.Function_Algebras Catalan_Numbers: theory HOL-Library.Landau_Symbols Catalan_Numbers: theory Catalan_Numbers.Catalan_Auxiliary_Integral Catalan_Numbers: theory Landau_Symbols.Group_Sort Timing Kuratowski_Closure_Complement (4 threads, 22.652s elapsed time, 72.212s cpu time, 1.832s GC time, factor 3.19) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement/outline.pdf Finished Kuratowski_Closure_Complement (0:00:28 elapsed time, 0:01:23 cpu time, factor 2.95) Running Error_Function ... Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem Error_Function: theory HOL-Library.Function_Algebras Error_Function: theory HOL-Library.Landau_Symbols Error_Function: theory Landau_Symbols.Group_Sort Timing pGCL (4 threads, 24.019s elapsed time, 91.320s cpu time, 1.744s GC time, factor 3.80) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/pGCL Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/pGCL/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/pGCL/outline.pdf Finished pGCL (0:00:33 elapsed time, 0:01:48 cpu time, factor 3.23) Running HOL-Probability-ex ... Catalan_Numbers: theory Landau_Symbols.Landau_Real_Products HOL-Probability-ex: theory HOL-Library.Permutation HOL-Probability-ex: theory HOL-Probability-ex.Dining_Cryptographers HOL-Probability-ex: theory HOL-Probability-ex.Measure_Not_CCC Timing Euler_MacLaurin (4 threads, 18.121s elapsed time, 67.096s cpu time, 2.384s GC time, factor 3.70) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin/outline.pdf Finished Euler_MacLaurin (0:00:23 elapsed time, 0:01:18 cpu time, factor 3.28) Running Bernoulli ... Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility HOL-Probability-ex: theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure Bernoulli: theory HOL-Library.Stirling Bernoulli: theory Bernoulli.Bernoulli Error_Function: theory Error_Function.Error_Function Error_Function: theory Landau_Symbols.Landau_Real_Products Bernoulli: theory Bernoulli.Periodic_Bernpoly Bernoulli: theory Bernoulli.Bernoulli_FPS Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton Timing Probabilistic_System_Zoo-BNFs (4 threads, 14.453s elapsed time, 53.500s cpu time, 1.760s GC time, factor 3.70) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-BNFs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-BNFs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-BNFs/outline.pdf Finished Probabilistic_System_Zoo-BNFs (0:00:19 elapsed time, 0:01:03 cpu time, factor 3.25) Running Random_Graph_Subgraph_Threshold ... Bernoulli: theory Bernoulli.Bernoulli_Zeta Catalan_Numbers: theory Landau_Symbols.Landau_Simprocs Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc Catalan_Numbers: theory Landau_Symbols.Landau_More Catalan_Numbers: theory Catalan_Numbers.Catalan_Numbers Error_Function: theory Landau_Symbols.Landau_Simprocs Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas Error_Function: theory Landau_Symbols.Landau_More Error_Function: theory Error_Function.Error_Function_Asymptotics Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold Timing Cayley_Hamilton (4 threads, 12.955s elapsed time, 40.052s cpu time, 1.672s GC time, factor 3.09) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cayley_Hamilton Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cayley_Hamilton/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cayley_Hamilton/outline.pdf Finished Cayley_Hamilton (0:00:17 elapsed time, 0:00:49 cpu time, factor 2.81) Running Rank_Nullity_Theorem ... Timing HOL-Probability-ex (4 threads, 9.833s elapsed time, 26.792s cpu time, 0.648s GC time, factor 2.72) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability-ex Finished HOL-Probability-ex (0:00:11 elapsed time, 0:00:28 cpu time, factor 2.42) Running First_Welfare_Theorem ... Rank_Nullity_Theorem: theory HOL-Library.Bit Rank_Nullity_Theorem: theory HOL-Library.Function_Algebras Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dual_Order Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Mod_Type Timing Random_BSTs (4 threads, 8.327s elapsed time, 16.688s cpu time, 0.892s GC time, factor 2.00) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_BSTs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_BSTs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_BSTs/outline.pdf Finished Random_BSTs (0:00:32 elapsed time, 0:00:56 cpu time, factor 1.74) Running Randomised_BSTs ... Timing Catalan_Numbers (4 threads, 12.245s elapsed time, 40.716s cpu time, 1.572s GC time, factor 3.33) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Catalan_Numbers Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Catalan_Numbers/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Catalan_Numbers/outline.pdf Finished Catalan_Numbers (0:00:16 elapsed time, 0:00:50 cpu time, factor 2.98) Timing Neumann_Morgenstern_Utility (4 threads, 12.231s elapsed time, 40.588s cpu time, 0.840s GC time, factor 3.32) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Neumann_Morgenstern_Utility Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Neumann_Morgenstern_Utility/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Neumann_Morgenstern_Utility/outline.pdf Finished Neumann_Morgenstern_Utility (0:00:18 elapsed time, 0:00:51 cpu time, factor 2.87) Running Comparison_Sort_Lower_Bound ... First_Welfare_Theorem: theory First_Welfare_Theorem.Syntax First_Welfare_Theorem: theory First_Welfare_Theorem.Argmax Running Chord_Segments ... First_Welfare_Theorem: theory First_Welfare_Theorem.Consumers First_Welfare_Theorem: theory First_Welfare_Theorem.Preferences Timing Error_Function (4 threads, 11.822s elapsed time, 42.232s cpu time, 1.504s GC time, factor 3.57) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Error_Function Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Error_Function/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Error_Function/outline.pdf Finished Error_Function (0:00:16 elapsed time, 0:00:51 cpu time, factor 3.11) Running Lower_Semicontinuous ... Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation Chord_Segments: theory Triangle.Angles Comparison_Sort_Lower_Bound: theory HOL-Library.Multiset_Permutations Comparison_Sort_Lower_Bound: theory List-Index.List_Index Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs Chord_Segments: theory Triangle.Triangle First_Welfare_Theorem: theory First_Welfare_Theorem.Utility_Functions Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Miscellaneous First_Welfare_Theorem: theory First_Welfare_Theorem.Common Chord_Segments: theory Chord_Segments.Chord_Segments Lower_Semicontinuous: theory Lower_Semicontinuous.Lower_Semicontinuous First_Welfare_Theorem: theory First_Welfare_Theorem.Arrow_Debreu_Model First_Welfare_Theorem: theory First_Welfare_Theorem.Exchange_Economy Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations First_Welfare_Theorem: theory First_Welfare_Theorem.Private_Ownership_Economy Timing Bernoulli (4 threads, 9.512s elapsed time, 25.400s cpu time, 0.408s GC time, factor 2.67) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli/outline.pdf Finished Bernoulli (0:00:14 elapsed time, 0:00:35 cpu time, factor 2.41) Running Buffons_Needle ... Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Fundamental_Subspaces Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dim_Formula Buffons_Needle: theory Buffons_Needle.Buffons_Needle Timing Random_Graph_Subgraph_Threshold (4 threads, 7.505s elapsed time, 21.848s cpu time, 0.528s GC time, factor 2.91) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_Graph_Subgraph_Threshold Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_Graph_Subgraph_Threshold/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_Graph_Subgraph_Threshold/outline.pdf Finished Random_Graph_Subgraph_Threshold (0:00:13 elapsed time, 0:00:33 cpu time, factor 2.45) Running Source_Coding_Theorem ... Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem Timing Chord_Segments (4 threads, 4.985s elapsed time, 10.140s cpu time, 0.124s GC time, factor 2.03) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Chord_Segments Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Chord_Segments/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Chord_Segments/outline.pdf Finished Chord_Segments (0:00:09 elapsed time, 0:00:20 cpu time, factor 2.04) Running Stewart_Apollonius ... Timing Rank_Nullity_Theorem (4 threads, 8.086s elapsed time, 16.704s cpu time, 0.612s GC time, factor 2.07) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem/outline.pdf Finished Rank_Nullity_Theorem (0:00:13 elapsed time, 0:00:26 cpu time, factor 2.04) Running Triangle ... Timing Lower_Semicontinuous (4 threads, 4.990s elapsed time, 15.768s cpu time, 0.260s GC time, factor 3.16) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lower_Semicontinuous Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lower_Semicontinuous/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lower_Semicontinuous/outline.pdf Finished Lower_Semicontinuous (0:00:10 elapsed time, 0:00:25 cpu time, factor 2.53) Running Fisher_Yates ... Stewart_Apollonius: theory Triangle.Angles Timing First_Welfare_Theorem (4 threads, 7.592s elapsed time, 26.180s cpu time, 0.556s GC time, factor 3.45) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/First_Welfare_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/First_Welfare_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/First_Welfare_Theorem/outline.pdf Finished First_Welfare_Theorem (0:00:12 elapsed time, 0:00:36 cpu time, factor 2.86) Running Ptolemys_Theorem ... Stewart_Apollonius: theory Triangle.Triangle Triangle: theory Triangle.Angles Stewart_Apollonius: theory Stewart_Apollonius.Stewart_Apollonius Timing Comparison_Sort_Lower_Bound (4 threads, 7.920s elapsed time, 21.020s cpu time, 0.748s GC time, factor 2.65) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Comparison_Sort_Lower_Bound Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Comparison_Sort_Lower_Bound/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Comparison_Sort_Lower_Bound/outline.pdf Finished Comparison_Sort_Lower_Bound (0:00:12 elapsed time, 0:00:30 cpu time, factor 2.42) Timing Buffons_Needle (4 threads, 4.399s elapsed time, 14.304s cpu time, 0.088s GC time, factor 3.25) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle/outline.pdf Finished Buffons_Needle (0:00:09 elapsed time, 0:00:23 cpu time, factor 2.56) Running Minkowskis_Theorem ... Running Cartan_FP ... Triangle: theory Triangle.Triangle Fisher_Yates: theory Fisher_Yates.Fisher_Yates Ptolemys_Theorem: theory Ptolemys_Theorem.Ptolemys_Theorem Minkowskis_Theorem: theory Minkowskis_Theorem.Minkowskis_Theorem Cartan_FP: theory Cartan_FP.Cartan Timing Source_Coding_Theorem (4 threads, 4.203s elapsed time, 11.192s cpu time, 0.132s GC time, factor 2.66) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Source_Coding_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Source_Coding_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Source_Coding_Theorem/outline.pdf Finished Source_Coding_Theorem (0:00:09 elapsed time, 0:00:21 cpu time, factor 2.30) Timing Randomised_BSTs (4 threads, 9.371s elapsed time, 30.880s cpu time, 0.624s GC time, factor 3.30) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_BSTs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_BSTs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_BSTs/outline.pdf Finished Randomised_BSTs (0:00:14 elapsed time, 0:00:40 cpu time, factor 2.79) Running Monad_Normalisation ... Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test Timing Cartan_FP (4 threads, 1.472s elapsed time, 4.616s cpu time, 0.076s GC time, factor 3.13) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cartan_FP Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cartan_FP/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cartan_FP/outline.pdf Finished Cartan_FP (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.37) Timing Stewart_Apollonius (4 threads, 3.938s elapsed time, 7.156s cpu time, 0.080s GC time, factor 1.82) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius/outline.pdf Finished Stewart_Apollonius (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.93) Timing Ptolemys_Theorem (4 threads, 2.056s elapsed time, 4.780s cpu time, 0.068s GC time, factor 2.32) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ptolemys_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ptolemys_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ptolemys_Theorem/outline.pdf Finished Ptolemys_Theorem (0:00:06 elapsed time, 0:00:13 cpu time, factor 2.19) Timing Minkowskis_Theorem (4 threads, 1.317s elapsed time, 4.544s cpu time, 0.092s GC time, factor 3.45) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem/outline.pdf Finished Minkowskis_Theorem (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.34) Timing Triangle (4 threads, 3.566s elapsed time, 6.200s cpu time, 0.072s GC time, factor 1.74) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Triangle Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Triangle/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Triangle/outline.pdf Finished Triangle (0:00:07 elapsed time, 0:00:14 cpu time, factor 1.90) Timing Fisher_Yates (4 threads, 2.929s elapsed time, 8.284s cpu time, 0.072s GC time, factor 2.83) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fisher_Yates Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fisher_Yates/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fisher_Yates/outline.pdf Finished Fisher_Yates (0:00:07 elapsed time, 0:00:17 cpu time, factor 2.35) Timing Monad_Normalisation (4 threads, 1.017s elapsed time, 1.516s cpu time, 0.000s GC time, factor 1.49) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation/outline.pdf Finished Monad_Normalisation (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.93) HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform *** Timeout Smooth_Manifolds FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Smooth_Manifolds) *** Failed to finish proof (line 587 of "$AFP/Smooth_Manifolds/Analysis_More.thy"): *** goal (1 subgoal): *** 1. \U. *** \U \ f ` topspace T; *** openin T (f -` U \ topspace T)\ *** \ openin T {x \ topspace T. f x \ U} *** At command "by" (line 587 of "$AFP/Smooth_Manifolds/Analysis_More.thy") *** Failed to finish proof (line 552 of "$AFP/Smooth_Manifolds/Analysis_More.thy"): *** goal (1 subgoal): *** 1. \openin Z V; *** \x\topspace (Y i). g (f i x) \ topspace Z; *** openin (Y i) {x \ topspace (Y i). g (f i x) \ V}\ *** \ openin (Y i) *** ((g \ f i) -` V \ topspace (Y i)) *** At command "by" (line 552 of "$AFP/Smooth_Manifolds/Analysis_More.thy") *** Failed to finish proof (line 540 of "$AFP/Smooth_Manifolds/Analysis_More.thy"): *** goal (1 subgoal): *** 1. \U. *** \\i. f i \ topspace (Y i) \ X; *** U \ X; *** \i. openin (Y i) (f i -` U \ topspace (Y i))\ *** \ openin (Y i) *** {x \ topspace (Y i). f i x \ U} *** At command "by" (line 540 of "$AFP/Smooth_Manifolds/Analysis_More.thy") *** Failed to finish proof (line 442 of "$AFP/Smooth_Manifolds/Analysis_More.thy"): *** goal (2 subgoals): *** 1. \X. *** \\x\topspace T1. x \ topspace T2; *** \U. *** openin T2 U \ *** openin T1 {x \ topspace T1. x \ U}; *** openin T2 X\ *** \ openin T1 (X \ topspace T1) *** 2. \U. *** \\X. *** openin T2 X \ *** openin T1 (X \ topspace T1); *** topspace T1 \ topspace T2; openin T2 U\ *** \ openin T1 {x \ topspace T1. x \ U} *** At command "by" (line 442 of "$AFP/Smooth_Manifolds/Analysis_More.thy") HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics Timing HOL-ODE-Numerics (4 threads, 1725.168s elapsed time, 5617.184s cpu time, 1529.592s GC time, factor 3.26) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Numerics Finished HOL-ODE-Numerics (0:30:23 elapsed time, 1:39:26 cpu time, factor 3.27) Building Lorenz_Approximation ... Running HOL-ODE-ARCH-COMP ... Running HOL-ODE-Examples ... Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples Timing HOL-ODE-Examples (4 threads, 233.463s elapsed time, 764.668s cpu time, 10.748s GC time, factor 3.28) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Examples Finished HOL-ODE-Examples (0:03:56 elapsed time, 0:12:47 cpu time, factor 3.25) Timing HOL-ODE-ARCH-COMP (4 threads, 266.761s elapsed time, 594.092s cpu time, 31.444s GC time, factor 2.23) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-ARCH-COMP Finished HOL-ODE-ARCH-COMP (0:04:29 elapsed time, 0:09:56 cpu time, factor 2.22) Timing Lorenz_Approximation (4 threads, 247.287s elapsed time, 510.024s cpu time, 49.960s GC time, factor 2.06) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_Approximation Finished Lorenz_Approximation (0:04:41 elapsed time, 0:09:30 cpu time, factor 2.03) Running Lorenz_C0 ... Running Lorenz_C1 ... Lorenz_C0: theory Lorenz_C0.Lorenz_C0 Lorenz_C1: theory Lorenz_C1.Lorenz_C1 Timing Lorenz_C1 (4 threads, 1.027s elapsed time, 1.760s cpu time, 0.000s GC time, factor 1.71) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_C1 Finished Lorenz_C1 (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.19) Timing Lorenz_C0 (4 threads, 638.363s elapsed time, 2505.436s cpu time, 29.404s GC time, factor 3.92) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_C0 Finished Lorenz_C0 (0:10:40 elapsed time, 0:41:47 cpu time, factor 3.91) Unfinished session(s): Functional_Ordered_Resolution_Prover, Higher_Order_Terms, Lambda_Free_EPO, Lambda_Free_KBOs, Lambda_Free_RPOs, Noninterference_Generic_Unwinding, Smooth_Manifolds === TIMING === Group AFP: 3:40:14 elapsed time, 10:15:00 cpu time, factor 2.79 Group main: 0:13:34 elapsed time, 0:42:31 cpu time, factor 3.13 Group doc: 0:00:00 elapsed time Group timing: 0:13:46 elapsed time, 0:43:00 cpu time, factor 3.12 Group large: 0:14:40 elapsed time, 0:54:39 cpu time, factor 3.72 Group no_doc: 0:00:00 elapsed time Overall: 1:01:54 elapsed time, 10:59:01 cpu time, factor 10.65 === FAILED SESSIONS === Session Lambda_Free_KBOs: FAILED 2 Session Smooth_Manifolds: FAILED 1 Session Functional_Ordered_Resolution_Prover: FAILED 2 Session Higher_Order_Terms: FAILED 2 Session Noninterference_Generic_Unwinding: FAILED 2 Session Lambda_Free_EPO: FAILED 2 Session Lambda_Free_RPOs: FAILED 2 === DEPENDENCIES === Generating dependencies file ... Writing dependencies file ... === REPORT === Writing report file ... === SITEGEN === Writing status file ... Running sitegen ... Success: Generated topics.html Success: Generated index.html Success: Generated html files for 466 entries Success: Generated statistics.html Success: Generated download.html Success: Generated about.html Success: Generated citing.html Success: Generated updating.html Success: Generated search.html Success: Generated submitting.html Success: Generated using.html Success: Generated rss.xml Success: Generated status.html Checked directory thys. Found 0 warnings. Packing tars ... === NOTIFICATIONS === Entry Noninterference_Generic_Unwinding: WARNING no maintainers specified === COMPLETED === Build step 'Execute shell' marked build as failure Archiving artifacts Started calculate disk usage of build Finished Calculation of disk usage of build in 0 seconds Started calculate disk usage of workspace Finished Calculation of disk usage of workspace in 0 seconds No emails were triggered. Finished: FAILURE