Isabelle build status

AFP Windows
Failed sessions:

CondNormReasHOL
```
Timeout
```
(Isabelle/86a7ec064208, AFP/f024bf0380ce)

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/86a7ec064208, AFP/f024bf0380ce)

Diophantine_Universal_Pairs
```
Timeout
```
(Isabelle/86a7ec064208, AFP/f024bf0380ce)
Hidden_Number_Problem
```
Timeout
```
(Isabelle/86a7ec064208, AFP/f024bf0380ce)
Lowe_Ontological_Argument
```
Timeout
```
(Isabelle/86a7ec064208, AFP/f024bf0380ce)
Proof_Terms_Term_Rewriting
```
Timeout
```
(Isabelle/86a7ec064208, AFP/f024bf0380ce)
Superposition_Calculus
```
Timeout
```
(Isabelle/86a7ec064208, AFP/f024bf0380ce)
Topological_Semantics
```
Timeout
```
(Isabelle/86a7ec064208, AFP/f024bf0380ce)
Types_Tableaus_and_Goedels_God
```
Timeout
```
(Isabelle/86a7ec064208, AFP/f024bf0380ce)
Zip_Benchmarks
```
Timeout
```
(Isabelle/86a7ec064208, AFP/f024bf0380ce)

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)

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

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 1396 of "~~/src/HOL/Library/Finite_Map.thy")

(Isabelle/c13a4bd3c018)

HOL-Predicate_Compile_Examples

Error caused by prolog system ISABELLE_SWIPL: return code 127
/tmp/isabelle-isatest/bash_script8009523405542848143: 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_script11678213875994694141: 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_script14623348769293341532: 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_script17578422238995519668: 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_script9558577269186614723: 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/c13a4bd3c018)

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 1396 of "~~/src/HOL/Library/Finite_Map.thy")

(Isabelle/c13a4bd3c018)

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

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

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 1396 of "~~/src/HOL/Library/Finite_Map.thy")

(Isabelle/c13a4bd3c018)

HOL-Predicate_Compile_Examples

Error caused by prolog system ISABELLE_SWIPL: return code 127
/tmp/isabelle-isatest/bash_script11522239744753353229: 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_script17840572049426944885: 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_script15076853019645315187: 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_script13887976359320820004: 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_script4801542381436593840: 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_script2630908073219851773: 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_script12709389297062872020: 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_script12191855053533421321: 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_script15783928762036664182: 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_script3187618719134839114: 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_script5587564923130624496: 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_script15561877936343024229: 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_script17181657235911890315: 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_script2616001886807348371: 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_script6102270801110256972: 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_script11726602038335982187: 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_script12407590481642842930: 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_script30580415676943481: 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_script8389479283186516257: 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_script8676430995765209246: 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_script15759006846145215641: 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_script10238493299146060606: 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_script9187556324326348100: 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_script17176098247794503520: 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_script11127275896692348545: 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/c13a4bd3c018)

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 1396 of "~~/src/HOL/Library/Finite_Map.thy")

(Isabelle/c13a4bd3c018)

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

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

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 1396 of "~~/src/HOL/Library/Finite_Map.thy")

(Isabelle/c13a4bd3c018)

HOL-Predicate_Compile_Examples

Error caused by prolog system ISABELLE_SWIPL: return code 127
/tmp/isabelle-isatest/bash_script2950564897232759794: 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_script8384635766436006931: 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_script4652956119275941382: 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_script3452892542492715783: 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_script13980982089329886768: 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_script1522485234898126829: 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_script10265606487452504853: 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_script3932522565024507539: 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_script1996751842345608506: 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_script15530280693163271549: 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_script7032865672383808012: 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_script12043366658617656414: 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_script17253804316032787543: 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_script8580034101200130272: 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_script17352664290591424142: 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_script2121389108177782111: 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_script12785103622656465203: 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_script11798452106363405019: 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_script11461569942694291135: 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_script4550851848219488570: 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_script11524171528684217641: 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_script14090437265146238306: 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_script18410507066840650672: 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_script16353568699213711066: 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_script4860841662964076734: 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/c13a4bd3c018)

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 1396 of "~~/src/HOL/Library/Finite_Map.thy")

(Isabelle/c13a4bd3c018)

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

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/c13a4bd3c018)
HOL-Algebra (Isabelle/6e4787b57ac6)
HOL-Analysis (Isabelle/6e4787b57ac6)
HOL-Data_Structures (Isabelle/6e4787b57ac6)
HOL-Library (Isabelle/6e4787b57ac6)
HOL-Nominal-Examples (Isabelle/6e4787b57ac6)
HOL-Proofs (Isabelle/c13a4bd3c018)
HOLCF (Isabelle/300cfc008718)
ZF (Isabelle/c13a4bd3c018)

macOS 14 Sonoma, skip_proofs, 4 threads
Failed sessions:

HOL

Failed to load theory "HOL.Argo" (unresolved "HOL.HOL")

Failed to load theory "HOL.SAT" (unresolved "HOL.Argo")

Failed to load theory "HOL.Ctr_Sugar" (unresolved "HOL.HOL")

Failed to load theory "HOL.Orderings" (unresolved "HOL.HOL")

Failed to load theory "HOL.Groups" (unresolved "HOL.Orderings")

Failed to load theory "HOL.Lattices" (unresolved "HOL.Groups")

Failed to load theory "HOL.Boolean_Algebras" (unresolved "HOL.Lattices")

Failed to load theory "HOL.Set" (unresolved "HOL.Boolean_Algebras", "HOL.Lattices")

Failed to load theory "HOL.Fun" (unresolved "HOL.Set")

Failed to load theory "HOL.Typedef" (unresolved "HOL.Set")

Failed to load theory "HOL.Complete_Lattices" (unresolved "HOL.Fun")

Failed to load theory "HOL.Rings" (unresolved "HOL.Fun", "HOL.Groups", "HOL.Set")

Failed to load theory "HOL.Inductive" (unresolved "HOL.Complete_Lattices", "HOL.Ctr_Sugar")

Failed to load theory "HOL.Product_Type" (unresolved "HOL.Fun", "HOL.Inductive", "HOL.Typedef")

Failed to load theory "HOL.Sum_Type" (unresolved "HOL.Fun", "HOL.Inductive", "HOL.Typedef")

Failed to load theory "HOL.Complete_Partial_Order" (unresolved "HOL.Product_Type")

Failed to load theory "HOL.Nat" (unresolved "HOL.Fun", "HOL.Inductive", "HOL.Rings", "HOL.Typedef")

Failed to load theory "HOL.Fields" (unresolved "HOL.Nat")

Failed to load theory "HOL.Meson" (unresolved "HOL.Nat")

Failed to load theory "HOL.Relation" (unresolved "HOL.Fields", "HOL.Product_Type", "HOL.Sum_Type")

Failed to load theory "HOL.Finite_Set" (unresolved "HOL.Fields", "HOL.Product_Type", "HOL.Relation", "HOL.Sum_Type")

Failed to load theory "HOL.Transitive_Closure" (unresolved "HOL.Finite_Set")

Failed to load theory "HOL.Wellfounded" (unresolved "HOL.Transitive_Closure")

Failed to load theory "HOL.Fun_Def_Base" (unresolved "HOL.Ctr_Sugar", "HOL.Set", "HOL.Wellfounded")

Failed to load theory "HOL.Hilbert_Choice" (unresolved "HOL.Wellfounded")

Failed to load theory "HOL.ATP" (unresolved "HOL.Hilbert_Choice", "HOL.Meson")

Failed to load theory "HOL.Wfrec" (unresolved "HOL.Wellfounded")

Failed to load theory "HOL.Metis" (unresolved "HOL.ATP")

Failed to load theory "HOL.Order_Relation" (unresolved "HOL.Wfrec")

Failed to load theory "HOL.BNF_Wellorder_Relation" (unresolved "HOL.Order_Relation")

Failed to load theory "HOL.BNF_Wellorder_Embedding" (unresolved "HOL.BNF_Wellorder_Relation", "HOL.Hilbert_Choice")

Failed to load theory "HOL.BNF_Wellorder_Constructions" (unresolved "HOL.BNF_Wellorder_Embedding")

Failed to load theory "HOL.Zorn" (unresolved "HOL.Hilbert_Choice", "HOL.Order_Relation")

Failed to load theory "HOL.BNF_Cardinal_Order_Relation" (unresolved "HOL.BNF_Wellorder_Constructions", "HOL.Zorn")

Failed to load theory "HOL.BNF_Cardinal_Arithmetic" (unresolved "HOL.BNF_Cardinal_Order_Relation")

Failed to load theory "HOL.BNF_Def" (unresolved "HOL.BNF_Cardinal_Arithmetic", "HOL.Fun_Def_Base")

Failed to load theory "HOL.BNF_Composition" (unresolved "HOL.BNF_Def")

Failed to load theory "HOL.Basic_BNFs" (unresolved "HOL.BNF_Def")

Failed to load theory "HOL.BNF_Fixpoint_Base" (unresolved "HOL.BNF_Composition", "HOL.Basic_BNFs")

Failed to load theory "HOL.BNF_Least_Fixpoint" (unresolved "HOL.BNF_Fixpoint_Base")

Failed to load theory "HOL.Basic_BNF_LFPs" (unresolved "HOL.BNF_Least_Fixpoint")

Failed to load theory "HOL.Equiv_Relations" (unresolved "HOL.BNF_Least_Fixpoint")

Failed to load theory "HOL.Transfer" (unresolved "HOL.Basic_BNF_LFPs", "HOL.Hilbert_Choice", "HOL.Metis")

Failed to load theory "HOL.Lifting" (unresolved "HOL.Equiv_Relations", "HOL.Transfer")

Failed to load theory "HOL.Num" (unresolved "HOL.BNF_Least_Fixpoint", "HOL.Transfer")

Failed to load theory "HOL.Option" (unresolved "HOL.Lifting")

Failed to load theory "HOL.Power" (unresolved "HOL.Num")

Failed to load theory "HOL.Quotient" (unresolved "HOL.Lifting")

Failed to load theory "HOL.Extraction" (unresolved "HOL.Option")

Failed to load theory "HOL.Partial_Function" (unresolved "HOL.Complete_Partial_Order", "HOL.Option")

Failed to load theory "HOL.Groups_Big" (unresolved "HOL.Equiv_Relations", "HOL.Power")

Failed to load theory "HOL.Fun_Def" (unresolved "HOL.Basic_BNF_LFPs", "HOL.Partial_Function", "HOL.SAT")

Failed to load theory "HOL.Int" (unresolved "HOL.Fun_Def", "HOL.Groups_Big", "HOL.Quotient")

Failed to load theory "HOL.Lattices_Big" (unresolved "HOL.Groups_Big", "HOL.Option")

Failed to load theory "HOL.Lifting_Set" (unresolved "HOL.Groups_Big", "HOL.Lifting")

Failed to load theory "HOL.Euclidean_Rings" (unresolved "HOL.Int", "HOL.Lattices_Big")

Failed to load theory "HOL.Parity" (unresolved "HOL.Euclidean_Rings")

Failed to load theory "HOL.Numeral_Simprocs" (unresolved "HOL.Parity")

Failed to load theory "HOL.Set_Interval" (unresolved "HOL.Parity")

Failed to load theory "HOL.SMT" (unresolved "HOL.Numeral_Simprocs")

Failed to load theory "HOL.Semiring_Normalization" (unresolved "HOL.Numeral_Simprocs")

Failed to load theory "HOL.Conditionally_Complete_Lattices" (unresolved "HOL.Finite_Set", "HOL.Lattices_Big", "HOL.Set_Interval")

Failed to load theory "HOL.Groebner_Basis" (unresolved "HOL.Parity", "HOL.Semiring_Normalization")

Failed to load theory "HOL.Filter" (unresolved "HOL.Lifting_Set", "HOL.Set_Interval")

Failed to load theory "HOL.Presburger" (unresolved "HOL.Groebner_Basis", "HOL.Set_Interval")

Failed to load theory "HOL.Try0_HOL" (unresolved "HOL.Presburger")

Failed to load theory "HOL.Sledgehammer" (unresolved "HOL.Presburger", "HOL.SMT", "HOL.Try0_HOL")

Failed to load theory "HOL.List" (unresolved "HOL.Lifting_Set", "HOL.Sledgehammer")

Failed to load theory "HOL.Groups_List" (unresolved "HOL.List")

Failed to load theory "HOL.Map" (unresolved "HOL.List")

Failed to load theory "HOL.Bit_Operations" (unresolved "HOL.Groups_List", "HOL.Presburger")

Failed to load theory "HOL.Factorial" (unresolved "HOL.Groups_List")

Failed to load theory "HOL.Enum" (unresolved "HOL.Groups_List", "HOL.Map")

Failed to load theory "HOL.Code_Numeral" (unresolved "HOL.Bit_Operations", "HOL.Lifting")

Failed to load theory "HOL.Binomial" (unresolved "HOL.Factorial", "HOL.Presburger")

Failed to load theory "HOL.GCD" (unresolved "HOL.Code_Numeral", "HOL.Groups_List")

Failed to load theory "HOL.String" (unresolved "HOL.Bit_Operations", "HOL.Code_Numeral", "HOL.Enum")

Failed to load theory "HOL.BNF_Greatest_Fixpoint" (unresolved "HOL.BNF_Fixpoint_Base", "HOL.String")

Failed to load theory "HOL.Predicate" (unresolved "HOL.String")

Failed to load theory "HOL.Typerep" (unresolved "HOL.String")

Failed to load theory "HOL.Random" (unresolved "HOL.Code_Numeral", "HOL.Groups_List", "HOL.List")

Failed to load theory "HOL.Lazy_Sequence" (unresolved "HOL.Predicate")

Failed to load theory "HOL.Limited_Sequence" (unresolved "HOL.Lazy_Sequence")

Failed to load theory "HOL.Code_Evaluation" (unresolved "HOL.Limited_Sequence", "HOL.Typerep")

Failed to load theory "HOL.Quickcheck_Random" (unresolved "HOL.Code_Evaluation", "HOL.Enum", "HOL.Random")

Failed to load theory "HOL.Quickcheck_Exhaustive" (unresolved "HOL.Quickcheck_Random")

Failed to load theory "HOL.Quickcheck_Narrowing" (unresolved "HOL.Quickcheck_Random")

Failed to load theory "HOL.Random_Pred" (unresolved "HOL.Quickcheck_Random")

Failed to load theory "HOL.Record" (unresolved "HOL.Quickcheck_Exhaustive")

Failed to load theory "HOL.Nitpick" (unresolved "HOL.GCD", "HOL.Record")

Failed to load theory "HOL.Random_Sequence" (unresolved "HOL.Random_Pred")

Failed to load theory "HOL.Nunchaku" (unresolved "HOL.Nitpick")

Failed to load theory "HOL.Predicate_Compile" (unresolved "HOL.Quickcheck_Exhaustive", "HOL.Random_Sequence")

Failed to load theory "HOL.Mirabelle" (unresolved "HOL.Predicate_Compile", "HOL.Presburger", "HOL.Sledgehammer")

Failed to load theory "Main" (unresolved "HOL.BNF_Greatest_Fixpoint", "HOL.Binomial", "HOL.Conditionally_Complete_Lattices", "HOL.Extraction", "HOL.Filter", "HOL.GCD", "HOL.Mirabelle", "HOL.Nunchaku", "HOL.Predicate_Compile", "HOL.Quickcheck_Narrowing")

Failed to load theory "HOL.Archimedean_Field" (unresolved "Main")

Failed to load theory "HOL.Hull" (unresolved "Main")

Failed to load theory "HOL.Rat" (unresolved "HOL.Archimedean_Field")

Failed to load theory "HOL.Topological_Spaces" (unresolved "Main")

Failed to load theory "HOL.Modules" (unresolved "HOL.Hull")

Failed to load theory "HOL.Real" (unresolved "HOL.Rat")

Failed to load theory "HOL.Vector_Spaces" (unresolved "HOL.Modules")

Failed to load theory "HOL.Binomial_Plus" (unresolved "HOL.Real")

Failed to load theory "HOL.Real_Vector_Spaces" (unresolved "HOL.Real", "HOL.Topological_Spaces", "HOL.Vector_Spaces")

Failed to load theory "HOL.Inequalities" (unresolved "HOL.Real_Vector_Spaces")

Failed to load theory "HOL.Limits" (unresolved "HOL.Real_Vector_Spaces")

Failed to load theory "HOL.Deriv" (unresolved "HOL.Limits")

Failed to load theory "HOL.Series" (unresolved "HOL.Inequalities", "HOL.Limits")

Failed to load theory "HOL.NthRoot" (unresolved "HOL.Deriv")

Failed to load theory "HOL.Transcendental" (unresolved "HOL.Deriv", "HOL.NthRoot", "HOL.Series")

Failed to load theory "HOL.Complex" (unresolved "HOL.Real_Vector_Spaces", "HOL.Transcendental")

Failed to load theory "HOL.MacLaurin" (unresolved "HOL.Transcendental")

Failed to load theory "Complex_Main" (unresolved "HOL.Binomial_Plus", "HOL.Complex", "HOL.MacLaurin")

Cheating requires interactive or quick_and_dirty mode!
At command "ML_file" (line 797 of "~~/src/HOL/HOL.thy")

(Isabelle/86a7ec064208)

HOL-Proofs (Isabelle/86a7ec064208)

Pure-ex

Cheating requires interactive or quick_and_dirty mode!
At command "by" (line 16 of "~~/src/Pure/ex/Guess_Examples.thy")

(Isabelle/86a7ec064208)

Failed to load theory "ZF.IntDiv" (unresolved "ZF.Bin")

Failed to load theory "ZF" (unresolved "ZF.IntDiv")

Failed to load theory "ZF.AC" (unresolved "ZF")

Failed to load theory "ZF.Zorn" (unresolved "ZF.AC")

Failed to load theory "ZF.Cardinal_AC" (unresolved "ZF.Zorn")

Failed to load theory "ZF.InfDatatype" (unresolved "ZF.Cardinal_AC")

Failed to load theory "ZFC" (unresolved "ZF", "ZF.InfDatatype")

Cheating requires interactive or quick_and_dirty mode!
At command "ML_file" (line 706 of "~~/src/ZF/Bin.thy")

(Isabelle/86a7ec064208)