File size: 3,707 Bytes
a3c590d | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 | from __future__ import annotations
from ragsolver.rag.ingest_mathlib import _should_exclude, record_to_chunk
CFG = {
"doc_id": "mathlib-v4.28.0-rc1",
"docs_url_base": "https://leanprover-community.github.io/mathlib4_docs",
"exclude_kinds": ["instance"],
"exclude_module_prefixes": ["Mathlib.Tactic", "Mathlib.Deprecated"],
"exclude_name_substrings": [".proof_", ".match_", "_aux"],
"exclude_name_regex": r"\.eq_(\d+|def)$",
}
def _record(**overrides) -> dict:
base = {
"name": ["Nat.Coprime"],
"module_name": ["Mathlib", "Data", "Nat", "GCD", "Basic"],
"type": "ℕ → ℕ → Prop",
"kind": "def",
"signature": "ℕ → ℕ → Prop",
"value": "",
"informal_name": "Coprimality",
"informal_description": "Two naturals are coprime if their gcd is 1.",
}
base.update(overrides)
return base
def test_excludes_instances():
assert _should_exclude(_record(kind="instance"), CFG) is True
assert _should_exclude(_record(kind="def"), CFG) is False
def test_excludes_tactic_and_deprecated_modules():
assert _should_exclude(_record(module_name=["Mathlib", "Tactic", "Ring"]), CFG) is True
assert _should_exclude(_record(module_name=["Mathlib", "Deprecated", "Foo"]), CFG) is True
assert _should_exclude(_record(module_name=["Mathlib", "Data", "Nat"]), CFG) is False
def test_excludes_autogenerated_aux_names():
assert _should_exclude(_record(name=["Nat.Coprime.proof_1"]), CFG) is True
assert _should_exclude(_record(name=["Nat.Coprime.match_1"]), CFG) is True
assert _should_exclude(_record(name=["Nat.Coprime_aux"]), CFG) is True
assert _should_exclude(_record(name=["Nat.Coprime.eq_1"]), CFG) is True
assert _should_exclude(_record(name=["Nat.Coprime"]), CFG) is False
def test_record_to_chunk_builds_expected_fields():
chunk = record_to_chunk(_record(), CFG, mathlib_tag="v4.28.0-rc1", lean_version="leanprover/lean4:v4.28.0-rc1")
assert chunk is not None
assert chunk.chunk_id == "mathlib:Nat.Coprime:0"
assert chunk.decl_name == "Nat.Coprime"
assert chunk.module_path == "Mathlib.Data.Nat.GCD.Basic"
assert chunk.corpus == "mathlib"
assert chunk.unit_type == "mathlib_decl"
assert "Coprimality" in chunk.text
assert "Two naturals are coprime" in chunk.text
assert chunk.docs_url == (
"https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/GCD/Basic.html#Nat.Coprime"
)
assert chunk.embedding is None
def test_record_to_chunk_returns_none_without_name():
assert record_to_chunk(_record(name=[]), CFG, "v4.28.0-rc1", "x") is None
def test_name_components_are_joined_into_the_full_declaration_name():
"""Regresión (docs/DECISIONS.md #31): en el JSONL de LeanSearch v2 `name` es la
lista de componentes del nombre, no una lista de alias. Con `name[0]` el 90% de
las declaraciones quedaba con nombre/chunk_id/docs_url incorrectos y repetidos."""
chunk = record_to_chunk(_record(name=["GCDMonoid", "dvd_gcd"]), CFG, mathlib_tag="v4.28.0-rc1", lean_version="x")
assert chunk.decl_name == "GCDMonoid.dvd_gcd"
assert chunk.chunk_id == "mathlib:GCDMonoid.dvd_gcd:0"
assert chunk.docs_url.endswith("#GCDMonoid.dvd_gcd")
assert chunk.decl_names_alt == []
assert _should_exclude(_record(name=["Nat", "Coprime", "proof_1"]), CFG) is True
def test_equation_lemmas_are_excluded_but_real_eq_lemmas_are_kept():
for name, excluded in ((["Nat", "gcd", "eq_1"], True), (["Nat", "gcd", "eq_def"], True), (["Nat", "Prime", "eq_one_or_self_of_dvd"], False), (["eq_comm"], False)):
assert _should_exclude(_record(name=name), CFG) is excluded, name
|