Timeout
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")
Timeout
Timeout
Timeout
Failed to load theory "Padic_Field.Padic_Semialgebraic_Function_Ring" (unresolved "Padic_Field.Padic_Field_Powers")
SMT: Solver "z3": Timed out (setting the configuration option "smt_timeout" might help) At command "by" (line 9415 of "~~/dirs/AFP/thys/Padic_Field/Padic_Field_Powers.thy")
Timeout
Timeout
Timeout
Timeout
Timeout
Timeout
Timeout
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")
Timeout
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")
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")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script3877228334983720296: 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_script18051411695846149685: 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_script7477673180095385479: 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_script11156497623781455937: 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_script16975052744472559754: 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")
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")
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")
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")
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")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script3902328824184623931: 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_script8035118934928437781: 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_script8518149844003184428: 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_script3160115860233024687: 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_script10590459108839856510: 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_script14249290962309809307: 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_script12202322518726601335: 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_script11790246183726990027: 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_script10116064203568597894: 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_script13439223444447561694: 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_script10747183404151527563: 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_script11770728146313785809: 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_script326958744259956105: 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_script8380620745734091954: 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_script7923390794685531852: 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_script17781267726455370589: 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_script139048863202613846: 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_script13799108641657214982: 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_script10174278075350485907: 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_script11064183469894801779: 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_script6165209113302214147: 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_script5229391078190561647: 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_script15271015298753206892: 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_script11256772814357247533: 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_script1669684453845027080: 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")
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")
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")
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")
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")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script2848822390742239836: 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_script213212475485510281: 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_script14041634066244242157: 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_script10990755602532873324: 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_script18144612108196806967: 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_script13979980040045435118: 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_script13044497719917137944: 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_script17680560199976718980: 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_script1501363518285574465: 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_script13259340423945711250: 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_script1482805774427350735: 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_script9174008854873114733: 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_script3570514308947307898: 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_script2114893928641921911: 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_script15772763644903133850: 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_script13244016805185356571: 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_script10489261704657525973: 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_script7795144808564398244: 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_script16677634650624808292: 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_script14994659531770567221: 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_script11469651344421345479: 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_script14064323997042286438: 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_script13422156560592050334: 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_script3920299001829640934: 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_script4314747104942610842: 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")
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")
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")
Code check failed for Haskell: "$ISABELLE_GHC" -XEmptyDataDecls -XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e "" Generated_Code.hs At command "export_code" (line 39 of "~~/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy")
Code check failed for Haskell: "$ISABELLE_GHC" -XEmptyDataDecls -XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e "" Generated_Code.hs At command "export_code" (line 17 of "~~/src/HOL/Codegenerator_Test/Generate_Abstract_Char.thy")
Code check failed for Haskell: "$ISABELLE_GHC" -XEmptyDataDecls -XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e "" Generated_Code.hs At command "export_code" (line 18 of "~~/src/HOL/Codegenerator_Test/Generate.thy")
Session startup failed: standard_output terminated Assertion failed: (0), function RelocateAddress, file savestate.cpp, line 1022. /tmp/isabelle-isatest/bash_script14843863795510564366: line 1: 64845 Abort trap: 6 /Users/isatest/.isabelle/contrib/polyml-5.9.1-1/x86_64_32-darwin/poly -q --minheap 1500 --gcthreads 4 --exportstats --eval \(PolyML.SaveState.loadHierarchy\ \[\"/Users/isatest/.isabelle/build_history-mini2-sonoma_1/heaps/polyml-5.9.1_x86_64_32-darwin/Pure\",\ \"/Users/isatest/.isabelle/build_history-mini2-sonoma_1/heaps/polyml-5.9.1_x86_64_32-darwin/HOL\"\]\;\ PolyML.print_depth\ 0\) --eval Options.load_default\ \(\) --eval Resources.init_session_env\ \(\) --eval Command_Line.tool\ \(fn\ \(\)\ \=\>\ \(Isabelle_Process.init_build\ \(\)\)\)\; Return code: 127 (COMMAND NOT FOUND)
Session startup failed: standard_output terminated Assertion failed: (0), function RelocateAddress, file savestate.cpp, line 1022. /tmp/isabelle-isatest/bash_script13163660010559584052: line 1: 67218 Abort trap: 6 /Users/isatest/.isabelle/contrib/polyml-5.9.1-1/x86_64_32-darwin/poly -q --minheap 1500 --gcthreads 4 --exportstats --eval \(PolyML.SaveState.loadHierarchy\ \[\"/Users/isatest/.isabelle/build_history-mini2-sonoma_2/heaps/polyml-5.9.1_x86_64_32-darwin/Pure\",\ \"/Users/isatest/.isabelle/build_history-mini2-sonoma_2/heaps/polyml-5.9.1_x86_64_32-darwin/HOL\"\]\;\ PolyML.print_depth\ 0\) --eval Options.load_default\ \(\) --eval Resources.init_session_env\ \(\) --eval Command_Line.tool\ \(fn\ \(\)\ \=\>\ \(Isabelle_Process.init_build\ \(\)\)\)\; Return code: 127 (COMMAND NOT FOUND)
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")
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.Quotient" (unresolved "HOL.Lifting")
Failed to load theory "HOL.Option" (unresolved "HOL.Lifting")
Failed to load theory "HOL.Power" (unresolved "HOL.Num")
Failed to load theory "HOL.Extraction" (unresolved "HOL.Option")
Failed to load theory "HOL.Partial_Function" (unresolved "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")
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.SMT" (unresolved "HOL.Numeral_Simprocs")
Failed to load theory "HOL.Semiring_Normalization" (unresolved "HOL.Numeral_Simprocs")
Failed to load theory "HOL.Groebner_Basis" (unresolved "HOL.Parity", "HOL.Semiring_Normalization")
Failed to load theory "HOL.Set_Interval" (unresolved "HOL.Parity")
Failed to load theory "HOL.Presburger" (unresolved "HOL.Groebner_Basis", "HOL.Set_Interval")
Failed to load theory "HOL.Conditionally_Complete_Lattices" (unresolved "HOL.Lattices_Big", "HOL.Set_Interval")
Failed to load theory "HOL.Filter" (unresolved "HOL.Lifting_Set", "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.Factorial" (unresolved "HOL.Groups_List")
Failed to load theory "HOL.Bit_Operations" (unresolved "HOL.Groups_List", "HOL.Presburger")
Failed to load theory "HOL.Enum" (unresolved "HOL.Groups_List", "HOL.Map")
Failed to load theory "HOL.Binomial" (unresolved "HOL.Factorial", "HOL.Presburger")
Failed to load theory "HOL.Code_Numeral" (unresolved "HOL.Bit_Operations", "HOL.Lifting")
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.Random" (unresolved "HOL.Code_Numeral", "HOL.Groups_List", "HOL.List")
Failed to load theory "HOL.BNF_Greatest_Fixpoint" (unresolved "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.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.Random_Sequence" (unresolved "HOL.Random_Pred")
Failed to load theory "HOL.Nitpick" (unresolved "HOL.GCD", "HOL.Record")
Failed to load theory "HOL.Predicate_Compile" (unresolved "HOL.Quickcheck_Exhaustive", "HOL.Random_Sequence")
Failed to load theory "HOL.Nunchaku" (unresolved "HOL.Nitpick")
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-Library.Realizers" (unresolved "Main")
Exception- Fail
"Exception- Option unexpectedly raised while compiling" raised
At command "ML_file" (line 194 of "~~/src/HOL/BNF_Least_Fixpoint.thy")