Started by an SCM change Running as SYSTEM [EnvInject] - Loading node environment variables. Building remotely on workermtahpc (mta_hpc) 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/ real URL is https://isabelle.in.tum.de/repos/isabelle/ no changes found [isabelle-all] $ hg update --clean --rev default 0 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 1250a1f2bc1e13d8c84c588987bbc7b678ba7350 --template exists\n exists [isabelle-all] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(1250a1f2bc1e13d8c84c588987bbc7b678ba7350)" --encoding UTF-8 --encodingmode replace [afp] $ hg showconfig paths.default [afp] $ hg pull --rev default pulling from https://foss.heptapod.net/isa-afp/afp-devel/ no changes found [afp] $ hg update --clean --rev default 1499 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 6d5f8fb53ac63cd9e1323a5bea3eb8439571f2c7 --template exists\n exists [afp] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(6d5f8fb53ac63cd9e1323a5bea3eb8439571f2c7)" --encoding UTF-8 --encodingmode replace No emails were triggered. [isabelle-all] $ /bin/sh -xe /tmp/jenkins7850469472125718653.sh + Admin/jenkins/run_build all + set -e + PROFILE=all + shift + bin/isabelle components -a + bin/isabelle jedit -bf ### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle.jar) ... ### Building graph browser (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_graphbrowser.jar) ... Note: Some input files use unchecked or unsafe operations. Note: Recompile with -Xlint:unchecked for details. ### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_admin.jar) ... ### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ... ### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ... + bin/isabelle ocaml_setup # Run eval $(opam env) to update the current shell environment [NOTE] It seems you have not updated your repositories for a while. Consider updating them with: opam update [NOTE] Package zarith is already installed (current version is 1.12). + 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.10.7 + bin/isabelle ci_build all === CONFIGURATION === ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g" ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64_32-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-bafe319bc3a6-1/x86_64_32-linux" ML_SYSTEM="polyml-5.9" ML_OPTIONS="-H 4000 --maxheap 8G" jobs = 8, threads = 8, numa = true === BUILD === Build started at Tue, 31 Jan 2023 22:24:30 +0100 Isabelle id 1250a1f2bc1e AFP id 61f7680ed799 === LOG === Session Pure/Pure Session Misc/CTT Session Misc/Cube Session FOL/FOL Session FOL/CCL Session FOL/FOL-ex Session FOL/FOLP Session FOL/FOLP-ex Session Doc/Intro (doc) Session FOL/LCF Session Doc/Logics (doc) Session Doc/Nitpick (doc) Session Pure/Pure-Examples Session Pure/Pure-ex Session Misc/SML Session Misc/Sequents Session Doc/Sledgehammer (doc) Session AFP/SpecCheck (AFP) Session Misc/Tools 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/Ackermanns_not_PR (AFP) Session AFP/AnselmGod (AFP) Session AFP/Aristotles_Assertoric_Syllogistic (AFP) Session AFP/Attack_Trees (AFP) Session AFP/AxiomaticCategoryTheory (AFP) Session AFP/Belief_Revision (AFP) Session AFP/BinarySearchTree (AFP) Session AFP/Binomial-Queues (AFP) Session AFP/Bondy (AFP) Session AFP/Boolos_Curious_Inference (AFP) Session AFP/Boolos_Curious_Inference_Automated (AFP) Session AFP/BytecodeLogicJmlTypes (AFP) Session AFP/C2KA_DistributedSystems (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/Complete_Non_Orders (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/Dedekind_Real (AFP) Session Doc/Demo_EPTCS (doc) Session Doc/Demo_Easychair (doc) Session Doc/Demo_FoilTeX (doc) Session Doc/Demo_LIPIcs (doc) Session Doc/Demo_LLNCS (doc) Session AFP/Depth-First-Search (AFP) Session AFP/Digit_Expansions (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/Foundation_of_geometry (AFP) Session AFP/Free-Boolean-Algebra (AFP) Session AFP/Fresh_Identifiers (AFP) Session AFP/FunWithFunctions (AFP) Session AFP/FunWithTilings (AFP) Session Doc/Functions (doc) Session AFP/GPU_Kernel_PL (AFP) Session AFP/GenClock (AFP) Session AFP/General-Triangle (AFP) Session AFP/Generic_Deriving (AFP) Session AFP/GewirthPGCProof (AFP) Session AFP/GoedelGod (AFP) Session AFP/Goodstein_Lambda (AFP) Session HOL/HOL-Cardinals (timing) Session AFP/Binding_Syntax_Theory (AFP) Session AFP/Epistemic_Logic (AFP) Session AFP/Public_Announcement_Logic (AFP) Session AFP/Stalnaker_Logic (AFP) Session AFP/Ordinals_and_Cardinals (AFP) Session AFP/Risk_Free_Lending (AFP) Session HOL/HOL-Hoare 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/ADS_Functor (AFP) Session AFP/Approximation_Algorithms (AFP) 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/Birkhoff_Finite_Distributive_Lattices (AFP) Session AFP/Boolean_Expression_Checkers (AFP) Session AFP/Bounded_Deducibility_Security (AFP) Session AFP/BD_Security_Compositional (AFP) Session AFP/CoSMeDis (AFP) Session AFP/CoCon (AFP) Session AFP/CoSMed (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 Doc/Codegen (doc) Session AFP/CofGroups (AFP) Session AFP/Completeness (AFP) Session AFP/ConcurrentIMP (AFP) Session AFP/Concurrent_Ref_Alg (AFP) Session AFP/Conditional_Simplification (AFP) Session AFP/Conditional_Transfer_Rule (AFP) Session AFP/CoreC++ (AFP) Session AFP/Core_DOM (AFP) Session AFP/Shadow_DOM (AFP) Session AFP/DOM_Components (AFP) Session AFP/Core_SC_DOM (AFP) Session AFP/Shadow_SC_DOM (AFP) Session AFP/SC_DOM_Components (AFP) Session Doc/Datatypes (doc) Session Doc/Corec (doc) Session AFP/Decl_Sem_Fun_PL (AFP) Session AFP/Encodability_Process_Calculi (AFP) Session AFP/Euler_Partition (AFP) Session AFP/FOL-Fitting (AFP) Session AFP/FOL_Seq_Calc1 (AFP) Session AFP/FOL_Axiomatic (AFP) Session AFP/FOL_Harrison (AFP) Session AFP/Factored_Transition_System_Bounding (AFP) Session AFP/FinFun (AFP) Session AFP/Extended_Finite_State_Machines (AFP) Session AFP/Extended_Finite_State_Machine_Inference (AFP) Session AFP/Finger-Trees (AFP) Session AFP/Finite-Map-Extras (AFP) Session AFP/Generalized_Counting_Sort (AFP) Session AFP/Graph_Saturation (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-Combinatorics (main timing) Session AFP/Blue_Eyes (AFP) Session AFP/Derangements (AFP) Session AFP/Discrete_Summation (AFP) Session AFP/Gauss-Jordan-Elim-Fun (AFP) Session AFP/Graph_Theory (AFP) Session AFP/ShortestPath (AFP) Session HOL/HOL-Computational_Algebra (main timing) Session AFP/Descartes_Sign_Rule (AFP) Session HOL/HOL-Algebra (main timing) Session AFP/Finitely_Generated_Abelian_Groups (AFP) Session HOL/HOL-Decision_Procs (timing) Session HOL/HOL-Quotient_Examples (timing) Session AFP/Interpolation_Polynomials_HOL_Algebra (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/Actuarial_Mathematics (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/Complex_Geometry (AFP) Session AFP/Poincare_Disc (AFP) Session AFP/Differential_Game_Logic (AFP) Session AFP/First_Welfare_Theorem (AFP) Session AFP/Green (AFP) Session HOL/HOL-Analysis-ex Session HOL/HOL-Complex_Analysis (main timing) Session AFP/Cartan_FP (AFP) Session HOL/HOL-Eisbach Session AFP/AOT (AFP) Session AFP/Allen_Calculus (AFP) Session AFP/Card_Partitions (AFP) Session AFP/Bell_Numbers_Spivey (AFP) Session AFP/Card_Equiv_Relations (AFP) Session AFP/Equivalence_Relation_Enumeration (AFP) Session AFP/Falling_Factorial_Sum (AFP) Session AFP/Combinatorial_Enumeration_Algorithms (AFP) Session AFP/Case_Labeling (AFP) Session AFP/Clean (AFP) Session AFP/Combinatorics_Words (AFP) Session AFP/Combinatorics_Words_Graph_Lemma (AFP) Session AFP/Cook_Levin (AFP) Session AFP/Dependent_SIFUM_Type_Systems (AFP) Session AFP/Dependent_SIFUM_Refinement (AFP) Session Doc/Eisbach (doc) Session HOL/HOL-Hahn_Banach Session HOL/HOL-Homology (timing) 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/Laws_of_Large_Numbers (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/Hahn_Jordan_Decomposition (AFP) Session AFP/Lp (AFP) Session AFP/MDP-Rewards (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/Quasi_Borel_Spaces (AFP) Session AFP/Skip_Lists (AFP) Session AFP/Source_Coding_Theorem (AFP) Session AFP/Turans_Graph_Theorem (AFP) Session AFP/Hyperdual (AFP) Session AFP/Irrationality_J_Hancl (AFP) Session AFP/Kuratowski_Closure_Complement (AFP) Session AFP/Laplace_Transform (AFP) Session AFP/Lower_Semicontinuous (AFP) Session AFP/Minkowskis_Theorem (AFP) Session AFP/Octonions (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/MDP-Algorithms (AFP) Session AFP/Tarskis_Geometry (AFP) Session AFP/Triangle (AFP) Session AFP/Chord_Segments (AFP) Session AFP/Stewart_Apollonius (AFP) Session AFP/Youngs_Inequality (AFP) Session AFP/pGCL (AFP) Session HOL/HOL-Examples 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/Arith_Prog_Rel_Primes (AFP) Session AFP/Bernoulli (AFP) Session AFP/E_Transcendental (AFP) Session AFP/Elliptic_Curves_Group_Law (AFP) Session AFP/Fermat3_4 (AFP) Session HOL/HOL-Data_Structures (timing) Session AFP/Efficient-Mergesort (AFP) Session HOL/HOL-Codegenerator_Test Session AFP/Query_Optimization (AFP) Session HOL/HOL-ex (timing) Session AFP/Automatic_Refinement (AFP) Session AFP/Refine_Monadic (AFP) Session AFP/Lehmer (AFP) Session AFP/Lifting_the_Exponent (AFP) Session AFP/Padic_Ints (AFP) Session AFP/Padic_Field (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/Lucas_Theorem (AFP) Session AFP/DPRM_Theorem (AFP) Session AFP/Mason_Stothers (AFP) Session AFP/Polynomial_Interpolation (AFP) Session AFP/Formal_Puiseux_Series (AFP) Session AFP/Probabilistic_Prime_Tests (AFP) Session AFP/Rep_Fin_Groups (AFP) Session AFP/Sturm_Sequences (AFP) Session AFP/Safe_Distance (AFP) Session AFP/Special_Function_Bounds (AFP) Session AFP/Sturm_Tarski (AFP) Session AFP/Budan_Fourier (AFP) Session AFP/Three_Circles (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-IMP (timing) Session AFP/Abs_Int_ITP2012 (AFP) Session AFP/Relational-Incorrectness-Logic (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-Metis_Examples (timing) Session HOL/HOL-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-ex Session HOL/HOL-Proofs-Lambda (timing) Session AFP/Applicative_Lifting (AFP) Session AFP/Free-Groups (AFP) Session AFP/Stern_Brocot (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/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/LightweightJava (AFP) Session AFP/LinearQuantifierElim (AFP) Session AFP/List-Infinite (AFP) Session AFP/Nat-Interval-Logic (AFP) Session AFP/AutoFocus-Stream (AFP) Session AFP/Median_Method (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/Prefix_Free_Code_Combinators (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/Stateful_Protocol_Composition_and_Typing (AFP) Session AFP/Automated_Stateful_Protocol_Verification (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/ResiduatedTransitionSystem (AFP) Session AFP/Ribbon_Proofs (AFP) Session AFP/SATSolverVerification (AFP) Session AFP/Safe_OCL (AFP) Session AFP/Schutz_Spacetime (AFP) Session AFP/Selection_Heap_Sort (AFP) Session AFP/Simplex (AFP) Session AFP/Skew_Heap (AFP) Session AFP/Solidity (AFP) Session AFP/Sort_Encodings (AFP) Session AFP/Splay_Tree (AFP) Session AFP/Amortized_Complexity (AFP) Session AFP/Dynamic_Tables (AFP) Session AFP/Root_Balanced_Tree (AFP) Session AFP/Closest_Pair_Points (AFP) Session AFP/Stable_Matching (AFP) Session AFP/SuperCalc (AFP) Session Doc/System (doc) Session AFP/Szemeredi_Regularity (AFP) Session AFP/Roth_Arithmetic_Progressions (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-Matrix_LP Session HOL/HOL-MicroJava (timing) Session HOL/HOL-Mirabelle-ex Session HOL/HOL-Mutabelle Session HOL/HOL-NanoJava 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-Prolog Session HOL/HOL-Quickcheck_Examples (timing) Session HOL/HOL-Real_Asymp Session AFP/Cotangent_PFD_Formula (AFP) Session AFP/Fourier (AFP) Session AFP/Furstenberg_Topology (AFP) Session HOL/HOL-Real_Asymp-Manual Session AFP/Sophomores_Dream (AFP) Session AFP/Stirling_Formula (AFP) Session AFP/Irrationals_From_THEBOOK (AFP) Session AFP/Lambert_W (AFP) Session HOL/HOL-SET_Protocol (timing) Session HOL/HOL-SMT_Examples (timing) Session HOL/HOL-SPARK Session HOL/HOL-SPARK-Examples Session AFP/RIPEMD-160-SPARK (AFP) Session HOL/HOL-SPARK-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-TPTP Session HOL/HOL-Types_To_Sets Session AFP/Banach_Steinhaus (AFP) Session AFP/Smooth_Manifolds (AFP) Session AFP/Types_To_Sets_Extension (AFP) Session HOL/HOL-Unix Session HOL/HOL-ZF Session AFP/Category2 (AFP) Session HOL/HOLCF (main timing) Session AFP/Circus (AFP) Session AFP/HOL-CSP (AFP) Session HOL/HOLCF-IMP Session HOL/HOLCF-Library Session AFP/CSP_RefTK (AFP) Session HOL/HOLCF-FOCUS Session HOL/HOLCF-ex Session AFP/PCF (AFP) Session AFP/HOLCF-Prelude (AFP) Session AFP/BirdKMP (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/Hales_Jewett (AFP) Session Misc/Haskell Session AFP/Heard_Of (AFP) Session AFP/Consensus_Refined (AFP) Session AFP/Hello_World (AFP) Session AFP/HoareForDivergence (AFP) Session AFP/Hood_Melville_Queue (AFP) Session AFP/HotelKeyCards (AFP) Session Doc/How_to_Prove_it (no_doc) Session AFP/Huffman (AFP) Session AFP/Hybrid_Logic (AFP) Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP) Session AFP/IFC_Tracking (AFP) Session AFP/IMP2 (AFP) Session AFP/IMP2_Binary_Heap (AFP) Session AFP/IMP_Compiler (AFP) Session AFP/IMP_Compiler_Reuse (AFP) Session Doc/Implementation (doc) Session AFP/Implicational_Logic (AFP) Session AFP/Impossible_Geometry (AFP) Session AFP/Inductive_Confidentiality (AFP) Session AFP/Inductive_Inference (AFP) Session AFP/InfPathElimination (AFP) Session AFP/Intro_Dest_Elim (AFP) Session AFP/Involutions2Squares (AFP) Session AFP/IsaGeoCoq (AFP) Session AFP/IsaNet (AFP) Session Doc/Isar_Ref (doc) Session AFP/Isabelle_C (AFP) Session Doc/JEdit (doc) Session AFP/Jacobson_Basic_Algebra (AFP) Session AFP/Grothendieck_Schemes (AFP) Session AFP/Pluennecke_Ruzsa_Inequality (AFP) Session AFP/Khovanskii_Theorem (AFP) Session AFP/Kneser_Cauchy_Davenport (AFP) Session AFP/JiveDataStoreModel (AFP) Session AFP/Key_Agreement_Strong_Adversaries (AFP) Session AFP/Kleene_Algebra (AFP) Session AFP/KAD (AFP) Session AFP/KAT_and_DRA (AFP) Session AFP/Algebraic_VCs (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/Relational_Paths (AFP) Session AFP/Residuated_Lattices (AFP) Session AFP/Knights_Tour (AFP) Session AFP/LambdaMu (AFP) Session AFP/LatticeProperties (AFP) Session AFP/DataRefinementIBP (AFP) Session AFP/GraphMarkingIBP (AFP) Session AFP/Lazy_Case (AFP) Session AFP/Lifting_Definition_Option (AFP) Session AFP/List-Index (AFP) Session AFP/Comparison_Sort_Lower_Bound (AFP) Session AFP/Jinja (AFP) Session AFP/Dominance_CHK (AFP) Session AFP/HRB-Slicing (AFP) Session AFP/InformationFlowSlicing_Inter (AFP) Session AFP/Slicing (AFP) Session AFP/InformationFlowSlicing (AFP) Session AFP/JinjaDCI (AFP) Session AFP/Regression_Test_Selection (AFP) Session AFP/List_Update (AFP) 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/PAPP_Impossibility (AFP) Session AFP/SDS_Impossibility (AFP) Session AFP/List_Interleaving (AFP) Session AFP/List_Inversions (AFP) Session AFP/LocalLexing (AFP) Session Doc/Locales (doc) Session AFP/Locally-Nameless-Sigma (AFP) Session AFP/Logging_Independent_Anonymity (AFP) Session AFP/Lowe_Ontological_Argument (AFP) Session Doc/Main (doc) Session AFP/Marriage (AFP) Session AFP/Latin_Square (AFP) Session AFP/Matroids (AFP) Session AFP/Max-Card-Matching (AFP) Session AFP/Maximum_Segment_Sum (AFP) Session AFP/Median_Of_Medians_Selection (AFP) Session AFP/KD_Tree (AFP) Session AFP/Menger (AFP) Session AFP/Mereology (AFP) Session AFP/Metalogic_ProofChecker (AFP) Session AFP/MiniML (AFP) Session AFP/Modular_Assembly_Kit_Security (AFP) Session AFP/MonoBoolTranAlgebra (AFP) Session AFP/Multitape_To_Singletape_TM (AFP) Session AFP/Name_Carrying_Type_Inference (AFP) Session AFP/Nano_JSON (AFP) Session AFP/Nash_Williams (AFP) Session AFP/No_FTL_observers (AFP) Session AFP/Nominal2 (AFP) Session AFP/Incompleteness (AFP) Session AFP/Surprise_Paradox (AFP) Session AFP/LambdaAuth (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/Ordinal (AFP) Session AFP/Nested_Multisets_Ordinals (AFP) Session AFP/Design_Theory (AFP) Session AFP/Undirected_Graph_Theory (AFP) Session AFP/Balog_Szemeredi_Gowers (AFP) Session AFP/Lambda_Free_RPOs (AFP) Session AFP/Lambda_Free_EPO (AFP) Session AFP/Ordered_Resolution_Prover (AFP) Session AFP/Chandy_Lamport (AFP) Session AFP/Saturation_Framework (AFP) Session AFP/Saturation_Framework_Extensions (AFP) Session AFP/Progress_Tracking (AFP) Session AFP/PAL (AFP) Session AFP/PLM (AFP) Session AFP/PSemigroupsConvolution (AFP) Session AFP/Package_logic (AFP) Session AFP/Combinable_Wands (AFP) Session AFP/Paraconsistency (AFP) Session AFP/Parity_Game (AFP) Session AFP/GaleStewart_Games (AFP) Session AFP/Partial_Function_MR (AFP) Session AFP/Physical_Quantities (AFP) Session AFP/Pop_Refinement (AFP) Session AFP/Possibilistic_Noninterference (AFP) Session AFP/Priority_Search_Trees (AFP) Session AFP/Prim_Dijkstra_Simple (AFP) Session Doc/Prog_Prove (doc) Session AFP/Projective_Geometry (AFP) Session AFP/Proof_Strategy_Language (AFP) Session AFP/PropResPI (AFP) Session AFP/Propositional_Logic_Class (AFP) Session AFP/Propositional_Proof_Systems (AFP) Session AFP/PseudoHoops (AFP) Session AFP/Ramsey-Infinite (AFP) Session AFP/Real_Power (AFP) Session AFP/Real_Time_Deque (AFP) Session AFP/Recursion-Theory-I (AFP) Session AFP/Minsky_Machines (AFP) Session AFP/RefinementReactive (AFP) Session AFP/Regex_Equivalence (AFP) Session AFP/Relational_Method (AFP) Session AFP/Resolution_FOL (AFP) Session AFP/Robbins-Conjecture (AFP) Session AFP/Roy_Floyd_Warshall (AFP) Session AFP/SCC_Bloemen_Sequential (AFP) Session AFP/SIFPL (AFP) Session AFP/SIFUM_Type_Systems (AFP) Session AFP/Sauer_Shelah_Lemma (AFP) Session AFP/Security_Protocol_Refinement (AFP) Session AFP/SenSocialChoice (AFP) Session AFP/Separation_Algebra (AFP) Session AFP/Hoare_Time (AFP) Session AFP/Separata (AFP) Session AFP/Separation_Logic_Unbounded (AFP) Session AFP/Simpl (AFP) Session AFP/BDD (AFP) Session AFP/SimplifiedOntologicalArgument (AFP) Session AFP/Sliding_Window_Algorithm (AFP) Session AFP/Statecharts (AFP) Session AFP/Stellar_Quorums (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/Relational_Disjoint_Set_Forests (AFP) Session AFP/Relational_Minimum_Spanning_Trees (AFP) Session AFP/Relational_Forests (AFP) Session AFP/Subset_Boolean_Algebras (AFP) Session AFP/Correctness_Algebras (AFP) Session AFP/Store_Buffer_Reduction (AFP) Session AFP/StrictOmegaCategories (AFP) Session AFP/Strong_Security (AFP) Session Doc/Sugar (doc) Session AFP/Sunflowers (AFP) Session AFP/Clique_and_Monotone_Circuits (AFP) Session AFP/Suppes_Theorem (AFP) Session AFP/Syntax_Independent_Logic (AFP) Session AFP/Goedel_Incompleteness (AFP) Session AFP/Goedel_HFSet_Semantic (AFP) Session AFP/Goedel_HFSet_Semanticless (AFP) Session AFP/Robinson_Arithmetic (AFP) Session AFP/Synthetic_Completeness (AFP) Session AFP/Szpilrajn (AFP) Session AFP/Combinatorics_Words_Lyndon (AFP) Session AFP/TESL_Language (AFP) Session AFP/TLA (AFP) Session AFP/Timed_Automata (AFP) Session AFP/Probabilistic_Timed_Automata (AFP) Session AFP/Topological_Semantics (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/Van_der_Waerden (AFP) Session AFP/VeriComp (AFP) Session AFP/Interpreter_Optimizations (AFP) Session AFP/Verified-Prover (AFP) Session AFP/VolpanoSmith (AFP) Session AFP/WHATandWHERE_Security (AFP) Session AFP/Weight_Balanced_Trees (AFP) Session AFP/Weighted_Arithmetic_Geometric_Mean (AFP) Session AFP/Word_Lib (AFP) Session AFP/Complx (AFP) Session AFP/IEEE_Floating_Point (AFP) Session AFP/IP_Addresses (AFP) Session AFP/Simple_Firewall (AFP) Session AFP/Routing (AFP) Session AFP/Interval_Arithmetic_Word32 (AFP) Session AFP/LEM (AFP) Session AFP/Native_Word (AFP) Session AFP/Collections (AFP) Session AFP/Abstract_Completeness (AFP) Session AFP/Abstract_Soundness (AFP) Session AFP/FOL_Seq_Calc3 (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/CHERI-C_Memory_Model (AFP) Session AFP/Collections_Examples (AFP) Session AFP/Containers-Benchmarks (AFP) Session AFP/Eval_FO (AFP) Session AFP/MFOTL_Monitor (AFP) Session AFP/Generic_Join (AFP) Session AFP/MFODL_Monitor_Optimized (AFP) Session AFP/VYDRA_MDL (AFP) Session AFP/Formula_Derivatives (AFP) Session AFP/MSO_Regex_Equivalence (AFP) Session AFP/Show (AFP) Session AFP/Affine_Arithmetic (AFP) Session AFP/Ordinary_Differential_Equations (AFP) Session AFP/Differential_Dynamic_Logic (AFP) Session AFP/Hybrid_Systems_VCs (AFP) Session AFP/Matrices_for_ODEs (AFP) Session AFP/Taylor_Models (AFP) Session AFP/CakeML (AFP) Session AFP/Certification_Monads (AFP) Session AFP/AI_Planning_Languages_Semantics (AFP) Session AFP/Verified_SAT_Based_AI_Planning (AFP) Session AFP/Dict_Construction (AFP) Session AFP/Formula_Derivatives-Examples (AFP) Session AFP/Monad_Memo_DP (AFP) Session AFP/Hidden_Markov_Models (AFP) Session AFP/Optimal_BST (AFP) Session AFP/Polynomial_Factorization (AFP) Session AFP/Amicable_Numbers (AFP) Session AFP/Dirichlet_Series (AFP) Session AFP/Finite_Fields (AFP) Session AFP/Universal_Hash_Families (AFP) Session AFP/Frequency_Moments (AFP) Session AFP/Zeta_Function (AFP) Session AFP/Dirichlet_L (AFP) Session AFP/Gauss_Sums (AFP) Session AFP/Prime_Number_Theorem (AFP) Session AFP/Prime_Distribution_Elementary (AFP) Session AFP/IMO2019 (AFP) Session AFP/Irrational_Series_Erdos_Straus (AFP) Session AFP/Transcendence_Series_Hancl_Rucki (AFP) Session AFP/Zeta_3_Irrational (AFP) Session AFP/Gaussian_Integers (AFP) Session AFP/Jordan_Normal_Form (AFP) Session AFP/Farkas (AFP) Session AFP/Isabelle_Marries_Dirac (AFP) Session AFP/Knuth_Bendix_Order (AFP) Session AFP/Functional_Ordered_Resolution_Prover (AFP) Session AFP/Regular_Tree_Relations (AFP) Session AFP/FO_Theory_Rewriting (AFP) Session AFP/Rewrite_Properties_Reduction (AFP) Session AFP/Weighted_Path_Order (AFP) Session AFP/Multiset_Ordering_NPC (AFP) Session AFP/Linear_Recurrences (AFP) Session AFP/Perron_Frobenius (AFP) Session AFP/Stochastic_Matrices (AFP) Session AFP/Subresultants (AFP) Session AFP/Berlekamp_Zassenhaus (AFP) Session AFP/Algebraic_Numbers (AFP) Session AFP/BenOr_Kozen_Reif (AFP) Session AFP/LLL_Basis_Reduction (AFP) Session AFP/LLL_Factorization (AFP) Session AFP/Linear_Inequalities (AFP) Session AFP/LP_Duality (AFP) Session AFP/Linear_Programming (AFP) Session AFP/Number_Theoretic_Transform (AFP) Session AFP/CRYSTALS-Kyber (AFP) Session AFP/Smith_Normal_Form (AFP) Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP) Session AFP/Polynomials (AFP) Session AFP/Deep_Learning (AFP) Session AFP/QHLProver (AFP) Session AFP/Projective_Measurements (AFP) Session AFP/Commuting_Hermitian (AFP) Session AFP/Groebner_Bases (AFP) Session AFP/Fishers_Inequality (AFP) Session AFP/Groebner_Macaulay (AFP) Session AFP/Nullstellensatz (AFP) Session AFP/Signature_Groebner (AFP) Session AFP/Lambda_Free_KBOs (AFP) Session AFP/Symmetric_Polynomials (AFP) Session AFP/Pi_Transcendental (AFP) Session AFP/Power_Sum_Polynomials (AFP) Session AFP/Hermite_Lindemann (AFP) Session AFP/Factor_Algebraic_Polynomial (AFP) Session AFP/Cubic_Quartic_Equations (AFP) Session AFP/Linear_Recurrences_Solver (AFP) Session AFP/Virtual_Substitution (AFP) Session AFP/Real_Impl (AFP) Session AFP/Complex_Bounded_Operators (AFP) Session AFP/Registers (AFP) Session AFP/QR_Decomposition (AFP) Session AFP/XML (AFP) Session AFP/Van_Emde_Boas_Trees (AFP) Session AFP/Dijkstra_Shortest_Path (AFP) Session AFP/Koenigsberg_Friendship (AFP) Session AFP/FOL_Seq_Calc2 (AFP) Session AFP/Formal_SSA (AFP) Session AFP/Minimal_SSA (AFP) Session AFP/Gale_Shapley (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/Poincare_Bendixson (AFP) Session AFP/Safe_Range_RC (AFP) Session AFP/Transition_Systems_and_Automata (AFP) Session AFP/Adaptive_State_Counting (AFP) Session AFP/Buchi_Complementation (AFP) Session AFP/LTL_Master_Theorem (AFP) Session AFP/LTL_Normal_Form (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/LTL_to_DRA (AFP) Session AFP/Network_Security_Policy_Verification (AFP) Session AFP/Planarity_Certificates (AFP) Session AFP/Tree-Automata (AFP) Session AFP/Datatype_Order_Generator (AFP) Session AFP/Higher_Order_Terms (AFP) Session AFP/CakeML_Codegen (AFP) Session AFP/Old_Datatype_Show (AFP) Session AFP/Quantifier_Elimination_Hybrid (AFP) Session AFP/WOOT_Strong_Eventual_Consistency (AFP) Session AFP/FSM_Tests (AFP) Session AFP/Iptables_Semantics (AFP) Session AFP/Iptables_Semantics_Examples (AFP) Session AFP/LOFT (AFP) Session AFP/Mersenne_Primes (AFP) Session AFP/MiniSail (AFP) Session AFP/Separation_Logic_Imperative_HOL (AFP) Session AFP/Sepref_Prereq (AFP) Session AFP/ROBDD (AFP) Session AFP/Refine_Imperative_HOL (AFP) Session AFP/BTree (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/Probabilistic_While (AFP) Session AFP/CryptHOL (AFP) Session AFP/Constructive_Cryptography (AFP) Session AFP/Game_Based_Crypto (AFP) Session AFP/Multi_Party_Computation (AFP) Session AFP/Sigma_Commit_Crypto (AFP) Session AFP/Constructive_Cryptography_CM (AFP) Session AFP/Prpu_Maxflow (AFP) Session AFP/Knuth_Morris_Pratt (AFP) Session AFP/Kruskal (AFP) Session AFP/PAC_Checker (AFP) Session AFP/VerifyThis2018 (AFP) Session AFP/VerifyThis2019 (AFP) Session AFP/Simplicial_complexes_and_boolean_functions (AFP) Session AFP/UpDown_Scheme (AFP) Session AFP/WebAssembly (AFP) Session AFP/SPARCv8 (AFP) Session AFP/X86_Semantics (AFP) Session AFP/ZFC_in_HOL (AFP) Session AFP/CZH_Foundations (AFP) Session AFP/CZH_Elementary_Categories (AFP) Session AFP/CZH_Universal_Constructions (AFP) Session AFP/Category3 (AFP) Session AFP/MonoidalCategory (AFP) Session AFP/Ordinal_Partitions (AFP) Session AFP/Wetzels_Problem (AFP) Session FOL/ZF (main timing) Session Doc/Logics_ZF (doc) Session AFP/Recursion-Addition (AFP) Session FOL/ZF-AC Session FOL/ZF-Coind Session FOL/ZF-Constructible Session AFP/Delta_System_Lemma (AFP) Session AFP/Transitive_Models (AFP) Session AFP/Independence_CH (AFP) Session AFP/Forcing (AFP) Session FOL/ZF-IMP Session FOL/ZF-Induct Session FOL/ZF-UNITY (timing) Session FOL/ZF-Resid Session FOL/ZF-ex Building ZFC_in_HOL ... Running Cook_Levin ... Running Quantifier_Elimination_Hybrid ... Running Virtual_Substitution ... Building Category3 ... Running Ordinal_Partitions ... Running Wetzels_Problem ... ZFC_in_HOL: theory HOL-Cardinals.Order_Union ZFC_in_HOL: theory HOL-Cardinals.Fun_More ZFC_in_HOL: theory HOL-Cardinals.Order_Relation_More ZFC_in_HOL: theory HOL-Library.Nat_Bijection ZFC_in_HOL: theory HOL-Library.FuncSet ZFC_in_HOL: theory HOL-Library.Infinite_Set ZFC_in_HOL: theory HOL-Library.Old_Datatype ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Extension ZFC_in_HOL: theory HOL-Cardinals.Wellfounded_More Ordinal_Partitions: theory HOL-Cardinals.Fun_More Ordinal_Partitions: theory HOL-Library.FuncSet Ordinal_Partitions: theory HOL-Cardinals.Order_Relation_More Ordinal_Partitions: theory HOL-Cardinals.Order_Union Ordinal_Partitions: theory HOL-Library.Infinite_Set Ordinal_Partitions: theory HOL-Library.Nat_Bijection Ordinal_Partitions: theory HOL-Library.Product_Lexorder Ordinal_Partitions: theory HOL-Library.Old_Datatype ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Relation Category3: theory Category3.Category Category3: theory HOL-Cardinals.Fun_More Category3: theory HOL-Cardinals.Order_Relation_More Category3: theory HOL-Cardinals.Order_Union Category3: theory HereditarilyFinite.HF Cook_Levin: theory HOL-Eisbach.Eisbach Cook_Levin: theory Cook_Levin.Basics Ordinal_Partitions: theory HOL-Cardinals.Wellorder_Extension Category3: theory HOL-Cardinals.Wellorder_Extension Wetzels_Problem: theory HOL-Cardinals.Order_Union Wetzels_Problem: theory HOL-Cardinals.Order_Relation_More Wetzels_Problem: theory HOL-Cardinals.Fun_More Wetzels_Problem: theory HOL-Library.Equipollence ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Embedding ZFC_in_HOL: theory HOL-Library.Countable Category3: theory HOL-Cardinals.Wellfounded_More ZFC_in_HOL: theory HOL-Library.Equipollence Wetzels_Problem: theory HOL-Cardinals.Wellorder_Extension Category3: theory HOL-Cardinals.Wellorder_Relation Category3: theory Category3.ConcreteCategory Ordinal_Partitions: theory HOL-Cardinals.Wellfounded_More Category3: theory Category3.DiscreteCategory Virtual_Substitution: theory Deriving.Generator_Aux Virtual_Substitution: theory Deriving.Derive_Manager Virtual_Substitution: theory HOL-Library.Code_Abstract_Nat Virtual_Substitution: theory HOL-Library.AList Virtual_Substitution: theory HOL-Library.Code_Target_Int Virtual_Substitution: theory HOL-Library.Conditional_Parametricity Virtual_Substitution: theory HOL-Library.Function_Algebras Virtual_Substitution: theory HOL-Library.Fun_Lexorder Ordinal_Partitions: theory HOL-Cardinals.Wellorder_Relation Category3: theory Category3.DualCategory Category3: theory Category3.EpiMonoIso Category3: theory HOL-Cardinals.Wellorder_Embedding ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Constructions Virtual_Substitution: theory HOL-Library.Groups_Big_Fun Virtual_Substitution: theory Abstract-Rewriting.Seq Wetzels_Problem: theory HOL-Cardinals.Wellfounded_More Wetzels_Problem: theory HOL-Cardinals.Wellorder_Relation Virtual_Substitution: theory HOL-Library.Code_Target_Nat Virtual_Substitution: theory HOL-Library.Ramsey Category3: theory HOL-Cardinals.Wellorder_Constructions Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Derive_Aux Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type Quantifier_Elimination_Hybrid: theory Polynomials.More_Modules Quantifier_Elimination_Hybrid: theory HOL-Analysis.Poly_Roots Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Vieta Quantifier_Elimination_Hybrid: theory Sturm_Tarski.PolyMisc Quantifier_Elimination_Hybrid: theory Open_Induction.Restricted_Predicates Quantifier_Elimination_Hybrid: theory Polynomials.Polynomials Category3: theory Category3.InitialTerminal Category3: theory Category3.ProductCategory Wetzels_Problem: theory HOL-Cardinals.Wellorder_Embedding Ordinal_Partitions: theory HOL-Cardinals.Wellorder_Embedding Virtual_Substitution: theory HOL-Library.More_List Wetzels_Problem: theory HOL-Cardinals.Wellorder_Constructions Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.More_Matrix Ordinal_Partitions: theory HOL-Library.Countable Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Sturm_Tarski Ordinal_Partitions: theory HOL-Library.Equipollence Ordinal_Partitions: theory HOL-Library.Ramsey Virtual_Substitution: theory HOL-Library.Sublist Ordinal_Partitions: theory HOL-Cardinals.Wellorder_Constructions Virtual_Substitution: theory HOL-Library.While_Combinator Quantifier_Elimination_Hybrid: theory Datatype_Order_Generator.Order_Generator ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Order_Relation Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Infinite_Sequences ZFC_in_HOL: theory HOL-Cardinals.Ordinal_Arithmetic Category3: theory HOL-Cardinals.Cardinal_Order_Relation Category3: theory HOL-Cardinals.Ordinal_Arithmetic Wetzels_Problem: theory HOL-Cardinals.Cardinal_Order_Relation Wetzels_Problem: theory HOL-Cardinals.Ordinal_Arithmetic Virtual_Substitution: theory HOL-Library.FSet Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Least_Enum Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Elements Virtual_Substitution: theory Polynomials.More_Modules Virtual_Substitution: theory HOL-Library.Poly_Mapping ZFC_in_HOL: theory HOL-Library.Countable_Set Cook_Levin: theory Cook_Levin.Combinations Virtual_Substitution: theory HOL-Computational_Algebra.Polynomial Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full Category3: theory Category3.FreeCategory Quantifier_Elimination_Hybrid: theory Polynomials.More_MPoly_Type Ordinal_Partitions: theory HOL-Cardinals.Cardinal_Order_Relation Ordinal_Partitions: theory HOL-Cardinals.Ordinal_Arithmetic Virtual_Substitution: theory HOL-Library.Quadratic_Discriminant Virtual_Substitution: theory Matrix.Utility Wetzels_Problem: theory HOL-Cardinals.Cardinal_Arithmetic ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Arithmetic Category3: theory HOL-Cardinals.Cardinal_Arithmetic Category3: theory Category3.Functor Virtual_Substitution: theory Open_Induction.Restricted_Predicates Virtual_Substitution: theory Regular-Sets.Regular_Set Quantifier_Elimination_Hybrid: theory Polynomials.Poly_Mapping_Finite_Map Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Univariate ZFC_in_HOL: theory HOL-Analysis.Continuum_Not_Denumerable Wetzels_Problem: theory HOL-Cardinals.Cardinals Cook_Levin: theory Cook_Levin.Elementary Wetzels_Problem: theory ZFC_in_HOL.ZFC_Library Category3: theory HOL-Cardinals.Cardinals Wetzels_Problem: theory ZFC_in_HOL.ZFC_in_HOL Virtual_Substitution: theory Show.Show Ordinal_Partitions: theory HOL-Library.Countable_Set Category3: theory ZFC_in_HOL.ZFC_Library ZFC_in_HOL: theory HOL-Cardinals.Cardinals Virtual_Substitution: theory Well_Quasi_Orders.Infinite_Sequences ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Library Category3: theory ZFC_in_HOL.ZFC_in_HOL Quantifier_Elimination_Hybrid: theory Symmetric_Polynomials.Symmetric_Polynomials ZFC_in_HOL: theory ZFC_in_HOL.ZFC_in_HOL Quantifier_Elimination_Hybrid: theory Sturm_Tarski.Pseudo_Remainder_Sequence Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Elements Virtual_Substitution: theory Well_Quasi_Orders.Least_Enum Wetzels_Problem: theory ZFC_in_HOL.ZFC_Cardinals Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Minimal_Bad_Sequences Ordinal_Partitions: theory HOL-Cardinals.Cardinal_Arithmetic Category3: theory ZFC_in_HOL.ZFC_Cardinals Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Almost_Full_Relations ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Cardinals Ordinal_Partitions: theory Nash_Williams.Nash_Extras Ordinal_Partitions: theory HOL-Cardinals.Cardinals Ordinal_Partitions: theory ZFC_in_HOL.ZFC_Library Ordinal_Partitions: theory Nash_Williams.Nash_Williams Wetzels_Problem: theory ZFC_in_HOL.ZFC_Typeclasses Quantifier_Elimination_Hybrid: theory Polynomials.Utils Quantifier_Elimination_Hybrid: theory Well_Quasi_Orders.Well_Quasi_Orders Ordinal_Partitions: theory ZFC_in_HOL.ZFC_in_HOL Virtual_Substitution: theory Polynomials.MPoly_Type Virtual_Substitution: theory Show.Show_Instances Virtual_Substitution: theory Show.Show_Real Wetzels_Problem: theory ZFC_in_HOL.General_Cardinals Wetzels_Problem: theory Wetzels_Problem.Wetzels_Problem Category3: theory Category3.NaturalTransformation Category3: theory Category3.Subcategory Cook_Levin: theory Cook_Levin.Composing Cook_Levin: theory Cook_Levin.Memorizing Ordinal_Partitions: theory ZFC_in_HOL.ZFC_Cardinals ZFC_in_HOL: theory ZFC_in_HOL.Kirby ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Typeclasses Quantifier_Elimination_Hybrid: theory Polynomials.Power_Products Category3: theory Category3.BinaryFunctor Category3: theory Category3.SetCategory Virtual_Substitution: theory Polynomials.More_MPoly_Type Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Algorithm ZFC_in_HOL: theory ZFC_in_HOL.Ordinal_Exp ZFC_in_HOL: theory ZFC_in_HOL.Cantor_NF Ordinal_Partitions: theory ZFC_in_HOL.Kirby Ordinal_Partitions: theory ZFC_in_HOL.ZFC_Typeclasses Cook_Levin: theory Cook_Levin.Arithmetic Cook_Levin: theory Cook_Levin.Oblivious Quantifier_Elimination_Hybrid: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library ZFC_in_HOL: theory ZFC_in_HOL.General_Cardinals Ordinal_Partitions: theory ZFC_in_HOL.Ordinal_Exp Wetzels_Problem FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9_x86_64_32-linux/log/Wetzels_Problem) *** Undefined fact: "Cantors_paradox" (line 224 of "$AFP/ZFC_in_HOL/ZFC_in_HOL.thy") *** At command "by" (line 224 of "$AFP/ZFC_in_HOL/ZFC_in_HOL.thy") Ordinal_Partitions: theory Ordinal_Partitions.Library_Additions Ordinal_Partitions: theory ZFC_in_HOL.Cantor_NF Category3: theory Category3.FunctorCategory Ordinal_Partitions: theory Ordinal_Partitions.Partitions Virtual_Substitution: theory HOL-Library.Finite_Map Ordinal_Partitions: theory Ordinal_Partitions.Erdos_Milner Category3: theory Category3.SetCat Ordinal_Partitions: theory Ordinal_Partitions.Omega_Omega Quantifier_Elimination_Hybrid: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Matrix_Equation_Construction Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Algorithm Quantifier_Elimination_Hybrid: theory Polynomials.Show_Polynomials Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Proofs Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Proofs Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.BKR_Decision Cook_Levin: theory Cook_Levin.Oblivious_Polynomial Virtual_Substitution: theory Polynomials.MPoly_Type_Univariate Cook_Levin: theory Cook_Levin.Lists_Lists Category3: theory Category3.Yoneda ZFC_in_HOL FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9_x86_64_32-linux/log/ZFC_in_HOL) *** Undefined fact: "Cantors_paradox" (line 224 of "$AFP/ZFC_in_HOL/ZFC_in_HOL.thy") *** At command "by" (line 224 of "$AFP/ZFC_in_HOL/ZFC_in_HOL.thy") CZH_Foundations CANCELLED CZH_Elementary_Categories CANCELLED CZH_Universal_Constructions CANCELLED Cook_Levin: theory Cook_Levin.Two_Four_Symbols Quantifier_Elimination_Hybrid: theory BenOr_Kozen_Reif.Renegar_Decision Virtual_Substitution: theory Regular-Sets.Regular_Exp Cook_Levin: theory Cook_Levin.Symbol_Ops Virtual_Substitution: theory Regular-Sets.NDerivative Virtual_Substitution: theory Regular-Sets.Relation_Interpretation Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Renegar_Modified Virtual_Substitution: theory Regular-Sets.Equivalence_Checking Virtual_Substitution: theory Regular-Sets.Regexp_Method Virtual_Substitution: theory Abstract-Rewriting.Abstract_Rewriting Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full Category3: theory Category3.Adjunction Cook_Levin: theory Cook_Levin.Wellformed Cook_Levin: theory Cook_Levin.NP Quantifier_Elimination_Hybrid: theory Factor_Algebraic_Polynomial.Poly_Connection Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_Ordered Cook_Levin: theory Cook_Levin.Oblivious_2_Tape Ordinal_Partitions FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9_x86_64_32-linux/log/Ordinal_Partitions) *** Undefined fact: "Cantors_paradox" (line 224 of "$AFP/ZFC_in_HOL/ZFC_in_HOL.thy") *** At command "by" (line 224 of "$AFP/ZFC_in_HOL/ZFC_in_HOL.thy") Cook_Levin: theory Cook_Levin.Satisfiability Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Bad_Sequences Virtual_Substitution: theory Abstract-Rewriting.SN_Orders Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full_Relations Virtual_Substitution: theory Polynomials.Utils Virtual_Substitution: theory Well_Quasi_Orders.Well_Quasi_Orders Virtual_Substitution: theory Polynomials.Power_Products Quantifier_Elimination_Hybrid: theory Polynomials.MPoly_Type_Class_FMap Quantifier_Elimination_Hybrid: theory Virtual_Substitution.MPolyExtension Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExecutiblePolyProps Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PolyAtoms Virtual_Substitution: theory Polynomials.Polynomials Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Debruijn Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Optimizations Quantifier_Elimination_Hybrid: theory Virtual_Substitution.OptimizationProofs Category3: theory Category3.EquivalenceOfCategories Category3: theory Category3.Limit Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Reindex Quantifier_Elimination_Hybrid: theory Virtual_Substitution.UniAtoms Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSAlgos Virtual_Substitution: theory Polynomials.Poly_Mapping_Finite_Map Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNF Virtual_Substitution: theory Polynomials.Show_Polynomials Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Heuristic Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LinearCase Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinity Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QuadraticCase Quantifier_Elimination_Hybrid: theory Virtual_Substitution.QE Quantifier_Elimination_Hybrid: theory Virtual_Substitution.PrettyPrinting Virtual_Substitution: theory Polynomials.MPoly_Type_Class Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EliminateVariable Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Infinitesimals Quantifier_Elimination_Hybrid: theory Virtual_Substitution.LuckyFind Quantifier_Elimination_Hybrid: theory Virtual_Substitution.EqualityVS Virtual_Substitution: theory Polynomials.MPoly_Type_Class_Ordered Virtual_Substitution: theory Polynomials.MPoly_Type_Class_FMap Cook_Levin: theory Cook_Levin.Reducing Quantifier_Elimination_Hybrid: theory Virtual_Substitution.Exports Virtual_Substitution: theory Virtual_Substitution.MPolyExtension Virtual_Substitution: theory Virtual_Substitution.ExecutiblePolyProps Cook_Levin: theory Cook_Levin.Aux_TM_Reducing Quantifier_Elimination_Hybrid: theory Virtual_Substitution.NegInfinityUni Virtual_Substitution: theory Virtual_Substitution.PolyAtoms Quantifier_Elimination_Hybrid: theory Virtual_Substitution.InfinitesimalsUni Quantifier_Elimination_Hybrid: theory Virtual_Substitution.DNFUni Quantifier_Elimination_Hybrid: theory Virtual_Substitution.GeneralVSProofs Quantifier_Elimination_Hybrid: theory Virtual_Substitution.VSQuad Cook_Levin: theory Cook_Levin.Sat_TM_CNF Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Poly_Props Quantifier_Elimination_Hybrid: theory Virtual_Substitution.HeuristicProofs Virtual_Substitution: theory Virtual_Substitution.Debruijn Quantifier_Elimination_Hybrid: theory Virtual_Substitution.ExportProofs Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Consistent_Sign_Assignments Virtual_Substitution: theory Virtual_Substitution.Optimizations Virtual_Substitution: theory Virtual_Substitution.Reindex Virtual_Substitution: theory Virtual_Substitution.UniAtoms Virtual_Substitution: theory Virtual_Substitution.QE Virtual_Substitution: theory Virtual_Substitution.PrettyPrinting Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Pseudo_Remainder_Sequence Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Multiv_Tarski_Query Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm Cook_Levin: theory Cook_Levin.Reduction_TM Virtual_Substitution: theory Virtual_Substitution.OptimizationProofs Virtual_Substitution: theory Virtual_Substitution.VSAlgos Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix_Proofs Virtual_Substitution: theory Virtual_Substitution.DNF Virtual_Substitution: theory Virtual_Substitution.Heuristic Virtual_Substitution: theory Virtual_Substitution.LinearCase Virtual_Substitution: theory Virtual_Substitution.NegInfinity Virtual_Substitution: theory Virtual_Substitution.QuadraticCase Virtual_Substitution: theory Virtual_Substitution.EliminateVariable Virtual_Substitution: theory Virtual_Substitution.Infinitesimals Virtual_Substitution: theory Virtual_Substitution.NegInfinityUni Virtual_Substitution: theory Virtual_Substitution.LuckyFind Virtual_Substitution: theory Virtual_Substitution.EqualityVS Quantifier_Elimination_Hybrid: theory Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm_Proofs Virtual_Substitution: theory Virtual_Substitution.InfinitesimalsUni Virtual_Substitution: theory Virtual_Substitution.DNFUni Virtual_Substitution: theory Virtual_Substitution.GeneralVSProofs Virtual_Substitution: theory Virtual_Substitution.VSQuad Virtual_Substitution: theory Virtual_Substitution.Exports Virtual_Substitution: theory Virtual_Substitution.HeuristicProofs Category3: theory Category3.CategoryWithPullbacks Category3: theory Category3.ZFC_SetCat Virtual_Substitution: theory Virtual_Substitution.ExportProofs Category3: theory Category3.CartesianCategory Category3: theory Category3.CartesianClosedCategory Category3: theory Category3.CategoryWithFiniteLimits Category3: theory Category3.HFSetCat Category3 FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9_x86_64_32-linux/log/Category3) *** Undefined fact: "Cantors_paradox" (line 224 of "$AFP/ZFC_in_HOL/ZFC_in_HOL.thy") *** At command "by" (line 224 of "$AFP/ZFC_in_HOL/ZFC_in_HOL.thy") MonoidalCategory CANCELLED Preparing Quantifier_Elimination_Hybrid/document ... Preparing Virtual_Substitution/document ... Finished Quantifier_Elimination_Hybrid/document (0:00:18 elapsed time) Preparing Quantifier_Elimination_Hybrid/outline ... Finished Quantifier_Elimination_Hybrid/outline (0:00:06 elapsed time) Timing Quantifier_Elimination_Hybrid (8 threads, 395.415s elapsed time, 1830.408s cpu time, 139.447s GC time, factor 4.63) Finished Quantifier_Elimination_Hybrid (0:06:44 elapsed time, 0:30:39 cpu time, factor 4.55) Finished Virtual_Substitution/document (0:00:45 elapsed time) Preparing Virtual_Substitution/outline ... Finished Virtual_Substitution/outline (0:00:13 elapsed time) Timing Virtual_Substitution (8 threads, 407.860s elapsed time, 1417.557s cpu time, 159.953s GC time, factor 3.48) Finished Virtual_Substitution (0:06:51 elapsed time, 0:23:40 cpu time, factor 3.45) Preparing Cook_Levin/document ... Finished Cook_Levin/document (0:01:21 elapsed time) Preparing Cook_Levin/outline ... Finished Cook_Levin/outline (0:00:33 elapsed time) Timing Cook_Levin (8 threads, 670.144s elapsed time, 3458.837s cpu time, 105.581s GC time, factor 5.16) Finished Cook_Levin (0:11:13 elapsed time, 0:57:42 cpu time, factor 5.14) Presentation in "/media/data/jenkins/workspace/isabelle-all/browser_info" Presenting Cook_Levin in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cook_Levin" ... Presenting Virtual_Substitution in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Virtual_Substitution" ... Presenting Quantifier_Elimination_Hybrid in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quantifier_Elimination_Hybrid" ... Presenting document Cook_Levin/document Presenting document Cook_Levin/outline Presenting document Virtual_Substitution/document Presenting document Virtual_Substitution/outline Presenting document Quantifier_Elimination_Hybrid/document Presenting document Quantifier_Elimination_Hybrid/outline Presenting theory "HOL-Library.Groups_Big_Fun" Presenting theory "Polynomials.MPoly_Type" Presenting theory "HOL-Library.Fun_Lexorder" Presenting theory "HOL-Library.More_List" Presenting theory "Polynomials.More_MPoly_Type" Presenting theory "Polynomials.MPoly_Type_Univariate" Presenting theory "Symmetric_Polynomials.Vieta" Presenting theory "Cook_Levin.Basics" Presenting theory "HOL-Library.Poly_Mapping" Presenting theory "Polynomials.MPoly_Type" Presenting theory "Symmetric_Polynomials.Symmetric_Polynomials" Presenting theory "Polynomials.More_MPoly_Type" Presenting theory "HOL-Eisbach.Eisbach" Presenting file "~~/src/HOL/Eisbach/parse_tools.ML" Presenting file "~~/src/HOL/Eisbach/method_closure.ML" Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML" Presenting file "~~/src/HOL/Eisbach/match_method.ML" Presenting theory "Power_Sum_Polynomials.Power_Sum_Polynomials_Library" Presenting theory "Hermite_Lindemann.More_Multivariate_Polynomial_HLW" Presenting theory "Well_Quasi_Orders.Least_Enum" Presenting theory "Well_Quasi_Orders.Infinite_Sequences" Presenting theory "Cook_Levin.Combinations" Presenting theory "Open_Induction.Restricted_Predicates" Presenting theory "Well_Quasi_Orders.Almost_Full" Presenting theory "Well_Quasi_Orders.Minimal_Elements" Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences" Presenting theory "Well_Quasi_Orders.Almost_Full_Relations" Presenting theory "HOL-Computational_Algebra.Polynomial" Presenting theory "Polynomials.Utils" Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders" Presenting theory "Cook_Levin.Elementary" Presenting theory "Polynomials.Power_Products" Presenting theory "Polynomials.MPoly_Type_Univariate" Presenting theory "Regular-Sets.Regular_Set" Presenting theory "Polynomials.More_Modules" Presenting theory "Regular-Sets.Regular_Exp" Presenting theory "Cook_Levin.Memorizing" Presenting theory "Regular-Sets.NDerivative" Presenting theory "HOL-Library.While_Combinator" Presenting theory "Regular-Sets.Equivalence_Checking" Presenting theory "Regular-Sets.Relation_Interpretation" Presenting theory "Regular-Sets.Regexp_Method" Presenting theory "Cook_Levin.Composing" Presenting theory "Polynomials.MPoly_Type_Class" Presenting theory "Abstract-Rewriting.Seq" Presenting theory "Factor_Algebraic_Polynomial.Poly_Connection" Presenting theory "Abstract-Rewriting.Abstract_Rewriting" Presenting theory "Polynomials.Polynomials" Presenting theory "Abstract-Rewriting.SN_Orders" Presenting theory "Matrix.Utility" Presenting theory "Cook_Levin.Arithmetic" Presenting theory "Polynomials.Polynomials" Presenting theory "Polynomials.MPoly_Type_Class_Ordered" Presenting theory "HOL-Library.Sublist" Presenting theory "Polynomials.Poly_Mapping_Finite_Map" Presenting theory "Polynomials.MPoly_Type_Class_FMap" Presenting theory "Virtual_Substitution.MPolyExtension" Presenting theory "HOL-Library.Ramsey" Presenting theory "Well_Quasi_Orders.Least_Enum" Presenting theory "Well_Quasi_Orders.Infinite_Sequences" Presenting theory "Virtual_Substitution.ExecutiblePolyProps" Presenting theory "Open_Induction.Restricted_Predicates" Presenting theory "Sturm_Tarski.PolyMisc" Presenting theory "Well_Quasi_Orders.Almost_Full" Presenting theory "Cook_Levin.Lists_Lists" Presenting theory "Well_Quasi_Orders.Minimal_Elements" Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences" Presenting theory "Well_Quasi_Orders.Almost_Full_Relations" Presenting theory "Polynomials.Utils" Presenting theory "Sturm_Tarski.Sturm_Tarski" Presenting theory "HOL-Library.Function_Algebras" Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders" Presenting theory "Cook_Levin.Two_Four_Symbols" Presenting theory "Sturm_Tarski.Pseudo_Remainder_Sequence" Presenting theory "Virtual_Substitution.PolyAtoms" Presenting theory "Polynomials.Power_Products" Presenting theory "Virtual_Substitution.Debruijn" Presenting theory "Polynomials.More_Modules" Presenting theory "Cook_Levin.Symbol_Ops" Presenting theory "Virtual_Substitution.Optimizations" Presenting theory "Virtual_Substitution.VSAlgos" Presenting theory "Polynomials.MPoly_Type_Class" Presenting theory "Virtual_Substitution.LinearCase" Presenting theory "Cook_Levin.Wellformed" Presenting theory "Cook_Levin.NP" Presenting theory "Virtual_Substitution.QuadraticCase" Presenting theory "Virtual_Substitution.EliminateVariable" Presenting theory "Polynomials.MPoly_Type_Class_Ordered" Presenting theory "Virtual_Substitution.LuckyFind" Presenting theory "Virtual_Substitution.EqualityVS" Presenting theory "Cook_Levin.Satisfiability" Presenting theory "HOL-Library.FSet" Presenting theory "HOL-Library.AList" Presenting theory "HOL-Library.Conditional_Parametricity" Presenting file "~~/src/HOL/Library/conditional_parametricity.ML" Presenting theory "Cook_Levin.Oblivious" Presenting theory "HOL-Library.Finite_Map" Presenting theory "Polynomials.Poly_Mapping_Finite_Map" Presenting theory "Polynomials.MPoly_Type_Class_FMap" Presenting theory "Cook_Levin.Oblivious_Polynomial" Presenting theory "HOL-Library.Quadratic_Discriminant" Presenting theory "Virtual_Substitution.QE" Presenting theory "Cook_Levin.Oblivious_2_Tape" Presenting theory "Virtual_Substitution.QE" Presenting theory "HOL-Analysis.Poly_Roots" Presenting theory "Virtual_Substitution.NegInfinity" Presenting theory "Virtual_Substitution.Infinitesimals" Presenting theory "Virtual_Substitution.UniAtoms" Presenting theory "Cook_Levin.Reducing" Presenting theory "Virtual_Substitution.NegInfinityUni" Presenting theory "Virtual_Substitution.InfinitesimalsUni" Presenting theory "Virtual_Substitution.DNFUni" Presenting theory "Virtual_Substitution.MPolyExtension" Presenting theory "Cook_Levin.Aux_TM_Reducing" Presenting theory "Virtual_Substitution.ExecutiblePolyProps" Presenting theory "Virtual_Substitution.GeneralVSProofs" Presenting theory "Virtual_Substitution.PolyAtoms" Presenting theory "Virtual_Substitution.Debruijn" Presenting theory "Virtual_Substitution.Reindex" Presenting theory "Virtual_Substitution.Reindex" Presenting theory "Virtual_Substitution.OptimizationProofs" Presenting theory "Virtual_Substitution.Optimizations" Presenting theory "Virtual_Substitution.OptimizationProofs" Presenting theory "Virtual_Substitution.DNF" Presenting theory "Virtual_Substitution.VSQuad" Presenting theory "Virtual_Substitution.VSAlgos" Presenting theory "Virtual_Substitution.Heuristic" Presenting theory "HOL-Library.Code_Target_Int" Presenting theory "HOL-Library.Code_Abstract_Nat" Presenting theory "Quantifier_Elimination_Hybrid.Multiv_Poly_Props" Presenting theory "HOL-Library.Code_Target_Nat" Presenting theory "Deriving.Generator_Aux" Presenting file "$AFP/Deriving/bnf_access.ML" Presenting file "$AFP/Deriving/generator_aux.ML" Presenting theory "Deriving.Derive_Manager" Presenting file "$AFP/Deriving/derive_manager.ML" Presenting theory "Datatype_Order_Generator.Derive_Aux" Presenting file "$AFP/Datatype_Order_Generator/derive_aux.ML" Presenting theory "Cook_Levin.Sat_TM_CNF" Presenting theory "Datatype_Order_Generator.Order_Generator" Presenting theory "Show.Show" Presenting file "$AFP/Datatype_Order_Generator/order_generator.ML" Presenting file "$AFP/Show/show_generator.ML" Presenting theory "Show.Show_Instances" Presenting theory "Polynomials.Show_Polynomials" Presenting theory "Virtual_Substitution.PrettyPrinting" Presenting theory "Show.Show_Real" Presenting theory "Virtual_Substitution.Exports" Presenting theory "Quantifier_Elimination_Hybrid.Multiv_Consistent_Sign_Assignments" Presenting theory "Virtual_Substitution.LinearCase" Presenting theory "Quantifier_Elimination_Hybrid.Multiv_Pseudo_Remainder_Sequence" Presenting theory "Virtual_Substitution.QuadraticCase" Presenting theory "BenOr_Kozen_Reif.More_Matrix" Presenting theory "Virtual_Substitution.EliminateVariable" Presenting theory "Virtual_Substitution.LuckyFind" Presenting theory "BenOr_Kozen_Reif.BKR_Algorithm" Presenting theory "BenOr_Kozen_Reif.Renegar_Algorithm" Presenting theory "Virtual_Substitution.EqualityVS" Presenting theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix" Presenting theory "Virtual_Substitution.UniAtoms" Presenting theory "Virtual_Substitution.Heuristic" Presenting theory "Virtual_Substitution.NegInfinity" Presenting theory "Virtual_Substitution.NegInfinityUni" Presenting theory "Virtual_Substitution.HeuristicProofs" Presenting theory "Cook_Levin.Reduction_TM" Presenting theory "Polynomials.Show_Polynomials" Presenting theory "Virtual_Substitution.Infinitesimals" Presenting theory "Virtual_Substitution.PrettyPrinting" Presenting theory "Virtual_Substitution.Exports" Presenting theory "Virtual_Substitution.ExportProofs" Presenting theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm" Presenting theory "Virtual_Substitution.InfinitesimalsUni" Presenting theory "BenOr_Kozen_Reif.Matrix_Equation_Construction" Presenting theory "Virtual_Substitution.DNFUni" Presenting theory "Quantifier_Elimination_Hybrid.Multiv_Tarski_Query" Presenting theory "Virtual_Substitution.GeneralVSProofs" Presenting theory "Virtual_Substitution.DNF" Presenting theory "BenOr_Kozen_Reif.BKR_Proofs" Presenting theory "Virtual_Substitution.VSQuad" Presenting theory "Virtual_Substitution.HeuristicProofs" Presenting theory "Virtual_Substitution.ExportProofs" Presenting theory "BenOr_Kozen_Reif.Renegar_Proofs" Presenting theory "BenOr_Kozen_Reif.BKR_Decision" Presenting theory "BenOr_Kozen_Reif.Renegar_Decision" Presenting theory "Quantifier_Elimination_Hybrid.Renegar_Modified" Presenting theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix_Proofs" Presenting theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm_Proofs" Unfinished session(s): CZH_Elementary_Categories, CZH_Foundations, CZH_Universal_Constructions, Category3, MonoidalCategory, Ordinal_Partitions, Wetzels_Problem, ZFC_in_HOL === TIMING === Group AFP: 0:34:18 elapsed time, 2:33:16 cpu time, factor 4.47 Group main: 0:00:00 elapsed time Group large: 0:00:00 elapsed time Group no_doc: 0:00:00 elapsed time Group doc: 0:00:00 elapsed time Group timing: 0:00:00 elapsed time Overall: 0:15:23 elapsed time, 2:33:16 cpu time, factor 9.96 === FAILED SESSIONS === Session Category3: FAILED 1 Session CZH_Elementary_Categories: CANCELLED Session Ordinal_Partitions: FAILED 1 Session MonoidalCategory: CANCELLED Session CZH_Universal_Constructions: CANCELLED Session Wetzels_Problem: FAILED 1 Session CZH_Foundations: CANCELLED Session ZFC_in_HOL: FAILED 1 === DEPENDENCIES === Generating dependencies file ... Writing dependencies file ... === REPORT === Writing report file ... === SITEGEN === Writing status file ... Running sitegen ... using [/media/data/jenkins/workspace/isabelle-all/bin/isabelle] Preparing site generation in out/hugo Cleaning up generated files... Preparing topics... Preparing licenses... Preparing releases... Preparing authors... Extracting keywords... Preparing entries... Preparing statistics... Preparing project files Preparing devel version... Finished sitegen preparation. Cleaning output dir... Building site... Build in /media/data/jenkins/workspace/isabelle-all/afp/web/index.html Packing tars ... === NOTIFICATIONS === === COMPLETED === Build step 'Execute shell' marked build as failure 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