#!/usr/bin/env python3 """Unit tests for lean_qc_flagger.py — QC inspection helpers.""" import importlib.util import json import os import sys import tempfile import unittest from pathlib import Path MODULE_PATH = Path(__file__).with_name("lean_qc_flagger.py") SPEC = importlib.util.spec_from_file_location("lean_qc_flagger", MODULE_PATH) assert SPEC is not None and SPEC.loader is not None flagger = importlib.util.module_from_spec(SPEC) sys.modules[SPEC.name] = flagger SPEC.loader.exec_module(flagger) # --------------------------------------------------------------------------- # Helper utilities # --------------------------------------------------------------------------- class TestGetLine(unittest.TestCase): def test_first_line(self): self.assertEqual(flagger._get_line("abc\ndef\n", 0), 1) def test_second_line(self): self.assertEqual(flagger._get_line("abc\ndef\n", 4), 2) def test_end_of_content(self): self.assertEqual(flagger._get_line("abc\ndef\nghi", 10), 3) class TestDefNames(unittest.TestCase): def test_extracts_defs(self): src = "def foo := 1\ndef bar := 2" self.assertEqual(flagger._def_names(src), {"foo", "bar"}) def test_no_defs(self): self.assertEqual(flagger._def_names("theorem t : True := trivial"), set()) class TestTheoremNames(unittest.TestCase): def test_extracts_theorems(self): src = "theorem thmA : True := trivial\ntheorem thmB : Nat = Nat := rfl" self.assertEqual(flagger._theorem_names(src), {"thmA", "thmB"}) class TestPrivateDefNames(unittest.TestCase): def test_extracts_private(self): src = "private def helper := 42\ndef public := 1" self.assertEqual(flagger._private_def_names(src), {"helper"}) class TestGetImportsOpens(unittest.TestCase): def test_get_imports(self): src = "import Mathlib.Data.Nat\nimport Semantics.RRC\ndef foo := 1" self.assertEqual(flagger._get_imports(src), ["Mathlib.Data.Nat", "Semantics.RRC"]) def test_get_opens(self): src = "open Nat\nopen List\ntheorem t := by decide" self.assertEqual(flagger._get_opens(src), ["Nat", "List"]) class TestNormalizePathSep(unittest.TestCase): def test_backslash(self): self.assertEqual(flagger._normalize_path_sep("a\\b\\c"), "a/b/c") def test_forward_slash_unchanged(self): self.assertEqual(flagger._normalize_path_sep("a/b/c"), "a/b/c") # --------------------------------------------------------------------------- # Code-line detection (block comment filtering) # --------------------------------------------------------------------------- class TestGetCodeLines(unittest.TestCase): def test_plain_code(self): src = "def foo := 1\ntheorem t := by decide" result = flagger._get_code_lines(src) self.assertTrue(all(v is True for v in result)) def test_line_comments(self): src = "-- comment\ndef foo := 1" result = flagger._get_code_lines(src) self.assertFalse(result[0]) self.assertTrue(result[1]) def test_block_comment(self): src = "/- block\n comment -/\ndef foo := 1" result = flagger._get_code_lines(src) self.assertFalse(result[0]) self.assertFalse(result[1]) self.assertTrue(result[2]) def test_empty_lines(self): src = "\n\ndef foo := 1" result = flagger._get_code_lines(src) self.assertFalse(result[0]) self.assertFalse(result[1]) self.assertTrue(result[2]) def test_single_line_block_comment(self): src = "/- inline -/\ndef foo := 1" result = flagger._get_code_lines(src) self.assertFalse(result[0]) self.assertTrue(result[1]) class TestPosIsCode(unittest.TestCase): def test_code_position(self): src = "def foo := 1" self.assertTrue(flagger._pos_is_code(src, 0)) def test_comment_position(self): src = "-- comment\ndef foo := 1" self.assertFalse(flagger._pos_is_code(src, 3)) class TestIsDataDef(unittest.TestCase): def test_struct_def(self): src = "def myConfig : Config := {\n field1 := 1\n}" self.assertTrue(flagger._is_data_def(src, "myConfig")) def test_numeric_def(self): src = "def maxSize : Nat := 42" self.assertTrue(flagger._is_data_def(src, "maxSize")) def test_function_def(self): src = "def addOne (n : Nat) : Nat := n + 1" self.assertFalse(flagger._is_data_def(src, "addOne")) # --------------------------------------------------------------------------- # QCIssue / FileResult # --------------------------------------------------------------------------- class TestQCIssue(unittest.TestCase): def test_to_dict(self): issue = flagger.QCIssue("structural_health", "test msg", 10, "ERROR") d = issue.to_dict() self.assertEqual(d["check"], "structural_health") self.assertEqual(d["message"], "test msg") self.assertEqual(d["line"], 10) self.assertEqual(d["severity"], "ERROR") class TestFileResult(unittest.TestCase): def test_empty_result_passes(self): r = flagger.FileResult("test.lean") self.assertTrue(r.passed) self.assertEqual(r.issues, []) def test_warning_keeps_pass(self): r = flagger.FileResult("test.lean") r.add_issue(flagger.QCIssue("check", "msg", 1, "WARNING")) self.assertTrue(r.passed) def test_error_fails(self): r = flagger.FileResult("test.lean") r.add_issue(flagger.QCIssue("check", "msg", 1, "ERROR")) self.assertFalse(r.passed) def test_to_dict_shape(self): r = flagger.FileResult("Test.lean") r.structural = {"theorems": 2} r.add_issue(flagger.QCIssue("check", "msg", 5, "WARNING")) d = r.to_dict() self.assertEqual(d["path"], "Test.lean") self.assertTrue(d["passed"]) self.assertEqual(d["issue_count"], 1) self.assertEqual(d["structural"]["theorems"], 2) # --------------------------------------------------------------------------- # Check functions # --------------------------------------------------------------------------- class TestCheckStructuralHealth(unittest.TestCase): def test_counts_theorems_and_defs(self): src = "theorem t1 : True := trivial\ndef f := 1\ndef g := 2" r = flagger.FileResult("Test.lean") flagger.check_structural_health(src, r) self.assertEqual(r.structural["theorems"], 1) self.assertEqual(r.structural["defs"], 2) def test_sorry_flagged_as_error(self): src = "theorem t : True := by sorry" r = flagger.FileResult("Test.lean") flagger.check_structural_health(src, r) self.assertFalse(r.passed) self.assertTrue(any(i.check == "structural_health" and "sorry" in i.message for i in r.issues)) def test_sorry_in_comment_not_flagged(self): src = "-- sorry is in comment\ntheorem t : True := trivial" r = flagger.FileResult("Test.lean") flagger.check_structural_health(src, r) self.assertEqual(r.structural["sorries"], 0) def test_empty_theorem_detected(self): src = "theorem t : True := by\ntheorem t2 : False := by decide" r = flagger.FileResult("Test.lean") flagger.check_structural_health(src, r) self.assertEqual(r.structural["empty_theorems"], 1) def test_eval_and_eval_bang_counted(self): src = "#eval 1 + 1\n#eval! IO.println" r = flagger.FileResult("Test.lean") flagger.check_structural_health(src, r) self.assertEqual(r.structural["eval"], 1) self.assertEqual(r.structural["eval_bang"], 1) def test_native_decide_counted(self): src = "theorem t := by native_decide" r = flagger.FileResult("Test.lean") flagger.check_structural_health(src, r) self.assertEqual(r.structural["native_decide"], 1) class TestCheckNamingConventions(unittest.TestCase): def test_pascal_case_file_passes(self): src = "def foo := 1" r = flagger.FileResult("MyModule.lean") flagger.check_naming_conventions(src, r, "MyModule.lean") naming_issues = [i for i in r.issues if "File name" in i.message] self.assertEqual(naming_issues, []) def test_snake_case_file_flagged(self): src = "def foo := 1" r = flagger.FileResult("my_module.lean") flagger.check_naming_conventions(src, r, "my_module.lean") self.assertTrue(any("snake_case" in i.message for i in r.issues)) def test_non_pascal_type_flagged(self): src = "inductive myType where | a | b" r = flagger.FileResult("Test.lean") flagger.check_naming_conventions(src, r, "Test.lean") self.assertTrue(any("myType" in i.message and "PascalCase" in i.message for i in r.issues)) def test_non_camel_def_flagged(self): src = "def MyFunc := 1" r = flagger.FileResult("Test.lean") flagger.check_naming_conventions(src, r, "Test.lean") self.assertTrue(any("MyFunc" in i.message for i in r.issues)) def test_banned_prefix_flagged(self): src = "def getItems := []" r = flagger.FileResult("Test.lean") flagger.check_naming_conventions(src, r, "Test.lean") self.assertTrue(any("Banned prefix" in i.message for i in r.issues)) def test_banned_suffix_flagged(self): src = "def helper_v2 := 1" r = flagger.FileResult("Test.lean") flagger.check_naming_conventions(src, r, "Test.lean") self.assertTrue(any("Banned suffix" in i.message for i in r.issues)) class TestCheckQ16Compliance(unittest.TestCase): def test_float_in_code_flagged(self): src = "def x : Float := 1.0" r = flagger.FileResult("Test.lean") flagger.check_q16_compliance(src, r) self.assertTrue(any("Float" in i.message for i in r.issues)) def test_float_in_comment_not_flagged(self): src = "-- Float is fine in comments\ndef x : Nat := 1" r = flagger.FileResult("Test.lean") flagger.check_q16_compliance(src, r) q16_issues = [i for i in r.issues if i.check == "q16_compliance"] self.assertEqual(q16_issues, []) class TestCheckProofQuality(unittest.TestCase): def test_def_without_companion_flagged(self): src = "def orphanFunc (n : Nat) : Nat := n + 1" r = flagger.FileResult("Test.lean") flagger.check_proof_quality(src, r) self.assertTrue(any("orphanFunc" in i.message and "companion" in i.message for i in r.issues)) def test_def_with_companion_theorem_ok(self): src = "def addOne (n : Nat) : Nat := n + 1\ntheorem addOneSpec : addOne 0 = 1 := rfl" r = flagger.FileResult("Test.lean") flagger.check_proof_quality(src, r) orphan = [i for i in r.issues if "addOne" in i.message and "companion" in i.message] self.assertEqual(orphan, []) def test_private_def_not_flagged(self): src = "private def helper := 42" r = flagger.FileResult("Test.lean") flagger.check_proof_quality(src, r) orphan = [i for i in r.issues if "helper" in i.message and "companion" in i.message] self.assertEqual(orphan, []) def test_data_def_not_flagged(self): src = "def maxSize : Nat := 42" r = flagger.FileResult("Test.lean") flagger.check_proof_quality(src, r) orphan = [i for i in r.issues if "maxSize" in i.message and "companion" in i.message] self.assertEqual(orphan, []) class TestCheckDependencyAnalysis(unittest.TestCase): def test_unused_import_flagged(self): src = "import Semantics.Unused\ndef foo := 1" r = flagger.FileResult("Test.lean") flagger.check_dependency_analysis(src, r, "Test.lean") self.assertTrue(any("Unused import" in i.message for i in r.issues)) def test_used_import_not_flagged(self): src = "import Semantics.RRC\ndef foo := RRC.classify x" r = flagger.FileResult("Test.lean") flagger.check_dependency_analysis(src, r, "Test.lean") unused = [i for i in r.issues if "Unused import" in i.message] self.assertEqual(unused, []) def test_opened_import_not_flagged(self): src = "import Semantics.Types\nopen Types\ndef foo := mkValue 1" r = flagger.FileResult("Test.lean") flagger.check_dependency_analysis(src, r, "Test.lean") unused = [i for i in r.issues if "Unused import" in i.message] self.assertEqual(unused, []) # --------------------------------------------------------------------------- # scan_file integration # --------------------------------------------------------------------------- class TestScanFile(unittest.TestCase): def test_scan_clean_file(self): with tempfile.NamedTemporaryFile(suffix=".lean", mode="w", delete=False) as f: f.write("def addOne (n : Nat) : Nat := n + 1\n#eval addOne 0\n") f.flush() try: result = flagger.scan_file(f.name) self.assertTrue(result.passed) finally: os.unlink(f.name) def test_scan_file_with_sorry(self): with tempfile.NamedTemporaryFile(suffix=".lean", mode="w", delete=False) as f: f.write("theorem bogus : True := by sorry\n") f.flush() try: result = flagger.scan_file(f.name) self.assertFalse(result.passed) finally: os.unlink(f.name) def test_scan_nonexistent_file(self): result = flagger.scan_file("/tmp/nonexistent_file_12345.lean") self.assertFalse(result.passed) # --------------------------------------------------------------------------- # find_lean_files / gather_imports # --------------------------------------------------------------------------- class TestFindLeanFiles(unittest.TestCase): def test_single_file(self): with tempfile.NamedTemporaryFile(suffix=".lean", delete=False) as f: try: files = flagger.find_lean_files(f.name) self.assertEqual(len(files), 1) finally: os.unlink(f.name) def test_directory(self): with tempfile.TemporaryDirectory() as td: (Path(td) / "A.lean").write_text("def a := 1") (Path(td) / "B.lean").write_text("def b := 2") (Path(td) / "not_lean.py").write_text("pass") files = flagger.find_lean_files(td) self.assertEqual(len(files), 2) def test_nonexistent_path(self): files = flagger.find_lean_files("/tmp/nonexistent_dir_12345") self.assertEqual(files, []) class TestGatherImports(unittest.TestCase): def test_gathers_imports_from_files(self): with tempfile.TemporaryDirectory() as td: a = Path(td) / "A.lean" a.write_text("import Semantics.RRC\ndef foo := 1") b = Path(td) / "B.lean" b.write_text("import Semantics.Types\nimport Semantics.AVM\ndef bar := 2") imports = flagger.gather_imports([str(a), str(b)]) self.assertEqual(imports[str(a)], ["Semantics.RRC"]) self.assertEqual(imports[str(b)], ["Semantics.Types", "Semantics.AVM"]) # --------------------------------------------------------------------------- # Markdown report generation # --------------------------------------------------------------------------- class TestGenerateMarkdownReport(unittest.TestCase): def test_report_structure(self): r = flagger.FileResult("Test.lean") r.structural = {"theorems": 1, "defs": 0} r.add_issue(flagger.QCIssue("check", "test issue", 5, "WARNING")) md = flagger.generate_markdown_report([r], "/path") self.assertIn("QC Flag Report", md) self.assertIn("Test.lean", md) self.assertIn("PASS", md) self.assertIn("test issue", md) if __name__ == "__main__": unittest.main()