From bc072eceea968c9c7b0969edd1e015cd52a47eb6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 18 Oct 2020 12:22:20 -0700
Subject: [PATCH] chore: document temporary workaround

---
 src/Lean/Message.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index f44210053a..3258418f20 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -305,6 +305,8 @@ macro_rules
   let r ← Lean.Syntax.expandInterpolatedStrChunks chunks (fun a b => `($a ++ $b)) (fun a => `(toMessageData $a))
   `(($r : MessageData))
 
+-- TODO: interpreter should not compiled code when building stdlib.
+-- The following instances cannot be defined before `syntax` because it would change the internal syntax node kinds and break the build.
 instance {α} [ToMessageData α] : ToMessageData (Option α) := ⟨fun | none => "none" | some e => "some ({toMessageData e})"⟩
 instance : ToMessageData (Option Expr) := ⟨fun | none => "<not-available>" | some e => toMessageData e⟩