From 1d66c32d5fef161fbcb354da1725d1f7e3457ca6 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 19 Feb 2024 16:34:21 +0100 Subject: [PATCH] fix: weaken builtin widget collision check --- src/Lean/Widget/UserWidget.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index d407de512c3e..e534fecfe295 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -95,8 +95,9 @@ builtin_initialize widgetModuleAttrImpl : AttributeImpl ← let e ← mkAppM ``ToModule.toModule #[.const decl []] let mod ← evalModule e let env ← getEnv - if let some _ := (← builtinModulesRef.get).find? mod.javascriptHash then - logWarning m!"A builtin widget module with the same hash(JS source code) was already registered." + unless builtin do -- don't warn on collision between previous and current stage + if let some _ := (← builtinModulesRef.get).find? mod.javascriptHash then + logWarning m!"A builtin widget module with the same hash(JS source code) was already registered." if let some (n, _) := moduleRegistry.getState env |>.find? mod.javascriptHash then logWarning m!"A widget module with the same hash(JS source code) was already registered at {Expr.const n []}." let env ← getEnv