828051 – [guru] sci-mathematics/lean-mathlib-0.1_p20211021 fails to compile: tree.lean:42:16: error: unknown identifier rbnode

Bug 828051 - [guru] sci-mathematics/lean-mathlib-0.1_p20211021 fails to compile: tree.lean:42:16: error: unknown identifier rbnode

Summary: [guru] sci-mathematics/lean-mathlib-0.1_p20211021 fails to compile: tree.lean...

Status:	RESOLVED OBSOLETE

Alias:	None

Product:	GURU
Classification:	Unclassified
Component:	Package issues (show other bugs)
Hardware:	All Linux

Importance:	Normal normal
Assignee:	Alessandro Barbieri

URL:
Whiteboard:
Keywords:

Depends on:
Blocks:

Reported:	2021-12-03 06:53 UTC by Agostino Sarubbo
Modified:	2022-03-26 14:52 UTC (History)
CC List:	1 user (show)

See Also:
Package list:
Runtime testing required:	---

Attachments
build.log.xz (build.log.xz,61.88 KB, application/x-xz) 2021-12-03 06:53 UTC, Agostino Sarubbo	Details
View All Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.

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)