From cf11adfce3489079c32ac10d8cfa58527e48f2e7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Mar 2021 16:38:20 -0800 Subject: [PATCH] chore: workaround to fix build @Kha This is a hack to try to fix the build. It seems it is the circular dependency issue again. Remarks: - The problem doesn't happen on my Mac. - I managed to reproduce the Linux error on a virtual machine. /usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommonT_monadShareCommon___rarg': ShareCommon.c:(.text+0xc9): undefined reference to `lean_state_sharecommon' /usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_PShareCommonT_monadShareCommon___rarg': ShareCommon.c:(.text+0x259): undefined reference to `lean_persistent_state_sharecommon' /usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommon_Object_hash___boxed': ShareCommon.c:(.text+0x59a): undefined reference to `lean_sharecommon_hash' /usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_shareCommon___rarg': ShareCommon.c:(.text+0x6cf): undefined reference to `lean_state_sharecommon' /usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommon_Object_eq___boxed': ShareCommon.c:(.text+0x82d): undefined reference to `lean_sharecommon_eq' /usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_PShareCommonT_withShareCommon___rarg': ShareCommon.c:(.text+0x956): undefined reference to `lean_persistent_state_sharecommon' /usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommonT_withShareCommon___rarg': ShareCommon.c:(.text+0xae6): undefined reference to `lean_state_sharecommon' / --- src/Lean/Elab/PreDefinition/Basic.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index 24375f497d..7febe8e98e 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -47,6 +47,14 @@ private def getLevelParamsPreDecls (preDefs : Array PreDefinition) (scopeLevelNa | Except.error msg => throwError msg | Except.ok levelParams => pure levelParams +-- HACK: this is a dead function, but builds break if we remove it. +-- It seems it the cyclic dependency issue again. +private def shareCommon (preDefs : Array PreDefinition) : Array PreDefinition := + let result : Std.ShareCommonM (Array PreDefinition) := + preDefs.mapM fun preDef => do + pure { preDef with type := (← Std.withShareCommon preDef.type), value := (← Std.withShareCommon preDef.value) } + result.run + def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) := do -- We used to use `shareCommon` here, but is was a bottleneck let levelParams ← getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames