Started by an SCM change
[EnvInject] - Loading node environment variables.
Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-all
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
pulling from http://isabelle.in.tum.de/repos/isabelle/
no changes found
[isabelle-all] $ hg update --clean --rev default
12 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 9497a6334a26752d09d58b7b934d639ea8f9e846 --template exists\n
exists
[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(9497a6334a26752d09d58b7b934d639ea8f9e846)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
[afp] $ hg pull --rev default
pulling from https://bitbucket.org/isa-afp/afp-devel/
no changes found
[afp] $ hg update --clean --rev default
478 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 ec3ff55171a95c2b44120d974b239e8d9bbcf65f --template exists\n
exists
[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(ec3ff55171a95c2b44120d974b239e8d9bbcf65f)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-all] $ /bin/sh -xe /tmp/jenkins8686717715024695347.sh
+ Admin/jenkins/run_build all
+ set -e
+ PROFILE=all
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
+ bin/isabelle ocaml_setup
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
       opam update

[NOTE] Package zarith is already installed (current version is 1.7).
+ bin/isabelle ghc_setup
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
The Glorious Glasgow Haskell Compilation System, version 8.4.4
+ bin/isabelle ci_build_all

=== CONFIGURATION ===

ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64_32-linux"
ML_SYSTEM="polyml-5.8"
ML_OPTIONS="-H 4000 --maxheap 8G"
jobs = 10, threads = 4, numa = false

=== BUILD ===

Build started at Sat, 22 Jun 2019 13:45:02 GMT
Isabelle id 4a327c061870
AFP id ec3ff55171a9

=== LOG ===

Session Pure/Pure
Session CTT/CTT
Session Cube/Cube
Session FOL/FOL
Session CCL/CCL
Session FOL/FOL-ex
Session FOLP/FOLP
Session FOLP/FOLP-ex
Session HOL/HOL (main)
Session AFP/AVL-Trees (AFP)
Session AFP/AWN (AFP)
Session AFP/Abortable_Linearizable_Modules (AFP)
Session AFP/Abstract-Hoare-Logics (AFP)
Session AFP/AnselmGod (AFP)
Session AFP/AxiomaticCategoryTheory (AFP)
Session AFP/BinarySearchTree (AFP)
Session AFP/Binomial-Queues (AFP)
Session AFP/Bondy (AFP)
Session AFP/Bounded_Deducibility_Security (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/CISC-Kernel (AFP)
Session AFP/CYK (AFP)
Session AFP/Cauchy (AFP)
Session AFP/Sqrt_Babylonian (AFP)
Session Doc/Classes (doc)
Session AFP/ClockSynchInst (AFP)
Session AFP/Compiling-Exceptions-Correctly (AFP)
Session AFP/ComponentDependencies (AFP)
Session AFP/Concurrent_Revisions (AFP)
Session AFP/Constructor_Funs (AFP)
Session AFP/CryptoBasedCompositionalProperties (AFP)
Session AFP/DPT-SAT-Solver (AFP)
Session AFP/Depth-First-Search (AFP)
Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
Session AFP/DiskPaxos (AFP)
Session AFP/Example-Submission (AFP)
Session AFP/FFT (AFP)
Session AFP/FLP (AFP)
Session AFP/FeatherweightJava (AFP)
Session AFP/Featherweight_OCL (AFP)
Session AFP/FileRefinement (AFP)
Session AFP/FocusStreamsCaseStudies (AFP)
Session AFP/Free-Boolean-Algebra (AFP)
Session AFP/FunWithFunctions (AFP)
Session AFP/FunWithTilings (AFP)
Session Doc/Functions (doc)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/GenClock (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/Generic_Deriving (AFP)
Session AFP/GewirthPGCProof (AFP)
Session AFP/GoedelGod (AFP)
Session HOL/HOL-Cardinals (timing)
Session AFP/Binding_Syntax_Theory (AFP)
Session AFP/Ordinals_and_Cardinals (AFP)
Session HOL/HOL-Eisbach
Session AFP/Allen_Calculus (AFP)
Session AFP/Dependent_SIFUM_Type_Systems (AFP)
Session AFP/Dependent_SIFUM_Refinement (AFP)
Session Doc/Eisbach (doc)
Session HOL/HOL-Hoare
Session AFP/Case_Labeling (AFP)
Session HOL/HOL-Hoare_Parallel (timing)
Session HOL/HOL-IMPP
Session HOL/HOL-IOA
Session HOL/HOL-Import
Session HOL/HOL-Lattice
Session HOL/HOL-Library (main timing)
Session AFP/ArrowImpossibilityGS (AFP)
Session AFP/Auto2_HOL (AFP)
Session AFP/BNF_CC (AFP)
Session AFP/BNF_Operations (AFP)
Session AFP/Binomial-Heaps (AFP)
Session AFP/Boolean_Expression_Checkers (AFP)
Session AFP/Buildings (AFP)
Session AFP/CRDT (AFP)
Session AFP/IMAP-CRDT (AFP)
Session AFP/Card_Multisets (AFP)
Session AFP/Card_Number_Partitions (AFP)
Session AFP/Category (AFP)
Session AFP/Category3 (AFP)
Session AFP/MonoidalCategory (AFP)
Session Doc/Codegen (doc)
Session AFP/CofGroups (AFP)
Session AFP/Completeness (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/Concurrent_Ref_Alg (AFP)
Session AFP/CoreC++ (AFP)
Session AFP/Core_DOM (AFP)
Session Doc/Datatypes (doc)
Session Doc/Corec (doc)
Session AFP/Decl_Sem_Fun_PL (AFP)
Session AFP/Derangements (AFP)
Session AFP/Discrete_Summation (AFP)
Session AFP/Card_Partitions (AFP)
Session AFP/Bell_Numbers_Spivey (AFP)
Session AFP/Card_Equiv_Relations (AFP)
Session AFP/Efficient-Mergesort (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Epistemic_Logic (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/FOL-Fitting (AFP)
Session AFP/FOL_Harrison (AFP)
Session AFP/Factored_Transition_System_Bounding (AFP)
Session AFP/Falling_Factorial_Sum (AFP)
Session AFP/FinFun (AFP)
Session AFP/Finger-Trees (AFP)
Session AFP/Graph_Saturation (AFP)
Session AFP/Graph_Theory (AFP)
Session AFP/ShortestPath (AFP)
Session AFP/Group-Ring-Module (AFP)
Session AFP/Valuation (AFP)
Session HOL/HOL-Auth (timing)
Session HOL/HOL-UNITY (timing)
Session HOL/HOL-Bali (timing)
Session HOL/HOL-Computational_Algebra (main timing)
Session AFP/Descartes_Sign_Rule (AFP)
Session HOL/HOL-Algebra (main timing)
Session HOL/HOL-Decision_Procs (timing)
Session HOL/HOL-Quotient_Examples (timing)
Session AFP/Localization_Ring (AFP)
Session AFP/Orbit_Stabiliser (AFP)
Session AFP/Perfect-Number-Thm (AFP)
Session AFP/Secondary_Sylow (AFP)
Session AFP/Jordan_Hoelder (AFP)
Session AFP/VectorSpace (AFP)
Session HOL/HOL-Analysis (main timing)
Session AFP/Bernoulli (AFP)
Session AFP/Cartan_FP (AFP)
Session AFP/Cayley_Hamilton (AFP)
Session AFP/Coinductive (AFP)
Session AFP/DynamicArchitectures (AFP)
Session AFP/Architectural_Design_Patterns (AFP)
Session AFP/Lazy-Lists-II (AFP)
Session AFP/Stream_Fusion_Code (AFP)
Session AFP/Topology (AFP)
Session AFP/First_Welfare_Theorem (AFP)
Session AFP/Green (AFP)
Session HOL/HOL-Analysis-ex
Session HOL/HOL-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/Fisher_Yates (AFP)
Session AFP/Girth_Chromatic (AFP)
Session AFP/Random_Graph_Subgraph_Threshold (AFP)
Session HOL/HOL-Probability-ex (timing)
Session AFP/Lp (AFP)
Session AFP/Markov_Models (AFP)
Session AFP/Monad_Normalisation (AFP)
Session AFP/Monomorphic_Monad (AFP)
Session AFP/Neumann_Morgenstern_Utility (AFP)
Session AFP/Probabilistic_Noninterference (AFP)
Session AFP/Probabilistic_System_Zoo (AFP)
Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)
Session AFP/Source_Coding_Theorem (AFP)
Session AFP/Irrationality_J_Hancl (AFP)
Session AFP/Kuratowski_Closure_Complement (AFP)
Session AFP/Lower_Semicontinuous (AFP)
Session AFP/Minkowskis_Theorem (AFP)
Session AFP/Octonions (AFP)
Session AFP/Probabilistic_System_Zoo-BNFs (AFP)
Session AFP/Ptolemys_Theorem (AFP)
Session AFP/Quaternions (AFP)
Session AFP/Rank_Nullity_Theorem (AFP)
Session AFP/Gauss_Jordan (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/Hermite (AFP)
Session AFP/Tarskis_Geometry (AFP)
Session AFP/Triangle (AFP)
Session AFP/Chord_Segments (AFP)
Session AFP/Stewart_Apollonius (AFP)
Session AFP/pGCL (AFP)
Session HOL/HOL-Isar_Examples
Session HOL/HOL-Nonstandard_Analysis (timing)
Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
Session HOL/HOL-Number_Theory (main timing)
Session AFP/E_Transcendental (AFP)
Session AFP/Elliptic_Curves_Group_Law (AFP)
Session AFP/Fermat3_4 (AFP)
Session HOL/HOL-Data_Structures (timing)
Session HOL/HOL-ex (timing)
Session AFP/Automatic_Refinement (AFP)
Session HOL/HOL-Codegenerator_Test
Session AFP/Lehmer (AFP)
Session AFP/Pratt_Certificate (AFP)
Session AFP/Bertrands_Postulate (AFP)
Session AFP/Prime_Harmonic_Series (AFP)
Session AFP/RSAPSS (AFP)
Session AFP/SumSquares (AFP)
Session AFP/Liouville_Numbers (AFP)
Session AFP/Mason_Stothers (AFP)
Session AFP/Polynomial_Interpolation (AFP)
Session AFP/Probabilistic_Prime_Tests (AFP)
Session AFP/Rep_Fin_Groups (AFP)
Session AFP/Sturm_Sequences (AFP)
Session AFP/Special_Function_Bounds (AFP)
Session AFP/Sturm_Tarski (AFP)
Session AFP/Budan_Fourier (AFP)
Session AFP/Winding_Number_Eval (AFP)
Session AFP/Count_Complex_Roots (AFP)
Session HOL/HOL-Corec_Examples (timing)
Session HOL/HOL-Datatype_Examples (timing)
Session HOL/HOL-Hahn_Banach
Session HOL/HOL-IMP (timing)
Session AFP/Abs_Int_ITP2012 (AFP)
Session HOL/HOL-Imperative_HOL (timing)
Session AFP/Auto2_Imperative_HOL (AFP)
Session AFP/Imperative_Insertion_Sort (AFP)
Session HOL/HOL-Induct
Session HOL/HOL-Matrix_LP
Session HOL/HOL-Metis_Examples (timing)
Session HOL/HOL-MicroJava (timing)
Session HOL/HOL-Mutabelle
Session HOL/HOL-Nitpick_Examples
Session HOL/HOL-Nominal
Session AFP/CCS (AFP)
Session HOL/HOL-Nominal-Examples (timing)
Session AFP/Lam-ml-Normalization (AFP)
Session AFP/Pi_Calculus (AFP)
Session AFP/Psi_Calculi (AFP)
Session AFP/SequentInvertibility (AFP)
Session HOL/HOL-Predicate_Compile_Examples (timing)
Session HOL/HOL-Quickcheck_Examples (timing)
Session HOL/HOL-SET_Protocol (timing)
Session HOL/HOL-TPTP
Session HOL/HOL-Unix
Session HOL/HOL-ZF
Session AFP/Category2 (AFP)
Session AFP/HereditarilyFinite (AFP)
Session AFP/HyperCTL (AFP)
Session AFP/Integration (AFP)
Session AFP/Isabelle_Meta_Model (AFP)
Session AFP/LTL (AFP)
Session AFP/Stuttering_Equivalence (AFP)
Session AFP/Lambda_Free_RPOs (AFP)
Session AFP/Lambda_Free_EPO (AFP)
Session AFP/Landau_Symbols (AFP)
Session AFP/Akra_Bazzi (AFP)
Session AFP/Catalan_Numbers (AFP)
Session AFP/Error_Function (AFP)
Session AFP/Euler_MacLaurin (AFP)
Session AFP/Stirling_Formula (AFP)
Session AFP/LightweightJava (AFP)
Session AFP/LinearQuantifierElim (AFP)
Session AFP/List-Infinite (AFP)
Session AFP/Nat-Interval-Logic (AFP)
Session AFP/AutoFocus-Stream (AFP)
Session AFP/MuchAdoAboutTwo (AFP)
Session AFP/Optics (AFP)
Session AFP/UTP-Toolkit (AFP)
Session AFP/UTP (AFP)
Session AFP/Order_Lattice_Props (AFP)
Session AFP/POPLmark-deBruijn (AFP)
Session AFP/Pairing_Heap (AFP)
Session AFP/Password_Authentication_Protocol (AFP)
Session AFP/Pell (AFP)
Session AFP/Presburger-Automata (AFP)
Session AFP/Priority_Queue_Braun (AFP)
Session AFP/Program-Conflict-Analysis (AFP)
Session AFP/Regular-Sets (AFP)
Session AFP/Abstract-Rewriting (AFP)
Session AFP/Decreasing-Diagrams (AFP)
Session AFP/First_Order_Terms (AFP)
Session AFP/Matrix (AFP)
Session AFP/Matrix_Tensor (AFP)
Session AFP/Knot_Theory (AFP)
Session AFP/Coinductive_Languages (AFP)
Session AFP/Finite_Automata_HF (AFP)
Session AFP/Functional-Automata (AFP)
Session AFP/Posix-Lexing (AFP)
Session AFP/Ribbon_Proofs (AFP)
Session AFP/SATSolverVerification (AFP)
Session AFP/Safe_OCL (AFP)
Session AFP/Selection_Heap_Sort (AFP)
Session AFP/Simplex (AFP)
Session AFP/Skew_Heap (AFP)
Session AFP/Sort_Encodings (AFP)
Session AFP/Splay_Tree (AFP)
Session AFP/Amortized_Complexity (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Root_Balanced_Tree (AFP)
Session AFP/Stable_Matching (AFP)
Session AFP/SuperCalc (AFP)
Session AFP/Tail_Recursive_Functions (AFP)
Session AFP/TortoiseHare (AFP)
Session AFP/Trie (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Twelvefold_Way (AFP)
Session AFP/Vickrey_Clarke_Groves (AFP)
Session HOL/HOL-Mirabelle
Session HOL/HOL-Mirabelle-ex
Session HOL/HOL-NanoJava
Session HOL/HOL-Prolog
Session HOL/HOL-Real_Asymp
Session HOL/HOL-Real_Asymp-Manual
Session HOL/HOL-Statespace
Session HOL/HOL-TLA
Session HOL/HOL-TLA-Buffer
Session HOL/HOL-TLA-Inc
Session HOL/HOL-TLA-Memory
Session HOL/HOL-Types_To_Sets
Session AFP/Smooth_Manifolds (AFP)
Session HOL/HOL-Word (main timing)
Session HOL/HOL-SPARK
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session HOL/HOL-SPARK-Manual
Session HOL/HOL-Word-SMT_Examples (timing)
Session AFP/Kleene_Algebra (AFP)
Session AFP/KAT_and_DRA (AFP)
Session AFP/Multirelations (AFP)
Session AFP/Quantales (AFP)
Session AFP/Transformer_Semantics (AFP)
Session AFP/Regular_Algebras (AFP)
Session AFP/Relation_Algebra (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/LEM (AFP)
Session AFP/Native_Word (AFP)
Session AFP/WebAssembly (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Collections (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Abstract_Soundness (AFP)
Session AFP/Incredible_Proof_Machine (AFP)
Session AFP/Deriving (AFP)
Session AFP/CAVA_Base (AFP)
Session AFP/CAVA_Automata (AFP)
Session AFP/DFS_Framework (AFP)
Session AFP/Gabow_SCC (AFP)
Session AFP/LTL_to_GBA (AFP)
Session AFP/Promela (AFP)
Session AFP/Containers (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Old_Datatype_Show (AFP)
Session AFP/Show (AFP)
Session AFP/JNF-AFP-Lib (AFP)
Session AFP/Real_Impl (AFP)
Session AFP/QR_Decomposition (AFP)
Session AFP/Dijkstra_Shortest_Path (AFP)
Session AFP/Koenigsberg_Friendship (AFP)
Session AFP/Transition_Systems_and_Automata (AFP)
Session AFP/Buchi_Complementation (AFP)
Session AFP/LTL_Master_Theorem (AFP)
Session AFP/Partial_Order_Reduction (AFP)
Session AFP/SM_Base (AFP)
Session AFP/SM (AFP)
Session AFP/CAVA_Setup (AFP)
Session AFP/CAVA_LTL_Modelchecker (AFP)
Session AFP/Transitive-Closure (AFP)
Session AFP/KBPs (AFP)
Session AFP/Tree-Automata (AFP)
Session AFP/SPARCv8 (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Separata (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sepref_Prereq (AFP)
Session AFP/ROBDD (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/Word_Lib (AFP)
Session AFP/Complx (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/CakeML (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Routing (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/LOFT (AFP)
Session HOL/HOLCF (main timing)
Session AFP/Circus (AFP)
Session AFP/HOL-CSP (AFP)
Session HOL/HOLCF-IMP
Session HOL/HOLCF-Library
Session HOL/HOLCF-FOCUS
Session HOL/HOLCF-ex
Session AFP/PCF (AFP)
Session AFP/HOLCF-Prelude (AFP)
Session HOL/HOLCF-Tutorial
Session HOL/IOA (timing)
Session HOL/IOA-ABP
Session HOL/IOA-NTP
Session HOL/IOA-Storage
Session HOL/IOA-ex
Session AFP/Shivers-CFA (AFP)
Session AFP/Stream-Fusion (AFP)
Session AFP/Tycon (AFP)
Session AFP/WorkerWrapper (AFP)
Session AFP/Heard_Of (AFP)
Session AFP/Consensus_Refined (AFP)
Session AFP/Hoare_Time (AFP)
Session AFP/HotelKeyCards (AFP)
Session Doc/How_to_Prove_it (no_doc)
Session AFP/Huffman (AFP)
Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
Session AFP/IMP2 (AFP)
Session Doc/Implementation (doc)
Session AFP/Impossible_Geometry (AFP)
Session AFP/Inductive_Confidentiality (AFP)
Session AFP/InfPathElimination (AFP)
Session Doc/Isar_Ref (doc)
Session Doc/JEdit (doc)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/KAD (AFP)
Session AFP/Algebraic_VCs (AFP)
Session AFP/Key_Agreement_Strong_Adversaries (AFP)
Session AFP/LambdaMu (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Lazy_Case (AFP)
Session AFP/Dict_Construction (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/List-Index (AFP)
Session AFP/Affine_Arithmetic (AFP)
Session AFP/Taylor_Models (AFP)
Session AFP/Comparison_Sort_Lower_Bound (AFP)
Session AFP/Formula_Derivatives (AFP)
Session AFP/Formula_Derivatives-Examples (AFP)
Session AFP/Higher_Order_Terms (AFP)
Session AFP/Jinja (AFP)
Session AFP/HRB-Slicing (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/Slicing (AFP)
Session AFP/Formal_SSA (AFP)
Session AFP/Minimal_SSA (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/LTL_to_DRA (AFP)
Session AFP/List_Update (AFP)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/Differential_Dynamic_Logic (AFP)
Session AFP/HOL-ODE-Numerics (AFP)
Session AFP/HOL-ODE-ARCH-COMP (AFP)
Session AFP/HOL-ODE-Examples (AFP large)
Session AFP/Lorenz_Approximation (AFP)
Session AFP/Lorenz_C0 (AFP large)
Session AFP/Lorenz_C1 (AFP large)
Session AFP/Quick_Sort_Cost (AFP)
Session AFP/Random_BSTs (AFP)
Session AFP/Randomised_BSTs (AFP)
Session AFP/Treaps (AFP)
Session AFP/Randomised_Social_Choice (AFP)
Session AFP/Fishburn_Impossibility (AFP)
Session AFP/SDS_Impossibility (AFP)
Session AFP/Refine_Imperative_HOL (AFP)
Session AFP/Floyd_Warshall (AFP)
Session AFP/Sepref_Basic (AFP)
Session AFP/Sepref_IICF (AFP)
Session AFP/Flow_Networks (AFP)
Session AFP/EdmondsKarp_Maxflow (AFP)
Session AFP/MFMC_Countable (AFP)
Session AFP/Prpu_Maxflow (AFP)
Session AFP/Knuth_Morris_Pratt (AFP)
Session AFP/VerifyThis2018 (AFP)
Session AFP/List_Interleaving (AFP)
Session AFP/List_Inversions (AFP)
Session AFP/LocalLexing (AFP)
Session Doc/Locales (doc)
Session AFP/Lowe_Ontological_Argument (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session Doc/Main (doc)
Session AFP/Marriage (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Matroids (AFP)
Session AFP/Kruskal (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Median_Of_Medians_Selection (AFP)
Session AFP/KD_Tree (AFP)
Session AFP/Menger (AFP)
Session AFP/MiniML (AFP)
Session AFP/Modular_Assembly_Kit_Security (AFP)
Session AFP/Monad_Memo_DP (AFP)
Session AFP/Hidden_Markov_Models (AFP)
Session AFP/Optimal_BST (AFP)
Session AFP/MonoBoolTranAlgebra (AFP)
Session AFP/Name_Carrying_Type_Inference (AFP)
Session AFP/Network_Security_Policy_Verification (AFP)
Session AFP/No_FTL_observers (AFP)
Session AFP/Nominal2 (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Surprise_Paradox (AFP)
Session AFP/LambdaAuth (AFP)
Session AFP/Launchbury (AFP)
Session AFP/Call_Arity (AFP)
Session AFP/Modal_Logics_for_NTS (AFP)
Session AFP/Rewriting_Z (AFP)
Session AFP/Noninterference_CSP (AFP)
Session AFP/Noninterference_Ipurge_Unwinding (AFP)
Session AFP/Noninterference_Generic_Unwinding (AFP)
Session AFP/Noninterference_Inductive_Unwinding (AFP)
Session AFP/Noninterference_Sequential_Composition (AFP)
Session AFP/Noninterference_Concurrent_Composition (AFP)
Session AFP/NormByEval (AFP)
Session AFP/OpSets (AFP)
Session AFP/Open_Induction (AFP)
Session AFP/Well_Quasi_Orders (AFP)
Session AFP/Decreasing-Diagrams-II (AFP)
Session AFP/Myhill-Nerode (AFP)
Session AFP/Polynomials (AFP)
Session AFP/Symmetric_Polynomials (AFP)
Session AFP/Pi_Transcendental (AFP)
Session AFP/Ordinal (AFP)
Session AFP/Nested_Multisets_Ordinals (AFP)
Session AFP/Lambda_Free_KBOs (AFP)
Session AFP/Ordered_Resolution_Prover (AFP)
Session AFP/PLM (AFP)
Session AFP/PSemigroupsConvolution (AFP)
Session AFP/Paraconsistency (AFP)
Session AFP/Parity_Game (AFP)
Session AFP/Partial_Function_MR (AFP)
Session AFP/Certification_Monads (AFP)
Session AFP/XML (AFP)
Session AFP/Polynomial_Factorization (AFP)
Session AFP/Dirichlet_Series (AFP)
Session AFP/Zeta_Function (AFP)
Session AFP/Dirichlet_L (AFP)
Session AFP/Prime_Number_Theorem (AFP)
Session AFP/Prime_Distribution_Elementary (AFP)
Session AFP/Transcendence_Series_Hancl_Rucki (AFP)
Session AFP/Functional_Ordered_Resolution_Prover (AFP)
Session AFP/Jordan_Normal_Form (AFP)
Session AFP/Deep_Learning (AFP)
Session AFP/Farkas (AFP)
Session AFP/Groebner_Bases (AFP)
Session AFP/Signature_Groebner (AFP)
Session AFP/QHLProver (AFP)
Session AFP/Linear_Recurrences (AFP)
Session AFP/Perron_Frobenius (AFP)
Session AFP/Stochastic_Matrices (AFP)
Session AFP/Subresultants (AFP)
Session AFP/Pre_BZ (AFP)
Session AFP/Berlekamp_Zassenhaus (AFP)
Session AFP/Algebraic_Numbers (AFP)
Session AFP/LLL_Basis_Reduction (AFP)
Session AFP/LLL_Factorization (AFP)
Session AFP/Linear_Recurrences_Solver (AFP)
Session AFP/Probabilistic_While (AFP)
Session AFP/Pop_Refinement (AFP)
Session AFP/Possibilistic_Noninterference (AFP)
Session Doc/Prog_Prove (doc)
Session AFP/Projective_Geometry (AFP)
Session AFP/Proof_Strategy_Language (AFP)
Session AFP/PropResPI (AFP)
Session AFP/Propositional_Proof_Systems (AFP)
Session AFP/PseudoHoops (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Recursion-Theory-I (AFP)
Session AFP/Minsky_Machines (AFP)
Session AFP/RefinementReactive (AFP)
Session AFP/Resolution_FOL (AFP)
Session AFP/Robbins-Conjecture (AFP)
Session AFP/Roy_Floyd_Warshall (AFP)
Session AFP/SIFPL (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Simpl (AFP)
Session AFP/BDD (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Statecharts (AFP)
Session AFP/Stone_Algebras (AFP)
Session AFP/Stone_Relation_Algebras (AFP)
Session AFP/Stone_Kleene_Relation_Algebras (AFP)
Session AFP/Aggregation_Algebras (AFP)
Session AFP/Store_Buffer_Reduction (AFP)
Session AFP/Strong_Security (AFP)
Session Doc/Sugar (doc)
Session AFP/TLA (AFP)
Session AFP/Timed_Automata (AFP)
Session AFP/Probabilistic_Timed_Automata (AFP)
Session AFP/Transitive-Closure-II (AFP)
Session AFP/Tree_Decomposition (AFP)
Session Doc/Tutorial (doc)
Session Doc/Typeclass_Hierarchy (doc)
Session AFP/Types_Tableaus_and_Goedels_God (AFP)
Session AFP/UPF (AFP)
Session AFP/UPF_Firewall (AFP)
Session AFP/Universal_Turing_Machine (AFP)
Session AFP/Verified-Prover (AFP)
Session AFP/VolpanoSmith (AFP)
Session AFP/WHATandWHERE_Security (AFP)
Session AFP/Weight_Balanced_Trees (AFP)
Session HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-Lambda (timing)
Session AFP/Applicative_Lifting (AFP)
Session AFP/CryptHOL (AFP)
Session AFP/Constructive_Cryptography (AFP)
Session AFP/Game_Based_Crypto (AFP)
Session AFP/Multi_Party_Computation (AFP)
Session AFP/Free-Groups (AFP)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Stern_Brocot (AFP)
Session HOL/HOL-Proofs-ex
Session Tools/Haskell
Session Doc/Intro (doc)
Session LCF/LCF
Session Doc/Logics (doc)
Session Doc/Nitpick (doc)
Session Tools/SML
Session Sequents/Sequents
Session Doc/Sledgehammer (doc)
Session Tools/Spec_Check
Session AFP/Regex_Equivalence (AFP)
Session Doc/System (doc)
Session ZF/ZF (main timing)
Session Doc/Logics_ZF (doc)
Session ZF/ZF-AC
Session ZF/ZF-Coind
Session ZF/ZF-Constructible
Session ZF/ZF-IMP
Session ZF/ZF-Induct
Session ZF/ZF-UNITY (timing)
Session ZF/ZF-Resid
Session ZF/ZF-ex
Building HOL ...
Building HOL-Proofs ...
HOL: theory HOL.Code_Generator
HOL-Proofs: theory HOL.Code_Generator
HOL: theory HOL.HOL
HOL-Proofs: theory HOL.HOL
HOL: theory HOL.Argo
HOL: theory HOL.Ctr_Sugar
HOL: theory HOL.Orderings
HOL-Proofs: theory HOL.Argo
HOL-Proofs: theory HOL.Ctr_Sugar
HOL-Proofs: theory HOL.Orderings
HOL: theory HOL.Groups
HOL: theory HOL.SAT
HOL-Proofs: theory HOL.SAT
HOL-Proofs: theory HOL.Groups
HOL: theory HOL.Lattices
HOL-Proofs: theory HOL.Lattices
HOL: theory HOL.Set
HOL: theory HOL.Fun
HOL: theory HOL.Typedef
HOL: theory HOL.Complete_Lattices
HOL: theory HOL.Rings
HOL-Proofs: theory HOL.Set
HOL: theory HOL.Inductive
HOL: theory HOL.Product_Type
HOL: theory HOL.Sum_Type
HOL-Proofs: theory HOL.Fun
HOL-Proofs: theory HOL.Typedef
HOL: theory HOL.Complete_Partial_Order
HOL-Proofs: theory HOL.Complete_Lattices
HOL-Proofs: theory HOL.Rings
HOL: theory HOL.Nat
HOL-Proofs: theory HOL.Inductive
HOL: theory HOL.Fields
HOL: theory HOL.Meson
HOL: theory HOL.ATP
HOL-Proofs: theory HOL.Product_Type
HOL-Proofs: theory HOL.Sum_Type
HOL: theory HOL.Metis
HOL-Proofs: theory HOL.Complete_Partial_Order
HOL: theory HOL.Finite_Set
HOL: theory HOL.Relation
HOL: theory HOL.Transitive_Closure
HOL: theory HOL.Wellfounded
HOL: theory HOL.Fun_Def_Base
HOL: theory HOL.Hilbert_Choice
HOL-Proofs: theory HOL.Nat
HOL: theory HOL.Wfrec
HOL: theory HOL.Order_Relation
HOL: theory HOL.BNF_Wellorder_Relation
HOL: theory HOL.BNF_Wellorder_Embedding
HOL: theory HOL.Zorn
HOL: theory HOL.BNF_Wellorder_Constructions
HOL: theory HOL.BNF_Cardinal_Order_Relation
HOL: theory HOL.BNF_Cardinal_Arithmetic
HOL: theory HOL.BNF_Def
HOL-Proofs: theory HOL.Fields
HOL-Proofs: theory HOL.Meson
HOL-Proofs: theory HOL.ATP
HOL: theory HOL.BNF_Composition
HOL: theory HOL.Basic_BNFs
HOL: theory HOL.BNF_Fixpoint_Base
HOL-Proofs: theory HOL.Metis
HOL: theory HOL.BNF_Least_Fixpoint
HOL-Proofs: theory HOL.Finite_Set
HOL: theory HOL.Basic_BNF_LFPs
HOL: theory HOL.Transfer
HOL: theory HOL.Num
HOL: theory HOL.Power
HOL: theory HOL.Groups_Big
HOL: theory HOL.Equiv_Relations
HOL: theory HOL.Lifting
HOL-Proofs: theory HOL.Relation
HOL: theory HOL.Lifting_Set
HOL: theory HOL.Option
HOL: theory HOL.Quotient
HOL: theory HOL.Extraction
HOL: theory HOL.Lattices_Big
HOL: theory HOL.Partial_Function
HOL-Proofs: theory HOL.Transitive_Closure
HOL: theory HOL.Fun_Def
HOL: theory HOL.Int
HOL-Proofs: theory HOL.Wellfounded
HOL: theory HOL.Euclidean_Division
HOL-Proofs: theory HOL.Fun_Def_Base
HOL-Proofs: theory HOL.Hilbert_Choice
HOL-Proofs: theory HOL.Wfrec
HOL-Proofs: theory HOL.Order_Relation
HOL-Proofs: theory HOL.BNF_Wellorder_Relation
HOL-Proofs: theory HOL.BNF_Wellorder_Embedding
HOL-Proofs: theory HOL.Zorn
HOL: theory HOL.Parity
HOL-Proofs: theory HOL.BNF_Wellorder_Constructions
HOL: theory HOL.Divides
HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation
HOL: theory HOL.Code_Numeral
HOL: theory HOL.Numeral_Simprocs
HOL: theory HOL.SMT
HOL: theory HOL.Set_Interval
HOL: theory HOL.Semiring_Normalization
HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic
HOL: theory HOL.Groebner_Basis
HOL-Proofs: theory HOL.BNF_Def
HOL: theory HOL.Conditionally_Complete_Lattices
HOL: theory HOL.Filter
HOL: theory HOL.Presburger
HOL-Proofs: theory HOL.BNF_Composition
HOL-Proofs: theory HOL.Basic_BNFs
HOL: theory HOL.Sledgehammer
HOL-Proofs: theory HOL.BNF_Fixpoint_Base
HOL: theory HOL.List
HOL-Proofs: theory HOL.BNF_Least_Fixpoint
HOL-Proofs: theory HOL.Basic_BNF_LFPs
HOL-Proofs: theory HOL.Transfer
HOL: theory HOL.Groups_List
HOL: theory HOL.Map
HOL-Proofs: theory HOL.Num
HOL: theory HOL.Factorial
HOL: theory HOL.GCD
HOL: theory HOL.Enum
HOL: theory HOL.Binomial
HOL: theory HOL.Random
HOL-Proofs: theory HOL.Power
HOL: theory HOL.String
HOL: theory HOL.BNF_Greatest_Fixpoint
HOL: theory HOL.Predicate
HOL: theory HOL.Typerep
HOL: theory HOL.Lazy_Sequence
HOL: theory HOL.Limited_Sequence
HOL-Proofs: theory HOL.Groups_Big
HOL: theory HOL.Code_Evaluation
HOL: theory HOL.Quickcheck_Random
HOL: theory HOL.Quickcheck_Exhaustive
HOL: theory HOL.Quickcheck_Narrowing
HOL: theory HOL.Random_Pred
HOL: theory HOL.Random_Sequence
HOL: theory HOL.Record
HOL: theory HOL.Predicate_Compile
HOL-Proofs: theory HOL.Equiv_Relations
HOL: theory HOL.Nitpick
HOL-Proofs: theory HOL.Lifting
HOL-Proofs: theory HOL.Lifting_Set
HOL-Proofs: theory HOL.Option
HOL-Proofs: theory HOL.Quotient
HOL-Proofs: theory HOL.Extraction
HOL-Proofs: theory HOL.Lattices_Big
HOL-Proofs: theory HOL.Partial_Function
HOL: theory HOL.Nunchaku
HOL: theory Main
HOL-Proofs: theory HOL.Fun_Def
HOL: theory HOL.Archimedean_Field
HOL: theory HOL.Hull
HOL: theory HOL.Topological_Spaces
HOL: theory HOL.Modules
HOL: theory HOL.Vector_Spaces
HOL-Proofs: theory HOL.Int
HOL: theory HOL.Rat
HOL-Proofs: theory HOL.Euclidean_Division
HOL: theory HOL.Real
HOL: theory HOL.Real_Vector_Spaces
HOL-Proofs: theory HOL.Parity
HOL: theory HOL.Inequalities
HOL: theory HOL.Limits
HOL-Proofs: theory HOL.Divides
HOL: theory HOL.Deriv
HOL: theory HOL.Series
HOL-Proofs: theory HOL.Code_Numeral
HOL-Proofs: theory HOL.Numeral_Simprocs
HOL-Proofs: theory HOL.SMT
HOL-Proofs: theory HOL.Set_Interval
HOL: theory HOL.NthRoot
HOL: theory HOL.Transcendental
HOL: theory HOL.Complex
HOL: theory HOL.MacLaurin
HOL: theory Complex_Main
HOL-Proofs: theory HOL.Semiring_Normalization
HOL-Proofs: theory HOL.Conditionally_Complete_Lattices
HOL-Proofs: theory HOL.Filter
HOL-Proofs: theory HOL.Groebner_Basis
HOL-Proofs: theory HOL.Presburger
HOL-Proofs: theory HOL.Sledgehammer
Timing HOL (4 threads, 192.863s elapsed time, 589.516s cpu time, 38.540s GC time, factor 3.06)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL
HOL FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64_32-linux/log/HOL)
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL/outline -o pdf -n outline -t /proof,/ML
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL/document -o pdf -n document
*** Latex error (line 86 of "~~/src/HOL/Fields.thy"):
***   Missing $ inserted.
***   <inserted text> 
***                   $
***   }
*** Latex error (line 86 of "~~/src/HOL/Fields.thy"):
***   Extra }, or forgotten $.
***   \isamarkupcmt #1->{\isastylecmt --- #1}
***                                          
***   }
*** Latex error (line 86 of "~~/src/HOL/Fields.thy"):
***   Missing $ inserted.
***   <inserted text> 
***                   $
***   \isanewline
*** Latex error (line 1333 of "~~/src/HOL/Fields.thy"):
***   Missing } inserted.
***   <inserted text> 
***                   }
***   \end{isabellebody}
*** Failed to build document in "/media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL/document"
HOL-Analysis CANCELLED
Ordinary_Differential_Equations CANCELLED
HOL-ODE-Numerics CANCELLED
Lorenz_Approximation CANCELLED
Lorenz_C0 CANCELLED
Automatic_Refinement CANCELLED
HOL-Library CANCELLED
Refine_Monadic CANCELLED
Collections CANCELLED
HOL-Computational_Algebra CANCELLED
HOL-Algebra CANCELLED
CAVA_Base CANCELLED
CAVA_Automata CANCELLED
CAVA_Setup CANCELLED
JNF-AFP-Lib CANCELLED
HOL-Word CANCELLED
Word_Lib CANCELLED
Jordan_Normal_Form CANCELLED
IP_Addresses CANCELLED
Simple_Firewall CANCELLED
Routing CANCELLED
Category3 CANCELLED
Iptables_Semantics CANCELLED
Subresultants CANCELLED
HOL-ODE-ARCH-COMP CANCELLED
Pre_BZ CANCELLED
HOL-ODE-Examples CANCELLED
HereditarilyFinite CANCELLED
Incompleteness CANCELLED
Native_Word CANCELLED
Jinja CANCELLED
HOL-Number_Theory CANCELLED
MSO_Regex_Equivalence CANCELLED
Iptables_Semantics_Examples CANCELLED
Berlekamp_Zassenhaus CANCELLED
HOL-Probability CANCELLED
CAVA_LTL_Modelchecker CANCELLED
HOL-Codegenerator_Test CANCELLED
HOL-Nominal CANCELLED
Groebner_Bases CANCELLED
HOL-Nominal-Examples CANCELLED
HOL-ex CANCELLED
HOL-Decision_Procs CANCELLED
Echelon_Form CANCELLED
LEM CANCELLED
Sepref_Prereq CANCELLED
Affine_Arithmetic CANCELLED
Algebraic_Numbers CANCELLED
CakeML CANCELLED
Formal_SSA CANCELLED
Sepref_Basic CANCELLED
HRB-Slicing CANCELLED
Markov_Models CANCELLED
HOL-Data_Structures CANCELLED
Sepref_IICF CANCELLED
Auto2_HOL CANCELLED
Psi_Calculi CANCELLED
Slicing CANCELLED
MonoidalCategory CANCELLED
Dirichlet_Series CANCELLED
Security_Protocol_Refinement CANCELLED
SM_Base CANCELLED
Deriving CANCELLED
Auto2_Imperative_HOL CANCELLED
Kleene_Algebra CANCELLED
Transition_Systems_and_Automata CANCELLED
Stone_Algebras CANCELLED
Formula_Derivatives CANCELLED
Probabilistic_While CANCELLED
Network_Security_Policy_Verification CANCELLED
Flow_Networks CANCELLED
KAT_and_DRA CANCELLED
Containers CANCELLED
HOLCF CANCELLED
Stochastic_Matrices CANCELLED
CryptHOL CANCELLED
HOL-CSP CANCELLED
Refine_Imperative_HOL CANCELLED
Proof_Strategy_Language CANCELLED
Stone_Relation_Algebras CANCELLED
Core_DOM CANCELLED
Algebraic_VCs CANCELLED
Linear_Recurrences_Solver CANCELLED
Complx CANCELLED
LLL_Basis_Reduction CANCELLED
Key_Agreement_Strong_Adversaries CANCELLED
Probabilistic_Prime_Tests CANCELLED
Differential_Dynamic_Logic CANCELLED
Dependent_SIFUM_Type_Systems CANCELLED
HOL-Corec_Examples CANCELLED
SPARCv8 CANCELLED
Perron_Frobenius CANCELLED
Transcendence_Series_Hancl_Rucki CANCELLED
Universal_Turing_Machine CANCELLED
No_FTL_observers CANCELLED
Group-Ring-Module CANCELLED
Count_Complex_Roots CANCELLED
Simpl CANCELLED
Promela CANCELLED
Probabilistic_Timed_Automata CANCELLED
Datatype_Order_Generator CANCELLED
Isabelle_Meta_Model CANCELLED
Stone_Kleene_Relation_Algebras CANCELLED
SM CANCELLED
QR_Decomposition CANCELLED
CoreC++ CANCELLED
HOL-Nitpick_Examples CANCELLED
Game_Based_Crypto CANCELLED
Simplex CANCELLED
KAD CANCELLED
Deep_Learning CANCELLED
LTL_to_GBA CANCELLED
Nominal2 CANCELLED
E_Transcendental CANCELLED
Abstract-Rewriting CANCELLED
Prpu_Maxflow CANCELLED
HOL-Auth CANCELLED
DFS_Framework CANCELLED
Timed_Automata CANCELLED
LOFT CANCELLED
Containers-Benchmarks CANCELLED
Safe_OCL CANCELLED
Collections_Examples CANCELLED
Featherweight_OCL CANCELLED
Modal_Logics_for_NTS CANCELLED
Multi_Party_Computation CANCELLED
Monad_Memo_DP CANCELLED
Order_Lattice_Props CANCELLED
LTL CANCELLED
Allen_Calculus CANCELLED
Datatypes CANCELLED
Polynomials CANCELLED
Zeta_Function CANCELLED
Store_Buffer_Reduction CANCELLED
KBPs CANCELLED
Coinductive CANCELLED
Gabow_SCC CANCELLED
Constructive_Cryptography CANCELLED
Dependent_SIFUM_Refinement CANCELLED
HOL-Quickcheck_Examples CANCELLED
HOL-Homology CANCELLED
Density_Compiler CANCELLED
Ordinal CANCELLED
Gromov_Hyperbolicity CANCELLED
InfPathElimination CANCELLED
Functional_Ordered_Resolution_Prover CANCELLED
Planarity_Certificates CANCELLED
Stable_Matching CANCELLED
Taylor_Models CANCELLED
Nested_Multisets_Ordinals CANCELLED
Flyspeck-Tame CANCELLED
HOL-Datatype_Examples CANCELLED
HOL-Cardinals CANCELLED
PseudoHoops CANCELLED
HOL-Hoare_Parallel CANCELLED
UPF CANCELLED
Hermite CANCELLED
Rep_Fin_Groups CANCELLED
Matrix CANCELLED
Launchbury CANCELLED
IMP2 CANCELLED
Paraconsistency CANCELLED
Resolution_FOL CANCELLED
WebAssembly CANCELLED
Binding_Syntax_Theory CANCELLED
Hoare_Time CANCELLED
Quantales CANCELLED
Vickrey_Clarke_Groves CANCELLED
HOL-IMP CANCELLED
HOL-MicroJava CANCELLED
EdmondsKarp_Maxflow CANCELLED
Aggregation_Algebras CANCELLED
HOL-Bali CANCELLED
Regular_Algebras CANCELLED
Winding_Number_Eval CANCELLED
Separation_Logic_Imperative_HOL CANCELLED
LTL_to_DRA CANCELLED
Abortable_Linearizable_Modules CANCELLED
Multirelations CANCELLED
List_Update CANCELLED
Buildings CANCELLED
UPF_Firewall CANCELLED
Prime_Harmonic_Series CANCELLED
List-Infinite CANCELLED
Signature_Groebner CANCELLED
Factored_Transition_System_Bounding CANCELLED
HOL-Word-SMT_Examples CANCELLED
Linear_Recurrences CANCELLED
Propositional_Proof_Systems CANCELLED
Matrix_Tensor CANCELLED
Password_Authentication_Protocol CANCELLED
Ergodic_Theory CANCELLED
Gauss_Jordan CANCELLED
Dijkstra_Shortest_Path CANCELLED
Green CANCELLED
BytecodeLogicJmlTypes CANCELLED
Dirichlet_L CANCELLED
HOL-Real_Asymp CANCELLED
Akra_Bazzi CANCELLED
Girth_Chromatic CANCELLED
Farkas CANCELLED
Sturm_Sequences CANCELLED
Hidden_Markov_Models CANCELLED
MFMC_Countable CANCELLED
Corec CANCELLED
Applicative_Lifting CANCELLED
Probabilistic_Noninterference CANCELLED
Abs_Int_ITP2012 CANCELLED
DiscretePricing CANCELLED
Pi_Transcendental CANCELLED
Cauchy CANCELLED
Free-Groups CANCELLED
Root_Balanced_Tree CANCELLED
Nat-Interval-Logic CANCELLED
Splay_Tree CANCELLED
Lambda_Free_KBOs CANCELLED
Sqrt_Babylonian CANCELLED
AWN CANCELLED
Parity_Game CANCELLED
LambdaAuth CANCELLED
HOL-Predicate_Compile_Examples CANCELLED
ComponentDependencies CANCELLED
Irrationality_J_Hancl CANCELLED
Regular-Sets CANCELLED
Symmetric_Polynomials CANCELLED
HOL-Imperative_HOL CANCELLED
LTL_Master_Theorem CANCELLED
Codegen CANCELLED
QHLProver CANCELLED
Sort_Encodings CANCELLED
Amortized_Complexity CANCELLED
LocalLexing CANCELLED
Real_Impl CANCELLED
Twelvefold_Way CANCELLED
UTP-Toolkit CANCELLED
LLL_Factorization CANCELLED
Polynomial_Factorization CANCELLED
Regex_Equivalence CANCELLED
Elliptic_Curves_Group_Law CANCELLED
Tree-Automata CANCELLED
Encodability_Process_Calculi CANCELLED
SATSolverVerification CANCELLED
Relation_Algebra CANCELLED
SIFUM_Type_Systems CANCELLED
Randomised_Social_Choice CANCELLED
Pi_Calculus CANCELLED
Generic_Deriving CANCELLED
HOLCF-Library CANCELLED
Higher_Order_Terms CANCELLED
LightweightJava CANCELLED
Stern_Brocot CANCELLED
BDD CANCELLED
Call_Arity CANCELLED
VerifyThis2018 CANCELLED
AutoFocus-Stream CANCELLED
HOL-SET_Protocol CANCELLED
Knot_Theory CANCELLED
Partial_Order_Reduction CANCELLED
Statecharts CANCELLED
Smooth_Manifolds CANCELLED
Dict_Construction CANCELLED
Bertrands_Postulate CANCELLED
Buchi_Complementation CANCELLED
Probabilistic_System_Zoo CANCELLED
Treaps CANCELLED
Ordered_Resolution_Prover CANCELLED
Hybrid_Multi_Lane_Spatial_Logic CANCELLED
HOL-Quotient_Examples CANCELLED
LinearQuantifierElim CANCELLED
PCF CANCELLED
Koenigsberg_Friendship CANCELLED
Prime_Distribution_Elementary CANCELLED
HOLCF-Prelude CANCELLED
SDS_Impossibility CANCELLED
SequentInvertibility CANCELLED
Probabilistic_System_Zoo-Non_BNFs CANCELLED
Concurrent_Revisions CANCELLED
DynamicArchitectures CANCELLED
HOL-UNITY CANCELLED
Circus CANCELLED
Monomorphic_Monad CANCELLED
Graph_Theory CANCELLED
UTP CANCELLED
Valuation CANCELLED
SIFPL CANCELLED
Possibilistic_Noninterference CANCELLED
CRDT CANCELLED
Special_Function_Bounds CANCELLED
Residuated_Lattices CANCELLED
Noninterference_CSP CANCELLED
VectorSpace CANCELLED
Quick_Sort_Cost CANCELLED
Tarskis_Geometry CANCELLED
SuperCalc CANCELLED
GewirthPGCProof CANCELLED
Incredible_Proof_Machine CANCELLED
UpDown_Scheme CANCELLED
Kruskal CANCELLED
Prime_Number_Theorem CANCELLED
Stirling_Formula CANCELLED
Formula_Derivatives-Examples CANCELLED
Localization_Ring CANCELLED
Decl_Sem_Fun_PL CANCELLED
DiskPaxos CANCELLED
Graph_Saturation CANCELLED
Noninterference_Ipurge_Unwinding CANCELLED
Locally-Nameless-Sigma CANCELLED
Rewriting_Z CANCELLED
Architectural_Design_Patterns CANCELLED
Consensus_Refined CANCELLED
Heard_Of CANCELLED
Myhill-Nerode CANCELLED
Median_Of_Medians_Selection CANCELLED
ROBDD CANCELLED
PLM CANCELLED
Lp CANCELLED
HOL-Hoare CANCELLED
IEEE_Floating_Point CANCELLED
WHATandWHERE_Security CANCELLED
HOL-Metis_Examples CANCELLED
HOL-Analysis-ex CANCELLED
Quaternions CANCELLED
Presburger-Automata CANCELLED
Trie CANCELLED
Projective_Geometry CANCELLED
Well_Quasi_Orders CANCELLED
Shivers-CFA CANCELLED
Modular_Assembly_Kit_Security CANCELLED
pGCL CANCELLED
Noninterference_Sequential_Composition CANCELLED
Abstract_Completeness CANCELLED
ConcurrentIMP CANCELLED
Lambda_Free_EPO CANCELLED
NormByEval CANCELLED
Noninterference_Generic_Unwinding CANCELLED
Fishburn_Impossibility CANCELLED
Priority_Queue_Braun CANCELLED
Show CANCELLED
Tutorial CANCELLED
HOL-Statespace CANCELLED
Budan_Fourier CANCELLED
XML CANCELLED
AxiomaticCategoryTheory CANCELLED
HOL-SPARK CANCELLED
Diophantine_Eqns_Lin_Hom CANCELLED
PSemigroupsConvolution CANCELLED
HOL-Eisbach CANCELLED
FocusStreamsCaseStudies CANCELLED
Kuratowski_Closure_Complement CANCELLED
Octonions CANCELLED
FOL_Harrison CANCELLED
IOA CANCELLED
Program-Conflict-Analysis CANCELLED
InformationFlowSlicing_Inter CANCELLED
IMAP-CRDT CANCELLED
Knuth_Morris_Pratt CANCELLED
FOL-Fitting CANCELLED
PropResPI CANCELLED
Isar_Ref CANCELLED
GraphMarkingIBP CANCELLED
Boolean_Expression_Checkers CANCELLED
Finger-Trees CANCELLED
Euler_MacLaurin CANCELLED
Pell CANCELLED
HOL-SPARK-Examples CANCELLED
SenSocialChoice CANCELLED
OpSets CANCELLED
Types_Tableaus_and_Goedels_God CANCELLED
Probabilistic_System_Zoo-BNFs CANCELLED
Finite_Automata_HF CANCELLED
Binomial-Heaps CANCELLED
Random_BSTs CANCELLED
FLP CANCELLED
CCS CANCELLED
Posix-Lexing CANCELLED
HOL-Proofs: theory HOL.List
Ribbon_Proofs CANCELLED
RSAPSS CANCELLED
Decreasing-Diagrams-II CANCELLED
Optics CANCELLED
POPLmark-deBruijn CANCELLED
Polynomial_Interpolation CANCELLED
Sturm_Tarski CANCELLED
Functional-Automata CANCELLED
BNF_CC CANCELLED
Coinductive_Languages CANCELLED
HOL-Types_To_Sets CANCELLED
Weight_Balanced_Trees CANCELLED
Floyd_Warshall CANCELLED
HOLCF-Tutorial CANCELLED
FunWithTilings CANCELLED
Transitive-Closure-II CANCELLED
Separation_Algebra CANCELLED
Minsky_Machines CANCELLED
Name_Carrying_Type_Inference CANCELLED
Decreasing-Diagrams CANCELLED
CISC-Kernel CANCELLED
KD_Tree CANCELLED
Inductive_Confidentiality CANCELLED
Abstract_Soundness CANCELLED
Stream_Fusion_Code CANCELLED
List_Inversions CANCELLED
HOL-Nonstandard_Analysis CANCELLED
Cayley_Hamilton CANCELLED
Completeness CANCELLED
Derangements CANCELLED
Old_Datatype_Show CANCELLED
Lowe_Ontological_Argument CANCELLED
HOL-Mirabelle CANCELLED
Neumann_Morgenstern_Utility CANCELLED
Optimal_BST CANCELLED
Constructor_Funs CANCELLED
Catalan_Numbers CANCELLED
Pratt_Certificate CANCELLED
HOL-Mirabelle-ex CANCELLED
HOL-TLA CANCELLED
Category2 CANCELLED
AVL-Trees CANCELLED
Error_Function CANCELLED
HOL-Induct CANCELLED
Bell_Numbers_Spivey CANCELLED
TLA CANCELLED
Jordan_Hoelder CANCELLED
Lambda_Free_RPOs CANCELLED
JiveDataStoreModel CANCELLED
Euler_Partition CANCELLED
CryptoBasedCompositionalProperties CANCELLED
BNF_Operations CANCELLED
HOL-TLA-Memory CANCELLED
Fermat3_4 CANCELLED
Recursion-Theory-I CANCELLED
Strong_Security CANCELLED
MiniML CANCELLED
Orbit_Stabiliser CANCELLED
HyperCTL CANCELLED
HOL-Probability-ex CANCELLED
Stream-Fusion CANCELLED
Randomised_BSTs CANCELLED
Lam-ml-Normalization CANCELLED
FeatherweightJava CANCELLED
Robbins-Conjecture CANCELLED
Efficient-Mergesort CANCELLED
Transformer_Semantics CANCELLED
Separata CANCELLED
RefinementReactive CANCELLED
Landau_Symbols CANCELLED
Huffman CANCELLED
MonoBoolTranAlgebra CANCELLED
Card_Multisets CANCELLED
HOL-Matrix_LP CANCELLED
GoedelGod CANCELLED
WorkerWrapper CANCELLED
Impossible_Geometry CANCELLED
VolpanoSmith CANCELLED
Noninterference_Concurrent_Composition CANCELLED
Bernoulli CANCELLED
Typeclass_Hierarchy CANCELLED
GPU_Kernel_PL CANCELLED
Random_Graph_Subgraph_Threshold CANCELLED
Integration CANCELLED
Abstract-Hoare-Logics CANCELLED
LambdaMu CANCELLED
Rank_Nullity_Theorem CANCELLED
First_Order_Terms CANCELLED
First_Welfare_Theorem CANCELLED
Selection_Heap_Sort CANCELLED
FileRefinement CANCELLED
Verified-Prover CANCELLED
Minimal_SSA CANCELLED
Tycon CANCELLED
FinFun CANCELLED
Pop_Refinement CANCELLED
Comparison_Sort_Lower_Bound CANCELLED
Noninterference_Inductive_Unwinding CANCELLED
InformationFlowSlicing CANCELLED
Menger CANCELLED
IOA-NTP CANCELLED
Concurrent_Ref_Alg CANCELLED
Card_Partitions CANCELLED
Partial_Function_MR CANCELLED
HOL-TPTP CANCELLED
Epistemic_Logic CANCELLED
HOLCF-IMP CANCELLED
HOL-Unix CANCELLED
Binomial-Queues CANCELLED
HOL-NanoJava CANCELLED
SumSquares CANCELLED
Latin_Square CANCELLED
Tree_Decomposition CANCELLED
ShortestPath CANCELLED
Ramsey-Infinite CANCELLED
IOA-ABP CANCELLED
Bounded_Deducibility_Security CANCELLED
Dynamic_Tables CANCELLED
Topology CANCELLED
Matroids CANCELLED
HotelKeyCards CANCELLED
Tail_Recursive_Functions CANCELLED
MuchAdoAboutTwo CANCELLED
Prog_Prove CANCELLED
Chord_Segments CANCELLED
Lower_Semicontinuous CANCELLED
HOL-IMPP CANCELLED
Stewart_Apollonius CANCELLED
Triangle CANCELLED
ArrowImpossibilityGS CANCELLED
Imperative_Insertion_Sort CANCELLED
Compiling-Exceptions-Correctly CANCELLED
Category CANCELLED
Certification_Monads CANCELLED
Buffons_Needle CANCELLED
Source_Coding_Theorem CANCELLED
Falling_Factorial_Sum CANCELLED
TortoiseHare CANCELLED
HOL-Hahn_Banach CANCELLED
Lazy_Case CANCELLED
DPT-SAT-Solver CANCELLED
HOL-Isar_Examples CANCELLED
Case_Labeling CANCELLED
Secondary_Sylow CANCELLED
CYK CANCELLED
HOL-SPARK-Manual CANCELLED
Pairing_Heap CANCELLED
HOLCF-FOCUS CANCELLED
LatticeProperties CANCELLED
Functions CANCELLED
HOLCF-ex CANCELLED
Transitive-Closure CANCELLED
DataRefinementIBP CANCELLED
Lifting_Definition_Option CANCELLED
Stuttering_Equivalence CANCELLED
Implementation CANCELLED
Fisher_Yates CANCELLED
HOL-ZF CANCELLED
Card_Number_Partitions CANCELLED
List_Interleaving CANCELLED
Mason_Stothers CANCELLED
Eisbach CANCELLED
HOL-IOA CANCELLED
Gauss-Jordan-Elim-Fun CANCELLED
BinarySearchTree CANCELLED
Surprise_Paradox CANCELLED
ClockSynchInst CANCELLED
GenClock CANCELLED
Discrete_Summation CANCELLED
HOL-Nonstandard_Analysis-Examples CANCELLED
Classes CANCELLED
HOL-Lattice CANCELLED
Descartes_Sign_Rule CANCELLED
List-Index CANCELLED
Lazy-Lists-II CANCELLED
HOL-TLA-Inc CANCELLED
Open_Induction CANCELLED
IOA-Storage CANCELLED
Marriage CANCELLED
Cartan_FP CANCELLED
Max-Card-Matching CANCELLED
Liouville_Numbers CANCELLED
Skew_Heap CANCELLED
RIPEMD-160-SPARK CANCELLED
Locales CANCELLED
Perfect-Number-Thm CANCELLED
AnselmGod CANCELLED
Ptolemys_Theorem CANCELLED
Minkowskis_Theorem CANCELLED
Main CANCELLED
CofGroups CANCELLED
Lehmer CANCELLED
Lorenz_C1 CANCELLED
FunWithFunctions CANCELLED
Monad_Normalisation CANCELLED
Free-Boolean-Algebra CANCELLED
HOL-Import CANCELLED
Sugar CANCELLED
FFT CANCELLED
Depth-First-Search CANCELLED
IOA-ex CANCELLED
HOL-Mutabelle CANCELLED
Roy_Floyd_Warshall CANCELLED
JEdit CANCELLED
Card_Equiv_Relations CANCELLED
Bondy CANCELLED
General-Triangle CANCELLED
HOL-Real_Asymp-Manual CANCELLED
HOL-TLA-Buffer CANCELLED
How_to_Prove_it CANCELLED
HOL-Prolog CANCELLED
Example-Submission CANCELLED
Ordinals_and_Cardinals CANCELLED
HOL-Proofs: theory HOL.Groups_List
HOL-Proofs: theory HOL.Map
HOL-Proofs: theory HOL.Factorial
HOL-Proofs: theory HOL.GCD
HOL-Proofs: theory HOL.Binomial
HOL-Proofs: theory HOL.Enum
HOL-Proofs: theory HOL.Random
HOL-Proofs: theory HOL.String
HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint
HOL-Proofs: theory HOL.Predicate
HOL-Proofs: theory HOL.Lazy_Sequence
HOL-Proofs: theory HOL.Limited_Sequence
HOL-Proofs: theory HOL.Typerep
HOL-Proofs: theory HOL.Code_Evaluation
HOL-Proofs: theory HOL.Quickcheck_Random
HOL-Proofs: theory HOL.Quickcheck_Exhaustive
HOL-Proofs: theory HOL.Quickcheck_Narrowing
HOL-Proofs: theory HOL.Random_Pred
HOL-Proofs: theory HOL.Random_Sequence
HOL-Proofs: theory HOL.Record
HOL-Proofs: theory HOL.Predicate_Compile
HOL-Proofs: theory HOL.Nitpick
HOL-Proofs: theory HOL.Nunchaku
HOL-Proofs: theory Main
HOL-Proofs: theory HOL-Library.Realizers
Timing HOL-Proofs (4 threads, 562.336s elapsed time, 1273.340s cpu time, 117.648s GC time, factor 2.26)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs
Finished HOL-Proofs (0:10:14 elapsed time, 0:22:50 cpu time, factor 2.23)
Running HOL-Proofs-Lambda ...
Running HOL-Proofs-Extraction ...
Running HOL-Proofs-ex ...
HOL-Proofs-ex: theory HOL-Proofs-ex.Hilbert_Classical
HOL-Proofs-ex: theory HOL-Proofs-ex.Proof_Terms
HOL-Proofs-ex: theory HOL-Isar_Examples.Drinker
HOL-Proofs-Lambda: theory HOL-Library.Code_Target_Int
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Commutation
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Lambda
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListOrder
HOL-Proofs-ex: theory HOL-Proofs-ex.XML_Data
HOL-Proofs-Extraction: theory HOL-Library.Cancellation
HOL-Proofs-Extraction: theory HOL-Library.Code_Abstract_Nat
HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Int
HOL-Proofs-Extraction: theory HOL-Library.Open_State_Syntax
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Warshall
HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Nat
HOL-Proofs-Extraction: theory HOL-Library.Multiset
Timing HOL-Proofs-ex (4 threads, 0.849s elapsed time, 1.832s cpu time, 0.000s GC time, factor 2.16)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-ex
Finished HOL-Proofs-ex (0:00:01 elapsed time)
HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Numeral
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListApplication
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ParRed
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.LambdaType
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListBeta
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman_Extraction
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Util
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Pigeonhole
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Eta
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.InductTermi
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.NormalForm
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.StrongNorm
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Standardization
HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.WeakNorm
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.QuotRem
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Greatest_Common_Divisor
HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Factorial_Ring
HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Euclidean_Algorithm
HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Primes
HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Euclid
Timing HOL-Proofs-Extraction (4 threads, 89.075s elapsed time, 188.452s cpu time, 8.760s GC time, factor 2.12)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Extraction
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Extraction/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Extraction/outline.pdf
Finished HOL-Proofs-Extraction (0:01:33 elapsed time, 0:03:16 cpu time, factor 2.12)
Timing HOL-Proofs-Lambda (4 threads, 106.721s elapsed time, 136.516s cpu time, 4.844s GC time, factor 1.28)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Lambda
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Lambda/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Lambda/outline.pdf
Finished HOL-Proofs-Lambda (0:01:51 elapsed time, 0:02:26 cpu time, factor 1.31)
Unfinished session(s): AVL-Trees, AWN, Abortable_Linearizable_Modules, Abs_Int_ITP2012, Abstract-Hoare-Logics, Abstract-Rewriting, Abstract_Completeness, Abstract_Soundness, Affine_Arithmetic, Aggregation_Algebras, Akra_Bazzi, Algebraic_Numbers, Algebraic_VCs, Allen_Calculus, Amortized_Complexity, AnselmGod, Applicative_Lifting, Architectural_Design_Patterns, ArrowImpossibilityGS, Auto2_HOL, Auto2_Imperative_HOL, AutoFocus-Stream, Automatic_Refinement, AxiomaticCategoryTheory, BDD, BNF_CC, BNF_Operations, Bell_Numbers_Spivey, Berlekamp_Zassenhaus, Bernoulli, Bertrands_Postulate, BinarySearchTree, Binding_Syntax_Theory, Binomial-Heaps, Binomial-Queues, Bondy, Boolean_Expression_Checkers, Bounded_Deducibility_Security, Buchi_Complementation, Budan_Fourier, Buffons_Needle, Buildings, BytecodeLogicJmlTypes, CAVA_Automata, CAVA_Base, CAVA_LTL_Modelchecker, CAVA_Setup, CCS, CISC-Kernel, CRDT, CYK, CakeML, Call_Arity, Card_Equiv_Relations, Card_Multisets, Card_Number_Partitions, Card_Partitions, Cartan_FP, Case_Labeling, Catalan_Numbers, Category, Category2, Category3, Cauchy, Cayley_Hamilton, Certification_Monads, Chord_Segments, Circus, Classes, ClockSynchInst, Codegen, CofGroups, Coinductive, Coinductive_Languages, Collections, Collections_Examples, Comparison_Sort_Lower_Bound, Compiling-Exceptions-Correctly, Completeness, Complx, ComponentDependencies, ConcurrentIMP, Concurrent_Ref_Alg, Concurrent_Revisions, Consensus_Refined, Constructive_Cryptography, Constructor_Funs, Containers, Containers-Benchmarks, CoreC++, Core_DOM, Corec, Count_Complex_Roots, CryptHOL, CryptoBasedCompositionalProperties, DFS_Framework, DPT-SAT-Solver, DataRefinementIBP, Datatype_Order_Generator, Datatypes, Decl_Sem_Fun_PL, Decreasing-Diagrams, Decreasing-Diagrams-II, Deep_Learning, Density_Compiler, Dependent_SIFUM_Refinement, Dependent_SIFUM_Type_Systems, Depth-First-Search, Derangements, Deriving, Descartes_Sign_Rule, Dict_Construction, Differential_Dynamic_Logic, Dijkstra_Shortest_Path, Diophantine_Eqns_Lin_Hom, Dirichlet_L, Dirichlet_Series, DiscretePricing, Discrete_Summation, DiskPaxos, DynamicArchitectures, Dynamic_Tables, E_Transcendental, Echelon_Form, EdmondsKarp_Maxflow, Efficient-Mergesort, Eisbach, Elliptic_Curves_Group_Law, Encodability_Process_Calculi, Epistemic_Logic, Ergodic_Theory, Error_Function, Euler_MacLaurin, Euler_Partition, Example-Submission, FFT, FLP, FOL-Fitting, FOL_Harrison, Factored_Transition_System_Bounding, Falling_Factorial_Sum, Farkas, FeatherweightJava, Featherweight_OCL, Fermat3_4, FileRefinement, FinFun, Finger-Trees, Finite_Automata_HF, First_Order_Terms, First_Welfare_Theorem, Fishburn_Impossibility, Fisher_Yates, Flow_Networks, Floyd_Warshall, Flyspeck-Tame, FocusStreamsCaseStudies, Formal_SSA, Formula_Derivatives, Formula_Derivatives-Examples, Free-Boolean-Algebra, Free-Groups, FunWithFunctions, FunWithTilings, Functional-Automata, Functional_Ordered_Resolution_Prover, Functions, GPU_Kernel_PL, Gabow_SCC, Game_Based_Crypto, Gauss-Jordan-Elim-Fun, Gauss_Jordan, GenClock, General-Triangle, Generic_Deriving, GewirthPGCProof, Girth_Chromatic, GoedelGod, GraphMarkingIBP, Graph_Saturation, Graph_Theory, Green, Groebner_Bases, Gromov_Hyperbolicity, Group-Ring-Module, HOL, HOL-Algebra, HOL-Analysis, HOL-Analysis-ex, HOL-Auth, HOL-Bali, HOL-CSP, HOL-Cardinals, HOL-Codegenerator_Test, HOL-Computational_Algebra, HOL-Corec_Examples, HOL-Data_Structures, HOL-Datatype_Examples, HOL-Decision_Procs, HOL-Eisbach, HOL-Hahn_Banach, HOL-Hoare, HOL-Hoare_Parallel, HOL-Homology, HOL-IMP, HOL-IMPP, HOL-IOA, HOL-Imperative_HOL, HOL-Import, HOL-Induct, HOL-Isar_Examples, HOL-Lattice, HOL-Library, HOL-Matrix_LP, HOL-Metis_Examples, HOL-MicroJava, HOL-Mirabelle, HOL-Mirabelle-ex, HOL-Mutabelle, HOL-NanoJava, HOL-Nitpick_Examples, HOL-Nominal, HOL-Nominal-Examples, HOL-Nonstandard_Analysis, HOL-Nonstandard_Analysis-Examples, HOL-Number_Theory, HOL-ODE-ARCH-COMP, HOL-ODE-Examples, HOL-ODE-Numerics, HOL-Predicate_Compile_Examples, HOL-Probability, HOL-Probability-ex, HOL-Prolog, HOL-Quickcheck_Examples, HOL-Quotient_Examples, HOL-Real_Asymp, HOL-Real_Asymp-Manual, HOL-SET_Protocol, HOL-SPARK, HOL-SPARK-Examples, HOL-SPARK-Manual, HOL-Statespace, HOL-TLA, HOL-TLA-Buffer, HOL-TLA-Inc, HOL-TLA-Memory, HOL-TPTP, HOL-Types_To_Sets, HOL-UNITY, HOL-Unix, HOL-Word, HOL-Word-SMT_Examples, HOL-ZF, HOL-ex, HOLCF, HOLCF-FOCUS, HOLCF-IMP, HOLCF-Library, HOLCF-Prelude, HOLCF-Tutorial, HOLCF-ex, HRB-Slicing, Heard_Of, HereditarilyFinite, Hermite, Hidden_Markov_Models, Higher_Order_Terms, Hoare_Time, HotelKeyCards, How_to_Prove_it, Huffman, Hybrid_Multi_Lane_Spatial_Logic, HyperCTL, IEEE_Floating_Point, IMAP-CRDT, IMP2, IOA, IOA-ABP, IOA-NTP, IOA-Storage, IOA-ex, IP_Addresses, Imperative_Insertion_Sort, Implementation, Impossible_Geometry, Incompleteness, Incredible_Proof_Machine, Inductive_Confidentiality, InfPathElimination, InformationFlowSlicing, InformationFlowSlicing_Inter, Integration, Iptables_Semantics, Iptables_Semantics_Examples, Irrationality_J_Hancl, Isabelle_Meta_Model, Isar_Ref, JEdit, JNF-AFP-Lib, Jinja, JiveDataStoreModel, Jordan_Hoelder, Jordan_Normal_Form, KAD, KAT_and_DRA, KBPs, KD_Tree, Key_Agreement_Strong_Adversaries, Kleene_Algebra, Knot_Theory, Knuth_Morris_Pratt, Koenigsberg_Friendship, Kruskal, Kuratowski_Closure_Complement, LEM, LLL_Basis_Reduction, LLL_Factorization, LOFT, LTL, LTL_Master_Theorem, LTL_to_DRA, LTL_to_GBA, Lam-ml-Normalization, LambdaAuth, LambdaMu, Lambda_Free_EPO, Lambda_Free_KBOs, Lambda_Free_RPOs, Landau_Symbols, Latin_Square, LatticeProperties, Launchbury, Lazy-Lists-II, Lazy_Case, Lehmer, Lifting_Definition_Option, LightweightJava, LinearQuantifierElim, Linear_Recurrences, Linear_Recurrences_Solver, Liouville_Numbers, List-Index, List-Infinite, List_Interleaving, List_Inversions, List_Update, LocalLexing, Locales, Localization_Ring, Locally-Nameless-Sigma, Lorenz_Approximation, Lorenz_C0, Lorenz_C1, Lowe_Ontological_Argument, Lower_Semicontinuous, Lp, MFMC_Countable, MSO_Regex_Equivalence, Main, Markov_Models, Marriage, Mason_Stothers, Matrix, Matrix_Tensor, Matroids, Max-Card-Matching, Median_Of_Medians_Selection, Menger, MiniML, Minimal_SSA, Minkowskis_Theorem, Minsky_Machines, Modal_Logics_for_NTS, Modular_Assembly_Kit_Security, Monad_Memo_DP, Monad_Normalisation, MonoBoolTranAlgebra, MonoidalCategory, Monomorphic_Monad, MuchAdoAboutTwo, Multi_Party_Computation, Multirelations, Myhill-Nerode, Name_Carrying_Type_Inference, Nat-Interval-Logic, Native_Word, Nested_Multisets_Ordinals, Network_Security_Policy_Verification, Neumann_Morgenstern_Utility, No_FTL_observers, Nominal2, Noninterference_CSP, Noninterference_Concurrent_Composition, Noninterference_Generic_Unwinding, Noninterference_Inductive_Unwinding, Noninterference_Ipurge_Unwinding, Noninterference_Sequential_Composition, NormByEval, Octonions, Old_Datatype_Show, OpSets, Open_Induction, Optics, Optimal_BST, Orbit_Stabiliser, Order_Lattice_Props, Ordered_Resolution_Prover, Ordinal, Ordinals_and_Cardinals, Ordinary_Differential_Equations, PCF, PLM, POPLmark-deBruijn, PSemigroupsConvolution, Pairing_Heap, Paraconsistency, Parity_Game, Partial_Function_MR, Partial_Order_Reduction, Password_Authentication_Protocol, Pell, Perfect-Number-Thm, Perron_Frobenius, Pi_Calculus, Pi_Transcendental, Planarity_Certificates, Polynomial_Factorization, Polynomial_Interpolation, Polynomials, Pop_Refinement, Posix-Lexing, Possibilistic_Noninterference, Pratt_Certificate, Pre_BZ, Presburger-Automata, Prime_Distribution_Elementary, Prime_Harmonic_Series, Prime_Number_Theorem, Priority_Queue_Braun, Probabilistic_Noninterference, Probabilistic_Prime_Tests, Probabilistic_System_Zoo, Probabilistic_System_Zoo-BNFs, Probabilistic_System_Zoo-Non_BNFs, Probabilistic_Timed_Automata, Probabilistic_While, Prog_Prove, Program-Conflict-Analysis, Projective_Geometry, Promela, Proof_Strategy_Language, PropResPI, Propositional_Proof_Systems, Prpu_Maxflow, PseudoHoops, Psi_Calculi, Ptolemys_Theorem, QHLProver, QR_Decomposition, Quantales, Quaternions, Quick_Sort_Cost, RIPEMD-160-SPARK, ROBDD, RSAPSS, Ramsey-Infinite, Random_BSTs, Random_Graph_Subgraph_Threshold, Randomised_BSTs, Randomised_Social_Choice, Rank_Nullity_Theorem, Real_Impl, Recursion-Theory-I, Refine_Imperative_HOL, Refine_Monadic, RefinementReactive, Regex_Equivalence, Regular-Sets, Regular_Algebras, Relation_Algebra, Rep_Fin_Groups, Residuated_Lattices, Resolution_FOL, Rewriting_Z, Ribbon_Proofs, Robbins-Conjecture, Root_Balanced_Tree, Routing, Roy_Floyd_Warshall, SATSolverVerification, SDS_Impossibility, SIFPL, SIFUM_Type_Systems, SM, SM_Base, SPARCv8, Safe_OCL, Secondary_Sylow, Security_Protocol_Refinement, Selection_Heap_Sort, SenSocialChoice, Separata, Separation_Algebra, Separation_Logic_Imperative_HOL, Sepref_Basic, Sepref_IICF, Sepref_Prereq, SequentInvertibility, Shivers-CFA, ShortestPath, Show, Signature_Groebner, Simpl, Simple_Firewall, Simplex, Skew_Heap, Slicing, Smooth_Manifolds, Sort_Encodings, Source_Coding_Theorem, Special_Function_Bounds, Splay_Tree, Sqrt_Babylonian, Stable_Matching, Statecharts, Stern_Brocot, Stewart_Apollonius, Stirling_Formula, Stochastic_Matrices, Stone_Algebras, Stone_Kleene_Relation_Algebras, Stone_Relation_Algebras, Store_Buffer_Reduction, Stream-Fusion, Stream_Fusion_Code, Strong_Security, Sturm_Sequences, Sturm_Tarski, Stuttering_Equivalence, Subresultants, Sugar, SumSquares, SuperCalc, Surprise_Paradox, Symmetric_Polynomials, TLA, Tail_Recursive_Functions, Tarskis_Geometry, Taylor_Models, Timed_Automata, Topology, TortoiseHare, Transcendence_Series_Hancl_Rucki, Transformer_Semantics, Transition_Systems_and_Automata, Transitive-Closure, Transitive-Closure-II, Treaps, Tree-Automata, Tree_Decomposition, Triangle, Trie, Tutorial, Twelvefold_Way, Tycon, Typeclass_Hierarchy, Types_Tableaus_and_Goedels_God, UPF, UPF_Firewall, UTP, UTP-Toolkit, Universal_Turing_Machine, UpDown_Scheme, Valuation, VectorSpace, Verified-Prover, VerifyThis2018, Vickrey_Clarke_Groves, VolpanoSmith, WHATandWHERE_Security, WebAssembly, Weight_Balanced_Trees, Well_Quasi_Orders, Winding_Number_Eval, Word_Lib, WorkerWrapper, XML, Zeta_Function, pGCL

=== TIMING ===

Group AFP: 0:00:00 elapsed time
Group main: 0:03:26 elapsed time, 0:10:20 cpu time, factor 3.00
Group doc: 0:00:00 elapsed time
Group timing: 0:13:38 elapsed time, 0:28:33 cpu time, factor 2.09
Group large: 0:00:00 elapsed time
Group no_doc: 0:00:00 elapsed time
Overall: 0:13:48 elapsed time, 0:38:56 cpu time, factor 2.82

=== FAILED SESSIONS ===

Session HOL-Matrix_LP: CANCELLED
Session InfPathElimination: CANCELLED
Session Liouville_Numbers: CANCELLED
Session SM_Base: CANCELLED
Session KAD: CANCELLED
Session Lifting_Definition_Option: CANCELLED
Session Fermat3_4: CANCELLED
Session Random_BSTs: CANCELLED
Session IMAP-CRDT: CANCELLED
Session Pell: CANCELLED
Session Markov_Models: CANCELLED
Session Stern_Brocot: CANCELLED
Session Lambda_Free_KBOs: CANCELLED
Session Taylor_Models: CANCELLED
Session Pi_Calculus: CANCELLED
Session Containers: CANCELLED
Session Simplex: CANCELLED
Session Probabilistic_Prime_Tests: CANCELLED
Session Integration: CANCELLED
Session Auto2_HOL: CANCELLED
Session Weight_Balanced_Trees: CANCELLED
Session Sugar: CANCELLED
Session Efficient-Mergesort: CANCELLED
Session Free-Boolean-Algebra: CANCELLED
Session Core_DOM: CANCELLED
Session Category3: CANCELLED
Session Datatype_Order_Generator: CANCELLED
Session Category2: CANCELLED
Session Regular-Sets: CANCELLED
Session Multi_Party_Computation: CANCELLED
Session Routing: CANCELLED
Session Dict_Construction: CANCELLED
Session Separation_Logic_Imperative_HOL: CANCELLED
Session Probabilistic_While: CANCELLED
Session Posix-Lexing: CANCELLED
Session Gromov_Hyperbolicity: CANCELLED
Session Impossible_Geometry: CANCELLED
Session QR_Decomposition: CANCELLED
Session Lazy-Lists-II: CANCELLED
Session GenClock: CANCELLED
Session Gauss_Jordan: CANCELLED
Session Security_Protocol_Refinement: CANCELLED
Session Chord_Segments: CANCELLED
Session Topology: CANCELLED
Session Subresultants: CANCELLED
Session Multirelations: CANCELLED
Session Flyspeck-Tame: CANCELLED
Session CofGroups: CANCELLED
Session Tarskis_Geometry: CANCELLED
Session Probabilistic_System_Zoo: CANCELLED
Session Lam-ml-Normalization: CANCELLED
Session WorkerWrapper: CANCELLED
Session ComponentDependencies: CANCELLED
Session HOL-Probability: CANCELLED
Session Abs_Int_ITP2012: CANCELLED
Session AnselmGod: CANCELLED
Session Simple_Firewall: CANCELLED
Session Tree_Decomposition: CANCELLED
Session Factored_Transition_System_Bounding: CANCELLED
Session First_Welfare_Theorem: CANCELLED
Session List-Index: CANCELLED
Session HOL-Predicate_Compile_Examples: CANCELLED
Session Slicing: CANCELLED
Session Perfect-Number-Thm: CANCELLED
Session CAVA_Setup: CANCELLED
Session Completeness: CANCELLED
Session Zeta_Function: CANCELLED
Session Noninterference_Sequential_Composition: CANCELLED
Session Probabilistic_System_Zoo-BNFs: CANCELLED
Session Count_Complex_Roots: CANCELLED
Session HOL-Word: CANCELLED
Session Propositional_Proof_Systems: CANCELLED
Session Refine_Monadic: CANCELLED
Session Iptables_Semantics_Examples: CANCELLED
Session Perron_Frobenius: CANCELLED
Session HOL-Nitpick_Examples: CANCELLED
Session HOL: FAILED 2
Session BNF_CC: CANCELLED
Session Codegen: CANCELLED
Session Buildings: CANCELLED
Session Modular_Assembly_Kit_Security: CANCELLED
Session Decl_Sem_Fun_PL: CANCELLED
Session Randomised_Social_Choice: CANCELLED
Session Containers-Benchmarks: CANCELLED
Session Pop_Refinement: CANCELLED
Session Featherweight_OCL: CANCELLED
Session Valuation: CANCELLED
Session Category: CANCELLED
Session No_FTL_observers: CANCELLED
Session Case_Labeling: CANCELLED
Session Transitive-Closure-II: CANCELLED
Session Types_Tableaus_and_Goedels_God: CANCELLED
Session Timed_Automata: CANCELLED
Session Derangements: CANCELLED
Session XML: CANCELLED
Session Regex_Equivalence: CANCELLED
Session EdmondsKarp_Maxflow: CANCELLED
Session MiniML: CANCELLED
Session Stone_Relation_Algebras: CANCELLED
Session Card_Multisets: CANCELLED
Session Treaps: CANCELLED
Session Formula_Derivatives: CANCELLED
Session Ordinary_Differential_Equations: CANCELLED
Session Projective_Geometry: CANCELLED
Session Nat-Interval-Logic: CANCELLED
Session Discrete_Summation: CANCELLED
Session Dependent_SIFUM_Type_Systems: CANCELLED
Session IOA-NTP: CANCELLED
Session Secondary_Sylow: CANCELLED
Session HOL-Types_To_Sets: CANCELLED
Session HOL-NanoJava: CANCELLED
Session Circus: CANCELLED
Session Quick_Sort_Cost: CANCELLED
Session Source_Coding_Theorem: CANCELLED
Session Promela: CANCELLED
Session Formal_SSA: CANCELLED
Session HOL-TLA: CANCELLED
Session SM: CANCELLED
Session Quaternions: CANCELLED
Session Vickrey_Clarke_Groves: CANCELLED
Session PseudoHoops: CANCELLED
Session HOL-TLA-Buffer: CANCELLED
Session HOL-SPARK-Manual: CANCELLED
Session Prog_Prove: CANCELLED
Session SequentInvertibility: CANCELLED
Session HOL-SPARK: CANCELLED
Session Regular_Algebras: CANCELLED
Session Network_Security_Policy_Verification: CANCELLED
Session Trie: CANCELLED
Session Program-Conflict-Analysis: CANCELLED
Session Key_Agreement_Strong_Adversaries: CANCELLED
Session FileRefinement: CANCELLED
Session Smooth_Manifolds: CANCELLED
Session HOL-Hahn_Banach: CANCELLED
Session Corec: CANCELLED
Session Bell_Numbers_Spivey: CANCELLED
Session Residuated_Lattices: CANCELLED
Session Example-Submission: CANCELLED
Session Prime_Harmonic_Series: CANCELLED
Session NormByEval: CANCELLED
Session Decreasing-Diagrams: CANCELLED
Session Selection_Heap_Sort: CANCELLED
Session SPARCv8: CANCELLED
Session Stirling_Formula: CANCELLED
Session Pratt_Certificate: CANCELLED
Session Old_Datatype_Show: CANCELLED
Session Octonions: CANCELLED
Session Architectural_Design_Patterns: CANCELLED
Session Catalan_Numbers: CANCELLED
Session Graph_Theory: CANCELLED
Session GPU_Kernel_PL: CANCELLED
Session Cayley_Hamilton: CANCELLED
Session Dependent_SIFUM_Refinement: CANCELLED
Session Nested_Multisets_Ordinals: CANCELLED
Session Abstract_Soundness: CANCELLED
Session LocalLexing: CANCELLED
Session Deriving: CANCELLED
Session HOL-Data_Structures: CANCELLED
Session LEM: CANCELLED
Session Cartan_FP: CANCELLED
Session How_to_Prove_it: CANCELLED
Session Comparison_Sort_Lower_Bound: CANCELLED
Session Prime_Distribution_Elementary: CANCELLED
Session RefinementReactive: CANCELLED
Session Minsky_Machines: CANCELLED
Session Iptables_Semantics: CANCELLED
Session Generic_Deriving: CANCELLED
Session Typeclass_Hierarchy: CANCELLED
Session Consensus_Refined: CANCELLED
Session Akra_Bazzi: CANCELLED
Session HOL-ODE-Examples: CANCELLED
Session Farkas: CANCELLED
Session HOL-Hoare_Parallel: CANCELLED
Session Imperative_Insertion_Sort: CANCELLED
Session Functional_Ordered_Resolution_Prover: CANCELLED
Session HOLCF: CANCELLED
Session HOLCF-Library: CANCELLED
Session BinarySearchTree: CANCELLED
Session Randomised_BSTs: CANCELLED
Session HOL-CSP: CANCELLED
Session HOL-Induct: CANCELLED
Session HOLCF-FOCUS: CANCELLED
Session Localization_Ring: CANCELLED
Session HOL-ZF: CANCELLED
Session Paraconsistency: CANCELLED
Session KD_Tree: CANCELLED
Session HOL-IOA: CANCELLED
Session PLM: CANCELLED
Session Sepref_IICF: CANCELLED
Session IEEE_Floating_Point: CANCELLED
Session Classes: CANCELLED
Session HOL-Nonstandard_Analysis-Examples: CANCELLED
Session DFS_Framework: CANCELLED
Session Higher_Order_Terms: CANCELLED
Session List-Infinite: CANCELLED
Session Launchbury: CANCELLED
Session HOL-Mutabelle: CANCELLED
Session Transformer_Semantics: CANCELLED
Session Diophantine_Eqns_Lin_Hom: CANCELLED
Session Relation_Algebra: CANCELLED
Session LTL_to_DRA: CANCELLED
Session CryptHOL: CANCELLED
Session Free-Groups: CANCELLED
Session FocusStreamsCaseStudies: CANCELLED
Session Lehmer: CANCELLED
Session Stream_Fusion_Code: CANCELLED
Session Safe_OCL: CANCELLED
Session Pre_BZ: CANCELLED
Session WebAssembly: CANCELLED
Session Winding_Number_Eval: CANCELLED
Session Binding_Syntax_Theory: CANCELLED
Session Parity_Game: CANCELLED
Session SumSquares: CANCELLED
Session FeatherweightJava: CANCELLED
Session GraphMarkingIBP: CANCELLED
Session Linear_Recurrences: CANCELLED
Session Name_Carrying_Type_Inference: CANCELLED
Session HOL-Nominal: CANCELLED
Session Dirichlet_L: CANCELLED
Session Priority_Queue_Braun: CANCELLED
Session Constructive_Cryptography: CANCELLED
Session Statecharts: CANCELLED
Session Open_Induction: CANCELLED
Session Concurrent_Ref_Alg: CANCELLED
Session HOL-Eisbach: CANCELLED
Session FOL_Harrison: CANCELLED
Session Sturm_Sequences: CANCELLED
Session IMP2: CANCELLED
Session Bondy: CANCELLED
Session JiveDataStoreModel: CANCELLED
Session LTL: CANCELLED
Session Huffman: CANCELLED
Session Coinductive: CANCELLED
Session Mason_Stothers: CANCELLED
Session HOL-Statespace: CANCELLED
Session HOL-Datatype_Examples: CANCELLED
Session Incompleteness: CANCELLED
Session DataRefinementIBP: CANCELLED
Session HOL-Isar_Examples: CANCELLED
Session Card_Partitions: CANCELLED
Session Locally-Nameless-Sigma: CANCELLED
Session Coinductive_Languages: CANCELLED
Session SenSocialChoice: CANCELLED
Session PCF: CANCELLED
Session Encodability_Process_Calculi: CANCELLED
Session LLL_Factorization: CANCELLED
Session HOL-Cardinals: CANCELLED
Session Optimal_BST: CANCELLED
Session WHATandWHERE_Security: CANCELLED
Session BytecodeLogicJmlTypes: CANCELLED
Session Fishburn_Impossibility: CANCELLED
Session Dijkstra_Shortest_Path: CANCELLED
Session HOL-Import: CANCELLED
Session List_Interleaving: CANCELLED
Session Finite_Automata_HF: CANCELLED
Session pGCL: CANCELLED
Session Resolution_FOL: CANCELLED
Session Bertrands_Postulate: CANCELLED
Session Landau_Symbols: CANCELLED
Session Card_Equiv_Relations: CANCELLED
Session Euler_Partition: CANCELLED
Session FunWithFunctions: CANCELLED
Session Lorenz_C0: CANCELLED
Session Signature_Groebner: CANCELLED
Session HereditarilyFinite: CANCELLED
Session Possibilistic_Noninterference: CANCELLED
Session Psi_Calculi: CANCELLED
Session Noninterference_Generic_Unwinding: CANCELLED
Session HOL-Word-SMT_Examples: CANCELLED
Session Lazy_Case: CANCELLED
Session HOLCF-ex: CANCELLED
Session Monomorphic_Monad: CANCELLED
Session Card_Number_Partitions: CANCELLED
Session Stewart_Apollonius: CANCELLED
Session List_Inversions: CANCELLED
Session HOL-IMPP: CANCELLED
Session AutoFocus-Stream: CANCELLED
Session Partial_Order_Reduction: CANCELLED
Session LightweightJava: CANCELLED
Session Separation_Algebra: CANCELLED
Session Datatypes: CANCELLED
Session Floyd_Warshall: CANCELLED
Session HOL-Nominal-Examples: CANCELLED
Session ArrowImpossibilityGS: CANCELLED
Session Optics: CANCELLED
Session LatticeProperties: CANCELLED
Session Lower_Semicontinuous: CANCELLED
Session Sort_Encodings: CANCELLED
Session Matrix_Tensor: CANCELLED
Session Binomial-Queues: CANCELLED
Session DiscretePricing: CANCELLED
Session Amortized_Complexity: CANCELLED
Session Prime_Number_Theorem: CANCELLED
Session KBPs: CANCELLED
Session Noninterference_Ipurge_Unwinding: CANCELLED
Session Aggregation_Algebras: CANCELLED
Session IOA-ABP: CANCELLED
Session Algebraic_Numbers: CANCELLED
Session Max-Card-Matching: CANCELLED
Session Dynamic_Tables: CANCELLED
Session HOL-Auth: CANCELLED
Session Abstract-Rewriting: CANCELLED
Session HOL-MicroJava: CANCELLED
Session Collections: CANCELLED
Session CISC-Kernel: CANCELLED
Session HOL-Corec_Examples: CANCELLED
Session IOA-ex: CANCELLED
Session HOL-Real_Asymp: CANCELLED
Session QHLProver: CANCELLED
Session Kleene_Algebra: CANCELLED
Session Native_Word: CANCELLED
Session FFT: CANCELLED
Session HOL-TLA-Memory: CANCELLED
Session Matroids: CANCELLED
Session Neumann_Morgenstern_Utility: CANCELLED
Session UTP-Toolkit: CANCELLED
Session InformationFlowSlicing_Inter: CANCELLED
Session Nominal2: CANCELLED
Session Call_Arity: CANCELLED
Session Buffons_Needle: CANCELLED
Session General-Triangle: CANCELLED
Session HOL-Bali: CANCELLED
Session Sturm_Tarski: CANCELLED
Session LOFT: CANCELLED
Session HOL-Real_Asymp-Manual: CANCELLED
Session Ptolemys_Theorem: CANCELLED
Session Functional-Automata: CANCELLED
Session Pi_Transcendental: CANCELLED
Session Tutorial: CANCELLED
Session VectorSpace: CANCELLED
Session Green: CANCELLED
Session Prpu_Maxflow: CANCELLED
Session Stone_Kleene_Relation_Algebras: CANCELLED
Session Roy_Floyd_Warshall: CANCELLED
Session LinearQuantifierElim: CANCELLED
Session MSO_Regex_Equivalence: CANCELLED
Session Abstract-Hoare-Logics: CANCELLED
Session Partial_Function_MR: CANCELLED
Session HOLCF-Prelude: CANCELLED
Session Graph_Saturation: CANCELLED
Session InformationFlowSlicing: CANCELLED
Session JNF-AFP-Lib: CANCELLED
Session Abstract_Completeness: CANCELLED
Session Password_Authentication_Protocol: CANCELLED
Session Modal_Logics_for_NTS: CANCELLED
Session ShortestPath: CANCELLED
Session Gauss-Jordan-Elim-Fun: CANCELLED
Session SIFPL: CANCELLED
Session Sepref_Basic: CANCELLED
Session Minimal_SSA: CANCELLED
Session Implementation: CANCELLED
Session BDD: CANCELLED
Session Kruskal: CANCELLED
Session IOA-Storage: CANCELLED
Session MonoidalCategory: CANCELLED
Session RSAPSS: CANCELLED
Session ClockSynchInst: CANCELLED
Session Locales: CANCELLED
Session HOL-UNITY: CANCELLED
Session Lowe_Ontological_Argument: CANCELLED
Session Special_Function_Bounds: CANCELLED
Session CakeML: CANCELLED
Session CoreC++: CANCELLED
Session Gabow_SCC: CANCELLED
Session DiskPaxos: CANCELLED
Session Menger: CANCELLED
Session Hidden_Markov_Models: CANCELLED
Session CYK: CANCELLED
Session Skew_Heap: CANCELLED
Session Compiling-Exceptions-Correctly: CANCELLED
Session RIPEMD-160-SPARK: CANCELLED
Session Applicative_Lifting: CANCELLED
Session Planarity_Certificates: CANCELLED
Session HOL-TLA-Inc: CANCELLED
Session Elliptic_Curves_Group_Law: CANCELLED
Session SDS_Impossibility: CANCELLED
Session Dirichlet_Series: CANCELLED
Session AWN: CANCELLED
Session Monad_Memo_DP: CANCELLED
Session E_Transcendental: CANCELLED
Session Group-Ring-Module: CANCELLED
Session CCS: CANCELLED
Session Separata: CANCELLED
Session Boolean_Expression_Checkers: CANCELLED
Session Auto2_Imperative_HOL: CANCELLED
Session Word_Lib: CANCELLED
Session Lambda_Free_EPO: CANCELLED
Session HOL-ex: CANCELLED
Session Pairing_Heap: CANCELLED
Session HOL-Quickcheck_Examples: CANCELLED
Session HOL-ODE-Numerics: CANCELLED
Session Real_Impl: CANCELLED
Session Ordered_Resolution_Prover: CANCELLED
Session Symmetric_Polynomials: CANCELLED
Session IP_Addresses: CANCELLED
Session FOL-Fitting: CANCELLED
Session SIFUM_Type_Systems: CANCELLED
Session Root_Balanced_Tree: CANCELLED
Session HOL-SPARK-Examples: CANCELLED
Session UTP: CANCELLED
Session VolpanoSmith: CANCELLED
Session Density_Compiler: CANCELLED
Session Incredible_Proof_Machine: CANCELLED
Session JEdit: CANCELLED
Session HOL-Unix: CANCELLED
Session VerifyThis2018: CANCELLED
Session Recursion-Theory-I: CANCELLED
Session Bernoulli: CANCELLED
Session HOL-TPTP: CANCELLED
Session HOL-Imperative_HOL: CANCELLED
Session Deep_Learning: CANCELLED
Session Girth_Chromatic: CANCELLED
Session Formula_Derivatives-Examples: CANCELLED
Session Ramsey-Infinite: CANCELLED
Session Median_Of_Medians_Selection: CANCELLED
Session Bounded_Deducibility_Security: CANCELLED
Session Concurrent_Revisions: CANCELLED
Session HRB-Slicing: CANCELLED
Session LTL_to_GBA: CANCELLED
Session Jordan_Normal_Form: CANCELLED
Session HOL-Probability-ex: CANCELLED
Session HOL-Metis_Examples: CANCELLED
Session SATSolverVerification: CANCELLED
Session HOL-IMP: CANCELLED
Session HyperCTL: CANCELLED
Session DynamicArchitectures: CANCELLED
Session Ordinal: CANCELLED
Session DPT-SAT-Solver: CANCELLED
Session Simpl: CANCELLED
Session Polynomial_Interpolation: CANCELLED
Session Lorenz_C1: CANCELLED
Session Buchi_Complementation: CANCELLED
Session Finger-Trees: CANCELLED
Session Differential_Dynamic_Logic: CANCELLED
Session Matrix: CANCELLED
Session HOL-Homology: CANCELLED
Session Irrationality_J_Hancl: CANCELLED
Session LambdaAuth: CANCELLED
Session ConcurrentIMP: CANCELLED
Session Ergodic_Theory: CANCELLED
Session Hybrid_Multi_Lane_Spatial_Logic: CANCELLED
Session Error_Function: CANCELLED
Session Stochastic_Matrices: CANCELLED
Session Lp: CANCELLED
Session HOL-Analysis: CANCELLED
Session Orbit_Stabiliser: CANCELLED
Session Main: CANCELLED
Session First_Order_Terms: CANCELLED
Session KAT_and_DRA: CANCELLED
Session Random_Graph_Subgraph_Threshold: CANCELLED
Session HOL-Lattice: CANCELLED
Session Functions: CANCELLED
Session POPLmark-deBruijn: CANCELLED
Session Abortable_Linearizable_Modules: CANCELLED
Session CAVA_Base: CANCELLED
Session Stone_Algebras: CANCELLED
Session Constructor_Funs: CANCELLED
Session TLA: CANCELLED
Session HOL-ODE-ARCH-COMP: CANCELLED
Session Stream-Fusion: CANCELLED
Session Tree-Automata: CANCELLED
Session Collections_Examples: CANCELLED
Session Marriage: CANCELLED
Session Allen_Calculus: CANCELLED
Session Sqrt_Babylonian: CANCELLED
Session CryptoBasedCompositionalProperties: CANCELLED
Session Order_Lattice_Props: CANCELLED
Session Robbins-Conjecture: CANCELLED
Session FinFun: CANCELLED
Session Hoare_Time: CANCELLED
Session AxiomaticCategoryTheory: CANCELLED
Session Show: CANCELLED
Session Minkowskis_Theorem: CANCELLED
Session Noninterference_Inductive_Unwinding: CANCELLED
Session HOL-SET_Protocol: CANCELLED
Session Koenigsberg_Friendship: CANCELLED
Session Universal_Turing_Machine: CANCELLED
Session CRDT: CANCELLED
Session Stable_Matching: CANCELLED
Session Hermite: CANCELLED
Session Well_Quasi_Orders: CANCELLED
Session Transcendence_Series_Hancl_Rucki: CANCELLED
Session Game_Based_Crypto: CANCELLED
Session Linear_Recurrences_Solver: CANCELLED
Session PropResPI: CANCELLED
Session UPF: CANCELLED
Session BNF_Operations: CANCELLED
Session LTL_Master_Theorem: CANCELLED
Session HOLCF-Tutorial: CANCELLED
Session Ordinals_and_Cardinals: CANCELLED
Session HOL-Number_Theory: CANCELLED
Session Transition_Systems_and_Automata: CANCELLED
Session Knuth_Morris_Pratt: CANCELLED
Session Jinja: CANCELLED
Session Eisbach: CANCELLED
Session Kuratowski_Closure_Complement: CANCELLED
Session GoedelGod: CANCELLED
Session Probabilistic_Noninterference: CANCELLED
Session Fisher_Yates: CANCELLED
Session Complx: CANCELLED
Session HOL-Decision_Procs: CANCELLED
Session Rep_Fin_Groups: CANCELLED
Session FLP: CANCELLED
Session Euler_MacLaurin: CANCELLED
Session FunWithTilings: CANCELLED
Session Transitive-Closure: CANCELLED
Session MonoBoolTranAlgebra: CANCELLED
Session Surprise_Paradox: CANCELLED
Session CAVA_LTL_Modelchecker: CANCELLED
Session HOL-Library: CANCELLED
Session Polynomial_Factorization: CANCELLED
Session HOLCF-IMP: CANCELLED
Session List_Update: CANCELLED
Session Sepref_Prereq: CANCELLED
Session HOL-Codegenerator_Test: CANCELLED
Session Certification_Monads: CANCELLED
Session Cauchy: CANCELLED
Session HOL-Mirabelle-ex: CANCELLED
Session MuchAdoAboutTwo: CANCELLED
Session Binomial-Heaps: CANCELLED
Session Refine_Imperative_HOL: CANCELLED
Session Strong_Security: CANCELLED
Session Heard_Of: CANCELLED
Session Depth-First-Search: CANCELLED
Session HOL-Quotient_Examples: CANCELLED
Session Myhill-Nerode: CANCELLED
Session AVL-Trees: CANCELLED
Session Presburger-Automata: CANCELLED
Session Rewriting_Z: CANCELLED
Session Flow_Networks: CANCELLED
Session UPF_Firewall: CANCELLED
Session Noninterference_Concurrent_Composition: CANCELLED
Session HOL-Nonstandard_Analysis: CANCELLED
Session Affine_Arithmetic: CANCELLED
Session HOL-Mirabelle: CANCELLED
Session PSemigroupsConvolution: CANCELLED
Session Knot_Theory: CANCELLED
Session HOL-Computational_Algebra: CANCELLED
Session Epistemic_Logic: CANCELLED
Session CAVA_Automata: CANCELLED
Session ROBDD: CANCELLED
Session Berlekamp_Zassenhaus: CANCELLED
Session Splay_Tree: CANCELLED
Session Polynomials: CANCELLED
Session Store_Buffer_Reduction: CANCELLED
Session Latin_Square: CANCELLED
Session Monad_Normalisation: CANCELLED
Session Probabilistic_Timed_Automata: CANCELLED
Session Proof_Strategy_Language: CANCELLED
Session Noninterference_CSP: CANCELLED
Session Rank_Nullity_Theorem: CANCELLED
Session HOL-Algebra: CANCELLED
Session SuperCalc: CANCELLED
Session GewirthPGCProof: CANCELLED
Session OpSets: CANCELLED
Session Isar_Ref: CANCELLED
Session Probabilistic_System_Zoo-Non_BNFs: CANCELLED
Session Falling_Factorial_Sum: CANCELLED
Session Decreasing-Diagrams-II: CANCELLED
Session Jordan_Hoelder: CANCELLED
Session Automatic_Refinement: CANCELLED
Session LLL_Basis_Reduction: CANCELLED
Session MFMC_Countable: CANCELLED
Session Tycon: CANCELLED
Session Inductive_Confidentiality: CANCELLED
Session Lambda_Free_RPOs: CANCELLED
Session UpDown_Scheme: CANCELLED
Session Twelvefold_Way: CANCELLED
Session Ribbon_Proofs: CANCELLED
Session Algebraic_VCs: CANCELLED
Session Echelon_Form: CANCELLED
Session Lorenz_Approximation: CANCELLED
Session Groebner_Bases: CANCELLED
Session Verified-Prover: CANCELLED
Session Tail_Recursive_Functions: CANCELLED
Session HOL-Analysis-ex: CANCELLED
Session Isabelle_Meta_Model: CANCELLED
Session HOL-Hoare: CANCELLED
Session Triangle: CANCELLED
Session LambdaMu: CANCELLED
Session Descartes_Sign_Rule: CANCELLED
Session Budan_Fourier: CANCELLED
Session Shivers-CFA: CANCELLED
Session IOA: CANCELLED
Session Quantales: CANCELLED
Session HotelKeyCards: CANCELLED
Session TortoiseHare: CANCELLED
Session Stuttering_Equivalence: CANCELLED
Session HOL-Prolog: CANCELLED

=== DEPENDENCIES ===

Generating dependencies file ...
Writing dependencies file ...

=== REPORT ===

Writing report file ...

=== SITEGEN ===

Writing status file ...
Running sitegen ...
Success: Generated topics.html
Success: Generated index.html
Success: Generated html files for 475 entries
Success: Generated statistics.html
Success: Generated download.html
Success: Generated about.html
Success: Generated citing.html
Success: Generated updating.html
Success: Generated search.html
Success: Generated submitting.html
Success: Generated using.html
Success: Generated rss.xml
Success: Generated status.html
Checked directory thys. Found 0 warnings.
Packing tars ...

=== NOTIFICATIONS ===


=== COMPLETED ===

Build step 'Execute shell' marked build as failure
Archiving artifacts
Started calculate disk usage of build
Finished Calculation of disk usage of build in 0 seconds
Started calculate disk usage of workspace
Finished Calculation of disk usage of workspace in 0 seconds
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@mail46.informatik.tu-muenchen.de
Finished: FAILURE