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
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 728f38b016c05fb8f525467ce9d403b194aafaa6 --template exists\n
exists
[isabelle-all] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(728f38b016c05fb8f525467ce9d403b194aafaa6)" --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
1429 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 "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(d81cfd823ae95fa189c898bf2ba24c81bc2a1637)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-all] $ /bin/sh -xe /tmp/jenkins9676481533623558812.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 Wed, 28 Sep 2022 12:27:26 +0200
Isabelle id cf8f85e2a807
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-Constructible ...
Building ZF-Induct ...
Running ZF-ex ...
ZF-Constructible: theory ZF-Constructible.Formula
ZF-Constructible: theory ZF-Constructible.Normal
ZF-Constructible: theory ZF-Constructible.MetaExists
ZF-Constructible: theory ZF-Constructible.Relative
Running ZF-AC ...
Running Stalnaker_Logic ...
ZF-Induct: theory ZF-Induct.Datatypes
ZF-Induct: theory ZF-Induct.Acc
ZF-Induct: theory ZF-Induct.Binary_Trees
ZF-Induct: theory ZF-Induct.Comb
ZF-Induct: theory ZF-Induct.ListN
ZF-Induct: theory ZF-Induct.FoldSet
ZF-Induct: theory ZF-Induct.Mutil
ZF-Induct: theory ZF-Induct.Ntree
ZF-ex: theory ZF-ex.LList
ZF-ex: theory ZF-ex.Commutation
ZF-ex: theory ZF-ex.CoUnit
ZF-ex: theory ZF-ex.BinEx
ZF-ex: theory ZF-ex.Group
ZF-ex: theory ZF-ex.Limit
ZF-ex: theory ZF-ex.NatSum
ZF-ex: theory ZF-ex.Primes
ZF-AC: theory ZF-AC.AC_Equiv
ZF-Induct: theory ZF-Induct.Primrec
ZF-ex: theory ZF-ex.Ramsey
ZF-ex: theory ZF-ex.misc
ZF-AC: theory ZF-AC.AC7_AC9
ZF-AC: theory ZF-AC.AC18_AC19
ZF-AC: theory ZF-AC.Hartog
ZF-AC: theory ZF-AC.WO1_AC
ZF-AC: theory ZF-AC.Cardinal_aux
ZF-AC: theory ZF-AC.WO1_WO7
ZF-Induct: theory ZF-Induct.PropLog
ZF-AC: theory ZF-AC.HH
ZF-Constructible: theory ZF-Constructible.Reflection
ZF-Induct: theory ZF-Induct.Rmap
ZF-AC: theory ZF-AC.WO6_WO1
ZF-AC: theory ZF-AC.AC16_lemmas
ZF-AC: theory ZF-AC.DC
ZF-Induct: theory ZF-Induct.Term
ZF-Induct: theory ZF-Induct.Tree_Forest
ZF-Induct: theory ZF-Induct.Brouwer
Stalnaker_Logic: theory Stalnaker_Logic.Stalnaker_Logic
ZF-AC: theory ZF-AC.AC15_WO6
ZF-AC: theory ZF-AC.AC16_WO4
ZF-AC: theory ZF-AC.AC17_AC1
ZF-AC: theory ZF-AC.WO2_AC16
ZF-Induct: theory ZF-Induct.Multiset
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")
*** 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-ex: theory ZF-ex.Ring
Preparing ZF-AC/document ...
ZF-Constructible: theory ZF-Constructible.L_axioms
ZF-Constructible: theory ZF-Constructible.Wellorderings
ZF-Constructible: theory ZF-Constructible.WFrec
ZF-Constructible: theory ZF-Constructible.WF_absolute
Timing ZF-ex (8 threads, 5.814s elapsed time, 19.879s cpu time, 0.685s GC time, factor 3.42)
Finished ZF-ex (0:00:11 elapsed time, 0:00:20 cpu time, factor 1.75)
ZF-Constructible: theory ZF-Constructible.Datatype_absolute
ZF-Constructible: theory ZF-Constructible.Rank
ZF-Constructible: theory ZF-Constructible.Separation
Preparing ZF-Induct/document ...
ZF-Constructible: theory ZF-Constructible.AC_in_L
ZF-Constructible: theory ZF-Constructible.Internalize
Finished ZF-AC/document (0:00:04 elapsed time)
Preparing ZF-AC/outline ...
ZF-Constructible: theory ZF-Constructible.Rec_Separation
ZF-Constructible: theory ZF-Constructible.Rank_Separation
ZF-Constructible: theory ZF-Constructible.Satisfies_absolute
ZF-Constructible: theory ZF-Constructible.DPow_absolute
Finished ZF-AC/outline (0:00:03 elapsed time)
Timing ZF-AC (8 threads, 2.116s elapsed time, 11.550s cpu time, 0.343s GC time, factor 5.46)
Finished ZF-AC (0:00:08 elapsed time, 0:00:12 cpu time, factor 1.38)
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.878s elapsed time, 13.521s cpu time, 0.648s GC time, factor 4.70)
Finished ZF-Induct (0:00:12 elapsed time, 0:00:17 cpu time, factor 1.34)
Running ZF-UNITY ...
ZF-UNITY: theory ZF-UNITY.State
ZF-UNITY: theory ZF-UNITY.MultisetSum
ZF-UNITY: theory ZF-UNITY.GenPrefix
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
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.824s elapsed time, 32.893s cpu time, 1.088s GC time, factor 6.82)
Finished ZF-UNITY (0:00:05 elapsed time, 0:00:33 cpu time, factor 5.94)
Finished ZF-Constructible/document (0:00:10 elapsed time)
Preparing ZF-Constructible/outline ...
Finished ZF-Constructible/outline (0:00:08 elapsed time)
Timing ZF-Constructible (8 threads, 8.432s elapsed time, 34.466s cpu time, 3.294s GC time, factor 4.09)
Finished ZF-Constructible (0:00:20 elapsed time, 0:00:43 cpu time, factor 2.14)
Building Delta_System_Lemma ...
Running Forcing ...
Forcing: theory Forcing.Utils
Delta_System_Lemma: theory Delta_System_Lemma.ZF_Library
Forcing: theory Forcing.Nat_Miscellanea
Forcing: theory Forcing.Recursion_Thms
Forcing: theory Forcing.Forcing_Notions
Forcing: theory Forcing.Synthetic_Definition
Forcing: theory Forcing.Internalizations
Forcing: theory Forcing.Pointed_DC
Forcing: theory Forcing.Relative_Univ
Forcing: theory Forcing.Renaming
Delta_System_Lemma: theory Delta_System_Lemma.Cofinality
Delta_System_Lemma: theory Delta_System_Lemma.Cardinal_Library
Forcing: theory Forcing.Rasiowa_Sikorski
Forcing: theory Forcing.Renaming_Auto
Delta_System_Lemma: theory Delta_System_Lemma.Delta_System
Delta_System_Lemma: theory Delta_System_Lemma.Cohen_Posets
Forcing: theory Forcing.Interface
Delta_System_Lemma: theory Delta_System_Lemma.Konig
Forcing: theory Forcing.Forcing_Data
Forcing: theory Forcing.Separation_Rename
Forcing: theory Forcing.Internal_ZFC_Axioms
Forcing: theory Forcing.Names
Forcing: theory Forcing.Extensionality_Axiom
Forcing: theory Forcing.Foundation_Axiom
Forcing: theory Forcing.FrecR
Forcing: theory Forcing.Least
Forcing: theory Forcing.Pairing_Axiom
Forcing: theory Forcing.Proper_Extension
Forcing: theory Forcing.Union_Axiom
Forcing: theory Forcing.Arities
Forcing: theory Forcing.Forces_Definition
Forcing: theory Forcing.Succession_Poset
Forcing: theory Forcing.Forcing_Theorems
Forcing: theory Forcing.Separation_Axiom
Forcing: theory Forcing.Infinity_Axiom
Forcing: theory Forcing.Powerset_Axiom
Forcing: theory Forcing.Ordinals_In_MG
Forcing: theory Forcing.Replacement_Axiom
Preparing Delta_System_Lemma/document ...
Forcing: theory Forcing.Choice_Axiom
Forcing: theory Forcing.Forcing_Main
Finished Delta_System_Lemma/document (0:00:05 elapsed time)
Preparing Delta_System_Lemma/outline ...
Finished Delta_System_Lemma/outline (0:00:03 elapsed time)
Timing Delta_System_Lemma (8 threads, 5.793s elapsed time, 29.521s cpu time, 0.611s GC time, factor 5.10)
Finished Delta_System_Lemma (0:00:08 elapsed time, 0:00:33 cpu time, factor 4.01)
Building Transitive_Models ...
Transitive_Models: theory Transitive_Models.Utils
Transitive_Models: theory Transitive_Models.Nat_Miscellanea
Transitive_Models: theory Transitive_Models.Eclose_Absolute
Transitive_Models: theory Transitive_Models.M_Basic_No_Repl
Transitive_Models: theory Transitive_Models.Synthetic_Definition
Transitive_Models: theory Transitive_Models.ZF_Miscellanea
Transitive_Models: theory Transitive_Models.Renaming
Preparing Forcing/document ...
Transitive_Models: theory Transitive_Models.Renaming_Auto
Transitive_Models: theory Transitive_Models.Datatype_absolute
Transitive_Models: theory Transitive_Models.Internalize
Transitive_Models: theory Transitive_Models.Recursion_Thms
Transitive_Models: theory Transitive_Models.Rec_Separation
Transitive_Models: theory Transitive_Models.Satisfies_absolute
Transitive_Models: theory Transitive_Models.DPow_absolute
Transitive_Models: theory Transitive_Models.Internalizations
Transitive_Models: theory Transitive_Models.Least
Transitive_Models: theory Transitive_Models.Higher_Order_Constructs
Transitive_Models: theory Transitive_Models.Relativization
Transitive_Models: theory Transitive_Models.Discipline_Base
Transitive_Models: theory Transitive_Models.Arities
Transitive_Models: theory Transitive_Models.Discipline_Function
Transitive_Models: theory Transitive_Models.Discipline_Cardinal
Transitive_Models: theory Transitive_Models.Univ_Relative
Transitive_Models: theory Transitive_Models.Lambda_Replacement
Transitive_Models: theory Transitive_Models.Cardinal_Relative
Transitive_Models: theory Transitive_Models.FiniteFun_Relative
Transitive_Models: theory Transitive_Models.CardinalArith_Relative
Transitive_Models: theory Transitive_Models.Aleph_Relative
Transitive_Models: theory Transitive_Models.Cardinal_AC_Relative
Transitive_Models: theory Transitive_Models.ZF_Library_Relative
Transitive_Models: theory Transitive_Models.Replacement_Lepoll
Finished Forcing/document (0:00:15 elapsed time)
Preparing Forcing/outline ...
Transitive_Models: theory Transitive_Models.Cardinal_Library_Relative
Transitive_Models: theory Transitive_Models.Delta_System_Relative
Transitive_Models: theory Transitive_Models.Partial_Functions_Relative
Transitive_Models: theory Transitive_Models.Pointed_DC_Relative
Finished Forcing/outline (0:00:08 elapsed time)
Timing Forcing (8 threads, 18.466s elapsed time, 101.623s cpu time, 2.475s GC time, factor 5.50)
Finished Forcing (0:00:19 elapsed time, 0:01:42 cpu time, factor 5.23)
Preparing Transitive_Models/document ...
Finished Transitive_Models/document (0:00:35 elapsed time)
Preparing Transitive_Models/outline ...
Finished Transitive_Models/outline (0:00:19 elapsed time)
Timing Transitive_Models (8 threads, 43.646s elapsed time, 189.824s cpu time, 6.431s GC time, factor 4.35)
Finished Transitive_Models (0:00:51 elapsed time, 0:03:25 cpu time, factor 4.01)
Running Independence_CH ...
Independence_CH: theory Independence_CH.Forcing_Notions
Independence_CH: theory Independence_CH.Edrel
Independence_CH: theory Independence_CH.FrecR
Independence_CH: theory Independence_CH.Cohen_Posets_Relative
Independence_CH: theory Independence_CH.FrecR_Arities
Independence_CH: theory Independence_CH.Fm_Definitions
Independence_CH: theory Independence_CH.Internal_ZFC_Axioms
Independence_CH: theory Independence_CH.Interface
Independence_CH: theory Independence_CH.Separation_Instances
Independence_CH: theory Independence_CH.Separation_Rename
Independence_CH: theory Independence_CH.Replacement_Instances
Independence_CH: theory Independence_CH.ZF_Trans_Interpretations
Independence_CH: theory Independence_CH.Forcing_Data
Independence_CH: theory Independence_CH.Forces_Definition
Independence_CH: theory Independence_CH.Names
Independence_CH: theory Independence_CH.Extensionality_Axiom
Independence_CH: theory Independence_CH.Forcing_Theorems
Independence_CH: theory Independence_CH.Foundation_Axiom
Independence_CH: theory Independence_CH.Pairing_Axiom
Independence_CH: theory Independence_CH.Proper_Extension
Independence_CH: theory Independence_CH.Union_Axiom
Independence_CH: theory Independence_CH.Infinity_Axiom
Independence_CH: theory Independence_CH.Succession_Poset
Independence_CH: theory Independence_CH.Ordinals_In_MG
Independence_CH: theory Independence_CH.Separation_Axiom
Independence_CH: theory Independence_CH.Replacement_Axiom
Independence_CH: theory Independence_CH.Powerset_Axiom
Independence_CH: theory Independence_CH.Choice_Axiom
Independence_CH: theory Independence_CH.Forcing_Main
Independence_CH: theory Independence_CH.Cardinal_Preservation
Independence_CH: theory Independence_CH.Not_CH
Independence_CH: theory Independence_CH.Kappa_Closed_Notions
Independence_CH: theory Independence_CH.CH
Independence_CH: theory Independence_CH.Absolute_Versions
Independence_CH: theory Independence_CH.Definitions_Main
Independence_CH: theory Independence_CH.Demonstrations
Preparing Independence_CH/document ...
Finished Independence_CH/document (0:00:27 elapsed time)
Preparing Independence_CH/outline ...
Finished Independence_CH/outline (0:00:13 elapsed time)
Timing Independence_CH (8 threads, 53.229s elapsed time, 278.201s cpu time, 8.849s GC time, factor 5.23)
Finished Independence_CH (0:00:54 elapsed time, 0:04:39 cpu time, factor 5.11)
Presentation in "/media/data/jenkins/workspace/isabelle-all/browser_info"
Presenting ZF-AC in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF-AC" ...
Presenting Transitive_Models in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Transitive_Models" ...
Presenting ZF-Constructible in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF-Constructible" ...
Presenting ZF-Induct in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF-Induct" ...
Presenting ZF-UNITY in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF-UNITY" ...
Presenting Forcing in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Forcing" ...
Presenting ZF-ex in "/media/data/jenkins/workspace/isabelle-all/browser_info/FOL/ZF-ex" ...
Presenting Delta_System_Lemma in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Delta_System_Lemma" ...
Presenting Independence_CH in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Independence_CH" ...
Presenting document Delta_System_Lemma/document
Presenting document ZF-Induct/document
Presenting document Delta_System_Lemma/outline
Presenting document ZF-Induct/outline
Presenting document ZF-AC/document
Presenting document ZF-AC/outline
Presenting document ZF-Constructible/document
Presenting document ZF-Constructible/outline
Presenting document Independence_CH/document
Presenting document Independence_CH/outline
Presenting theory "ZF-Induct.Datatypes"
Presenting theory "ZF-UNITY.State"
Presenting document Transitive_Models/document
Presenting document Forcing/document
Presenting document Forcing/outline
Presenting document Transitive_Models/outline
Presenting theory "ZF-ex.misc"
Presenting theory "ZF-AC.AC_Equiv"
Presenting theory "ZF-Induct.Binary_Trees"
Presenting theory "Forcing.Utils"
Presenting file "$AFP/Forcing/utils.ML"
Presenting theory "Transitive_Models.Utils"
Presenting file "$AFP/Transitive_Models/Utils.ml"
Presenting theory "ZF-Induct.Term"
Presenting theory "Independence_CH.Forcing_Notions"
Presenting theory "ZF-AC.Cardinal_aux"
Presenting theory "Transitive_Models.Nat_Miscellanea"
Presenting theory "ZF-Induct.Ntree"
Presenting theory "ZF-UNITY.UNITY"
Presenting theory "ZF-Induct.Tree_Forest"
Presenting theory "ZF-Constructible.Formula"
Presenting theory "ZF-Induct.Brouwer"
Presenting theory "Transitive_Models.ZF_Miscellanea"
Presenting theory "ZF-Induct.Mutil"
Presenting theory "ZF-AC.WO6_WO1"
Presenting theory "Delta_System_Lemma.ZF_Library"
Presenting theory "Forcing.Forcing_Notions"
Presenting theory "ZF-AC.WO1_WO7"
Presenting theory "ZF-Induct.FoldSet"
Presenting theory "ZF-UNITY.WFair"
Presenting theory "ZF-AC.AC7_AC9"
Presenting theory "ZF-Induct.Acc"
Presenting theory "ZF-AC.WO1_AC"
Presenting theory "Forcing.Pointed_DC"
Presenting theory "ZF-AC.Hartog"
Presenting theory "Independence_CH.Cohen_Posets_Relative"
Presenting theory "Forcing.Rasiowa_Sikorski"
Presenting theory "ZF-UNITY.Constrains"
Presenting theory "Transitive_Models.Renaming"
Presenting theory "ZF-AC.HH"
Presenting theory "Independence_CH.Edrel"
Presenting theory "ZF-UNITY.SubstAx"
Presenting theory "Forcing.Nat_Miscellanea"
Presenting theory "Forcing.Internalizations"
Presenting theory "Transitive_Models.Renaming_Auto"
Presenting file "$AFP/Transitive_Models/Renaming_ML.ml"
Presenting theory "ZF-ex.Group"
Presenting theory "ZF-Induct.Multiset"
Presenting theory "ZF-AC.AC15_WO6"
Presenting theory "ZF-UNITY.Mutex"
Presenting theory "Transitive_Models.M_Basic_No_Repl"
Presenting theory "ZF-Induct.Rmap"
Presenting theory "ZF-UNITY.FP"
Presenting theory "ZF-Constructible.Relative"
Presenting theory "Forcing.Recursion_Thms"
Presenting theory "ZF-Induct.PropLog"
Presenting theory "ZF-Induct.ListN"
Presenting theory "ZF-AC.AC16_lemmas"
Presenting theory "ZF-Constructible.Wellorderings"
Presenting theory "ZF-Induct.Comb"
Presenting theory "ZF-ex.Ring"
Presenting theory "ZF-ex.Commutation"
Presenting theory "ZF-UNITY.Union"
Presenting theory "Independence_CH.FrecR"
Presenting theory "Delta_System_Lemma.Cofinality"
Presenting theory "ZF-Constructible.WFrec"
Presenting theory "Transitive_Models.Eclose_Absolute"
Presenting theory "Independence_CH.FrecR_Arities"
Presenting theory "Forcing.Relative_Univ"
Presenting theory "ZF-Induct.Primrec"
Presenting theory "ZF-Constructible.WF_absolute"
Presenting theory "ZF-ex.Primes"
Presenting theory "ZF-AC.WO2_AC16"
Presenting theory "ZF-UNITY.GenPrefix"
Presenting theory "ZF-ex.NatSum"
Presenting theory "Delta_System_Lemma.Cardinal_Library"
Presenting theory "Forcing.Synthetic_Definition"
Presenting theory "ZF-UNITY.MultisetSum"
Presenting theory "Transitive_Models.Recursion_Thms"
Presenting theory "ZF-UNITY.Monotonicity"
Presenting theory "ZF-ex.Ramsey"
Presenting theory "Delta_System_Lemma.Konig"
Presenting theory "ZF-UNITY.Increasing"
Presenting theory "ZF-AC.AC16_WO4"
Presenting theory "ZF-Constructible.Datatype_absolute"
Presenting theory "Delta_System_Lemma.Delta_System"
Presenting theory "ZF-UNITY.Comp"
Presenting theory "ZF-Constructible.Normal"
Presenting theory "ZF-AC.AC17_AC1"
Presenting theory "ZF-UNITY.Guar"
Presenting theory "Delta_System_Lemma.Cohen_Posets"
Presenting theory "Transitive_Models.Datatype_absolute"
Presenting theory "ZF-AC.AC18_AC19"
Presenting theory "ZF-UNITY.Follows"
Presenting theory "ZF-Constructible.Reflection"
Presenting theory "ZF-Constructible.MetaExists"
Presenting theory "ZF-UNITY.AllocBase"
Presenting theory "ZF-UNITY.Distributor"
Presenting theory "ZF-UNITY.Merge"
Presenting theory "ZF-UNITY.ClientImpl"
Presenting theory "ZF-AC.DC"
Presenting theory "ZF-Constructible.L_axioms"
Presenting theory "ZF-UNITY.AllocImpl"
Presenting theory "ZF-Constructible.Separation"
Presenting theory "Forcing.Interface"
Presenting theory "ZF-ex.Limit"
Presenting theory "Independence_CH.Fm_Definitions"
Presenting theory "Forcing.Forcing_Data"
Presenting theory "ZF-Constructible.Internalize"
Presenting theory "ZF-ex.BinEx"
Presenting theory "Transitive_Models.Internalize"
Presenting theory "ZF-ex.LList"
Presenting theory "ZF-ex.CoUnit"
Presenting theory "Forcing.Internal_ZFC_Axioms"
Presenting theory "Independence_CH.Internal_ZFC_Axioms"
Presenting theory "ZF-Constructible.Rec_Separation"
Presenting theory "Transitive_Models.Rec_Separation"
Presenting theory "Forcing.Renaming"
Presenting theory "ZF-Constructible.Satisfies_absolute"
Presenting theory "Forcing.Renaming_Auto"
Presenting file "$AFP/Forcing/renaming.ML"
Presenting theory "ZF-Constructible.DPow_absolute"
Presenting theory "ZF-Constructible.AC_in_L"
Presenting theory "Transitive_Models.Satisfies_absolute"
Presenting theory "Forcing.Names"
Presenting theory "Independence_CH.Interface"
Presenting theory "ZF-Constructible.Rank"
Presenting theory "ZF-Constructible.Rank_Separation"
Presenting theory "Independence_CH.Separation_Instances"
Presenting theory "Transitive_Models.DPow_absolute"
Presenting theory "Forcing.FrecR"
Presenting theory "Forcing.Arities"
Presenting theory "Transitive_Models.Synthetic_Definition"
Presenting file "$AFP/Transitive_Models/Synthetic_Definition.ml"
Presenting theory "Transitive_Models.Internalizations"
Presenting theory "Transitive_Models.Least"
Presenting theory "Transitive_Models.Higher_Order_Constructs"
Presenting theory "Forcing.Forces_Definition"
Presenting theory "Independence_CH.Replacement_Instances"
Presenting theory "Independence_CH.ZF_Trans_Interpretations"
Presenting theory "Independence_CH.Forcing_Data"
Presenting theory "Transitive_Models.Relativization"
Presenting file "$AFP/Transitive_Models/Relativization_Database.ml"
Presenting file "$AFP/Transitive_Models/Relativization.ml"
Presenting theory "Forcing.Forcing_Theorems"
Presenting theory "Independence_CH.Forces_Definition"
Presenting theory "Transitive_Models.Discipline_Base"
Presenting theory "Forcing.Separation_Rename"
Presenting theory "Transitive_Models.Arities"
Presenting theory "Independence_CH.Names"
Presenting theory "Forcing.Separation_Axiom"
Presenting theory "Forcing.Pairing_Axiom"
Presenting theory "Forcing.Union_Axiom"
Presenting theory "Transitive_Models.Discipline_Function"
Presenting theory "Forcing.Powerset_Axiom"
Presenting theory "Forcing.Extensionality_Axiom"
Presenting theory "Forcing.Foundation_Axiom"
Presenting theory "Forcing.Least"
Presenting theory "Independence_CH.Forcing_Theorems"
Presenting theory "Forcing.Replacement_Axiom"
Presenting theory "Independence_CH.Ordinals_In_MG"
Presenting theory "Forcing.Infinity_Axiom"
Presenting theory "Forcing.Choice_Axiom"
Presenting theory "Independence_CH.Separation_Rename"
Presenting theory "Forcing.Ordinals_In_MG"
Presenting theory "Forcing.Proper_Extension"
Presenting theory "Forcing.Succession_Poset"
Presenting theory "Independence_CH.Separation_Axiom"
Presenting theory "Forcing.Forcing_Main"
Presenting theory "Independence_CH.Pairing_Axiom"
Presenting theory "Transitive_Models.Lambda_Replacement"
Presenting theory "Independence_CH.Union_Axiom"
Presenting theory "Independence_CH.Powerset_Axiom"
Presenting theory "Independence_CH.Extensionality_Axiom"
Presenting theory "Independence_CH.Foundation_Axiom"
Presenting theory "Independence_CH.Replacement_Axiom"
Presenting theory "Independence_CH.Infinity_Axiom"
Presenting theory "Independence_CH.Choice_Axiom"
Presenting theory "Independence_CH.Proper_Extension"
Presenting theory "Transitive_Models.Discipline_Cardinal"
Presenting theory "Independence_CH.Succession_Poset"
Presenting theory "Independence_CH.Forcing_Main"
Presenting theory "Transitive_Models.Univ_Relative"
Presenting theory "Independence_CH.Cardinal_Preservation"
Presenting theory "Independence_CH.Not_CH"
Presenting theory "Transitive_Models.Cardinal_Relative"
Presenting theory "Independence_CH.Kappa_Closed_Notions"
Presenting theory "Independence_CH.CH"
Presenting theory "Independence_CH.Absolute_Versions"
Presenting theory "Independence_CH.Definitions_Main"
Presenting theory "Transitive_Models.CardinalArith_Relative"
Presenting theory "Independence_CH.Demonstrations"
Presenting theory "Transitive_Models.Aleph_Relative"
Presenting theory "Transitive_Models.Cardinal_AC_Relative"
Presenting theory "Transitive_Models.FiniteFun_Relative"
Presenting theory "Transitive_Models.ZF_Library_Relative"
Presenting theory "Transitive_Models.Replacement_Lepoll"
Presenting theory "Transitive_Models.Cardinal_Library_Relative"
Presenting theory "Transitive_Models.Delta_System_Relative"
Presenting theory "Transitive_Models.Pointed_DC_Relative"
Presenting theory "Transitive_Models.Partial_Functions_Relative"
Unfinished session(s): Stalnaker_Logic
=== TIMING ===
Group AFP: 0:02:19 elapsed time, 0:10:26 cpu time, factor 4.50
Group main: 0:00:00 elapsed time
Group large: 0:00:00 elapsed time
Group no_doc: 0:00:00 elapsed time
Group doc: 0:00:00 elapsed time
Group timing: 0:00:05 elapsed time, 0:00:33 cpu time, factor 5.94
Overall: 0:05:56 elapsed time, 0:12:33 cpu time, factor 2.11
=== FAILED SESSIONS ===
Session Stalnaker_Logic: FAILED 1
=== DEPENDENCIES ===
Generating dependencies file ...
Writing dependencies file ...
=== REPORT ===
Writing report file ...
=== SITEGEN ===
Writing status file ...
Running sitegen ...
using [/media/data/jenkins/workspace/isabelle-all/bin/isabelle]
Preparing site generation in out/hugo
Cleaning up generated files...
Preparing topics...
Preparing licenses...
Preparing releases...
Preparing authors...
Extracting keywords...
Preparing entries...
Preparing statistics...
Preparing project files
Preparing devel version...
Finished sitegen preparation.
Cleaning output dir...
Building site...
Build in /media/data/jenkins/workspace/isabelle-all/afp/web/index.html
Packing tars ...
=== NOTIFICATIONS ===
=== COMPLETED ===
Build step 'Execute shell' marked build as failure
Started calculate disk usage of build
Finished Calculation of disk usage of build in 0 seconds
Started calculate disk usage of workspace
Finished Calculation of disk usage of workspace in 0 seconds
No emails were triggered.
Finished: FAILURE