Building Lean 4.15-rc1 with default build settings runs into a Stack Overflow in Data/UInt/Lemmas.lean

[soulsource]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• [not applicable] Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• [not applicable] Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Building Lean 4.15-rc1 from source with the default build settings fails with a stack overflow when compiling Data/UInt/Lemmas.lean for stage1.

Context

I am not sure if this is specific to my system, or if others might be running into the same issue. Also, not sure why it doesn't happen in CI. Compiling Lean 4.14 with identical settings was working fine on the same machine.

Looking at the call-stack in the crashdump, there are over 3000 recursions of l_Lean_IR_NormalizeIds_normFnBody. However, it is not an infinite recursion, as increasing the thread stack size via LEAN_EXTRA_MAKE_OPTS allows to work around this build issue.
I haven't tested what stack size exactly is needed, but passing -DLEAN_EXTRA_MAKE_OPTS="-s 262144" to cmake allowed the build to finish.

Depending on the question if anyone else sees this, it might be a good idea to set a higher default stack size while building Lean.

Steps to Reproduce

1. Compile Lean 4.15-rc1 from source with default settings on AMD64 Linux

Expected behavior: The build succeeds

Actual behavior: The build fails with a stack overflow when compiling Data/UInt/Lemmas.lean

Versions

Gentoo Linux, kernel 6.6.62, gcc (Gentoo 14.2.1_p20241116 p3) 14.2.1 20241116

Additional Information

I've used an ebuild to build lean4. Not sure if this is relevant, but for the sake of completeness:
Edit: This is the ebuild that already passes -DLEAN_EXTRA_MAKE_OPTS="-s 262144". To repro the issue with it, please remove the respective line.

MAJOR="$(ver_cut 1)"

CMAKE_MAKEFILE_GENERATOR="emake"
PYTHON_COMPAT=( python3_{10..12} )

inherit cmake flag-o-matic python-any-r1

DESCRIPTION="The Lean Theorem Prover"
HOMEPAGE="https://leanprover-community.github.io/"

if [[ "${PV}" == *9999* ]] ; then
	inherit git-r3

	EGIT_REPO_URI="https://github.com/leanprover/${PN}${MAJOR}.git"
else
	SRC_URI="https://github.com/leanprover/${PN}${MAJOR}/archive/refs/tags/v${PV/_/-}.tar.gz
		-> ${P}.tar.gz"
	S="${WORKDIR}/${PN}${MAJOR}-${PV/_/-}"

	KEYWORDS="~amd64 ~x86"
fi

LICENSE="Apache-2.0"
SLOT="0/${MAJOR}"
IUSE="debug source"

RDEPEND="
	dev-libs/gmp:=
	sci-mathematics/cadical
"
DEPEND="
	${RDEPEND}
"
BDEPEND="
	${PYTHON_DEPS}
"

pkg_setup() {
	python-any-r1_pkg_setup
}

src_prepare() {
	filter-lto

	sed -e "s|-O[23]|${CFLAGS}|g" -i src/CMakeLists.txt || die

	cmake_src_prepare
}

src_configure() {
	local CMAKE_BUILD_TYPE

	if use debug ; then
		CMAKE_BUILD_TYPE="Debug"
	else
		CMAKE_BUILD_TYPE="Release"
	fi

	local -a mycmakeargs=(
		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
		-DLEAN_EXTRA_LINKER_FLAGS="${LDFLAGS}"
		-DLEAN_EXTRA_MAKE_OPTS="-s 262144"
		-DINSTALL_CADICAL=OFF
	)
	cmake_src_configure
}

src_install() {
	cmake_src_install

	rm "${ED}/usr/LICENSE"* || die

	if ! use source ; then
		rm -r "${ED}/usr/src" || die
	fi
}

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.