| 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 |
|
|
