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/fileYnBG8e.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileZIsdyT.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file0Ms8E1.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filex9UA9g.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileCircDX.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file5wlYsY.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileOXHrUy.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filexgg9Rz.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileIbFTmV.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file2yp7fv.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileQys36X.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")
Compilation with MLton failed: "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-isatest/process5831764205130969062/Code_Test5842782/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/process5831764205130969062/Code_Test5840520/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 763.5-763.25.
Function is not exhaustive.
missing pattern: nil
in: fun hd (x21 :: x22) = x21
Warning: checker.ML 867.5-867.22.
Function is not exhaustive.
missing pattern: NONE
in: fun the (SOME x2) = x2
Warning: checker.ML 1212.5-1212.31.
Function is not exhaustive.
missing pattern: CFOUND | CSUCCESS
in: fun the_error (CFAILED x1) = x1
Warning: checker.ML 1958.5-1958.45.
Function is not exhaustive.
missing pattern: Del _ | Extension _ | Mult _
in: fun pac_src2 (Add (x11, x12, x13, x14)) = x12
Warning: checker.ML 1960.5-1962.26.
Function is not exhaustive.
missing pattern: Extension _
in: fun pac_src1 (Add (x11, x12, x13, ... c_src1 (Del x4) = x4
Warning: checker.ML 1964.5-1964.46.
Function is not exhaustive.
missing pattern: Add _ | Del _ | Extension _
in: fun pac_mult (Mult (x21, x22, x23, x24)) = x22
Warning: checker.ML 1966.5-1968.45.
Function is not exhaustive.
missing pattern: Del _
in: fun pac_res (Add (x11, x12, x13, ... 31, x32, x33)) = x33
Warning: checker.ML 1970.5-1970.45.
Function is not exhaustive.
missing pattern: Add _ | Del _ | Mult _
in: fun new_var (Extension (x31, x32, x33)) = x32
Warning: checker.ML 1985.5-1987.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.67 + 1.41 (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/fileYL4CB3.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileC2SkcN.6.c
cc -c -m64 -o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileFurKXW.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileHupe0u.5.s
cc -c -m64 -o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileVqa8Kq.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filerd364a.4.s
cc -c -m64 -o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file3iS6N0.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filePcHiMJ.3.s
cc -c -m64 -o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileBDIrHK.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file5ovIvY.2.s
cc -c -m64 -o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileJWJq85.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/filer77Wng.1.s
cc -c -m64 -o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileFubPHb.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileEsQfKV.0.s
Compile and Assemble finished in 1.22 + 0.00 (0% GC)
Link starting
cc -o pasteque \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileYL4CB3.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileFurKXW.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileVqa8Kq.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file3iS6N0.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileBDIrHK.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileJWJq85.o \
/var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileFubPHb.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/fileYL4CB3.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileFurKXW.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileVqa8Kq.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/file3iS6N0.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileBDIrHK.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileJWJq85.o /var/folders/xn/wn9y19y126g4j1t1rj3r5cnh0000gr/T/fileFubPHb.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.24 + 0.00 (0% GC)
MLton 20210117 raised in 5.14 + 1.41 (21% GC)
At command "compile_generated_files" (line 19 of "~~/dirs/AFP/thys/PAC_Checker/PAC_Checker_MLton.thy")
Timeout
Compilation with MLton failed: "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-isatest/process16329717637960511229/Code_Test11785612/test.mlb At command "test_code" (line 9 of "~~/src/HOL/Codegenerator_Test/Code_Test_MLton.thy")
Compilation with MLton failed: "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-isatest/process16329717637960511229/Code_Test11785610/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/process16329717637960511229/Code_Test11785608/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/process9517763172667792517/Code_Test7379286/test.mlb At command "test_code" (line 9 of "~~/src/HOL/Codegenerator_Test/Code_Test_MLton.thy")
Compilation with MLton failed: "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-isatest/process9517763172667792517/Code_Test7379284/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/process9517763172667792517/Code_Test7379282/test.mlb At command "test_code" (line 13 of "~~/src/HOL/Codegenerator_Test/Code_Test_MLton.thy")