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