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/0n43gkkd4565sii8qv31asjj9b4n3rqy-ocaml-4.11.1/bin:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/bin:/gnu/store/6h907snwcc3gjcxi6b41wx8nzim3390q-camlp5-7.13/bin:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/bin:/gnu/store/am3imbjafa1wdvw9j6qabrxc09w169lz-tar-1.32/bin:/gnu/store/chqjscapsg928dy8pg6yrdhw3ypk8c9x-gzip-1.10/bin:/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/bin:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/bin:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/bin:/gnu/store/m8fnsfqs18c3srjiaw4frqadb9rqsq16-diffutils-3.7/bin:/gnu/store/2cfnrxy8icrz3sxfn86k0klmvsnj1n82-patch-2.7.6/bin:/gnu/store/0bmzacdzdhi41kkjbsq7iakwjzxkv6fm-findutils-4.7.0/bin:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/bin:/gnu/store/qy7gpiba7s7ylpfxaay6i76rk892j52n-sed-4.8/bin:/gnu/store/74d5jq5sj2fhy5j0j07jqdclf8nyxgqn-grep-3.4/bin:/gnu/store/wy177cwa387g9kaf3ss716d4fhzb21wx-coreutils-8.32/bin:/gnu/store/wsxnp4k7mp7b705kxp94j7hs8as5fmsl-make-4.3/bin:/gnu/store/7zp9ifpgm3zj481nk6jg1im13g4mza2g-bash-minimal-5.0.16/bin:/gnu/store/y4iy1jvfq07gxynkb9jl1f69jmy349vi-ld-wrapper-0/bin:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/bin:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/bin:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/bin:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/sbin'
environment variable `OCAMLPATH' set to `/gnu/store/0n43gkkd4565sii8qv31asjj9b4n3rqy-ocaml-4.11.1/lib/ocaml:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml/site-lib:/gnu/store/6h907snwcc3gjcxi6b41wx8nzim3390q-camlp5-7.13/lib/ocaml:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/lib/ocaml:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/lib/ocaml/site-lib'
environment variable `CAML_LD_LIBRARY_PATH' set to `/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml/site-lib/stublibs:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/lib/ocaml/site-lib/stublibs'
environment variable `COQPATH' unset
environment variable `COQLIB' set to `/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml/site-lib/coq'
environment variable `BASH_LOADABLES_PATH' unset
environment variable `C_INCLUDE_PATH' set to `/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/include:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/include:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/include:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/include:/gnu/store/wsxnp4k7mp7b705kxp94j7hs8as5fmsl-make-4.3/include:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/include:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/include:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/include:/gnu/store/72z9rxrrmfw1xx9gf27jm2s8h5h0fkh0-linux-libre-headers-5.4.20/include'
environment variable `CPLUS_INCLUDE_PATH' set to `/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/include:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/include:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/include:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/include:/gnu/store/wsxnp4k7mp7b705kxp94j7hs8as5fmsl-make-4.3/include:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/include:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/include/c++:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/include:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/include:/gnu/store/72z9rxrrmfw1xx9gf27jm2s8h5h0fkh0-linux-libre-headers-5.4.20/include'
environment variable `LIBRARY_PATH' set to `/gnu/store/0n43gkkd4565sii8qv31asjj9b4n3rqy-ocaml-4.11.1/lib:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib:/gnu/store/6h907snwcc3gjcxi6b41wx8nzim3390q-camlp5-7.13/lib:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/lib:/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/lib:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/lib:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/lib:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/lib:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/lib:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/lib:/gnu/store/m4l52mw8m0amgy4j129z5j0syryb7pkg-glibc-2.31-static/lib:/gnu/store/vispxhcwmvasm225pm373jhfn21q1sa1-glibc-utf8-locales-2.31/lib'
environment variable `GUIX_LOCPATH' set to `/gnu/store/vispxhcwmvasm225pm373jhfn21q1sa1-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/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/.gitignore' -> `./.gitignore'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/BigNumPrelude.v' -> `./BigNumPrelude.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/LICENSE' -> `./LICENSE'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/Makefile' -> `./Makefile'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/Makefile.coq.local' -> `./Makefile.coq.local'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/README.md' -> `./README.md'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/_CoqProject' -> `./_CoqProject'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/coq-bignums.opam' -> `./coq-bignums.opam'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/default.nix' -> `./default.nix'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/dune' -> `./dune'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/dune-project' -> `./dune-project'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/meta.yml' -> `./meta.yml'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/tests/Makefile' -> `./tests/Makefile'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/tests/dune' -> `./tests/dune'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/tests/success/NumberScopes.v' -> `./tests/success/NumberScopes.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/tests/success/bigQ.v' -> `./tests/success/bigQ.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/tests/output/NumbersSyntax.out' -> `./tests/output/NumbersSyntax.out'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/tests/output/NumbersSyntax.v' -> `./tests/output/NumbersSyntax.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/plugin/bignums_syntax.ml' -> `./plugin/bignums_syntax.ml'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/plugin/bignums_syntax_plugin.mlpack' -> `./plugin/bignums_syntax_plugin.mlpack'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/plugin/dune' -> `./plugin/dune'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/SpecViaZ/NSig.v' -> `./SpecViaZ/NSig.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/SpecViaZ/NSigNAxioms.v' -> `./SpecViaZ/NSigNAxioms.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/SpecViaZ/ZSig.v' -> `./SpecViaZ/ZSig.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/SpecViaZ/ZSigZAxioms.v' -> `./SpecViaZ/ZSigZAxioms.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/SpecViaQ/QSig.v' -> `./SpecViaQ/QSig.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/CyclicDouble/DoubleAdd.v' -> `./CyclicDouble/DoubleAdd.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/CyclicDouble/DoubleBase.v' -> `./CyclicDouble/DoubleBase.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/CyclicDouble/DoubleCyclic.v' -> `./CyclicDouble/DoubleCyclic.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/CyclicDouble/DoubleDiv.v' -> `./CyclicDouble/DoubleDiv.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/CyclicDouble/DoubleDivn1.v' -> `./CyclicDouble/DoubleDivn1.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/CyclicDouble/DoubleLift.v' -> `./CyclicDouble/DoubleLift.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/CyclicDouble/DoubleMul.v' -> `./CyclicDouble/DoubleMul.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/CyclicDouble/DoubleSqrt.v' -> `./CyclicDouble/DoubleSqrt.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/CyclicDouble/DoubleSub.v' -> `./CyclicDouble/DoubleSub.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/BigZ/BigZ.v' -> `./BigZ/BigZ.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/BigZ/ZMake.v' -> `./BigZ/ZMake.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/BigQ/BigQ.v' -> `./BigQ/BigQ.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/BigQ/QMake.v' -> `./BigQ/QMake.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/BigN/BigN.v' -> `./BigN/BigN.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/BigN/NMake.v' -> `./BigN/NMake.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/BigN/Nbasic.v' -> `./BigN/Nbasic.v'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/BigN/dune' -> `./BigN/dune'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/BigN/gen/NMake_gen.ml' -> `./BigN/gen/NMake_gen.ml'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/BigN/gen/dune' -> `./BigN/gen/dune'
`/gnu/store/7fzpriy8ix4jh3ljmx4371p79aswzghf-coq-bignums-8.13.0-checkout/.github/workflows/build-coq-bignums.yml' -> `./.github/workflows/build-coq-bignums.yml'
phase `unpack' succeeded after 0.0 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.13.0.drv-0/source'
ocaml BigN/gen/NMake_gen.ml > BigN/NMake_gen.v || (RV=$?; rm -f BigN/NMake_gen.v; exit ${RV})
OCAMLLIBDEP 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.13.0.drv-0/source'
make -f Makefile.coq all
make[1]: Entering directory '/tmp/guix-build-coq-bignums-8.13.0.drv-0/source'
CAMLOPT -c -for-pack Bignums_syntax_plugin plugin/bignums_syntax.ml
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
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 52, characters 0-242:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,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]
File "./BigNumPrelude.v", line 59, characters 0-227:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./BigNumPrelude.v", line 67, characters 0-47:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./BigNumPrelude.v", line 235, characters 2-8:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigNumPrelude.v", line 235, characters 9-15:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigNumPrelude.v", line 305, characters 1-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
COQC CyclicDouble/DoubleBase.v
COQC CyclicDouble/DoubleAdd.v
COQC CyclicDouble/DoubleSub.v
COQC CyclicDouble/DoubleMul.v
COQC CyclicDouble/DoubleSqrt.v
File "./CyclicDouble/DoubleAdd.v", line 186, characters 23-68:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleAdd.v", line 191, characters 29-74:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleSub.v", line 203, characters 4-64:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleSub.v", line 207, characters 4-64:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleSub.v", line 222, characters 4-64:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleSub.v", line 246, characters 5-65:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleSub.v", line 252, characters 5-65:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleAdd.v", line 277, characters 4-65:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleMul.v", line 336, characters 5-11:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleMul.v", line 343, characters 12-47:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
COQC CyclicDouble/DoubleLift.v
File "./CyclicDouble/DoubleSub.v", line 310, characters 4-63:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
COQC CyclicDouble/DoubleDivn1.v
File "./CyclicDouble/DoubleDivn1.v", line 105, characters 30-36:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDivn1.v", line 200, characters 30-36:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleMul.v", line 517, characters 3-9:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDivn1.v", line 379, characters 60-66:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDivn1.v", line 383, characters 4-47:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
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]
File "./CyclicDouble/DoubleDivn1.v", line 404, characters 4-35:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
COQC SpecViaZ/NSig.v
File "./CyclicDouble/DoubleLift.v", line 341, characters 3-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleLift.v", line 348, characters 3-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
COQC SpecViaZ/ZSig.v
COQC CyclicDouble/DoubleDiv.v
COQC SpecViaZ/NSigNAxioms.v
COQC SpecViaZ/ZSigZAxioms.v
File "./CyclicDouble/DoubleDiv.v", line 321, characters 49-55:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDiv.v", line 325, characters 45-51:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 194, characters 14-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDiv.v", line 420, characters 3-25:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDiv.v", line 424, characters 22-31:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDiv.v", line 427, characters 48-54:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDiv.v", line 440, characters 36-42:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 205, characters 14-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDiv.v", line 547, characters 46-68:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
COQC BigQ/QMake.v
COQC BigZ/ZMake.v
File "./CyclicDouble/DoubleDiv.v", line 1013, characters 28-47:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDiv.v", line 1014, characters 28-48:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigZ/ZMake.v", line 102, characters 14-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigZ/ZMake.v", line 103, characters 32-38:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigZ/ZMake.v", line 106, characters 32-38:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigZ/ZMake.v", line 107, characters 14-20:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDiv.v", line 1037, characters 3-42:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigZ/ZMake.v", line 232, characters 1-199:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigZ/ZMake.v", line 252, characters 1-138:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigZ/ZMake.v", line 277, characters 1-198:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDiv.v", line 1210, characters 3-32:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./CyclicDouble/DoubleDiv.v", line 1232, characters 3-32:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigZ/ZMake.v", line 441, characters 55-67:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigZ/ZMake.v", line 456, characters 55-67:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
COQC CyclicDouble/DoubleCyclic.v
File "./CyclicDouble/DoubleCyclic.v", line 585, characters 35-41:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
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
File "./BigN/Nbasic.v", line 296, characters 8-9:
Warning: Unused variable r catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
File "./BigN/Nbasic.v", line 342, characters 2-54:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigN/Nbasic.v", line 354, characters 8-9:
Warning: Unused variable r catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
File "./BigN/Nbasic.v", line 400, characters 1-53:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
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 448, characters 37-39:
Warning: Unused variable m' catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
File "./BigN/NMake_gen.v", line 448, characters 37-39:
Warning: Unused variable m' catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
File "./BigN/NMake_gen.v", line 448, characters 37-39:
Warning: Unused variable m' catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
File "./BigN/NMake_gen.v", line 448, characters 37-39:
Warning: Unused variable m' catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
File "./BigN/NMake_gen.v", line 448, characters 37-39:
Warning: Unused variable m' catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
File "./BigN/NMake_gen.v", line 448, characters 37-39:
Warning: Unused variable m' catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
File "./BigN/NMake_gen.v", line 448, characters 37-39:
Warning: Unused variable m' catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
File "./BigN/NMake_gen.v", line 445, characters 19-21:
Warning: Unused variable n' catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
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]
File "./BigN/NMake_gen.v", line 761, characters 1-104:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
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]
File "./BigN/NMake.v", line 1359, characters 1-47:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
File "./BigN/NMake.v", line 1695, characters 4-22:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
COQC BigN/BigN.v
File "./BigN/BigN.v", line 197, characters 30-36:
Warning: omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
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.13.0.drv-0/source'
phase `build' succeeded after 88.9 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.13.0.drv-0/source'
make[1]: Nothing to be done for 'Makefile'.
make[1]: Leaving directory '/tmp/guix-build-coq-bignums-8.13.0.drv-0/source'
make -f Makefile.coq install
make[1]: Entering directory '/tmp/guix-build-coq-bignums-8.13.0.drv-0/source'
INSTALL BigN/Nbasic.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake_gen.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/BigN.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL SpecViaZ/NSig.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSig.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/NSigNAxioms.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSigZAxioms.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaQ/QSig.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaQ
INSTALL BigQ/QMake.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL BigQ/BigQ.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL CyclicDouble/DoubleBase.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleAdd.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDiv.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleMul.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSub.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDivn1.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSqrt.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleCyclic.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleLift.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL BigNumPrelude.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums/
INSTALL BigZ/ZMake.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL BigZ/BigZ.vo /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL BigN/Nbasic.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake_gen.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/BigN.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL SpecViaZ/NSig.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSig.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/NSigNAxioms.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSigZAxioms.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaQ/QSig.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaQ
INSTALL BigQ/QMake.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL BigQ/BigQ.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL CyclicDouble/DoubleBase.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleAdd.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDiv.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleMul.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSub.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDivn1.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSqrt.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleCyclic.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleLift.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL BigNumPrelude.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums/
INSTALL BigZ/ZMake.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL BigZ/BigZ.v /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL BigN/Nbasic.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/NMake_gen.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL BigN/BigN.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigN
INSTALL SpecViaZ/NSig.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSig.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/NSigNAxioms.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSigZAxioms.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaZ
INSTALL SpecViaQ/QSig.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//SpecViaQ
INSTALL BigQ/QMake.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL BigQ/BigQ.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigQ
INSTALL CyclicDouble/DoubleBase.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleAdd.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDiv.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleMul.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSub.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDivn1.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSqrt.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleCyclic.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleLift.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//CyclicDouble
INSTALL BigNumPrelude.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums/
INSTALL BigZ/ZMake.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL BigZ/BigZ.glob /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//BigZ
INSTALL plugin/bignums_syntax_plugin.cmi /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmxs /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmxs /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmxa /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmx /gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.0/lib/coq/user-contrib/Bignums//plugin
make[2]: Entering directory '/tmp/guix-build-coq-bignums-8.13.0.drv-0/source'
make[2]: Leaving directory '/tmp/guix-build-coq-bignums-8.13.0.drv-0/source'
make[1]: Leaving directory '/tmp/guix-build-coq-bignums-8.13.0.drv-0/source'
phase `install' succeeded after 1.6 seconds
starting phase `patch-shebangs'
phase `patch-shebangs' succeeded after 0.0 seconds
starting phase `strip'
stripping binaries in "/gnu/store/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.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/h65z5g1adcgglwckg7njvwgmbmlsw5ms-coq-bignums-8.13.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