From 815cb59d3a8c15e1c669665ebabaf265333eff5a Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Tue, 9 Jun 2026 16:30:12 -0300 Subject: [PATCH 1/3] test: add leanclient LSP round-trip test for guard diagnostics This PR adds a test that verifies the axiom guard's diagnostics actually reach a language-server client, not just a batch build. It points leanclient at the existing test/consumer project (which loads the guard via plugins := with no import) and asserts the non-standard-axiom warning is published for the declaration depending on the custom axiom. The test is added to test/run.sh and CI gains a uv setup step to run it. The test ensures the consumer is built once first, because the language server elaborates source on its own but cannot load a plugin whose shared library has not yet been compiled. --- .github/workflows/ci.yml | 5 ++- test/lsp_diagnostics_test.py | 86 ++++++++++++++++++++++++++++++++++++ test/run.sh | 14 ++++++ 3 files changed, 104 insertions(+), 1 deletion(-) create mode 100755 test/lsp_diagnostics_test.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6096ce6..d5daba6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -90,8 +90,11 @@ jobs: - name: Pin toolchain run: echo "${{ matrix.toolchain }}" > lean-toolchain + - name: Install uv (for the leanclient LSP round-trip test) + uses: astral-sh/setup-uv@v5 + - name: Build linter library run: lake build LeanExtensions - - name: Behavioral test suite (both registration paths + --wfail gate) + - name: Behavioral test suite (registration paths, --wfail gate, LSP round-trip) run: bash test/run.sh diff --git a/test/lsp_diagnostics_test.py b/test/lsp_diagnostics_test.py new file mode 100755 index 0000000..6cfe80f --- /dev/null +++ b/test/lsp_diagnostics_test.py @@ -0,0 +1,86 @@ +#!/usr/bin/env -S uv run --script +# /// script +# requires-python = ">=3.11" +# dependencies = ["leanclient>=0.10,<0.11"] +# /// +"""LSP round-trip test for the axiom guard. + +Verifies that the extension's diagnostics actually reach a language-server client: it points +`leanclient` at the existing `test/consumer` project (which loads the guard via `plugins :=` with +no import) and asserts the guard's "non-standard axiom" warning is published for the declaration +that depends on the custom `evil` axiom — exactly what downstream tooling (e.g. lean4-toolkit's +lsp_utils) parses instead of `#print axioms` injection. + +Reuses the consumer fixtures already tested by run.sh — no new project. The LSP server elaborates +*source* itself, but it cannot load a *plugin* whose shared library has not been built yet (the +dynlib is a build artifact); without it the file fatals before any diagnostic is published. So this +test ensures the consumer is built once (which fetches the dep and compiles the guard's dynlib) +before opening the client. + +Run: test/lsp_diagnostics_test.py (PEP-723 inline deps; `uv run --script` provides leanclient) +Exit: 0 on success, 1 on assertion failure. +""" + +import subprocess +import sys +from pathlib import Path + +from leanclient import LeanLSPClient + +HERE = Path(__file__).resolve().parent +CONSUMER = HERE / "consumer" + +# Distinctive substrings emitted by LeanExtensions/AxiomGuard.lean. +GUARD_MARKER = "non-standard axiom" +# The consumer's fixtures (test/consumer/Consumer/Defs.lean + Consumer.lean): `evil`/`benign` are +# declared axioms; `uses_evil` depends on `evil`. +EXPECT_AXIOM = "evil" + + +def diagnostics_for(client: LeanLSPClient, rel: str): + # Drain initial elaboration, then read the settled diagnostic set. + client.get_diagnostics(rel, inactivity_timeout=10) + return client.get_diagnostics(rel, inactivity_timeout=15).diagnostics + + +def main() -> int: + if not (CONSUMER / "lakefile.lean").exists(): + print(f"FAIL: consumer project missing at {CONSUMER}") + return 1 + + # Plugin loading needs the guard's shared library compiled; build once if absent. This also + # fetches the lean_extensions dependency. (The LSP elaborates source on its own, but cannot + # load a not-yet-built plugin.) + print("Building consumer (fetches dep + compiles the guard plugin)...") + subprocess.run(["lake", "build"], cwd=CONSUMER, check=True) + + client = LeanLSPClient(str(CONSUMER), max_opened_files=4) + failures = [] + + # Consumer.lean depends on `evil` (no import of the guard — loaded via plugins:=). + consumer_diags = diagnostics_for(client, "Consumer.lean") + consumer_msgs = [d.get("message", "") for d in consumer_diags] + guard_hits = [m for m in consumer_msgs if GUARD_MARKER in m] + + if not guard_hits: + failures.append( + f"expected a '{GUARD_MARKER}' diagnostic in Consumer.lean (guard loaded via plugins:=); " + f"got messages: {consumer_msgs}" + ) + elif not any(EXPECT_AXIOM in m for m in guard_hits): + failures.append( + f"guard fired but did not name '{EXPECT_AXIOM}'; guard diagnostics: {guard_hits}" + ) + + if failures: + print("FAIL: LSP round-trip assertions failed:") + for f in failures: + print(" -", f) + return 1 + + print(f"PASS: guard '{GUARD_MARKER}' diagnostic published via LSP for Consumer.lean: {guard_hits}") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/test/run.sh b/test/run.sh index ec04f88..aa96dc4 100755 --- a/test/run.sh +++ b/test/run.sh @@ -74,6 +74,20 @@ else ok "consumer under --wfail fails the build" fi +note "" +note "== LSP round-trip (guard diagnostics reach a language-server client) ==" +# Requires `uv` (for leanclient). Skip with a notice if uv is unavailable rather than failing the +# whole suite on a missing optional tool. +if command -v uv >/dev/null 2>&1; then + if test/lsp_diagnostics_test.py; then + ok "LSP round-trip: guard diagnostic published to leanclient" + else + bad "LSP round-trip test failed" + fi +else + note "SKIP LSP round-trip (uv not installed)" +fi + note "" note "== $pass passed, $fail failed ==" [ "$fail" -eq 0 ] From c051ac68367cff2cd94186fb78add2582af3feb6 Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Tue, 9 Jun 2026 16:39:40 -0300 Subject: [PATCH 2/3] ci: bump setup-uv to v8 (Node 24) --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d5daba6..48e3c12 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -91,7 +91,7 @@ jobs: run: echo "${{ matrix.toolchain }}" > lean-toolchain - name: Install uv (for the leanclient LSP round-trip test) - uses: astral-sh/setup-uv@v5 + uses: astral-sh/setup-uv@v8 - name: Build linter library run: lake build LeanExtensions From 3d56c829a3a44a2890336b0e716d59144a14a97c Mon Sep 17 00:00:00 2001 From: Mario Rugiero Date: Tue, 9 Jun 2026 16:49:25 -0300 Subject: [PATCH 3/3] ci: pin setup-uv to v8.2.0 (no v8 major alias exists) --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 48e3c12..5bf2577 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -91,7 +91,7 @@ jobs: run: echo "${{ matrix.toolchain }}" > lean-toolchain - name: Install uv (for the leanclient LSP round-trip test) - uses: astral-sh/setup-uv@v8 + uses: astral-sh/setup-uv@v8.2.0 - name: Build linter library run: lake build LeanExtensions