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'
/
This commit is contained in:
Leonardo de Moura 2021-03-04 16:38:20 -08:00
parent b6d86fdd57
commit cf11adfce3

View file

@ -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