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")
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")
Timeout
Compilation with MLton failed: "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-isatest/process18031102765245427819/Code_Test5836902/test.mlb At command "test_code" (line 12 of "~~/dirs/AFP/thys/Native_Word/Native_Word_Test_MLton.thy")
Compilation with MLton failed: "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-isatest/process18031102765245427819/Code_Test5834628/test.mlb At command "test_code" (line 12 of "~~/dirs/AFP/thys/Native_Word/Native_Word_Test_MLton2.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.78 + 1.51 (29% 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.21 + 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.27 + 0.00 (0% GC)
MLton 20210117 raised in 5.29 + 1.51 (22% GC)
At command "compile_generated_files" (line 19 of "~~/dirs/AFP/thys/PAC_Checker/PAC_Checker_MLton.thy")
Build failed (line 24 of "~~/src/Tools/Haskell/Test.thy"): Error: [S-7353] Error when running shouldUpgradeCheck: SQLite3 returned ErrorNotFound while attempting to perform step: database disk image is malformed SQLite3 returned ErrorNotFound while attempting to perform step: database disk image is malformed At command "compile_generated_files" (line 11 of "~~/src/Tools/Haskell/Test.thy")
Build failed (line 24 of "~~/src/Tools/Haskell/Test.thy"): Error: [S-7353] Error when running shouldUpgradeCheck: SQLite3 returned ErrorNotFound while attempting to perform step: database disk image is malformed SQLite3 returned ErrorNotFound while attempting to perform step: database disk image is malformed At command "compile_generated_files" (line 11 of "~~/src/Tools/Haskell/Test.thy")
Build failed (line 24 of "~~/src/Tools/Haskell/Test.thy"): Error: [S-7353] Error when running shouldUpgradeCheck: SQLite3 returned ErrorNotFound while attempting to perform step: database disk image is malformed SQLite3 returned ErrorNotFound while attempting to perform step: database disk image is malformed At command "compile_generated_files" (line 11 of "~~/src/Tools/Haskell/Test.thy")
Session startup failed: standard_output terminated /tmp/isabelle-isatest/bash_script5341837735863966834: line 1: 62798 Bus error: 10 "$POLYML_EXE" -q --minheap 1500 --gcthreads 4 --exportstats --eval ' '\ \ \ \ \ \ \ \ \ \ fun\ chapter\ \(_:\ string\)\ \=\ \(\)\;' '\ \ \ \ \ \ \ \ \ \ fun\ section\ \(_:\ string\)\ \=\ \(\)\;' '\ \ \ \ \ \ \ \ \ \ fun\ subsection\ \(_:\ string\)\ \=\ \(\)\;' '\ \ \ \ \ \ \ \ \ \ fun\ subsubsection\ \(_:\ string\)\ \=\ \(\)\;' '\ \ \ \ \ \ \ \ \ \ fun\ paragraph\ \(_:\ string\)\ \=\ \(\)\;' '\ \ \ \ \ \ \ \ \ \ fun\ subparagraph\ \(_:\ string\)\ \=\ \(\)\;' '\ \ \ \ \ \ \ \ \ \ val\ ML_file\ \=\ PolyML.use\;' '\ \ \ \ \ \ \ \ \ \ --eval fun\ exit\ rc\ \=\ Posix.Process.exit\ \(Word8.fromInt\ rc\) --eval PolyML.Compiler.prompt1\ :\=\ \"Poly/ML\>\ \" --eval PolyML.Compiler.prompt2\ :\=\ \"Poly/ML\#\ \" --use ROOT0.ML --use ROOT.ML --eval Command_Line.tool\ \(fn\ \(\)\ \=\>\ \(Isabelle_Process.init_build\ \(\)\;\ ML_Heap.share_common_data\ \(\)\;\ ML_Heap.save_child\ \"/Users/isatest/.isabelle/build_history-mini1/heaps/polyml-5.9.1_x86_64_32-darwin/Pure\"\)\)\; Return code: 127 (COMMAND NOT FOUND)
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")
Compilation with MLton failed: "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-isatest/process11444585004259858410/Code_Test7609498/test.mlb At command "test_code" (line 13 of "~~/src/HOL/Codegenerator_Test/Code_Test_MLton.thy")
Compilation with MLton failed: "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-isatest/process11444585004259858410/Code_Test7609500/test.mlb At command "value" (line 11 of "~~/src/HOL/Codegenerator_Test/Code_Test_MLton.thy")
Compilation with MLton failed: "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-isatest/process11444585004259858410/Code_Test7609502/test.mlb At command "test_code" (line 9 of "~~/src/HOL/Codegenerator_Test/Code_Test_MLton.thy")