Isabelle build status

status date:

08-Apr-2026 01:55:41 +0200

• AFP Windows
  Failed sessions:
  • CondNormReasHOL

    Timeout

    (Isabelle/c6fc0c7ef56f, AFP/7128e7a41134)
  • 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/c6fc0c7ef56f, AFP/7128e7a41134)
  • Diophantine_Universal_Pairs

    Timeout

    (Isabelle/c6fc0c7ef56f, AFP/7128e7a41134)
  • Hidden_Number_Problem

    Timeout

    (Isabelle/c6fc0c7ef56f, AFP/7128e7a41134)
  • Lowe_Ontological_Argument

    Timeout

    (Isabelle/c6fc0c7ef56f, AFP/7128e7a41134)
  • Proof_Terms_Term_Rewriting

    Timeout

    (Isabelle/c6fc0c7ef56f, AFP/7128e7a41134)
  • Superposition_Calculus

    Timeout

    (Isabelle/c6fc0c7ef56f, AFP/7128e7a41134)
  • Topological_Semantics

    Timeout

    (Isabelle/c6fc0c7ef56f, AFP/7128e7a41134)
  • Types_Tableaus_and_Goedels_God

    Timeout

    (Isabelle/c6fc0c7ef56f, AFP/7128e7a41134)
  • Zip_Benchmarks

    Timeout

    (Isabelle/c6fc0c7ef56f, AFP/7128e7a41134)
• AFP macOS (macOS 14 Sonoma, Apple Silicon)
  Failed sessions:
  • Diophantine_Universal_Pairs

    Timeout

    (Isabelle/4b7fdf77af07, AFP/2f539b3aa0b8)
  • Hidden_Number_Problem

    Timeout

    (Isabelle/4b7fdf77af07, AFP/2f539b3aa0b8)
  • Munta_Base

    Timeout

    (Isabelle/4b7fdf77af07, AFP/2f539b3aa0b8)
  • 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/4b7fdf77af07, AFP/2f539b3aa0b8)
  • Proof_Terms_Term_Rewriting

    Timeout

    (Isabelle/4b7fdf77af07, AFP/2f539b3aa0b8)
  • Set_Reconciliation

    Timeout

    (Isabelle/4b7fdf77af07, AFP/2f539b3aa0b8)
  • Superposition_Calculus

    Timeout

    (Isabelle/4b7fdf77af07, AFP/2f539b3aa0b8)
  • Zip_Benchmarks

    Timeout

    (Isabelle/4b7fdf77af07, AFP/2f539b3aa0b8)
• Linux (ARM)
• Linux C
• Linux C, 2 threads
• Linux C, 4 threads
• Linux C, 8 threads
• 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/6b2ac8d13c7a)
  • 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/6b2ac8d13c7a)
  • HOL-Predicate_Compile_Examples

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script15968293853497427189: 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_script16637577889621455029: 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_script10881674918639695822: 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_script12416904731670064654: 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_script12424570105414538049: 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/6b2ac8d13c7a)
  • 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/6b2ac8d13c7a)
  • 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/6b2ac8d13c7a)
• 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/6b2ac8d13c7a)
  • 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/6b2ac8d13c7a)
  • HOL-Predicate_Compile_Examples

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script5372550926896511877: 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_script6953352772571109876: 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_script9113906666005870038: 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_script13722387304664970812: 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_script17950507174820391925: 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_script8572150711594927916: 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_script1851665306245429530: 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_script15157652695652638095: 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_script5745255466358067049: 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_script13477935958024969675: 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_script14757853165095122800: 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_script9667293129456613814: 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_script11073862041285977779: 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_script7602612810620814992: 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_script1238305897438474144: 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_script9201565810838541192: 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_script7483422299056372110: 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_script2634427442107277455: 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_script668902579511566655: 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_script11738271250011572094: 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_script15618622587531957872: 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_script1993002532073050943: 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_script15480690531387536100: 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_script16425213259810815539: 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_script15275393991780509096: 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/6b2ac8d13c7a)
  • 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/6b2ac8d13c7a)
  • 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/6b2ac8d13c7a)
• 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 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")

    (Isabelle/6b2ac8d13c7a)
  • 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/6b2ac8d13c7a)
  • HOL-Predicate_Compile_Examples

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script2360321018091766615: 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_script1947573949723423048: 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_script10133863901123570802: 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_script12855340226537351279: 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_script1615179049155229715: 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_script3281754797205222820: 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_script3891706053730623825: 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_script7766169749644689807: 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_script13371217928483476560: 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_script10704507294638898620: 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_script16739563399360672564: 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_script14219243179439619322: 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_script11533120105328005720: 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_script1618970385076301345: 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_script15241441158414178535: 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_script2832453532018019089: 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_script12977409387344158901: 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_script13435043906212331444: 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_script15493454244802940119: 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_script120648400852320183: 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_script9661559868614966074: 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_script661772936606391664: 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_script16547950131123781232: 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_script9234231095334884064: 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_script11640751231564760911: 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/6b2ac8d13c7a)
  • 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/6b2ac8d13c7a)
  • 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/6b2ac8d13c7a)
• macOS 13 Ventura (ARM)
• macOS 13 Ventura (ARM), 2 threads
• macOS 13 Ventura (ARM), 4 threads
• macOS 14 Sonoma, quick_and_dirty, 4 threads
  Failed sessions:
  • HOL-Corec_Examples (Isabelle/6b2ac8d13c7a)
  • HOL-Datatype_Examples

    Session startup failed:
    standard_output terminated
    Assertion failed: (0), function RelocateAddress, file savestate.cpp, line 1022.
    /tmp/isabelle-isatest/bash_script17329866109244400565: line 1: 77723 Abort trap: 6           /Users/isatest/.isabelle/contrib/polyml-5.9.2-3/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\",\ \"/Users/isatest/.isabelle/build_history-mini2-sonoma_1/heaps/polyml-5.9.2_x86_64_32-darwin/HOL-Library\"\]\;\ 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/6b2ac8d13c7a)
  • HOL-Decision_Procs (Isabelle/6b2ac8d13c7a)
  • HOL-Nominal-Examples (Isabelle/6b2ac8d13c7a)
  • HOL-Number_Theory (Isabelle/6b2ac8d13c7a)
• macOS 14 Sonoma, skip_proofs, 4 threads