Reverse FFI with Mathlib

Stream: lean4

[Cruise Song]

I'm trying to link newer version of Mathlib (4.22.0-rc2) with the Reverse-FFI, but running into "redefinition" errors when lake build:

✖ [6088/13835] Building Mathlib.Computability.TMToPartrec:c.o
trace: .> /Users/cruis/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/bin/clang -c -o /Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c.o.export /Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c -I /Users/cruis/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/cruis/.elan/toolchains/leanprover--lean4---v4.22.0-rc2 -nostdinc -isystem /Users/cruis/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
/Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2319:26: error: redefinition of 'l_Turing_PartrecToTM2_Cont_x27___sizeOf__1'
 2319 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_Cont_x27___sizeOf__1(lean_object* x_1) {
      |                          ^
/Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:1667:26: note: previous definition is here
 1667 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_Cont_x27___sizeOf__1(lean_object* x_1) {
      |                          ^
/Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2338:21: error: redefinition of '_init_l_Turing_PartrecToTM2_Cont_x27___sizeOf__inst'
 2338 | static lean_object* _init_l_Turing_PartrecToTM2_Cont_x27___sizeOf__inst() {
      |                     ^
/Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:1711:21: note: previous definition is here
 1711 | static lean_object* _init_l_Turing_PartrecToTM2_Cont_x27___sizeOf__inst() {
      |                     ^
/Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2346:26: error: redefinition of 'l_Turing_PartrecToTM2_K_x27___sizeOf__1'
 2346 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_K_x27___sizeOf__1(uint8_t x_1) {
      |                          ^
/Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:1883:26: note: previous definition is here
 1883 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_K_x27___sizeOf__1(uint8_t x_1) {
      |                          ^
/Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2354:26: error: redefinition of 'l_Turing_PartrecToTM2_K_x27___sizeOf__1___boxed'
 2354 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_K_x27___sizeOf__1___boxed(lean_object* x_1) {
      |                          ^
/Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:1891:26: note: previous definition is here
 1891 | LEAN_EXPORT lean_object* l_Turing_PartrecToTM2_K_x27___sizeOf__1___boxed(lean_object* x_1) {
      |                          ^
/Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:2372:21: error: redefinition of '_init_l_Turing_PartrecToTM2_K_x27___sizeOf__inst'
 2372 | static lean_object* _init_l_Turing_PartrecToTM2_K_x27___sizeOf__inst() {
      |                     ^
/Users/cruis/Documents/Lean4SAT/.lake/packages/mathlib/.lake/build/ir/Mathlib/Computability/TMToPartrec.c:1909:21: note: previous definition is here
 1909 | static lean_object* _init_l_Turing_PartrecToTM2_K_x27___sizeOf__inst() {
      |                     ^
5 errors generated.
error: external command '/Users/cruis/.elan/toolchains/leanprover--lean4---v4.22.0-rc2/bin/clang' exited with code 1
Some required builds logged failures:
- Mathlib.Computability.TMToPartrec:c.o
error: build failed

FYI this is my setting for the lakefile, which works fine for older version of Mathlib (4.16.0) :

defaultFacets := #[LeanLib.sharedFacet]
moreLinkArgs :=
  #["-L.lake/packages/aesop/.lake/build/lib/", "-lAesop",
    "-L.lake/packages/Cli/.lake/build/lib/", "-lCli",
    "-L.lake/packages/importGraph/.lake/build/lib/", "-lImportGraph",
    "-L.lake/packages/mathlib/.lake/build/lib/", "-lMathlib",
    "-L.lake/packages/proofwidgets/.lake/build/lib/", "-lProofWidgets",
    "-L.lake/packages/Qq/.lake/build/lib/", "-lQq",
    "-L.lake/packages/batteries/.lake/build/lib/", "-lBatteries",
    "-L.lake/packages/LeanSearchClient/.lake/build/lib/", "-lLeanSearchClient",
    "-L.lake/packages/plausible/.lake/build/lib/", "-lPlausible",
    "-lLake", "-lLean"]

Any suggestion will be greatly appreciated!