by@shell_mug
AC
3941ms
Require Import Io.System.All Io.All List ListString.All Ascii. Import ListNotations C.Notations. Definition j(line:LString.t):ascii:=match line with[_;x;y;_;z;_;_]=>if eqb x y then x else z|_=>"X"%char end. Fixpoint q(n:nat):C.t System.effect unit:=match n with 0=>ret tt|S m=>let! line:=read_line in do!(match line with Some s=>log[j s]|_=>ret tt end)in q m end. Definition main:=Extraction.launch(fun _=>q 32).
318 519 848 588 495 869 589 429 153 558 977 671 687 278 877 172 214 771 194 496 899 338 615 851 719 924 677 787 311 992 233 291 338 831 211 112 541 412 334 344 661 635 693 955 255 918 379 997 926 229 433 393 581 123 466 668 579 899 694 773 616 916 458 885
5 5 8 4 5 7 2 7 7 4 9 8 9 7 1 3 8 1 4 3 6 9 5 9 2 3 1 6 8 7 9 8
ocamlfind ocamldep -package io-system -modules main.ml > main.ml.depends ocamlfind ocamldep -package io-system -modules main.mli > main.mli.depends ocamlfind ocamlc -c -package io-system -o main.cmi main.mli + ocamlfind ocamlc -c -package io-system -o main.cmi main.mli ocamlfind: [WARNING] Package `threads': Linking problems may arise because of the missing -thread or -vmthread switch ocamlfind ocamlopt -c -package io-system -o main.cmx main.ml + ocamlfind ocamlopt -c -package io-system -o main.cmx main.ml ocamlfind: [WARNING] Package `threads': Linking problems may arise because of the missing -thread or -vmthread switch ocamlfind ocamlopt -linkpkg -package io-system main.cmx -o main.native + ocamlfind ocamlopt -linkpkg -package io-system main.cmx -o main.native ocamlfind: [WARNING] Package `threads': Linking problems may arise because of the missing -thread or -vmthread switch
10 execve("/bin/sh", ["/bin/sh", "/root/script", "/volume/CODE"], 0x7ffc0d1253a0 /* 9 vars */) = 0
11 execve("/bin/cat", ["cat", "/volume/CODE", "/root/tail.v"], 0x5605c37e6d60 /* 9 vars */) = 0
11 +++ exited with 0 +++
10 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=11, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
12 execve("/root/.opam/4.10.0/bin/coqc", ["coqc", "Main.v"], 0x5605c37e6cb8 /* 10 vars */) = 0
12 +++ exited with 0 +++
10 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=12, si_uid=0, si_status=0, si_utime=39, si_stime=36} ---
13 execve("/root/.opam/4.10.0/bin/ocamlbuild", ["ocamlbuild", "main.native", "-use-ocamlfind", "-package", "io-system"], 0x5605c3e43100 /* 10 vars */) = 0
14 execve("/bin/sh", ["/bin/sh", "-c", "mkdir /tmp/_build"], 0x7f5798bf5800 /* 10 vars */) = 0
14 execve("/bin/mkdir", ["mkdir", "/tmp/_build"], 0x5623fb464cb0 /* 10 vars */) = 0
14 +++ exited with 0 +++
13 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=14, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
15 execve("/bin/sh", ["/bin/sh", "-c", "camlp4 -where 2>/dev/null"], 0x7ffc8a469788 /* 10 vars */) = 0
15 +++ exited with 127 +++
13 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=15, si_uid=0, si_status=127, si_utime=0, si_stime=0} ---
16 execve("/bin/sh", ["/bin/sh", "-c", "ocamlfind ocamldep -package io-s"...], 0x7f5798bf5860 /* 10 vars */) = 0
16 execve("/root/.opam/4.10.0/bin/ocamlfind", ["ocamlfind", "ocamldep", "-package", "io-system", "-modules", "main.ml"], 0x563afe1c7130 /* 10 vars */) = 0
17 execve("/root/.opam/4.10.0/bin/ocamldep.opt", ["ocamldep.opt", "-modules", "main.ml"], 0x7ffc1df86360 /* 10 vars */) = 0
17 +++ exited with 0 +++
16 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=17, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
16 +++ exited with 0 +++
13 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=16, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
18 execve("/bin/sh", ["/bin/sh", "-c", "ocamlfind ocamldep -package io-s"...], 0x7f5798bf58a0 /* 10 vars */) = 0
18 execve("/root/.opam/4.10.0/bin/ocamlfind", ["ocamlfind", "ocamldep", "-package", "io-system", "-modules", "main.mli"], 0x557386c0c150 /* 10 vars */) = 0
19 execve("/root/.opam/4.10.0/bin/ocamldep.opt", ["ocamldep.opt", "-modules", "main.mli"], 0x7ffc5814dcd0 /* 10 vars */) = 0
19 +++ exited with 0 +++
18 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=19, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
18 +++ exited with 0 +++
13 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=18, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
20 execve("/bin/sh", ["/bin/sh", "-c", "ocamlfind ocamlc -where > /tmp/_"...], 0x7f5798bf5940 /* 10 vars */) = 0
20 execve("/root/.opam/4.10.0/bin/ocamlfind", ["ocamlfind", "ocamlc", "-where"], 0x5610d8ae5028 /* 10 vars */) = 0
21 execve("/root/.opam/4.10.0/bin/ocamlc.opt", ["ocamlc.opt", "-where"], 0x7fff53637a58 /* 10 vars */) = 0
21 +++ exited with 0 +++
20 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=21, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
20 +++ exited with 0 +++
13 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=20, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
22 execve("/bin/sh", ["/bin/sh", "-c", "ocamlfind ocamlc -c -package io-"...], 0x7f5798bf58a0 /* 10 vars */) = 0
22 execve("/root/.opam/4.10.0/bin/ocamlfind", ["ocamlfind", "ocamlc", "-c", "-package", "io-system", "-o", "main.cmi", "main.mli"], 0x5604ce516138 /* 10 vars */) = 0
23 execve("/root/.opam/4.10.0/bin/ocamlc.opt", ["ocamlc.opt", "-c", "-o", "main.cmi", "-I", "/root/.opam/4.10.0/lib/bytes", "-I", "/root/.opam/4.10.0/lib/result", "-I", "/root/.opam/4.10.0/lib/seq", "-I", "/root/.opam/4.10.0/lib/lwt", "-I", "/root/.opam/4.10.0/lib/mmap", "-I", "/root/.opam/4.10.0/lib/ocplib-en"..., "-I", "/root/.opam/4.10.0/lib/ocplib-en"..., "-I", "/root/.opam/4.10.0/lib/lwt/unix", "-I", "/root/.opam/4.10.0/lib/num", "-I", "/root/.opam/4.10.0/lib/io-system", "main.mli"], 0x7ffc4a1876c0 /* 10 vars */) = 0
23 +++ exited with 0 +++
22 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=23, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
22 +++ exited with 0 +++
13 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=22, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
24 execve("/bin/sh", ["/bin/sh", "-c", "ocamlfind ocamlopt -c -package i"...], 0x7f5798bf58a0 /* 10 vars */) = 0
24 execve("/root/.opam/4.10.0/bin/ocamlfind", ["ocamlfind", "ocamlopt", "-c", "-package", "io-system", "-o", "main.cmx", "main.ml"], 0x558db99ee130 /* 10 vars */) = 0
25 execve("/root/.opam/4.10.0/bin/ocamlopt.opt", ["ocamlopt.opt", "-c", "-o", "main.cmx", "-I", "/root/.opam/4.10.0/lib/bytes", "-I", "/root/.opam/4.10.0/lib/result", "-I", "/root/.opam/4.10.0/lib/seq", "-I", "/root/.opam/4.10.0/lib/lwt", "-I", "/root/.opam/4.10.0/lib/mmap", "-I", "/root/.opam/4.10.0/lib/ocplib-en"..., "-I", "/root/.opam/4.10.0/lib/ocplib-en"..., "-I", "/root/.opam/4.10.0/lib/lwt/unix", "-I", "/root/.opam/4.10.0/lib/num", "-I", "/root/.opam/4.10.0/lib/io-system", "main.ml"], 0x7fffe86c4a90 /* 10 vars */) = 0
26 execve("/bin/sh", ["sh", "-c", "as -o 'main.o' '/tmp/camlasm5f5"...], 0x7ffd0b14de18 /* 10 vars */) = 0
26 execve("/usr/bin/as", ["as", "-o", "main.o", "/tmp/camlasm5f5a0e.s"], 0x563414c62028 /* 10 vars */) = 0
26 +++ exited with 0 +++
25 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=26, si_uid=0, si_status=0, si_utime=1, si_stime=0} ---
25 +++ exited with 0 +++
24 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=25, si_uid=0, si_status=0, si_utime=2, si_stime=1} ---
24 +++ exited with 0 +++
13 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=24, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
27 execve("/bin/sh", ["/bin/sh", "-c", "ocamlfind ocamlopt -linkpkg -pac"...], 0x7f5798bf5940 /* 10 vars */) = 0
27 execve("/root/.opam/4.10.0/bin/ocamlfind", ["ocamlfind", "ocamlopt", "-linkpkg", "-package", "io-system", "main.cmx", "-o", "main.native"], 0x5562b420c160 /* 10 vars */) = 0
28 execve("/root/.opam/4.10.0/bin/ocamlopt.opt", ["ocamlopt.opt", "-o", "main.native", "-I", "/root/.opam/4.10.0/lib/bytes", "-I", "/root/.opam/4.10.0/lib/result", "-I", "/root/.opam/4.10.0/lib/seq", "-I", "/root/.opam/4.10.0/lib/lwt", "-I", "/root/.opam/4.10.0/lib/mmap", "-I", "/root/.opam/4.10.0/lib/ocplib-en"..., "-I", "/root/.opam/4.10.0/lib/ocplib-en"..., "-I", "/root/.opam/4.10.0/lib/lwt/unix", "-I", "/root/.opam/4.10.0/lib/num", "-I", "/root/.opam/4.10.0/lib/io-system", "/root/.opam/4.10.0/lib/result/re"..., "/root/.opam/4.10.0/lib/lwt/lwt.c"..., "/root/.opam/4.10.0/lib/ocaml/uni"..., "/root/.opam/4.10.0/lib/ocaml/big"..., "/root/.opam/4.10.0/lib/mmap/mmap"..., "/root/.opam/4.10.0/lib/ocplib-en"..., "/root/.opam/4.10.0/lib/ocplib-en"..., "/root/.opam/4.10.0/lib/lwt/unix/"..., "/root/.opam/4.10.0/lib/ocaml/num"..., ...], 0x7fff452fdd60 /* 10 vars */) = 0
29 execve("/bin/sh", ["sh", "-c", "as -o '/tmp/camlstartupa4e2f3.o"...], 0x7ffed359bbe0 /* 10 vars */) = 0
29 execve("/usr/bin/as", ["as", "-o", "/tmp/camlstartupa4e2f3.o", "/tmp/camlstartup95a13b.s"], 0x55b0f4ba5028 /* 10 vars */) = 0
29 +++ exited with 0 +++
28 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=29, si_uid=0, si_status=0, si_utime=1, si_stime=0} ---
30 execve("/bin/sh", ["sh", "-c", "gcc -O2 -fno-strict-aliasing -fw"...], 0x7ffed359bbe0 /* 10 vars */) = 0
30 execve("/usr/bin/gcc", ["gcc", "-O2", "-fno-strict-aliasing", "-fwrapv", "-Wall", "-fno-common", "-fno-tree-vrp", "-ffunction-sections", "-D_FILE_OFFSET_BITS=64", "-D_REENTRANT", "-DCAML_NAME_SPACE", "-Wl,-E", "-o", "main.native", "-L/root/.opam/4.10.0/lib/bytes", "-L/root/.opam/4.10.0/lib/result", "-L/root/.opam/4.10.0/lib/seq", "-L/root/.opam/4.10.0/lib/lwt", "-L/root/.opam/4.10.0/lib/mmap", "-L/root/.opam/4.10.0/lib/ocplib-"..., "-L/root/.opam/4.10.0/lib/ocplib-"..., "-L/root/.opam/4.10.0/lib/lwt/uni"..., "-L/root/.opam/4.10.0/lib/num", "-L/root/.opam/4.10.0/lib/io-syst"..., "-L/root/.opam/4.10.0/lib/ocaml", "/tmp/camlstartupa4e2f3.o", "/root/.opam/4.10.0/lib/ocaml/std"..., "main.o", "/root/.opam/4.10.0/lib/io-system"..., "/root/.opam/4.10.0/lib/ocaml/num"..., "/root/.opam/4.10.0/lib/lwt/unix/"..., "/root/.opam/4.10.0/lib/ocplib-en"..., ...], 0x55b706a56bb8 /* 10 vars */) = 0
31 execve("/usr/libexec/gcc/x86_64-alpine-linux-musl/9.3.0/collect2", ["/usr/libexec/gcc/x86_64-alpine-l"..., "-plugin", "/usr/libexec/gcc/x86_64-alpine-l"..., "-plugin-opt=/usr/libexec/gcc/x86"..., "-plugin-opt=-fresolution=/tmp/cc"..., "-plugin-opt=-pass-through=-lgcc", "-plugin-opt=-pass-through=-lgcc_"..., "-plugin-opt=-pass-through=-lc", "-plugin-opt=-pass-through=-lgcc", "-plugin-opt=-pass-through=-lgcc_"..., "--eh-frame-hdr", "--hash-style=gnu", "-m", "elf_x86_64", "--as-needed", "-dynamic-linker", "/lib/ld-musl-x86_64.so.1", "-pie", "-z", "relro", "-z", "now", "-o", "main.native", "/usr/lib/gcc/x86_64-alpine-linux"..., "/usr/lib/gcc/x86_64-alpine-linux"..., "/usr/lib/gcc/x86_64-alpine-linux"..., "-L/root/.opam/4.10.0/lib/bytes", "-L/root/.opam/4.10.0/lib/result", "-L/root/.opam/4.10.0/lib/seq", "-L/root/.opam/4.10.0/lib/lwt", "-L/root/.opam/4.10.0/lib/mmap", ...], 0x2330060 /* 15 vars */) = 0
32 execve("/usr/lib/gcc/x86_64-alpine-linux-musl/9.3.0/../../../../x86_64-alpine-linux-musl/bin/ld", ["/usr/lib/gcc/x86_64-alpine-linux"..., "-plugin", "/usr/libexec/gcc/x86_64-alpine-l"..., "-plugin-opt=/usr/libexec/gcc/x86"..., "-plugin-opt=-fresolution=/tmp/cc"..., "-plugin-opt=-pass-through=-lgcc", "-plugin-opt=-pass-through=-lgcc_"..., "-plugin-opt=-pass-through=-lc", "-plugin-opt=-pass-through=-lgcc", "-plugin-opt=-pass-through=-lgcc_"..., "--eh-frame-hdr", "--hash-style=gnu", "-m", "elf_x86_64", "--as-needed", "-dynamic-linker", "/lib/ld-musl-x86_64.so.1", "-pie", "-z", "relro", "-z", "now", "-o", "main.native", "/usr/lib/gcc/x86_64-alpine-linux"..., "/usr/lib/gcc/x86_64-alpine-linux"..., "/usr/lib/gcc/x86_64-alpine-linux"..., "-L/root/.opam/4.10.0/lib/bytes", "-L/root/.opam/4.10.0/lib/result", "-L/root/.opam/4.10.0/lib/seq", "-L/root/.opam/4.10.0/lib/lwt", "-L/root/.opam/4.10.0/lib/mmap", ...], 0x7fff25786378 /* 15 vars */) = 0
32 +++ exited with 0 +++
31 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=32, si_uid=0, si_status=0, si_utime=16, si_stime=42} ---
31 +++ exited with 0 +++
30 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=31, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
30 +++ exited with 0 +++
28 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=30, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
28 +++ exited with 0 +++
27 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=28, si_uid=0, si_status=0, si_utime=5, si_stime=3} ---
27 +++ exited with 0 +++
13 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=27, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
33 execve("/bin/sh", ["sh", "-c", "ln -sf /tmp/_build/main.native /"...], 0x7ffc8a469788 /* 10 vars */) = 0
33 execve("/bin/ln", ["ln", "-sf", "/tmp/_build/main.native", "/tmp"], 0x5652fa51dd60 /* 10 vars */) = 0
33 +++ exited with 0 +++
13 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=33, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
13 +++ exited with 0 +++
10 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=13, si_uid=0, si_status=0, si_utime=2, si_stime=2} ---
34 execve("/bin/cat", ["cat", "-"], 0x5605c37e6d08 /* 10 vars */ <unfinished ...>
35 execve("./main.native", ["./main.native"], 0x5605c37e6cf0 /* 10 vars */ <unfinished ...>
34 <... execve resumed>) = 0
35 <... execve resumed>) = 0
34 +++ exited with 0 +++
10 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=34, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
36 +++ exited with 0 +++
35 +++ exited with 0 +++
10 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=35, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
37 execve("/bin/rm", ["rm", "-rf", "/tmp/Main.glob", "/tmp/Main.v", "/tmp/Main.vo", "/tmp/Main.vok", "/tmp/Main.vos", "/tmp/_build", "/tmp/main.ml", "/tmp/main.mli", "/tmp/main.native"], 0x5605c3e43148 /* 10 vars */) = 0
37 +++ exited with 0 +++
10 --- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=37, si_uid=0, si_status=0, si_utime=0, si_stime=0} ---
10 +++ exited with 0 +++