mathlib test executable failure

Stream: nightly-testing

[Kim Morrison]

github mathlib4 bot said:

:cross_mark: mathlib_test_executable failed on 73094ff2aa9a2188dd00a9847afc362f6d66b560 (branch: nightly-testing-2025-03-17)

Oh dear! This is a test that runs each day to check that an executable with import Mathlib can actually run.

Today it failed with a bunch of errors like:

././.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2121:26: error: redefinition of 'l_Turing_PartrecToTM2_Cont_x27___sizeOf__1'
LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_Cont_x27___sizeOf__1(lean_object* x_1) {

Any ideas?

[Kim Morrison]

I am guessing that asynchronous elaboration is the cause... Sorry @Sebastian Ullrich!

[Sebastian Ullrich]

@Kim Morrison Thanks, this turned out to be a regression in compile_inductive%. Which wasn't even needed in the breaking file but I nevertheless pushed a fix to nightly-testing... hopefully this will all become obsolete with the new codegen