Isabelle build status

status date:

30-Dec-2025 00:41:20 +0100

• AFP Windows
  Failed sessions:
  • CondNormReasHOL

    Timeout

    (Isabelle/7313c4d69316, AFP/7e4523a74be8)
  • Difference_Bound_Matrices

    Solver verit: Solver terminated abnormally with error code 127
    At command "by" (line 834 of "~~/dirs/AFP/thys/Difference_Bound_Matrices/DBM_Constraint_Systems.thy")

    (Isabelle/7313c4d69316, AFP/7e4523a74be8)
  • Diophantine_Universal_Pairs

    Timeout

    (Isabelle/7313c4d69316, AFP/7e4523a74be8)
  • Hidden_Number_Problem

    Timeout

    (Isabelle/7313c4d69316, AFP/7e4523a74be8)
  • Lowe_Ontological_Argument

    Timeout

    (Isabelle/7313c4d69316, AFP/7e4523a74be8)
  • Proof_Terms_Term_Rewriting

    Timeout

    (Isabelle/7313c4d69316, AFP/7e4523a74be8)
  • Superposition_Calculus

    Timeout

    (Isabelle/7313c4d69316, AFP/7e4523a74be8)
  • Topological_Semantics

    Timeout

    (Isabelle/7313c4d69316, AFP/7e4523a74be8)
  • Types_Tableaus_and_Goedels_God

    Timeout

    (Isabelle/7313c4d69316, AFP/7e4523a74be8)
  • Zip_Benchmarks

    Timeout

    (Isabelle/7313c4d69316, AFP/7e4523a74be8)
• AFP macOS (macOS 14 Sonoma, Apple Silicon)
  Failed sessions:
  • Diophantine_Universal_Pairs

    Timeout

    (Isabelle/252739089bc8, AFP/a42f36c1f1f5)
  • Hidden_Number_Problem

    Timeout

    (Isabelle/252739089bc8, AFP/a42f36c1f1f5)
  • Munta_Base

    Timeout

    (Isabelle/252739089bc8, AFP/a42f36c1f1f5)
  • PAC_Checker

    Compilation failed (line 28 of "~~/dirs/AFP/thys/PAC_Checker/PAC_Checker_MLton.thy"):
    can't use native codegen on ARM64 target
    usage: mlton [option ...] file.{c|mlb|o|sml} [file.{c|o|s|S} ...]
        -align {8|4}                    object alignment
        -as-opt <opt>                   pass option to assembler
        -cc <cc>                        executable for C compiler
        -cc-opt <opt>                   pass option to C compiler
        -codegen {c|llvm}               which code generator to use
        -const '<name> <value>'         set compile-time constant
        -default-ann <ann>              set annotation default for mlb files
        -default-type '<ty><N>'         set default type
        -disable-ann <ann>              disable annotation in mlb files
        -export-header <file>           write C header file for _export's
        -ieee-fp {false|true}           use strict IEEE floating-point
        -inline <n>                     set inlining threshold
        -keep {g|o}                     save intermediate files
        -link-opt <opt>                 pass option to linker
        -llvm-as <llvm-as>              executable for llvm .ll -> .bc assembler
        -llvm-as-opt <opt>              pass option to llvm assembler
        -llvm-llc <llc>                 executable for llvm .bc -> .o system compiler
        -llvm-llc-opt <opt>             pass option to llvm compiler
        -llvm-opt <opt>                 executable for llvm .bc -> .bc optimizer
        -llvm-opt-opt <opt>             pass option to llvm optimizer
        -mlb-path-map <file>            additional MLB path map
        -mlb-path-var '<name> <value>'  additional MLB path var
        -output <file>                  name of output file
        -profile {no|alloc|count|time}  produce executable suitable for profiling
        -profile-branch {false|true}    profile branches in addition to functions
        -profile-stack {false|true}     profile the stack
        -profile-val {false|true}       profile val bindings in addition to functions
        -runtime <arg>                  pass arg to runtime via @MLton
        -show-basis <file>              write final basis environment
        -show-def-use <file>            write def-use information
        -stop {f|g|o|tc}                when to stop
        -target {self}                  platform that executable will run on
        -target-as-opt <target> <opt>   target-dependent assembler option
        -target-cc-opt <target> <opt>   target-dependent C compiler option
        -target-link-opt <target> <opt> target-dependent linker option
        -verbose {0|1|2|3}              how verbose to be
    
    At command "compile_generated_files" (line 19 of "~~/dirs/AFP/thys/PAC_Checker/PAC_Checker_MLton.thy")

    (Isabelle/252739089bc8, AFP/a42f36c1f1f5)
  • Proof_Terms_Term_Rewriting

    Timeout

    (Isabelle/252739089bc8, AFP/a42f36c1f1f5)
• Linux (ARM)
  Failed sessions:
  • HOL-ex

    Timeout

    (Isabelle/7313c4d69316)
  • HOLCF

    Timeout

    (Isabelle/7313c4d69316)
• macOS 12 Monterey (Intel)
  Failed sessions:
  • HOL-Imperative_HOL

    Failed to load theory "HOL-Imperative_HOL.Imperative_HOL_ex" (unresolved "HOL-Imperative_HOL.Imperative_Quicksort", "HOL-Imperative_HOL.Imperative_Reverse", "HOL-Imperative_HOL.Linked_Lists")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")

    (Isabelle/7313c4d69316)
  • HOL-Library

    Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-Library.Finite_Map")

    Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Disjoint_FSets", "HOL-Library.Finite_Map")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/7313c4d69316)
  • HOL-Predicate_Compile_Examples

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script17256561915327075848: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 27 of "~~/src/HOL/Predicate_Compile_Examples/List_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script17285242953698754144: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 82 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script535624550095410277: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 98 of "~~/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script8923502266836953093: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 39 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script1991481218347304898: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 21 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    (Isabelle/7313c4d69316)
  • HOL-Probability

    Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map")

    Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map")

    Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/7313c4d69316)
  • HOL-Proofs (Isabelle/7313c4d69316)
  • HOL-Quotient_Examples

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 98 of "~~/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy")

    (Isabelle/7313c4d69316)
• macOS 12 Monterey (Intel), 2 threads
  Failed sessions:
  • HOL-Imperative_HOL

    Failed to load theory "HOL-Imperative_HOL.Imperative_HOL_ex" (unresolved "HOL-Imperative_HOL.Imperative_Quicksort", "HOL-Imperative_HOL.Imperative_Reverse", "HOL-Imperative_HOL.Linked_Lists")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")

    (Isabelle/7313c4d69316)
  • HOL-Library

    Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-Library.Finite_Map")

    Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Disjoint_FSets", "HOL-Library.Finite_Map")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/7313c4d69316)
  • HOL-Predicate_Compile_Examples

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script8953319391207403266: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 98 of "~~/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script6763125847177927430: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 27 of "~~/src/HOL/Predicate_Compile_Examples/List_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script5466021868470329176: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 154 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script3481717170633841905: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 137 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script17167177119211006054: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 118 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script4322797906119674060: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 105 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script13824033616923868970: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 90 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script9185754822964770696: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 82 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script8610232882188660367: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 162 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script5734038560480605014: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 228 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script8843873788086842390: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 119 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script8553894037396014357: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 220 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script14323578122469797977: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 214 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script10225392151651342353: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 97 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script16541353590774235884: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 73 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script4545455734301578855: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 39 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script14355696455399014035: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 196 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script16055438328237293918: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 195 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script14321387551338935708: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 194 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script9895662768840720055: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 193 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script5279645953806489585: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 103 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script17256653243269087954: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 35 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script3186443496153229501: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 25 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script10108500482690655881: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 23 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script15987133435907358807: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 21 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    (Isabelle/7313c4d69316)
  • HOL-Probability

    Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map")

    Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map")

    Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/7313c4d69316)
  • HOL-Quotient_Examples

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 98 of "~~/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy")

    (Isabelle/7313c4d69316)
• macOS 12 Monterey (Intel), 4 threads
  Failed sessions:
  • HOL-Imperative_HOL

    Failed to load theory "HOL-Imperative_HOL.Imperative_HOL_ex" (unresolved "HOL-Imperative_HOL.Imperative_Quicksort", "HOL-Imperative_HOL.Imperative_Reverse", "HOL-Imperative_HOL.Linked_Lists")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")

    (Isabelle/7313c4d69316)
  • HOL-Library

    Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-Library.Finite_Map")

    Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Disjoint_FSets", "HOL-Library.Finite_Map")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/7313c4d69316)
  • HOL-Predicate_Compile_Examples

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script12023268748153576554: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 154 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script720185697200459426: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 196 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script15926670000360751348: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 228 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script18093529442220753880: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 220 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script7138793956322650683: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 195 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script6414520921763896578: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 214 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script16578897066692182518: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 194 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script6196975606876385730: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 193 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script16502368214488909399: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 137 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script15392613152093291643: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 118 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script17010198153803631241: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 105 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script7100976201361542456: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 90 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script6023414530294032720: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 82 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script16829803396143318016: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 27 of "~~/src/HOL/Predicate_Compile_Examples/List_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script3475347230287797017: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 98 of "~~/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script14215629605764000186: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 162 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script1547421731268215139: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 119 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script706107391717669313: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 97 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script8340132785224463689: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 73 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script4362880614816694806: line 1: /usr/local/bin/swipl: No such file or directory
    At command "quickcheck" (line 39 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script4268426089764713764: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 103 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script15246039519805657244: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 35 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script6082722178366214233: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 25 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script12835970694359714233: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 23 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script12869787705816473769: line 1: /usr/local/bin/swipl: No such file or directory
    At command "values_prolog" (line 21 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")

    (Isabelle/7313c4d69316)
  • HOL-Probability

    Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map")

    Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map")

    Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit")

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/7313c4d69316)
  • HOL-Quotient_Examples

    Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml
    At command "export_code" (line 98 of "~~/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy")

    (Isabelle/7313c4d69316)
• macOS 13 Ventura (ARM)
  Failed sessions:
  • HOL-Probability (Isabelle/7313c4d69316)
  • HOL-Probability-ex (Isabelle/490ffe526eeb)
  • HOL-Quickcheck_Benchmark (Isabelle/7313c4d69316)
  • HOL-Quickcheck_Examples (Isabelle/7313c4d69316)
  • HOL-Real_Asymp (Isabelle/7313c4d69316)
  • HOL-Real_Asymp-Manual (Isabelle/c3b95902bc4d)
  • HOL-Record_Benchmark (Isabelle/13d5b3ded580)
• macOS 13 Ventura (ARM), 2 threads
• macOS 13 Ventura (ARM), 4 threads
• macOS 14 Sonoma, quick_and_dirty, 4 threads
  Failed sessions:
  • HOL (Isabelle/02c8a8393f53)
  • HOL-Codegenerator_Test

    exception TERM raised (line 177 of "logic.ML"):
      dest_equals
      B.31091328385286147 HEAD
       unknown.Rep_unknown_IITN_unknown
    At command "export_code" (line 19 of "~~/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy")

    Code check failed for SML: isabelle ML_process -o ML_platform\=x86_64_32-darwin -C /tmp/isabelle-isatest/process16405447184328456618/Code_Test12391148 -r -e datatype\ ref\ \=\ datatype\ Unsynchronized.ref -f /tmp/isabelle-isatest/process16405447184328456618/Code_Test12391148/ROOT.ML -l Pure
    At command "export_code" (line 17 of "~~/src/HOL/Codegenerator_Test/Generate_Abstract_Char.thy")

    (Isabelle/c3b95902bc4d)
  • HOL-Corec_Examples (Isabelle/c3b95902bc4d)
  • HOL-MicroJava (Isabelle/c3b95902bc4d)
  • HOL-Nominal-Examples (Isabelle/c3b95902bc4d)
  • HOL-Proofs (Isabelle/02c8a8393f53)
  • HOL-ex (Isabelle/c3b95902bc4d)
  • IOA-ABP (Isabelle/c3b95902bc4d)
  • Implementation

    Session startup failed:
    standard_output terminated
    Assertion failed: (0), function RelocateAddress, file savestate.cpp, line 1022.
    /tmp/isabelle-isatest/bash_script1665090051485112270: line 1: 70689 Abort trap: 6           /Users/isatest/.isabelle/contrib/polyml-5.9.2-2/x86_64_32-darwin/poly -q --minheap 1500 --gcthreads 4 --exportstats --eval \(PolyML.SaveState.loadHierarchy\ \[\"/Users/isatest/.isabelle/build_history-mini2-sonoma_1/heaps/polyml-5.9.2_x86_64_32-darwin/Pure\",\ \"/Users/isatest/.isabelle/build_history-mini2-sonoma_1/heaps/polyml-5.9.2_x86_64_32-darwin/HOL\"\]\;\ PolyML.print_depth\ 0\) --eval Options.load_default\ \(\) --eval Resources.init_session_env\ \(\) --eval Command_Line.tool\ \(fn\ \(\)\ \=\>\ \(Isabelle_Process.init_build\ \(\)\)\)\;
    Return code: 127 (COMMAND NOT FOUND)

    (Isabelle/c3b95902bc4d)
• macOS 14 Sonoma, skip_proofs, 4 threads
  Failed sessions:
  • HOL (Isabelle/02c8a8393f53)
  • HOL-Proofs (Isabelle/02c8a8393f53)
  • System (Isabelle/02c8a8393f53)