| # python/tests/services/test_lean_compiler.py | |
| from src.server.services.lean.compiler_service import LeanCompilerService | |
| def test_parse_lake_errors_single(): | |
| compiler = LeanCompilerService() | |
| sample_output = ( | |
| "lean_proofs/LeanProofs/Basic.lean:4:2: error: type mismatch\n" | |
| " rfl\n" | |
| "has type\n" | |
| " n + m = n + m\n" | |
| "but is expected to have type\n" | |
| " n + m = m + n\n" | |
| ) | |
| errors = compiler.parse_lake_errors(sample_output) | |
| assert len(errors) == 1 | |
| assert errors[0]["file"] == "lean_proofs/LeanProofs/Basic.lean" | |
| assert errors[0]["line"] == 4 | |
| assert errors[0]["column"] == 2 | |
| assert "type mismatch" in errors[0]["message"] | |
| assert "but is expected to have type" in errors[0]["message"] | |
| def test_parse_lake_errors_multiple(): | |
| compiler = LeanCompilerService() | |
| sample_output = ( | |
| "lean_proofs/LeanProofs/Basic.lean:4:2: error: error 1\n" | |
| "some detail lines here\n" | |
| "\n" | |
| "lean_proofs/LeanProofs/Advanced.lean:10:5: error: error 2\n" | |
| "more details\n" | |
| ) | |
| errors = compiler.parse_lake_errors(sample_output) | |
| assert len(errors) == 2 | |
| assert errors[0]["file"] == "lean_proofs/LeanProofs/Basic.lean" | |
| assert errors[0]["line"] == 4 | |
| assert "error 1" in errors[0]["message"] | |
| assert errors[1]["file"] == "lean_proofs/LeanProofs/Advanced.lean" | |
| assert errors[1]["line"] == 10 | |
| assert "error 2" in errors[1]["message"] | |