Clarify docstring and add comment based on GitHub thread

Author: david-christiansen

src/Lean/BuiltinDocAttr.lean

@@ -19,7 +19,7 @@ def declareBuiltinDocStringAndRanges (declName : Name) : AttrM Unit := do
 Makes the documentation and location of a declaration available as a builtin.
 
 This allows the documentation of core Lean features to be visible without importing the file they
-are defined in. This is only possible because of bootstrapping and should not be used outside of
+are defined in. This is only useful during bootstrapping and should not be used outside of
 the Lean source code.
 -/
 @[builtin_init, builtin_doc]

src/Lean/PrettyPrinter/Formatter.lean

@@ -100,6 +100,10 @@ unsafe builtin_initialize combinatorFormatterAttribute : ParserCompiler.Combinat
     "Register a formatter for a parser combinator"
     `Lean.PrettyPrinter.mkCombinatorFormatterAttribute -- TODO (bootstrapping): remove if possible
 
+-- More details on TODO: Removing this would lead to an environment extension with a name that
+-- doesn't match what's saved in the oleans, so tests don't pass. Removing it will require a
+-- non-CI stage0 update, or careful work to keep the test working across updates.
+
 namespace Formatter
 
 open Lean.Core