diff --git a/Mathlib.lean b/Mathlib.lean
index 9517e4c849841..4ba585872ad68 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1283,6 +1283,9 @@ import Mathlib.Data.Bool.Basic
 import Mathlib.Data.Bool.Count
 import Mathlib.Data.Bool.Set
 import Mathlib.Data.Bracket
+import Mathlib.Data.Buffer.Basic
+import Mathlib.Data.Buffer.Parser.Basic
+import Mathlib.Data.Buffer.Parser.Numeral
 import Mathlib.Data.Bundle
 import Mathlib.Data.ByteArray
 import Mathlib.Data.Char
diff --git a/Mathlib/Data/Buffer/Basic.lean b/Mathlib/Data/Buffer/Basic.lean
new file mode 100644
index 0000000000000..5509bb54b611a
--- /dev/null
+++ b/Mathlib/Data/Buffer/Basic.lean
@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2020 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+
+! This file was ported from Lean 3 source module data.buffer.basic
+! leanprover-community/mathlib commit 2220b0cbab795e73674b8191170b0cc68c6b54a8
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+
+Porting note:
+As the parsing framework has completely changed in Lean 4
+there is no point porting these files directly.
+They can be rewritten from scratch as needed, just as for tactics.
+-/
diff --git a/Mathlib/Data/Buffer/Parser/Basic.lean b/Mathlib/Data/Buffer/Parser/Basic.lean
new file mode 100644
index 0000000000000..6886d93acb718
--- /dev/null
+++ b/Mathlib/Data/Buffer/Parser/Basic.lean
@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2020 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+
+! This file was ported from Lean 3 source module data.buffer.parser.basic
+! leanprover-community/mathlib commit 2220b0cbab795e73674b8191170b0cc68c6b54a8
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+
+Porting note:
+As the parsing framework has completely changed in Lean 4
+there is no point porting these files directly.
+They can be rewritten from scratch as needed, just as for tactics.
+-/
diff --git a/Mathlib/Data/Buffer/Parser/Numeral.lean b/Mathlib/Data/Buffer/Parser/Numeral.lean
new file mode 100644
index 0000000000000..0ca622aac1e42
--- /dev/null
+++ b/Mathlib/Data/Buffer/Parser/Numeral.lean
@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2020 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+
+! This file was ported from Lean 3 source module data.buffer.parser.numeral
+! leanprover-community/mathlib commit 2220b0cbab795e73674b8191170b0cc68c6b54a8
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+
+Porting note:
+As the parsing framework has completely changed in Lean 4
+there is no point porting these files directly.
+They can be rewritten from scratch as needed, just as for tactics.
+-/