COQC ssreflect/ssrnotations.v COQC ssreflect/ssrfun.v COQC ssreflect/ssrbool.v File "./ssreflect/ssrbool.v", line 42, characters 0-128: Error: Notation "[ rel _ _ : _ | _ ]" is already defined at level 0 with arguments name, name, constr, constr while it is now required to be at level 0 with arguments ident, ident, constr, constr. ------------------------------------------------------------------- This is an unstable amd64 chroot image at a tinderbox (==build bot) name: 17.0_musl_hardened-j4-20220904-151557 ------------------------------------------------------------------- gcc-config -l: [1] x86_64-gentoo-linux-musl-12.2.0 * clang/llvm (if any): clang version 15.0.0 Target: x86_64-gentoo-linux-musl Thread model: posix InstalledDir: /usr/lib/llvm/15/bin /usr/lib/llvm/15 15.0.0 Python 3.10.7 Available Ruby profiles: (none found) php cli (if any): GNU Make 4.3 HEAD of ::gentoo commit e94694ae3bdfb9be82019c95fcb89ade71c56b58 Author: Repository mirror & CI <repomirrorci@gentoo.org> Date: Wed Sep 7 05:12:29 2022 +0000 2022-09-07 05:12:29 UTC emerge -qpvO sci-mathematics/coq-mathcomp [ebuild N ] sci-mathematics/coq-mathcomp-1.14.0
Created attachment 803785 [details] emerge-info.txt
Created attachment 803788 [details] emerge-history.txt
Created attachment 803791 [details] environment
Created attachment 803794 [details] etc.portage.tar.bz2
Created attachment 803797 [details] sci-mathematics:coq-mathcomp-1.14.0:20220907-055856.log
The bug has been closed via the following commit(s): https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=10130c0f4c9b16f6eebcb4d44319e7035937891e commit 10130c0f4c9b16f6eebcb4d44319e7035937891e Author: Maciej Barć <xgqt@gentoo.org> AuthorDate: 2022-09-07 11:56:59 +0000 Commit: Maciej Barć <xgqt@gentoo.org> CommitDate: 2022-09-07 12:17:44 +0000 sci-mathematics/coq-mathcomp: constraint coq version to <8.16.0 Closes: https://bugs.gentoo.org/869053 Signed-off-by: Maciej Barć <xgqt@gentoo.org> .../{coq-mathcomp-1.14.0.ebuild => coq-mathcomp-1.14.0-r1.ebuild} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-)
