From f3aeff4e812e47b495f8bcfac367210979362a34 Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@meta.com>
Date: Tue, 10 Jun 2025 02:38:40 +0000
Subject: [PATCH] bump to v4.20.0

---
 docs/source/conf.py                            | 2 +-
 lean-toolchain                                 | 1 +
 pyproject.toml                                 | 2 +-
 src/lean_dojo/constants.py                     | 2 +-
 src/lean_dojo/data_extraction/ExtractData.lean | 2 +-
 5 files changed, 5 insertions(+), 4 deletions(-)
 create mode 100644 lean-toolchain

diff --git a/docs/source/conf.py b/docs/source/conf.py
index a47e7f9e..d5f7a843 100644
--- a/docs/source/conf.py
+++ b/docs/source/conf.py
@@ -13,7 +13,7 @@
 project = "LeanDojo"
 copyright = "2023, LeanDojo Team"
 author = "Kaiyu Yang"
-release = "4.19.0"
+release = "4.20.0"
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 00000000..5e485899
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.20.0
\ No newline at end of file
diff --git a/pyproject.toml b/pyproject.toml
index c7009f9f..859aac53 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -12,7 +12,7 @@ exclude = [
 
 [project]
 name = "lean-dojo"
-version = "4.19.0"
+version = "4.20.0"
 authors = [
   { name="Kaiyu Yang", email="kaiyuy@meta.com" },
 ]
diff --git a/src/lean_dojo/constants.py b/src/lean_dojo/constants.py
index fd512df1..93612daa 100644
--- a/src/lean_dojo/constants.py
+++ b/src/lean_dojo/constants.py
@@ -14,7 +14,7 @@
 
 load_dotenv()
 
-__version__ = "4.19.0"
+__version__ = "4.20.0"
 
 logger.remove()
 if "VERBOSE" in os.environ or "DEBUG" in os.environ:
diff --git a/src/lean_dojo/data_extraction/ExtractData.lean b/src/lean_dojo/data_extraction/ExtractData.lean
index 8ef6a341..0c61c5e4 100644
--- a/src/lean_dojo/data_extraction/ExtractData.lean
+++ b/src/lean_dojo/data_extraction/ExtractData.lean
@@ -406,7 +406,7 @@ end Traversal
 open Traversal
 
 
-def getImports (header: Syntax) : IO String := do
+def getImports (header: TSyntax `Lean.Parser.Module.header) : IO String := do
   -- Similar to `lean --deps` in Lean 3.
   let mut s := ""