Bug 828051

Summary:	[guru] sci-mathematics/lean-mathlib-0.1_p20211021 fails to compile: tree.lean:42:16: error: unknown identifier rbnode
Product:	GURU	Reporter:	Agostino Sarubbo <ago>
Component:	Package issues	Assignee:	Alessandro Barbieri <lssndrbarbieri>
Status:	RESOLVED OBSOLETE
Severity:	normal	CC:	guru-bugs
Priority:	Normal
Version:	unspecified
Hardware:	All
OS:	Linux
Whiteboard:
Package list:		Runtime testing required:	---
Attachments:	build.log.xz

Description Agostino Sarubbo gentoo-dev

2021-12-03 06:53:18 UTC

https://blogs.gentoo.org/ago/2020/07/04/gentoo-tinderbox/

Issue: sci-mathematics/lean-mathlib-0.1_p20211021 fails to compile.
Discovered on: amd64 (internal ref: guru_ci)

Comment 1 Agostino Sarubbo gentoo-dev

2021-12-03 06:53:21 UTC

Created attachment 757241 [details]
build.log.xz

build log and emerge --info (compressed because it exceeds attachment limit, use 'xzless' to read it)