[EnvInject] - Loading node environment variables.
workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-all Building remotely on
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
http://isabelle.in.tum.de/repos/isabelle/ pulling from
https://isabelle.in.tum.de/repos/isabelle/ real URL is
[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 1cadc477f644c89c0fae513f51ff81f4af684c1d --template exists\n
[isabelle-all] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(1cadc477f644c89c0fae513f51ff81f4af684c1d)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
https://foss.heptapod.net/isa-afp/afp-devel/ pulling from
[afp] $ hg update --clean --rev default
2007 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 a0663cd726cc06543f9689efe66c628dfdb6af7e --template exists\n
[afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(a0663cd726cc06543f9689efe66c628dfdb6af7e)" --encoding UTF-8 --encodingmode replace
[isabelle-all] $ /bin/sh -xe /tmp/jenkins12050969793957505254.sh
### 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) ...
# 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:
[NOTE] Package zarith is already installed (current version is 1.12). 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
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-a5d5fba90286/x86_64_32-linux"
Session Doc/Sledgehammer (doc) Session AFP/Abortable_Linearizable_Modules (AFP) Session AFP/Abstract-Hoare-Logics (AFP) Session AFP/Ackermanns_not_PR (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/Boolos_Curious_Inference (AFP) Session AFP/Boolos_Curious_Inference_Automated (AFP) Session AFP/BytecodeLogicJmlTypes (AFP) Session AFP/C2KA_DistributedSystems (AFP) Session AFP/Sqrt_Babylonian (AFP) Session AFP/ClockSynchInst (AFP) Session AFP/Compiling-Exceptions-Correctly (AFP) Session AFP/ComponentDependencies (AFP) Session AFP/Concurrent_Revisions (AFP) Session AFP/Constructor_Funs (AFP) Session AFP/CryptoBasedCompositionalProperties (AFP) Session AFP/DPT-SAT-Solver (AFP) Session AFP/Dedekind_Real (AFP) Session Doc/Demo_Easychair (doc) Session Doc/Demo_FoilTeX (doc) Session AFP/Depth-First-Search (AFP) Session AFP/Digit_Expansions (AFP) Session AFP/Diophantine_Eqns_Lin_Hom (AFP) Session AFP/Example-Submission (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 AFP/GPU_Kernel_PL (AFP) Session AFP/General-Triangle (AFP) Session AFP/Generic_Deriving (AFP) Session AFP/GewirthPGCProof (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_Parallel (timing) Session HOL/HOL-Library (main timing) Session AFP/Approximation_Algorithms (AFP) Session AFP/ArrowImpossibilityGS (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/Card_Multisets (AFP) Session AFP/Card_Number_Partitions (AFP) Session AFP/Complete_Non_Orders (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/DOM_Components (AFP) Session AFP/Shadow_SC_DOM (AFP) Session AFP/SC_DOM_Components (AFP) Session AFP/Decl_Sem_Fun_PL (AFP) Session AFP/Encodability_Process_Calculi (AFP) Session AFP/Euler_Partition (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/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 HOL/HOL-UNITY (timing) Session HOL/HOL-Combinatorics (main timing) 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/Edwards_Elliptic_Curves_Group (AFP) 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 HOL/HOL-Analysis (main timing) Session AFP/Actuarial_Mathematics (AFP) Session AFP/Cayley_Hamilton (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/Complex_Geometry (AFP) Session AFP/Poincare_Disc (AFP) Session AFP/Differential_Game_Logic (AFP) Session AFP/First_Welfare_Theorem (AFP) Session HOL/HOL-Complex_Analysis (main timing) 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/Combinatorics_Words (AFP) Session AFP/Combinatorics_Words_Graph_Lemma (AFP) Session AFP/Binary_Code_Imprimitive (AFP) Session AFP/Two_Generated_Word_Monoids_Intersection (AFP) Session AFP/Dependent_SIFUM_Type_Systems (AFP) Session AFP/Dependent_SIFUM_Refinement (AFP) 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/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/Source_Coding_Theorem (AFP) Session AFP/Turans_Graph_Theorem (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/Ptolemys_Theorem (AFP) Session AFP/Rank_Nullity_Theorem (AFP) Session AFP/Gauss_Jordan (AFP) Session AFP/Echelon_Form (AFP) Session AFP/Tarskis_Geometry (AFP) Session AFP/Chord_Segments (AFP) Session AFP/Stewart_Apollonius (AFP) Session AFP/Youngs_Inequality (AFP) 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/DigitsInBase (AFP) Session AFP/E_Transcendental (AFP) Session AFP/Elliptic_Curves_Group_Law (AFP) Session HOL/HOL-Data_Structures (timing) Session AFP/Efficient-Mergesort (AFP) Session HOL/HOL-Codegenerator_Test Session AFP/Query_Optimization (AFP) Session AFP/Automatic_Refinement (AFP) Session AFP/Refine_Monadic (AFP) Session AFP/Lifting_the_Exponent (AFP) Session AFP/Pratt_Certificate (AFP) Session AFP/Bertrands_Postulate (AFP) Session AFP/Prime_Harmonic_Series (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 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-Metis_Examples (timing) Session HOL/HOL-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-Lambda (timing) Session AFP/Applicative_Lifting (AFP) Session AFP/Stern_Brocot (AFP) Session AFP/HereditarilyFinite (AFP) Session AFP/Isabelle_Meta_Model (AFP) Session AFP/Stuttering_Equivalence (AFP) Session AFP/Landau_Symbols (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/Order_Lattice_Props (AFP) Session AFP/POPLmark-deBruijn (AFP) Session AFP/Pairing_Heap (AFP) Session AFP/Password_Authentication_Protocol (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_Tensor (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/Schutz_Spacetime (AFP) Session AFP/Selection_Heap_Sort (AFP) Session AFP/Sort_Encodings (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/Szemeredi_Regularity (AFP) Session AFP/Roth_Arithmetic_Progressions (AFP) Session AFP/Tail_Recursive_Functions (AFP) Session AFP/TortoiseHare (AFP) Session AFP/Flyspeck-Tame (AFP) Session AFP/Twelvefold_Way (AFP) Session AFP/Vickrey_Clarke_Groves (AFP) Session HOL/HOL-MicroJava (timing) Session HOL/HOL-Nitpick_Examples Session HOL/HOL-Nominal-Examples (timing) Session AFP/Lam-ml-Normalization (AFP) Session AFP/SequentInvertibility (AFP) Session HOL/HOL-Predicate_Compile_Examples (timing) Session HOL/HOL-Quickcheck_Examples (timing) Session AFP/Cotangent_PFD_Formula (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 HOL/HOL-SET_Protocol (timing) Session HOL/HOL-SMT_Examples (timing) Session HOL/HOL-SPARK-Examples Session AFP/RIPEMD-160-SPARK (AFP) Session AFP/Banach_Steinhaus (AFP) Session AFP/Smooth_Manifolds (AFP) Session AFP/Types_To_Sets_Extension (AFP) Session HOL/HOLCF (main timing) Session AFP/HOLCF-Prelude (AFP) Session AFP/Stream-Fusion (AFP) Session AFP/WorkerWrapper (AFP) Session AFP/Hales_Jewett (AFP) Session AFP/Consensus_Refined (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/Hybrid_Logic (AFP) Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP) Session AFP/HyperHoareLogic (AFP) Session AFP/IFC_Tracking (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/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/Algebraic_VCs (AFP) Session AFP/Multirelations (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/LatticeProperties (AFP) Session AFP/DataRefinementIBP (AFP) Session AFP/GraphMarkingIBP (AFP) Session AFP/Lifting_Definition_Option (AFP) Session AFP/Comparison_Sort_Lower_Bound (AFP) Session AFP/Dominance_CHK (AFP) Session AFP/InformationFlowSlicing_Inter (AFP) Session AFP/InformationFlowSlicing (AFP) Session AFP/Regression_Test_Selection (AFP) Session AFP/Quick_Sort_Cost (AFP) Session AFP/Randomised_BSTs (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/Locally-Nameless-Sigma (AFP) Session AFP/Logging_Independent_Anonymity (AFP) Session AFP/Lowe_Ontological_Argument (AFP) Session AFP/MHComputation (AFP) Session AFP/MLSS_Decision_Proc (AFP) Session AFP/Latin_Square (AFP) Session AFP/Max-Card-Matching (AFP) Session AFP/Maximum_Segment_Sum (AFP) Session AFP/Median_Of_Medians_Selection (AFP) Session AFP/Metalogic_ProofChecker (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/Nash_Williams (AFP) Session AFP/No_FTL_observers (AFP) Session AFP/No_FTL_observers_Gen_Rel (AFP) Session AFP/Incompleteness (AFP) Session AFP/Surprise_Paradox (AFP) Session AFP/Modal_Logics_for_NTS (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/Open_Induction (AFP) Session AFP/Well_Quasi_Orders (AFP) Session AFP/Decreasing-Diagrams-II (AFP) Session AFP/Myhill-Nerode (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/PSemigroupsConvolution (AFP) Session AFP/Package_logic (AFP) Session AFP/Combinable_Wands (AFP) Session AFP/Paraconsistency (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 AFP/Projective_Geometry (AFP) Session AFP/Proof_Strategy_Language (AFP) Session AFP/Propositional_Logic_Class (AFP) Session AFP/Propositional_Proof_Systems (AFP) Session AFP/Ramsey-Infinite (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/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/Separation_Logic_Unbounded (AFP) Session AFP/SimplifiedOntologicalArgument (AFP) Session AFP/Sliding_Window_Algorithm (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 AFP/Clique_and_Monotone_Circuits (AFP) Session AFP/Suppes_Theorem (AFP) Session AFP/Probability_Inequality_Completeness (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/Combinatorics_Words_Lyndon (AFP) Session AFP/TESL_Language (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 AFP/Tree_Enumeration (AFP) Session Doc/Typeclass_Hierarchy (doc) Session AFP/Types_Tableaus_and_Goedels_God (AFP) Session AFP/UPF_Firewall (AFP) Session AFP/Universal_Turing_Machine (AFP) Session AFP/Van_der_Waerden (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/IEEE_Floating_Point (AFP) Session AFP/IP_Addresses (AFP) Session AFP/Simple_Firewall (AFP) Session AFP/Interval_Arithmetic_Word32 (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/CAVA_Automata (AFP) Session AFP/DFS_Framework (AFP) Session AFP/CHERI-C_Memory_Model (AFP) Session AFP/Collections_Examples (AFP) Session AFP/Containers-Benchmarks (AFP) Session AFP/MFOTL_Monitor (AFP) Session AFP/Generic_Join (AFP) Session AFP/MFODL_Monitor_Optimized (AFP) Session AFP/Formula_Derivatives (AFP) Session AFP/MSO_Regex_Equivalence (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/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/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/Three_Squares (AFP) Session AFP/Prime_Number_Theorem (AFP) Session AFP/Prime_Distribution_Elementary (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/Isabelle_Marries_Dirac (AFP) Session AFP/Knuth_Bendix_Order (AFP) Session AFP/Functional_Ordered_Resolution_Prover (AFP) Session AFP/Simple_Clause_Learning (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/Efficient_Weighted_Path_Order (AFP) Session AFP/Given_Clause_Loops (AFP) Session AFP/Multiset_Ordering_NPC (AFP) Session AFP/Linear_Recurrences (AFP) Session AFP/Perron_Frobenius (AFP) Session AFP/MDP-Algorithms (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/CVP_Hardness (AFP) Session AFP/LLL_Factorization (AFP) Session AFP/Linear_Inequalities (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/Deep_Learning (AFP) Session AFP/Projective_Measurements (AFP) Session AFP/Commuting_Hermitian (AFP) Session AFP/Expander_Graphs (AFP) Session AFP/Distributed_Distinct_Elements (AFP) Session AFP/TsirelsonBound (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/Schwartz_Zippel (AFP) Session AFP/Virtual_Substitution (AFP) Session AFP/Complex_Bounded_Operators (AFP) Session AFP/QR_Decomposition (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/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/CAVA_LTL_Modelchecker (AFP) Session AFP/Transitive-Closure (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/Iptables_Semantics (AFP) Session AFP/Iptables_Semantics_Examples (AFP) Session AFP/Mersenne_Primes (AFP) Session AFP/Separation_Logic_Imperative_HOL (AFP) Session AFP/Sepref_Prereq (AFP) Session AFP/Refine_Imperative_HOL (AFP) Session AFP/Floyd_Warshall (AFP) Session AFP/Sepref_Basic (AFP) Session AFP/Flow_Networks (AFP) Session AFP/EdmondsKarp_Maxflow (AFP) Session AFP/MFMC_Countable (AFP) Session AFP/Probabilistic_While (AFP) Session AFP/ABY3_Protocols (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/VerifyThis2018 (AFP) Session AFP/VerifyThis2019 (AFP) Session AFP/Simplicial_complexes_and_boolean_functions (AFP) Session AFP/UpDown_Scheme (AFP) Session AFP/X86_Semantics (AFP) Session AFP/CZH_Foundations (AFP) Session AFP/CZH_Elementary_Categories (AFP) Session AFP/CZH_Universal_Constructions (AFP) Session AFP/MonoidalCategory (AFP) Session AFP/Ordinal_Partitions (AFP) Session AFP/Wetzels_Problem (AFP) Session AFP/Recursion-Addition (AFP) Session AFP/Delta_System_Lemma (AFP) Session AFP/Transitive_Models (AFP) Session AFP/Independence_CH (AFP) Building Frequency_Moments on hpcisabelle/0 ... Building Suppes_Theorem on hpcisabelle/1 ... Building Commuting_Hermitian on hpcisabelle/2 ... Running Schwartz_Zippel on hpcisabelle/3 ... Running MLSS_Decision_Proc on hpcisabelle/4 ... Running ABY3_Protocols on hpcisabelle/5 ... Running Binary_Code_Imprimitive on hpcisabelle/6 ... Running CVP_Hardness on hpcisabelle/7 ... Suppes_Theorem: theory Propositional_Logic_Class.Implication_Logic Suppes_Theorem: theory HOL-Library.Cancellation Suppes_Theorem: theory HOL-Library.Old_Datatype Suppes_Theorem: theory HOL-Library.Nat_Bijection Suppes_Theorem: theory HOL-Combinatorics.Transposition Suppes_Theorem: theory HOL-Library.FuncSet Binary_Code_Imprimitive: theory Combinatorics_Words_Graph_Lemma.Glued_Codes Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Square_Interpretation MLSS_Decision_Proc: theory Graph_Theory.Rtrancl_On MLSS_Decision_Proc: theory Fresh_Identifiers.Fresh MLSS_Decision_Proc: theory HOL-Library.Adhoc_Overloading MLSS_Decision_Proc: theory HOL-Combinatorics.Transposition MLSS_Decision_Proc: theory HOL-Library.Cancellation MLSS_Decision_Proc: theory HOL-Library.Infinite_Set MLSS_Decision_Proc: theory HOL-Library.FuncSet MLSS_Decision_Proc: theory HOL-Library.Nat_Bijection Frequency_Moments: theory HOL-Eisbach.Eisbach Frequency_Moments: theory HOL-Combinatorics.Stirling Frequency_Moments: theory HOL-Library.Code_Abstract_Nat Frequency_Moments: theory HOL-Decision_Procs.Dense_Linear_Order Frequency_Moments: theory HOL-Number_Theory.Cong Frequency_Moments: theory HOL-Library.Code_Target_Int Frequency_Moments: theory HOL-Algebra.Congruence Frequency_Moments: theory Card_Partitions.Set_Partition Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian_Misc MLSS_Decision_Proc: theory HOL-Library.Old_Datatype Schwartz_Zippel: theory HOL-Computational_Algebra.Fraction_Field Schwartz_Zippel: theory HOL-Computational_Algebra.Nth_Powers Schwartz_Zippel: theory HOL-Computational_Algebra.Group_Closure Schwartz_Zippel: theory HOL-Computational_Algebra.Squarefree Schwartz_Zippel: theory HOL-Library.Fun_Lexorder Schwartz_Zippel: theory HOL-Algebra.Congruence Schwartz_Zippel: theory Jordan_Normal_Form.Missing_Misc Schwartz_Zippel: theory HOL-Library.Function_Algebras Suppes_Theorem: theory Propositional_Logic_Class.Classical_Logic ABY3_Protocols: theory ABY3_Protocols.Finite_Number_Type ABY3_Protocols: theory ABY3_Protocols.Spmf_Common Schwartz_Zippel: theory HOL-Library.Groups_Big_Fun Commuting_Hermitian: theory Commuting_Hermitian.Spectral_Theory_Complements CVP_Hardness: theory CVP_Hardness.Reduction CVP_Hardness: theory CVP_Hardness.Digits_int CVP_Hardness: theory Algebraic_Numbers.Bivariate_Polynomials CVP_Hardness: theory BenOr_Kozen_Reif.More_Matrix CVP_Hardness: theory CVP_Hardness.Partition CVP_Hardness: theory CVP_Hardness.Subset_Sum MLSS_Decision_Proc: theory HOL-Library.Rewrite ABY3_Protocols: theory ABY3_Protocols.Additive_Sharing MLSS_Decision_Proc: theory Fresh_Identifiers.Fresh_Nat MLSS_Decision_Proc: theory HOL-Library.Sublist Suppes_Theorem: theory HOL-Library.Disjoint_Sets Suppes_Theorem: theory HOL-Library.Countable Schwartz_Zippel: theory Abstract-Rewriting.Seq Frequency_Moments: theory HOL-Library.Code_Target_Nat Schwartz_Zippel: theory HOL-Library.Ramsey Suppes_Theorem: theory HOL-Library.Multiset Frequency_Moments: theory HOL-Combinatorics.List_Permutation Suppes_Theorem: theory Propositional_Logic_Class.Classical_Logic_Completeness ABY3_Protocols: theory ABY3_Protocols.Sharing_Lemmas Schwartz_Zippel: theory HOL-Library.More_List Schwartz_Zippel: theory HOL-Library.While_Combinator MLSS_Decision_Proc: theory HOL-Library.Liminf_Limsup ABY3_Protocols: theory ABY3_Protocols.Multiplication ABY3_Protocols: theory ABY3_Protocols.Shuffle MLSS_Decision_Proc: theory List-Index.List_Index Frequency_Moments: theory HOL-Library.Function_Algebras CVP_Hardness: theory Algebraic_Numbers.Resultant ABY3_Protocols: theory ABY3_Protocols.Multiplication_Synthesization Schwartz_Zippel: theory Polynomials.More_Modules MLSS_Decision_Proc: theory HereditarilyFinite.HF Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Code_Imprimitive Schwartz_Zippel: theory HOL-Library.Poly_Mapping Frequency_Moments: theory HOL-Library.Code_Target_Numeral Frequency_Moments: theory HOL-Library.List_Lexorder Frequency_Moments: theory HOL-Library.Power_By_Squaring Frequency_Moments: theory HOL-Number_Theory.Eratosthenes Frequency_Moments: theory HOL-Library.Landau_Symbols Frequency_Moments: theory HOL-Library.Lattice_Algebras Schwartz_Zippel: theory Polynomial_Interpolation.Missing_Unsorted CVP_Hardness: theory CVP_Hardness.Lattice_int Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial Schwartz_Zippel: theory Jordan_Normal_Form.Conjugate Schwartz_Zippel: theory Skip_Lists.Pi_pmf MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Logic MLSS_Decision_Proc: theory HOL-Library.Disjoint_Sets Schwartz_Zippel: theory HOL-Algebra.Order Schwartz_Zippel: theory Open_Induction.Restricted_Predicates CVP_Hardness: theory CVP_Hardness.CVP_p MLSS_Decision_Proc: theory HOL-Library.Multiset MLSS_Decision_Proc: theory HOL-Library.Countable Schwartz_Zippel: theory HOL-Computational_Algebra.Normalized_Fraction Frequency_Moments: theory HOL-Library.Log_Nat Frequency_Moments: theory Card_Partitions.Injectivity_Solver Preparing Binary_Code_Imprimitive/document ... Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom Frequency_Moments: theory Median_Method.Median MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Suc_Theory Schwartz_Zippel: theory Regular-Sets.Regular_Set Frequency_Moments: theory Universal_Hash_Families.Definitions Frequency_Moments: theory HOL-Algebra.Order Frequency_Moments: theory Universal_Hash_Families.Preliminary_Results Frequency_Moments: theory Card_Partitions.Card_Partitions Suppes_Theorem: theory HOL-Combinatorics.Permutations Schwartz_Zippel: theory Well_Quasi_Orders.Infinite_Sequences Preparing ABY3_Protocols/document ... Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Elements MLSS_Decision_Proc: theory HereditarilyFinite.Ordinal Schwartz_Zippel: theory HOL-Algebra.Lattice Schwartz_Zippel: theory Polynomials.MPoly_Type Finished Binary_Code_Imprimitive/document (0:00:09 elapsed time) Preparing Binary_Code_Imprimitive/outline ... Schwartz_Zippel: theory Well_Quasi_Orders.Least_Enum Frequency_Moments: theory Ergodic_Theory.SG_Library_Complement Suppes_Theorem: theory HOL-Combinatorics.List_Permutation Frequency_Moments: theory HOL-Number_Theory.Mod_Exp Suppes_Theorem: theory Propositional_Logic_Class.List_Utilities Frequency_Moments: theory Bell_Numbers_Spivey.Bell_Numbers Finished ABY3_Protocols/document (0:00:05 elapsed time) Preparing ABY3_Protocols/outline ... Suppes_Theorem: theory Propositional_Logic_Class.Classical_Connectives Frequency_Moments: theory Card_Equiv_Relations.Card_Equiv_Relations Frequency_Moments: theory Equivalence_Relation_Enumeration.Equivalence_Relation_Enumeration MLSS_Decision_Proc: theory HereditarilyFinite.Finitary Suppes_Theorem: theory Suppes_Theorem.Probability_Logic MLSS_Decision_Proc: theory HereditarilyFinite.Rank Suppes_Theorem: theory Suppes_Theorem.Suppes_Theorem Finished Binary_Code_Imprimitive/outline (0:00:05 elapsed time) Timing Binary_Code_Imprimitive (8 threads, 24.662s elapsed time, 20.935s cpu time, 0.615s GC time, factor 0.85) Finished Binary_Code_Imprimitive (0:00:26 elapsed time, 0:00:23 cpu time, factor 0.88) Frequency_Moments: theory HOL-Algebra.Lattice Running CommCSL on hpcisabelle/6 ... Schwartz_Zippel: theory Polynomials.More_MPoly_Type Finished ABY3_Protocols/outline (0:00:03 elapsed time) Timing ABY3_Protocols (8 threads, 16.408s elapsed time, 39.187s cpu time, 0.911s GC time, factor 2.39) Finished ABY3_Protocols (0:00:33 elapsed time, 0:00:43 cpu time, factor 1.31) Frequency_Moments: theory HOL-Number_Theory.Fib Running Edwards_Elliptic_Curves_Group on hpcisabelle/5 ... MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Semantics MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_HF_Extras MLSS_Decision_Proc: theory HOL-Library.Countable_Set CVP_Hardness: theory LLL_Basis_Reduction.Missing_Lemmas Edwards_Elliptic_Curves_Group: theory HOL-Library.Rewrite Edwards_Elliptic_Curves_Group: theory HOL-Library.FuncSet CommCSL: theory CommCSL.PartialMap Frequency_Moments: theory Lp.Functional_Spaces CommCSL: theory CommCSL.PosRat Frequency_Moments: theory HOL-Number_Theory.Prime_Powers CommCSL: theory CommCSL.FractionalHeap Schwartz_Zippel: theory HOL-Algebra.Complete_Lattice CommCSL: theory CommCSL.StateModel CVP_Hardness: theory LLL_Basis_Reduction.Norms Frequency_Moments: theory HOL-Number_Theory.Totient MLSS_Decision_Proc: theory HOL-Library.Countable_Complete_Lattices Frequency_Moments: theory HOL-Algebra.Complete_Lattice Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Congruence Schwartz_Zippel: theory HOL-Algebra.Group Frequency_Moments: theory Frequency_Moments.Landau_Ext Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Order CommCSL: theory CommCSL.CommCSL Frequency_Moments: theory HOL-Algebra.Group Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Lattice Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Complete_Lattice MLSS_Decision_Proc: theory HOL-Library.Order_Continuity MLSS_Decision_Proc: theory HOL-Combinatorics.Permutations Schwartz_Zippel: theory HOL-Algebra.FiniteProduct MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Typing_Defs Preparing Commuting_Hermitian/document ... Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Group MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Calculus Frequency_Moments: theory Lp.Lp MLSS_Decision_Proc: theory HOL-Library.Extended_Nat Schwartz_Zippel: theory HOL-Algebra.Ring MLSS_Decision_Proc: theory HOL-Combinatorics.Orbits MLSS_Decision_Proc: theory HOL-Library.Extended_Real MLSS_Decision_Proc: theory Graph_Theory.Auxiliary Schwartz_Zippel: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_FPS Schwartz_Zippel: theory Polynomials.MPoly_Type_Univariate Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_Factorial Finished Commuting_Hermitian/document (0:00:06 elapsed time) Preparing Commuting_Hermitian/outline ... CommCSL: theory CommCSL.AbstractCommutativity Edwards_Elliptic_Curves_Group: theory Edwards_Elliptic_Curves_Group.Edwards_Elliptic_Curves_Group Frequency_Moments: theory HOL-Algebra.Coset Frequency_Moments: theory HOL-Algebra.FiniteProduct Preparing Suppes_Theorem/document ... Frequency_Moments: theory HOL-Library.Interval MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Typing Frequency_Moments: theory HOL-Library.Float Finished Commuting_Hermitian/outline (0:00:02 elapsed time) Timing Commuting_Hermitian (8 threads, 14.470s elapsed time, 95.869s cpu time, 2.507s GC time, factor 6.63) Finished Commuting_Hermitian (0:01:05 elapsed time, 0:02:15 cpu time, factor 2.09) Running TsirelsonBound on hpcisabelle/2 ... Schwartz_Zippel: theory HOL-Computational_Algebra.Formal_Laurent_Series MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Typing_Urelems Frequency_Moments: theory HOL-Algebra.Ring TsirelsonBound: theory TsirelsonBound.Tensor_Mat_Compl_Properties Schwartz_Zippel: theory Polynomial_Interpolation.Missing_Polynomial CommCSL: theory CommCSL.Guards Finished Suppes_Theorem/document (0:00:04 elapsed time) Preparing Suppes_Theorem/outline ... CVP_Hardness: theory CVP_Hardness.infnorm CVP_Hardness: theory CVP_Hardness.Additional_Lemmas CVP_Hardness: theory CVP_Hardness.CVP_vec Schwartz_Zippel: theory HOL-Algebra.Module Finished Suppes_Theorem/outline (0:00:03 elapsed time) Timing Suppes_Theorem (8 threads, 62.277s elapsed time, 103.047s cpu time, 4.255s GC time, factor 1.65) Finished Suppes_Theorem (0:01:13 elapsed time, 0:02:04 cpu time, factor 1.70) CVP_Hardness: theory CVP_Hardness.BHLE Running Efficient_Weighted_Path_Order on hpcisabelle/1 ... Schwartz_Zippel: theory Jordan_Normal_Form.Missing_Ring Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.Indexed_Term CVP_Hardness: theory CVP_Hardness.SVP_vec Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.List_Memo_Functions CommCSL: theory CommCSL.Safety TsirelsonBound: theory TsirelsonBound.Matrix_L2_Operator_Norm MLSS_Decision_Proc: theory Graph_Theory.Stuff Frequency_Moments: theory HOL-Algebra.Generated_Groups Schwartz_Zippel: theory Polynomial_Factorization.Order_Polynomial Frequency_Moments: theory HOL-Algebra.Divisibility Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom_Poly MLSS_Decision_Proc: theory Graph_Theory.Digraph Schwartz_Zippel: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized TsirelsonBound: theory TsirelsonBound.Density_Matrix_Basics Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.WPO_Approx TsirelsonBound: theory TsirelsonBound.Tsirelson Frequency_Moments: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.WPO_Mem_Impl Schwartz_Zippel: theory HOL-Computational_Algebra.Computational_Algebra MLSS_Decision_Proc: theory Graph_Theory.Arc_Walk MLSS_Decision_Proc: theory Graph_Theory.Bidirected_Digraph Frequency_Moments: theory HOL-Library.Interval_Float Schwartz_Zippel: theory Symmetric_Polynomials.Vieta MLSS_Decision_Proc: theory Graph_Theory.Vertex_Walk MLSS_Decision_Proc: theory Graph_Theory.Pair_Digraph MLSS_Decision_Proc: theory Graph_Theory.Weighted_Graph MLSS_Decision_Proc: theory Graph_Theory.Shortest_Path Schwartz_Zippel: theory Symmetric_Polynomials.Symmetric_Polynomials Frequency_Moments: theory HOL-Algebra.Elementary_Groups Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.RPO_Unbounded Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.RPO_Mem_Impl Preparing Efficient_Weighted_Path_Order/document ... CommCSL: theory CommCSL.Soundness Frequency_Moments: theory HOL-Decision_Procs.Approximation_Bounds Schwartz_Zippel: theory Jordan_Normal_Form.Matrix Frequency_Moments: theory HOL-Algebra.AbelCoset Finished Efficient_Weighted_Path_Order/document (0:00:05 elapsed time) Preparing Efficient_Weighted_Path_Order/outline ... Frequency_Moments: theory HOL-Algebra.Module Schwartz_Zippel: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library Finished Efficient_Weighted_Path_Order/outline (0:00:03 elapsed time) Timing Efficient_Weighted_Path_Order (8 threads, 16.502s elapsed time, 33.112s cpu time, 1.757s GC time, factor 2.01) Finished Efficient_Weighted_Path_Order (0:00:23 elapsed time, 0:00:36 cpu time, factor 1.56) Running HyperHoareLogic on hpcisabelle/1 ... Schwartz_Zippel: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW MLSS_Decision_Proc: theory Graph_Theory.Digraph_Component Preparing TsirelsonBound/document ... HyperHoareLogic: theory HyperHoareLogic.Language Frequency_Moments: theory HOL-Algebra.Ideal HyperHoareLogic: theory HyperHoareLogic.Logic MLSS_Decision_Proc: theory Graph_Theory.Digraph_Component_Vwalk MLSS_Decision_Proc: theory Graph_Theory.Digraph_Isomorphism MLSS_Decision_Proc: theory Graph_Theory.Subdivision Finished TsirelsonBound/document (0:00:06 elapsed time) Preparing TsirelsonBound/outline ... Frequency_Moments: theory HOL-Algebra.RingHom Schwartz_Zippel: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Frequency_Moments: theory HOL-Algebra.QuotRing Frequency_Moments: theory HOL-Algebra.UnivPoly HyperHoareLogic: theory HyperHoareLogic.Examples Finished TsirelsonBound/outline (0:00:02 elapsed time) HyperHoareLogic: theory HyperHoareLogic.ProgramHyperproperties Timing TsirelsonBound (8 threads, 27.733s elapsed time, 147.242s cpu time, 2.060s GC time, factor 5.31) Finished TsirelsonBound (0:00:40 elapsed time, 0:02:32 cpu time, factor 3.75) Running MHComputation on hpcisabelle/2 ... MLSS_Decision_Proc: theory Graph_Theory.Kuratowski MLSS_Decision_Proc: theory Graph_Theory.Euler MHComputation: theory MHComputation.MHComputation CommCSL: theory CommCSL.NonInterference HyperHoareLogic: theory HyperHoareLogic.Expressivity Frequency_Moments: theory HOL-Algebra.IntRing Schwartz_Zippel: theory Jordan_Normal_Form.Column_Operations Schwartz_Zippel: theory Jordan_Normal_Form.Determinant Preparing MHComputation/document ... Preparing Edwards_Elliptic_Curves_Group/document ... Finished MHComputation/document (0:00:02 elapsed time) Preparing MHComputation/outline ... Frequency_Moments: theory HOL-Algebra.Multiplicative_Group Finished MHComputation/outline (0:00:02 elapsed time) Timing MHComputation (8 threads, 5.282s elapsed time, 5.573s cpu time, 0.162s GC time, factor 1.06) Finished MHComputation (0:00:07 elapsed time, 0:00:07 cpu time, factor 1.06) Running No_FTL_observers_Gen_Rel on hpcisabelle/2 ... No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Sorts Preparing CVP_Hardness/document ... MLSS_Decision_Proc: theory Graph_Theory.Graph_Theory Frequency_Moments: theory HOL-Algebra.Ring_Divisibility Frequency_Moments: theory HOL-Algebra.Subrings Frequency_Moments: theory HOL-Number_Theory.Residues MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Realisation Preparing HyperHoareLogic/document ... Frequency_Moments: theory HOL-Algebra.Embedded_Algebras Frequency_Moments: theory HOL-Number_Theory.Euler_Criterion Frequency_Moments: theory HOL-Number_Theory.Gauss Frequency_Moments: theory HOL-Number_Theory.Quadratic_Reciprocity Frequency_Moments: theory HOL-Number_Theory.Pocklington MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Proc Frequency_Moments: theory HOL-Number_Theory.Residue_Primitive_Roots Finished Edwards_Elliptic_Curves_Group/document (0:00:11 elapsed time) Preparing Edwards_Elliptic_Curves_Group/outline ... Finished CVP_Hardness/document (0:00:06 elapsed time) Preparing CVP_Hardness/outline ... Frequency_Moments: theory HOL-Number_Theory.Number_Theory Frequency_Moments: theory Lehmer.Lehmer Frequency_Moments: theory Pratt_Certificate.Pratt_Certificate Frequency_Moments: theory HOL-Algebra.Polynomials Finished HyperHoareLogic/document (0:00:06 elapsed time) Preparing HyperHoareLogic/outline ... No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxEField No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Points Finished Edwards_Elliptic_Curves_Group/outline (0:00:04 elapsed time) Timing Edwards_Elliptic_Curves_Group (8 threads, 85.450s elapsed time, 293.444s cpu time, 6.085s GC time, factor 3.43) Finished Edwards_Elliptic_Curves_Group (0:01:27 elapsed time, 0:04:58 cpu time, factor 3.40) Running Probability_Inequality_Completeness on hpcisabelle/5 ... Finished CVP_Hardness/outline (0:00:03 elapsed time) Timing CVP_Hardness (8 threads, 133.522s elapsed time, 460.562s cpu time, 8.300s GC time, factor 3.45) Finished CVP_Hardness (0:02:18 elapsed time, 0:07:47 cpu time, factor 3.39) Running Rensets on hpcisabelle/7 ... Frequency_Moments: theory Bertrands_Postulate.Bertrand Probability_Inequality_Completeness: theory Probability_Inequality_Completeness.Probability_Inequality_Completeness Rensets: theory Rensets.Lambda_Terms Finished HyperHoareLogic/outline (0:00:03 elapsed time) Timing HyperHoareLogic (8 threads, 9.588s elapsed time, 49.475s cpu time, 1.506s GC time, factor 5.16) Finished HyperHoareLogic (0:00:25 elapsed time, 0:00:52 cpu time, factor 2.04) Running Simple_Clause_Learning on hpcisabelle/1 ... MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Proc_Code Simple_Clause_Learning: theory Deriving.Comparator Simple_Clause_Learning: theory Deriving.Generator_Aux Simple_Clause_Learning: theory Deriving.Derive_Manager Simple_Clause_Learning: theory Simple_Clause_Learning.Multiset_Order_Extra Simple_Clause_Learning: theory Word_Lib.Bit_Comprehension Simple_Clause_Learning: theory HOL-Cardinals.Order_Union Simple_Clause_Learning: theory Word_Lib.More_Divides Simple_Clause_Learning: theory Word_Lib.Signed_Division_Word Simple_Clause_Learning: theory Nested_Multisets_Ordinals.Multiset_More Simple_Clause_Learning: theory Deriving.Countable_Generator Rensets: theory Rensets.Nominal_Sets Rensets: theory Rensets.Rensets Rensets: theory Rensets.FRBCE_Rensets Simple_Clause_Learning: theory HOL-Cardinals.Wellorder_Extension Frequency_Moments: theory HOL-Algebra.Polynomial_Divisibility Rensets: theory Rensets.Examples Rensets: theory Rensets.Substitutive_Sets Rensets: theory Rensets.Rensets_to_Nominal_Sets MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Proc_All Frequency_Moments: theory Frequency_Moments.Frequency_Moments_Preliminary_Results Simple_Clause_Learning: theory Deriving.Equality_Generator Simple_Clause_Learning: theory Coinductive.Coinductive_Nat Simple_Clause_Learning: theory List-Index.List_Index Simple_Clause_Learning: theory Matrix.Utility Simple_Clause_Learning: theory Native_Word.Code_Int_Integer_Conversion Simple_Clause_Learning: theory Open_Induction.Restricted_Predicates Preparing Rensets/document ... Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation Simple_Clause_Learning: theory Deriving.Equality_Instances Simple_Clause_Learning: theory Polynomial_Factorization.Missing_List Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family Simple_Clause_Learning: theory Ordered_Resolution_Prover.Map2 Frequency_Moments: theory Frequency_Moments.K_Smallest Simple_Clause_Learning: theory Knuth_Bendix_Order.Order_Pair Frequency_Moments: theory Frequency_Moments.Probability_Ext Simple_Clause_Learning: theory Simple_Clause_Learning.First_Order_Terms_Extra Finished Rensets/document (0:00:04 elapsed time) Simple_Clause_Learning: theory Ordered_Resolution_Prover.Clausal_Logic Simple_Clause_Learning: theory Knuth_Bendix_Order.Subterm_and_Context Simple_Clause_Learning: theory Deriving.Compare Frequency_Moments: theory Frequency_Moments.Product_PMF_Ext Simple_Clause_Learning: theory Deriving.Comparator_Generator Simple_Clause_Learning: theory Coinductive.Coinductive_List Simple_Clause_Learning: theory Knuth_Bendix_Order.Lexicographic_Extension Finished Rensets/outline (0:00:03 elapsed time) Timing Rensets (8 threads, 14.270s elapsed time, 63.309s cpu time, 1.558s GC time, factor 4.44) Finished Rensets (0:00:16 elapsed time, 0:01:06 cpu time, factor 4.09) Running Three_Squares on hpcisabelle/7 ... Simple_Clause_Learning: theory Simple_Clause_Learning.Abstract_Renaming_Apart Simple_Clause_Learning: theory Simple_Clause_Learning.Relation_Extra Preparing MLSS_Decision_Proc/document ... Three_Squares: theory Pure-ex.Guess Three_Squares: theory HOL-Eisbach.Eisbach Three_Squares: theory HOL-Computational_Algebra.Fraction_Field Three_Squares: theory HOL-Combinatorics.Stirling Three_Squares: theory HOL-Computational_Algebra.Group_Closure Three_Squares: theory HOL-Library.Adhoc_Overloading Three_Squares: theory HOL-Decision_Procs.Dense_Linear_Order Three_Squares: theory HOL-Library.BNF_Corec Three_Squares: theory HOL-Computational_Algebra.Nth_Powers Simple_Clause_Learning: theory Simple_Clause_Learning.Trail_Induced_Ordering Simple_Clause_Learning: theory Ordered_Resolution_Prover.Herbrand_Interpretation Finished MLSS_Decision_Proc/document (0:00:02 elapsed time) Preparing MLSS_Decision_Proc/outline ... No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Functions No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Norms No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.WorldView Three_Squares: theory Three_Squares.Low_Dimensional_Linear_Algebra Simple_Clause_Learning: theory Ordered_Resolution_Prover.Abstract_Substitution Simple_Clause_Learning: theory Ordered_Resolution_Prover.Ground_Resolution_Model Finished MLSS_Decision_Proc/outline (0:00:02 elapsed time) Timing MLSS_Decision_Proc (8 threads, 170.322s elapsed time, 547.852s cpu time, 20.685s GC time, factor 3.22) Finished MLSS_Decision_Proc (0:02:53 elapsed time, 0:09:16 cpu time, factor 3.22) Running Tree_Enumeration on hpcisabelle/4 ... Tree_Enumeration: theory HOL-Library.Cancellation Tree_Enumeration: theory HOL-Combinatorics.Transposition Tree_Enumeration: theory HOL-Library.FuncSet Tree_Enumeration: theory HOL-Library.Infinite_Set Tree_Enumeration: theory HOL-Library.Nat_Bijection Tree_Enumeration: theory HOL-Library.Old_Datatype Tree_Enumeration: theory HOL-Library.Sublist Tree_Enumeration: theory HOL-Library.Liminf_Limsup No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxTriangleInequality No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Vectors Simple_Clause_Learning: theory Deriving.Compare_Generator Three_Squares: theory HOL-Computational_Algebra.Squarefree Three_Squares: theory HOL-Number_Theory.Cong Preparing Probability_Inequality_Completeness/document ... Simple_Clause_Learning: theory Ordered_Resolution_Prover.Inference_System No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxEventMinus No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxSelfMinus Three_Squares: theory HOL-Library.Code_Abstract_Nat Simple_Clause_Learning: theory Word_Lib.More_Arithmetic Simple_Clause_Learning: theory Word_Lib.More_Word Simple_Clause_Learning: theory Deriving.Compare_Instances Tree_Enumeration: theory HOL-Library.Disjoint_Sets Tree_Enumeration: theory HOL-Library.Countable Three_Squares: theory HOL-Library.Code_Target_Nat Three_Squares: theory HOL-Eisbach.Eisbach_Tools Schwartz_Zippel: theory Regular-Sets.Regular_Exp Tree_Enumeration: theory HOL-Library.Multiset Three_Squares: theory HOL-Library.Code_Target_Int Schwartz_Zippel: theory Regular-Sets.NDerivative Schwartz_Zippel: theory Regular-Sets.Relation_Interpretation Tree_Enumeration: theory Card_Partitions.Set_Partition Three_Squares: theory HOL-Algebra.Congruence Schwartz_Zippel: theory Regular-Sets.Equivalence_Checking Three_Squares: theory HOL-Library.Function_Algebras Schwartz_Zippel: theory Regular-Sets.Regexp_Method Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full Three_Squares: theory HOL-Library.Code_Target_Numeral Three_Squares: theory HOL-Library.Power_By_Squaring Simple_Clause_Learning: theory Ordered_Resolution_Prover.Unordered_Ground_Resolution Three_Squares: theory HOL-Number_Theory.Eratosthenes Three_Squares: theory HOL-Computational_Algebra.Normalized_Fraction Three_Squares: theory HOL-Real_Asymp.Inst_Existentials Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Bad_Sequences Three_Squares: theory Bernoulli.Bernoulli Simple_Clause_Learning: theory Knuth_Bendix_Order.Term_Aux Three_Squares: theory HOL-Computational_Algebra.Field_as_Ring Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full_Relations Schwartz_Zippel: theory Polynomials.Utils Finished Probability_Inequality_Completeness/document (0:00:16 elapsed time) Preparing Probability_Inequality_Completeness/outline ... Preparing CommCSL/document ... Schwartz_Zippel: theory Well_Quasi_Orders.Well_Quasi_Orders Three_Squares: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Three_Squares: theory HOL-Algebra.Order Tree_Enumeration: theory HOL-Library.Countable_Set Tree_Enumeration: theory HOL-Library.FSet Simple_Clause_Learning: theory Native_Word.Code_Target_Word_Base Three_Squares: theory HOL-Computational_Algebra.Polynomial_Factorial Simple_Clause_Learning: theory Word_Lib.Bit_Shifts_Infix_Syntax Three_Squares: theory HOL-Number_Theory.Mod_Exp Simple_Clause_Learning: theory Word_Lib.Least_significant_bit Three_Squares: theory HOL-Library.Going_To_Filter Schwartz_Zippel: theory Polynomials.Power_Products Three_Squares: theory HOL-Library.Lattice_Algebras Simple_Clause_Learning: theory Knuth_Bendix_Order.KBO Tree_Enumeration: theory HOL-Library.Countable_Complete_Lattices Finished Probability_Inequality_Completeness/outline (0:00:05 elapsed time) Timing Probability_Inequality_Completeness (8 threads, 35.902s elapsed time, 110.185s cpu time, 6.993s GC time, factor 3.07) Finished Probability_Inequality_Completeness (0:00:38 elapsed time, 0:01:54 cpu time, factor 3.02) Running Two_Generated_Word_Monoids_Intersection on hpcisabelle/5 ... Simple_Clause_Learning: theory Simple_Clause_Learning.Ordered_Resolution_Prover_Extra No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Cardinalities No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Quadratics No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Translations No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.WorldLine Two_Generated_Word_Monoids_Intersection: theory Combinatorics_Words_Graph_Lemma.Glued_Codes Three_Squares: theory HOL-Library.Log_Nat No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.CauchySchwarz No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Matrices Two_Generated_Word_Monoids_Intersection: theory Two_Generated_Word_Monoids_Intersection.Two_Generated_Word_Monoids_Intersection Three_Squares: theory Bernoulli.Periodic_Bernpoly Three_Squares: theory Winding_Number_Eval.Missing_Topology Three_Squares: theory HOL-Algebra.Lattice Three_Squares: theory Winding_Number_Eval.Missing_Analysis Three_Squares: theory HOL-Number_Theory.Fib Three_Squares: theory HOL-Number_Theory.Prime_Powers No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.ReverseCauchySchwarz Three_Squares: theory HOL-Number_Theory.Totient Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.TangentLines Three_Squares: theory HOL-Computational_Algebra.Computational_Algebra Finished CommCSL/document (0:00:15 elapsed time) Three_Squares: theory Sturm_Tarski.PolyMisc Simple_Clause_Learning: theory Word_Lib.Most_significant_bit Three_Squares: theory HOL-Real_Asymp.Eventuallize Three_Squares: theory HOL-Real_Asymp.Lazy_Eval Frequency_Moments: theory Finite_Fields.Ring_Characteristic Three_Squares: theory Sturm_Tarski.Sturm_Tarski Schwartz_Zippel: theory Polynomials.MPoly_Type_Class Simple_Clause_Learning: theory Word_Lib.Generic_set_bit Three_Squares: theory Three_Squares.Quadratic_Forms Three_Squares: theory HOL-Algebra.Complete_Lattice Three_Squares: theory Landau_Symbols.Group_Sort Finished CommCSL/outline (0:00:05 elapsed time) Timing CommCSL (8 threads, 54.832s elapsed time, 332.569s cpu time, 17.592s GC time, factor 6.07) Finished CommCSL (0:02:37 elapsed time, 0:05:44 cpu time, factor 2.18) Running DigitsInBase on hpcisabelle/6 ... Preparing Two_Generated_Word_Monoids_Intersection/document ... Simple_Clause_Learning: theory Native_Word.Code_Target_Integer_Bit Simple_Clause_Learning: theory Native_Word.Word_Type_Copies Tree_Enumeration: theory HOL-Library.Order_Continuity DigitsInBase: theory DigitsInBase.DigitsInBase Tree_Enumeration: theory HOL-Library.Multiset_Order Tree_Enumeration: theory HOL-Combinatorics.Permutations Schwartz_Zippel: theory Factor_Algebraic_Polynomial.Poly_Connection Schwartz_Zippel: theory Schwartz_Zippel.Schwartz_Zippel Preparing DigitsInBase/document ... Simple_Clause_Learning: theory Ordered_Resolution_Prover.Lazy_List_Liminf Finished Two_Generated_Word_Monoids_Intersection/document (0:00:06 elapsed time) Preparing Two_Generated_Word_Monoids_Intersection/outline ... Tree_Enumeration: theory HOL-Library.Extended_Nat Tree_Enumeration: theory Nested_Multisets_Ordinals.Multiset_More Simple_Clause_Learning: theory Ordered_Resolution_Prover.Lazy_List_Chain Schwartz_Zippel: theory Schwartz_Zippel.Rand_Perfect_Matching Frequency_Moments: theory Universal_Hash_Families.Field Frequency_Moments: theory Frequency_Moments.Frequency_Moments Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2 Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k Finished DigitsInBase/document (0:00:03 elapsed time) Preparing DigitsInBase/outline ... Tree_Enumeration: theory HOL-Combinatorics.Multiset_Permutations Tree_Enumeration: theory HOL-Library.Extended_Real Tree_Enumeration: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset Finished Two_Generated_Word_Monoids_Intersection/outline (0:00:04 elapsed time) Timing Two_Generated_Word_Monoids_Intersection (8 threads, 12.681s elapsed time, 21.882s cpu time, 0.883s GC time, factor 1.73) Finished Two_Generated_Word_Monoids_Intersection (0:00:15 elapsed time, 0:00:23 cpu time, factor 1.52) Running Given_Clause_Loops on hpcisabelle/5 ... Tree_Enumeration: theory Design_Theory.Multisets_Extras Finished DigitsInBase/outline (0:00:02 elapsed time) Timing DigitsInBase (8 threads, 3.755s elapsed time, 9.440s cpu time, 0.169s GC time, factor 2.51) Finished DigitsInBase (0:00:06 elapsed time, 0:00:13 cpu time, factor 2.12) Tree_Enumeration: theory Design_Theory.Design_Basics Given_Clause_Loops: theory Abstract-Rewriting.Seq Given_Clause_Loops: theory Regular-Sets.Regular_Set Given_Clause_Loops: theory Given_Clause_Loops.More_Given_Clause_Architectures Simple_Clause_Learning: theory Saturation_Framework.Calculus Simple_Clause_Learning: theory Simple_Clause_Learning.Wellfounded_Extra Tree_Enumeration: theory Design_Theory.Design_Operations Simple_Clause_Learning: theory Saturation_Framework_Extensions.Soundness Simple_Clause_Learning: theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion Preparing Schwartz_Zippel/document ... Given_Clause_Loops: theory Regular-Sets.Regular_Exp Simple_Clause_Learning: theory Saturation_Framework_Extensions.Clausal_Calculus No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxLightMinus No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Sublemma3 No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Cones Given_Clause_Loops: theory Regular-Sets.NDerivative Given_Clause_Loops: theory Regular-Sets.Relation_Interpretation Three_Squares: theory Budan_Fourier.BF_Misc Finished Schwartz_Zippel/document (0:00:03 elapsed time) Preparing Schwartz_Zippel/outline ... Simple_Clause_Learning: theory Simple_Clause_Learning.SCL_FOL Tree_Enumeration: theory Design_Theory.Block_Designs Tree_Enumeration: theory Girth_Chromatic.Girth_Chromatic_Misc Tree_Enumeration: theory Undirected_Graph_Theory.Undirected_Graph_Basics Three_Squares: theory HOL-Algebra.Group Finished Schwartz_Zippel/outline (0:00:02 elapsed time) Timing Schwartz_Zippel (8 threads, 237.579s elapsed time, 511.999s cpu time, 20.967s GC time, factor 2.16) Finished Schwartz_Zippel (0:04:01 elapsed time, 0:08:41 cpu time, factor 2.16) Given_Clause_Loops: theory Regular-Sets.Equivalence_Checking Three_Squares: theory Landau_Symbols.Landau_Real_Products Given_Clause_Loops: theory Regular-Sets.Regexp_Method Given_Clause_Loops: theory Abstract-Rewriting.Abstract_Rewriting Tree_Enumeration: theory Design_Theory.BIBD Three_Squares: theory Winding_Number_Eval.Missing_Algebraic Tree_Enumeration: theory Design_Theory.Resolvable_Designs Given_Clause_Loops: theory Weighted_Path_Order.Relations Given_Clause_Loops: theory Weighted_Path_Order.Multiset_Extension_Pair No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.LinearMaps Given_Clause_Loops: theory Given_Clause_Loops.Given_Clause_Loops_Util Given_Clause_Loops: theory Given_Clause_Loops.Prover_Queue Given_Clause_Loops: theory Given_Clause_Loops.DISCOUNT_Loop Given_Clause_Loops: theory Given_Clause_Loops.Otter_Loop Given_Clause_Loops: theory Given_Clause_Loops.Prover_Lazy_List_Queue Given_Clause_Loops: theory Given_Clause_Loops.Fair_Otter_Loop_Def Given_Clause_Loops: theory Given_Clause_Loops.Fair_DISCOUNT_Loop Given_Clause_Loops: theory Given_Clause_Loops.Zipperposition_Loop Given_Clause_Loops: theory Given_Clause_Loops.iProver_Loop Tree_Enumeration: theory Design_Theory.Group_Divisible_Designs Three_Squares: theory HOL-Real_Asymp.Multiseries_Expansion Three_Squares: theory Winding_Number_Eval.Missing_Transcendental Three_Squares: theory Winding_Number_Eval.Cauchy_Index_Theorem Three_Squares: theory HOL-Algebra.Coset Given_Clause_Loops: theory Given_Clause_Loops.Fair_iProver_Loop Given_Clause_Loops: theory Given_Clause_Loops.Fair_Zipperposition_Loop Three_Squares: theory HOL-Algebra.FiniteProduct Tree_Enumeration: theory Undirected_Graph_Theory.Graph_Triangles Tree_Enumeration: theory Undirected_Graph_Theory.Undirected_Graph_Walks Three_Squares: theory HOL-Library.Interval Tree_Enumeration: theory Undirected_Graph_Theory.Bipartite_Graphs Tree_Enumeration: theory Undirected_Graph_Theory.Connectivity Given_Clause_Loops: theory Given_Clause_Loops.Fair_Otter_Loop_Complete Three_Squares: theory HOL-Algebra.Ring Three_Squares: theory HOL-Library.Float Tree_Enumeration: theory Undirected_Graph_Theory.Graph_Theory_Relations Tree_Enumeration: theory Undirected_Graph_Theory.Girth_Independence No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Affine No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Classification No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Proposition1 Simple_Clause_Learning: theory Native_Word.Uint32 Three_Squares: theory HOL-Algebra.Generated_Groups Three_Squares: theory Landau_Symbols.Landau_Simprocs Simple_Clause_Learning: theory Collections.HashCode Simple_Clause_Learning: theory Deriving.Hash_Generator Given_Clause_Loops: theory Given_Clause_Loops.Fair_Zipperposition_Loop_without_Ghosts Three_Squares: theory Winding_Number_Eval.Winding_Number_Eval Tree_Enumeration: theory Undirected_Graph_Theory.Undirected_Graphs_Root Tree_Enumeration: theory Tree_Enumeration.Tree_Graph Simple_Clause_Learning: theory Deriving.Hash_Instances Simple_Clause_Learning: theory Deriving.Derive Simple_Clause_Learning: theory Functional_Ordered_Resolution_Prover.IsaFoR_Term Three_Squares: theory Landau_Symbols.Landau_More Given_Clause_Loops: theory Given_Clause_Loops.Given_Clause_Loops Three_Squares: theory HOL-Algebra.Elementary_Groups Preparing Given_Clause_Loops/document ... Three_Squares: theory HOL-Library.Interval_Float Three_Squares: theory HOL-Decision_Procs.Approximation_Bounds Three_Squares: theory HOL-Algebra.AbelCoset Three_Squares: theory HOL-Algebra.Module Three_Squares: theory HOL-Algebra.Ideal Tree_Enumeration: theory Tree_Enumeration.Rooted_Tree Tree_Enumeration: theory Tree_Enumeration.Labeled_Tree_Enumeration Simple_Clause_Learning FAILED (see also "isabelle build_log -H Error Simple_Clause_Learning") *** Duplicate fact declaration "SCL_FOL.grounding_of_clss_empty" vs. "SCL_FOL.grounding_of_clss_empty" (line 543 of "$AFP/Simple_Clause_Learning/SCL_FOL.thy") *** The above error(s) occurred while activating facts of locale instance *** substitution "(⋅a)" "Var" "(⊙)" *** At command "global_interpretation" (line 543 of "$AFP/Simple_Clause_Learning/SCL_FOL.thy") *** Undefined fact: "asymp.simps" (line 25 of "$AFP/Simple_Clause_Learning/Relation_Extra.thy") *** At command "by" (line 25 of "$AFP/Simple_Clause_Learning/Relation_Extra.thy") *** Undefined fact: "asymp.simps" (line 22 of "$AFP/Simple_Clause_Learning/Relation_Extra.thy") *** At command "by" (line 22 of "$AFP/Simple_Clause_Learning/Relation_Extra.thy") *** Failed to apply initial proof method (line 570 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy"): *** At command "by" (line 570 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy") *** Failed to apply initial proof method (line 558 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy"): *** 1. (⋀xs. ⟦unify [(s, t)] [] = Some xs; μ = subst_of xs⟧ ⟹ thesis) ⟹ *** At command "by" (line 558 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy") *** Failed to apply initial proof method (line 537 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy"): *** 1. (⋀xs. ⟦unify [(s, t)] [] = Some xs; μ = subst_of xs⟧ ⟹ thesis) ⟹ *** At command "by" (line 537 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy") Three_Squares: theory HOL-Algebra.RingHom Finished Given_Clause_Loops/document (0:00:07 elapsed time) Preparing Given_Clause_Loops/outline ... Three_Squares: theory HOL-Algebra.QuotRing Three_Squares: theory HOL-Algebra.UnivPoly Three_Squares: theory HOL-Algebra.IntRing Three_Squares: theory Finitely_Generated_Abelian_Groups.General_Auxiliary Finished Given_Clause_Loops/outline (0:00:03 elapsed time) Timing Given_Clause_Loops (8 threads, 38.634s elapsed time, 172.975s cpu time, 6.626s GC time, factor 4.48) Finished Given_Clause_Loops (0:00:45 elapsed time, 0:03:01 cpu time, factor 3.96) Three_Squares: theory HOL-Algebra.Multiplicative_Group Tree_Enumeration: theory Tree_Enumeration.Rooted_Tree_Enumeration Three_Squares: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Three_Squares: theory Finitely_Generated_Abelian_Groups.Set_Multiplication Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Hom Three_Squares: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups Three_Squares: theory HOL-Number_Theory.Residues Three_Squares: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups Three_Squares: theory Finitely_Generated_Abelian_Groups.IDirProds Three_Squares: theory HOL-Number_Theory.Euler_Criterion Three_Squares: theory HOL-Number_Theory.Gauss Three_Squares: theory HOL-Number_Theory.Quadratic_Reciprocity Three_Squares: theory Three_Squares.Residues_Properties Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend Three_Squares: theory HOL-Number_Theory.Pocklington Three_Squares: theory HOL-Number_Theory.Residue_Primitive_Roots Three_Squares: theory Finitely_Generated_Abelian_Groups.DirProds Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Relations Three_Squares: theory HOL-Number_Theory.Number_Theory Three_Squares: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups Three_Squares: theory Dirichlet_L.Multiplicative_Characters Three_Squares: theory Bernoulli.Bernoulli_FPS Three_Squares: theory Dirichlet_Series.Dirichlet_Misc Three_Squares: theory Dirichlet_Series.Multiplicative_Function Three_Squares: theory Dirichlet_L.Dirichlet_Characters Three_Squares: theory Dirichlet_Series.Dirichlet_Product No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.KeyLemma Three_Squares: theory Dirichlet_Series.Dirichlet_Series Three_Squares: theory Bernoulli.Bernoulli_Zeta Three_Squares: theory Euler_MacLaurin.Euler_MacLaurin No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Sublemma4 No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxDiff Three_Squares: theory Dirichlet_Series.Euler_Products Three_Squares: theory Dirichlet_Series.Moebius_Mu Three_Squares: theory Dirichlet_Series.More_Totient Three_Squares: theory Dirichlet_Series.Divisor_Count Three_Squares: theory Dirichlet_Series.Liouville_Lambda Three_Squares: theory HOL-Real_Asymp.Real_Asymp Three_Squares: theory Dirichlet_Series.Arithmetic_Summatory Three_Squares: theory Lehmer.Lehmer Three_Squares: theory Dirichlet_Series.Partial_Summation Three_Squares: theory Pratt_Certificate.Pratt_Certificate Three_Squares: theory Dirichlet_Series.Dirichlet_Series_Analysis Three_Squares: theory Bertrands_Postulate.Bertrand Three_Squares: theory Zeta_Function.Zeta_Library Three_Squares: theory Zeta_Function.Zeta_Function Three_Squares: theory Dirichlet_L.Dirichlet_L_Functions Three_Squares: theory Dirichlet_L.Dirichlet_Theorem Three_Squares: theory Three_Squares.Three_Squares No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.MainLemma Preparing Tree_Enumeration/document ... Finished Tree_Enumeration/document (0:00:06 elapsed time) Preparing Tree_Enumeration/outline ... Finished Tree_Enumeration/outline (0:00:03 elapsed time) Timing Tree_Enumeration (8 threads, 133.433s elapsed time, 490.369s cpu time, 17.635s GC time, factor 3.68) Finished Tree_Enumeration (0:02:15 elapsed time, 0:08:18 cpu time, factor 3.67) No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.TangentLineLemma No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AffineConeLemma No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Proposition2 No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Proposition3 Preparing Frequency_Moments/document ... Finished Frequency_Moments/document (0:00:08 elapsed time) Preparing Frequency_Moments/outline ... Finished Frequency_Moments/outline (0:00:04 elapsed time) No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.ObserverConeLemma Timing Frequency_Moments (8 threads, 325.148s elapsed time, 1262.029s cpu time, 95.074s GC time, factor 3.88) Finished Frequency_Moments (0:06:08 elapsed time, 0:22:45 cpu time, factor 3.71) Building Expander_Graphs on hpcisabelle/6 ... Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method Expander_Graphs: theory Graph_Theory.Rtrancl_On Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc Expander_Graphs: theory Abstract-Rewriting.Seq Expander_Graphs: theory Perron_Frobenius.Bij_Nat Expander_Graphs: theory HOL-Library.More_List Expander_Graphs: theory HOL-Library.While_Combinator Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted Expander_Graphs: theory HOL-Computational_Algebra.Polynomial Expander_Graphs: theory Jordan_Normal_Form.Conjugate Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint Expander_Graphs: theory HOL-Decision_Procs.Approximation Expander_Graphs: theory Graph_Theory.Stuff Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction Expander_Graphs: theory Graph_Theory.Digraph Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound Expander_Graphs: theory Matrix.Utility Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom Expander_Graphs: theory Regular-Sets.Regular_Set No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.NoFTLGR Expander_Graphs: theory VectorSpace.FunctionLemmas Expander_Graphs: theory Graph_Theory.Arc_Walk Expander_Graphs: theory Graph_Theory.Bidirected_Digraph Expander_Graphs: theory VectorSpace.RingModuleFacts Expander_Graphs: theory VectorSpace.MonoidSums Expander_Graphs: theory Graph_Theory.Pair_Digraph Expander_Graphs: theory VectorSpace.LinearCombinations Expander_Graphs: theory Regular-Sets.Regular_Exp Expander_Graphs: theory Jordan_Normal_Form.Matrix Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial Expander_Graphs: theory Regular-Sets.NDerivative Expander_Graphs: theory Regular-Sets.Relation_Interpretation Expander_Graphs: theory VectorSpace.SumSpaces Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial Expander_Graphs: theory VectorSpace.VectorSpace Expander_Graphs: theory Graph_Theory.Digraph_Component Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Expander_Graphs: theory Jordan_Normal_Form.Column_Operations Expander_Graphs: theory Regular-Sets.Equivalence_Checking Expander_Graphs: theory Regular-Sets.Regexp_Method Expander_Graphs: theory Jordan_Normal_Form.Determinant Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting Expander_Graphs: theory Jordan_Normal_Form.Char_Poly Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition Expander_Graphs: theory Abstract-Rewriting.SN_Orders Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form Expander_Graphs: theory Isabelle_Marries_Dirac.Basics Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum Expander_Graphs: theory Jordan_Normal_Form.VS_Connect Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS Expander_Graphs: theory Matrix.Ordered_Semiring Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors Expander_Graphs: theory Matrix.Matrix_Legacy Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius Expander_Graphs: theory QHLProver.Complex_Matrix Expander_Graphs: theory Perron_Frobenius.HMA_Connect Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG Expander_Graphs: theory QHLProver.Gates Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements Expander_Graphs: theory Projective_Measurements.Projective_Measurements Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks Preparing No_FTL_observers_Gen_Rel/document ... Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit Finished No_FTL_observers_Gen_Rel/document (0:00:10 elapsed time) Preparing No_FTL_observers_Gen_Rel/outline ... Finished No_FTL_observers_Gen_Rel/outline (0:00:04 elapsed time) Timing No_FTL_observers_Gen_Rel (8 threads, 326.778s elapsed time, 1253.219s cpu time, 31.596s GC time, factor 3.84) Finished No_FTL_observers_Gen_Rel (0:05:29 elapsed time, 0:21:02 cpu time, factor 3.83) Preparing Three_Squares/document ... Finished Three_Squares/document (0:00:05 elapsed time) Preparing Three_Squares/outline ... Finished Three_Squares/outline (0:00:03 elapsed time) Timing Three_Squares (8 threads, 419.495s elapsed time, 1717.509s cpu time, 88.929s GC time, factor 4.09) Finished Three_Squares (0:07:04 elapsed time, 0:28:58 cpu time, factor 4.09) Preparing Expander_Graphs/document ... Finished Expander_Graphs/document (0:00:11 elapsed time) Preparing Expander_Graphs/outline ... Finished Expander_Graphs/outline (0:00:04 elapsed time) Timing Expander_Graphs (8 threads, 306.712s elapsed time, 1849.017s cpu time, 92.444s GC time, factor 6.03) Finished Expander_Graphs (0:06:11 elapsed time, 0:33:32 cpu time, factor 5.41) Running Distributed_Distinct_Elements on hpcisabelle/7 ... Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Group_Closure Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Nth_Powers Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Squarefree Distributed_Distinct_Elements: theory Discrete_Summation.Factorials Distributed_Distinct_Elements: theory Finite_Fields.Formal_Polynomial_Derivatives Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Polynomial_FPS Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Misc Distributed_Distinct_Elements: theory Landau_Symbols.Group_Sort Distributed_Distinct_Elements: theory Dirichlet_Series.Multiplicative_Function Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Product Distributed_Distinct_Elements: theory Finite_Fields.Monic_Polynomial_Factorization Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Formal_Laurent_Series Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Real_Products Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Computational_Algebra Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Simprocs Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series Distributed_Distinct_Elements: theory Landau_Symbols.Landau_More Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials_Aux Distributed_Distinct_Elements: theory Stirling_Formula.Stirling_Formula Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary Distributed_Distinct_Elements: theory Dirichlet_Series.Moebius_Mu Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Pseudorandom_Combinators Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm Preparing Distributed_Distinct_Elements/document ... Finished Distributed_Distinct_Elements/document (0:00:11 elapsed time) Preparing Distributed_Distinct_Elements/outline ... Finished Distributed_Distinct_Elements/outline (0:00:04 elapsed time) Timing Distributed_Distinct_Elements (8 threads, 52.614s elapsed time, 302.732s cpu time, 8.291s GC time, factor 5.75) Finished Distributed_Distinct_Elements (0:00:56 elapsed time, 0:05:09 cpu time, factor 5.45) Presentation in "/media/data/jenkins/workspace/isabelle-all/browser_info" Presenting Edwards_Elliptic_Curves_Group in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Edwards_Elliptic_Curves_Group" ... Presenting Three_Squares in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Three_Squares" ... Presenting Frequency_Moments in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Frequency_Moments" ... Presenting Schwartz_Zippel in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Schwartz_Zippel" ... Presenting Commuting_Hermitian in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Commuting_Hermitian" ... Presenting ABY3_Protocols in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/ABY3_Protocols" ... Presenting Distributed_Distinct_Elements in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Distributed_Distinct_Elements" ... Presenting TsirelsonBound in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/TsirelsonBound" ... Presenting Expander_Graphs in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Expander_Graphs" ... Presenting document Edwards_Elliptic_Curves_Group/document Presenting document Edwards_Elliptic_Curves_Group/outline Presenting document Schwartz_Zippel/document Presenting document TsirelsonBound/document Presenting document Schwartz_Zippel/outline Presenting document TsirelsonBound/outline Presenting document Commuting_Hermitian/document Presenting document Commuting_Hermitian/outline Presenting document ABY3_Protocols/document Presenting document ABY3_Protocols/outline Presenting document Three_Squares/document Presenting document Three_Squares/outline Presenting document Distributed_Distinct_Elements/document Presenting document Distributed_Distinct_Elements/outline Presenting document Expander_Graphs/document Presenting document Expander_Graphs/outline Presenting document Frequency_Moments/document Presenting document Frequency_Moments/outline Presenting theory "ABY3_Protocols.Finite_Number_Type" Presenting theory "Commuting_Hermitian.Commuting_Hermitian_Misc" Presenting theory "HOL-Library.Log_Nat" Presenting theory "Landau_Symbols.Group_Sort" Presenting theory "HOL-Library.Groups_Big_Fun" Presenting theory "HOL-Library.Fun_Lexorder" Presenting theory "Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean" Presenting theory "HOL-Number_Theory.Cong" Presenting theory "ABY3_Protocols.Additive_Sharing" Presenting theory "HOL-Library.Lattice_Algebras" Presenting theory "HOL-Library.FuncSet" Presenting theory "Commuting_Hermitian.Spectral_Theory_Complements" Presenting theory "HOL-Algebra.Congruence" Presenting theory "HOL-Library.More_List" Presenting theory "ABY3_Protocols.Spmf_Common" Presenting theory "Landau_Symbols.Landau_Real_Products" Presenting theory "Expander_Graphs.Constructive_Chernoff_Bound" Presenting theory "HOL-Algebra.Congruence" Presenting theory "Graph_Theory.Rtrancl_On" Presenting theory "Landau_Symbols.Landau_Simprocs" Presenting theory "ABY3_Protocols.Sharing_Lemmas" Presenting file "$AFP/Landau_Symbols/landau_simprocs.ML" Presenting theory "HOL-Algebra.Order" Presenting theory "Graph_Theory.Stuff" Presenting theory "Landau_Symbols.Landau_More" Presenting theory "HOL-Library.Poly_Mapping" Presenting theory "HOL-Algebra.Lattice" Presenting theory "Stirling_Formula.Stirling_Formula" Presenting theory "HOL-Algebra.Order" Presenting theory "Polynomials.MPoly_Type" Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary" Presenting theory "Graph_Theory.Digraph" Presenting theory "HOL-Computational_Algebra.Squarefree" Presenting theory "Dirichlet_Series.Dirichlet_Misc" Presenting theory "Polynomials.More_MPoly_Type" Presenting theory "HOL-Library.Float" Presenting theory "Dirichlet_Series.Multiplicative_Function" Presenting theory "HOL-Library.List_Lexorder" Presenting theory "HOL-Algebra.Lattice" Presenting theory "TsirelsonBound.Tensor_Mat_Compl_Properties" Presenting theory "Dirichlet_Series.Dirichlet_Product" Presenting theory "HOL-Algebra.Complete_Lattice" Presenting theory "HOL-Computational_Algebra.Polynomial_FPS" Presenting theory "Graph_Theory.Arc_Walk" Presenting theory "Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators" Presenting theory "Graph_Theory.Bidirected_Digraph" Presenting theory "HOL-Number_Theory.Fib" Presenting theory "HOL-Computational_Algebra.Formal_Laurent_Series" Presenting theory "HOL-Algebra.Complete_Lattice" Presenting theory "HOL-Computational_Algebra.Group_Closure" Presenting theory "HOL-Number_Theory.Cong" Presenting theory "HOL-Computational_Algebra.Nth_Powers" Presenting theory "HOL-Computational_Algebra.Computational_Algebra" Presenting theory "HOL-Algebra.Congruence" Presenting theory "Dirichlet_Series.Dirichlet_Series" Presenting theory "HOL-Algebra.Group" Presenting theory "Graph_Theory.Pair_Digraph" Presenting theory "HOL-Algebra.Order" Presenting theory "Dirichlet_Series.Moebius_Mu" Presenting theory "TsirelsonBound.Matrix_L2_Operator_Norm" Presenting theory "ABY3_Protocols.Shuffle" Presenting theory "Finite_Fields.Formal_Polynomial_Derivatives" Presenting theory "ABY3_Protocols.Multiplication" Presenting theory "Finite_Fields.Monic_Polynomial_Factorization" Presenting theory "ABY3_Protocols.Multiplication_Synthesization" Presenting theory "HOL-Algebra.Lattice" Presenting Binary_Code_Imprimitive in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Binary_Code_Imprimitive" ... Presenting document Binary_Code_Imprimitive/document Presenting document Binary_Code_Imprimitive/outline Presenting theory "Finite_Fields.Card_Irreducible_Polynomials_Aux" Presenting theory "Finite_Fields.Card_Irreducible_Polynomials" Presenting theory "Commuting_Hermitian.Commuting_Hermitian" Presenting theory "HOL-Algebra.Group" Presenting Two_Generated_Word_Monoids_Intersection in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Two_Generated_Word_Monoids_Intersection" ... Presenting document Two_Generated_Word_Monoids_Intersection/document Presenting document Two_Generated_Word_Monoids_Intersection/outline Presenting theory "Distributed_Distinct_Elements.Pseudorandom_Combinators" Presenting theory "Discrete_Summation.Factorials" Presenting theory "TsirelsonBound.Density_Matrix_Basics" Presenting theory "HOL-Library.Rewrite" Presenting file "~~/src/HOL/Library/cconv.ML" Presenting file "~~/src/HOL/Library/rewrite.ML" Presenting theory "HOL-Algebra.Complete_Lattice" Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins" Presenting theory "Combinatorics_Words_Graph_Lemma.Glued_Codes" Presenting theory "Binary_Code_Imprimitive.Binary_Square_Interpretation" Presenting theory "Graph_Theory.Digraph_Component" Presenting theory "HOL-Computational_Algebra.Polynomial" Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds" Presenting theory "HOL-Algebra.Coset" Presenting theory "Combinatorics_Words_Graph_Lemma.Glued_Codes" Presenting theory "Polynomials.MPoly_Type_Univariate" Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm" Presenting theory "Jordan_Normal_Form.Missing_Misc" Presenting theory "HOL-Algebra.Group" Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff" Presenting theory "HOL-Algebra.FiniteProduct" Presenting theory "Graph_Theory.Digraph_Isomorphism" Presenting theory "Expander_Graphs.Extra_Congruence_Method" Presenting theory "TsirelsonBound.Tsirelson" Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level" Presenting theory "Polynomial_Interpolation.Ring_Hom" Presenting theory "Expander_Graphs.Expander_Graphs_Multiset_Extras" Presenting Efficient_Weighted_Path_Order in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Efficient_Weighted_Path_Order" ... Presenting document Efficient_Weighted_Path_Order/document Presenting document Efficient_Weighted_Path_Order/outline Presenting theory "Jordan_Normal_Form.Conjugate" Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy" Presenting theory "Two_Generated_Word_Monoids_Intersection.Two_Generated_Word_Monoids_Intersection" Presenting theory "HOL-Computational_Algebra.Fraction_Field" Presenting CommCSL in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CommCSL" ... Presenting document CommCSL/document Presenting document CommCSL/outline Presenting theory "Binary_Code_Imprimitive.Binary_Code_Imprimitive" Presenting theory "CommCSL.PartialMap" Presenting theory "HOL-Algebra.Ring" Presenting CVP_Hardness in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CVP_Hardness" ... Presenting document CVP_Hardness/document Presenting document CVP_Hardness/outline Presenting theory "CVP_Hardness.Reduction" Presenting file "~~/src/HOL/Algebra/ringsimp.ML" Presenting theory "HOL-Computational_Algebra.Normalized_Fraction" Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm" Presenting theory "CommCSL.PosRat" Presenting DigitsInBase in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DigitsInBase" ... Presenting document DigitsInBase/document Presenting document DigitsInBase/outline Presenting theory "HOL-Algebra.Module" Presenting theory "Efficient_Weighted_Path_Order.Indexed_Term" Presenting theory "HOL-Algebra.AbelCoset" Presenting theory "DigitsInBase.DigitsInBase" Presenting Given_Clause_Loops in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Given_Clause_Loops" ... Presenting theory "HOL-Computational_Algebra.Polynomial_Factorial" Presenting document Given_Clause_Loops/document Presenting document Given_Clause_Loops/outline Presenting theory "HOL-Algebra.Ideal" Presenting theory "HOL-Algebra.Coset" Presenting theory "HOL-Algebra.RingHom" Presenting theory "CommCSL.FractionalHeap" Presenting theory "Regular-Sets.Regular_Set" Presenting theory "Regular-Sets.Regular_Exp" Presenting theory "Polynomial_Interpolation.Missing_Unsorted" Presenting theory "Regular-Sets.NDerivative" Presenting theory "Regular-Sets.Equivalence_Checking" Presenting theory "Regular-Sets.Relation_Interpretation" Presenting theory "Regular-Sets.Regexp_Method" Presenting theory "HOL-Algebra.FiniteProduct" Presenting theory "Expander_Graphs.Expander_Graphs_Definition" Presenting theory "Abstract-Rewriting.Seq" Presenting theory "Edwards_Elliptic_Curves_Group.Edwards_Elliptic_Curves_Group" Presenting theory "HOL-Types_To_Sets.Types_To_Sets" Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML" Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML" Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML" Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML" Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML" Presenting theory "Efficient_Weighted_Path_Order.List_Memo_Functions" Presenting theory "Polynomial_Interpolation.Missing_Polynomial" Presenting theory "Abstract-Rewriting.Abstract_Rewriting" Presenting theory "Expander_Graphs.Expander_Graphs_TTS" Presenting theory "HOL-Algebra.UnivPoly" Presenting theory "HOL-Algebra.Ring" Presenting theory "Weighted_Path_Order.Relations" Presenting file "~~/src/HOL/Algebra/ringsimp.ML" Presenting theory "BenOr_Kozen_Reif.More_Matrix" Presenting theory "Efficient_Weighted_Path_Order.WPO_Approx" Presenting theory "HOL-Algebra.Module" Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly" Presenting theory "Weighted_Path_Order.Multiset_Extension_Pair" Presenting theory "Polynomial_Factorization.Order_Polynomial" Presenting theory "HOL-Algebra.Generated_Groups" Presenting theory "Given_Clause_Loops.Given_Clause_Loops_Util" Presenting theory "Given_Clause_Loops.More_Given_Clause_Architectures" Presenting theory "Expander_Graphs.Expander_Graphs_Algebra" Presenting theory "Given_Clause_Loops.DISCOUNT_Loop" Presenting theory "Polynomial_Interpolation.Ring_Hom" Presenting theory "HOL-Algebra.AbelCoset" Presenting theory "CommCSL.StateModel" Presenting theory "Given_Clause_Loops.Prover_Queue" Presenting theory "Jordan_Normal_Form.Missing_Misc" Presenting theory "Jordan_Normal_Form.Missing_Ring" Presenting theory "HOL-Computational_Algebra.Fundamental_Theorem_Algebra" Presenting theory "HOL-Algebra.Elementary_Groups" Presenting theory "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized" Presenting theory "Given_Clause_Loops.Fair_DISCOUNT_Loop" Presenting theory "HOL-Computational_Algebra.Polynomial_FPS" Presenting theory "HOL-Algebra.Ideal" Presenting theory "Given_Clause_Loops.Otter_Loop" Presenting theory "Jordan_Normal_Form.Matrix" Presenting theory "HOL-Algebra.RingHom" Presenting theory "Given_Clause_Loops.Fair_Otter_Loop_Def" Presenting theory "Efficient_Weighted_Path_Order.WPO_Mem_Impl" Presenting theory "Given_Clause_Loops.iProver_Loop" Presenting theory "CVP_Hardness.Lattice_int" Presenting theory "CVP_Hardness.Partition" Presenting theory "HOL-Algebra.Multiplicative_Group" Presenting theory "HOL-Library.More_List" Presenting theory "CommCSL.Lang" Presenting theory "CVP_Hardness.Subset_Sum" Presenting theory "Efficient_Weighted_Path_Order.RPO_Unbounded" Presenting theory "HOL-Number_Theory.Totient" Presenting theory "CVP_Hardness.CVP_p" Presenting theory "Efficient_Weighted_Path_Order.RPO_Mem_Impl" Presenting HyperHoareLogic in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HyperHoareLogic" ... Presenting document HyperHoareLogic/document Presenting document HyperHoareLogic/outline Presenting theory "HOL-Number_Theory.Residues" Presenting theory "Given_Clause_Loops.Fair_iProver_Loop" Presenting theory "Given_Clause_Loops.Fair_Otter_Loop_Complete" Presenting theory "HOL-Number_Theory.Euler_Criterion" Presenting theory "HOL-Computational_Algebra.Polynomial" Presenting theory "HyperHoareLogic.Language" Presenting theory "Given_Clause_Loops.Zipperposition_Loop" Presenting theory "Algebraic_Numbers.Bivariate_Polynomials" Presenting theory "HOL-Number_Theory.Gauss" Presenting theory "HOL-Computational_Algebra.Fraction_Field" Presenting theory "HOL-Computational_Algebra.Normalized_Fraction" Presenting theory "HOL-Algebra.UnivPoly" Presenting theory "HOL-Computational_Algebra.Polynomial_Factorial" Presenting theory "CommCSL.CommCSL" Presenting theory "Polynomial_Interpolation.Missing_Unsorted" Presenting theory "HOL-Computational_Algebra.Formal_Laurent_Series" Presenting theory "HOL-Number_Theory.Quadratic_Reciprocity" Presenting theory "Given_Clause_Loops.Prover_Lazy_List_Queue" Presenting theory "HOL-Computational_Algebra.Group_Closure" Presenting theory "HOL-Algebra.Generated_Groups" Presenting theory "Polynomial_Interpolation.Missing_Polynomial" Presenting theory "Three_Squares.Residues_Properties" Presenting theory "HOL-Computational_Algebra.Nth_Powers" Presenting theory "HOL-Computational_Algebra.Squarefree" Presenting theory "Polynomial_Factorization.Order_Polynomial" Presenting theory "HOL-Computational_Algebra.Computational_Algebra" Presenting theory "Algebraic_Numbers.Resultant" Presenting theory "Symmetric_Polynomials.Vieta" Presenting theory "HOL-Algebra.Elementary_Groups" Presenting theory "HOL-Library.Adhoc_Overloading" Presenting file "~~/src/HOL/Library/adhoc_overloading.ML" Presenting theory "HOL-Computational_Algebra.Fundamental_Theorem_Algebra" Presenting theory "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized" Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly" Presenting theory "Three_Squares.Low_Dimensional_Linear_Algebra" Presenting theory "LLL_Basis_Reduction.Missing_Lemmas" Presenting theory "Symmetric_Polynomials.Symmetric_Polynomials" Presenting theory "Given_Clause_Loops.Fair_Zipperposition_Loop" Presenting theory "Power_Sum_Polynomials.Power_Sum_Polynomials_Library" Presenting theory "LLL_Basis_Reduction.Norms" Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination" Presenting theory "CVP_Hardness.infnorm" Presenting theory "Hermite_Lindemann.More_Multivariate_Polynomial_HLW" Presenting theory "HOL-Algebra.Multiplicative_Group" Presenting theory "Jordan_Normal_Form.Column_Operations" Presenting theory "Three_Squares.Quadratic_Forms" Presenting theory "CVP_Hardness.CVP_vec" Presenting theory "HyperHoareLogic.Logic" Presenting theory "HOL-Library.Ramsey" Presenting theory "CVP_Hardness.Digits_int" Presenting theory "Finitely_Generated_Abelian_Groups.Set_Multiplication" Presenting theory "CVP_Hardness.Additional_Lemmas" Presenting theory "Given_Clause_Loops.Fair_Zipperposition_Loop_without_Ghosts" Presenting theory "Regular-Sets.Regular_Set" Presenting theory "Given_Clause_Loops.Given_Clause_Loops" Presenting MHComputation in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MHComputation" ... Presenting document MHComputation/document Presenting document MHComputation/outline Presenting theory "MHComputation.MHComputation" Presenting theory "Regular-Sets.Regular_Exp" Presenting MLSS_Decision_Proc in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MLSS_Decision_Proc" ... Presenting document MLSS_Decision_Proc/document Presenting document MLSS_Decision_Proc/outline Presenting theory "Finitely_Generated_Abelian_Groups.Miscellaneous_Groups" Presenting theory "MLSS_Decision_Proc.MLSS_Logic" Presenting theory "HOL-Number_Theory.Totient" Presenting theory "Regular-Sets.NDerivative" Presenting theory "Jordan_Normal_Form.Determinant" Presenting theory "HOL-Library.Nat_Bijection" Presenting theory "HOL-Library.While_Combinator" Presenting theory "HyperHoareLogic.Examples" Presenting theory "HOL-Number_Theory.Residues" Presenting theory "Regular-Sets.Equivalence_Checking" Presenting theory "Regular-Sets.Relation_Interpretation" Presenting theory "Regular-Sets.Regexp_Method" Presenting theory "Finitely_Generated_Abelian_Groups.Generated_Groups_Extend" Presenting theory "Jordan_Normal_Form.Char_Poly" Presenting theory "HOL-Number_Theory.Eratosthenes" Presenting theory "Abstract-Rewriting.Seq" Presenting theory "Well_Quasi_Orders.Least_Enum" Presenting theory "HOL-Library.Power_By_Squaring" Presenting theory "HereditarilyFinite.HF" Presenting theory "Well_Quasi_Orders.Infinite_Sequences" Presenting theory "HOL-Number_Theory.Mod_Exp" Presenting theory "HOL-Number_Theory.Euler_Criterion" Presenting theory "Open_Induction.Restricted_Predicates" Presenting theory "HyperHoareLogic.ProgramHyperproperties" Presenting theory "HereditarilyFinite.Ordinal" Presenting theory "Well_Quasi_Orders.Almost_Full" Presenting theory "HOL-Number_Theory.Gauss" Presenting theory "CommCSL.AbstractCommutativity" Presenting theory "HereditarilyFinite.Rank" Presenting theory "MLSS_Decision_Proc.MLSS_HF_Extras" Presenting theory "Well_Quasi_Orders.Minimal_Elements" Presenting theory "HereditarilyFinite.Finitary" Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences" Presenting theory "Graph_Theory.Rtrancl_On" Presenting theory "Well_Quasi_Orders.Almost_Full_Relations" Presenting theory "HOL-Number_Theory.Quadratic_Reciprocity" Presenting theory "Polynomials.Utils" Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form" Presenting theory "HOL-Library.Function_Algebras" Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders" Presenting theory "VectorSpace.RingModuleFacts" Presenting theory "VectorSpace.FunctionLemmas" Presenting theory "HOL-Library.Old_Datatype" Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML" Presenting theory "VectorSpace.MonoidSums" Presenting theory "CVP_Hardness.BHLE" Presenting theory "HOL-Algebra.QuotRing" Presenting theory "Polynomials.Power_Products" Presenting theory "HOL-Library.Countable" Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML" Presenting theory "HOL-Number_Theory.Pocklington" Presenting theory "HOL-Algebra.IntRing" Presenting theory "Polynomials.More_Modules" Presenting theory "VectorSpace.LinearCombinations" Presenting theory "CVP_Hardness.SVP_vec" Presenting No_FTL_observers_Gen_Rel in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/No_FTL_observers_Gen_Rel" ... Presenting theory "HOL-Library.Infinite_Set" Presenting document No_FTL_observers_Gen_Rel/document Presenting document No_FTL_observers_Gen_Rel/outline Presenting theory "Finitely_Generated_Abelian_Groups.General_Auxiliary" Presenting theory "VectorSpace.SumSpaces" Presenting theory "HOL-Number_Theory.Prime_Powers" Presenting theory "No_FTL_observers_Gen_Rel.Sorts" Presenting theory "HOL-Library.Countable_Set" Presenting theory "Polynomials.MPoly_Type_Class" Presenting theory "HOL-Library.Countable_Complete_Lattices" Presenting theory "Finitely_Generated_Abelian_Groups.IDirProds" Presenting theory "No_FTL_observers_Gen_Rel.Points" Presenting theory "Factor_Algebraic_Polynomial.Poly_Connection" Presenting theory "HOL-Number_Theory.Residue_Primitive_Roots" Presenting theory "No_FTL_observers_Gen_Rel.WorldView" Presenting theory "HOL-Number_Theory.Number_Theory" Presenting theory "HOL-Library.Order_Continuity" Presenting theory "Skip_Lists.Pi_pmf" Presenting theory "No_FTL_observers_Gen_Rel.Functions" Presenting theory "No_FTL_observers_Gen_Rel.WorldLine" Presenting theory "HOL-Library.Interval" Presenting theory "Schwartz_Zippel.Schwartz_Zippel" Presenting theory "HOL-Library.Extended_Nat" Presenting theory "CommCSL.Guards" Presenting theory "HOL-Algebra.Congruence" Presenting theory "HOL-Library.Interval_Float" Presenting theory "VectorSpace.VectorSpace" Presenting theory "No_FTL_observers_Gen_Rel.Translations" Presenting theory "HOL-Algebra.Order" Presenting theory "No_FTL_observers_Gen_Rel.AxSelfMinus" Presenting theory "HOL-Algebra.Lattice" Presenting theory "Finitely_Generated_Abelian_Groups.Finite_Product_Extend" Presenting theory "No_FTL_observers_Gen_Rel.TangentLines" Presenting theory "No_FTL_observers_Gen_Rel.Cones" Presenting theory "HOL-Library.Liminf_Limsup" Presenting theory "No_FTL_observers_Gen_Rel.AxLightMinus" Presenting theory "HOL-Algebra.Complete_Lattice" Presenting theory "Finitely_Generated_Abelian_Groups.Group_Hom" Presenting theory "No_FTL_observers_Gen_Rel.Proposition1" Presenting theory "No_FTL_observers_Gen_Rel.AxEField" Presenting theory "No_FTL_observers_Gen_Rel.Norms" Presenting theory "No_FTL_observers_Gen_Rel.AxTriangleInequality" Presenting theory "Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups" Presenting theory "HOL-Algebra.Group" Presenting theory "No_FTL_observers_Gen_Rel.Sublemma3" Presenting theory "HOL-Decision_Procs.Dense_Linear_Order" Presenting theory "HOL-Algebra.FiniteProduct" Presenting theory "Jordan_Normal_Form.Missing_VectorSpace" Presenting file "~~/src/HOL/Decision_Procs/langford_data.ML" Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff_data.ML" Presenting file "~~/src/HOL/Decision_Procs/langford.ML" Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML" Presenting theory "No_FTL_observers_Gen_Rel.Vectors" Presenting theory "HOL-Algebra.Ring" Presenting file "~~/src/HOL/Algebra/ringsimp.ML" Presenting theory "No_FTL_observers_Gen_Rel.CauchySchwarz" Presenting theory "Jordan_Normal_Form.Missing_Ring" Presenting theory "No_FTL_observers_Gen_Rel.Matrices" Presenting theory "Jordan_Normal_Form.Conjugate" Presenting theory "HOL-Algebra.Module" Presenting theory "HyperHoareLogic.Expressivity" Presenting Rensets in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rensets" ... Presenting document Rensets/document Presenting document Rensets/outline Presenting theory "No_FTL_observers_Gen_Rel.LinearMaps" Presenting theory "Finitely_Generated_Abelian_Groups.DirProds" Presenting theory "Jordan_Normal_Form.Matrix" Presenting theory "Jordan_Normal_Form.VS_Connect" Presenting theory "HOL-Library.Extended_Real" Presenting theory "Finitely_Generated_Abelian_Groups.Group_Relations" Presenting theory "No_FTL_observers_Gen_Rel.Affine" Presenting theory "Graph_Theory.Stuff" Presenting theory "No_FTL_observers_Gen_Rel.Sublemma4" Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination" Presenting theory "Rensets.Lambda_Terms" Presenting theory "HOL-Decision_Procs.Approximation_Bounds" Presenting theory "Jordan_Normal_Form.Gram_Schmidt" Presenting theory "Graph_Theory.Digraph" Presenting theory "Jordan_Normal_Form.Column_Operations" Presenting theory "Rensets.Rensets" Presenting theory "HOL-Library.Cancellation" Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML" Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML" Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML" Presenting theory "HOL-Library.Code_Target_Int" Presenting theory "Rensets.Nominal_Sets" Presenting theory "HOL-Library.Code_Abstract_Nat" Presenting theory "Rensets.Rensets_to_Nominal_Sets" Presenting theory "HOL-Library.Code_Target_Nat" Presenting theory "HOL-Library.Code_Target_Numeral" Presenting theory "No_FTL_observers_Gen_Rel.MainLemma" Presenting theory "Lehmer.Lehmer" Presenting theory "Jordan_Normal_Form.Schur_Decomposition" Presenting theory "No_FTL_observers_Gen_Rel.AxDiff" Presenting theory "CommCSL.Safety" Presenting theory "Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups" Presenting theory "Rensets.FRBCE_Rensets" Presenting theory "No_FTL_observers_Gen_Rel.TangentLineLemma" Presenting theory "No_FTL_observers_Gen_Rel.Proposition2" Presenting theory "No_FTL_observers_Gen_Rel.AxEventMinus" Presenting theory "Rensets.Substitutive_Sets" Presenting theory "No_FTL_observers_Gen_Rel.Proposition3" Presenting theory "No_FTL_observers_Gen_Rel.ObserverConeLemma" Presenting theory "Jordan_Normal_Form.Determinant" Presenting theory "Rensets.Examples" Presenting theory "Rensets.All" Presenting theory "Pratt_Certificate.Pratt_Certificate" Presenting Suppes_Theorem in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Suppes_Theorem" ... Presenting document Suppes_Theorem/document Presenting document Suppes_Theorem/outline Presenting theory "No_FTL_observers_Gen_Rel.Quadratics" Presenting file "$AFP/Pratt_Certificate/pratt.ML" Presenting theory "Schwartz_Zippel.Rand_Perfect_Matching" Presenting theory "Propositional_Logic_Class.Implication_Logic" Presenting Probability_Inequality_Completeness in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probability_Inequality_Completeness" ... Presenting document Probability_Inequality_Completeness/document Presenting document Probability_Inequality_Completeness/outline Presenting theory "Propositional_Logic_Class.Classical_Logic" Presenting theory "Propositional_Logic_Class.Classical_Logic_Completeness" Presenting theory "HOL-Library.Cancellation" Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML" Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML" Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML" Presenting theory "No_FTL_observers_Gen_Rel.Classification" Presenting theory "Dirichlet_L.Multiplicative_Characters" Presenting theory "HOL-Number_Theory.Fib" Presenting theory "No_FTL_observers_Gen_Rel.ReverseCauchySchwarz" Presenting theory "Bertrands_Postulate.Bertrand" Presenting theory "HOL-Number_Theory.Eratosthenes" Presenting theory "HOL-Library.Power_By_Squaring" Presenting theory "HOL-Number_Theory.Mod_Exp" Presenting file "$AFP/Bertrands_Postulate/bertrand.ML" Presenting theory "No_FTL_observers_Gen_Rel.KeyLemma" Presenting theory "No_FTL_observers_Gen_Rel.Cardinalities" Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form_Existence" Presenting theory "HOL-Number_Theory.Pocklington" Presenting theory "No_FTL_observers_Gen_Rel.AffineConeLemma" Presenting theory "Frequency_Moments.Frequency_Moments_Preliminary_Results" Presenting theory "HOL-Combinatorics.List_Permutation" Presenting theory "HOL-Number_Theory.Prime_Powers" Presenting theory "No_FTL_observers_Gen_Rel.NoFTLGR" Presenting Tree_Enumeration in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tree_Enumeration" ... Presenting document Tree_Enumeration/document Presenting document Tree_Enumeration/outline Presenting theory "Jordan_Normal_Form.Spectral_Radius" Presenting theory "HOL-Library.Cancellation" Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML" Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML" Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML" Presenting theory "HOL-Number_Theory.Residue_Primitive_Roots" Presenting theory "Perron_Frobenius.Bij_Nat" Presenting theory "HOL-Library.Multiset" Presenting theory "HOL-Number_Theory.Number_Theory" Presenting theory "Dirichlet_Series.Dirichlet_Misc" Presenting file "~~/src/HOL/Library/multiset_simprocs.ML" Presenting theory "Dirichlet_Series.Multiplicative_Function" Presenting theory "Perron_Frobenius.Cancel_Card_Constraint" Presenting file "$AFP/Perron_Frobenius/cancel_card_constraint.ML" Presenting theory "Dirichlet_L.Dirichlet_Characters" Presenting theory "Bernoulli.Bernoulli" Presenting theory "Bernoulli.Periodic_Bernpoly" Presenting theory "HOL-Computational_Algebra.Fraction_Field" Presenting theory "HOL-Computational_Algebra.Fundamental_Theorem_Algebra" Presenting theory "HOL-Computational_Algebra.Group_Closure" Presenting theory "HOL-Library.FuncSet" Presenting theory "HOL-Computational_Algebra.Normalized_Fraction" Presenting theory "HOL-Computational_Algebra.Nth_Powers" Presenting theory "Perron_Frobenius.HMA_Connect" Presenting theory "HOL-Library.Multiset" Presenting theory "HOL-Computational_Algebra.Polynomial_Factorial" Presenting theory "HOL-Algebra.Divisibility" Presenting file "~~/src/HOL/Library/multiset_simprocs.ML" Presenting theory "Isabelle_Marries_Dirac.Basics" Presenting theory "HOL-Computational_Algebra.Squarefree" Presenting theory "HOL-Computational_Algebra.Computational_Algebra" Presenting theory "HOL-Combinatorics.Stirling" Presenting theory "HOL-Library.Disjoint_Sets" Presenting theory "Isabelle_Marries_Dirac.Binary_Nat" Presenting theory "HOL-Combinatorics.Transposition" Presenting theory "Bernoulli.Bernoulli_FPS" Presenting theory "HOL-Library.FuncSet" Presenting theory "HOL-Library.Multiset" Presenting file "~~/src/HOL/Library/multiset_simprocs.ML" Presenting theory "HOL-Library.Disjoint_Sets" Presenting theory "Euler_MacLaurin.Euler_MacLaurin" Presenting theory "HOL-Algebra.QuotRing" Presenting theory "HOL-Library.Old_Datatype" Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML" Presenting theory "Bernoulli.Bernoulli_Zeta" Presenting theory "HOL-Library.Going_To_Filter" Presenting theory "HOL-Library.Nat_Bijection" Presenting theory "HOL-Library.FuncSet" Presenting theory "HOL-Combinatorics.Permutations" Presenting theory "HOL-Library.Countable" Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML" Presenting theory "HOL-Algebra.Ring_Divisibility" Presenting theory "Graph_Theory.Bidirected_Digraph" Presenting theory "Isabelle_Marries_Dirac.Quantum" Presenting theory "HOL-Library.Infinite_Set" Presenting theory "HOL-Library.Disjoint_Sets" Presenting theory "HOL-Algebra.Subrings" Presenting theory "Isabelle_Marries_Dirac.Complex_Vectors" Presenting theory "HOL-Combinatorics.Transposition" Presenting theory "HOL-Library.Countable_Set" Presenting theory "Graph_Theory.Arc_Walk" Presenting theory "HOL-Library.Countable_Complete_Lattices" Presenting theory "Matrix.Utility" Presenting theory "Probability_Inequality_Completeness.Probability_Inequality_Completeness" Presenting theory "HOL-Library.Order_Continuity" Presenting theory "Graph_Theory.Pair_Digraph" Presenting theory "HOL-Library.Extended_Nat" Presenting theory "Regular-Sets.Regular_Set" Presenting theory "Regular-Sets.Regular_Exp" Presenting theory "HOL-Library.Liminf_Limsup" Presenting theory "Regular-Sets.NDerivative" Presenting theory "HOL-Combinatorics.Permutations" Presenting theory "HOL-Combinatorics.List_Permutation" Presenting theory "Graph_Theory.Digraph_Component" Presenting theory "HOL-Library.While_Combinator" Presenting theory "Regular-Sets.Equivalence_Checking" Presenting theory "Graph_Theory.Vertex_Walk" Presenting theory "Regular-Sets.Relation_Interpretation" Presenting theory "Graph_Theory.Digraph_Component_Vwalk" Presenting theory "HOL-Algebra.Polynomials" Presenting theory "Regular-Sets.Regexp_Method" Presenting theory "Propositional_Logic_Class.List_Utilities" Presenting theory "Abstract-Rewriting.Seq" Presenting theory "HOL-Library.BNF_Corec" Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML" Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML" Presenting theory "Graph_Theory.Digraph_Isomorphism" Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML" Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML" Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML" Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML" Presenting theory "HOL-Real_Asymp.Lazy_Eval" Presenting file "~~/src/HOL/Real_Asymp/lazy_eval.ML" Presenting theory "HOL-Real_Asymp.Inst_Existentials" Presenting file "~~/src/HOL/Real_Asymp/inst_existentials.ML" Presenting theory "HOL-Real_Asymp.Eventuallize" Presenting theory "Propositional_Logic_Class.Classical_Connectives" Presenting theory "HOL-Combinatorics.Orbits" Presenting theory "HOL-Algebra.Embedded_Algebras" Presenting theory "Graph_Theory.Auxiliary" Presenting theory "Graph_Theory.Subdivision" Presenting theory "HOL-Library.Old_Datatype" Presenting theory "HOL-Library.Extended_Real" Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML" Presenting theory "HOL-Library.Nat_Bijection" Presenting theory "Graph_Theory.Euler" Presenting theory "Girth_Chromatic.Girth_Chromatic_Misc" Presenting theory "HOL-Library.Countable" Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML" Presenting theory "Suppes_Theorem.Probability_Logic" Presenting theory "Undirected_Graph_Theory.Undirected_Graph_Basics" Presenting theory "HOL-Library.Rewrite" Presenting file "~~/src/HOL/Library/cconv.ML" Presenting file "~~/src/HOL/Library/rewrite.ML" Presenting theory "HOL-Algebra.Polynomial_Divisibility" Presenting theory "Suppes_Theorem.Suppes_Theorem" Presenting theory "Undirected_Graph_Theory.Undirected_Graph_Walks" Presenting theory "HOL-Real_Asymp.Multiseries_Expansion" Presenting theory "Abstract-Rewriting.Abstract_Rewriting" Presenting theory "Undirected_Graph_Theory.Connectivity" Presenting theory "Finite_Fields.Finite_Fields_Preliminary_Results" Presenting theory "Graph_Theory.Kuratowski" Presenting theory "Undirected_Graph_Theory.Girth_Independence" Presenting file "~~/src/HOL/Real_Asymp/asymptotic_basis.ML" Presenting file "~~/src/HOL/Real_Asymp/exp_log_expression.ML" Presenting file "~~/src/HOL/Real_Asymp/expansion_interface.ML" Presenting file "~~/src/HOL/Real_Asymp/multiseries_expansion.ML" Presenting theory "HOL-Combinatorics.Transposition" Presenting theory "Graph_Theory.Weighted_Graph" Presenting file "~~/src/HOL/Real_Asymp/real_asymp.ML" Presenting theory "Finite_Fields.Finite_Fields_Factorization_Ext" Presenting theory "Graph_Theory.Shortest_Path" Presenting theory "Graph_Theory.Graph_Theory" Presenting theory "Abstract-Rewriting.SN_Orders" Presenting theory "HOL-Algebra.IntRing" Presenting theory "MLSS_Decision_Proc.MLSS_Realisation" Presenting theory "Matrix.Ordered_Semiring" Presenting theory "HOL-Library.Adhoc_Overloading" Presenting file "~~/src/HOL/Library/adhoc_overloading.ML" Presenting theory "MLSS_Decision_Proc.MLSS_Semantics" Presenting theory "Finite_Fields.Ring_Characteristic" Presenting theory "HOL-Real_Asymp.Multiseries_Expansion_Bounds" Presenting file "~~/src/HOL/Real_Asymp/multiseries_expansion_bounds.ML" Presenting theory "Universal_Hash_Families.Field" Presenting theory "Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials" Presenting theory "HOL-Real_Asymp.Real_Asymp" Presenting file "~~/src/HOL/Real_Asymp/real_asymp_diag.ML" Presenting theory "HOL-Combinatorics.Permutations" Presenting theory "Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation" Presenting theory "Dirichlet_Series.Dirichlet_Product" Presenting theory "HOL-Library.Sublist" Presenting theory "Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities" Presenting theory "Matrix.Matrix_Legacy" Presenting theory "MLSS_Decision_Proc.MLSS_Typing_Defs" Presenting theory "Frequency_Moments.Frequency_Moments" Presenting theory "HOL-Combinatorics.Multiset_Permutations" Presenting theory "Dirichlet_Series.Dirichlet_Series" Presenting theory "Undirected_Graph_Theory.Graph_Triangles" Presenting theory "Dirichlet_Series.Moebius_Mu" Presenting theory "MLSS_Decision_Proc.MLSS_Calculus" Presenting theory "Dirichlet_Series.More_Totient" Presenting theory "Dirichlet_Series.Liouville_Lambda" Presenting theory "Median_Method.Median" Presenting theory "Dirichlet_Series.Divisor_Count" Presenting theory "Undirected_Graph_Theory.Bipartite_Graphs" Presenting theory "Dirichlet_Series.Arithmetic_Summatory" Presenting theory "Dirichlet_Series.Partial_Summation" Presenting theory "Frequency_Moments.K_Smallest" Presenting theory "MLSS_Decision_Proc.MLSS_Typing" Presenting theory "Universal_Hash_Families.Definitions" Presenting theory "Dirichlet_Series.Euler_Products" Presenting theory "Universal_Hash_Families.Preliminary_Results" Presenting theory "Card_Partitions.Set_Partition" Presenting theory "Universal_Hash_Families.Carter_Wegman_Hash_Family" Presenting theory "Dirichlet_Series.Dirichlet_Series_Analysis" Presenting theory "HOL-Library.Multiset_Order" Presenting theory "Sturm_Tarski.PolyMisc" Presenting theory "HOL-Computational_Algebra.Field_as_Ring" Presenting theory "Sturm_Tarski.Sturm_Tarski" Presenting theory "HOL-Library.Landau_Symbols" Presenting theory "MLSS_Decision_Proc.MLSS_Proc" Presenting theory "Winding_Number_Eval.Missing_Topology" Presenting theory "Fresh_Identifiers.Fresh" Presenting theory "Frequency_Moments.Landau_Ext" Presenting theory "Budan_Fourier.BF_Misc" Presenting theory "HOL-Library.Sublist" Presenting theory "Winding_Number_Eval.Missing_Algebraic" Presenting theory "Frequency_Moments.Probability_Ext" Presenting theory "MLSS_Decision_Proc.MLSS_Suc_Theory" Presenting theory "Winding_Number_Eval.Missing_Transcendental" Presenting theory "Frequency_Moments.Product_PMF_Ext" Presenting theory "Winding_Number_Eval.Missing_Analysis" Presenting theory "MLSS_Decision_Proc.MLSS_Typing_Urelems" Presenting theory "Fresh_Identifiers.Fresh_Nat" Presenting theory "Nested_Multisets_Ordinals.Multiset_More" Presenting theory "Nested_Multisets_Ordinals.Duplicate_Free_Multiset" Presenting theory "CommCSL.Soundness" Presenting theory "List-Index.List_Index" Presenting theory "CommCSL.NonInterference" Presenting theory "Frequency_Moments.Frequency_Moment_0" Presenting theory "MLSS_Decision_Proc.MLSS_Proc_Code" Presenting theory "Design_Theory.Multisets_Extras" Presenting theory "MLSS_Decision_Proc.MLSS_Proc_All" Presenting theory "HOL-Combinatorics.Stirling" Presenting theory "Design_Theory.Design_Basics" Presenting theory "Winding_Number_Eval.Cauchy_Index_Theorem" Presenting theory "Card_Partitions.Set_Partition" Presenting theory "Design_Theory.Design_Operations" Presenting theory "Design_Theory.Block_Designs" Presenting theory "Design_Theory.BIBD" Presenting theory "Design_Theory.Resolvable_Designs" 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 "Card_Partitions.Injectivity_Solver" 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 "Card_Partitions.Card_Partitions" Presenting theory "HOL-Eisbach.Eisbach_Tools" Presenting theory "Design_Theory.Group_Divisible_Designs" Presenting theory "Bell_Numbers_Spivey.Bell_Numbers" Presenting theory "Undirected_Graph_Theory.Graph_Theory_Relations" Presenting theory "Undirected_Graph_Theory.Undirected_Graphs_Root" Presenting theory "Card_Equiv_Relations.Card_Equiv_Relations" Presenting theory "Equivalence_Relation_Enumeration.Equivalence_Relation_Enumeration" Presenting theory "Tree_Enumeration.Tree_Graph" Presenting theory "Winding_Number_Eval.Winding_Number_Eval" Presenting theory "Tree_Enumeration.Labeled_Tree_Enumeration" Presenting theory "Frequency_Moments.Frequency_Moment_2" Presenting theory "HOL-Library.Function_Algebras" Presenting theory "Zeta_Function.Zeta_Library" Presenting theory "Pure-ex.Guess" Presenting theory "Matrix_Tensor.Matrix_Tensor" Presenting theory "HOL-Library.FSet" Presenting theory "Ergodic_Theory.SG_Library_Complement" Presenting theory "Isabelle_Marries_Dirac.Tensor" Presenting theory "Lp.Functional_Spaces" Presenting theory "Zeta_Function.Zeta_Function" Presenting theory "Tree_Enumeration.Rooted_Tree" Presenting theory "Isabelle_Marries_Dirac.More_Tensor" Presenting theory "Tree_Enumeration.Rooted_Tree_Enumeration" Presenting theory "Dirichlet_L.Dirichlet_L_Functions" Presenting theory "HOL-Library.Lattice_Algebras" Presenting theory "HOL-Library.Interval" Presenting theory "QHLProver.Complex_Matrix" Presenting theory "HOL-Library.Log_Nat" Presenting file "$AFP/QHLProver/mat_alg.ML" Presenting theory "HOL-Library.Float" Presenting theory "QHLProver.Gates" Presenting theory "HOL-Types_To_Sets.Prerequisites" Presenting theory "HOL-Library.Interval_Float" Presenting theory "Frequency_Moments.Frequency_Moment_k" Presenting theory "HOL-Types_To_Sets.Group_On_With" Presenting theory "HOL-Decision_Procs.Dense_Linear_Order" Presenting file "~~/src/HOL/Decision_Procs/langford_data.ML" Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff_data.ML" Presenting file "~~/src/HOL/Decision_Procs/langford.ML" Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML" Presenting theory "Projective_Measurements.Linear_Algebra_Complements" Presenting theory "HOL-Decision_Procs.Approximation_Bounds" Presenting theory "Projective_Measurements.Projective_Measurements" Presenting theory "HOL-Library.Code_Target_Int" Presenting theory "HOL-Library.Code_Abstract_Nat" Presenting theory "HOL-Library.Code_Target_Nat" Presenting theory "HOL-Library.Code_Target_Numeral" Presenting theory "Lehmer.Lehmer" Presenting theory "Commuting_Hermitian.Spectral_Theory_Complements" Presenting theory "Pratt_Certificate.Pratt_Certificate" Presenting file "$AFP/Pratt_Certificate/pratt.ML" Presenting theory "Commuting_Hermitian.Commuting_Hermitian_Misc" Presenting theory "Bertrands_Postulate.Bertrand" Presenting file "$AFP/Bertrands_Postulate/bertrand.ML" Presenting theory "HOL-Library.Function_Algebras" Presenting theory "Landau_Symbols.Group_Sort" Presenting theory "Commuting_Hermitian.Commuting_Hermitian" Presenting theory "Landau_Symbols.Landau_Real_Products" Presenting theory "Landau_Symbols.Landau_Simprocs" Presenting file "$AFP/Landau_Symbols/landau_simprocs.ML" Presenting theory "Landau_Symbols.Landau_More" Presenting theory "Dirichlet_L.Dirichlet_Theorem" Presenting theory "Expander_Graphs.Expander_Graphs_Eigenvalues" Presenting theory "Three_Squares.Three_Squares" Presenting theory "Expander_Graphs.Expander_Graphs_Cheeger_Inequality" Presenting theory "HOL-Library.Code_Target_Numeral_Float" Presenting theory "HOL-Decision_Procs.Approximation" Presenting file "~~/src/HOL/Decision_Procs/approximation.ML" Presenting file "~~/src/HOL/Decision_Procs/approximation_generator.ML" Presenting theory "Expander_Graphs.Expander_Graphs_MGG" Presenting theory "Expander_Graphs.Expander_Graphs_Walks" Presenting theory "Expander_Graphs.Expander_Graphs_Power_Construction" Presenting theory "Expander_Graphs.Expander_Graphs_Strongly_Explicit"
Group AFP: 0:50:40 elapsed time, 2:57:49 cpu time, factor 3.51 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:19:08 elapsed time, 2:57:49 cpu time, factor 9.29
using [/media/data/jenkins/workspace/isabelle-all/bin/isabelle] Preparing site generation in out/hugo Cleaning up generated files... Build in /media/data/jenkins/workspace/isabelle-all/afp/web/index.html
Build step 'Execute shell' marked build as failure ERROR: Failed to evaluate groovy script. java.lang.InterruptedException at java.base/java.lang.Object.wait(Native Method) at hudson.remoting.Request$1.get(Request.java:318) at hudson.remoting.Request$1.get(Request.java:240) at hudson.remoting.FutureAdapter.get(FutureAdapter.java:66) at hudson.FilePath.copyRecursiveTo(FilePath.java:2831) at hudson.FilePath.copyRecursiveTo(FilePath.java:2792) at hudson.FilePath.copyRecursiveTo(FilePath.java:2780) at hudson.FilePath.copyRecursiveTo(FilePath.java:2763) at hudson.FilePath.copyRecursiveTo(FilePath.java:2748) at hudson.FilePath$copyRecursiveTo$2.call(Unknown Source) at org.codehaus.groovy.runtime.callsite.CallSiteArray.defaultCall(CallSiteArray.java:47) at org.codehaus.groovy.runtime.callsite.AbstractCallSite.call(AbstractCallSite.java:116) at org.codehaus.groovy.runtime.callsite.AbstractCallSite.call(AbstractCallSite.java:128) at Script1.run(Script1.groovy:17) at groovy.lang.GroovyShell.evaluate(GroovyShell.java:574) at groovy.lang.GroovyShell.evaluate(GroovyShell.java:612) at groovy.lang.GroovyShell.evaluate(GroovyShell.java:583) at org.jenkinsci.plugins.scriptsecurity.sandbox.groovy.SecureGroovyScript.evaluate(SecureGroovyScript.java:450) at org.jenkinsci.plugins.scriptsecurity.sandbox.groovy.SecureGroovyScript.evaluate(SecureGroovyScript.java:387) at org.jvnet.hudson.plugins.groovypostbuild.GroovyPostbuildRecorder.perform(GroovyPostbuildRecorder.java:406) at hudson.tasks.BuildStepMonitor$1.perform(BuildStepMonitor.java:20) at hudson.model.AbstractBuild$AbstractBuildExecution.perform(AbstractBuild.java:818) at hudson.model.AbstractBuild$AbstractBuildExecution.performAllBuildSteps(AbstractBuild.java:767) at hudson.model.Build$BuildExecution.post2(Build.java:179) at hudson.model.AbstractBuild$AbstractBuildExecution.post(AbstractBuild.java:711) at hudson.model.Run.execute(Run.java:1925) at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44) at hudson.model.ResourceController.execute(ResourceController.java:101) at hudson.model.Executor.run(Executor.java:442) Build step 'Groovy Postbuild' marked build as failure Started calculate disk usage of build Finished Calculation of disk usage of build in 0 seconds Email was triggered for: Failure - 1st Trigger Failure - Any was overridden by another trigger and will not send an email. Trigger Failure - Still was overridden by another trigger and will not send an email. Sending email for trigger: Failure - 1st Sending email to: isabelle-ci@mailman46.in.tum.de ERROR: Could not send email as a part of the post-build publishers. java.lang.IllegalStateException: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong. at jenkins.model.Jenkins.get(Jenkins.java:814) at hudson.plugins.emailext.plugins.EmailTrigger.getDescriptor(EmailTrigger.java:144) at hudson.plugins.emailext.ExtendedEmailPublisher.getRuntimeMacros(ExtendedEmailPublisher.java:671) at hudson.plugins.emailext.ExtendedEmailPublisher.executeScript(ExtendedEmailPublisher.java:695) at hudson.plugins.emailext.ExtendedEmailPublisher.executePostsendScript(ExtendedEmailPublisher.java:683) at hudson.plugins.emailext.ExtendedEmailPublisher.sendMail(ExtendedEmailPublisher.java:641) at hudson.plugins.emailext.ExtendedEmailPublisher._perform(ExtendedEmailPublisher.java:484) at hudson.plugins.emailext.ExtendedEmailPublisher.perform(ExtendedEmailPublisher.java:385) at hudson.tasks.BuildStepMonitor$1.perform(BuildStepMonitor.java:20) at hudson.model.AbstractBuild$AbstractBuildExecution.perform(AbstractBuild.java:818) at hudson.model.AbstractBuild$AbstractBuildExecution.performAllBuildSteps(AbstractBuild.java:767) at hudson.model.Build$BuildExecution.cleanUp(Build.java:189) at hudson.model.Run.execute(Run.java:1947) at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44) at hudson.model.ResourceController.execute(ResourceController.java:101) at hudson.model.Executor.run(Executor.java:442) ERROR: Build step failed with exception java.lang.IllegalStateException: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong. at jenkins.model.Jenkins.get(Jenkins.java:814) at hudson.plugins.emailext.ExtendedEmailPublisher.getDescriptor(ExtendedEmailPublisher.java:1194) at hudson.plugins.emailext.ExtendedEmailPublisher.debug(ExtendedEmailPublisher.java:367) at hudson.plugins.emailext.ExtendedEmailPublisher.sendMail(ExtendedEmailPublisher.java:663) at hudson.plugins.emailext.ExtendedEmailPublisher._perform(ExtendedEmailPublisher.java:484) at hudson.plugins.emailext.ExtendedEmailPublisher.perform(ExtendedEmailPublisher.java:385) at hudson.tasks.BuildStepMonitor$1.perform(BuildStepMonitor.java:20) at hudson.model.AbstractBuild$AbstractBuildExecution.perform(AbstractBuild.java:818) at hudson.model.AbstractBuild$AbstractBuildExecution.performAllBuildSteps(AbstractBuild.java:767) at hudson.model.Build$BuildExecution.cleanUp(Build.java:189) at hudson.model.Run.execute(Run.java:1947) at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44) at hudson.model.ResourceController.execute(ResourceController.java:101) at hudson.model.Executor.run(Executor.java:442) ERROR: Post-build steps failed java.lang.IllegalStateException: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong. at jenkins.model.Jenkins.get(Jenkins.java:814) at hudson.plugins.emailext.ExtendedEmailPublisher.getDescriptor(ExtendedEmailPublisher.java:1194) at hudson.plugins.emailext.ExtendedEmailPublisher.getDescriptor(ExtendedEmailPublisher.java:102) at hudson.model.AbstractBuild$AbstractBuildExecution.reportError(AbstractBuild.java:786) at hudson.model.AbstractBuild$AbstractBuildExecution.performAllBuildSteps(AbstractBuild.java:775) at hudson.model.Build$BuildExecution.cleanUp(Build.java:189) at hudson.model.Run.execute(Run.java:1947) at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44) at hudson.model.ResourceController.execute(ResourceController.java:101) at hudson.model.Executor.run(Executor.java:442) FATAL: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong. java.lang.IllegalStateException: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong. at jenkins.model.Jenkins.get(Jenkins.java:814) at hudson.tasks.BuildTrigger.execute(BuildTrigger.java:274) at hudson.model.AbstractBuild$AbstractBuildExecution.cleanUp(AbstractBuild.java:728) at hudson.model.Build$BuildExecution.cleanUp(Build.java:194) at hudson.model.Run.execute(Run.java:1947) at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44) at hudson.model.ResourceController.execute(ResourceController.java:101)