Isabelle build status

AFP Windows
Failed sessions:

CondNormReasHOL
```
Timeout
```
(Isabelle/e8423c714e72, AFP/da3d8a58c9b3)

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/e8423c714e72, AFP/da3d8a58c9b3)

Diophantine_Universal_Pairs
```
Timeout
```
(Isabelle/e8423c714e72, AFP/da3d8a58c9b3)
Hidden_Number_Problem
```
Timeout
```
(Isabelle/e8423c714e72, AFP/da3d8a58c9b3)
Lowe_Ontological_Argument
```
Timeout
```
(Isabelle/e8423c714e72, AFP/da3d8a58c9b3)
Proof_Terms_Term_Rewriting
```
Timeout
```
(Isabelle/e8423c714e72, AFP/da3d8a58c9b3)
Set_Reconciliation
```
Timeout
```
(Isabelle/e8423c714e72, AFP/da3d8a58c9b3)
Superposition_Calculus
```
Timeout
```
(Isabelle/e8423c714e72, AFP/da3d8a58c9b3)
Topological_Semantics
```
Timeout
```
(Isabelle/e8423c714e72, AFP/da3d8a58c9b3)
Types_Tableaus_and_Goedels_God
```
Timeout
```
(Isabelle/e8423c714e72, AFP/da3d8a58c9b3)
Zip_Benchmarks
```
Timeout
```
(Isabelle/e8423c714e72, AFP/da3d8a58c9b3)

AFP macOS (macOS 14 Sonoma, Apple Silicon)
Failed sessions:

Diophantine_Universal_Pairs
```
Timeout
```
(Isabelle/c197f6bd0526, AFP/e6f2c01e3796)
Hidden_Number_Problem
```
Timeout
```
(Isabelle/c197f6bd0526, AFP/e6f2c01e3796)
Munta_Base
```
Timeout
```
(Isabelle/c197f6bd0526, AFP/e6f2c01e3796)

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/c197f6bd0526, AFP/e6f2c01e3796)

Proof_Terms_Term_Rewriting
```
Timeout
```
(Isabelle/c197f6bd0526, AFP/e6f2c01e3796)
Set_Reconciliation
```
Timeout
```
(Isabelle/c197f6bd0526, AFP/e6f2c01e3796)
Superposition_Calculus
```
Timeout
```
(Isabelle/c197f6bd0526, AFP/e6f2c01e3796)
Zip_Benchmarks
```
Timeout
```
(Isabelle/c197f6bd0526, AFP/e6f2c01e3796)

Linux (ARM)

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/e8423c714e72)

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/e8423c714e72)

HOL-Predicate_Compile_Examples

Error caused by prolog system ISABELLE_SWIPL: return code 127
/tmp/isabelle-isatest/bash_script8570074141847053420: 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_script3832661724447334403: 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_script16060785520167210201: 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_script10278702402592265119: 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_script64450653866175211: 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/e8423c714e72)

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/e8423c714e72)

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/e8423c714e72)

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/e8423c714e72)

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/e8423c714e72)

HOL-Predicate_Compile_Examples

Error caused by prolog system ISABELLE_SWIPL: return code 127
/tmp/isabelle-isatest/bash_script6983559093504488878: 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_script14986510230666274859: 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_script13442988093145541863: 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_script13055030355252357860: 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_script1302376234192638405: 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_script663599559687546170: 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_script12299029540280233490: 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_script4909405353691966467: 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_script1262391293341119409: 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_script2597575811118124713: 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_script6741327179035474076: 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_script7196793222407392217: 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_script9331391870614217966: 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_script6747785293731212833: 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_script6198122610530924655: 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_script2273661019263188809: 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_script8218298473351650987: 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_script8349496742368744425: 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_script2797330461603761887: 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_script13294036584119442232: 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_script7233031104130920489: 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_script4626433188048750750: 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_script14142915521045180453: 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_script4036066575558870797: 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_script14267128538397503077: 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/e8423c714e72)

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/e8423c714e72)

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/e8423c714e72)

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/e8423c714e72)

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/e8423c714e72)

HOL-Predicate_Compile_Examples

Error caused by prolog system ISABELLE_SWIPL: return code 127
/tmp/isabelle-isatest/bash_script8947013987305212531: 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_script1850039305467107840: 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_script15642922396044868181: 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_script3759485969334205579: 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_script8455684575671744037: 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_script6947932781243757792: 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_script1273117976119533930: 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_script18324813683078318653: 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_script8653432944918897557: 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_script2376715047668663753: 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_script8947413071962928851: 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_script5716875921963645252: 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_script1924476415894646466: 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_script15760914697426489248: 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_script6646510272200597371: 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_script15456144251524552625: 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_script8239809401088193489: 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_script18368193440921946433: 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_script15157934058531117615: 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_script13141609422496110848: 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_script17327150868327134523: 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_script14129182070808836458: 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_script13539207116887888100: 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_script12897116226231488710: 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_script16331322143808663053: 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/e8423c714e72)

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/e8423c714e72)

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/e8423c714e72)

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 (Isabelle/e8423c714e72)
HOL-Proofs (Isabelle/e8423c714e72)

macOS 14 Sonoma, skip_proofs, 4 threads
Failed sessions:

HOL-Codegenerator_Test (Isabelle/e8423c714e72)
HOL-Datatype_Examples (Isabelle/e8423c714e72)
HOL-Nominal-Examples (Isabelle/e8423c714e72)