this derivation will be built: /nix/store/c0v240j4c6jr2x8n6kivgnn9vjj4a9h5-coq8.16-compcert-3.11.drv these 4 paths will be fetched (185.7 MiB download, 823.7 MiB unpacked): /nix/store/f7bj3ac2bysmkgd7amnczz8gnpjavigz-blas-3 /nix/store/xhrf5cq7cil1p3q34j5q2300mqx69pwd-coq-8.16.1 /nix/store/igq0rs00wdhj0hrjr16h82ffzw9h0ids-csdp-6.1.1 /nix/store/69lvvsk8wpxgn5a4zypc8zkkcqyslfhh-lapack-3 building '/nix/store/c0v240j4c6jr2x8n6kivgnn9vjj4a9h5-coq8.16-compcert-3.11.drv' coq8.16-compcert-3.11> unpacking sources coq8.16-compcert-3.11> unpacking source archive /nix/store/xi10sd06bx32jymiysgy8c22hlza00f7-source coq8.16-compcert-3.11> source root is source coq8.16-compcert-3.11> patching sources coq8.16-compcert-3.11> applying patch /nix/store/1616cywlq5w00z46yy64kjxbixv2h5d5-34be08a23d18d56f2dde24fd24b6dbe3bcb01ec3.patch coq8.16-compcert-3.11> patching file configure coq8.16-compcert-3.11> applying patch /nix/store/mqzbgy1gj4zy0rd0mjqsqnkaxk2q68gz-35531503b3493cb9b0ec8a8585e84928c85b4af9.patch coq8.16-compcert-3.11> patching file configure coq8.16-compcert-3.11> configuring coq8.16-compcert-3.11> Testing assembler support for CFI directives... yes coq8.16-compcert-3.11> Testing linker support for '-no-pie' / '-nopie' option... yes, '-no-pie' coq8.16-compcert-3.11> Testing Coq... version 8.16.1 -- good! coq8.16-compcert-3.11> Testing OCaml... version 4.14.0 -- good! coq8.16-compcert-3.11> Testing OCaml native-code compiler... yes coq8.16-compcert-3.11> Testing OCaml .opt compilers... yes coq8.16-compcert-3.11> Testing Menhir... version 20220210 -- good! coq8.16-compcert-3.11> Testing GNU make... version 4.4 (command 'make') -- good! coq8.16-compcert-3.11> coq8.16-compcert-3.11> CompCert configuration: coq8.16-compcert-3.11> Target architecture........... x86 coq8.16-compcert-3.11> Hardware model................ 64 coq8.16-compcert-3.11> Application binary interface.. standard coq8.16-compcert-3.11> Endianness.................... little coq8.16-compcert-3.11> OS and development env........ linux coq8.16-compcert-3.11> C compiler.................... /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc -m64 coq8.16-compcert-3.11> C preprocessor................ /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc -std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E coq8.16-compcert-3.11> Assembler..................... /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc -m64 -c coq8.16-compcert-3.11> Assembler supports CFI........ true coq8.16-compcert-3.11> Assembler for runtime lib..... /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc -m64 -c coq8.16-compcert-3.11> Linker........................ /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc -m64 -no-pie coq8.16-compcert-3.11> Archiver...................... ar rcs coq8.16-compcert-3.11> Math library.................. -lm coq8.16-compcert-3.11> Build command to use.......... make coq8.16-compcert-3.11> Menhir API library............ /nix/store/72jz2fcr51xy5mn84z2kca7bhpf316ac-ocaml4.14.0-menhirLib-20220210/lib/ocaml/4.14.0/site-lib/menhirLib coq8.16-compcert-3.11> The Flocq library............. external coq8.16-compcert-3.11> The MenhirLib library......... local coq8.16-compcert-3.11> Binaries installed in......... /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/bin coq8.16-compcert-3.11> Runtime library provided...... true coq8.16-compcert-3.11> Library files installed in.... /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/lib/compcert coq8.16-compcert-3.11> Man pages installed in........ /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/share/man coq8.16-compcert-3.11> Standard headers provided..... true coq8.16-compcert-3.11> Standard headers installed in. /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/lib/compcert/include coq8.16-compcert-3.11> Coq development installed in.. /nix/store/z8f4wg6bqyg2b9djzsmgf8flgp7dmqss-coq8.16-compcert-3.11-lib/lib/coq/8.16/user-contrib/compcert/ coq8.16-compcert-3.11> building coq8.16-compcert-3.11> build flags: -j48 SHELL=/nix/store/4xw8n979xpivdc46a9ndcvyhwgif00hz-bash-5.1-p16/bin/bash coq8.16-compcert-3.11> make[1]: Entering directory '/build/source' coq8.16-compcert-3.11> ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml coq8.16-compcert-3.11> menhir --coq --coq-no-version-check cparser/Parser.vy coq8.16-compcert-3.11> Preprocessing x86/ConstpropOp.vp coq8.16-compcert-3.11> Preprocessing x86/SelectOp.vp coq8.16-compcert-3.11> Preprocessing x86/SelectLong.vp coq8.16-compcert-3.11> Preprocessing backend/SelectDiv.vp coq8.16-compcert-3.11> Preprocessing backend/SplitLong.vp coq8.16-compcert-3.11> Analyzing Coq dependencies coq8.16-compcert-3.11> make[1]: Leaving directory '/build/source' coq8.16-compcert-3.11> make proof coq8.16-compcert-3.11> make[1]: Entering directory '/build/source' coq8.16-compcert-3.11> COQC lib/Axioms.v coq8.16-compcert-3.11> COQC lib/Coqlib.v coq8.16-compcert-3.11> COQC x86_64/Archi.v coq8.16-compcert-3.11> COQC lib/IEEE754_extra.v coq8.16-compcert-3.11> COQC driver/Compopts.v coq8.16-compcert-3.11> COQC MenhirLib/Alphabet.v coq8.16-compcert-3.11> COQC cparser/Cabs.v coq8.16-compcert-3.11> COQC lib/Wfsimpl.v coq8.16-compcert-3.11> File "./MenhirLib/Alphabet.v", line 78, characters 7-15: coq8.16-compcert-3.11> Warning: Notation gt_trans is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Gt file is obsolete. Use Nat.lt_trans instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Alphabet.v", line 78, characters 7-15: coq8.16-compcert-3.11> Warning: Notation gt_trans is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Gt file is obsolete. Use Nat.lt_trans instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> COQC MenhirLib/Grammar.v coq8.16-compcert-3.11> COQC MenhirLib/Validator_classes.v coq8.16-compcert-3.11> File "./lib/Coqlib.v", line 439, characters 14-26: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Coqlib.v", line 439, characters 14-26: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Coqlib.v", line 514, characters 14-26: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Coqlib.v", line 514, characters 14-26: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Coqlib.v", line 529, characters 14-26: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Coqlib.v", line 529, characters 14-26: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Coqlib.v", line 552, characters 14-26: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Coqlib.v", line 552, characters 14-26: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> COQC lib/Intv.v coq8.16-compcert-3.11> COQC lib/Maps.v coq8.16-compcert-3.11> COQC lib/Zbits.v coq8.16-compcert-3.11> COQC lib/Iteration.v coq8.16-compcert-3.11> COQC lib/Parmov.v coq8.16-compcert-3.11> COQC lib/UnionFind.v coq8.16-compcert-3.11> COQC lib/FSetAVLplus.v coq8.16-compcert-3.11> COQC lib/IntvSets.v coq8.16-compcert-3.11> COQC lib/Decidableplus.v coq8.16-compcert-3.11> COQC common/Errors.v coq8.16-compcert-3.11> COQC lib/BoolEqual.v coq8.16-compcert-3.11> File "./lib/IEEE754_extra.v", line 1039, characters 10-26: coq8.16-compcert-3.11> Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/IEEE754_extra.v", line 1039, characters 10-26: coq8.16-compcert-3.11> Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/IEEE754_extra.v", line 1039, characters 10-26: coq8.16-compcert-3.11> Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/IEEE754_extra.v", line 1039, characters 10-26: coq8.16-compcert-3.11> Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> COQC MenhirLib/Automaton.v coq8.16-compcert-3.11> File "./lib/Zbits.v", line 75, characters 28-40: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Zbits.v", line 75, characters 28-40: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Zbits.v", line 190, characters 13-25: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Zbits.v", line 190, characters 13-25: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> COQC MenhirLib/Validator_safe.v coq8.16-compcert-3.11> COQC MenhirLib/Validator_complete.v coq8.16-compcert-3.11> File "./lib/Zbits.v", line 482, characters 21-33: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Zbits.v", line 482, characters 21-33: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 282, characters 17-20: coq8.16-compcert-3.11> Warning: Notation max is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.max instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 282, characters 17-20: coq8.16-compcert-3.11> Warning: Notation max is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.max instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 282, characters 17-20: coq8.16-compcert-3.11> Warning: Notation max is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.max instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 282, characters 17-20: coq8.16-compcert-3.11> Warning: Notation max is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.max instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 282, characters 45-48: coq8.16-compcert-3.11> Warning: Notation max is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.max instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 282, characters 45-48: coq8.16-compcert-3.11> Warning: Notation max is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.max instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 282, characters 45-48: coq8.16-compcert-3.11> Warning: Notation max is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.max instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 282, characters 45-48: coq8.16-compcert-3.11> Warning: Notation max is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.max instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 283, characters 8-16: coq8.16-compcert-3.11> Warning: Notation le_max_r is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.le_max_r instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 283, characters 8-16: coq8.16-compcert-3.11> Warning: Notation le_max_r is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.le_max_r instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 283, characters 24-32: coq8.16-compcert-3.11> Warning: Notation le_max_l is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.le_max_l instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Iteration.v", line 283, characters 24-32: coq8.16-compcert-3.11> Warning: Notation le_max_l is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Max file is obsolete. Use Nat.le_max_l instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Zbits.v", line 946, characters 18-30: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Zbits.v", line 946, characters 18-30: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Zbits.v", line 946, characters 18-30: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Zbits.v", line 946, characters 18-30: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Zbits.v", line 954, characters 22-34: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Zbits.v", line 954, characters 22-34: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> COQC MenhirLib/Interpreter.v coq8.16-compcert-3.11> COQC lib/Integers.v coq8.16-compcert-3.11> COQC common/Unityping.v coq8.16-compcert-3.11> COQC lib/Lattice.v coq8.16-compcert-3.11> COQC lib/Postorder.v coq8.16-compcert-3.11> COQC MenhirLib/Interpreter_complete.v coq8.16-compcert-3.11> COQC MenhirLib/Interpreter_correct.v coq8.16-compcert-3.11> File "./lib/Integers.v", line 955, characters 45-57: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Integers.v", line 955, characters 45-57: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Integers.v", line 1933, characters 11-23: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Integers.v", line 1933, characters 11-23: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Integers.v", line 1961, characters 11-23: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Integers.v", line 1961, characters 11-23: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 791, characters 28-38: coq8.16-compcert-3.11> Warning: Notation plus_assoc is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use Nat.add_assoc instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 791, characters 28-38: coq8.16-compcert-3.11> Warning: Notation plus_assoc is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use Nat.add_assoc instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 791, characters 28-38: coq8.16-compcert-3.11> Warning: Notation plus_assoc is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use Nat.add_assoc instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 791, characters 28-38: coq8.16-compcert-3.11> Warning: Notation plus_assoc is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use Nat.add_assoc instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 792, characters 30-46: coq8.16-compcert-3.11> Warning: Notation plus_lt_compat_l is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 792, characters 30-46: coq8.16-compcert-3.11> Warning: Notation plus_lt_compat_l is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 793, characters 15-28: coq8.16-compcert-3.11> Warning: Notation lt_plus_trans is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use Nat.le_add_r (together with Nat.lt_le_trans) instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 793, characters 15-28: coq8.16-compcert-3.11> Warning: Notation lt_plus_trans is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use Nat.le_add_r (together with Nat.lt_le_trans) instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 819, characters 10-20: coq8.16-compcert-3.11> Warning: Notation le_lt_n_Sm is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 819, characters 22-31: coq8.16-compcert-3.11> Warning: Notation le_plus_l is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use Nat.le_add_r instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 819, characters 10-20: coq8.16-compcert-3.11> Warning: Notation le_lt_n_Sm is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 819, characters 22-31: coq8.16-compcert-3.11> Warning: Notation le_plus_l is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use Nat.le_add_r instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 820, characters 47-54: coq8.16-compcert-3.11> Warning: Notation lt_le_S is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./MenhirLib/Interpreter_complete.v", line 820, characters 47-54: coq8.16-compcert-3.11> Warning: Notation lt_le_S is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_succ_l instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> COQC MenhirLib/Main.v coq8.16-compcert-3.11> File "./lib/Integers.v", line 4501, characters 37-49: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./lib/Integers.v", line 4501, characters 37-49: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> COQC lib/Ordered.v coq8.16-compcert-3.11> COQC lib/Floats.v coq8.16-compcert-3.11> COQC cparser/Parser.v coq8.16-compcert-3.11> COQC lib/Heaps.v coq8.16-compcert-3.11> COQC common/AST.v coq8.16-compcert-3.11> COQC common/Values.v coq8.16-compcert-3.11> COQC common/Linking.v coq8.16-compcert-3.11> COQC common/Memdata.v coq8.16-compcert-3.11> COQC common/Switch.v coq8.16-compcert-3.11> COQC backend/Registers.v coq8.16-compcert-3.11> COQC cfrontend/Ctypes.v coq8.16-compcert-3.11> File "./common/Switch.v", line 274, characters 55-67: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Switch.v", line 274, characters 55-67: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Switch.v", line 311, characters 8-20: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Switch.v", line 311, characters 8-20: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Switch.v", line 312, characters 21-33: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Switch.v", line 312, characters 21-33: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Switch.v", line 317, characters 8-20: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Switch.v", line 317, characters 8-20: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 429, characters 13-25: coq8.16-compcert-3.11> Warning: Notation beq_nat_refl is deprecated since 8.16. coq8.16-compcert-3.11> Use Nat.eqb_refl (with symmetry of equality) instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 429, characters 13-25: coq8.16-compcert-3.11> Warning: Notation beq_nat_refl is deprecated since 8.16. coq8.16-compcert-3.11> Use Nat.eqb_refl (with symmetry of equality) instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 429, characters 13-25: coq8.16-compcert-3.11> Warning: Notation beq_nat_refl is deprecated since 8.16. coq8.16-compcert-3.11> Use Nat.eqb_refl (with symmetry of equality) instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 722, characters 53-65: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 722, characters 53-65: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 741, characters 17-29: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 741, characters 17-29: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 800, characters 41-53: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 800, characters 41-53: coq8.16-compcert-3.11> Warning: Notation beq_nat_true is deprecated since 8.16. coq8.16-compcert-3.11> Use the bidirectional version Nat.eqb_eq instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 802, characters 57-69: coq8.16-compcert-3.11> Warning: Notation beq_nat_refl is deprecated since 8.16. coq8.16-compcert-3.11> Use Nat.eqb_refl (with symmetry of equality) instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 802, characters 57-69: coq8.16-compcert-3.11> Warning: Notation beq_nat_refl is deprecated since 8.16. coq8.16-compcert-3.11> Use Nat.eqb_refl (with symmetry of equality) instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./common/Memdata.v", line 802, characters 57-69: coq8.16-compcert-3.11> Warning: Notation beq_nat_refl is deprecated since 8.16. coq8.16-compcert-3.11> Use Nat.eqb_refl (with symmetry of equality) instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./cfrontend/Ctypes.v", line 739, characters 16-28: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./cfrontend/Ctypes.v", line 739, characters 16-28: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> COQC common/Memtype.v coq8.16-compcert-3.11> COQC common/Builtins0.v coq8.16-compcert-3.11> COQC common/Memory.v coq8.16-compcert-3.11> COQC x86/Builtins1.v coq8.16-compcert-3.11> COQC export/Ctypesdefs.v coq8.16-compcert-3.11> COQC common/Builtins.v coq8.16-compcert-3.11> COQC common/Globalenvs.v coq8.16-compcert-3.11> COQC cfrontend/Cop.v coq8.16-compcert-3.11> COQC common/Events.v coq8.16-compcert-3.11> COQC backend/Kildall.v coq8.16-compcert-3.11> COQC cfrontend/Csyntax.v coq8.16-compcert-3.11> COQC cfrontend/Initializers.v coq8.16-compcert-3.11> COQC export/Csyntaxdefs.v coq8.16-compcert-3.11> COQC common/Smallstep.v coq8.16-compcert-3.11> COQC common/Separation.v coq8.16-compcert-3.11> COQC x86/Op.v coq8.16-compcert-3.11> COQC common/Behaviors.v coq8.16-compcert-3.11> COQC backend/Cminor.v coq8.16-compcert-3.11> COQC cfrontend/Clight.v coq8.16-compcert-3.11> COQC cfrontend/Csem.v coq8.16-compcert-3.11> COQC cfrontend/SimplExpr.v coq8.16-compcert-3.11> COQC export/Clightdefs.v coq8.16-compcert-3.11> COQC cfrontend/ClightBigstep.v coq8.16-compcert-3.11> COQC cfrontend/Ctyping.v coq8.16-compcert-3.11> COQC cfrontend/Cstrategy.v coq8.16-compcert-3.11> COQC cfrontend/Initializersproof.v coq8.16-compcert-3.11> COQC common/Determinism.v coq8.16-compcert-3.11> COQC cfrontend/SimplExprspec.v coq8.16-compcert-3.11> COQC backend/Cminortyping.v coq8.16-compcert-3.11> COQC cfrontend/Csharpminor.v coq8.16-compcert-3.11> COQC cfrontend/Cminorgen.v coq8.16-compcert-3.11> COQC cfrontend/Cminorgenproof.v coq8.16-compcert-3.11> COQC cfrontend/Cexec.v coq8.16-compcert-3.11> COQC cfrontend/SimplExprproof.v coq8.16-compcert-3.11> COQC backend/CminorSel.v coq8.16-compcert-3.11> COQC x86/Machregs.v coq8.16-compcert-3.11> COQC backend/RTL.v coq8.16-compcert-3.11> COQC x86/SelectOp.v coq8.16-compcert-3.11> COQC backend/Locations.v coq8.16-compcert-3.11> COQC backend/RTLgen.v coq8.16-compcert-3.11> COQC backend/Inlining.v coq8.16-compcert-3.11> COQC backend/Renumber.v coq8.16-compcert-3.11> COQC backend/Liveness.v coq8.16-compcert-3.11> COQC backend/ValueDomain.v coq8.16-compcert-3.11> COQC backend/CSEdomain.v coq8.16-compcert-3.11> COQC backend/Unusedglob.v coq8.16-compcert-3.11> COQC backend/Unusedglobproof.v coq8.16-compcert-3.11> COQC backend/Inliningspec.v coq8.16-compcert-3.11> COQC backend/Renumberproof.v coq8.16-compcert-3.11> COQC backend/RTLgenspec.v coq8.16-compcert-3.11> COQC x86/CombineOp.v coq8.16-compcert-3.11> COQC x86/Conventions1.v coq8.16-compcert-3.11> COQC backend/Conventions.v coq8.16-compcert-3.11> COQC cfrontend/SimplLocals.v coq8.16-compcert-3.11> COQC cfrontend/Cshmgen.v coq8.16-compcert-3.11> COQC backend/Inliningproof.v coq8.16-compcert-3.11> COQC backend/SplitLong.v coq8.16-compcert-3.11> COQC x86/SelectOpproof.v coq8.16-compcert-3.11> COQC cfrontend/SimplLocalsproof.v coq8.16-compcert-3.11> COQC backend/RTLtyping.v coq8.16-compcert-3.11> COQC backend/Tailcall.v coq8.16-compcert-3.11> COQC backend/LTL.v coq8.16-compcert-3.11> COQC cfrontend/Cshmgenproof.v coq8.16-compcert-3.11> COQC backend/Tailcallproof.v coq8.16-compcert-3.11> COQC backend/Tunneling.v coq8.16-compcert-3.11> COQC backend/Linear.v coq8.16-compcert-3.11> COQC x86/SelectLong.v coq8.16-compcert-3.11> COQC backend/Lineartyping.v coq8.16-compcert-3.11> COQC backend/CleanupLabels.v coq8.16-compcert-3.11> COQC backend/Debugvar.v coq8.16-compcert-3.11> COQC backend/Bounds.v coq8.16-compcert-3.11> COQC backend/Linearize.v coq8.16-compcert-3.11> COQC backend/Tunnelingproof.v coq8.16-compcert-3.11> COQC x86/CombineOpproof.v coq8.16-compcert-3.11> COQC backend/Allocation.v coq8.16-compcert-3.11> File "./cfrontend/SimplExprproof.v", line 1977, characters 46-62: coq8.16-compcert-3.11> Warning: Notation plus_lt_compat_r is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_r instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./cfrontend/SimplExprproof.v", line 1977, characters 46-62: coq8.16-compcert-3.11> Warning: Notation plus_lt_compat_r is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_r instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./cfrontend/SimplExprproof.v", line 1999, characters 46-62: coq8.16-compcert-3.11> Warning: Notation plus_lt_compat_r is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_r instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./cfrontend/SimplExprproof.v", line 1999, characters 46-62: coq8.16-compcert-3.11> Warning: Notation plus_lt_compat_r is deprecated since 8.16. coq8.16-compcert-3.11> The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_r instead. coq8.16-compcert-3.11> [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> COQC backend/Linearizeproof.v coq8.16-compcert-3.11> COQC backend/CleanupLabelsproof.v coq8.16-compcert-3.11> COQC backend/Debugvarproof.v coq8.16-compcert-3.11> COQC x86/Stacklayout.v coq8.16-compcert-3.11> COQC backend/RTLgenproof.v coq8.16-compcert-3.11> COQC backend/Mach.v coq8.16-compcert-3.11> COQC x86/Asm.v coq8.16-compcert-3.11> COQC backend/SplitLongproof.v coq8.16-compcert-3.11> COQC backend/Stacking.v coq8.16-compcert-3.11> COQC x86/Asmgen.v coq8.16-compcert-3.11> COQC backend/SelectDiv.v coq8.16-compcert-3.11> COQC backend/Stackingproof.v coq8.16-compcert-3.11> COQC backend/Selection.v coq8.16-compcert-3.11> COQC backend/Allocproof.v coq8.16-compcert-3.11> COQC backend/Asmgenproof0.v coq8.16-compcert-3.11> COQC x86/Asmgenproof1.v coq8.16-compcert-3.11> COQC x86/SelectLongproof.v coq8.16-compcert-3.11> COQC backend/NeedDomain.v coq8.16-compcert-3.11> COQC x86/ValueAOp.v coq8.16-compcert-3.11> COQC backend/SelectDivproof.v coq8.16-compcert-3.11> COQC backend/ValueAnalysis.v coq8.16-compcert-3.11> COQC x86/ConstpropOp.v coq8.16-compcert-3.11> File "./backend/SelectDivproof.v", line 42, characters 11-23: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./backend/SelectDivproof.v", line 42, characters 11-23: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./backend/SelectDivproof.v", line 108, characters 11-23: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> File "./backend/SelectDivproof.v", line 108, characters 11-23: coq8.16-compcert-3.11> Warning: Notation Z_div_mod_eq is deprecated since 8.14. coq8.16-compcert-3.11> Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated] coq8.16-compcert-3.11> COQC x86/NeedOp.v coq8.16-compcert-3.11> COQC backend/Selectionproof.v coq8.16-compcert-3.11> COQC backend/Constprop.v coq8.16-compcert-3.11> COQC x86/ConstpropOpproof.v coq8.16-compcert-3.11> COQC backend/CSE.v coq8.16-compcert-3.11> COQC backend/Deadcode.v coq8.16-compcert-3.11> COQC backend/CSEproof.v coq8.16-compcert-3.11> COQC backend/Deadcodeproof.v coq8.16-compcert-3.11> COQC x86/Asmgenproof.v coq8.16-compcert-3.11> COQC backend/Constpropproof.v coq8.16-compcert-3.11> COQC driver/Compiler.v coq8.16-compcert-3.11> COQC driver/Complements.v coq8.16-compcert-3.11> make[1]: Leaving directory '/build/source' coq8.16-compcert-3.11> make extraction coq8.16-compcert-3.11> make[1]: Entering directory '/build/source' coq8.16-compcert-3.11> rm -f extraction/*.ml extraction/*.mli coq8.16-compcert-3.11> "/nix/store/xhrf5cq7cil1p3q34j5q2300mqx69pwd-coq-8.16.1/bin/coqtop" -R lib compcert.lib -R common compcert.common -R x86_64 compcert.x86_64 -R x86 compcert.x86 -R backend compcert.backend -R cfrontend compcert.cfrontend -R driver compcert.driver -R export compcert.export -R cparser compcert.cparser -R MenhirLib MenhirLib -batch -load-vernac-source extraction/extraction.v coq8.16-compcert-3.11> File "/build/source/extraction/extraction.v", line 154, characters 0-1084: coq8.16-compcert-3.11> Warning: The extraction is currently set to bypass opacity, the following coq8.16-compcert-3.11> opaque constant bodies have been accessed : solve_constraints_terminate. coq8.16-compcert-3.11> [extraction-opaque-accessed,extraction] coq8.16-compcert-3.11> touch extraction/STAMP coq8.16-compcert-3.11> make[1]: Leaving directory '/build/source' coq8.16-compcert-3.11> make ccomp coq8.16-compcert-3.11> make[1]: Entering directory '/build/source' coq8.16-compcert-3.11> ocamlopt -o tools/modorder str.cmxa tools/modorder.ml coq8.16-compcert-3.11> (echo 'let version = "3.11"'; \ coq8.16-compcert-3.11> echo 'let buildnr = ""'; \ coq8.16-compcert-3.11> echo 'let tag = ""'; \ coq8.16-compcert-3.11> echo 'let branch = ""') > driver/Version.ml coq8.16-compcert-3.11> (echo "stdlib_path=/nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/lib/compcert"; \ coq8.16-compcert-3.11> echo "prepro=/nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc"; \ coq8.16-compcert-3.11> echo "linker=/nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc"; \ coq8.16-compcert-3.11> echo "asm=/nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc"; \ coq8.16-compcert-3.11> echo "prepro_options=-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E";\ coq8.16-compcert-3.11> echo "asm_options=-m64 -c";\ coq8.16-compcert-3.11> echo "linker_options=-m64 -no-pie";\ coq8.16-compcert-3.11> echo "arch=x86"; \ coq8.16-compcert-3.11> echo "model=64"; \ coq8.16-compcert-3.11> echo "abi=standard"; \ coq8.16-compcert-3.11> echo "endianness=little"; \ coq8.16-compcert-3.11> echo "system=linux"; \ coq8.16-compcert-3.11> echo "has_runtime_lib=true"; \ coq8.16-compcert-3.11> echo "has_standard_headers=true"; \ coq8.16-compcert-3.11> echo "asm_supports_cfi=true"; \ coq8.16-compcert-3.11> echo "response_file_style=gnu";) \ coq8.16-compcert-3.11> > compcert.ini coq8.16-compcert-3.11> make -f Makefile.extr depend coq8.16-compcert-3.11> make[2]: Entering directory '/build/source' coq8.16-compcert-3.11> menhir --table -v --no-stdlib -la 1 cparser/pre_parser.mly coq8.16-compcert-3.11> ocamllex -q cparser/Lexer.mll coq8.16-compcert-3.11> ocamllex -q lib/Tokenize.mll coq8.16-compcert-3.11> ocamllex -q lib/Readconfig.mll coq8.16-compcert-3.11> ocamllex -q lib/Responsefile.mll coq8.16-compcert-3.11> make -C cparser correct coq8.16-compcert-3.11> make[3]: Entering directory '/build/source/cparser' coq8.16-compcert-3.11> Built an LR(0) automaton with 628 states. coq8.16-compcert-3.11> The construction mode is pager. coq8.16-compcert-3.11> Built an LR(1) automaton with 628 states. coq8.16-compcert-3.11> 2 shift/reduce conflicts were silently solved. coq8.16-compcert-3.11> Extra reductions on error were added in 103 states. coq8.16-compcert-3.11> Priority played a role in 0 of these states. coq8.16-compcert-3.11> Built an LR(0) automaton with 628 states. coq8.16-compcert-3.11> The construction mode is pager. coq8.16-compcert-3.11> Built an LR(1) automaton with 628 states. coq8.16-compcert-3.11> 2 shift/reduce conflicts were silently solved. coq8.16-compcert-3.11> Extra reductions on error were added in 103 states. coq8.16-compcert-3.11> Priority played a role in 0 of these states. coq8.16-compcert-3.11> Read 233 sample input sentences and 180 error messages. coq8.16-compcert-3.11> OK. The set of erroneous inputs is correct and irredundant. coq8.16-compcert-3.11> make[3]: Leaving directory '/build/source/cparser' coq8.16-compcert-3.11> Analyzing OCaml dependencies coq8.16-compcert-3.11> make[2]: Leaving directory '/build/source' coq8.16-compcert-3.11> make -f Makefile.extr ccomp coq8.16-compcert-3.11> make[2]: Entering directory '/build/source' coq8.16-compcert-3.11> OCAMLOPT driver/Version.ml coq8.16-compcert-3.11> OCAMLC lib/Readconfig.mli coq8.16-compcert-3.11> OCAMLC lib/Responsefile.mli coq8.16-compcert-3.11> OCAMLC lib/Commandline.mli coq8.16-compcert-3.11> OCAMLC driver/Configuration.mli coq8.16-compcert-3.11> OCAMLC extraction/Datatypes.mli coq8.16-compcert-3.11> OCAMLC extraction/BinNums.mli coq8.16-compcert-3.11> OCAMLC extraction/Bool.mli coq8.16-compcert-3.11> OCAMLC extraction/EquivDec.mli coq8.16-compcert-3.11> OCAMLC extraction/BoolEqual.mli coq8.16-compcert-3.11> OCAMLC extraction/String0.mli coq8.16-compcert-3.11> OCAMLC extraction/Equalities.mli coq8.16-compcert-3.11> OCAMLC extraction/Specif.mli coq8.16-compcert-3.11> OCAMLC lib/Tokenize.mli coq8.16-compcert-3.11> OCAMLC cparser/Diagnostics.mli coq8.16-compcert-3.11> OCAMLC cparser/Machine.mli coq8.16-compcert-3.11> OCAMLC cparser/C.mli coq8.16-compcert-3.11> OCAMLC extraction/Memtype.mli coq8.16-compcert-3.11> OCAMLC extraction/PeanoNat.mli coq8.16-compcert-3.11> OCAMLC x86/Machregsaux.mli coq8.16-compcert-3.11> OCAMLC lib/Printlines.mli coq8.16-compcert-3.11> OCAMLC driver/Linker.mli coq8.16-compcert-3.11> OCAMLC extraction/DecidableClass.mli coq8.16-compcert-3.11> OCAMLC extraction/Cabs.mli coq8.16-compcert-3.11> OCAMLC cparser/pre_parser_aux.mli coq8.16-compcert-3.11> OCAMLOPT cparser/pre_parser_messages.ml coq8.16-compcert-3.11> OCAMLC cparser/Cleanup.mli coq8.16-compcert-3.11> OCAMLC cparser/Checks.mli coq8.16-compcert-3.11> OCAMLC cparser/Parse.mli coq8.16-compcert-3.11> OCAMLC extraction/UnionFind.mli coq8.16-compcert-3.11> OCAMLC extraction/Compopts.mli coq8.16-compcert-3.11> OCAMLC extraction/Compare_dec.mli coq8.16-compcert-3.11> OCAMLC driver/Clflags.ml coq8.16-compcert-3.11> OCAMLC driver/Assembler.mli coq8.16-compcert-3.11> OCAMLOPT lib/Readconfig.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Datatypes.ml coq8.16-compcert-3.11> OCAMLOPT lib/Responsefile.ml coq8.16-compcert-3.11> OCAMLC extraction/Nat.mli coq8.16-compcert-3.11> OCAMLOPT extraction/BinNums.ml coq8.16-compcert-3.11> OCAMLC extraction/BinPosDef.mli coq8.16-compcert-3.11> OCAMLC extraction/List0.mli coq8.16-compcert-3.11> OCAMLC extraction/Archi.mli coq8.16-compcert-3.11> OCAMLC extraction/Zaux.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Bool.ml coq8.16-compcert-3.11> OCAMLC extraction/Orders.mli coq8.16-compcert-3.11> OCAMLOPT extraction/EquivDec.ml coq8.16-compcert-3.11> OCAMLOPT extraction/BoolEqual.ml coq8.16-compcert-3.11> OCAMLOPT extraction/String0.ml coq8.16-compcert-3.11> OCAMLC extraction/Errors.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Equalities.ml coq8.16-compcert-3.11> OCAMLC extraction/DecidableType.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Specif.ml coq8.16-compcert-3.11> OCAMLOPT lib/Tokenize.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Machine.ml coq8.16-compcert-3.11> OCAMLC cparser/Env.mli coq8.16-compcert-3.11> OCAMLC cparser/Cprint.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Memtype.ml coq8.16-compcert-3.11> OCAMLOPT extraction/PeanoNat.ml coq8.16-compcert-3.11> OCAMLOPT x86/Machregsaux.ml coq8.16-compcert-3.11> OCAMLOPT lib/Printlines.ml coq8.16-compcert-3.11> OCAMLC driver/Driveraux.mli coq8.16-compcert-3.11> OCAMLOPT extraction/DecidableClass.ml coq8.16-compcert-3.11> OCAMLC cparser/Unblock.mli coq8.16-compcert-3.11> OCAMLC cparser/Transform.mli coq8.16-compcert-3.11> OCAMLC cparser/StructPassing.mli coq8.16-compcert-3.11> OCAMLC cparser/Rename.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Cabs.ml coq8.16-compcert-3.11> OCAMLOPT cparser/pre_parser_aux.ml coq8.16-compcert-3.11> OCAMLC cparser/pre_parser.mli coq8.16-compcert-3.11> OCAMLC cparser/Elab.mli coq8.16-compcert-3.11> OCAMLOPT extraction/UnionFind.ml coq8.16-compcert-3.11> OCAMLC cparser/Cflow.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Compare_dec.ml coq8.16-compcert-3.11> OCAMLC extraction/Mergesort.mli coq8.16-compcert-3.11> OCAMLC x86/CBuiltins.ml coq8.16-compcert-3.11> OCAMLOPT lib/Commandline.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Nat.ml coq8.16-compcert-3.11> OCAMLOPT extraction/BinPosDef.ml coq8.16-compcert-3.11> OCAMLC extraction/BinPos.mli coq8.16-compcert-3.11> OCAMLOPT extraction/List0.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Zaux.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Orders.ml coq8.16-compcert-3.11> OCAMLC extraction/OrdersTac.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Errors.ml coq8.16-compcert-3.11> OCAMLOPT extraction/DecidableType.ml coq8.16-compcert-3.11> OCAMLC extraction/FSetInterface.mli coq8.16-compcert-3.11> OCAMLOPT cparser/Env.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Cprint.ml coq8.16-compcert-3.11> OCAMLC cparser/Cutil.mli coq8.16-compcert-3.11> OCAMLC cparser/Ceval.mli coq8.16-compcert-3.11> OCAMLOPT cparser/pre_parser.ml coq8.16-compcert-3.11> OCAMLC cparser/ErrorReports.mli coq8.16-compcert-3.11> OCAMLOPT cparser/Cabshelper.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Mergesort.ml coq8.16-compcert-3.11> OCAMLOPT driver/Configuration.ml coq8.16-compcert-3.11> OCAMLOPT extraction/BinPos.ml coq8.16-compcert-3.11> OCAMLC extraction/Zpower.mli coq8.16-compcert-3.11> OCAMLC extraction/BinNat.mli coq8.16-compcert-3.11> OCAMLOPT extraction/OrdersTac.ml coq8.16-compcert-3.11> OCAMLC extraction/OrderedType.mli coq8.16-compcert-3.11> OCAMLC extraction/OrdersFacts.mli coq8.16-compcert-3.11> OCAMLOPT extraction/FSetInterface.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Diagnostics.ml coq8.16-compcert-3.11> OCAMLC extraction/BinInt.mli coq8.16-compcert-3.11> OCAMLC extraction/MSetInterface.mli coq8.16-compcert-3.11> OCAMLC extraction/OrdersAlt.mli coq8.16-compcert-3.11> OCAMLC extraction/Alphabet.mli coq8.16-compcert-3.11> OCAMLC extraction/FMapList.mli coq8.16-compcert-3.11> OCAMLOPT driver/Clflags.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Archi.ml coq8.16-compcert-3.11> OCAMLOPT extraction/OrderedType.ml coq8.16-compcert-3.11> OCAMLC extraction/Int0.mli coq8.16-compcert-3.11> OCAMLOPT extraction/OrdersFacts.ml coq8.16-compcert-3.11> OCAMLC extraction/Znumtheory.mli coq8.16-compcert-3.11> OCAMLC extraction/Decidableplus.mli coq8.16-compcert-3.11> OCAMLC extraction/Grammar.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Zpower.ml coq8.16-compcert-3.11> OCAMLOPT extraction/BinNat.ml coq8.16-compcert-3.11> OCAMLC extraction/ZArith_dec.mli coq8.16-compcert-3.11> OCAMLC extraction/Zbool.mli coq8.16-compcert-3.11> OCAMLOPT extraction/OrdersAlt.ml coq8.16-compcert-3.11> OCAMLC extraction/MSetAVL.mli coq8.16-compcert-3.11> OCAMLOPT x86/CBuiltins.ml coq8.16-compcert-3.11> OCAMLOPT backend/Fileinfo.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Alphabet.ml coq8.16-compcert-3.11> OCAMLC extraction/Automaton.mli coq8.16-compcert-3.11> OCAMLOPT extraction/FMapList.ml coq8.16-compcert-3.11> OCAMLC extraction/FMapAVL.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Compopts.ml coq8.16-compcert-3.11> OCAMLOPT driver/CommonOptions.ml coq8.16-compcert-3.11> OCAMLOPT extraction/BinInt.ml coq8.16-compcert-3.11> OCAMLC extraction/Coqlib.mli coq8.16-compcert-3.11> OCAMLC extraction/SpecFloat.mli coq8.16-compcert-3.11> OCAMLOPT extraction/MSetInterface.ml coq8.16-compcert-3.11> OCAMLC extraction/FSetAVL.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Grammar.ml coq8.16-compcert-3.11> OCAMLC extraction/Interpreter_correct.mli coq8.16-compcert-3.11> OCAMLC extraction/Validator_safe.mli coq8.16-compcert-3.11> OCAMLC extraction/FSetAVLplus.mli coq8.16-compcert-3.11> OCAMLC extraction/Zbits.mli coq8.16-compcert-3.11> OCAMLC extraction/Round.mli coq8.16-compcert-3.11> OCAMLC extraction/Maps.mli coq8.16-compcert-3.11> OCAMLC extraction/Iteration.mli coq8.16-compcert-3.11> OCAMLC extraction/IntvSets.mli coq8.16-compcert-3.11> OCAMLC extraction/Integers.mli coq8.16-compcert-3.11> OCAMLOPT extraction/ZArith_dec.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Zbool.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Int0.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Znumtheory.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Decidableplus.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Automaton.ml coq8.16-compcert-3.11> OCAMLC extraction/Interpreter.mli coq8.16-compcert-3.11> OCAMLC extraction/Switch.mli coq8.16-compcert-3.11> OCAMLC extraction/Postorder.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Coqlib.ml coq8.16-compcert-3.11> OCAMLOPT extraction/SpecFloat.ml coq8.16-compcert-3.11> OCAMLC extraction/BinarySingleNaN.mli coq8.16-compcert-3.11> OCAMLC extraction/Ordered.mli coq8.16-compcert-3.11> OCAMLOPT extraction/MSetAVL.ml coq8.16-compcert-3.11> OCAMLC extraction/Lattice.mli coq8.16-compcert-3.11> OCAMLC extraction/Unityping.mli coq8.16-compcert-3.11> OCAMLC extraction/Binary.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Interpreter_correct.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Validator_safe.ml coq8.16-compcert-3.11> OCAMLC extraction/Registers.mli coq8.16-compcert-3.11> OCAMLC extraction/Heaps.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Zbits.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Maps.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Iteration.ml coq8.16-compcert-3.11> OCAMLOPT extraction/IntvSets.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Round.ml coq8.16-compcert-3.11> OCAMLC extraction/IEEE754_extra.mli coq8.16-compcert-3.11> OCAMLC extraction/Bits.mli coq8.16-compcert-3.11> OCAMLC extraction/Kildall.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Integers.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Interpreter.ml coq8.16-compcert-3.11> OCAMLOPT extraction/BinarySingleNaN.ml coq8.16-compcert-3.11> OCAMLC extraction/Floats.mli coq8.16-compcert-3.11> OCAMLC extraction/Validator_complete.mli coq8.16-compcert-3.11> OCAMLC extraction/AST.mli coq8.16-compcert-3.11> OCAMLC lib/Camlcoq.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Binary.ml coq8.16-compcert-3.11> OCAMLOPT extraction/FSetAVL.ml coq8.16-compcert-3.11> OCAMLOPT extraction/FSetAVLplus.ml coq8.16-compcert-3.11> OCAMLC extraction/Op.mli coq8.16-compcert-3.11> OCAMLC common/Sections.mli coq8.16-compcert-3.11> OCAMLC extraction/Values.mli coq8.16-compcert-3.11> OCAMLC backend/AisAnnot.mli coq8.16-compcert-3.11> OCAMLC extraction/Cminor.mli coq8.16-compcert-3.11> OCAMLC extraction/Ctypes.mli coq8.16-compcert-3.11> OCAMLC extraction/Events.mli coq8.16-compcert-3.11> OCAMLC extraction/Interpreter_complete.mli coq8.16-compcert-3.11> OCAMLC debug/DebugTypes.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Switch.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Postorder.ml coq8.16-compcert-3.11> OCAMLOPT extraction/IEEE754_extra.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Bits.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Ordered.ml coq8.16-compcert-3.11> OCAMLC extraction/Machregs.mli coq8.16-compcert-3.11> OCAMLC extraction/RTL.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Lattice.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Unityping.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Cutil.ml coq8.16-compcert-3.11> OCAMLC extraction/Memdata.mli coq8.16-compcert-3.11> OCAMLC debug/DwarfTypes.mli coq8.16-compcert-3.11> OCAMLC extraction/Determinism.mli coq8.16-compcert-3.11> OCAMLC extraction/CminorSel.mli coq8.16-compcert-3.11> OCAMLC extraction/Cminortyping.mli coq8.16-compcert-3.11> OCAMLC extraction/Csharpminor.mli coq8.16-compcert-3.11> OCAMLC extraction/CSEdomain.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Floats.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Registers.ml coq8.16-compcert-3.11> OCAMLC extraction/Locations.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Heaps.ml coq8.16-compcert-3.11> OCAMLC backend/Machregsnames.mli coq8.16-compcert-3.11> OCAMLC extraction/Memory.mli coq8.16-compcert-3.11> OCAMLC debug/Debug.mli coq8.16-compcert-3.11> OCAMLC extraction/Mach.mli coq8.16-compcert-3.11> OCAMLC extraction/Asm.mli coq8.16-compcert-3.11> OCAMLOPT debug/DwarfUtil.ml coq8.16-compcert-3.11> OCAMLC debug/DwarfPrinter.mli coq8.16-compcert-3.11> OCAMLC extraction/Builtins0.mli coq8.16-compcert-3.11> OCAMLOPT extraction/FMapAVL.ml coq8.16-compcert-3.11> OCAMLOPT cparser/ErrorReports.ml coq8.16-compcert-3.11> OCAMLC extraction/Unusedglob.mli coq8.16-compcert-3.11> OCAMLC extraction/Linear.mli coq8.16-compcert-3.11> OCAMLC extraction/Renumber.mli coq8.16-compcert-3.11> OCAMLC extraction/RTLgen.mli coq8.16-compcert-3.11> OCAMLC cparser/ExtendedAsm.ml coq8.16-compcert-3.11> OCAMLC extraction/ValueDomain.mli coq8.16-compcert-3.11> OCAMLC extraction/Liveness.mli coq8.16-compcert-3.11> OCAMLC extraction/Cminorgen.mli coq8.16-compcert-3.11> OCAMLC extraction/CombineOp.mli coq8.16-compcert-3.11> OCAMLC extraction/Asmgen.mli coq8.16-compcert-3.11> OCAMLC backend/Asmexpandaux.mli coq8.16-compcert-3.11> OCAMLC x86/AsmToJSON.mli coq8.16-compcert-3.11> OCAMLC backend/XTL.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Kildall.ml coq8.16-compcert-3.11> OCAMLC extraction/Conventions1.mli coq8.16-compcert-3.11> OCAMLC extraction/LTL.mli coq8.16-compcert-3.11> OCAMLC extraction/Cop.mli coq8.16-compcert-3.11> OCAMLC backend/PrintAsm.mli coq8.16-compcert-3.11> OCAMLC extraction/Globalenvs.mli coq8.16-compcert-3.11> OCAMLC extraction/Builtins1.mli coq8.16-compcert-3.11> OCAMLC debug/DebugInformation.mli coq8.16-compcert-3.11> OCAMLC extraction/ValueAOp.mli coq8.16-compcert-3.11> OCAMLC extraction/NeedDomain.mli coq8.16-compcert-3.11> OCAMLC extraction/CleanupLabels.mli coq8.16-compcert-3.11> OCAMLOPT x86/AsmToJSON.ml coq8.16-compcert-3.11> OCAMLOPT lib/Camlcoq.ml coq8.16-compcert-3.11> OCAMLOPT extraction/AST.ml coq8.16-compcert-3.11> OCAMLC extraction/Conventions.mli coq8.16-compcert-3.11> OCAMLC extraction/Csyntax.mli coq8.16-compcert-3.11> OCAMLC backend/IRC.mli coq8.16-compcert-3.11> OCAMLC extraction/Clight.mli coq8.16-compcert-3.11> OCAMLC extraction/Builtins.mli coq8.16-compcert-3.11> OCAMLC extraction/Main.mli coq8.16-compcert-3.11> OCAMLC extraction/Tunneling.mli coq8.16-compcert-3.11> OCAMLC extraction/Tailcall.mli coq8.16-compcert-3.11> OCAMLC extraction/Bounds.mli coq8.16-compcert-3.11> OCAMLC extraction/Lineartyping.mli coq8.16-compcert-3.11> OCAMLC extraction/SelectOp.mli coq8.16-compcert-3.11> OCAMLC extraction/Linearize.mli coq8.16-compcert-3.11> OCAMLC extraction/Debugvar.mli coq8.16-compcert-3.11> OCAMLC extraction/ValueAnalysis.mli coq8.16-compcert-3.11> OCAMLC extraction/NeedOp.mli coq8.16-compcert-3.11> OCAMLC extraction/Cshmgen.mli coq8.16-compcert-3.11> OCAMLC extraction/RTLtyping.mli coq8.16-compcert-3.11> OCAMLC extraction/Initializers.mli coq8.16-compcert-3.11> OCAMLC extraction/Ctyping.mli coq8.16-compcert-3.11> OCAMLC extraction/Csem.mli coq8.16-compcert-3.11> OCAMLC driver/Frontend.mli coq8.16-compcert-3.11> OCAMLC extraction/Stacklayout.mli coq8.16-compcert-3.11> OCAMLC extraction/SimplLocals.mli coq8.16-compcert-3.11> OCAMLC extraction/SimplExpr.mli coq8.16-compcert-3.11> OCAMLC extraction/SplitLong.mli coq8.16-compcert-3.11> OCAMLC extraction/Deadcode.mli coq8.16-compcert-3.11> OCAMLC extraction/ConstpropOp.mli coq8.16-compcert-3.11> OCAMLC extraction/CSE.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Op.ml coq8.16-compcert-3.11> OCAMLOPT common/Sections.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Values.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Ctypes.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Ceval.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Cminor.ml coq8.16-compcert-3.11> OCAMLOPT driver/Driveraux.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Events.ml coq8.16-compcert-3.11> OCAMLC extraction/Cexec.mli coq8.16-compcert-3.11> OCAMLOPT cparser/Transform.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Rename.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Checks.ml coq8.16-compcert-3.11> OCAMLC extraction/Stacking.mli coq8.16-compcert-3.11> OCAMLOPT common/Switchaux.ml coq8.16-compcert-3.11> OCAMLC extraction/SelectLong.mli coq8.16-compcert-3.11> OCAMLC cfrontend/C2C.ml coq8.16-compcert-3.11> OCAMLC extraction/Constprop.mli coq8.16-compcert-3.11> OCAMLC extraction/Allocation.mli coq8.16-compcert-3.11> OCAMLOPT driver/Timing.ml coq8.16-compcert-3.11> OCAMLOPT common/PrintAST.ml coq8.16-compcert-3.11> OCAMLOPT backend/Selectionaux.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Cminortyping.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Csharpminor.ml coq8.16-compcert-3.11> OCAMLOPT debug/Debug.ml coq8.16-compcert-3.11> OCAMLOPT driver/Linker.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Determinism.ml coq8.16-compcert-3.11> OCAMLC extraction/Parser.mli coq8.16-compcert-3.11> OCAMLC extraction/SelectDiv.mli coq8.16-compcert-3.11> OCAMLOPT driver/Assembler.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Cminorgen.ml coq8.16-compcert-3.11> OCAMLC extraction/Selection.mli coq8.16-compcert-3.11> OCAMLOPT backend/PrintCminor.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Cflow.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Unblock.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Cleanup.ml coq8.16-compcert-3.11> OCAMLOPT debug/DebugInformation.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Memdata.ml coq8.16-compcert-3.11> OCAMLOPT cparser/StructPassing.ml coq8.16-compcert-3.11> OCAMLOPT cparser/PackedStructs.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Validator_complete.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Memory.ml coq8.16-compcert-3.11> OCAMLOPT backend/AisAnnot.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Builtins0.ml coq8.16-compcert-3.11> OCAMLOPT extraction/ValueDomain.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Elab.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Machregs.ml coq8.16-compcert-3.11> OCAMLOPT extraction/RTL.ml coq8.16-compcert-3.11> OCAMLOPT x86/PrintOp.ml coq8.16-compcert-3.11> OCAMLOPT extraction/CminorSel.ml coq8.16-compcert-3.11> OCAMLOPT extraction/CSEdomain.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Cop.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Globalenvs.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Builtins1.ml coq8.16-compcert-3.11> OCAMLOPT backend/RTLgenaux.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Interpreter_complete.ml coq8.16-compcert-3.11> OCAMLOPT extraction/CombineOp.ml coq8.16-compcert-3.11> OCAMLOPT debug/Dwarfgen.ml coq8.16-compcert-3.11> OCAMLC backend/Inliningaux.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Unusedglob.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Renumber.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Liveness.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Locations.ml coq8.16-compcert-3.11> OCAMLOPT backend/Machregsnames.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Mach.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Asm.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Builtins.ml coq8.16-compcert-3.11> OCAMLOPT extraction/RTLgen.ml coq8.16-compcert-3.11> OCAMLC extraction/Inlining.mli coq8.16-compcert-3.11> OCAMLOPT backend/XTL.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Conventions1.ml coq8.16-compcert-3.11> OCAMLOPT extraction/LTL.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Linear.ml coq8.16-compcert-3.11> OCAMLOPT cparser/ExtendedAsm.ml coq8.16-compcert-3.11> OCAMLC extraction/Compiler.mli coq8.16-compcert-3.11> OCAMLOPT extraction/Tunneling.ml coq8.16-compcert-3.11> OCAMLOPT backend/Splitting.ml coq8.16-compcert-3.11> OCAMLOPT backend/Linearizeaux.ml coq8.16-compcert-3.11> OCAMLOPT extraction/CleanupLabels.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Asmgen.ml coq8.16-compcert-3.11> OCAMLOPT backend/Asmexpandaux.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Conventions.ml coq8.16-compcert-3.11> OCAMLOPT backend/PrintXTL.ml coq8.16-compcert-3.11> OCAMLOPT backend/PrintLTL.ml coq8.16-compcert-3.11> OCAMLOPT backend/PrintRTL.ml coq8.16-compcert-3.11> OCAMLOPT backend/PrintMach.ml coq8.16-compcert-3.11> OCAMLOPT backend/PrintAsmaux.ml coq8.16-compcert-3.11> OCAMLOPT debug/DebugInit.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Debugvar.ml coq8.16-compcert-3.11> OCAMLOPT extraction/ValueAOp.ml coq8.16-compcert-3.11> OCAMLOPT extraction/NeedDomain.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Linearize.ml coq8.16-compcert-3.11> OCAMLOPT extraction/RTLtyping.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Tailcall.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Bounds.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Lineartyping.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Csyntax.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Clight.ml coq8.16-compcert-3.11> OCAMLOPT extraction/NeedOp.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Stacklayout.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Main.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Initializers.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Ctyping.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Csem.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Stacking.ml coq8.16-compcert-3.11> OCAMLOPT extraction/SimplLocals.ml coq8.16-compcert-3.11> OCAMLOPT extraction/SimplExpr.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Cshmgen.ml coq8.16-compcert-3.11> OCAMLOPT extraction/ValueAnalysis.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Cexec.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Deadcode.ml coq8.16-compcert-3.11> OCAMLOPT extraction/CSE.ml coq8.16-compcert-3.11> OCAMLOPT debug/DwarfPrinter.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Parser.ml coq8.16-compcert-3.11> OCAMLOPT cfrontend/C2C.ml coq8.16-compcert-3.11> OCAMLOPT x86/Asmexpand.ml coq8.16-compcert-3.11> OCAMLOPT cfrontend/CPragmas.ml coq8.16-compcert-3.11> OCAMLOPT cfrontend/PrintCsyntax.ml coq8.16-compcert-3.11> OCAMLOPT x86/TargetPrinter.ml coq8.16-compcert-3.11> OCAMLOPT extraction/SelectOp.ml coq8.16-compcert-3.11> OCAMLOPT backend/Inliningaux.ml coq8.16-compcert-3.11> OCAMLOPT backend/IRC.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Inlining.ml coq8.16-compcert-3.11> OCAMLOPT cfrontend/PrintClight.ml coq8.16-compcert-3.11> OCAMLOPT driver/Interp.ml coq8.16-compcert-3.11> OCAMLOPT backend/Regalloc.ml coq8.16-compcert-3.11> OCAMLOPT backend/PrintAsm.ml coq8.16-compcert-3.11> OCAMLOPT extraction/SplitLong.ml coq8.16-compcert-3.11> OCAMLOPT extraction/ConstpropOp.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Allocation.ml coq8.16-compcert-3.11> OCAMLOPT extraction/SelectLong.ml coq8.16-compcert-3.11> OCAMLOPT extraction/SelectDiv.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Constprop.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Selection.ml coq8.16-compcert-3.11> OCAMLOPT extraction/Compiler.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Lexer.ml coq8.16-compcert-3.11> OCAMLOPT cparser/Parse.ml coq8.16-compcert-3.11> OCAMLOPT driver/Frontend.ml coq8.16-compcert-3.11> OCAMLOPT driver/Driver.ml coq8.16-compcert-3.11> Linking ccomp coq8.16-compcert-3.11> make[2]: Leaving directory '/build/source' coq8.16-compcert-3.11> make[1]: Leaving directory '/build/source' coq8.16-compcert-3.11> make runtime coq8.16-compcert-3.11> make[1]: Entering directory '/build/source' coq8.16-compcert-3.11> make -C runtime coq8.16-compcert-3.11> make[2]: Entering directory '/build/source/runtime' coq8.16-compcert-3.11> /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_linux -o i64_dtou.o x86_64/i64_dtou.S coq8.16-compcert-3.11> /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_linux -o i64_utod.o x86_64/i64_utod.S coq8.16-compcert-3.11> /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_linux -o i64_utof.o x86_64/i64_utof.S coq8.16-compcert-3.11> /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/cc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_linux -o vararg.o x86_64/vararg.S coq8.16-compcert-3.11> rm -f libcompcert.a coq8.16-compcert-3.11> ar rcs libcompcert.a i64_dtou.o i64_utod.o i64_utof.o vararg.o coq8.16-compcert-3.11> make[2]: Leaving directory '/build/source/runtime' coq8.16-compcert-3.11> make[1]: Leaving directory '/build/source' coq8.16-compcert-3.11> make clightgen coq8.16-compcert-3.11> make[1]: Entering directory '/build/source' coq8.16-compcert-3.11> make -f Makefile.extr clightgen coq8.16-compcert-3.11> make[2]: Entering directory '/build/source' coq8.16-compcert-3.11> OCAMLOPT export/ExportBase.ml coq8.16-compcert-3.11> OCAMLOPT export/Clightnorm.ml coq8.16-compcert-3.11> OCAMLOPT export/ExportCtypes.ml coq8.16-compcert-3.11> OCAMLOPT export/ExportCsyntax.ml coq8.16-compcert-3.11> OCAMLOPT export/ExportClight.ml coq8.16-compcert-3.11> OCAMLOPT export/ExportDriver.ml coq8.16-compcert-3.11> Linking clightgen coq8.16-compcert-3.11> make[2]: Leaving directory '/build/source' coq8.16-compcert-3.11> make[1]: Leaving directory '/build/source' coq8.16-compcert-3.11> make compcert.config coq8.16-compcert-3.11> make[1]: Entering directory '/build/source' coq8.16-compcert-3.11> (echo "# CompCert configuration parameters"; \ coq8.16-compcert-3.11> echo "COMPCERT_ARCH=x86"; \ coq8.16-compcert-3.11> echo "COMPCERT_MODEL=64"; \ coq8.16-compcert-3.11> echo "COMPCERT_ABI=standard"; \ coq8.16-compcert-3.11> echo "COMPCERT_ENDIANNESS=little"; \ coq8.16-compcert-3.11> echo "COMPCERT_BITSIZE=64"; \ coq8.16-compcert-3.11> echo "COMPCERT_SYSTEM=linux"; \ coq8.16-compcert-3.11> echo "COMPCERT_VERSION=3.11"; \ coq8.16-compcert-3.11> echo "COMPCERT_BUILDNR="; \ coq8.16-compcert-3.11> echo "COMPCERT_TAG="; \ coq8.16-compcert-3.11> echo "COMPCERT_BRANCH=" \ coq8.16-compcert-3.11> ) > compcert.config coq8.16-compcert-3.11> make[1]: Leaving directory '/build/source' coq8.16-compcert-3.11> buildPhase completed in 4 minutes 8 seconds coq8.16-compcert-3.11> installing coq8.16-compcert-3.11> install flags: SHELL=/nix/store/4xw8n979xpivdc46a9ndcvyhwgif00hz-bash-5.1-p16/bin/bash documentation install coq8.16-compcert-3.11> mkdir -p doc/html coq8.16-compcert-3.11> rm -f doc/html/*.html coq8.16-compcert-3.11> coq2html -d doc/html/ -base compcert -short-names doc/*.glob \ coq8.16-compcert-3.11> lib/Axioms.v lib/Coqlib.v lib/Intv.v lib/Maps.v lib/Heaps.v lib/Lattice.v lib/Ordered.v lib/Iteration.v lib/Zbits.v lib/Integers.v x86_64/Archi.v lib/IEEE754_extra.v lib/Floats.v lib/Parmov.v lib/UnionFind.v lib/Wfsimpl.v lib/Postorder.v lib/FSetAVLplus.v lib/IntvSets.v lib/Decidableplus.v lib/BoolEqual.v common/Errors.v common/AST.v common/Linking.v common/Events.v common/Globalenvs.v common/Memdata.v common/Memtype.v common/Memory.v common/Values.v common/Smallstep.v common/Behaviors.v common/Switch.v common/Determinism.v common/Unityping.v common/Separation.v common/Builtins0.v x86/Builtins1.v common/Builtins.v backend/Cminor.v backend/Cminortyping.v x86/Op.v backend/CminorSel.v x86/SelectOp.v backend/SelectDiv.v backend/SplitLong.v x86/SelectLong.v backend/Selection.v x86/SelectOpproof.v backend/SelectDivproof.v backend/SplitLongproof.v x86/SelectLongproof.v backend/Selectionproof.v backend/Registers.v backend/RTL.v backend/RTLgen.v backend/RTLgenspec.v backend/RTLgenproof.v backend/Tailcall.v backend/Tailcallproof.v backend/Inlining.v backend/Inliningspec.v backend/Inliningproof.v backend/Renumber.v backend/Renumberproof.v backend/RTLtyping.v backend/Kildall.v backend/Liveness.v backend/ValueDomain.v x86/ValueAOp.v backend/ValueAnalysis.v x86/ConstpropOp.v backend/Constprop.v x86/ConstpropOpproof.v backend/Constpropproof.v backend/CSEdomain.v x86/CombineOp.v backend/CSE.v x86/CombineOpproof.v backend/CSEproof.v backend/NeedDomain.v x86/NeedOp.v backend/Deadcode.v backend/Deadcodeproof.v backend/Unusedglob.v backend/Unusedglobproof.v x86/Machregs.v backend/Locations.v x86/Conventions1.v backend/Conventions.v backend/LTL.v backend/Allocation.v backend/Allocproof.v backend/Tunneling.v backend/Tunnelingproof.v backend/Linear.v backend/Lineartyping.v backend/Linearize.v backend/Linearizeproof.v backend/CleanupLabels.v backend/CleanupLabelsproof.v backend/Debugvar.v backend/Debugvarproof.v backend/Mach.v backend/Bounds.v x86/Stacklayout.v backend/Stacking.v backend/Stackingproof.v x86/Asm.v x86/Asmgen.v backend/Asmgenproof0.v x86/Asmgenproof1.v x86/Asmgenproof.v cfrontend/Ctypes.v cfrontend/Cop.v cfrontend/Csyntax.v cfrontend/Csem.v cfrontend/Ctyping.v cfrontend/Cstrategy.v cfrontend/Cexec.v cfrontend/Initializers.v cfrontend/Initializersproof.v cfrontend/SimplExpr.v cfrontend/SimplExprspec.v cfrontend/SimplExprproof.v cfrontend/Clight.v cfrontend/ClightBigstep.v cfrontend/SimplLocals.v cfrontend/SimplLocalsproof.v cfrontend/Cshmgen.v cfrontend/Cshmgenproof.v cfrontend/Csharpminor.v cfrontend/Cminorgen.v cfrontend/Cminorgenproof.v driver/Compopts.v driver/Compiler.v driver/Complements.v MenhirLib/Alphabet.v MenhirLib/Automaton.v MenhirLib/Grammar.v MenhirLib/Interpreter_complete.v MenhirLib/Interpreter_correct.v MenhirLib/Interpreter.v MenhirLib/Main.v MenhirLib/Validator_complete.v MenhirLib/Validator_safe.v MenhirLib/Validator_classes.v cparser/Cabs.v export/Ctypesdefs.v export/Clightdefs.v export/Csyntaxdefs.v coq8.16-compcert-3.11> install -d /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/bin coq8.16-compcert-3.11> install -m 0755 ./ccomp /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/bin coq8.16-compcert-3.11> install -d /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/share coq8.16-compcert-3.11> install -m 0644 ./compcert.ini /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/share coq8.16-compcert-3.11> install -d /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/share/man/man1 coq8.16-compcert-3.11> install -m 0644 ./doc/ccomp.1 /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/share/man/man1 coq8.16-compcert-3.11> make -C runtime install coq8.16-compcert-3.11> make[1]: Entering directory '/build/source/runtime' coq8.16-compcert-3.11> install -d /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/lib/compcert coq8.16-compcert-3.11> install -m 0644 libcompcert.a /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/lib/compcert coq8.16-compcert-3.11> install -d /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/lib/compcert/include coq8.16-compcert-3.11> install -m 0644 include/float.h include/stdarg.h include/stdbool.h include/stddef.h include/varargs.h include/stdalign.h include/stdnoreturn.h /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/lib/compcert/include coq8.16-compcert-3.11> make[1]: Leaving directory '/build/source/runtime' coq8.16-compcert-3.11> install -m 0755 ./clightgen /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/bin coq8.16-compcert-3.11> install -d /nix/store/z8f4wg6bqyg2b9djzsmgf8flgp7dmqss-coq8.16-compcert-3.11-lib/lib/coq/8.16/user-contrib/compcert/ coq8.16-compcert-3.11> for d in lib common x86_64 x86 backend cfrontend driver export cparser MenhirLib; do \ coq8.16-compcert-3.11> install -d /nix/store/z8f4wg6bqyg2b9djzsmgf8flgp7dmqss-coq8.16-compcert-3.11-lib/lib/coq/8.16/user-contrib/compcert//$d && \ coq8.16-compcert-3.11> install -m 0644 $d/*.vo /nix/store/z8f4wg6bqyg2b9djzsmgf8flgp7dmqss-coq8.16-compcert-3.11-lib/lib/coq/8.16/user-contrib/compcert//$d/; \ coq8.16-compcert-3.11> done coq8.16-compcert-3.11> install -m 0644 ./VERSION /nix/store/z8f4wg6bqyg2b9djzsmgf8flgp7dmqss-coq8.16-compcert-3.11-lib/lib/coq/8.16/user-contrib/compcert/ coq8.16-compcert-3.11> install -m 0644 ./compcert.config /nix/store/z8f4wg6bqyg2b9djzsmgf8flgp7dmqss-coq8.16-compcert-3.11-lib/lib/coq/8.16/user-contrib/compcert/ coq8.16-compcert-3.11> post-installation fixup coq8.16-compcert-3.11> shrinking RPATHs of ELF executables and libraries in /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11 coq8.16-compcert-3.11> shrinking /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/bin/.clightgen-wrapped coq8.16-compcert-3.11> shrinking /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/bin/.ccomp-wrapped coq8.16-compcert-3.11> strip is /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/strip coq8.16-compcert-3.11> stripping (with command strip and flags -S) in /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/lib /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11/bin coq8.16-compcert-3.11> patching script interpreter paths in /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11 coq8.16-compcert-3.11> checking for references to /build/ in /nix/store/wnh96zvarryhnfhlibhf2j4h3y3flq76-coq8.16-compcert-3.11... coq8.16-compcert-3.11> shrinking RPATHs of ELF executables and libraries in /nix/store/z8f4wg6bqyg2b9djzsmgf8flgp7dmqss-coq8.16-compcert-3.11-lib coq8.16-compcert-3.11> strip is /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/strip coq8.16-compcert-3.11> stripping (with command strip and flags -S) in /nix/store/z8f4wg6bqyg2b9djzsmgf8flgp7dmqss-coq8.16-compcert-3.11-lib/lib coq8.16-compcert-3.11> patching script interpreter paths in /nix/store/z8f4wg6bqyg2b9djzsmgf8flgp7dmqss-coq8.16-compcert-3.11-lib coq8.16-compcert-3.11> checking for references to /build/ in /nix/store/z8f4wg6bqyg2b9djzsmgf8flgp7dmqss-coq8.16-compcert-3.11-lib... coq8.16-compcert-3.11> shrinking RPATHs of ELF executables and libraries in /nix/store/anj8pl77n2hkz69fwd40xbwgqsgs0mmd-coq8.16-compcert-3.11-doc coq8.16-compcert-3.11> strip is /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/strip coq8.16-compcert-3.11> patching script interpreter paths in /nix/store/anj8pl77n2hkz69fwd40xbwgqsgs0mmd-coq8.16-compcert-3.11-doc coq8.16-compcert-3.11> checking for references to /build/ in /nix/store/anj8pl77n2hkz69fwd40xbwgqsgs0mmd-coq8.16-compcert-3.11-doc... coq8.16-compcert-3.11> shrinking RPATHs of ELF executables and libraries in /nix/store/dr61lj6jjfihkw63y7w1sldbqcyhfxzx-coq8.16-compcert-3.11-man coq8.16-compcert-3.11> gzipping man pages under /nix/store/dr61lj6jjfihkw63y7w1sldbqcyhfxzx-coq8.16-compcert-3.11-man/share/man/ coq8.16-compcert-3.11> strip is /nix/store/wn31i3dzwahz6ccws8bs1nwyqrpgsvj7-gcc-wrapper-11.3.0/bin/strip coq8.16-compcert-3.11> patching script interpreter paths in /nix/store/dr61lj6jjfihkw63y7w1sldbqcyhfxzx-coq8.16-compcert-3.11-man coq8.16-compcert-3.11> checking for references to /build/ in /nix/store/dr61lj6jjfihkw63y7w1sldbqcyhfxzx-coq8.16-compcert-3.11-man... upload niks3: ok