Mock Version: 6.1 Mock Version: 6.1 Mock Version: 6.1 ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --noclean --target aarch64 --nodeps /builddir/build/SPECS/flocq.spec'], chrootPath='/var/lib/mock/f43-build-59133858-6571275/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=timeout=201600uid=1000gid=425user='mockbuild'unshare_net=TrueprintOutput=Falsenspawn_args=['--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.bsidkt7u:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']) Using nspawn with args ['--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.bsidkt7u:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11'] Executing command: ['/usr/bin/systemd-nspawn', '-q', '-M', 'b15b29137f3845d098edce0c50dbbf97', '-D', '/var/lib/mock/f43-build-59133858-6571275/root', '-a', '-u', 'mockbuild', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.bsidkt7u:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11', '--console=pipe', '--setenv=TERM=vt100', '--setenv=SHELL=/bin/bash', '--setenv=HOME=/builddir', '--setenv=HOSTNAME=mock', '--setenv=PATH=/usr/bin:/bin:/usr/sbin:/sbin', '--setenv=PROMPT_COMMAND=printf "\\033]0;\\007"', '--setenv=PS1= \\s-\\v\\$ ', '--setenv=LANG=C.UTF-8', '--resolv-conf=off', 'bash', '--login', '-c', '/usr/bin/rpmbuild -bs --noclean --target aarch64 --nodeps /builddir/build/SPECS/flocq.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8', 'SYSTEMD_NSPAWN_TMPFS_TMP': '0', 'SYSTEMD_SECCOMP': '0'} and shell False Building target platforms: aarch64 Building for target aarch64 setting SOURCE_DATE_EPOCH=1739404800 Wrote: /builddir/build/SRPMS/flocq-4.2.1-1.fc43.src.rpm Child return code was: 0 ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --noclean --target aarch64 --nodeps /builddir/build/SPECS/flocq.spec'], chrootPath='/var/lib/mock/f43-build-59133858-6571275/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=timeout=201600uid=1000gid=425user='mockbuild'unshare_net=TrueprintOutput=Falsenspawn_args=['--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.bsidkt7u:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']) Using nspawn with args ['--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.bsidkt7u:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11'] Executing command: ['/usr/bin/systemd-nspawn', '-q', '-M', '0e03147c6e564760bb936a333a9353f4', '-D', '/var/lib/mock/f43-build-59133858-6571275/root', '-a', '-u', 'mockbuild', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.bsidkt7u:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/fuse', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11', '--console=pipe', '--setenv=TERM=vt100', '--setenv=SHELL=/bin/bash', '--setenv=HOME=/builddir', '--setenv=HOSTNAME=mock', '--setenv=PATH=/usr/bin:/bin:/usr/sbin:/sbin', '--setenv=PROMPT_COMMAND=printf "\\033]0;\\007"', '--setenv=PS1= \\s-\\v\\$ ', '--setenv=LANG=C.UTF-8', '--resolv-conf=off', 'bash', '--login', '-c', '/usr/bin/rpmbuild -bb --noclean --target aarch64 --nodeps /builddir/build/SPECS/flocq.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8', 'SYSTEMD_NSPAWN_TMPFS_TMP': '0', 'SYSTEMD_SECCOMP': '0'} and shell False Building target platforms: aarch64 Building for target aarch64 setting SOURCE_DATE_EPOCH=1739404800 Executing(%mkbuilddir): /bin/sh -e /var/tmp/rpm-tmp.YLVQJS Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.YTQV4M + umask 022 + cd /builddir/build/BUILD/flocq-4.2.1-build + cd /builddir/build/BUILD/flocq-4.2.1-build + rm -rf flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d + /usr/lib/rpm/rpmuncompress -x /builddir/build/SOURCES/flocq-4.2.1.tar.gz + STATUS=0 + '[' 0 -ne 0 ']' + cd flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d + /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w . + RPM_EC=0 ++ jobs -p + exit 0 Executing(%conf): /bin/sh -e /var/tmp/rpm-tmp.PSTVsA + umask 022 + cd /builddir/build/BUILD/flocq-4.2.1-build + CFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer ' + export CFLAGS + CXXFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer ' + export CXXFLAGS + FFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer -I/usr/lib64/gfortran/modules ' + export FFLAGS + FCFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer -I/usr/lib64/gfortran/modules ' + export FCFLAGS + VALAFLAGS=-g + export VALAFLAGS + RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none -Cforce-frame-pointers=yes -Clink-arg=-specs=/usr/lib/rpm/redhat/redhat-package-notes --cap-lints=warn' + export RUSTFLAGS + LDFLAGS='-Wl,-z,relro -Wl,--as-needed -Wl,-z,pack-relative-relocs -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-hardened-ld-errors -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes ' + export LDFLAGS + LT_SYS_LIBRARY_PATH=/usr/lib64: + export LT_SYS_LIBRARY_PATH + CC=gcc + export CC + CXX=g++ + export CXX + cd flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d + sed -i 's,\(--coqlib \)[^[:blank:]]*,\1/usr/lib64/ocaml/coq,' Remakefile.in + autoconf -f configure.in:5: warning: prefer named diversions + RPM_EC=0 ++ jobs -p + exit 0 Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.25vek8 + umask 022 + cd /builddir/build/BUILD/flocq-4.2.1-build + CFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer ' + export CFLAGS + CXXFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer ' + export CXXFLAGS + FFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer -I/usr/lib64/gfortran/modules ' + export FFLAGS + FCFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer -I/usr/lib64/gfortran/modules ' + export FCFLAGS + VALAFLAGS=-g + export VALAFLAGS + RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none -Cforce-frame-pointers=yes -Clink-arg=-specs=/usr/lib/rpm/redhat/redhat-package-notes --cap-lints=warn' + export RUSTFLAGS + LDFLAGS='-Wl,-z,relro -Wl,--as-needed -Wl,-z,pack-relative-relocs -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-hardened-ld-errors -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes ' + export LDFLAGS + LT_SYS_LIBRARY_PATH=/usr/lib64: + export LT_SYS_LIBRARY_PATH + CC=gcc + export CC + CXX=g++ + export CXX + cd flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d + ./configure checking for coqc... /usr/bin/coqc checking Coq version... 8.20.1 checking for coqdep... /usr/bin/coqdep checking for coqdoc... /usr/bin/coqdoc checking whether the C++ compiler works... yes checking for C++ compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether the compiler supports GNU C++... yes checking whether g++ accepts -g... yes checking for g++ option to enable C++11 features... none needed configure: building remake... /usr/bin/ld: /tmp/ccQa1W7N.o: in function `main': remake.cpp:(.text.startup+0xaa4): warning: the use of `tempnam' is dangerous, better use `mkstemp' configure: creating ./config.status config.status: creating Remakefile config.status: creating src/Version.v + rm -f remake + ln -s /usr/bin/remake remake + remake -d -j12 all doc Building src/Version.vo Building src/Core/Raux.vo Building src/Core/Zaux.vo Building src/Core/Defs.vo Building src/Core/Digits.vo Building src/Core/Float_prop.vo Building src/Core/FIX.vo Building src/Core/FLT.vo /usr/bin/coqdep -R src Flocq src/Version.v | ./remake -r src/Version.vo Building src/Core/FLX.vo /usr/bin/coqdep -R src Flocq src/Core/Raux.v | ./remake -r src/Core/Raux.vo /usr/bin/coqdep -R src Flocq src/Core/Zaux.v | ./remake -r src/Core/Zaux.vo /usr/bin/coqdep -R src Flocq src/Core/Defs.v | ./remake -r src/Core/Defs.vo /usr/bin/coqdep -R src Flocq src/Core/Digits.v | ./remake -r src/Core/Digits.vo /usr/bin/coqdep -R src Flocq src/Core/Float_prop.v | ./remake -r src/Core/Float_prop.vo /usr/bin/coqdep -R src Flocq src/Core/FIX.v | ./remake -r src/Core/FIX.vo /usr/bin/coqdep -R src Flocq src/Core/FLT.v | ./remake -r src/Core/FLT.vo Building src/Core/FTZ.vo Building src/Core/Generic_fmt.vo Building src/Core/Round_pred.vo /usr/bin/coqdep -R src Flocq src/Core/FTZ.v | ./remake -r src/Core/FTZ.vo /usr/bin/coqdep -R src Flocq src/Core/FLX.v | ./remake -r src/Core/FLX.vo /usr/bin/coqdep -R src Flocq src/Core/Generic_fmt.v | ./remake -r src/Core/Generic_fmt.vo /usr/bin/coqdep -R src Flocq src/Core/Round_pred.v | ./remake -r src/Core/Round_pred.vo Building src/Core/Round_NE.vo Building src/Core/Ulp.vo Building src/Core/Core.vo /usr/bin/coqdep -R src Flocq src/Core/Round_NE.v | ./remake -r src/Core/Round_NE.vo /usr/bin/coqdep -R src Flocq src/Core/Ulp.v | ./remake -r src/Core/Ulp.vo /usr/bin/coqdep -R src Flocq src/Core/Core.v | ./remake -r src/Core/Core.vo Building src/Calc/Bracket.vo Building src/Calc/Div.vo /usr/bin/coqc -q -R src Flocq src/Version.v Building src/Calc/Operations.vo /usr/bin/coqdep -R src Flocq src/Calc/Bracket.v | ./remake -r src/Calc/Bracket.vo /usr/bin/coqdep -R src Flocq src/Calc/Div.v | ./remake -r src/Calc/Div.vo /usr/bin/coqdep -R src Flocq src/Calc/Operations.v | ./remake -r src/Calc/Operations.vo Building src/Calc/Plus.vo /usr/bin/coqc -q -R src Flocq src/Core/Zaux.v /usr/bin/coqdep -R src Flocq src/Calc/Plus.v | ./remake -r src/Calc/Plus.vo Building src/Calc/Round.vo /usr/bin/coqdep -R src Flocq src/Calc/Round.v | ./remake -r src/Calc/Round.vo Building src/Calc/Sqrt.vo /usr/bin/coqdep -R src Flocq src/Calc/Sqrt.v | ./remake -r src/Calc/Sqrt.vo Building src/Prop/Div_sqrt_error.vo /usr/bin/coqdep -R src Flocq src/Prop/Div_sqrt_error.v | ./remake -r src/Prop/Div_sqrt_error.vo Building src/Prop/Mult_error.vo Building src/Prop/Plus_error.vo Building src/Prop/Relative.vo /usr/bin/coqdep -R src Flocq src/Prop/Mult_error.v | ./remake -r src/Prop/Mult_error.vo Building src/Prop/Sterbenz.vo /usr/bin/coqdep -R src Flocq src/Prop/Plus_error.v | ./remake -r src/Prop/Plus_error.vo /usr/bin/coqdep -R src Flocq src/Prop/Relative.v | ./remake -r src/Prop/Relative.vo /usr/bin/coqdep -R src Flocq src/Prop/Sterbenz.v | ./remake -r src/Prop/Sterbenz.vo Building src/Prop/Round_odd.vo Building src/Prop/Double_rounding.vo /usr/bin/coqdep -R src Flocq src/Prop/Round_odd.v | ./remake -r src/Prop/Round_odd.vo /usr/bin/coqdep -R src Flocq src/Prop/Double_rounding.v | ./remake -r src/Prop/Double_rounding.vo Building src/IEEE754/BinarySingleNaN.vo /usr/bin/coqdep -R src Flocq src/IEEE754/BinarySingleNaN.v | ./remake -r src/IEEE754/BinarySingleNaN.vo Building src/IEEE754/Binary.vo Building src/IEEE754/Bits.vo /usr/bin/coqdep -R src Flocq src/IEEE754/Binary.v | ./remake -r src/IEEE754/Binary.vo /usr/bin/coqdep -R src Flocq src/IEEE754/Bits.v | ./remake -r src/IEEE754/Bits.vo Building src/IEEE754/PrimFloat.vo /usr/bin/coqdep -R src Flocq src/IEEE754/PrimFloat.v | ./remake -r src/IEEE754/PrimFloat.vo Building src/Pff/Pff.vo /usr/bin/coqdep -R src Flocq src/Pff/Pff.v | ./remake -r src/Pff/Pff.vo Building src/Pff/Pff2FlocqAux.vo /usr/bin/coqdep -R src Flocq src/Pff/Pff2FlocqAux.v | ./remake -r src/Pff/Pff2FlocqAux.vo Building src/Pff/Pff2Flocq.vo /usr/bin/coqdep -R src Flocq src/Pff/Pff2Flocq.v | ./remake -r src/Pff/Pff2Flocq.vo /usr/bin/coqc -q -R src Flocq src/Pff/Pff.v Finished src/Version.vo File "./src/Core/Zaux.v", line 327, characters 2-6: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Zaux.v", line 327, characters 8-12: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Zaux.v", line 327, characters 28-32: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Zaux.v", line 361, characters 10-14: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Zaux.v", line 361, characters 31-35: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Zaux.v", line 367, characters 25-29: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Zaux.v", line 367, characters 25-29: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Zaux.v", line 367, characters 25-29: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Zaux.v", line 367, characters 25-29: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Pff/Pff.v", line 68, characters 30-45: Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Pff/Pff.v", line 69, characters 24-33: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Pff/Pff.v", line 70, characters 23-31: Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Pff/Pff.v", line 71, characters 30-45: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Pff/Pff.v", line 72, characters 25-35: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Pff/Pff.v", line 73, characters 26-37: Warning: Notation powerRZ_inv is deprecated since 8.16. Use powerRZ_inv'. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Pff/Pff.v", line 74, characters 26-37: Warning: Notation powerRZ_neg is deprecated since 8.16. Use powerRZ_neg' and powerRZ_inv'. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Pff/Pff.v", line 80, characters 22-29: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Zaux.v", line 855, characters 31-35: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Zaux.v", line 858, characters 14-18: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] Finished src/Core/Zaux.vo /usr/bin/coqc -q -R src Flocq src/Core/Raux.v /usr/bin/coqc -q -R src Flocq src/Core/Digits.v File "./src/Core/Raux.v", line 189, characters 6-14: Warning: Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 189, characters 6-14: Warning: Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 571, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 571, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 583, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 583, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1284, characters 8-24: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1284, characters 8-24: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1284, characters 8-24: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1312, characters 35-43: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1312, characters 35-43: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1312, characters 35-43: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1319, characters 35-47: Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1319, characters 35-47: Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1319, characters 35-47: Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1319, characters 35-47: Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1325, characters 36-44: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1325, characters 36-44: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1325, characters 36-44: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1325, characters 54-66: Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1325, characters 54-66: Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1325, characters 54-66: Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1325, characters 54-66: Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1429, characters 15-30: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1429, characters 15-30: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1429, characters 15-30: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1429, characters 15-30: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1884, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1884, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1994, characters 12-22: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 1994, characters 12-22: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 2078, characters 10-19: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 2078, characters 10-19: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 2078, characters 10-19: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] Finished src/Core/Digits.vo File "./src/Core/Raux.v", line 2343, characters 14-29: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 2343, characters 14-29: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 2343, characters 14-29: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 2375, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 2375, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Raux.v", line 2375, characters 12-27: Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] Finished src/Core/Raux.vo /usr/bin/coqc -q -R src Flocq src/Core/Defs.v Finished src/Core/Defs.vo /usr/bin/coqc -q -R src Flocq src/Core/Round_pred.v /usr/bin/coqc -q -R src Flocq src/Core/Float_prop.v File "./src/Core/Float_prop.v", line 461, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Float_prop.v", line 461, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Float_prop.v", line 471, characters 16-23: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Float_prop.v", line 471, characters 16-23: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] Finished src/Core/Float_prop.vo /usr/bin/coqc -q -R src Flocq src/Calc/Operations.v /usr/bin/coqc -q -R src Flocq src/Calc/Bracket.v Finished src/Core/Round_pred.vo /usr/bin/coqc -q -R src Flocq src/Core/Generic_fmt.v Finished src/Calc/Operations.vo File "./src/Calc/Bracket.v", line 183, characters 13-23: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Calc/Bracket.v", line 183, characters 13-23: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Calc/Bracket.v", line 629, characters 85-89: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Calc/Bracket.v", line 660, characters 63-67: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] Finished src/Calc/Bracket.vo Finished src/Core/Generic_fmt.vo /usr/bin/coqc -q -R src Flocq src/Calc/Div.v /usr/bin/coqc -q -R src Flocq src/Prop/Sterbenz.v /usr/bin/coqc -q -R src Flocq src/Calc/Sqrt.v /usr/bin/coqc -q -R src Flocq src/Core/Ulp.v File "./src/Calc/Div.v", line 89, characters 14-21: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Calc/Div.v", line 89, characters 14-21: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Calc/Div.v", line 98, characters 14-21: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Calc/Div.v", line 98, characters 14-21: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Calc/Div.v", line 115, characters 12-19: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Calc/Div.v", line 115, characters 12-19: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] Finished src/Prop/Sterbenz.vo File "./src/Calc/Div.v", line 117, characters 12-19: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Calc/Div.v", line 117, characters 12-19: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] Finished src/Calc/Sqrt.vo Finished src/Calc/Div.vo File "./src/Core/Ulp.v", line 1424, characters 10-20: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Ulp.v", line 1424, characters 10-20: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Ulp.v", line 1451, characters 24-34: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Core/Ulp.v", line 1451, characters 24-34: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] Finished src/Core/Ulp.vo /usr/bin/coqc -q -R src Flocq src/Core/Round_NE.v Finished src/Core/Round_NE.vo /usr/bin/coqc -q -R src Flocq src/Core/FIX.v Finished src/Core/FIX.vo /usr/bin/coqc -q -R src Flocq src/Core/FLX.v Finished src/Core/FLX.vo /usr/bin/coqc -q -R src Flocq src/Core/FLT.v /usr/bin/coqc -q -R src Flocq src/Core/FTZ.v Finished src/Core/FTZ.vo Finished src/Core/FLT.vo /usr/bin/coqc -q -R src Flocq src/Core/Core.v Finished src/Core/Core.vo /usr/bin/coqc -q -R src Flocq src/Prop/Round_odd.v /usr/bin/coqc -q -R src Flocq src/Prop/Double_rounding.v /usr/bin/coqc -q -R src Flocq src/Prop/Relative.v /usr/bin/coqc -q -R src Flocq src/Calc/Round.v File "./src/Prop/Relative.v", line 568, characters 17-26: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Relative.v", line 568, characters 17-26: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Relative.v", line 568, characters 17-26: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Calc/Round.v", line 612, characters 41-45: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Relative.v", line 572, characters 43-52: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Relative.v", line 572, characters 43-52: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Relative.v", line 572, characters 43-52: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Calc/Round.v", line 1146, characters 43-47: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] Finished src/Calc/Round.vo /usr/bin/coqc -q -R src Flocq src/Calc/Plus.v Finished src/Prop/Relative.vo /usr/bin/coqc -q -R src Flocq src/IEEE754/BinarySingleNaN.v /usr/bin/coqc -q -R src Flocq src/Prop/Plus_error.v Finished src/Prop/Round_odd.vo Finished src/Calc/Plus.vo Finished src/Prop/Plus_error.vo /usr/bin/coqc -q -R src Flocq src/Prop/Mult_error.v File "./src/Prop/Double_rounding.v", line 1456, characters 14-20: Warning: Notation double is deprecated since 8.19. Use Rplus_diag. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 1456, characters 14-20: Warning: Notation double is deprecated since 8.19. Use Rplus_diag. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 1456, characters 14-20: Warning: Notation double is deprecated since 8.19. Use Rplus_diag. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 2637, characters 8-18: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 2637, characters 8-18: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] Finished src/Prop/Mult_error.vo /usr/bin/coqc -q -R src Flocq src/Prop/Div_sqrt_error.v File "./src/Prop/Double_rounding.v", line 3057, characters 8-18: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 3057, characters 8-18: Warning: Notation Rlt_Rminus is deprecated since 8.19. Use the bidirectional version Rlt_0_minus instead. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2246, characters 11-27: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2246, characters 11-27: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2246, characters 11-27: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2246, characters 11-27: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2288, characters 21-30: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2288, characters 21-30: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2288, characters 21-30: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2288, characters 21-30: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2297, characters 34-43: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2297, characters 34-43: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2297, characters 34-43: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2297, characters 34-43: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2298, characters 47-56: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2298, characters 47-56: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2298, characters 47-56: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2298, characters 47-56: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19: Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19: Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19: Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19: Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 204, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 204, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 211, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 211, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 218, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 218, characters 10-17: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2473, characters 16-18: Warning: Unused variable sx might be a misspelled constructor. Use _ or _sx to silence this warning. [unused-pattern-matching-variable,default] File "./src/Prop/Double_rounding.v", line 3492, characters 10-25: Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 3493, characters 25-32: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 3492, characters 10-25: Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 3492, characters 10-25: Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 3492, characters 10-25: Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 3492, characters 10-25: Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 3493, characters 25-32: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 3497, characters 31-38: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 3497, characters 31-38: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2987, characters 29-36: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 2987, characters 29-36: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 3026, characters 29-36: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/BinarySingleNaN.v", line 3026, characters 29-36: Warning: Notation IZR_neq is deprecated since 8.19. Use eq_IZR_contrapositive. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20: Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] Finished src/Prop/Div_sqrt_error.vo Finished src/IEEE754/BinarySingleNaN.vo /usr/bin/coqc -q -R src Flocq src/IEEE754/Binary.v /usr/bin/coqc -q -R src Flocq src/IEEE754/PrimFloat.v File "./src/Prop/Double_rounding.v", line 4322, characters 12-20: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4322, characters 12-20: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4322, characters 12-20: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4323, characters 28-44: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4323, characters 28-44: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4323, characters 28-44: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4323, characters 28-44: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4337, characters 12-20: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4337, characters 12-20: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4337, characters 12-20: Warning: Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l. [deprecated-syntactic-definition-since-8.19,deprecated-since-8.19,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4352, characters 28-44: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4352, characters 28-44: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4352, characters 28-44: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./src/Prop/Double_rounding.v", line 4352, characters 28-44: Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] Finished src/Prop/Double_rounding.vo Finished src/IEEE754/PrimFloat.vo Finished src/IEEE754/Binary.vo /usr/bin/coqc -q -R src Flocq src/IEEE754/Bits.v File "./src/IEEE754/Bits.v", line 80, characters 25-29: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] File "./src/IEEE754/Bits.v", line 80, characters 36-40: Warning: Notation Zmod is deprecated since 8.17. Use Coq.ZArith.BinIntDef.Z.modulo instead [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] Finished src/IEEE754/Bits.vo Finished src/Pff/Pff.vo /usr/bin/coqc -q -R src Flocq src/Pff/Pff2FlocqAux.v Finished src/Pff/Pff2FlocqAux.vo /usr/bin/coqc -q -R src Flocq src/Pff/Pff2Flocq.v Finished src/Pff/Pff2Flocq.vo Building all Finished all Building html/index.html rm -rf html mkdir -p html /usr/bin/coqdoc -toc -interpolate -utf8 -html -g -R src Flocq -d html \ --coqlib_url http://coq.inria.fr/distrib/current/stdlib \ src/Version.v src/Core/Raux.v src/Core/Zaux.v src/Core/Defs.v src/Core/Digits.v src/Core/Float_prop.v src/Core/FIX.v src/Core/FLT.v src/Core/FLX.v src/Core/FTZ.v src/Core/Generic_fmt.v src/Core/Round_pred.v src/Core/Round_NE.v src/Core/Ulp.v src/Core/Core.v src/Calc/Bracket.v src/Calc/Div.v src/Calc/Operations.v src/Calc/Plus.v src/Calc/Round.v src/Calc/Sqrt.v src/Prop/Div_sqrt_error.v src/Prop/Mult_error.v src/Prop/Plus_error.v src/Prop/Relative.v src/Prop/Sterbenz.v src/Prop/Round_odd.v src/Prop/Double_rounding.v src/IEEE754/BinarySingleNaN.v src/IEEE754/Binary.v src/IEEE754/Bits.v src/IEEE754/PrimFloat.v src/Pff/Pff.v src/Pff/Pff2FlocqAux.v src/Pff/Pff2Flocq.v for f in html/*.html; do sed -e 's;Index;Go back to the Main page or Index.;' -i $f done Finished html/index.html Building doc Finished doc + RPM_EC=0 ++ jobs -p + exit 0 Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.4wY7CL + umask 022 + cd /builddir/build/BUILD/flocq-4.2.1-build + '[' /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT '!=' / ']' + rm -rf /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT ++ dirname /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT + mkdir -p /builddir/build/BUILD/flocq-4.2.1-build + mkdir /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT + CFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer ' + export CFLAGS + CXXFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer ' + export CXXFLAGS + FFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer -I/usr/lib64/gfortran/modules ' + export FFLAGS + FCFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -mbranch-protection=standard -fasynchronous-unwind-tables -fstack-clash-protection -fno-omit-frame-pointer -mno-omit-leaf-frame-pointer -I/usr/lib64/gfortran/modules ' + export FCFLAGS + VALAFLAGS=-g + export VALAFLAGS + RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none -Cforce-frame-pointers=yes -Clink-arg=-specs=/usr/lib/rpm/redhat/redhat-package-notes --cap-lints=warn' + export RUSTFLAGS + LDFLAGS='-Wl,-z,relro -Wl,--as-needed -Wl,-z,pack-relative-relocs -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-hardened-ld-errors -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes ' + export LDFLAGS + LT_SYS_LIBRARY_PATH=/usr/lib64: + export LT_SYS_LIBRARY_PATH + CC=gcc + export CC + CXX=g++ + export CXX + cd flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d + sed -i s,/usr/lib64,/builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/lib64, Remakefile + remake install Building install Finished install + cp -p src/Version.v /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/lib64/ocaml/coq/user-contrib/Flocq + cp -p src/Calc/Bracket.v src/Calc/Div.v src/Calc/Operations.v src/Calc/Plus.v src/Calc/Round.v src/Calc/Sqrt.v /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/lib64/ocaml/coq/user-contrib/Flocq/Calc + cp -p src/Core/Core.v src/Core/Defs.v src/Core/Digits.v src/Core/FIX.v src/Core/FLT.v src/Core/FLX.v src/Core/FTZ.v src/Core/Float_prop.v src/Core/Generic_fmt.v src/Core/Raux.v src/Core/Round_NE.v src/Core/Round_pred.v src/Core/Ulp.v src/Core/Zaux.v /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/lib64/ocaml/coq/user-contrib/Flocq/Core + cp -p src/IEEE754/Binary.v src/IEEE754/BinarySingleNaN.v src/IEEE754/Bits.v src/IEEE754/PrimFloat.v /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/lib64/ocaml/coq/user-contrib/Flocq/IEEE754 + cp -p src/Pff/Nat2Z_8_12.v src/Pff/Pff.v src/Pff/Pff2Flocq.v src/Pff/Pff2FlocqAux.v /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/lib64/ocaml/coq/user-contrib/Flocq/Pff + cp -p src/Prop/Div_sqrt_error.v src/Prop/Double_rounding.v src/Prop/Mult_error.v src/Prop/Plus_error.v src/Prop/Relative.v src/Prop/Round_odd.v src/Prop/Sterbenz.v /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/lib64/ocaml/coq/user-contrib/Flocq/Prop + /usr/lib/rpm/check-buildroot + /usr/lib/rpm/redhat/brp-ldconfig + /usr/lib/rpm/brp-compress + /usr/lib/rpm/brp-strip /usr/bin/strip + /usr/lib/rpm/brp-strip-comment-note /usr/bin/strip /usr/bin/objdump + /usr/lib/rpm/redhat/brp-strip-lto /usr/bin/strip + /usr/lib/rpm/brp-strip-static-archive /usr/bin/strip + /usr/lib/rpm/check-rpaths + /usr/lib/rpm/redhat/brp-mangle-shebangs + /usr/lib/rpm/brp-remove-la-files + /usr/lib/rpm/redhat/brp-python-rpm-in-distinfo + env /usr/lib/rpm/redhat/brp-python-bytecompile '' 1 0 -j12 + /usr/lib/rpm/redhat/brp-python-hardlink + /usr/bin/add-determinism --brp -j12 /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT Scanned 12 directories and 71 files, processed 0 inodes, 0 modified (0 replaced + 0 rewritten), 0 unsupported format, 0 errors Reading /builddir/build/BUILD/flocq-4.2.1-build/SPECPARTS/rpm-debuginfo.specpart Processing files: flocq-4.2.1-1.fc43.aarch64 Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.FlBn6V + umask 022 + cd /builddir/build/BUILD/flocq-4.2.1-build + cd flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d + DOCDIR=/builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/share/doc/flocq + export LC_ALL=C.UTF-8 + LC_ALL=C.UTF-8 + export DOCDIR + /usr/bin/mkdir -p /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/share/doc/flocq + cp -pr /builddir/build/BUILD/flocq-4.2.1-build/flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d/AUTHORS /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/share/doc/flocq + cp -pr /builddir/build/BUILD/flocq-4.2.1-build/flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d/NEWS.md /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/share/doc/flocq + cp -pr /builddir/build/BUILD/flocq-4.2.1-build/flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d/README.md /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/share/doc/flocq + cp -pr /builddir/build/BUILD/flocq-4.2.1-build/flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d/html /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/share/doc/flocq + RPM_EC=0 ++ jobs -p + exit 0 Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.cxuvIj + umask 022 + cd /builddir/build/BUILD/flocq-4.2.1-build + cd flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d + LICENSEDIR=/builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/share/licenses/flocq + export LC_ALL=C.UTF-8 + LC_ALL=C.UTF-8 + export LICENSEDIR + /usr/bin/mkdir -p /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/share/licenses/flocq + cp -pr /builddir/build/BUILD/flocq-4.2.1-build/flocq-flocq-4.2.1-e1443068c65f644989e1f4eefecd72084de4e13d/COPYING /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT/usr/share/licenses/flocq + RPM_EC=0 ++ jobs -p + exit 0 Provides: flocq = 4.2.1-1.fc43 flocq(aarch-64) = 4.2.1-1.fc43 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Processing files: flocq-source-4.2.1-1.fc43.aarch64 Provides: flocq-source = 4.2.1-1.fc43 flocq-source(aarch-64) = 4.2.1-1.fc43 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILD/flocq-4.2.1-build/BUILDROOT Wrote: /builddir/build/RPMS/flocq-source-4.2.1-1.fc43.aarch64.rpm Wrote: /builddir/build/RPMS/flocq-4.2.1-1.fc43.aarch64.rpm Child return code was: 0