Started by an SCM change
Running as SYSTEM
[EnvInject] - Loading node environment variables.
Building remotely on workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-all
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
pulling from http://isabelle.in.tum.de/repos/isabelle/
real URL is https://isabelle.in.tum.de/repos/isabelle/
no changes found
[isabelle-all] $ hg update --clean --rev default
131 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 f2094906e4916b460cded1a5a7938d24ff6327a1 --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(f2094906e4916b460cded1a5a7938d24ff6327a1)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
[afp] $ hg pull --rev default
pulling from https://foss.heptapod.net/isa-afp/afp-devel/
no changes found
[afp] $ hg update --clean --rev default
0 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 d81cfd823ae95fa189c898bf2ba24c81bc2a1637 --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(d81cfd823ae95fa189c898bf2ba24c81bc2a1637)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-all] $ /bin/sh -xe /tmp/jenkins16529520059888205989.sh
+ Admin/jenkins/run_build all
+ set -e
+ PROFILE=all
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle.jar) ...
### Building graph browser (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_graphbrowser.jar) ...
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_admin.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
+ bin/isabelle ocaml_setup
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
       opam update

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

=== CONFIGURATION ===

ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-15c840d48c9a/x86_64_32-linux"
ML_SYSTEM="polyml-5.9"
ML_OPTIONS="-H 4000 --maxheap 8G"
jobs = 8, threads = 8, numa = true

=== BUILD ===

Build started at Tue, 27 Sep 2022 19:09:28 +0200
Isabelle id 8655344f1cf6
AFP id d81cfd823ae9

=== LOG ===

Session Pure/Pure
Session Misc/CTT
Session Misc/Cube
Session FOL/FOL
Session FOL/CCL
Session FOL/FOL-ex
Session FOL/FOLP
Session FOL/FOLP-ex
Session Doc/Intro (doc)
Session FOL/LCF
Session Doc/Logics (doc)
Session Doc/Nitpick (doc)
Session Pure/Pure-Examples
Session Pure/Pure-ex
Session Misc/SML
Session Misc/Sequents
Session Doc/Sledgehammer (doc)
Session AFP/SpecCheck (AFP)
Session Misc/Tools
Session HOL/HOL (main)
Session AFP/AVL-Trees (AFP)
Session AFP/AWN (AFP)
Session AFP/Abortable_Linearizable_Modules (AFP)
Session AFP/Abstract-Hoare-Logics (AFP)
Session AFP/Ackermanns_not_PR (AFP)
Session AFP/AnselmGod (AFP)
Session AFP/Aristotles_Assertoric_Syllogistic (AFP)
Session AFP/Attack_Trees (AFP)
Session AFP/AxiomaticCategoryTheory (AFP)
Session AFP/Belief_Revision (AFP)
Session AFP/BinarySearchTree (AFP)
Session AFP/Binomial-Queues (AFP)
Session AFP/Bondy (AFP)
Session AFP/Boolos_Curious_Inference (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/C2KA_DistributedSystems (AFP)
Session AFP/CISC-Kernel (AFP)
Session AFP/CYK (AFP)
Session AFP/Cauchy (AFP)
Session AFP/Sqrt_Babylonian (AFP)
Session Doc/Classes (doc)
Session AFP/ClockSynchInst (AFP)
Session AFP/Compiling-Exceptions-Correctly (AFP)
Session AFP/Complete_Non_Orders (AFP)
Session AFP/ComponentDependencies (AFP)
Session AFP/Concurrent_Revisions (AFP)
Session AFP/Constructor_Funs (AFP)
Session AFP/CryptoBasedCompositionalProperties (AFP)
Session AFP/DPT-SAT-Solver (AFP)
Session AFP/Dedekind_Real (AFP)
Session AFP/Depth-First-Search (AFP)
Session AFP/Digit_Expansions (AFP)
Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
Session AFP/DiskPaxos (AFP)
Session AFP/Example-Submission (AFP)
Session AFP/FFT (AFP)
Session AFP/FLP (AFP)
Session AFP/FeatherweightJava (AFP)
Session AFP/Featherweight_OCL (AFP)
Session AFP/FileRefinement (AFP)
Session AFP/FocusStreamsCaseStudies (AFP)
Session AFP/Foundation_of_geometry (AFP)
Session AFP/Free-Boolean-Algebra (AFP)
Session AFP/Fresh_Identifiers (AFP)
Session AFP/FunWithFunctions (AFP)
Session AFP/FunWithTilings (AFP)
Session Doc/Functions (doc)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/GenClock (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/Generic_Deriving (AFP)
Session AFP/GewirthPGCProof (AFP)
Session AFP/GoedelGod (AFP)
Session AFP/Goodstein_Lambda (AFP)
Session HOL/HOL-Cardinals (timing)
Session AFP/Binding_Syntax_Theory (AFP)
Session AFP/Ordinals_and_Cardinals (AFP)
Session AFP/Risk_Free_Lending (AFP)
Session HOL/HOL-Hoare
Session HOL/HOL-Hoare_Parallel (timing)
Session HOL/HOL-IMPP
Session HOL/HOL-IOA
Session HOL/HOL-Import
Session HOL/HOL-Lattice
Session HOL/HOL-Library (main timing)
Session AFP/ADS_Functor (AFP)
Session AFP/Approximation_Algorithms (AFP)
Session AFP/ArrowImpossibilityGS (AFP)
Session AFP/Auto2_HOL (AFP)
Session AFP/BNF_CC (AFP)
Session AFP/BNF_Operations (AFP)
Session AFP/Binomial-Heaps (AFP)
Session AFP/Boolean_Expression_Checkers (AFP)
Session AFP/Bounded_Deducibility_Security (AFP)
Session AFP/BD_Security_Compositional (AFP)
Session AFP/CoSMeDis (AFP)
Session AFP/CoCon (AFP)
Session AFP/CoSMed (AFP)
Session AFP/Buildings (AFP)
Session AFP/CRDT (AFP)
Session AFP/IMAP-CRDT (AFP)
Session AFP/Card_Multisets (AFP)
Session AFP/Card_Number_Partitions (AFP)
Session AFP/Category (AFP)
Session Doc/Codegen (doc)
Session AFP/CofGroups (AFP)
Session AFP/Completeness (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/Concurrent_Ref_Alg (AFP)
Session AFP/Conditional_Simplification (AFP)
Session AFP/Conditional_Transfer_Rule (AFP)
Session AFP/CoreC++ (AFP)
Session AFP/Core_DOM (AFP)
Session AFP/Shadow_DOM (AFP)
Session AFP/DOM_Components (AFP)
Session AFP/Core_SC_DOM (AFP)
Session AFP/Shadow_SC_DOM (AFP)
Session AFP/SC_DOM_Components (AFP)
Session Doc/Datatypes (doc)
Session Doc/Corec (doc)
Session AFP/Decl_Sem_Fun_PL (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Epistemic_Logic (AFP)
Session AFP/Public_Announcement_Logic (AFP)
Session AFP/Stalnaker_Logic (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/FOL-Fitting (AFP)
Session AFP/FOL_Seq_Calc1 (AFP)
Session AFP/FOL_Axiomatic (AFP)
Session AFP/FOL_Harrison (AFP)
Session AFP/Factored_Transition_System_Bounding (AFP)
Session AFP/FinFun (AFP)
Session AFP/Extended_Finite_State_Machines (AFP)
Session AFP/Extended_Finite_State_Machine_Inference (AFP)
Session AFP/Finger-Trees (AFP)
Session AFP/Finite-Map-Extras (AFP)
Session AFP/Generalized_Counting_Sort (AFP)
Session AFP/Graph_Saturation (AFP)
Session AFP/Group-Ring-Module (AFP)
Session AFP/Valuation (AFP)
Session HOL/HOL-Auth (timing)
Session HOL/HOL-UNITY (timing)
Session HOL/HOL-Bali (timing)
Session HOL/HOL-Combinatorics (main timing)
Session AFP/Blue_Eyes (AFP)
Session AFP/Derangements (AFP)
Session AFP/Discrete_Summation (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/Graph_Theory (AFP)
Session AFP/ShortestPath (AFP)
Session HOL/HOL-Computational_Algebra (main timing)
Session AFP/Descartes_Sign_Rule (AFP)
Session HOL/HOL-Algebra (main timing)
Session AFP/Finitely_Generated_Abelian_Groups (AFP)
Session HOL/HOL-Decision_Procs (timing)
Session HOL/HOL-Quotient_Examples (timing)
Session AFP/Interpolation_Polynomials_HOL_Algebra (AFP)
Session AFP/Localization_Ring (AFP)
Session AFP/Orbit_Stabiliser (AFP)
Session AFP/Perfect-Number-Thm (AFP)
Session AFP/Secondary_Sylow (AFP)
Session AFP/Jordan_Hoelder (AFP)
Session AFP/VectorSpace (AFP)
Session HOL/HOL-Analysis (main timing)
Session AFP/Actuarial_Mathematics (AFP)
Session AFP/Cayley_Hamilton (AFP)
Session AFP/Coinductive (AFP)
Session AFP/DynamicArchitectures (AFP)
Session AFP/Architectural_Design_Patterns (AFP)
Session AFP/Lazy-Lists-II (AFP)
Session AFP/Stream_Fusion_Code (AFP)
Session AFP/Topology (AFP)
Session AFP/Complex_Geometry (AFP)
Session AFP/Poincare_Disc (AFP)
Session AFP/Differential_Game_Logic (AFP)
Session AFP/First_Welfare_Theorem (AFP)
Session AFP/Green (AFP)
Session HOL/HOL-Analysis-ex
Session HOL/HOL-Complex_Analysis (main timing)
Session AFP/Cartan_FP (AFP)
Session HOL/HOL-Eisbach
Session AFP/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/Case_Labeling (AFP)
Session AFP/Clean (AFP)
Session AFP/Combinatorics_Words (AFP)
Session AFP/Combinatorics_Words_Graph_Lemma (AFP)
Session AFP/Dependent_SIFUM_Type_Systems (AFP)
Session AFP/Dependent_SIFUM_Refinement (AFP)
Session Doc/Eisbach (doc)
Session HOL/HOL-Hahn_Banach
Session HOL/HOL-Homology (timing)
Session HOL/HOL-Probability (main timing)
Session AFP/Buffons_Needle (AFP)
Session AFP/Density_Compiler (AFP)
Session AFP/DiscretePricing (AFP)
Session AFP/Ergodic_Theory (AFP)
Session AFP/Gromov_Hyperbolicity (AFP)
Session AFP/Laws_of_Large_Numbers (AFP)
Session AFP/Fisher_Yates (AFP)
Session AFP/Girth_Chromatic (AFP)
Session AFP/Random_Graph_Subgraph_Threshold (AFP)
Session HOL/HOL-Probability-ex (timing)
Session AFP/Hahn_Jordan_Decomposition (AFP)
Session AFP/Lp (AFP)
Session AFP/MDP-Rewards (AFP)
Session AFP/Markov_Models (AFP)
Session AFP/Monad_Normalisation (AFP)
Session AFP/Monomorphic_Monad (AFP)
Session AFP/Neumann_Morgenstern_Utility (AFP)
Session AFP/Probabilistic_Noninterference (AFP)
Session AFP/Probabilistic_System_Zoo (AFP)
Session AFP/Quasi_Borel_Spaces (AFP)
Session AFP/Skip_Lists (AFP)
Session AFP/Source_Coding_Theorem (AFP)
Session AFP/Hyperdual (AFP)
Session AFP/Irrationality_J_Hancl (AFP)
Session AFP/Kuratowski_Closure_Complement (AFP)
Session AFP/Laplace_Transform (AFP)
Session AFP/Lower_Semicontinuous (AFP)
Session AFP/Minkowskis_Theorem (AFP)
Session AFP/Octonions (AFP)
Session AFP/Ptolemys_Theorem (AFP)
Session AFP/Quaternions (AFP)
Session AFP/Rank_Nullity_Theorem (AFP)
Session AFP/Gauss_Jordan (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/Hermite (AFP)
Session AFP/MDP-Algorithms (AFP)
Session AFP/Tarskis_Geometry (AFP)
Session AFP/Triangle (AFP)
Session AFP/Chord_Segments (AFP)
Session AFP/Stewart_Apollonius (AFP)
Session AFP/Youngs_Inequality (AFP)
Session AFP/pGCL (AFP)
Session HOL/HOL-Examples
Session HOL/HOL-Isar_Examples
Session HOL/HOL-Nonstandard_Analysis (timing)
Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
Session HOL/HOL-Number_Theory (main timing)
Session AFP/Arith_Prog_Rel_Primes (AFP)
Session AFP/Bernoulli (AFP)
Session AFP/E_Transcendental (AFP)
Session AFP/Elliptic_Curves_Group_Law (AFP)
Session AFP/Fermat3_4 (AFP)
Session HOL/HOL-Data_Structures (timing)
Session AFP/Efficient-Mergesort (AFP)
Session HOL/HOL-Codegenerator_Test
Session HOL/HOL-ex (timing)
Session AFP/Automatic_Refinement (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Lehmer (AFP)
Session AFP/Lifting_the_Exponent (AFP)
Session AFP/Padic_Ints (AFP)
Session AFP/Padic_Field (AFP)
Session AFP/Pratt_Certificate (AFP)
Session AFP/Bertrands_Postulate (AFP)
Session AFP/Prime_Harmonic_Series (AFP)
Session AFP/RSAPSS (AFP)
Session AFP/SumSquares (AFP)
Session AFP/Liouville_Numbers (AFP)
Session AFP/Lucas_Theorem (AFP)
Session AFP/DPRM_Theorem (AFP)
Session AFP/Mason_Stothers (AFP)
Session AFP/Polynomial_Interpolation (AFP)
Session AFP/Formal_Puiseux_Series (AFP)
Session AFP/Probabilistic_Prime_Tests (AFP)
Session AFP/Rep_Fin_Groups (AFP)
Session AFP/Sturm_Sequences (AFP)
Session AFP/Safe_Distance (AFP)
Session AFP/Special_Function_Bounds (AFP)
Session AFP/Sturm_Tarski (AFP)
Session AFP/Budan_Fourier (AFP)
Session AFP/Three_Circles (AFP)
Session AFP/Winding_Number_Eval (AFP)
Session AFP/Count_Complex_Roots (AFP)
Session HOL/HOL-Corec_Examples (timing)
Session HOL/HOL-Datatype_Examples (timing)
Session HOL/HOL-IMP (timing)
Session AFP/Abs_Int_ITP2012 (AFP)
Session AFP/Relational-Incorrectness-Logic (AFP)
Session HOL/HOL-Imperative_HOL (timing)
Session AFP/Auto2_Imperative_HOL (AFP)
Session AFP/Imperative_Insertion_Sort (AFP)
Session HOL/HOL-Induct
Session HOL/HOL-Metis_Examples (timing)
Session HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-ex
Session HOL/HOL-Proofs-Lambda (timing)
Session AFP/Applicative_Lifting (AFP)
Session AFP/Free-Groups (AFP)
Session AFP/Stern_Brocot (AFP)
Session AFP/HereditarilyFinite (AFP)
Session AFP/HyperCTL (AFP)
Session AFP/Integration (AFP)
Session AFP/Isabelle_Meta_Model (AFP)
Session AFP/LTL (AFP)
Session AFP/Stuttering_Equivalence (AFP)
Session AFP/Landau_Symbols (AFP)
Session AFP/Akra_Bazzi (AFP)
Session AFP/Catalan_Numbers (AFP)
Session AFP/Error_Function (AFP)
Session AFP/Euler_MacLaurin (AFP)
Session AFP/LightweightJava (AFP)
Session AFP/LinearQuantifierElim (AFP)
Session AFP/List-Infinite (AFP)
Session AFP/Nat-Interval-Logic (AFP)
Session AFP/AutoFocus-Stream (AFP)
Session AFP/Median_Method (AFP)
Session AFP/MuchAdoAboutTwo (AFP)
Session AFP/Optics (AFP)
Session AFP/UTP-Toolkit (AFP)
Session AFP/UTP (AFP)
Session AFP/Order_Lattice_Props (AFP)
Session AFP/POPLmark-deBruijn (AFP)
Session AFP/Pairing_Heap (AFP)
Session AFP/Password_Authentication_Protocol (AFP)
Session AFP/Pell (AFP)
Session AFP/Prefix_Free_Code_Combinators (AFP)
Session AFP/Presburger-Automata (AFP)
Session AFP/Priority_Queue_Braun (AFP)
Session AFP/Program-Conflict-Analysis (AFP)
Session AFP/Regular-Sets (AFP)
Session AFP/Abstract-Rewriting (AFP)
Session AFP/Decreasing-Diagrams (AFP)
Session AFP/First_Order_Terms (AFP)
Session AFP/Stateful_Protocol_Composition_and_Typing (AFP)
Session AFP/Automated_Stateful_Protocol_Verification (AFP)
Session AFP/Matrix (AFP)
Session AFP/Matrix_Tensor (AFP)
Session AFP/Knot_Theory (AFP)
Session AFP/Coinductive_Languages (AFP)
Session AFP/Finite_Automata_HF (AFP)
Session AFP/Functional-Automata (AFP)
Session AFP/Posix-Lexing (AFP)
Session AFP/ResiduatedTransitionSystem (AFP)
Session AFP/Ribbon_Proofs (AFP)
Session AFP/SATSolverVerification (AFP)
Session AFP/Safe_OCL (AFP)
Session AFP/Schutz_Spacetime (AFP)
Session AFP/Selection_Heap_Sort (AFP)
Session AFP/Simplex (AFP)
Session AFP/Skew_Heap (AFP)
Session AFP/Solidity (AFP)
Session AFP/Sort_Encodings (AFP)
Session AFP/Splay_Tree (AFP)
Session AFP/Amortized_Complexity (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Root_Balanced_Tree (AFP)
Session AFP/Closest_Pair_Points (AFP)
Session AFP/Stable_Matching (AFP)
Session AFP/SuperCalc (AFP)
Session Doc/System (doc)
Session AFP/Szemeredi_Regularity (AFP)
Session AFP/Roth_Arithmetic_Progressions (AFP)
Session AFP/Tail_Recursive_Functions (AFP)
Session AFP/TortoiseHare (AFP)
Session AFP/Trie (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Twelvefold_Way (AFP)
Session AFP/Vickrey_Clarke_Groves (AFP)
Session HOL/HOL-Matrix_LP
Session HOL/HOL-MicroJava (timing)
Session HOL/HOL-Mirabelle-ex
Session HOL/HOL-Mutabelle
Session HOL/HOL-NanoJava
Session HOL/HOL-Nitpick_Examples
Session HOL/HOL-Nominal
Session AFP/CCS (AFP)
Session HOL/HOL-Nominal-Examples (timing)
Session AFP/Lam-ml-Normalization (AFP)
Session AFP/Pi_Calculus (AFP)
Session AFP/Psi_Calculi (AFP)
Session AFP/SequentInvertibility (AFP)
Session HOL/HOL-Predicate_Compile_Examples (timing)
Session HOL/HOL-Prolog
Session HOL/HOL-Quickcheck_Examples (timing)
Session HOL/HOL-Real_Asymp
Session AFP/Cotangent_PFD_Formula (AFP)
Session AFP/Fourier (AFP)
Session AFP/Furstenberg_Topology (AFP)
Session HOL/HOL-Real_Asymp-Manual
Session AFP/Sophomores_Dream (AFP)
Session AFP/Stirling_Formula (AFP)
Session AFP/Irrationals_From_THEBOOK (AFP)
Session AFP/Lambert_W (AFP)
Session HOL/HOL-SET_Protocol (timing)
Session HOL/HOL-SMT_Examples (timing)
Session HOL/HOL-SPARK
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session HOL/HOL-SPARK-Manual
Session HOL/HOL-Statespace
Session HOL/HOL-TLA
Session HOL/HOL-TLA-Buffer
Session HOL/HOL-TLA-Inc
Session HOL/HOL-TLA-Memory
Session HOL/HOL-TPTP
Session HOL/HOL-Types_To_Sets
Session AFP/Banach_Steinhaus (AFP)
Session AFP/Smooth_Manifolds (AFP)
Session AFP/Types_To_Sets_Extension (AFP)
Session HOL/HOL-Unix
Session HOL/HOL-ZF
Session AFP/Category2 (AFP)
Session HOL/HOLCF (main timing)
Session AFP/Circus (AFP)
Session AFP/HOL-CSP (AFP)
Session HOL/HOLCF-IMP
Session HOL/HOLCF-Library
Session AFP/CSP_RefTK (AFP)
Session HOL/HOLCF-FOCUS
Session HOL/HOLCF-ex
Session AFP/PCF (AFP)
Session AFP/HOLCF-Prelude (AFP)
Session AFP/BirdKMP (AFP)
Session HOL/HOLCF-Tutorial
Session HOL/IOA (timing)
Session HOL/IOA-ABP
Session HOL/IOA-NTP
Session HOL/IOA-Storage
Session HOL/IOA-ex
Session AFP/Shivers-CFA (AFP)
Session AFP/Stream-Fusion (AFP)
Session AFP/Tycon (AFP)
Session AFP/WorkerWrapper (AFP)
Session AFP/Hales_Jewett (AFP)
Session Misc/Haskell
Session AFP/Heard_Of (AFP)
Session AFP/Consensus_Refined (AFP)
Session AFP/Hello_World (AFP)
Session AFP/Hood_Melville_Queue (AFP)
Session AFP/HotelKeyCards (AFP)
Session Doc/How_to_Prove_it (no_doc)
Session AFP/Huffman (AFP)
Session AFP/Hybrid_Logic (AFP)
Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
Session AFP/IFC_Tracking (AFP)
Session AFP/IMP2 (AFP)
Session AFP/IMP2_Binary_Heap (AFP)
Session AFP/IMP_Compiler (AFP)
Session AFP/IMP_Compiler_Reuse (AFP)
Session Doc/Implementation (doc)
Session AFP/Implicational_Logic (AFP)
Session AFP/Impossible_Geometry (AFP)
Session AFP/Inductive_Confidentiality (AFP)
Session AFP/Inductive_Inference (AFP)
Session AFP/InfPathElimination (AFP)
Session AFP/Intro_Dest_Elim (AFP)
Session AFP/Involutions2Squares (AFP)
Session AFP/IsaGeoCoq (AFP)
Session AFP/IsaNet (AFP)
Session Doc/Isar_Ref (doc)
Session AFP/Isabelle_C (AFP)
Session Doc/JEdit (doc)
Session AFP/Jacobson_Basic_Algebra (AFP)
Session AFP/Grothendieck_Schemes (AFP)
Session AFP/Pluennecke_Ruzsa_Inequality (AFP)
Session AFP/Khovanskii_Theorem (AFP)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/Key_Agreement_Strong_Adversaries (AFP)
Session AFP/Kleene_Algebra (AFP)
Session AFP/KAD (AFP)
Session AFP/KAT_and_DRA (AFP)
Session AFP/Algebraic_VCs (AFP)
Session AFP/Multirelations (AFP)
Session AFP/Quantales (AFP)
Session AFP/Transformer_Semantics (AFP)
Session AFP/Regular_Algebras (AFP)
Session AFP/Relation_Algebra (AFP)
Session AFP/Relational_Paths (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/Knights_Tour (AFP)
Session AFP/LambdaMu (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Lazy_Case (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/List-Index (AFP)
Session AFP/Comparison_Sort_Lower_Bound (AFP)
Session AFP/Jinja (AFP)
Session AFP/Dominance_CHK (AFP)
Session AFP/HRB-Slicing (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/Slicing (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/JinjaDCI (AFP)
Session AFP/Regression_Test_Selection (AFP)
Session AFP/List_Update (AFP)
Session AFP/Quick_Sort_Cost (AFP)
Session AFP/Random_BSTs (AFP)
Session AFP/Randomised_BSTs (AFP)
Session AFP/Treaps (AFP)
Session AFP/Randomised_Social_Choice (AFP)
Session AFP/Fishburn_Impossibility (AFP)
Session AFP/SDS_Impossibility (AFP)
Session AFP/List_Interleaving (AFP)
Session AFP/List_Inversions (AFP)
Session AFP/LocalLexing (AFP)
Session Doc/Locales (doc)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Logging_Independent_Anonymity (AFP)
Session AFP/Lowe_Ontological_Argument (AFP)
Session Doc/Main (doc)
Session AFP/Marriage (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Matroids (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Median_Of_Medians_Selection (AFP)
Session AFP/KD_Tree (AFP)
Session AFP/Menger (AFP)
Session AFP/Mereology (AFP)
Session AFP/Metalogic_ProofChecker (AFP)
Session AFP/MiniML (AFP)
Session AFP/Modular_Assembly_Kit_Security (AFP)
Session AFP/MonoBoolTranAlgebra (AFP)
Session AFP/Name_Carrying_Type_Inference (AFP)
Session AFP/Nano_JSON (AFP)
Session AFP/Nash_Williams (AFP)
Session AFP/No_FTL_observers (AFP)
Session AFP/Nominal2 (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Surprise_Paradox (AFP)
Session AFP/LambdaAuth (AFP)
Session AFP/Launchbury (AFP)
Session AFP/Call_Arity (AFP)
Session AFP/Modal_Logics_for_NTS (AFP)
Session AFP/Rewriting_Z (AFP)
Session AFP/Noninterference_CSP (AFP)
Session AFP/Noninterference_Ipurge_Unwinding (AFP)
Session AFP/Noninterference_Generic_Unwinding (AFP)
Session AFP/Noninterference_Inductive_Unwinding (AFP)
Session AFP/Noninterference_Sequential_Composition (AFP)
Session AFP/Noninterference_Concurrent_Composition (AFP)
Session AFP/NormByEval (AFP)
Session AFP/OpSets (AFP)
Session AFP/Open_Induction (AFP)
Session AFP/Well_Quasi_Orders (AFP)
Session AFP/Decreasing-Diagrams-II (AFP)
Session AFP/Myhill-Nerode (AFP)
Session AFP/Ordinal (AFP)
Session AFP/Nested_Multisets_Ordinals (AFP)
Session AFP/Design_Theory (AFP)
Session AFP/Lambda_Free_RPOs (AFP)
Session AFP/Lambda_Free_EPO (AFP)
Session AFP/Ordered_Resolution_Prover (AFP)
Session AFP/Chandy_Lamport (AFP)
Session AFP/Saturation_Framework (AFP)
Session AFP/Saturation_Framework_Extensions (AFP)
Session AFP/Progress_Tracking (AFP)
Session AFP/PAL (AFP)
Session AFP/PLM (AFP)
Session AFP/PSemigroupsConvolution (AFP)
Session AFP/Package_logic (AFP)
Session AFP/Combinable_Wands (AFP)
Session AFP/Paraconsistency (AFP)
Session AFP/Parity_Game (AFP)
Session AFP/GaleStewart_Games (AFP)
Session AFP/Partial_Function_MR (AFP)
Session AFP/Physical_Quantities (AFP)
Session AFP/Pop_Refinement (AFP)
Session AFP/Possibilistic_Noninterference (AFP)
Session AFP/Priority_Search_Trees (AFP)
Session AFP/Prim_Dijkstra_Simple (AFP)
Session Doc/Prog_Prove (doc)
Session AFP/Projective_Geometry (AFP)
Session AFP/Proof_Strategy_Language (AFP)
Session AFP/PropResPI (AFP)
Session AFP/Propositional_Proof_Systems (AFP)
Session AFP/PseudoHoops (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Real_Power (AFP)
Session AFP/Real_Time_Deque (AFP)
Session AFP/Recursion-Theory-I (AFP)
Session AFP/Minsky_Machines (AFP)
Session AFP/RefinementReactive (AFP)
Session AFP/Regex_Equivalence (AFP)
Session AFP/Relational_Method (AFP)
Session AFP/Resolution_FOL (AFP)
Session AFP/Robbins-Conjecture (AFP)
Session AFP/Roy_Floyd_Warshall (AFP)
Session AFP/SCC_Bloemen_Sequential (AFP)
Session AFP/SIFPL (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Hoare_Time (AFP)
Session AFP/Separata (AFP)
Session AFP/Separation_Logic_Unbounded (AFP)
Session AFP/Simpl (AFP)
Session AFP/BDD (AFP)
Session AFP/SimplifiedOntologicalArgument (AFP)
Session AFP/Sliding_Window_Algorithm (AFP)
Session AFP/Statecharts (AFP)
Session AFP/Stellar_Quorums (AFP)
Session AFP/Stone_Algebras (AFP)
Session AFP/Stone_Relation_Algebras (AFP)
Session AFP/Stone_Kleene_Relation_Algebras (AFP)
Session AFP/Aggregation_Algebras (AFP)
Session AFP/Relational_Disjoint_Set_Forests (AFP)
Session AFP/Relational_Minimum_Spanning_Trees (AFP)
Session AFP/Relational_Forests (AFP)
Session AFP/Subset_Boolean_Algebras (AFP)
Session AFP/Correctness_Algebras (AFP)
Session AFP/Store_Buffer_Reduction (AFP)
Session AFP/Strong_Security (AFP)
Session Doc/Sugar (doc)
Session AFP/Sunflowers (AFP)
Session AFP/Clique_and_Monotone_Circuits (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/Szpilrajn (AFP)
Session AFP/Combinatorics_Words_Lyndon (AFP)
Session AFP/TESL_Language (AFP)
Session AFP/TLA (AFP)
Session AFP/Timed_Automata (AFP)
Session AFP/Probabilistic_Timed_Automata (AFP)
Session AFP/Topological_Semantics (AFP)
Session AFP/Transitive-Closure-II (AFP)
Session AFP/Tree_Decomposition (AFP)
Session Doc/Tutorial (doc)
Session Doc/Typeclass_Hierarchy (doc)
Session AFP/Types_Tableaus_and_Goedels_God (AFP)
Session AFP/UPF (AFP)
Session AFP/UPF_Firewall (AFP)
Session AFP/Universal_Turing_Machine (AFP)
Session AFP/Van_der_Waerden (AFP)
Session AFP/VeriComp (AFP)
Session AFP/Interpreter_Optimizations (AFP)
Session AFP/Verified-Prover (AFP)
Session AFP/VolpanoSmith (AFP)
Session AFP/WHATandWHERE_Security (AFP)
Session AFP/Weight_Balanced_Trees (AFP)
Session AFP/Weighted_Arithmetic_Geometric_Mean (AFP)
Session AFP/Word_Lib (AFP)
Session AFP/Complx (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Routing (AFP)
Session AFP/Interval_Arithmetic_Word32 (AFP)
Session AFP/LEM (AFP)
Session AFP/Native_Word (AFP)
Session AFP/Collections (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Abstract_Soundness (AFP)
Session AFP/FOL_Seq_Calc3 (AFP)
Session AFP/Incredible_Proof_Machine (AFP)
Session AFP/Deriving (AFP)
Session AFP/CAVA_Base (AFP)
Session AFP/CAVA_Automata (AFP)
Session AFP/DFS_Framework (AFP)
Session AFP/Gabow_SCC (AFP)
Session AFP/LTL_to_GBA (AFP)
Session AFP/Promela (AFP)
Session AFP/Containers (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/Eval_FO (AFP)
Session AFP/MFOTL_Monitor (AFP)
Session AFP/Generic_Join (AFP)
Session AFP/MFODL_Monitor_Optimized (AFP)
Session AFP/VYDRA_MDL (AFP)
Session AFP/Formula_Derivatives (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session AFP/Show (AFP)
Session AFP/Affine_Arithmetic (AFP)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/Differential_Dynamic_Logic (AFP)
Session AFP/Hybrid_Systems_VCs (AFP)
Session AFP/Matrices_for_ODEs (AFP)
Session AFP/Taylor_Models (AFP)
Session AFP/CakeML (AFP)
Session AFP/Certification_Monads (AFP)
Session AFP/AI_Planning_Languages_Semantics (AFP)
Session AFP/Verified_SAT_Based_AI_Planning (AFP)
Session AFP/Dict_Construction (AFP)
Session AFP/Formula_Derivatives-Examples (AFP)
Session AFP/Monad_Memo_DP (AFP)
Session AFP/Hidden_Markov_Models (AFP)
Session AFP/Optimal_BST (AFP)
Session AFP/Polynomial_Factorization (AFP)
Session AFP/Amicable_Numbers (AFP)
Session AFP/Dirichlet_Series (AFP)
Session AFP/Finite_Fields (AFP)
Session AFP/Universal_Hash_Families (AFP)
Session AFP/Frequency_Moments (AFP)
Session AFP/Zeta_Function (AFP)
Session AFP/Dirichlet_L (AFP)
Session AFP/Gauss_Sums (AFP)
Session AFP/Prime_Number_Theorem (AFP)
Session AFP/Prime_Distribution_Elementary (AFP)
Session AFP/IMO2019 (AFP)
Session AFP/Irrational_Series_Erdos_Straus (AFP)
Session AFP/Transcendence_Series_Hancl_Rucki (AFP)
Session AFP/Zeta_3_Irrational (AFP)
Session AFP/Gaussian_Integers (AFP)
Session AFP/Jordan_Normal_Form (AFP)
Session AFP/Farkas (AFP)
Session AFP/Isabelle_Marries_Dirac (AFP)
Session AFP/Knuth_Bendix_Order (AFP)
Session AFP/Functional_Ordered_Resolution_Prover (AFP)
Session AFP/Regular_Tree_Relations (AFP)
Session AFP/FO_Theory_Rewriting (AFP)
Session AFP/Rewrite_Properties_Reduction (AFP)
Session AFP/Weighted_Path_Order (AFP)
Session AFP/Multiset_Ordering_NPC (AFP)
Session AFP/Linear_Recurrences (AFP)
Session AFP/Perron_Frobenius (AFP)
Session AFP/Stochastic_Matrices (AFP)
Session AFP/Subresultants (AFP)
Session AFP/Berlekamp_Zassenhaus (AFP)
Session AFP/Algebraic_Numbers (AFP)
Session AFP/BenOr_Kozen_Reif (AFP)
Session AFP/LLL_Basis_Reduction (AFP)
Session AFP/LLL_Factorization (AFP)
Session AFP/Linear_Inequalities (AFP)
Session AFP/LP_Duality (AFP)
Session AFP/Linear_Programming (AFP)
Session AFP/Number_Theoretic_Transform (AFP)
Session AFP/CRYSTALS-Kyber (AFP)
Session AFP/Smith_Normal_Form (AFP)
Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP)
Session AFP/Polynomials (AFP)
Session AFP/Deep_Learning (AFP)
Session AFP/QHLProver (AFP)
Session AFP/Projective_Measurements (AFP)
Session AFP/Commuting_Hermitian (AFP)
Session AFP/Groebner_Bases (AFP)
Session AFP/Fishers_Inequality (AFP)
Session AFP/Groebner_Macaulay (AFP)
Session AFP/Nullstellensatz (AFP)
Session AFP/Signature_Groebner (AFP)
Session AFP/Lambda_Free_KBOs (AFP)
Session AFP/Symmetric_Polynomials (AFP)
Session AFP/Pi_Transcendental (AFP)
Session AFP/Power_Sum_Polynomials (AFP)
Session AFP/Hermite_Lindemann (AFP)
Session AFP/Factor_Algebraic_Polynomial (AFP)
Session AFP/Cubic_Quartic_Equations (AFP)
Session AFP/Linear_Recurrences_Solver (AFP)
Session AFP/Virtual_Substitution (AFP)
Session AFP/Real_Impl (AFP)
Session AFP/Complex_Bounded_Operators (AFP)
Session AFP/Registers (AFP)
Session AFP/QR_Decomposition (AFP)
Session AFP/XML (AFP)
Session AFP/Van_Emde_Boas_Trees (AFP)
Session AFP/Dijkstra_Shortest_Path (AFP)
Session AFP/Koenigsberg_Friendship (AFP)
Session AFP/FOL_Seq_Calc2 (AFP)
Session AFP/Formal_SSA (AFP)
Session AFP/Minimal_SSA (AFP)
Session AFP/Gale_Shapley (AFP)
Session AFP/HOL-ODE-Numerics (AFP)
Session AFP/HOL-ODE-ARCH-COMP (AFP)
Session AFP/HOL-ODE-Examples (AFP large)
Session AFP/Lorenz_Approximation (AFP)
Session AFP/Lorenz_C0 (AFP large)
Session AFP/Lorenz_C1 (AFP large)
Session AFP/Poincare_Bendixson (AFP)
Session AFP/Transition_Systems_and_Automata (AFP)
Session AFP/Adaptive_State_Counting (AFP)
Session AFP/Buchi_Complementation (AFP)
Session AFP/LTL_Master_Theorem (AFP)
Session AFP/LTL_Normal_Form (AFP)
Session AFP/Partial_Order_Reduction (AFP)
Session AFP/SM_Base (AFP)
Session AFP/SM (AFP)
Session AFP/CAVA_Setup (AFP)
Session AFP/CAVA_LTL_Modelchecker (AFP)
Session AFP/Transitive-Closure (AFP)
Session AFP/KBPs (AFP)
Session AFP/LTL_to_DRA (AFP)
Session AFP/Network_Security_Policy_Verification (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Tree-Automata (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Higher_Order_Terms (AFP)
Session AFP/CakeML_Codegen (AFP)
Session AFP/Old_Datatype_Show (AFP)
Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
Session AFP/FSM_Tests (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/LOFT (AFP)
Session AFP/Mersenne_Primes (AFP)
Session AFP/MiniSail (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sepref_Prereq (AFP)
Session AFP/ROBDD (AFP)
Session AFP/Refine_Imperative_HOL (AFP)
Session AFP/BTree (AFP)
Session AFP/Floyd_Warshall (AFP)
Session AFP/Sepref_Basic (AFP)
Session AFP/Sepref_IICF (AFP)
Session AFP/Flow_Networks (AFP)
Session AFP/EdmondsKarp_Maxflow (AFP)
Session AFP/MFMC_Countable (AFP)
Session AFP/Probabilistic_While (AFP)
Session AFP/CryptHOL (AFP)
Session AFP/Constructive_Cryptography (AFP)
Session AFP/Game_Based_Crypto (AFP)
Session AFP/Multi_Party_Computation (AFP)
Session AFP/Sigma_Commit_Crypto (AFP)
Session AFP/Constructive_Cryptography_CM (AFP)
Session AFP/Prpu_Maxflow (AFP)
Session AFP/Knuth_Morris_Pratt (AFP)
Session AFP/Kruskal (AFP)
Session AFP/PAC_Checker (AFP)
Session AFP/VerifyThis2018 (AFP)
Session AFP/VerifyThis2019 (AFP)
Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/WebAssembly (AFP)
Session AFP/SPARCv8 (AFP)
Session AFP/X86_Semantics (AFP)
Session AFP/ZFC_in_HOL (AFP)
Session AFP/CZH_Foundations (AFP)
Session AFP/CZH_Elementary_Categories (AFP)
Session AFP/CZH_Universal_Constructions (AFP)
Session AFP/Category3 (AFP)
Session AFP/MonoidalCategory (AFP)
Session AFP/Ordinal_Partitions (AFP)
Session AFP/Wetzels_Problem (AFP)
Session FOL/ZF (main timing)
Session Doc/Logics_ZF (doc)
Session AFP/Recursion-Addition (AFP)
Session FOL/ZF-AC
Session FOL/ZF-Coind
Session FOL/ZF-Constructible
Session AFP/Delta_System_Lemma (AFP)
Session AFP/Transitive_Models (AFP)
Session AFP/Independence_CH (AFP)
Session AFP/Forcing (AFP)
Session FOL/ZF-IMP
Session FOL/ZF-Induct
Session FOL/ZF-UNITY (timing)
Session FOL/ZF-Resid
Session FOL/ZF-ex
Building ZF ...
Running Stalnaker_Logic ...
ZF: theory IFOL
ZF: theory FOL
Stalnaker_Logic: theory Stalnaker_Logic.Stalnaker_Logic
Stalnaker_Logic FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9_x86_64_32-linux/log/Stalnaker_Logic)
*** Inner syntax error (line 553 of "$AFP/Stalnaker_Logic/Stalnaker_Logic.thy")
*** at "⊢⇩S⇩4 p ⟹ ⊢⇩T⇩o⇩p p"
*** Failed to parse prop
*** At command "lemma" (line 553 of "$AFP/Stalnaker_Logic/Stalnaker_Logic.thy")
*** Type unification failed
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  semantics :: (??'a, ??'b) kripke ⇒ ??'b ⇒ ??'a fm ⇒ bool
*** Operand:   ?M :: 'd
*** 
*** At command "have" (line 481 of "$AFP/Stalnaker_Logic/Stalnaker_Logic.thy")
*** Failed to refine any pending goal
*** At command "by" (line 416 of "$AFP/Stalnaker_Logic/Stalnaker_Logic.thy")
*** Type unification failed
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  semantics :: (??'a, ??'b) kripke ⇒ ??'b ⇒ ??'a fm ⇒ bool
*** Operand:   ?M :: 'd
*** 
*** At command "have" (line 434 of "$AFP/Stalnaker_Logic/Stalnaker_Logic.thy")
*** Type unification failed
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  𝒲 :: (??'a, ??'b, ??'c) frame_scheme ⇒ ??'b set
*** Operand:   ?M :: 'b
*** 
*** At command "have" (line 122 of "$AFP/Stalnaker_Logic/Stalnaker_Logic.thy")
ZF: theory ZF.ZF_Base
ZF: theory ZF.upair
ZF: theory ZF.pair
ZF: theory ZF.Bool
ZF: theory ZF.equalities
ZF: theory ZF.Fixedpt
ZF: theory ZF.Sum
ZF: theory ZF.func
ZF: theory ZF.QPair
ZF: theory ZF.Perm
ZF: theory ZF.Trancl
ZF: theory ZF.WF
ZF: theory ZF.EquivClass
ZF: theory ZF.Order
ZF: theory ZF.Ordinal
ZF: theory ZF.OrdQuant
ZF: theory ZF.OrderArith
ZF: theory ZF.Nat
ZF: theory ZF.Epsilon
ZF: theory ZF.Inductive
ZF: theory ZF.OrderType
ZF: theory ZF.Finite
ZF: theory ZF.Cardinal
ZF: theory ZF.Univ
ZF: theory ZF.Arith
ZF: theory ZF.QUniv
ZF: theory ZF.Datatype
ZF: theory ZF.ArithSimp
ZF: theory ZF.Int
ZF: theory ZF.CardinalArith
ZF: theory ZF.List
ZF: theory ZF.Bin
ZF: theory ZF.IntDiv
ZF: theory ZF
ZF: theory ZF.AC
ZF: theory ZF.Zorn
ZF: theory ZF.Cardinal_AC
ZF: theory ZF.InfDatatype
ZF: theory ZFC
Preparing ZF/document ...
Finished ZF/document (0:00:14 elapsed time)
Preparing ZF/outline ...
Finished ZF/outline (0:00:09 elapsed time)
Timing ZF (8 threads, 13.582s elapsed time, 46.593s cpu time, 2.451s GC time, factor 3.43)
Finished ZF (0:00:20 elapsed time, 0:00:54 cpu time, factor 2.68)
Building ZF-Constructible ...
Building ZF-Induct ...
Running ZF-ex ...
Running ZF-AC ...
Running ZF-Resid ...
Running ZF-IMP ...
Running ZF-Coind ...
Running Recursion-Addition ...
ZF-Constructible: theory ZF-Constructible.Normal
ZF-Constructible: theory ZF-Constructible.Formula
ZF-Constructible: theory ZF-Constructible.MetaExists
ZF-Constructible: theory ZF-Constructible.Relative
ZF-Induct: theory ZF-Induct.Binary_Trees
ZF-Induct: theory ZF-Induct.Comb
ZF-Induct: theory ZF-Induct.Acc
ZF-Resid: theory ZF-Resid.Redex
ZF-Induct: theory ZF-Induct.Datatypes
ZF-Induct: theory ZF-Induct.FoldSet
ZF-Induct: theory ZF-Induct.ListN
ZF-Induct: theory ZF-Induct.Ntree
ZF-Induct: theory ZF-Induct.Mutil
Recursion-Addition: theory Recursion-Addition.recursion
ZF-IMP: theory ZF-IMP.Com
ZF-ex: theory ZF-ex.LList
ZF-ex: theory ZF-ex.BinEx
ZF-ex: theory ZF-ex.CoUnit
ZF-ex: theory ZF-ex.Group
ZF-ex: theory ZF-ex.Commutation
ZF-Coind: theory ZF-Coind.Map
ZF-ex: theory ZF-ex.Limit
ZF-Coind: theory ZF-Coind.Language
ZF-AC: theory ZF-AC.AC_Equiv
ZF-ex: theory ZF-ex.NatSum
ZF-ex: theory ZF-ex.Primes
ZF-Coind: theory ZF-Coind.Types
ZF-IMP: theory ZF-IMP.Denotation
ZF-Resid: theory ZF-Resid.Substitution
ZF-Coind: theory ZF-Coind.Values
ZF-ex: theory ZF-ex.Ramsey
ZF-Induct: theory ZF-Induct.Primrec
ZF-AC: theory ZF-AC.AC7_AC9
ZF-AC: theory ZF-AC.Cardinal_aux
ZF-AC: theory ZF-AC.AC18_AC19
ZF-AC: theory ZF-AC.WO1_AC
ZF-AC: theory ZF-AC.Hartog
ZF-AC: theory ZF-AC.WO1_WO7
ZF-IMP: theory ZF-IMP.Equiv
ZF-Induct: theory ZF-Induct.PropLog
ZF-Coind: theory ZF-Coind.Dynamic
ZF-Coind: theory ZF-Coind.Static
ZF-ex: theory ZF-ex.misc
Preparing ZF-IMP/document ...
ZF-Coind: theory ZF-Coind.ECR
ZF-Resid: theory ZF-Resid.Residuals
ZF-Induct: theory ZF-Induct.Rmap
Timing ZF-Coind (8 threads, 0.691s elapsed time, 1.714s cpu time, 0.000s GC time, factor 2.48)
Finished ZF-Coind (0:00:03 elapsed time)
Running Logics_ZF ...
ZF-Induct: theory ZF-Induct.Term
ZF-Resid: theory ZF-Resid.Reduction
ZF-AC: theory ZF-AC.HH
ZF-Induct: theory ZF-Induct.Tree_Forest
Logics_ZF: theory Logics_ZF.If
Logics_ZF: theory Logics_ZF.FOL_examples
Logics_ZF: theory Logics_ZF.ZF_Isar
Logics_ZF: theory Logics_ZF.IFOL_examples
Logics_ZF: theory Logics_ZF.ZF_examples
ZF-Resid: theory ZF-Resid.Confluence
ZF-Induct: theory ZF-Induct.Brouwer
Finished ZF-IMP/document (0:00:02 elapsed time)
Preparing ZF-IMP/outline ...
ZF-AC: theory ZF-AC.WO6_WO1
ZF-AC: theory ZF-AC.AC16_lemmas
ZF-AC: theory ZF-AC.DC
Timing ZF-Resid (8 threads, 1.231s elapsed time, 3.360s cpu time, 0.000s GC time, factor 2.73)
Finished ZF-Resid (0:00:04 elapsed time, 0:00:03 cpu time, factor 0.81)
Preparing Logics_ZF/logics-ZF ...
ZF-Constructible: theory ZF-Constructible.Reflection
ZF-AC: theory ZF-AC.AC15_WO6
ZF-AC: theory ZF-AC.AC17_AC1
Finished ZF-IMP/outline (0:00:02 elapsed time)
Timing ZF-IMP (8 threads, 1.117s elapsed time, 1.462s cpu time, 0.000s GC time, factor 1.31)
Finished ZF-IMP (0:00:02 elapsed time)
ZF-AC: theory ZF-AC.AC16_WO4
ZF-AC: theory ZF-AC.WO2_AC16
ZF-Induct: theory ZF-Induct.Multiset
Preparing Recursion-Addition/document ...
ZF-ex: theory ZF-ex.Ring
Finished Recursion-Addition/document (0:00:02 elapsed time)
Preparing Recursion-Addition/outline ...
Finished Recursion-Addition/outline (0:00:01 elapsed time)
ZF-Constructible: theory ZF-Constructible.L_axioms
ZF-Constructible: theory ZF-Constructible.Wellorderings
Timing ZF-ex (8 threads, 5.817s elapsed time, 20.313s cpu time, 0.739s GC time, factor 3.49)
Finished ZF-ex (0:00:12 elapsed time, 0:00:21 cpu time, factor 1.74)
Timing Recursion-Addition (8 threads, 0.527s elapsed time, 2.061s cpu time, 0.000s GC time, factor 3.91)
Finished Recursion-Addition (0:00:08 elapsed time)
Preparing ZF-Induct/document ...
ZF-Constructible: theory ZF-Constructible.WFrec
ZF-Constructible: theory ZF-Constructible.WF_absolute
Preparing ZF-AC/document ...
ZF-Constructible: theory ZF-Constructible.Datatype_absolute
ZF-Constructible: theory ZF-Constructible.Separation
ZF-Constructible: theory ZF-Constructible.Rank
ZF-Constructible: theory ZF-Constructible.AC_in_L
Latex error (line 129 of "HH.tex"):
  Undefined control sequence.
  <argument> Lemmas used in the proofs of AC1 \<
                                     Longrightarrow> WO2 and AC17 \<Longrightarro
  }
Latex error (line 129 of "HH.tex"):
  Undefined control sequence.
  <argument> ...proofs of AC1 \<Longrightarrow> WO2 and AC17 \<
                                                    Longrightarrow> AC1
  }
Latex error (line 129 of "HH.tex"):
  Undefined control sequence.
  <argument> ...csname }\fi Lemmas used in the proofs of AC1 \<
                                                    Longrightarrow> WO2 and AC...
  }
Latex error (line 129 of "HH.tex"):
  Undefined control sequence.
  <argument> ...proofs of AC1 \<Longrightarrow> WO2 and AC17 \<
                                                    Longrightarrow> AC1
  }
Latex error (line 129 of "HH.tex"):
  Undefined control sequence.
  <argument> ...csname }\fi Lemmas used in the proofs of AC1 \<
                                                    Longrightarrow> WO2 and AC...
  }
Latex error (line 129 of "HH.tex"):
  Undefined control sequence.
  <argument> ...proofs of AC1 \<Longrightarrow> WO2 and AC17 \<
                                                    Longrightarrow> AC1}{\thep...
  }
Latex error (line 216 of "HH.tex"):
  Undefined control sequence.
  <argument> The proof of AC1 \<
                     Longrightarrow> WO2
  }
Latex error (line 216 of "HH.tex"):
  Undefined control sequence.
  <argument> ...hesubsection\endcsname }\fi The proof of AC1 \<
                                                    Longrightarrow> WO2
  }
Latex error (line 216 of "HH.tex"):
  Undefined control sequence.
  <argument> ...hesubsection\endcsname }\fi The proof of AC1 \<
                                                    Longrightarrow> WO2}{\thep...
  }
Failed to build document "document"
ZF-AC FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9_x86_64_32-linux/log/ZF-AC)
***   Undefined control sequence.
***   <argument> ...proofs of AC1 \<Longrightarrow> WO2 and AC17 \<
***                                                     Longrightarrow> AC1
***   }
*** Latex error (line 129 of "HH.tex"):
***   Undefined control sequence.
***   <argument> ...csname }\fi Lemmas used in the proofs of AC1 \<
***                                                     Longrightarrow> WO2 and AC...
***   }
*** Latex error (line 129 of "HH.tex"):
***   Undefined control sequence.
***   <argument> ...proofs of AC1 \<Longrightarrow> WO2 and AC17 \<
***                                                     Longrightarrow> AC1
***   }
*** Latex error (line 129 of "HH.tex"):
***   Undefined control sequence.
***   <argument> ...csname }\fi Lemmas used in the proofs of AC1 \<
***                                                     Longrightarrow> WO2 and AC...
***   }
*** Latex error (line 129 of "HH.tex"):
***   Undefined control sequence.
***   <argument> ...proofs of AC1 \<Longrightarrow> WO2 and AC17 \<
***                                                     Longrightarrow> AC1}{\thep...
***   }
*** Latex error (line 216 of "HH.tex"):
***   Undefined control sequence.
***   <argument> The proof of AC1 \<
***                      Longrightarrow> WO2
***   }
*** Latex error (line 216 of "HH.tex"):
***   Undefined control sequence.
***   <argument> ...hesubsection\endcsname }\fi The proof of AC1 \<
***                                                     Longrightarrow> WO2
***   }
*** Latex error (line 216 of "HH.tex"):
***   Undefined control sequence.
***   <argument> ...hesubsection\endcsname }\fi The proof of AC1 \<
***                                                     Longrightarrow> WO2}{\thep...
***   }
*** Failed to build document "document"
ZF-Constructible: theory ZF-Constructible.Internalize
Finished Logics_ZF/logics-ZF (0:00:10 elapsed time)
Timing Logics_ZF (8 threads, 0.315s elapsed time, 0.706s cpu time, 0.000s GC time, factor 2.24)
Finished Logics_ZF (0:00:01 elapsed time)
ZF-Constructible: theory ZF-Constructible.Rec_Separation
ZF-Constructible: theory ZF-Constructible.Satisfies_absolute
ZF-Constructible: theory ZF-Constructible.Rank_Separation
ZF-Constructible: theory ZF-Constructible.DPow_absolute
Finished ZF-Induct/document (0:00:05 elapsed time)
Preparing ZF-Induct/outline ...
Preparing ZF-Constructible/document ...
Finished ZF-Induct/outline (0:00:04 elapsed time)
Timing ZF-Induct (8 threads, 2.825s elapsed time, 13.263s cpu time, 0.639s GC time, factor 4.69)
Finished ZF-Induct (0:00:12 elapsed time, 0:00:16 cpu time, factor 1.31)
Running ZF-UNITY ...
ZF-UNITY: theory ZF-UNITY.GenPrefix
ZF-UNITY: theory ZF-UNITY.MultisetSum
ZF-UNITY: theory ZF-UNITY.State
ZF-UNITY: theory ZF-UNITY.UNITY
ZF-UNITY: theory ZF-UNITY.Monotonicity
ZF-UNITY: theory ZF-UNITY.Constrains
ZF-UNITY: theory ZF-UNITY.FP
ZF-UNITY: theory ZF-UNITY.WFair
Latex error (line 16 of "DPow_absolute.tex"):
  Undefined control sequence.
     within 11 quantifiers\<
Latex error (line 456 of "AC_in_L.tex"):
  Undefined control sequence.
  <recently read> \<
    
        the Axiom of Choice hold in \isa{L}\<
Failed to build document "document"
ZF-Constructible FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9_x86_64_32-linux/log/ZF-Constructible)
Overfull \hbox (10.11699pt too wide) in paragraph at lines 691--692
[][]  \T1/lmr/bx/n/10 and \T1/lmtt/m/sl/10 wellfounded_on_imp_wf_on = M_wfrank.
wellfounded_on_imp_wf_on [OF
))
No file root.bbl.
[250] (./root.aux)
Package rerunfilecheck Warning: File `root.out' has changed.
(rerunfilecheck)                Rerun to get outlines right
(rerunfilecheck)                or use package `bookmark'.
LaTeX Warning: There were undefined references.
)
(see the transcript file for additional information)
 566 words of node memory still in use:
   3 hlist, 1 vlist, 1 rule, 2 glue, 3 kern, 1 glyph, 4 attribute, 80 glue_spec
, 4 attribute_list, 1 write nodes
   avail lists: 1:1,2:2308,3:66,4:15,5:490,6:51,7:2576,8:10,9:311,10:7,11:123
{/usr/share/texmf/fonts/enc/dvips/lm/lm-ec.enc}</usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmmi12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
sy10.pfb></usr/share/texmf/fonts/type1/public/lm/lmbx10.pfb></usr/share/texmf/f
onts/type1/public/lm/lmbx12.pfb></usr/share/texmf/fonts/type1/public/lm/lmr10.p
fb></usr/share/texmf/fonts/type1/public/lm/lmr12.pfb></usr/share/texmf/fonts/ty
pe1/public/lm/lmr17.pfb></usr/share/texmf/fonts/type1/public/lm/lmri10.pfb></us
r/share/texmf/fonts/type1/public/lm/lmtt10.pfb></usr/share/texmf/fonts/type1/pu
blic/lm/lmtto10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
symbols/msam10.pfb>
Output written on root.pdf (250 pages, 779927 bytes).
Transcript written on root.log.
*** Latex error (line 16 of "DPow_absolute.tex"):
***   Undefined control sequence.
***      within 11 quantifiers\<
*** Latex error (line 456 of "AC_in_L.tex"):
***   Undefined control sequence.
***   <recently read> \<
***     
***         the Axiom of Choice hold in \isa{L}\<
*** Failed to build document "document"
Delta_System_Lemma CANCELLED
Transitive_Models CANCELLED
Independence_CH CANCELLED
Forcing CANCELLED
ZF-UNITY: theory ZF-UNITY.Increasing
ZF-UNITY: theory ZF-UNITY.SubstAx
ZF-UNITY: theory ZF-UNITY.Follows
ZF-UNITY: theory ZF-UNITY.Mutex
ZF-UNITY: theory ZF-UNITY.Union
ZF-UNITY: theory ZF-UNITY.Comp
ZF-UNITY: theory ZF-UNITY.Guar
ZF-UNITY: theory ZF-UNITY.AllocBase
ZF-UNITY: theory ZF-UNITY.ClientImpl
ZF-UNITY: theory ZF-UNITY.Distributor
ZF-UNITY: theory ZF-UNITY.Merge
ZF-UNITY: theory ZF-UNITY.AllocImpl
Timing ZF-UNITY (8 threads, 4.729s elapsed time, 32.550s cpu time, 1.102s GC time, factor 6.88)
Finished ZF-UNITY (0:00:05 elapsed time, 0:00:33 cpu time, factor 5.74)
Presentation in "/media/data/jenkins/workspace/isabelle-all/browser_info"
Presenting ZF in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF" ...
Presenting ZF-Coind in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF-Coind" ...
Presenting Logics_ZF in "/media/data/jenkins/workspace/isabelle-all/browser_info/Doc/Logics_ZF" ...
Presenting ZF-Resid in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF-Resid" ...
Presenting ZF-UNITY in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF-UNITY" ...
Presenting ZF-Induct in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF-Induct" ...
Presenting ZF-ex in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF-ex" ...
Presenting Recursion-Addition in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Recursion-Addition" ...
Presenting ZF-IMP in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF-IMP" ...
Presenting document Recursion-Addition/document
Presenting document ZF-IMP/document
Presenting document Recursion-Addition/outline
Presenting document ZF-IMP/outline
Presenting document Logics_ZF/logics-ZF
Presenting document ZF-Induct/document
Presenting document ZF-Induct/outline
Presenting theory "ZF-Coind.Language"
Presenting theory "Logics_ZF.IFOL_examples"
Presenting document ZF/document
Presenting document ZF/outline
Presenting theory "Logics_ZF.FOL_examples"
Presenting theory "ZF-Induct.Datatypes"
Presenting theory "ZF-UNITY.State"
Presenting theory "ZF-Resid.Redex"
Presenting theory "ZF-Coind.Map"
Presenting theory "ZF-Coind.Values"
Presenting theory "ZF-IMP.Com"
Presenting theory "ZF-ex.misc"
Presenting theory "ZF-Coind.Types"
Presenting theory "ZF-Induct.Binary_Trees"
Presenting theory "Logics_ZF.ZF_examples"
Presenting theory "ZF-Coind.Static"
Presenting theory "ZF-Coind.Dynamic"
Presenting theory "ZF-Resid.Substitution"
Presenting theory "ZF-Coind.ECR"
Presenting theory "Logics_ZF.If"
Presenting theory "ZF-IMP.Denotation"
Presenting theory "ZF-Resid.Residuals"
Presenting theory "ZF-IMP.Equiv"
Presenting theory "ZF-UNITY.UNITY"
Presenting theory "ZF-Resid.Reduction"
Presenting theory "ZF-Resid.Confluence"
Presenting theory "ZF-Induct.Term"
Presenting theory "Logics_ZF.ZF_Isar"
Presenting theory "ZF-Induct.Ntree"
Presenting file "~~/src/Doc/antiquote_setup.ML"
Presenting theory "ZF-Induct.Tree_Forest"
Presenting theory "ZF-Induct.Brouwer"
Presenting theory "ZF-Induct.Mutil"
Presenting theory "ZF-UNITY.WFair"
Presenting theory "ZF-Induct.FoldSet"
Presenting theory "ZF-Induct.Acc"
Presenting theory "ZF-UNITY.Constrains"
Presenting theory "Recursion-Addition.recursion"
Presenting theory "ZF-ex.Group"
Presenting theory "ZF-UNITY.SubstAx"
Presenting theory "ZF-UNITY.Mutex"
Presenting theory "IFOL"
Presenting file "~~/src/Tools/misc_legacy.ML"
Presenting file "~~/src/Provers/splitter.ML"
Presenting theory "ZF-UNITY.FP"
Presenting theory "ZF-Induct.Multiset"
Presenting file "~~/src/Provers/hypsubst.ML"
Presenting file "~~/src/Tools/IsaPlanner/zipper.ML"
Presenting file "~~/src/Tools/IsaPlanner/isand.ML"
Presenting file "~~/src/Tools/IsaPlanner/rw_inst.ML"
Presenting file "~~/src/Provers/quantifier1.ML"
Presenting file "~~/src/Tools/intuitionistic.ML"
Presenting file "~~/src/Tools/project_rule.ML"
Presenting theory "ZF-ex.Ring"
Presenting file "~~/src/Tools/atomize_elim.ML"
Presenting file "~~/src/FOL/fologic.ML"
Presenting file "~~/src/FOL/intprover.ML"
Presenting theory "ZF-UNITY.Union"
Presenting theory "ZF-ex.Commutation"
Presenting theory "ZF-Induct.Rmap"
Presenting theory "ZF-ex.Primes"
Presenting theory "ZF-Induct.PropLog"
Presenting theory "ZF-UNITY.GenPrefix"
Presenting theory "ZF-Induct.ListN"
Presenting theory "ZF-ex.NatSum"
Presenting theory "ZF-Induct.Comb"
Presenting theory "ZF-UNITY.MultisetSum"
Presenting theory "ZF-ex.Ramsey"
Presenting theory "ZF-UNITY.Monotonicity"
Presenting theory "ZF-UNITY.Increasing"
Presenting theory "ZF-Induct.Primrec"
Presenting theory "ZF-UNITY.Comp"
Presenting theory "ZF-UNITY.Guar"
Presenting theory "ZF-UNITY.Follows"
Presenting theory "ZF-UNITY.AllocBase"
Presenting theory "ZF-UNITY.Distributor"
Presenting theory "ZF-ex.Limit"
Presenting theory "ZF-UNITY.Merge"
Presenting theory "ZF-UNITY.ClientImpl"
Presenting theory "ZF-ex.BinEx"
Presenting theory "ZF-UNITY.AllocImpl"
Presenting theory "ZF-ex.LList"
Presenting theory "ZF-ex.CoUnit"
Presenting theory "FOL"
Presenting file "~~/src/Provers/classical.ML"
Presenting file "~~/src/Provers/blast.ML"
Presenting file "~~/src/Provers/clasimp.ML"
Presenting file "~~/src/FOL/simpdata.ML"
Presenting file "~~/src/Tools/eqsubst.ML"
Presenting file "~~/src/Tools/induct.ML"
Presenting file "~~/src/Tools/case_product.ML"
Presenting theory "ZF.ZF_Base"
Presenting theory "ZF.upair"
Presenting file "~~/src/ZF/Tools/typechk.ML"
Presenting theory "ZF.pair"
Presenting file "~~/src/ZF/simpdata.ML"
Presenting theory "ZF.equalities"
Presenting theory "ZF.Fixedpt"
Presenting theory "ZF.Bool"
Presenting theory "ZF.Sum"
Presenting theory "ZF.func"
Presenting theory "ZF.QPair"
Presenting theory "ZF.Perm"
Presenting theory "ZF.Trancl"
Presenting theory "ZF.WF"
Presenting theory "ZF.Ordinal"
Presenting theory "ZF.OrdQuant"
Presenting theory "ZF.Nat"
Presenting theory "ZF.Inductive"
Presenting file "~~/src/ZF/ind_syntax.ML"
Presenting file "~~/src/ZF/Tools/ind_cases.ML"
Presenting file "~~/src/ZF/Tools/cartprod.ML"
Presenting file "~~/src/ZF/Tools/inductive_package.ML"
Presenting file "~~/src/ZF/Tools/induct_tacs.ML"
Presenting file "~~/src/ZF/Tools/primrec_package.ML"
Presenting theory "ZF.Epsilon"
Presenting theory "ZF.Order"
Presenting theory "ZF.OrderArith"
Presenting theory "ZF.OrderType"
Presenting theory "ZF.Finite"
Presenting theory "ZF.Cardinal"
Presenting theory "ZF.Univ"
Presenting theory "ZF.QUniv"
Presenting theory "ZF.Datatype"
Presenting file "~~/src/ZF/Tools/datatype_package.ML"
Presenting theory "ZF.Arith"
Presenting theory "ZF.ArithSimp"
Presenting file "~~/src/Provers/Arith/cancel_numerals.ML"
Presenting file "~~/src/Provers/Arith/combine_numerals.ML"
Presenting file "~~/src/ZF/arith_data.ML"
Presenting theory "ZF.List"
Presenting theory "ZF.EquivClass"
Presenting theory "ZF.Int"
Presenting theory "ZF.Bin"
Presenting file "~~/src/ZF/Tools/numeral_syntax.ML"
Presenting file "~~/src/ZF/int_arith.ML"
Presenting theory "ZF.IntDiv"
Presenting theory "ZF.CardinalArith"
Presenting theory "ZF"
Presenting theory "ZF.AC"
Presenting theory "ZF.Zorn"
Presenting theory "ZF.Cardinal_AC"
Presenting theory "ZF.InfDatatype"
Presenting theory "ZFC"
Unfinished session(s): Delta_System_Lemma, Forcing, Independence_CH, Stalnaker_Logic, Transitive_Models, ZF-AC, ZF-Constructible

=== TIMING ===

Group AFP: 0:00:11 elapsed time, 0:00:08 cpu time, factor 0.73
Group main: 0:00:20 elapsed time, 0:00:54 cpu time, factor 2.68
Group large: 0:00:00 elapsed time
Group no_doc: 0:00:00 elapsed time
Group doc: 0:00:01 elapsed time
Group timing: 0:00:25 elapsed time, 0:01:27 cpu time, factor 3.36
Overall: 0:02:39 elapsed time, 0:03:15 cpu time, factor 1.23

=== FAILED SESSIONS ===

Session Delta_System_Lemma: CANCELLED
Session ZF-Constructible: FAILED 1
Session Forcing: CANCELLED
Session ZF-AC: FAILED 1
Session Stalnaker_Logic: FAILED 1
Session Independence_CH: CANCELLED
Session Transitive_Models: CANCELLED

=== DEPENDENCIES ===

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

=== REPORT ===

Writing report file ...

=== SITEGEN ===

Writing status file ...
Running sitegen ...
using [/media/data/jenkins/workspace/isabelle-all/bin/isabelle]
Preparing site generation in out/hugo
Cleaning up generated files...
Preparing topics...
Preparing licenses...
Preparing releases...
Preparing authors...
Extracting keywords...
Preparing entries...
Preparing statistics...
Preparing project files
Preparing devel version...
Finished sitegen preparation.
Cleaning output dir...
Building site...
Build in /media/data/jenkins/workspace/isabelle-all/afp/web/index.html
Packing tars ...

=== NOTIFICATIONS ===


=== COMPLETED ===

Build step 'Execute shell' marked build as failure
Started calculate disk usage of build
Finished Calculation of disk usage of build in 0 seconds
Started calculate disk usage of workspace
Finished Calculation of disk usage of workspace in 0 seconds
No emails were triggered.
Finished: FAILURE