diff --git a/docs/source/getting-started.rst b/docs/source/getting-started.rst
index f76493c..2d10ba4 100644
--- a/docs/source/getting-started.rst
+++ b/docs/source/getting-started.rst
@@ -229,28 +229,27 @@ We use LeanDojo to trace the repo in Python by specifying its URL and a commit h
from lean_dojo import LeanGitRepo, trace
- repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "a61b40b90afba0ee5a3357665a86f7d0bb57461d")
+ repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "fd14c4c8b29cc74a082e5ae6f64c2fb25b28e15e")
trace(repo, dst_dir="traced_lean4-example")
After a few minutes or one hour (depending on #CPUs), it generates a :file:`traced_lean4-example` directory with the subdirectories below.
-The directory structure is different from that of Lean 3, as Lean 4 uses a different build system.
+The directory structure is different from that of Lean 3, as Lean 4 uses a different build system.
Please check out :ref:`troubleshooting` if you encounter any issue.
::
traced_lean4-example
└─lean4-example
- ├─lake-packages
- │ ├─lean4
- │ └─...
- ├─build
- │ ├─ir
- │ │ ├─Lean4Example.dep_paths
- │ │ ├─Lean4Example.ast.json
- │ │ └─Lean4Example.trace.xml
- │ ├─lib
- │ │ └─Lean4Example.olean
- │ └─bin
+ ├─.lake
+ │ ├─packages
+ │ │ └─lean4
+ │ └─build
+ │ ├─ir
+ │ │ ├─Lean4Example.dep_paths
+ │ │ ├─Lean4Example.ast.json
+ │ │ └─Lean4Example.trace.xml
+ │ └─lib
+ │ └─Lean4Example.olean
├─Lean4Example.lean
└─...
@@ -264,7 +263,7 @@ and :file:`lean-example` is the traced example repo. We call them "traced" becau
* :file:`*.trace.xml`: Syntactic and semantic information extracted from Lean.
The most important one is :file:`*.trace.xml`. Its format is different from Lean 3.
-For example, below is :file:`traced_lean4-example/lean4-example/build/ir/Lean4Example.trace.xml`:
+For example, below is :file:`traced_lean4-example/lean4-example/.lake/build/ir/Lean4Example.trace.xml`:
.. code-block::
:caption: Lean4Example.trace.xml
@@ -281,8 +280,8 @@ For example, below is :file:`traced_lean4-example/lean4-example/build/ir/Lean4Ex
-
-
+
+
@@ -313,7 +312,7 @@ For example, below is :file:`traced_lean4-example/lean4-example/build/ir/Lean4Ex
-
+
@@ -359,13 +358,13 @@ For example, below is :file:`traced_lean4-example/lean4-example/build/ir/Lean4Ex
-
+
-
+
@@ -380,7 +379,7 @@ For example, below is :file:`traced_lean4-example/lean4-example/build/ir/Lean4Ex
-
+
@@ -421,7 +420,7 @@ For example, below is :file:`traced_lean4-example/lean4-example/build/ir/Lean4Ex
-
+
@@ -439,7 +438,7 @@ For example, below is :file:`traced_lean4-example/lean4-example/build/ir/Lean4Ex
-
+
@@ -486,7 +485,7 @@ can be downloaded from `our AWS S3 `_ (see :
from lean_dojo import *
- repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "a61b40b90afba0ee5a3357665a86f7d0bb57461d")
+ repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "fd14c4c8b29cc74a082e5ae6f64c2fb25b28e15e")
theorem = Theorem(repo, "Lean4Example.lean", "hello_world")
with Dojo(theorem) as (dojo, init_state):
diff --git a/docs/source/limitations.rst b/docs/source/limitations.rst
index 789a388..88576d3 100644
--- a/docs/source/limitations.rst
+++ b/docs/source/limitations.rst
@@ -10,6 +10,7 @@ Limitations
LeanDojo has the following limitations. Addressing them won't be our priority in the near future, but we welcome contributions:
* LeanDojo cannot extract data from the `lean4 `_ repo itself nor interact with theorems in it.
+* Currently, LeanDojo cannot process Lean repos that use FFI, e.g., [LeanCopilot](https://github.com/lean-dojo/LeanCopilot).
* LeanDojo does not support term-based proofs or proofs that mixes tactics and terms.
* Entering all tactic-style proofs in mathlib 3 to LeanDojo, we found ~1.4% of them are misjudged as incorrect. The errors fall into a few categories documented in `test_unexpected_errors.py `_. We didn't perform this analysis on Lean 4.
* Theorems extracted by LeanDojo are "syntactic theorems", i.e., they are Lean constants defined using keywords :code:`theorem` or :code:`lemma`. First, they are not guaranteed to be real theorems (Lean constants of type :code:`Prop`). Second, theorems defined in other ways (e.g., using :code:`def`) are not extracted.
diff --git a/docs/source/user-guide.rst b/docs/source/user-guide.rst
index 0313bdc..ef40ed0 100644
--- a/docs/source/user-guide.rst
+++ b/docs/source/user-guide.rst
@@ -236,7 +236,7 @@ LeanDojo's behavior can be configured through the following environment variable
* :code:`TACTIC_CPU_LIMIT`: Number of CPUs for executing tactics (see the `--cpus` flag of `docker run `_) when interacting with Lean (only applicable when :code:`CONTAINER=docker`). Default to 1.
* :code:`TACTIC_MEMORY_LIMIT`: Maximum memory when interacting with Lean (see the `--memory` flag of `docker run `_) (only applicable when :code:`CONTAINER=docker`). Default to 16 GB.
* :code:`GITHUB_ACCESS_TOKEN`: GitHub `personal access token `_ for using the GitHub API. They are optional. If provided, they can increase the `API rate limit `_.
-* :code:`LOAD_USED_DEPS_ONLY`: Setting it to any value will cause LeanDojo to load only the dependency files that are actually used by the target repo. Otherwise, for Lean 4, it will load all files in the dependency repos. Not set by default.
+* :code:`LOAD_USED_PACKAGES_ONLY`: Setting it to any value will cause LeanDojo to load only the dependency files that are actually used by the target repo. Otherwise, for Lean 4, it will load all files in the dependency repos. Not set by default.
* :code:`VERBOSE` or :code:`DEBUG`: Setting either of them to any value will cause LeanDojo to print debug information. Not set by default.
LeanDojo supports `python-dotenv `_. You can use it to manage environment variables in a :file:`.env` file.
diff --git a/pyproject.toml b/pyproject.toml
index 0514c59..bb22345 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -13,7 +13,7 @@ exclude = [
[project]
name = "lean-dojo"
-version = "1.4.0"
+version = "1.4.1"
authors = [
{ name="Kaiyu Yang", email="kaiyuy@caltech.edu" },
]
diff --git a/scripts/generate-benchmark-lean3.ipynb b/scripts/generate-benchmark-lean3.ipynb
index baeade0..e79f4b0 100644
--- a/scripts/generate-benchmark-lean3.ipynb
+++ b/scripts/generate-benchmark-lean3.ipynb
@@ -42,7 +42,7 @@
"\n",
"import lean_dojo\n",
"from lean_dojo import *\n",
- "from lean_dojo.constants import LEAN3_DEPS_DIR\n",
+ "from lean_dojo.constants import LEAN3_PACKAGES_DIR\n",
"\n",
"random.seed(3407) # https://arxiv.org/abs/2109.08203\n",
"\n",
@@ -220,7 +220,7 @@
" return str(thm.theorem.file_path)\n",
" else:\n",
" # The theorem belongs to one of the dependencies.\n",
- " return f\"{LEAN3_DEPS_DIR}/{thm.repo.name}/{thm.theorem.file_path}\"\n",
+ " return f\"{LEAN3_PACKAGES_DIR}/{thm.repo.name}/{thm.theorem.file_path}\"\n",
"\n",
"\n",
"def export_proofs(\n",
diff --git a/scripts/generate-benchmark-lean4.ipynb b/scripts/generate-benchmark-lean4.ipynb
index 85c95d0..e8bcc7f 100644
--- a/scripts/generate-benchmark-lean4.ipynb
+++ b/scripts/generate-benchmark-lean4.ipynb
@@ -42,7 +42,7 @@
"\n",
"import lean_dojo\n",
"from lean_dojo import *\n",
- "from lean_dojo.constants import LEAN4_DEPS_DIR\n",
+ "from lean_dojo.constants import LEAN4_PACKAGES_DIR\n",
"\n",
"random.seed(3407) # https://arxiv.org/abs/2109.08203\n",
"\n",
@@ -224,7 +224,7 @@
" # The theorem belongs to one of the dependencies.\n",
" for name, dep in traced_repo.dependencies.items():\n",
" if dep == thm.repo:\n",
- " return f\"{LEAN4_DEPS_DIR}/{name}/{thm.theorem.file_path}\"\n",
+ " return f\"{LEAN4_PACKAGES_DIR}/{name}/{thm.theorem.file_path}\"\n",
" raise ValueError(f\"Unable to find the dependency {thm.repo}\")\n",
"\n",
"\n",
diff --git a/src/lean_dojo/__init__.py b/src/lean_dojo/__init__.py
index 3df6ff6..eda3a13 100644
--- a/src/lean_dojo/__init__.py
+++ b/src/lean_dojo/__init__.py
@@ -1,7 +1,6 @@
import os
from .data_extraction.trace import (
trace,
- trace_local,
get_traced_repo_path,
is_available_in_cache,
)
diff --git a/src/lean_dojo/constants.py b/src/lean_dojo/constants.py
index c3b52aa..3bb004b 100644
--- a/src/lean_dojo/constants.py
+++ b/src/lean_dojo/constants.py
@@ -15,7 +15,7 @@
load_dotenv()
-__version__ = "1.4.0"
+__version__ = "1.4.1"
logger.remove()
if "VERBOSE" in os.environ or "DEBUG" in os.environ:
@@ -53,7 +53,7 @@
LEAN3_URL = "https://github.com/leanprover-community/lean"
"""The URL of the Lean 3 repo."""
-LEAN3_DEPS_DIR = Path("_target/deps")
+LEAN3_PACKAGES_DIR = Path("_target/deps")
"""The directory where Lean 3 dependencies are stored."""
LEAN4_URL = "https://github.com/leanprover/lean4"
@@ -80,12 +80,19 @@
LEAN4_NIGHTLY_REPO = GITHUB.get_repo("leanprover/lean4-nightly")
"""The GitHub Repo for Lean 4 nightly releases."""
-LEAN4_DEPS_DIR = Path("lake-packages")
-"""The directory where Lean 4 dependencies are stored."""
+LEAN4_PACKAGES_DIR_OLD = Path("lake-packages")
+"""The directory where Lean 4 dependencies are stored (before v4.3.0-rc2)."""
-LOAD_USED_DEPS_ONLY = "LOAD_USED_DEPS_ONLY" in os.environ
+LEAN4_PACKAGES_DIR = Path(".lake/packages")
+"""The directory where Lean 4 dependencies are stored (since v4.3.0-rc2)."""
+
+LOAD_USED_PACKAGES_ONLY = "LOAD_USED_PACKAGES_ONLY" in os.environ
"""Only load depdendency files that are actually used by the target repo."""
+LEAN4_BUILD_DIR = Path(".lake/build")
+
+LEAN_BUILD_DIR_OLD = Path("build")
+
TACTIC_TIMEOUT = int(os.getenv("TACTIC_TIMEOUT", 5000))
"""Maximum time (in milliseconds) before interrupting a tactic when interacting with Lean (only for Lean 3).
"""
diff --git a/src/lean_dojo/data_extraction/ExtractData.lean b/src/lean_dojo/data_extraction/ExtractData.lean
index 3155883..8d5e8de 100644
--- a/src/lean_dojo/data_extraction/ExtractData.lean
+++ b/src/lean_dojo/data_extraction/ExtractData.lean
@@ -1,4 +1,6 @@
import Lean
+import Lake
+
open Lean Elab System
@@ -180,43 +182,57 @@ private def trim (path : FilePath) : FilePath :=
| _ => path
+def packagesDir : FilePath :=
+ if Lake.defaultPackagesDir == "packages" then -- Lean >= v4.3.0-rc2
+ ".lake" / Lake.defaultPackagesDir
+ else -- Lean < v4.3.0-rc2
+ Lake.defaultPackagesDir
+
+
+def buildDir : FilePath :=
+ if Lake.defaultPackagesDir == "packages" then -- Lean >= v4.3.0-rc2
+ ".lake/build"
+ else -- Lean < v4.3.0-rc2
+ "build"
+
+
+def libDir : FilePath := buildDir / "lib"
+
+
/--
Convert the path of a *.lean file to its corresponding file (e.g., *.olean) in the "build" directory.
-/
-def toBuildDir (subDir : String) (path : FilePath) (ext : String) : Option FilePath :=
+def toBuildDir (subDir : FilePath) (path : FilePath) (ext : String) : Option FilePath :=
let path' := (trim path).withExtension ext
- match relativeTo path' "lake-packages/lean4/src" with
- | some p => some $ "lake-packages/lean4/lib" / p
- | none => match relativeTo path' "lake-packages" with
+ match relativeTo path' $ packagesDir / "lean4/src" with
+ | some p => packagesDir / "lean4/lib" / p
+ | none => match relativeTo path' packagesDir with
| some p =>
match p.components with
| [] => none
- | hd :: tl => some $ "lake-packages" / hd / "build" / subDir / (mkFilePath tl)
- | none => some $ "build" / subDir / path'
+ | hd :: tl => packagesDir / hd / buildDir / subDir / (mkFilePath tl)
+ | none => buildDir / subDir / path'
/--
The reverse of `toBuildDir`.
-/
-def toSrcDir (path : FilePath) (ext : String) : Option FilePath :=
+-- proofwidgets/build/lib/ProofWidgets/Compat.lean
+-- proofwidgets/.lake/build/lib
+def toSrcDir! (path : FilePath) (ext : String) : FilePath :=
let path' := (trim path).withExtension ext
- match relativeTo path' "lake-packages/lean4/lib" with
- | some p => some $ "lake-packages/lean4/src" / p
+ match relativeTo path' $ packagesDir / "lean4/lib" with
+ | some p => -- E.g., `.lake/packages/lean4/lib/lean/Init/Prelude.olean` -> `.lake/packages/lean4/src/lean/Init/Prelude.lean`
+ packagesDir / "lean4/src" / p
| none =>
- match relativeTo path' "lake-packages" with
- | some p =>
- let comps := p.components
- assert! comps[1]! == "build"
- match comps with
- | t0 :: "build" :: "lib" :: t1 => mkFilePath $ "lake-packages" :: t0 :: t1
- | _ :: _ :: _ :: tl => mkFilePath tl
- | _ => "invalid path"
+ match relativeTo path' packagesDir with
+ | some p => -- E.g., `.lake/packages/aesop/.lake/build/lib/Aesop.olean`-> `.lake/packages/aesop/Aesop.lean`
+ let pkgName := p.components.head!
+ let sep := "build/lib/"
+ packagesDir / pkgName / (p.toString.splitOn sep |>.tail!.head!)
| none =>
- let comps := path'.components
- assert! comps[0]! == "build"
- match comps with
- | _ :: _ :: tl => mkFilePath tl
- | _ => "invalid path"
+ -- E.g., `.lake/build/lib/Mathlib/LinearAlgebra/Basic.olean` -> `Mathlib/LinearAlgebra/Basic.lean`
+ relativeTo path' libDir |>.get!
/--
@@ -234,13 +250,16 @@ def findLean (mod : Name) : IO FilePath := do
let modStr := mod.toString
if modStr.startsWith "«lake-packages»." then
return FilePath.mk (modStr.replace "«lake-packages»" "lake-packages" |>.replace "." "/") |>.withExtension "lean"
+ if modStr.startsWith "«.lake»." then
+ return FilePath.mk (modStr.replace "«.lake»" ".lake" |>.replace "." "/") |>.withExtension "lean"
let olean ← findOLean mod
-- Remove a "build/lib/" substring from the path.
- let lean := olean.toString.replace (toString (FilePath.mk "build" / "lib") ++ FilePath.pathSeparator.toString) ""
+ let lean := olean.toString.replace ".lake/build/lib/" ""
+ |>.replace "build/lib/" "" |>.replace "lib/lean/Lake/" "lib/lean/lake/Lake/"
let mut path := FilePath.mk lean |>.withExtension "lean"
let leanLib ← getLibDir (← getBuildDir)
if let some p := relativeTo path leanLib then
- path := "lake-packages/lean4/src/lean" / p
+ path := packagesDir / "lean4/src/lean" / p
assert! ← path.pathExists
return path
@@ -404,15 +423,10 @@ unsafe def processFile (path : FilePath) : IO Unit := do
let (trace, _) ← traceM.run'.toIO {fileName := s!"{path}", fileMap := FileMap.ofString input} {env := env}
let cwd ← IO.currentDir
- let is_lean := cwd.fileName == "lean4"
+ assert! cwd.fileName != "lean4"
let some relativePath := Path.relativeTo path cwd | throw $ IO.userError s!"Invalid path: {path}"
- let json_path := (
- if is_lean then
- mkFilePath $ "lib" :: (relativePath.withExtension "ast.json").components.tail!
- else
- (Path.toBuildDir "ir" relativePath "ast.json").get!
- )
+ let json_path := Path.toBuildDir "ir" relativePath "ast.json" |>.get!
Path.makeParentDirs json_path
IO.FS.writeFile json_path (toJson trace).pretty
@@ -421,27 +435,23 @@ unsafe def processFile (path : FilePath) : IO Unit := do
for dep in headerToImports header do
let oleanPath ← findOLean dep.module
if oleanPath.isRelative then
- let some leanPath := Path.toSrcDir oleanPath "lean" | throw $ IO.userError s!"Invalid path: {oleanPath}"
+ let leanPath := Path.toSrcDir! oleanPath "lean"
+ assert! ← leanPath.pathExists
s := s ++ "\n" ++ leanPath.toString
- else if !(oleanPath.toString.endsWith "/lib/lean/Init.olean") then
- s := s ++ "\n"
- if !is_lean then
- s := s ++ "lake-packages/lean4/"
+ else if ¬(oleanPath.toString.endsWith "/lib/lean/Init.olean") then
+ let mut p := (Path.packagesDir / "lean4").toString ++ FilePath.pathSeparator.toString
let mut found := false
for c in (oleanPath.withExtension "lean").components do
if c == "lib" then
found := true
- s := s ++ "src"
+ p := p ++ "src"
continue
if found then
- s := s ++ FilePath.pathSeparator.toString ++ c
+ p := p ++ FilePath.pathSeparator.toString ++ c
+ assert! ← FilePath.mk p |>.pathExists
+ s := s ++ "\n" ++ p
- let dep_path := (
- if is_lean then
- mkFilePath $ "lib" :: (relativePath.withExtension "dep_paths").components.tail!
- else
- (Path.toBuildDir "ir" relativePath "dep_paths").get!
- )
+ let dep_path := Path.toBuildDir "ir" relativePath "dep_paths" |>.get!
Path.makeParentDirs dep_path
IO.FS.writeFile dep_path s.trim
@@ -461,15 +471,9 @@ def shouldProcess (path : FilePath) : IO Bool := do
let cwd ← IO.currentDir
let some relativePath := Path.relativeTo path cwd |
throw $ IO.userError s!"Invalid path: {path}"
-
- if cwd.fileName == "lean4" then
- let oleanPath := mkFilePath $ "lib" ::
- (relativePath.withExtension "olean").components.tail!
- return ← oleanPath.pathExists
- else
- let some oleanPath := Path.toBuildDir "lib" relativePath "olean" |
- throw $ IO.userError s!"Invalid path: {path}"
- return ← oleanPath.pathExists
+ let some oleanPath := Path.toBuildDir "lib" relativePath "olean" |
+ throw $ IO.userError s!"Invalid path: {path}"
+ return ← oleanPath.pathExists
unsafe def main (args : List String) : IO Unit := do
diff --git a/src/lean_dojo/data_extraction/ast/lean4/node.py b/src/lean_dojo/data_extraction/ast/lean4/node.py
index bcea2ab..6af2a8b 100644
--- a/src/lean_dojo/data_extraction/ast/lean4/node.py
+++ b/src/lean_dojo/data_extraction/ast/lean4/node.py
@@ -986,15 +986,17 @@ def from_data(
children = _parse_children(node_data, lean_file)
assert isinstance(children[0], AtomNode4) and children[0].val == "theorem"
- assert isinstance(children[1], CommandDeclidNode4)
- decl_id_node = children[1]
- ident_node = decl_id_node.children[0]
- if isinstance(ident_node, IdentNode4):
- name = ident_node.val
+ declid_node = children[1]
+ if isinstance(declid_node, CommandDeclidAntiquotNode4):
+ name = None
else:
- assert isinstance(ident_node, IdentAntiquotNode4)
- name = ident_node.get_ident()
+ ident_node = declid_node.children[0]
+ if isinstance(ident_node, IdentNode4):
+ name = ident_node.val
+ else:
+ assert isinstance(ident_node, IdentAntiquotNode4)
+ name = ident_node.get_ident()
assert isinstance(children[2], CommandDeclsigNode4)
decl_val_node = children[3]
diff --git a/src/lean_dojo/data_extraction/build_lean4_repo.py b/src/lean_dojo/data_extraction/build_lean4_repo.py
index def461e..82cda1b 100644
--- a/src/lean_dojo/data_extraction/build_lean4_repo.py
+++ b/src/lean_dojo/data_extraction/build_lean4_repo.py
@@ -3,6 +3,7 @@
Only this file runs in Docker. So it must be self-contained.
"""
import os
+import re
import sys
import shutil
import itertools
@@ -96,6 +97,13 @@ def launch_progressbar(paths: List[Union[str, Path]]) -> Generator[None, None, N
p.kill()
+def get_lean_version() -> str:
+ """Get the version of Lean."""
+ output = run_cmd("lean --version", capture_output=True).strip()
+ m = re.match(r"Lean \(version (?P\S+?),", output)
+ return m["version"]
+
+
def check_files() -> None:
"""Check if all *.lean files have been processed to produce *.ast.json and *.dep_paths files."""
cwd = Path.cwd()
@@ -109,8 +117,23 @@ def check_files() -> None:
missing_deps = {p.with_suffix(".dep_paths") for p in cs - deps}
if len(missing_jsons) > 0 or len(missing_deps) > 0:
for p in missing_jsons.union(missing_deps):
- logger.error(f"Missing {p}")
- raise RuntimeError("Missing intermediate files.")
+ logger.warning(f"Missing {p}")
+
+
+def is_new_version(v) -> bool:
+ """Check if ``v`` is at least `4.3.0-rc2`."""
+ major, minor, patch = [int(_) for _ in v.split("-")[0].split(".")]
+ if major < 4 or (major == 4 and minor < 3):
+ return False
+ if (
+ major > 4
+ or (major == 4 and minor > 3)
+ or (major == 4 and minor == 3 and patch > 0)
+ ):
+ return True
+ assert major == 4 and minor == 3 and patch == 0
+ rc = int(v.split("-")[1][2:])
+ return rc >= 2
def main() -> None:
@@ -122,13 +145,19 @@ def main() -> None:
logger.info(f"Building {repo_name}")
run_cmd("lake build")
- # Copy the Lean 4 stdlib into lake-packages.
+ # Copy the Lean 4 stdlib into the path of packages.
lean_prefix = run_cmd(f"lean --print-prefix", capture_output=True).strip()
- shutil.copytree(lean_prefix, "lake-packages/lean4")
+ if is_new_version(get_lean_version()):
+ packages_path = ".lake/packages"
+ build_path = ".lake/build"
+ else:
+ packages_path = "lake-packages"
+ build_path = "build"
+ shutil.copytree(lean_prefix, f"{packages_path}/lean4")
# Run ExtractData.lean to extract ASTs, tactic states, and premise information.
logger.info(f"Tracing {repo_name}")
- with launch_progressbar(["build", "lake-packages"]):
+ with launch_progressbar([build_path, packages_path]):
run_cmd(
f"lake env lean --threads {num_procs} --run ExtractData.lean",
capture_output=True,
diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py
index 7219aff..aef0208 100644
--- a/src/lean_dojo/data_extraction/lean.py
+++ b/src/lean_dojo/data_extraction/lean.py
@@ -23,7 +23,17 @@
working_directory,
get_latest_commit,
)
-from ..constants import LEAN3_URL, LEAN4_URL, LEAN4_REPO, LEAN4_NIGHTLY_REPO
+from ..constants import (
+ LEAN3_URL,
+ LEAN4_URL,
+ LEAN4_REPO,
+ LEAN4_NIGHTLY_REPO,
+ LEAN3_PACKAGES_DIR,
+ LEAN4_PACKAGES_DIR,
+ LEAN4_PACKAGES_DIR_OLD,
+ LEAN4_BUILD_DIR,
+ LEAN_BUILD_DIR_OLD,
+)
def _to_commit_hash(repo: Repository, label: str) -> str:
@@ -265,18 +275,26 @@ def __getitem__(self, key) -> str:
_COMMIT_REGEX = re.compile(r"[0-9a-z]+")
-_LEAN_VERSION_REGEX = re.compile(
+_LEAN3_VERSION_REGEX = re.compile(
r"leanprover-community/lean:(?P\d+\.\d+\.\d+)"
)
+_LEAN4_VERSION_REGEX = re.compile(r"leanprover/lean4:(?Pv.+?)")
def get_lean3_version_from_config(config: Dict[str, Any]) -> str:
"""Return the required Lean version given a ``leanpkg.toml`` config."""
- m = _LEAN_VERSION_REGEX.fullmatch(config["package"]["lean_version"])
+ m = _LEAN3_VERSION_REGEX.fullmatch(config["package"]["lean_version"])
assert m is not None, "Invalid config."
return f"v{m['version']}"
+def get_lean4_version_from_config(toolchain: str) -> str:
+ """Return the required Lean version given a ``lean-toolchain`` config."""
+ m = _LEAN4_VERSION_REGEX.fullmatch(toolchain.strip())
+ assert m is not None, "Invalid config."
+ return m["version"]
+
+
def get_lean4_commit_from_config(config_dict: Dict[str, Any]) -> str:
"""Return the required Lean commit given a ``lean-toolchain`` config."""
assert "content" in config_dict, "config_dict must have a 'content' field"
@@ -318,6 +336,25 @@ class RepoInfoCache:
)
+def is_new_version(v) -> bool:
+ """Check if ``v`` is at least `v4.3.0-rc2`."""
+ if not v.startswith("v"):
+ return False
+ v = v[1:]
+ major, minor, patch = [int(_) for _ in v.split("-")[0].split(".")]
+ if major < 4 or (major == 4 and minor < 3):
+ return False
+ if (
+ major > 4
+ or (major == 4 and minor > 3)
+ or (major == 4 and minor == 3 and patch > 0)
+ ):
+ return True
+ assert major == 4 and minor == 3 and patch == 0
+ rc = int(v.split("-")[1][2:])
+ return rc >= 2
+
+
@dataclass(frozen=True)
class LeanGitRepo:
"""Git repo of a Lean project."""
@@ -448,6 +485,29 @@ def clone_and_checkout(self) -> None:
capture_output=True,
)
+ def get_packages_dir(self) -> Path:
+ """Return the path to the directory where Lean packages are stored."""
+ if self.uses_lean3:
+ return LEAN3_PACKAGES_DIR
+ else:
+ toolchain = self.get_config("lean-toolchain")
+ v = get_lean4_version_from_config(toolchain["content"])
+ if is_new_version(v):
+ return LEAN4_PACKAGES_DIR
+ else:
+ return LEAN4_PACKAGES_DIR_OLD
+
+ def get_build_dir(self) -> Path:
+ if self.uses_lean3:
+ return LEAN_BUILD_DIR_OLD
+ else:
+ toolchain = self.get_config("lean-toolchain")
+ v = get_lean4_version_from_config(toolchain["content"])
+ if is_new_version(v):
+ return LEAN4_BUILD_DIR
+ else:
+ return LEAN_BUILD_DIR_OLD
+
def get_dependencies(
self, path: Union[str, Path, None] = None
) -> Dict[str, "LeanGitRepo"]:
diff --git a/src/lean_dojo/data_extraction/trace.py b/src/lean_dojo/data_extraction/trace.py
index e346335..1cdc237 100644
--- a/src/lean_dojo/data_extraction/trace.py
+++ b/src/lean_dojo/data_extraction/trace.py
@@ -188,7 +188,3 @@ def trace(repo: LeanGitRepo, dst_dir: Optional[Union[str, Path]] = None) -> Trac
shutil.copytree(cached_path, dst_dir / cached_path.name)
return traced_repo
-
-
-def trace_local(path: Path) -> TracedRepo:
- raise NotImplementedError
diff --git a/src/lean_dojo/data_extraction/traced_data.py b/src/lean_dojo/data_extraction/traced_data.py
index c5e8d1b..d3cc1b1 100644
--- a/src/lean_dojo/data_extraction/traced_data.py
+++ b/src/lean_dojo/data_extraction/traced_data.py
@@ -12,8 +12,6 @@
from lxml import etree
from pathlib import Path
from loguru import logger
-from collections import deque
-from datetime import datetime
from dataclasses import dataclass, field
from typing import List, Optional, Dict, Any, Tuple, Generator, Union
@@ -26,15 +24,13 @@
to_dep_path,
to_json_path,
to_xml_path,
- get_line_creation_date,
- get_module,
)
from .ast.lean3.node import *
from .ast.lean4.node import *
-from ..constants import LOAD_USED_DEPS_ONLY
+from ..constants import NUM_WORKERS
+from ..constants import LOAD_USED_PACKAGES_ONLY
from .lean import LeanFile, LeanGitRepo, Theorem, Pos
from .ast.lean3.expr import Expr, ConstExpr, parse_exprs_forest
-from ..constants import NUM_WORKERS, LEAN3_DEPS_DIR, LEAN4_DEPS_DIR
@dataclass(frozen=True)
@@ -307,26 +303,6 @@ def __getstate__(self) -> Dict[str, Any]:
d["traced_file"] = None
return d
- def get_creation_date(self) -> datetime:
- """Return the date on which the theorem was added to the repo."""
- if self.root_dir.name == self.repo.name:
- dirname = self.root_dir
- elif self.uses_lean3:
- dirname = self.root_dir / LEAN3_DEPS_DIR / self.repo.name
- elif self.repo.name == "lean4":
- # Cannot determine creation date of theorems in lean4 repo.
- return datetime.min
- else:
- traced_repo = self.traced_file.traced_repo
- for name, dep in traced_repo.dependencies.items():
- if dep == self.repo:
- dirname = self.root_dir / LEAN4_DEPS_DIR / name
- break
- else:
- raise RuntimeError(f"Cannot find the dependency {self.repo}.")
- assert dirname.exists()
- return get_line_creation_date(dirname, self.file_path, self.start.line_nb)
-
@property
def start(self) -> Pos:
"""Start position in :file:`*.lean` file."""
@@ -568,6 +544,10 @@ class TracedFile:
"""Root directory (in absolute path) of the corresponding traced repo.
"""
+ repo: LeanGitRepo
+ """The Lean repo this traced file belongs to.
+ """
+
lean_file: LeanFile
"""Lean source file of this traced file.
"""
@@ -662,13 +642,15 @@ def from_traced_file(
], f"{json_path} is not a *.ast.json file"
if repo.uses_lean3:
- return cls._from_lean3_traced_file(root_dir, json_path)
+ return cls._from_lean3_traced_file(root_dir, json_path, repo)
else:
assert repo.uses_lean4, f"repo {repo} uses neither Lean 3 nor Lean 4"
- return cls._from_lean4_traced_file(root_dir, json_path)
+ return cls._from_lean4_traced_file(root_dir, json_path, repo)
@classmethod
- def _from_lean3_traced_file(cls, root_dir: Path, json_path: Path) -> "TracedFile":
+ def _from_lean3_traced_file(
+ cls, root_dir: Path, json_path: Path, repo: LeanGitRepo
+ ) -> "TracedFile":
lean_path = json_path.with_suffix("").with_suffix(".lean").relative_to(root_dir)
lean_file = LeanFile(root_dir, lean_path, uses_lean4=False)
data = json.load(json_path.open())
@@ -693,11 +675,13 @@ def _from_lean3_traced_file(cls, root_dir: Path, json_path: Path) -> "TracedFile
comments = [Comment.from_lean3_data(d, lean_file) for d in data["comments"]]
- return cls(root_dir, lean_file, ast, exprs, comments)
+ return cls(root_dir, repo, lean_file, ast, exprs, comments)
@classmethod
- def _from_lean4_traced_file(cls, root_dir: Path, json_path: Path) -> "TracedFile":
- lean_path = to_lean_path(root_dir, json_path, uses_lean4=True)
+ def _from_lean4_traced_file(
+ cls, root_dir: Path, json_path: Path, repo: LeanGitRepo
+ ) -> "TracedFile":
+ lean_path = to_lean_path(root_dir, json_path, repo)
lean_file = LeanFile(root_dir, lean_path, uses_lean4=True)
data = json.load(json_path.open())
@@ -722,7 +706,7 @@ def _from_lean4_traced_file(cls, root_dir: Path, json_path: Path) -> "TracedFile
comments,
)
- return cls(root_dir, lean_file, ast, None, comments)
+ return cls(root_dir, repo, lean_file, ast, None, comments)
@classmethod
def _post_process_lean3(
@@ -967,11 +951,11 @@ def traverse_preorder(self, callback, node_cls: Optional[type] = None):
def _get_repo_and_relative_path(self) -> Tuple[LeanGitRepo, Path]:
"""Return the repo this file belongs to, as well as the file's path relative to it."""
- deps_dir = LEAN3_DEPS_DIR if self.uses_lean3 else LEAN4_DEPS_DIR
+ packages_dir = self.traced_repo.repo.get_packages_dir()
- if self.path.is_relative_to(deps_dir):
+ if self.path.is_relative_to(packages_dir):
# The theorem belongs to one of the dependencies.
- p = self.path.relative_to(deps_dir)
+ p = self.path.relative_to(packages_dir)
name = p.parts[0]
repo = self.traced_repo.dependencies[name]
return repo, p.relative_to(name)
@@ -1039,24 +1023,25 @@ def _filter_comments(self, start: Pos, end: Pos) -> List[Comment]:
comments.append(c)
return comments
- def get_direct_dependencies(self) -> List[Tuple[str, Path]]:
+ def get_direct_dependencies(self, repo: LeanGitRepo) -> List[Tuple[str, Path]]:
"""Return the names and paths of all modules imported by the current :file:`*.lean` file."""
deps = set()
if not self.has_prelude: # Add the prelude as a dependency.
+ packages_dir = repo.get_packages_dir()
if self.uses_lean3:
init_lean = Path("library/init/default.lean")
if self.root_dir.name == "lean":
deps.add(("init", init_lean))
else:
- deps.add(("init", LEAN3_DEPS_DIR / "lean" / init_lean))
+ deps.add(("init", packages_dir / "lean" / init_lean))
else:
assert self.uses_lean4
init_lean = Path("src/lean/Init.lean")
if self.root_dir.name == "lean4":
deps.add(("Init", init_lean))
else:
- deps.add(("Init", LEAN4_DEPS_DIR / "lean4" / init_lean))
+ deps.add(("Init", packages_dir / "lean4" / init_lean))
def _callback(node: Union[ModuleNode, ModuleImportNode4], _) -> None:
if node.module is not None and node.path is not None:
@@ -1203,7 +1188,7 @@ def from_xml(
root_dir = Path(root_dir)
path = Path(path)
assert path.suffixes == [".trace", ".xml"]
- lean_path = to_lean_path(root_dir, path, repo.uses_lean4)
+ lean_path = to_lean_path(root_dir, path, repo)
lean_file = LeanFile(root_dir, lean_path, repo.uses_lean4)
tree = etree.parse(path).getroot()
@@ -1222,11 +1207,11 @@ def from_xml(
exprs = [Expr.from_xml(e) for e in exprs_tree]
comments = [Comment.from_xml(c) for c in comments_tree]
- return cls(root_dir, lean_file, ast, exprs, comments)
+ return cls(root_dir, repo, lean_file, ast, exprs, comments)
def _save_xml_to_disk(tf: TracedFile) -> None:
- xml_path = tf.root_dir / to_xml_path(tf.root_dir, tf.path, tf.uses_lean4)
+ xml_path = tf.root_dir / to_xml_path(tf.root_dir, tf.path, tf.repo)
with xml_path.open("wt") as oup:
oup.write(tf.to_xml())
@@ -1248,11 +1233,11 @@ def _build_dependency_graph(
tf = traced_files[i]
tf_path_str = str(tf.path)
- for dep_module, dep_path in tf.get_direct_dependencies():
+ for dep_module, dep_path in tf.get_direct_dependencies(repo):
dep_path_str = str(dep_path)
if not G.has_node(dep_path_str):
- xml_path = to_xml_path(root_dir, dep_path, repo.uses_lean4)
- tf_dep = TracedFile.from_xml(root_dir, xml_path, repo)
+ json_path = to_json_path(root_dir, dep_path, repo)
+ tf_dep = TracedFile.from_traced_file(root_dir, json_path, repo)
assert tf_dep.path == tf.path
G.add_node(dep_path_str, traced_file=tf_dep)
traced_files.append(tf_dep)
@@ -1365,7 +1350,7 @@ def check_sanity(self) -> None:
p.relative_to(self.root_dir) for p in self.root_dir.glob("**/*.dep_paths")
}
- if not LOAD_USED_DEPS_ONLY:
+ if not LOAD_USED_PACKAGES_ONLY:
assert len(json_files) == self.traced_files_graph.number_of_nodes()
for path_str, tf_node in self.traced_files_graph.nodes.items():
@@ -1376,18 +1361,15 @@ def check_sanity(self) -> None:
assert tf.traced_repo is None or tf.traced_repo is self
assert path in lean_files
assert (
- to_dep_path(self.root_dir, path, uses_lean4=self.uses_lean4)
- in path_files
- ), to_dep_path(self.root_dir, path, uses_lean4=self.uses_lean4)
+ to_dep_path(self.root_dir, path, self.repo) in path_files
+ ), to_dep_path(self.root_dir, path, self.repo)
assert (
- to_json_path(self.root_dir, path, uses_lean4=self.uses_lean4)
- in json_files
- ), to_json_path(self.root_dir, path, uses_lean4=self.uses_lean4)
+ to_json_path(self.root_dir, path, self.repo) in json_files
+ ), to_json_path(self.root_dir, path, self.repo)
if len(xml_files) > 0:
assert (
- to_xml_path(self.root_dir, path, uses_lean4=self.uses_lean4)
- in xml_files
- ), to_xml_path(self.root_dir, path, uses_lean4=False)
+ to_xml_path(self.root_dir, path, self.repo) in xml_files
+ ), to_xml_path(self.root_dir, path, self.repo)
@classmethod
def from_traced_files(cls, root_dir: Union[str, Path]) -> None:
@@ -1484,8 +1466,12 @@ def load_from_disk(cls, root_dir: Union[str, Path]) -> "TracedRepo":
# Start from files in the target repo as seeds.
# Only load dependency files that are actually used.
- if LOAD_USED_DEPS_ONLY:
- xml_paths = [p for p in xml_paths if not "lake-packages" in p.parts]
+ if LOAD_USED_PACKAGES_ONLY:
+ xml_paths = [
+ p
+ for p in xml_paths
+ if not "lake-packages/" in str(p) and not ".lake/packages" in str(p)
+ ]
if NUM_WORKERS <= 1:
traced_files = [
@@ -1522,6 +1508,6 @@ def get_traced_theorem(self, thm: Theorem) -> Optional[TracedTheorem]:
path = Path(thm.repo.name) / thm.file_path
else:
assert thm.repo in self.dependencies.values()
- deps_dir = LEAN3_DEPS_DIR if thm.repo.is_lean3 else LEAN4_DEPS_DIR
- path = Path(self.name) / deps_dir / thm.repo.name / thm.file_path
+ packages_dir = thm.repo.get_packages_dir()
+ path = Path(self.name) / packages_dir / thm.repo.name / thm.file_path
return self.get_traced_file(path).get_traced_theorem(thm.full_name)
diff --git a/src/lean_dojo/interaction/dojo.py b/src/lean_dojo/interaction/dojo.py
index 89c0573..c77e671 100644
--- a/src/lean_dojo/interaction/dojo.py
+++ b/src/lean_dojo/interaction/dojo.py
@@ -15,7 +15,7 @@
from ..constants import (
TMP_DIR,
- LEAN3_DEPS_DIR,
+ LEAN3_PACKAGES_DIR,
TACTIC_TIMEOUT,
TACTIC_CPU_LIMIT,
TACTIC_MEMORY_LIMIT,
@@ -109,9 +109,9 @@ def _get_all_dependencies(
stack = [lean_path]
while stack != []:
- json_path = to_json_path(root_dir, stack.pop(), repo.uses_lean4)
+ json_path = to_json_path(root_dir, stack.pop(), repo)
tf = TracedFile.from_traced_file(root_dir, json_path, repo)
- for _, d in tf.get_direct_dependencies():
+ for _, d in tf.get_direct_dependencies(repo):
if d not in all_deps:
all_deps.append(d)
stack.append(d)
@@ -293,7 +293,7 @@ def __enter__(self) -> Tuple["Dojo", State]:
raise ex
def _locate_traced_file(self, traced_repo_path: Path) -> TracedFile:
- json_path = to_json_path(traced_repo_path, self.file_path, self.uses_lean4)
+ json_path = to_json_path(traced_repo_path, self.file_path, self.repo)
return TracedFile.from_traced_file(traced_repo_path, json_path, self.repo)
def _get_unsupported_deps(self, traced_repo_path: Path) -> List[Path]:
@@ -301,7 +301,7 @@ def _get_unsupported_deps(self, traced_repo_path: Path) -> List[Path]:
if self.repo.is_lean3:
path = Path("library/system/io.lean")
else:
- path = LEAN3_DEPS_DIR / "lean/library/system/io.lean"
+ path = LEAN3_PACKAGES_DIR / "lean/library/system/io.lean"
return [path] + _get_all_dependencies(traced_repo_path, path, self.repo)
else:
# We shouldn't be interacting with the Lean 4 repo itself anyway.
diff --git a/src/lean_dojo/utils.py b/src/lean_dojo/utils.py
index b533385..8eb7616 100644
--- a/src/lean_dojo/utils.py
+++ b/src/lean_dojo/utils.py
@@ -2,7 +2,6 @@
"""
import re
import os
-import sys
import ray
import time
import urllib
@@ -12,13 +11,12 @@
import subprocess
from pathlib import Path
from loguru import logger
-from datetime import datetime
from contextlib import contextmanager
from github.Repository import Repository
from ray.util.actor_pool import ActorPool
from typing import Tuple, Union, List, Generator, Optional
-from .constants import GITHUB, NUM_WORKERS, TMP_DIR, LEAN4_DEPS_DIR
+from .constants import GITHUB, NUM_WORKERS, TMP_DIR
@contextmanager
@@ -197,20 +195,6 @@ def remove_optional_type(tp: type) -> type:
raise ValueError(f"{tp} is not Optional")
-def get_line_creation_date(repo_path: Path, file_path: Path, line_nb: int):
- """Return the date of creation of the line ``line_nb`` in the file ``file_path`` of the Git repo ``repo_path``."""
- with working_directory(repo_path):
- output, _ = execute(
- f"git log --pretty=short -u -L {line_nb},{line_nb}:{file_path}",
- capture_output=True,
- )
- m = re.match(r"commit (?P[A-Za-z0-9]+)\n", output)
- assert m is not None
- commit = m["commit"]
- output, _ = execute(f"git show -s --format=%ci {commit}", capture_output=True)
- return datetime.strptime(output.strip(), "%Y-%m-%d %H:%M:%S %z")
-
-
def read_url(url: str, num_retries: int = 1) -> str:
"""Read the contents of the URL ``url``. Retry if failed"""
while True:
@@ -285,43 +269,45 @@ def is_git_repo(path: Path) -> bool:
)
-def _from_lean_path(root_dir: Path, path: Path, uses_lean4: bool, ext: str) -> Path:
+def _from_lean_path(root_dir: Path, path: Path, repo, ext: str) -> Path:
assert path.suffix == ".lean"
if path.is_absolute():
path = path.relative_to(root_dir)
- if not uses_lean4:
+ if not repo.uses_lean4:
return path.with_suffix(ext)
- if root_dir.name == "lean4":
- return Path("lib") / path.relative_to("src").with_suffix(ext)
- elif path.is_relative_to(LEAN4_DEPS_DIR / "lean4/src"):
+ packages_dir = repo.get_packages_dir()
+ build_dir = repo.get_build_dir()
+
+ assert root_dir.name != "lean4"
+ if path.is_relative_to(packages_dir / "lean4/src"):
# E.g., "lake-packages/lean4/src/lean/Init.lean"
- p = path.relative_to(LEAN4_DEPS_DIR / "lean4/src").with_suffix(ext)
- return LEAN4_DEPS_DIR / "lean4/lib" / p
- elif path.is_relative_to(LEAN4_DEPS_DIR):
+ p = path.relative_to(packages_dir / "lean4/src").with_suffix(ext)
+ return packages_dir / "lean4/lib" / p
+ elif path.is_relative_to(packages_dir):
# E.g., "lake-packages/std/Std.lean"
- p = path.relative_to(LEAN4_DEPS_DIR).with_suffix(ext)
+ p = path.relative_to(packages_dir).with_suffix(ext)
repo_name = p.parts[0]
- return LEAN4_DEPS_DIR / repo_name / "build/ir" / p.relative_to(repo_name)
+ return packages_dir / repo_name / build_dir / "ir" / p.relative_to(repo_name)
else:
# E.g., "Mathlib/LinearAlgebra/Basics.lean"
- return Path("build/ir") / path.with_suffix(ext)
+ return build_dir / "ir" / path.with_suffix(ext)
-def to_xml_path(root_dir: Path, path: Path, uses_lean4: bool) -> Path:
- return _from_lean_path(root_dir, path, uses_lean4, ext=".trace.xml")
+def to_xml_path(root_dir: Path, path: Path, repo) -> Path:
+ return _from_lean_path(root_dir, path, repo, ext=".trace.xml")
-def to_dep_path(root_dir: Path, path: Path, uses_lean4: bool) -> Path:
- return _from_lean_path(root_dir, path, uses_lean4, ext=".dep_paths")
+def to_dep_path(root_dir: Path, path: Path, repo) -> Path:
+ return _from_lean_path(root_dir, path, repo, ext=".dep_paths")
-def to_json_path(root_dir: Path, path: Path, uses_lean4: bool) -> Path:
- return _from_lean_path(root_dir, path, uses_lean4, ext=".ast.json")
+def to_json_path(root_dir: Path, path: Path, repo) -> Path:
+ return _from_lean_path(root_dir, path, repo, ext=".ast.json")
-def to_lean_path(root_dir: Path, path: Path, uses_lean4: bool) -> bool:
+def to_lean_path(root_dir: Path, path: Path, repo) -> bool:
if path.is_absolute():
path = path.relative_to(root_dir)
@@ -331,33 +317,25 @@ def to_lean_path(root_dir: Path, path: Path, uses_lean4: bool) -> bool:
assert path.suffix == ".dep_paths"
path = path.with_suffix(".lean")
- if not uses_lean4:
+ if not repo.uses_lean4:
return path
- if root_dir.name == "lean4":
- return Path("src") / path.relative_to("lib")
- elif path.is_relative_to(LEAN4_DEPS_DIR / "lean4/lib"):
+ packages_dir = repo.get_packages_dir()
+ build_dir = repo.get_build_dir()
+
+ assert root_dir.name != "lean4"
+ if path.is_relative_to(packages_dir / "lean4/lib"):
# E.g., "lake-packages/lean4/lib/lean/Init.lean"
- p = path.relative_to(LEAN4_DEPS_DIR / "lean4/lib")
- return LEAN4_DEPS_DIR / "lean4/src" / p
- elif path.is_relative_to(LEAN4_DEPS_DIR):
+ p = path.relative_to(packages_dir / "lean4/lib")
+ return packages_dir / "lean4/src" / p
+ elif path.is_relative_to(packages_dir):
# E.g., "lake-packages/std/build/ir/Std.lean"
- p = path.relative_to(LEAN4_DEPS_DIR)
+ p = path.relative_to(packages_dir)
repo_name = p.parts[0]
- return LEAN4_DEPS_DIR / repo_name / p.relative_to(Path(repo_name) / "build/ir")
- else:
- # E.g., "build/ir/Mathlib/LinearAlgebra/Basics.lean"
- assert path.is_relative_to("build/ir"), path
- return path.relative_to("build/ir")
-
-
-def get_module(path: Path) -> str:
- assert path.suffix == ".lean"
- if path.is_relative_to(LEAN4_DEPS_DIR / "lean4/lib"):
- return ".".join(
- path.with_suffix("").relative_to(LEAN4_DEPS_DIR / "lean4/lib").parts[1:]
+ return (
+ packages_dir / repo_name / p.relative_to(Path(repo_name) / build_dir / "ir")
)
- elif path.is_relative_to(LEAN4_DEPS_DIR):
- return ".".join(path.with_suffix("").relative_to(LEAN4_DEPS_DIR).parts[1:])
else:
- return ".".join(path.with_suffix("").parts)
+ # E.g., ".lake/build/ir/Mathlib/LinearAlgebra/Basics.lean" or "build/ir/Mathlib/LinearAlgebra/Basics.lean"
+ assert path.is_relative_to(build_dir / "ir"), path
+ return path.relative_to(build_dir / "ir")
diff --git a/tests/conftest.py b/tests/conftest.py
index a0a3026..0e136f1 100644
--- a/tests/conftest.py
+++ b/tests/conftest.py
@@ -48,7 +48,7 @@ def lean4_example_repo():
@pytest.fixture(scope="session")
def std4_repo():
- commit = "ccbe74d4406be21b91c04d62b4c93dec9adfc546"
+ commit = get_latest_commit(STD4_URL)
return LeanGitRepo(STD4_URL, commit)
@@ -64,6 +64,12 @@ def mathlib4_repo():
return LeanGitRepo(MATHLIB4_URL, commit)
+@pytest.fixture(scope="session")
+def latest_mathlib4_repo():
+ commit = get_latest_commit(MATHLIB4_URL)
+ return LeanGitRepo(MATHLIB4_URL, commit)
+
+
@pytest.fixture(scope="session")
def aesop_repo():
commit = get_latest_commit(AESOP_URL)
@@ -76,20 +82,6 @@ def minif2f_repo():
return LeanGitRepo(MINIF2F_URL, commit)
-"""
-@pytest.fixture(scope="session")
-def local_traced_repo():
- commit = get_latest_commit(LEAN4_EXAMPLE_URL)
- repo = LeanGitRepo(LEAN4_EXAMPLE_URL, commit)
-
- with working_directory():
- repo.clone_and_checkout()
- with working_directory(repo.name):
- shutil.rmtree(".git")
- return trace_local(repo.name)
-"""
-
-
@pytest.fixture(scope="session", params=URLS)
def traced_repo(request):
url = request.param
diff --git a/tests/data_extraction/test_trace.py b/tests/data_extraction/test_trace.py
index bd8889e..bb941be 100644
--- a/tests/data_extraction/test_trace.py
+++ b/tests/data_extraction/test_trace.py
@@ -10,13 +10,3 @@ def test_trace(traced_repo):
def test_get_traced_repo_path(mathlib_repo):
path = get_traced_repo_path(mathlib_repo)
assert isinstance(path, Path) and path.exists()
-
-
-@pytest.mark.skip()
-def test_trace_local_repo(local_traced_repo):
- local_traced_repo.check_sanity()
-
-
-@pytest.mark.skip()
-def test_trace_local_file():
- pass
diff --git a/tests/interaction/test_tactics.py b/tests/interaction/test_tactics.py
index 0b7e85a..cedde14 100644
--- a/tests/interaction/test_tactics.py
+++ b/tests/interaction/test_tactics.py
@@ -158,7 +158,7 @@ def test_example_12(std4_repo: LeanGitRepo) -> None:
thm = Theorem(
std4_repo,
"Std/Data/List/Lemmas.lean",
- "List.isSuffix.length_le",
+ "List.IsSuffix.length_le",
)
with Dojo(thm) as (dojo, s0):
s1 = dojo.run_tac(s0, "exact h.sublist.length_le")