From 694e54d4d520cce1fd5118fced7abb496d7b14da Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Fri, 23 Feb 2024 14:40:06 -0600 Subject: [PATCH] minor fix --- docs/source/developer-guide.rst | 30 +----------------------------- tests/interaction/test_imports.py | 2 +- 2 files changed, 2 insertions(+), 30 deletions(-) diff --git a/docs/source/developer-guide.rst b/docs/source/developer-guide.rst index 06b862c5..dd5e11a0 100644 --- a/docs/source/developer-guide.rst +++ b/docs/source/developer-guide.rst @@ -14,34 +14,6 @@ please first reach out to us before implementing. All contributions should conform to our code formatting standards (see :ref:`code-formatting`). -Implementation Notes -******************** - -.. _modified-lean: - -Modified Lean 3 ---------------- - -Lean 3's AST export mechanism (:code:`lean --ast --tsast --tspp`) provides rich -syntactic information about :file:`*.lean` files, as well as certain semantic information -such as tactic states. However, it does not provide everything we need for retrieval-augmented -theorem proving. For each constant (premise) in a tactic, we'd like to know: - -* Its start/end positions within the tactic. -* Its fully qualified name. -* Where to find its definition (:file:`*.lean` file and the position within the file). - -The first one is syntactic and is already provided by :code:`lean --ast --tsast --tspp`. The remaining -two are produced by Lean's elaborator but not exported. Therefore, we modify Lean to export them. -Our modification is implemented as a `patch `_ -, which can be applied to Lean from `v3.42.1 `_ up to the most recent version by :code:`git apply` (see :ref:`lean_dojo.data_extraction.trace`). -Note that: - -* The modification only changes Lean's frontend but not its core functions for proof checking. Therefore, we do not compromise Lean's soundness. -* The modification is only for data extraction. For interaction, we still use the original, unmodified Lean. - - - Testing ******* @@ -49,7 +21,7 @@ We use `pytest `_ for testing. You can run tests by: .. code-block:: bash - VERBOSE=1 CACHE_DIR=~/.cache/lean_dojo_testing DISABLE_REMOTE_CACHE=1 CONTAINER=docker pytest -s tests + VERBOSE=1 CACHE_DIR=~/.cache/lean_dojo_testing DISABLE_REMOTE_CACHE=1 pytest -s tests rm -rf ~/.cache/lean_dojo_testing The environment variable :code:`CACHE_DIR` makes sure the testing uses a temporary cache directory that diff --git a/tests/interaction/test_imports.py b/tests/interaction/test_imports.py index 94d2e602..be58cced 100644 --- a/tests/interaction/test_imports.py +++ b/tests/interaction/test_imports.py @@ -17,7 +17,7 @@ def test_additional_imports_failure_1(lean4_example_repo) -> None: with pytest.raises(DojoInitError): with Dojo(thm, additional_imports=["Aesop"]): pass -wwa + def test_additional_imports(mathlib4_repo) -> None: """This test doesn't have the problem above because aesop is used by other files in mathlib4."""