Isabelle build status

status date:

17-Sep-2025 01:21:48 +0200

• AFP Windows
  Failed sessions:
  • CondNormReasHOL

    Timeout

    (Isabelle/cfd4cd1c2f23, AFP/781fee4f0d37)
  • 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/cfd4cd1c2f23, AFP/781fee4f0d37)
  • Hidden_Number_Problem

    Timeout

    (Isabelle/cfd4cd1c2f23, AFP/781fee4f0d37)
  • Lowe_Ontological_Argument

    Timeout

    (Isabelle/cfd4cd1c2f23, AFP/781fee4f0d37)
  • Proof_Terms_Term_Rewriting

    Timeout

    (Isabelle/cfd4cd1c2f23, AFP/781fee4f0d37)
  • Superposition_Calculus

    Timeout

    (Isabelle/cfd4cd1c2f23, AFP/781fee4f0d37)
  • Topological_Semantics

    Timeout

    (Isabelle/cfd4cd1c2f23, AFP/781fee4f0d37)
  • Types_Tableaus_and_Goedels_God

    Timeout

    (Isabelle/cfd4cd1c2f23, AFP/781fee4f0d37)
• AFP macOS (macOS 14 Sonoma, Apple Silicon)
  Failed sessions:
  • Hidden_Number_Problem

    Timeout

    (Isabelle/87ceb18f23f3, AFP/781fee4f0d37)
  • Munta_Base

    Timeout

    (Isabelle/87ceb18f23f3, AFP/781fee4f0d37)
  • 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/87ceb18f23f3, AFP/781fee4f0d37)
  • Proof_Terms_Term_Rewriting

    Timeout

    (Isabelle/87ceb18f23f3, AFP/781fee4f0d37)
• Linux (ARM)
• macOS 12 Monterey (Intel)
  Failed sessions:
  • HOL (Isabelle/87ceb18f23f3)
  • HOL-Codegenerator_Test

    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")

    Failed to load theory "HOL-Codegenerator_Test.Candidates" (unresolved "HOL-Library.Library")

    Failed to load theory "HOL-Codegenerator_Test.Generate" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Abstract_Char" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Binary_Nat" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Efficient_Datastructures" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Target_Nat" (unresolved "HOL-Codegenerator_Test.Candidates")

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

    (Isabelle/c3c278374b5b)
  • 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 </dev/null
    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 </dev/null
    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 </dev/null
    At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")

    (Isabelle/c3c278374b5b)
  • 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 </dev/null
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/c3c278374b5b)
  • HOL-Predicate_Compile_Examples

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script9232438728226351814: 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_script16290108502734884286: 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_script11536439708678906936: 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_script18074504789075388034: 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_script4418429834481381547: 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/c3c278374b5b)
  • 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 </dev/null
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/c3c278374b5b)
  • HOL-Proofs (Isabelle/87ceb18f23f3)
  • HOL-Quotient_Examples

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

    (Isabelle/c3c278374b5b)
  • HOL-ex

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

    (Isabelle/c3c278374b5b)
• macOS 12 Monterey (Intel), 2 threads
  Failed sessions:
  • HOL (Isabelle/87ceb18f23f3)
  • HOL-Codegenerator_Test

    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")

    Failed to load theory "HOL-Codegenerator_Test.Candidates" (unresolved "HOL-Library.Library")

    Failed to load theory "HOL-Codegenerator_Test.Generate" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Abstract_Char" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Binary_Nat" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Efficient_Datastructures" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Target_Nat" (unresolved "HOL-Codegenerator_Test.Candidates")

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

    (Isabelle/c3c278374b5b)
  • 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 </dev/null
    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 </dev/null
    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 </dev/null
    At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")

    (Isabelle/c3c278374b5b)
  • 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 </dev/null
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/c3c278374b5b)
  • HOL-Predicate_Compile_Examples

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script16949365981019942680: 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_script11468628484800029132: 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_script8067562337406928454: 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_script7117782808376440748: 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_script12168972320427029574: 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_script17449922766535862769: 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_script11739157363152302797: 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_script5938329707725573761: 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_script3742846811703509714: 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_script6017700559858944789: 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_script5078697932644911171: 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_script4888371567111471430: 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_script450958073167304077: 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_script1505973702200986938: 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_script10824573596724791862: 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_script5202059896473347023: 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_script6701097450065385010: 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_script8600149277603929470: 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_script11998367047339707242: 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_script10822809506409785829: 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_script16266986025820607178: 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_script12489174442128786253: 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_script14146731526702029604: 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_script1644240021390199031: 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_script8789445469365479528: 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/c3c278374b5b)
  • 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 </dev/null
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/c3c278374b5b)
  • HOL-Quotient_Examples

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

    (Isabelle/c3c278374b5b)
  • HOL-ex

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

    (Isabelle/c3c278374b5b)
• macOS 12 Monterey (Intel), 4 threads
  Failed sessions:
  • HOL (Isabelle/87ceb18f23f3)
  • HOL-Codegenerator_Test

    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")

    Failed to load theory "HOL-Codegenerator_Test.Candidates" (unresolved "HOL-Library.Library")

    Failed to load theory "HOL-Codegenerator_Test.Generate" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Abstract_Char" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Binary_Nat" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Target_Nat" (unresolved "HOL-Codegenerator_Test.Candidates")

    Failed to load theory "HOL-Codegenerator_Test.Generate_Efficient_Datastructures" (unresolved "HOL-Codegenerator_Test.Candidates")

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

    (Isabelle/c3c278374b5b)
  • 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 </dev/null
    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 </dev/null
    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 </dev/null
    At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")

    (Isabelle/c3c278374b5b)
  • 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 </dev/null
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/c3c278374b5b)
  • HOL-Predicate_Compile_Examples

    Error caused by prolog system ISABELLE_SWIPL: return code 127
    /tmp/isabelle-isatest/bash_script5819701451861907214: 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_script250985823950616337: 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_script10793309460547492005: 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_script6949421118697863460: 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_script11649870444816260739: 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_script6858604346060833025: 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_script11364452503418048228: 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_script1824092178583685533: 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_script15999061518579683697: 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_script16961439323736391491: 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_script15679556036515610299: 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_script18309942593880418344: 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_script8157582722732937946: 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_script12294229871331853308: 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_script4285337686440935043: 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_script12666853335853809133: 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_script13605761909637276302: 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_script11106053707593787441: 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_script1795215441150253052: 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_script14863217136517645064: 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_script14004453379288620060: 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_script9348176337883688335: 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_script6091933410303497385: 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_script5468481446040750189: 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_script4420683778144282984: 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/c3c278374b5b)
  • 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 </dev/null
    At command "export_code" (line 1406 of "~~/src/HOL/Library/Finite_Map.thy")

    (Isabelle/c3c278374b5b)
  • HOL-Quotient_Examples

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

    (Isabelle/c3c278374b5b)
  • HOL-ex

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

    (Isabelle/c3c278374b5b)
• macOS 13 Ventura (ARM)
• macOS 13 Ventura (ARM), 2 threads
• macOS 13 Ventura (ARM), 4 threads
• macOS 14 Sonoma, quick_and_dirty, 4 threads
• macOS 14 Sonoma, skip_proofs, 4 threads