WARNING: (guile-user): imported module (guix build utils) overrides core binding `delete'
starting phase `set-SOURCE-DATE-EPOCH'
phase `set-SOURCE-DATE-EPOCH' succeeded after 0.0 seconds
starting phase `set-paths'
environment variable `PATH' set to `/gnu/store/kl6nfdbxxblvzbi4rf5fl8bp80clrk6p-ocaml-4.11.1/bin:/gnu/store/k4r8r6k6bdr7p2p7m74ifamwbnkm5wqw-coq-8.11.2/bin:/gnu/store/wiv0qy4wc58iwhgwwn5frq8paxyh2vjq-camlp5-7.13/bin:/gnu/store/v6f44zccwh9z5zk3pjlywjybbi8n2hjh-tar-1.32/bin:/gnu/store/ncydgq2znms5n1d2k5yqshhf58nsixwv-gzip-1.10/bin:/gnu/store/i8h2pcxqdq07ijm3ibkka8f4smn1w48v-bzip2-1.0.8/bin:/gnu/store/9860f1abqj8wjjnwl8a9v54pdcc3bhgf-xz-5.2.4/bin:/gnu/store/60g7r3l01fd7c58yjbm6krgcwj1jkpwg-file-5.38/bin:/gnu/store/n4n560pfvvw50a9369axw5vj5rrqfj1n-diffutils-3.7/bin:/gnu/store/cd5qf3kcnlq35p9k392pjdpdzpsnds70-patch-2.7.6/bin:/gnu/store/hic7snhayfl7m6cpfqqr73nmm19bpqkg-findutils-4.7.0/bin:/gnu/store/swqdvwri9dbv6zssg6v0by7l05hd6wxp-gawk-5.0.1/bin:/gnu/store/ishk7fswcs4gkwcp8mh788z4mvvl9bxh-sed-4.8/bin:/gnu/store/bhs4rj58v8j1narb2454raan2ps38xd8-grep-3.4/bin:/gnu/store/57xj5gcy1jbl9ai2lnrqnpr0dald9i65-coreutils-8.32/bin:/gnu/store/hm40bxnv8jxmbc1lpb7zfimii4xm9m81-make-4.3/bin:/gnu/store/pwcp239kjf7lnj5i4lkdzcfcxwcfyk72-bash-minimal-5.0.16/bin:/gnu/store/mpa04aq8lblbcviyxywxcsb1zbi0mf39-ld-wrapper-0/bin:/gnu/store/m1z7cdbqsqyp9xnjw5cvlb4a7gkcg3m4-binutils-2.34/bin:/gnu/store/rn75fm7adgx3pw5j8pg3bczfqq1y17lk-gcc-7.5.0/bin:/gnu/store/fa6wj5bxkj5ll1d7292a70knmyl7a0cr-glibc-2.31/bin:/gnu/store/fa6wj5bxkj5ll1d7292a70knmyl7a0cr-glibc-2.31/sbin'
environment variable `OCAMLPATH' set to `/gnu/store/kl6nfdbxxblvzbi4rf5fl8bp80clrk6p-ocaml-4.11.1/lib/ocaml:/gnu/store/k4r8r6k6bdr7p2p7m74ifamwbnkm5wqw-coq-8.11.2/lib/ocaml:/gnu/store/k4r8r6k6bdr7p2p7m74ifamwbnkm5wqw-coq-8.11.2/lib/ocaml/site-lib:/gnu/store/wiv0qy4wc58iwhgwwn5frq8paxyh2vjq-camlp5-7.13/lib/ocaml'
environment variable `CAML_LD_LIBRARY_PATH' unset
environment variable `COQPATH' set to `/gnu/store/k4r8r6k6bdr7p2p7m74ifamwbnkm5wqw-coq-8.11.2/lib/coq/user-contrib'
environment variable `BASH_LOADABLES_PATH' unset
environment variable `C_INCLUDE_PATH' set to `/gnu/store/i8h2pcxqdq07ijm3ibkka8f4smn1w48v-bzip2-1.0.8/include:/gnu/store/9860f1abqj8wjjnwl8a9v54pdcc3bhgf-xz-5.2.4/include:/gnu/store/60g7r3l01fd7c58yjbm6krgcwj1jkpwg-file-5.38/include:/gnu/store/swqdvwri9dbv6zssg6v0by7l05hd6wxp-gawk-5.0.1/include:/gnu/store/hm40bxnv8jxmbc1lpb7zfimii4xm9m81-make-4.3/include:/gnu/store/m1z7cdbqsqyp9xnjw5cvlb4a7gkcg3m4-binutils-2.34/include:/gnu/store/rn75fm7adgx3pw5j8pg3bczfqq1y17lk-gcc-7.5.0/include:/gnu/store/fa6wj5bxkj5ll1d7292a70knmyl7a0cr-glibc-2.31/include:/gnu/store/gfapkk5c6hvl1d94m4sqnhn7f9l5gqyh-linux-libre-headers-5.4.20/include'
environment variable `CPLUS_INCLUDE_PATH' set to `/gnu/store/i8h2pcxqdq07ijm3ibkka8f4smn1w48v-bzip2-1.0.8/include:/gnu/store/9860f1abqj8wjjnwl8a9v54pdcc3bhgf-xz-5.2.4/include:/gnu/store/60g7r3l01fd7c58yjbm6krgcwj1jkpwg-file-5.38/include:/gnu/store/swqdvwri9dbv6zssg6v0by7l05hd6wxp-gawk-5.0.1/include:/gnu/store/hm40bxnv8jxmbc1lpb7zfimii4xm9m81-make-4.3/include:/gnu/store/m1z7cdbqsqyp9xnjw5cvlb4a7gkcg3m4-binutils-2.34/include:/gnu/store/rn75fm7adgx3pw5j8pg3bczfqq1y17lk-gcc-7.5.0/include/c++:/gnu/store/rn75fm7adgx3pw5j8pg3bczfqq1y17lk-gcc-7.5.0/include:/gnu/store/fa6wj5bxkj5ll1d7292a70knmyl7a0cr-glibc-2.31/include:/gnu/store/gfapkk5c6hvl1d94m4sqnhn7f9l5gqyh-linux-libre-headers-5.4.20/include'
environment variable `LIBRARY_PATH' set to `/gnu/store/kl6nfdbxxblvzbi4rf5fl8bp80clrk6p-ocaml-4.11.1/lib:/gnu/store/k4r8r6k6bdr7p2p7m74ifamwbnkm5wqw-coq-8.11.2/lib:/gnu/store/wiv0qy4wc58iwhgwwn5frq8paxyh2vjq-camlp5-7.13/lib:/gnu/store/i8h2pcxqdq07ijm3ibkka8f4smn1w48v-bzip2-1.0.8/lib:/gnu/store/9860f1abqj8wjjnwl8a9v54pdcc3bhgf-xz-5.2.4/lib:/gnu/store/60g7r3l01fd7c58yjbm6krgcwj1jkpwg-file-5.38/lib:/gnu/store/swqdvwri9dbv6zssg6v0by7l05hd6wxp-gawk-5.0.1/lib:/gnu/store/m1z7cdbqsqyp9xnjw5cvlb4a7gkcg3m4-binutils-2.34/lib:/gnu/store/fa6wj5bxkj5ll1d7292a70knmyl7a0cr-glibc-2.31/lib:/gnu/store/s3dcqzwqaakv1yx37by9chksdbkgih17-glibc-2.31-static/lib:/gnu/store/hwcky7446s952w0mwchhmm211ll07zrq-glibc-utf8-locales-2.31/lib'
environment variable `GUIX_LOCPATH' set to `/gnu/store/hwcky7446s952w0mwchhmm211ll07zrq-glibc-utf8-locales-2.31/lib/locale'
phase `set-paths' succeeded after 0.1 seconds
starting phase `install-locale'
using 'en_US.utf8' locale for category "LC_ALL"
phase `install-locale' succeeded after 0.0 seconds
starting phase `unpack'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/.travis.yml' -> `./.travis.yml'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/default.nix' -> `./default.nix'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/meta.yml' -> `./meta.yml'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/Makefile' -> `./Makefile'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/coq-bignums.opam' -> `./coq-bignums.opam'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/LICENSE' -> `./LICENSE'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/_CoqProject' -> `./_CoqProject'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/BigNumPrelude.v' -> `./BigNumPrelude.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/README.md' -> `./README.md'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/dune' -> `./dune'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/dune-project' -> `./dune-project'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/.gitignore' -> `./.gitignore'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/BigQ/QMake.v' -> `./BigQ/QMake.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/BigQ/BigQ.v' -> `./BigQ/BigQ.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/BigZ/BigZ.v' -> `./BigZ/BigZ.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/BigZ/ZMake.v' -> `./BigZ/ZMake.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/tests/dune' -> `./tests/dune'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/tests/output/NumbersSyntax.v' -> `./tests/output/NumbersSyntax.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/tests/output/NumbersSyntax.out' -> `./tests/output/NumbersSyntax.out'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/tests/success/NumberScopes.v' -> `./tests/success/NumberScopes.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/tests/success/bigQ.v' -> `./tests/success/bigQ.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/SpecViaQ/QSig.v' -> `./SpecViaQ/QSig.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/BigN/NMake.v' -> `./BigN/NMake.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/BigN/dune' -> `./BigN/dune'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/BigN/BigN.v' -> `./BigN/BigN.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/BigN/Nbasic.v' -> `./BigN/Nbasic.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/BigN/gen/dune' -> `./BigN/gen/dune'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/BigN/gen/NMake_gen.ml' -> `./BigN/gen/NMake_gen.ml'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/plugin/bignums_syntax.ml' -> `./plugin/bignums_syntax.ml'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/plugin/dune' -> `./plugin/dune'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/plugin/bignums_syntax_plugin.mlpack' -> `./plugin/bignums_syntax_plugin.mlpack'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/CyclicDouble/DoubleMul.v' -> `./CyclicDouble/DoubleMul.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/CyclicDouble/DoubleSub.v' -> `./CyclicDouble/DoubleSub.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/CyclicDouble/DoubleDivn1.v' -> `./CyclicDouble/DoubleDivn1.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/CyclicDouble/DoubleBase.v' -> `./CyclicDouble/DoubleBase.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/CyclicDouble/DoubleSqrt.v' -> `./CyclicDouble/DoubleSqrt.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/CyclicDouble/DoubleDiv.v' -> `./CyclicDouble/DoubleDiv.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/CyclicDouble/DoubleAdd.v' -> `./CyclicDouble/DoubleAdd.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/CyclicDouble/DoubleLift.v' -> `./CyclicDouble/DoubleLift.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/CyclicDouble/DoubleCyclic.v' -> `./CyclicDouble/DoubleCyclic.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/SpecViaZ/NSig.v' -> `./SpecViaZ/NSig.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/SpecViaZ/ZSigZAxioms.v' -> `./SpecViaZ/ZSigZAxioms.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/SpecViaZ/NSigNAxioms.v' -> `./SpecViaZ/NSigNAxioms.v'
`/gnu/store/mk8x540zs0pml5rs3spg12g6m2frr6yp-coq-bignums-8.11.0-checkout/SpecViaZ/ZSig.v' -> `./SpecViaZ/ZSig.v'
phase `unpack' succeeded after 0.3 seconds
starting phase `bootstrap'
no 'configure.ac' or anything like that, doing nothing
phase `bootstrap' succeeded after 0.0 seconds
starting phase `patch-usr-bin-file'
phase `patch-usr-bin-file' succeeded after 0.0 seconds
starting phase `patch-source-shebangs'
phase `patch-source-shebangs' succeeded after 0.0 seconds
starting phase `patch-generated-file-shebangs'
phase `patch-generated-file-shebangs' succeeded after 0.0 seconds
starting phase `build'
coq_makefile -f _CoqProject -o Makefile.coq
Warning: -extra and -extra-phony are deprecated.
Warning: Write the extra targets in Makefile.coq.local.

make -f Makefile.coq Makefile
make[1]: Entering directory '/tmp/guix-build-coq-bignums-8.11.0.drv-0/source'
ocaml BigN/gen/NMake_gen.ml > BigN/NMake_gen.v || (RV=$?; rm -f BigN/NMake_gen.v; exit ${RV})
COQDEP plugin/bignums_syntax_plugin.mlpack
CAMLDEP plugin/bignums_syntax.ml
COQDEP VFILES
make[1]: Nothing to be done for 'Makefile'.
make[1]: Leaving directory '/tmp/guix-build-coq-bignums-8.11.0.drv-0/source'
make -f Makefile.coq all
make[1]: Entering directory '/tmp/guix-build-coq-bignums-8.11.0.drv-0/source'
CAMLOPT -c -for-pack Bignums_syntax_plugin plugin/bignums_syntax.ml
COQC SpecViaZ/NSig.v
COQC SpecViaZ/ZSig.v
COQC SpecViaQ/QSig.v
CAMLOPT -pack -o plugin/bignums_syntax_plugin.cmx
CAMLOPT -a -o plugin/bignums_syntax_plugin.cmxa
CAMLOPT -shared -o plugin/bignums_syntax_plugin.cmxs
COQC BigNumPrelude.v
COQC SpecViaZ/ZSigZAxioms.v
COQC SpecViaZ/NSigNAxioms.v
File "./BigNumPrelude.v", line 52, characters 0-242:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./BigNumPrelude.v", line 59, characters 0-227:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
COQC CyclicDouble/DoubleBase.v
COQC BigZ/ZMake.v
COQC BigQ/QMake.v
COQC CyclicDouble/DoubleMul.v
COQC CyclicDouble/DoubleAdd.v
COQC CyclicDouble/DoubleSub.v
COQC CyclicDouble/DoubleSqrt.v
COQC CyclicDouble/DoubleLift.v
COQC CyclicDouble/DoubleDivn1.v
File "./CyclicDouble/DoubleSqrt.v", line 676, characters 1-23:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
COQC CyclicDouble/DoubleDiv.v
COQC CyclicDouble/DoubleCyclic.v
File "./CyclicDouble/DoubleCyclic.v", line 825, characters 1-26:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
COQC BigN/Nbasic.v
COQC BigN/NMake_gen.v
File "./BigN/NMake_gen.v", line 270, characters 1-179:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./BigN/NMake_gen.v", line 591, characters 1-68:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./BigN/NMake_gen.v", line 601, characters 1-76:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./BigN/NMake_gen.v", line 609, characters 1-119:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./BigN/NMake_gen.v", line 617, characters 1-119:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
COQC BigN/NMake.v
File "./BigN/NMake.v", line 250, characters 1-141:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
COQC BigN/BigN.v
COQC BigZ/BigZ.v
COQC BigQ/BigQ.v
make -f Makefile.coq BigN/NMake_gen.v
make[3]: 'BigN/NMake_gen.v' is up to date.
make[1]: Leaving directory '/tmp/guix-build-coq-bignums-8.11.0.drv-0/source'
phase `build' succeeded after 55.2 seconds
starting phase `check'
test suite not run
phase `check' succeeded after 0.0 seconds
starting phase `install'
make -f Makefile.coq Makefile
make[1]: Entering directory '/tmp/guix-build-coq-bignums-8.11.0.drv-0/source'
make[1]: Nothing to be done for 'Makefile'.
make[1]: Leaving directory '/tmp/guix-build-coq-bignums-8.11.0.drv-0/source'
make -f Makefile.coq install
make[1]: Entering directory '/tmp/guix-build-coq-bignums-8.11.0.drv-0/source'
INSTALL BigN/Nbasic.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake_gen.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/BigN.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL SpecViaZ/NSig.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSig.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/NSigNAxioms.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSigZAxioms.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaQ/QSig.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaQ
INSTALL BigQ/QMake.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL BigQ/BigQ.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL CyclicDouble/DoubleBase.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleAdd.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDiv.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleMul.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSub.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDivn1.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSqrt.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleCyclic.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleLift.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL BigNumPrelude.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums/
INSTALL BigZ/ZMake.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL BigZ/BigZ.vo /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL BigN/Nbasic.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake_gen.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/BigN.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL SpecViaZ/NSig.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSig.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/NSigNAxioms.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSigZAxioms.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaQ/QSig.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaQ
INSTALL BigQ/QMake.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL BigQ/BigQ.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL CyclicDouble/DoubleBase.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleAdd.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDiv.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleMul.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSub.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDivn1.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSqrt.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleCyclic.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleLift.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL BigNumPrelude.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums/
INSTALL BigZ/ZMake.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL BigZ/BigZ.v /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL BigN/Nbasic.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake_gen.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/BigN.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigN
INSTALL SpecViaZ/NSig.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSig.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/NSigNAxioms.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSigZAxioms.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaQ/QSig.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//SpecViaQ
INSTALL BigQ/QMake.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL BigQ/BigQ.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL CyclicDouble/DoubleBase.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleAdd.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDiv.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleMul.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSub.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDivn1.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSqrt.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleCyclic.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleLift.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL BigNumPrelude.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums/
INSTALL BigZ/ZMake.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL BigZ/BigZ.glob /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL plugin/bignums_syntax_plugin.cmi /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmxs /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmxs /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmxa /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmx /gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib/coq/user-contrib/Bignums//plugin
make[2]: Entering directory '/tmp/guix-build-coq-bignums-8.11.0.drv-0/source'
make[2]: Leaving directory '/tmp/guix-build-coq-bignums-8.11.0.drv-0/source'
make[1]: Leaving directory '/tmp/guix-build-coq-bignums-8.11.0.drv-0/source'
phase `install' succeeded after 1.2 seconds
starting phase `patch-shebangs'
phase `patch-shebangs' succeeded after 0.0 seconds
starting phase `strip'
stripping binaries in "/gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib" with "strip" and flags ("--strip-debug" "--enable-deterministic-archives")
phase `strip' succeeded after 0.0 seconds
starting phase `validate-runpath'
validating RUNPATH of 1 binaries in "/gnu/store/kfy5rqijgnp9abdp996hdkd967s9xml7-coq-bignums-8.11.0/lib"...
phase `validate-runpath' succeeded after 0.0 seconds
starting phase `validate-documentation-location'
phase `validate-documentation-location' succeeded after 0.0 seconds
starting phase `delete-info-dir-file'
phase `delete-info-dir-file' succeeded after 0.0 seconds
starting phase `patch-dot-desktop-files'
phase `patch-dot-desktop-files' succeeded after 0.0 seconds
starting phase `install-license-files'
installing 1 license files from '.'
phase `install-license-files' succeeded after 0.0 seconds
starting phase `reset-gzip-timestamps'
phase `reset-gzip-timestamps' succeeded after 0.0 seconds
starting phase `compress-documentation'
phase `compress-documentation' succeeded after 0.0 seconds