From 92b59ae4f69319f35b9cc9bf39fa89fc91edd820 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 13 May 2025 15:00:47 +0200 Subject: [PATCH] test: goals accomplished (#8319) This PR adds a test for the goals accomplished diagnostics so that we notice when they break. Follow-up for #8242. --- src/Lean/Server/Test/Runner.lean | 3 + .../cancellation.lean.expected.out | 147 ++++++++++++++++-- tests/lean/interactive/goalsAccomplished.lean | 9 ++ .../goalsAccomplished.lean.expected.out | 31 ++++ 4 files changed, 177 insertions(+), 13 deletions(-) create mode 100644 tests/lean/interactive/goalsAccomplished.lean create mode 100644 tests/lean/interactive/goalsAccomplished.lean.expected.out diff --git a/src/Lean/Server/Test/Runner.lean b/src/Lean/Server/Test/Runner.lean index 8a7c4a8de2..018847581e 100644 --- a/src/Lean/Server/Test/Runner.lean +++ b/src/Lean/Server/Test/Runner.lean @@ -95,6 +95,9 @@ partial def main (args : List String) : IO Unit := do } } } + lean? := some { + silentDiagnosticSupport? := some true + } } Ipc.writeRequest ⟨0, "initialize", { capabilities : InitializeParams }⟩ let _ ← Ipc.readResponseAs 0 InitializeResult diff --git a/tests/lean/interactive/cancellation.lean.expected.out b/tests/lean/interactive/cancellation.lean.expected.out index aa386a04b9..a7a30cd692 100644 --- a/tests/lean/interactive/cancellation.lean.expected.out +++ b/tests/lean/interactive/cancellation.lean.expected.out @@ -1,7 +1,29 @@ blocked! cancelled! rerun! -{"version": 2, "uri": "file:///cancellation.lean", "diagnostics": []} +{"version": 2, + "uri": "file:///cancellation.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 11, "character": 0}, "end": {"line": 12, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 11, "character": 0}, + "end": {"line": 12, "character": 15}}}, + {"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 18, "character": 0}, "end": {"line": 19, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 18, "character": 0}, + "end": {"line": 21, "character": 9}}}]} blocked! unblocking! {"version": 2, @@ -20,8 +42,17 @@ unblocking! {"start": {"line": 7, "character": 2}, "end": {"line": 7, "character": 18}}, "message": "blocked", "fullRange": - {"start": {"line": 7, "character": 2}, - "end": {"line": 7, "character": 18}}}]} + {"start": {"line": 7, "character": 2}, "end": {"line": 7, "character": 18}}}, + {"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 10, "character": 0}, "end": {"line": 11, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 10, "character": 0}, + "end": {"line": 11, "character": 18}}}]} unblocking! {"version": 2, "uri": "file:///cancellation.lean", @@ -32,8 +63,17 @@ unblocking! {"start": {"line": 7, "character": 2}, "end": {"line": 7, "character": 24}}, "message": "blocked", "fullRange": - {"start": {"line": 7, "character": 2}, - "end": {"line": 7, "character": 24}}}]} + {"start": {"line": 7, "character": 2}, "end": {"line": 7, "character": 24}}}, + {"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 10, "character": 0}, "end": {"line": 11, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 10, "character": 0}, + "end": {"line": 11, "character": 18}}}]} unblocking! {"version": 2, "uri": "file:///cancellation.lean", @@ -64,14 +104,47 @@ unblocking! {"start": {"line": 7, "character": 2}, "end": {"line": 7, "character": 18}}, "message": "blocked", "fullRange": - {"start": {"line": 7, "character": 2}, - "end": {"line": 7, "character": 18}}}]} + {"start": {"line": 7, "character": 2}, "end": {"line": 7, "character": 18}}}, + {"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 9, "character": 0}, "end": {"line": 9, "character": 37}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 9, "character": 0}, + "end": {"line": 9, "character": 37}}}]} blocked! cancelled! -{"version": 2, "uri": "file:///cancellation.lean", "diagnostics": []} +{"version": 2, + "uri": "file:///cancellation.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 6, "character": 0}, "end": {"line": 7, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 6, "character": 0}, + "end": {"line": 13, "character": 9}}}]} blocked! cancelled! -{"version": 2, "uri": "file:///cancellation.lean", "diagnostics": []} +{"version": 2, + "uri": "file:///cancellation.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 6, "character": 0}, "end": {"line": 7, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 6, "character": 0}, + "end": {"line": 13, "character": 9}}}]} unblocking! {"version": 2, "uri": "file:///cancellation.lean", @@ -86,13 +159,61 @@ unblocking! "end": {"line": 6, "character": 39}}}]} blocked! cancelled! -{"version": 2, "uri": "file:///cancellation.lean", "diagnostics": []} +{"version": 2, + "uri": "file:///cancellation.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 6, "character": 0}, "end": {"line": 7, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 6, "character": 0}, + "end": {"line": 11, "character": 9}}}]} blocked! cancelled! -{"version": 2, "uri": "file:///cancellation.lean", "diagnostics": []} +{"version": 2, + "uri": "file:///cancellation.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 6, "character": 0}, "end": {"line": 7, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 6, "character": 0}, + "end": {"line": 11, "character": 9}}}]} blocked! cancelled! -{"version": 2, "uri": "file:///cancellation.lean", "diagnostics": []} +{"version": 2, + "uri": "file:///cancellation.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 6, "character": 0}, "end": {"line": 7, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 6, "character": 0}, + "end": {"line": 13, "character": 10}}}]} blocked! cancelled! -{"version": 2, "uri": "file:///cancellation.lean", "diagnostics": []} +{"version": 2, + "uri": "file:///cancellation.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 6, "character": 0}, "end": {"line": 7, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 6, "character": 0}, + "end": {"line": 13, "character": 10}}}]} diff --git a/tests/lean/interactive/goalsAccomplished.lean b/tests/lean/interactive/goalsAccomplished.lean new file mode 100644 index 0000000000..c686821495 --- /dev/null +++ b/tests/lean/interactive/goalsAccomplished.lean @@ -0,0 +1,9 @@ +theorem foo : True := by + exact True.intro +--^ collectDiagnostics + +theorem foobar : True := True.intro +--^ collectDiagnostics + +example : True := True.intro +--^ collectDiagnostics diff --git a/tests/lean/interactive/goalsAccomplished.lean.expected.out b/tests/lean/interactive/goalsAccomplished.lean.expected.out new file mode 100644 index 0000000000..e402f1a24f --- /dev/null +++ b/tests/lean/interactive/goalsAccomplished.lean.expected.out @@ -0,0 +1,31 @@ +{"version": 1, + "uri": "file:///goalsAccomplished.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 0, "character": 0}, "end": {"line": 1, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 0, "character": 0}, "end": {"line": 1, "character": 18}}}, + {"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 4, "character": 0}, "end": {"line": 4, "character": 35}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 4, "character": 0}, "end": {"line": 4, "character": 35}}}, + {"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 7, "character": 0}, "end": {"line": 7, "character": 28}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, + "fullRange": + {"start": {"line": 7, "character": 0}, + "end": {"line": 7, "character": 28}}}]}