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
Compilation failed (line 22 of "~~/dirs/AFP/thys/Buchi_Complementation/Complementation_Build.thy"): Warning: Autool.sml 31.43-31.53. Case is not exhaustive. missing pattern: NONE in: case Int.fromString w of SOME n => n Warning: Autool.sml 124.55-124.92. Case is not exhaustive. missing pattern: NONE in: case TextIO.inputLine input of SO ... (w, 0, size w - 1)) Warning: Autool.sml 126.4-134.45. Case is not exhaustive. missing pattern: :: (("" .. "AO" | "AQ" .. "HO@" | "HOB" .. "namd" | "namf" .. "Stars" | "Staru" .. "Stater" | "Statet" .. "acc-namd" | "acc-namf" .. "Acceptancd" | "Acceptancf" .. "propertier" | "propertiet" ..., :: (_, :: _)) | ("" .. "AO" | "AQ" .. "HO@" | "HOB" .. "namd" | "namf" .. "Stars" | "Staru" .. "Stater" | "Statet" .. "acc-namd" | "acc-namf" .. "Acceptancd" | "Acceptancf" .. "propertier" | "propertiet" ..., nil) | ("AP", :: (_, :: _)) | ("AP", nil) | ("HOA", :: (_, :: _)) | ("HOA", nil) | ("name", :: (_, :: _)) | ("name", nil) | ("Start", :: (_, :: _)) | ("Start", nil) | ("States", :: (_, :: _)) | ("States", nil) | ("acc-name", :: (_, :: _)) | ("acc-name", nil) | ("Acceptance", :: (_, :: _)) | ("Acceptance", nil) | ("properties", :: (_, :: _)) | ("properties", nil)) | nil in: case split ": " w of ["HOA", u] = ... perty (name, value)) Warning: Autool.sml 129.38-129.102. Case is not exhaustive. missing pattern: nil in: case split " " u of v :: vs => (H ... map parseString vs)) Warning: Autool.sml 139.4-139.69. Case is not exhaustive. missing pattern: :: ((_, :: (_, :: _)) | (_, nil)) | nil in: case split "] " (substring (w, 1, ... able u, parseNat v)) Warning: Autool.sml 144.4-146.83. Case is not exhaustive. missing pattern: :: ((_, :: ("" .. "|" | "~" ..., :: _)) | (_, :: ("}", :: _))) | nil in: case split " {" w of [u] => (pars ... v, 0, size v - 1)))) Warning: Autool.sml 148.25-151.29. Case is not exhaustive. missing pattern: :: (("" .. "Statd" | "Statf" ..., _) | ("State", :: (_, :: _)) | ("State", nil)) | nil in: case split ": " w of ["State", u] ... e (p, cs, ts), w'))) Warning: Autool.sml 161.7-162.74. Function is not exhaustive. missing pattern: nil in: fun atomicPropositions (HoaAtomic ... ositions properties) Warning: Autool.sml 164.53-164.66. Case is not exhaustive. missing pattern: Coset _ in: case pow {equal = eq} (Set aps) of Set pps => pps Warning: Autool.sml 176.7-176.15. Declaration is not exhaustive. missing pattern: Coset _ in: val Set nodes = sup_seta {equal = ... bot_set))) (Set t)) Warning: Autool.sml 209.2-237.61. Case is not exhaustive. missing pattern: "" .. "helo" | "helq" .. "parsd" | "parsf" .. "producs" | "producu" .. "complemens" | "complemenu" .. "equivalencd" | "equivalencf" .. "complement_quicj" | "complement_quicl" ... in: case hd parameters of "help" => ( ... aton aps nbaei)) end ld: warning: disabling chained fixups because of unaligned pointers ld: illegal text-relocation in '___gmpn_modexact_1_odd'+0xC (/Users/isatest/.isabelle/contrib/mlton-20210117-3/x86_64-darwin/lib/mlton/targets/self/libgmp.a[312](mode1o.o)) to '___gmp_binvert_limb_table' clang: error: linker command failed with exit code 1 (use -v to see invocation) MLton 20210117 raised: Fail: call to system failed with Fail: exit status 1: cc -o Autool /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file6I4WyB.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file96aBFp.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filezsKqmA.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filec72ux0.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileyZ0jQD.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileSWcT8q.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileEPIr7W.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filede4fW2.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file4jMceC.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileMVvJ6x.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileycLWAI.o -L/Users/isatest/.isabelle/contrib/mlton-20210117-3/x86_64-darwin/lib/mlton/targets/self -lmlton -lgdtoa -lm -lgmp -m64 -arch x86_64 At command "compile_generated_files" (line 11 of "~~/dirs/AFP/thys/Buchi_Complementation/Complementation_Build.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 5 of "~~/dirs/AFP/thys/CakeML/Tests/Code_Test_Haskell.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 90 of "~~/dirs/AFP/thys/Collections/ICF/tools/Locale_Code_Ex.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 1095 of "~~/dirs/AFP/thys/Collections/Lib/Diff_Array.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 14 of "~~/dirs/AFP/thys/Diophantine_Eqns_Lin_Hom/Solver_Code.thy")
Failed to load theory "Factored_Transition_System_Bounding.FactoredSystemLib" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "Factored_Transition_System_Bounding.FmapUtils" (unresolved "Factored_Transition_System_Bounding.FactoredSystemLib", "HOL-Library.Finite_Map")
Failed to load theory "Factored_Transition_System_Bounding.FactoredSystem" (unresolved "Factored_Transition_System_Bounding.FactoredSystemLib", "Factored_Transition_System_Bounding.FmapUtils", "HOL-Library.Finite_Map")
Failed to load theory "Factored_Transition_System_Bounding.ActionSeqProcess" (unresolved "Factored_Transition_System_Bounding.FactoredSystem", "Factored_Transition_System_Bounding.FactoredSystemLib")
Failed to load theory "Factored_Transition_System_Bounding.Dependency" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.FactoredSystem", "HOL-Library.Finite_Map")
Failed to load theory "Factored_Transition_System_Bounding.Invariants" (unresolved "Factored_Transition_System_Bounding.FactoredSystem")
Failed to load theory "Factored_Transition_System_Bounding.TopologicalProps" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.FactoredSystem")
Failed to load theory "Factored_Transition_System_Bounding.SystemAbstraction" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.Dependency", "Factored_Transition_System_Bounding.FactoredSystem", "Factored_Transition_System_Bounding.FactoredSystemLib", "Factored_Transition_System_Bounding.FmapUtils", "Factored_Transition_System_Bounding.TopologicalProps", "HOL-Library.Finite_Map")
Failed to load theory "Factored_Transition_System_Bounding.AcycSspace" (unresolved "Factored_Transition_System_Bounding.ActionSeqProcess", "Factored_Transition_System_Bounding.FactoredSystem", "Factored_Transition_System_Bounding.FmapUtils", "Factored_Transition_System_Bounding.SystemAbstraction")
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 1408 of "~~/src/HOL/Library/Finite_Map.thy")
Failed to load theory "Finite-Map-Extras.Finite_Map_Extras" (unresolved "HOL-Library.Finite_Map")
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 1408 of "~~/src/HOL/Library/Finite_Map.thy")
Failed to load theory "Gale_Shapley.Gale_Shapley2" (unresolved "Collections.Diff_Array")
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 1095 of "~~/dirs/AFP/thys/Collections/Lib/Diff_Array.thy")
Unknown statement name: "Code_Numeral.Neg" At command "export_code" (line 12 of "~~/dirs/AFP/thys/Go/test/slow/Generate_Binary_Nat.thy")
Unknown statement name: "Code_Numeral.Neg" At command "export_code" (line 19 of "~~/dirs/AFP/thys/Go/test/slow/Generate.thy")
Failed to load theory "Collections.Impl_Array_Stack" (unresolved "Collections.Diff_Array")
Failed to load theory "Collections.Array_Iterator" (unresolved "Collections.Diff_Array")
Failed to load theory "Collections.Impl_Array_Map" (unresolved "Collections.Diff_Array")
Failed to load theory "Collections.Impl_Array_Hash_Map" (unresolved "Collections.Array_Iterator", "Collections.Diff_Array")
Failed to load theory "HOL-ODE-Numerics.GenCF_No_Comp" (unresolved "Collections.Impl_Array_Hash_Map", "Collections.Impl_Array_Map", "Collections.Impl_Array_Stack", "Collections.Impl_Uv_Set")
Failed to load theory "HOL-ODE-Numerics.Refine_Dflt_No_Comp" (unresolved "HOL-ODE-Numerics.GenCF_No_Comp")
Failed to load theory "HOL-ODE-Numerics.Autoref_Misc" (unresolved "HOL-ODE-Numerics.Refine_Dflt_No_Comp")
Failed to load theory "HOL-ODE-Numerics.Refine_Folds" (unresolved "HOL-ODE-Numerics.Autoref_Misc")
Failed to load theory "HOL-ODE-Numerics.Refine_String" (unresolved "HOL-ODE-Numerics.Autoref_Misc")
Failed to load theory "HOL-ODE-Numerics.Weak_Set" (unresolved "HOL-ODE-Numerics.Autoref_Misc")
Failed to load theory "HOL-ODE-Numerics.Refine_Parallel" (unresolved "HOL-ODE-Numerics.Autoref_Misc", "HOL-ODE-Numerics.Weak_Set")
Failed to load theory "HOL-ODE-Numerics.Enclosure_Operations" (unresolved "HOL-ODE-Numerics.Autoref_Misc")
Failed to load theory "HOL-ODE-Numerics.Refine_Default" (unresolved "HOL-ODE-Numerics.Enclosure_Operations", "HOL-ODE-Numerics.Weak_Set")
Failed to load theory "HOL-ODE-Numerics.Refine_Unions" (unresolved "HOL-ODE-Numerics.Enclosure_Operations", "HOL-ODE-Numerics.Weak_Set")
Failed to load theory "HOL-ODE-Numerics.Refine_Intersection" (unresolved "HOL-ODE-Numerics.Refine_Unions")
Failed to load theory "HOL-ODE-Numerics.Refine_Invar" (unresolved "HOL-ODE-Numerics.Refine_Intersection", "HOL-ODE-Numerics.Refine_Unions")
Failed to load theory "HOL-ODE-Numerics.Refine_Phantom" (unresolved "HOL-ODE-Numerics.Autoref_Misc", "HOL-ODE-Numerics.Refine_Unions")
Failed to load theory "HOL-ODE-Numerics.Refine_Vector_List" (unresolved "HOL-ODE-Numerics.Autoref_Misc", "HOL-ODE-Numerics.Enclosure_Operations", "HOL-ODE-Numerics.Weak_Set")
Failed to load theory "HOL-ODE-Numerics.Refine_Info" (unresolved "HOL-ODE-Numerics.Refine_Unions", "HOL-ODE-Numerics.Refine_Vector_List")
Failed to load theory "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector" (unresolved "HOL-ODE-Numerics.Refine_Vector_List")
Failed to load theory "HOL-ODE-Numerics.Refine_Hyperplane" (unresolved "HOL-ODE-Numerics.Autoref_Misc", "HOL-ODE-Numerics.Refine_Vector_List")
Failed to load theory "HOL-ODE-Numerics.Refine_Interval" (unresolved "HOL-ODE-Numerics.Refine_Hyperplane", "HOL-ODE-Numerics.Refine_Invar", "HOL-ODE-Numerics.Refine_Unions", "HOL-ODE-Numerics.Refine_Vector_List")
Failed to load theory "HOL-ODE-Numerics.Abstract_Rigorous_Numerics" (unresolved "HOL-ODE-Numerics.Enclosure_Operations", "HOL-ODE-Numerics.Refine_Hyperplane", "HOL-ODE-Numerics.Refine_Info", "HOL-ODE-Numerics.Refine_Interval", "HOL-ODE-Numerics.Refine_Invar", "HOL-ODE-Numerics.Refine_Unions", "HOL-ODE-Numerics.Refine_Vector_List", "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector")
Failed to load theory "HOL-ODE-Numerics.Concrete_Rigorous_Numerics" (unresolved "HOL-ODE-Numerics.Abstract_Rigorous_Numerics")
Failed to load theory "HOL-ODE-Numerics.Refine_Rigorous_Numerics" (unresolved "HOL-ODE-Numerics.Abstract_Rigorous_Numerics")
Failed to load theory "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform" (unresolved "HOL-ODE-Numerics.Refine_Rigorous_Numerics")
Failed to load theory "HOL-ODE-Numerics.Refine_ScaleR2" (unresolved "HOL-ODE-Numerics.Refine_Interval", "HOL-ODE-Numerics.Refine_String", "HOL-ODE-Numerics.Refine_Unions")
Failed to load theory "HOL-ODE-Numerics.Abstract_Reachability_Analysis" (unresolved "HOL-ODE-Numerics.Abstract_Rigorous_Numerics", "HOL-ODE-Numerics.Refine_Folds", "HOL-ODE-Numerics.Refine_String")
Failed to load theory "HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1" (unresolved "HOL-ODE-Numerics.Abstract_Reachability_Analysis", "HOL-ODE-Numerics.Refine_Default", "HOL-ODE-Numerics.Refine_Parallel", "HOL-ODE-Numerics.Refine_Phantom", "HOL-ODE-Numerics.Refine_ScaleR2", "HOL-ODE-Numerics.Weak_Set")
Failed to load theory "HOL-ODE-Numerics.Concrete_Reachability_Analysis" (unresolved "HOL-ODE-Numerics.Abstract_Reachability_Analysis", "HOL-ODE-Numerics.Concrete_Rigorous_Numerics")
Failed to load theory "HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1" (unresolved "HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1", "HOL-ODE-Numerics.Concrete_Reachability_Analysis")
Failed to load theory "HOL-ODE-Numerics.Refine_Reachability_Analysis" (unresolved "HOL-ODE-Numerics.Abstract_Reachability_Analysis", "HOL-ODE-Numerics.Refine_Rigorous_Numerics")
Failed to load theory "HOL-ODE-Numerics.Refine_Reachability_Analysis_C1" (unresolved "HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1", "HOL-ODE-Numerics.Refine_Reachability_Analysis")
Failed to load theory "HOL-ODE-Numerics.Init_ODE_Solver" (unresolved "HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1", "HOL-ODE-Numerics.Refine_Reachability_Analysis_C1", "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform")
Failed to load theory "HOL-ODE-Numerics.Example_Utilities" (unresolved "HOL-ODE-Numerics.Init_ODE_Solver")
Failed to load theory "HOL-ODE-Numerics.ODE_Numerics" (unresolved "HOL-ODE-Numerics.Example_Utilities", "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform", "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector")
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 384 of "~~/dirs/AFP/thys/Collections/GenCF/Impl/Impl_Uv_Set.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 1095 of "~~/dirs/AFP/thys/Collections/Lib/Diff_Array.thy")
Failed to load theory "Hello_World.HelloWorld_Proof" (unresolved "Hello_World.HelloWorld")
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 27 of "~~/dirs/AFP/thys/Hello_World/HelloWorld.thy")
Failed to load theory "Higher_Order_Terms.Term_Utils" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "Higher_Order_Terms.Find_First" (unresolved "HOL-Library.Finite_Map")
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 1408 of "~~/src/HOL/Library/Finite_Map.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 32 of "~~/dirs/AFP/thys/Iptables_Semantics/Code_haskell.thy")
Failed to load theory "LL1_Parser.First_Map" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "LL1_Parser.Follow_Map" (unresolved "LL1_Parser.First_Map")
Failed to load theory "LL1_Parser.Parse_Table" (unresolved "LL1_Parser.Follow_Map")
Failed to load theory "LL1_Parser.LL1_Parser" (unresolved "LL1_Parser.Parse_Table")
Failed to load theory "LL1_Parser.LL1_Parser_show" (unresolved "LL1_Parser.LL1_Parser")
Failed to load theory "LL1_Parser.Json_Parser" (unresolved "LL1_Parser.LL1_Parser_show")
Failed to load theory "LL1_Parser.Parser_Example" (unresolved "LL1_Parser.LL1_Parser_show")
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 1408 of "~~/src/HOL/Library/Finite_Map.thy")
Failed to load theory "LambdaAuth.FMap_Lemmas" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "LambdaAuth.Semantics" (unresolved "LambdaAuth.FMap_Lemmas")
Failed to load theory "LambdaAuth.Agreement" (unresolved "LambdaAuth.Semantics")
Failed to load theory "LambdaAuth.Results" (unresolved "LambdaAuth.Agreement")
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 1408 of "~~/src/HOL/Library/Finite_Map.thy")
Failed to load theory "Native_Word.Native_Word_Test_Emu" (unresolved "Native_Word.Native_Word_Test")
Failed to load theory "Native_Word.Native_Word_Test_PolyML2" (unresolved "Native_Word.Native_Word_Test_Emu")
Failed to load theory "Native_Word.Native_Word_Test_PolyML" (unresolved "Native_Word.Native_Word_Test")
Failed to load theory "Native_Word.Native_Word_Test_PolyML64" (unresolved "Native_Word.Native_Word_Test")
Failed to load theory "Native_Word.Native_Word_Test_Scala" (unresolved "Native_Word.Native_Word_Test")
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 54 of "~~/dirs/AFP/thys/Native_Word/Native_Word_Test.thy")
Compilation failed (line 28 of "~~/dirs/AFP/thys/PAC_Checker/PAC_Checker_MLton.thy"): MLton 20210117 starting Compile SML starting Warning: checker.ML 781.5-781.25. Function is not exhaustive. missing pattern: nil in: fun hd (x21 :: x22) = x21 Warning: checker.ML 885.5-885.22. Function is not exhaustive. missing pattern: NONE in: fun the (SOME x2) = x2 Warning: checker.ML 1230.5-1230.31. Function is not exhaustive. missing pattern: CFOUND | CSUCCESS in: fun the_error (CFAILED x1) = x1 Warning: checker.ML 1976.5-1976.45. Function is not exhaustive. missing pattern: Del _ | Extension _ | Mult _ in: fun pac_src2 (Add (x11, x12, x13, x14)) = x12 Warning: checker.ML 1978.5-1980.26. Function is not exhaustive. missing pattern: Extension _ in: fun pac_src1 (Add (x11, x12, x13, ... c_src1 (Del x4) = x4 Warning: checker.ML 1982.5-1982.46. Function is not exhaustive. missing pattern: Add _ | Del _ | Extension _ in: fun pac_mult (Mult (x21, x22, x23, x24)) = x22 Warning: checker.ML 1984.5-1986.45. Function is not exhaustive. missing pattern: Del _ in: fun pac_res (Add (x11, x12, x13, ... 31, x32, x33)) = x33 Warning: checker.ML 1988.5-1988.45. Function is not exhaustive. missing pattern: Add _ | Del _ | Mult _ in: fun new_var (Extension (x31, x32, x33)) = x32 Warning: checker.ML 2003.5-2005.44. Function is not exhaustive. missing pattern: Del _ in: fun new_id (Add (x11, x12, x13, x ... 31, x32, x33)) = x31 Warning: parser.sml 275.13-282.91. Case is not exhaustive. missing pattern: NONE in: case TextIO.input1 istream of SOM ... implode [c] ^ "'"))) Warning: pasteque.sml 96.5-132.7. Function is not exhaustive. missing pattern: :: ((_, :: (_, :: (_, :: _))) | (_, :: (_, nil)) | (_, nil)) | nil in: fun inside_loop [polys, pac, spec ... ssing full in () end Warning: pasteque.sml 134.5-160.82. Function is not exhaustive. missing pattern: :: ((_, :: (_, :: (_, :: _))) | (_, :: (_, nil)) | (_, nil)) | nil in: fun checker [polys, pac, spec] = ... th error: " ^ err))) Warning: pasteque.sml 162.5-172.34. Function is not exhaustive. missing pattern: :: ((_, :: (_, :: (_, :: (_, :: _)))) | (_, :: (_, nil))) in: fun process_args [arg, polys, pac ... [] = (print_help ()) Compile SML finished in 3.72 + 1.46 (28% GC) Compile and Assemble starting cc -c \ -I/Users/isatest/.isabelle/contrib/mlton-20210117-3/x86_64-darwin/lib/mlton/targets/self/include \ -std=gnu11 -fno-common -O1 -fno-strict-aliasing \ -foptimize-sibling-calls -w \ -I/Users/isatest/.isabelle/contrib/mlton-20210117-3/x86_64-darwin/lib/mlton/include \ -m64 -arch x86_64 -O3 -o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileQfRXyQ.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filev8tF7S.6.c cc -c -m64 -o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filebqst7w.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file2r0DSf.5.s cc -c -m64 -o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileiXR2gG.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileAQl4Y7.4.s cc -c -m64 -o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileWbWmjN.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileIneSLS.3.s cc -c -m64 -o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file1KP90M.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filenG2tfk.2.s cc -c -m64 -o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileL2vz5J.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filelEeJq3.1.s cc -c -m64 -o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileBEYIHl.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileuqfOUP.0.s Compile and Assemble finished in 1.15 + 0.00 (0% GC) Link starting cc -o pasteque \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileQfRXyQ.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filebqst7w.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileiXR2gG.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileWbWmjN.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file1KP90M.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileL2vz5J.o \ /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileBEYIHl.o \ -L/Users/isatest/.isabelle/contrib/mlton-20210117-3/x86_64-darwin/lib/mlton/targets/self \ -lmlton -lgdtoa -lm -lgmp -m64 -arch x86_64 ld: warning: disabling chained fixups because of unaligned pointers ld: illegal text-relocation in '___gmpn_modexact_1_odd'+0xC (/Users/isatest/.isabelle/contrib/mlton-20210117-3/x86_64-darwin/lib/mlton/targets/self/libgmp.a[312](mode1o.o)) to '___gmp_binvert_limb_table' clang: error: linker command failed with exit code 1 (use -v to see invocation) Link raised: Fail: call to system failed with Fail: exit status 1: cc -o pasteque /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileQfRXyQ.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filebqst7w.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileiXR2gG.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileWbWmjN.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file1KP90M.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileL2vz5J.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileBEYIHl.o -L/Users/isatest/.isabelle/contrib/mlton-20210117-3/x86_64-darwin/lib/mlton/targets/self -lmlton -lgdtoa -lm -lgmp -m64 -arch x86_64 Link raised in 0.23 + 0.00 (0% GC) MLton 20210117 raised in 5.12 + 1.46 (22% GC) At command "compile_generated_files" (line 19 of "~~/dirs/AFP/thys/PAC_Checker/PAC_Checker_MLton.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 279 of "~~/dirs/AFP/thys/Prim_Dijkstra_Simple/Dijkstra_Impl.thy")
Failed to load theory "Top_Down_Solver.Basics" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "Top_Down_Solver.TD_plain" (unresolved "Top_Down_Solver.Basics")
Failed to load theory "Top_Down_Solver.TD_equiv" (unresolved "HOL-Library.Finite_Map", "Top_Down_Solver.Basics", "Top_Down_Solver.TD_plain")
Failed to load theory "Top_Down_Solver.Example" (unresolved "Top_Down_Solver.TD_equiv", "Top_Down_Solver.TD_plain")
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 1408 of "~~/src/HOL/Library/Finite_Map.thy")
Failed to load theory "Polynomials.Poly_Mapping_Finite_Map" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "Polynomials.MPoly_Type_Class_FMap" (unresolved "Polynomials.Poly_Mapping_Finite_Map")
Failed to load theory "Virtual_Substitution.MPolyExtension" (unresolved "Polynomials.MPoly_Type_Class_FMap")
Failed to load theory "Virtual_Substitution.ExecutiblePolyProps" (unresolved "Virtual_Substitution.MPolyExtension")
Failed to load theory "Virtual_Substitution.PolyAtoms" (unresolved "Virtual_Substitution.ExecutiblePolyProps")
Failed to load theory "Virtual_Substitution.Debruijn" (unresolved "Virtual_Substitution.PolyAtoms")
Failed to load theory "Virtual_Substitution.Optimizations" (unresolved "Virtual_Substitution.Debruijn")
Failed to load theory "Virtual_Substitution.OptimizationProofs" (unresolved "Virtual_Substitution.Optimizations")
Failed to load theory "Virtual_Substitution.Reindex" (unresolved "Virtual_Substitution.Debruijn")
Failed to load theory "Virtual_Substitution.UniAtoms" (unresolved "Virtual_Substitution.Debruijn")
Failed to load theory "Virtual_Substitution.VSAlgos" (unresolved "Virtual_Substitution.Debruijn", "Virtual_Substitution.Optimizations")
Failed to load theory "Virtual_Substitution.DNF" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.Heuristic" (unresolved "Virtual_Substitution.Optimizations", "Virtual_Substitution.Reindex", "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.LinearCase" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.NegInfinity" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.QuadraticCase" (unresolved "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.EliminateVariable" (unresolved "Virtual_Substitution.LinearCase", "Virtual_Substitution.QuadraticCase")
Failed to load theory "Virtual_Substitution.LuckyFind" (unresolved "Virtual_Substitution.EliminateVariable")
Failed to load theory "Virtual_Substitution.EqualityVS" (unresolved "Virtual_Substitution.EliminateVariable", "Virtual_Substitution.LuckyFind")
Failed to load theory "Virtual_Substitution.Infinitesimals" (unresolved "Virtual_Substitution.Debruijn", "Virtual_Substitution.ExecutiblePolyProps", "Virtual_Substitution.LinearCase", "Virtual_Substitution.NegInfinity", "Virtual_Substitution.QuadraticCase")
Failed to load theory "Virtual_Substitution.QE" (unresolved "Polynomials.MPoly_Type_Class_FMap")
Failed to load theory "Virtual_Substitution.NegInfinityUni" (unresolved "Virtual_Substitution.NegInfinity", "Virtual_Substitution.QE", "Virtual_Substitution.UniAtoms")
Failed to load theory "Virtual_Substitution.InfinitesimalsUni" (unresolved "Virtual_Substitution.Infinitesimals", "Virtual_Substitution.NegInfinityUni", "Virtual_Substitution.QE", "Virtual_Substitution.UniAtoms")
Failed to load theory "Virtual_Substitution.DNFUni" (unresolved "Virtual_Substitution.InfinitesimalsUni", "Virtual_Substitution.QE")
Failed to load theory "Virtual_Substitution.GeneralVSProofs" (unresolved "Virtual_Substitution.DNFUni", "Virtual_Substitution.EqualityVS", "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.VSQuad" (unresolved "Virtual_Substitution.DNF", "Virtual_Substitution.EqualityVS", "Virtual_Substitution.GeneralVSProofs", "Virtual_Substitution.OptimizationProofs", "Virtual_Substitution.Reindex")
Failed to load theory "Virtual_Substitution.HeuristicProofs" (unresolved "Virtual_Substitution.Heuristic", "Virtual_Substitution.OptimizationProofs", "Virtual_Substitution.VSQuad")
Failed to load theory "Virtual_Substitution.PrettyPrinting" (unresolved "Virtual_Substitution.ExecutiblePolyProps", "Virtual_Substitution.PolyAtoms")
Failed to load theory "Virtual_Substitution.Exports" (unresolved "Virtual_Substitution.Heuristic", "Virtual_Substitution.Optimizations", "Virtual_Substitution.PrettyPrinting", "Virtual_Substitution.VSAlgos")
Failed to load theory "Virtual_Substitution.ExportProofs" (unresolved "Virtual_Substitution.Exports", "Virtual_Substitution.HeuristicProofs", "Virtual_Substitution.PrettyPrinting")
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 1408 of "~~/src/HOL/Library/Finite_Map.thy")
Timeout
Compilation with MLton failed: "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-isatest/process14686978319500303004/Code_Test12061912/test.mlb At command "test_code" (line 12 of "~~/src/HOL/Codegenerator_Test/Generate_Target_MLton.thy")
Compilation with MLton failed: "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-isatest/process14686978319500303004/Code_Test12061910/test.mlb At command "test_code" (line 11 of "~~/src/HOL/Codegenerator_Test/Generate_Target_MLton.thy")