max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/server_interactive
History
Exact
Joachim Breitner 6279ae98c7
test: resurrect try cancellation tests (#13707) 
This PR resurrects the tests about cancellation of `try?` tactics.

They were flaky before. By introducing an option
(`debug.tactic.try.onlyUserSuggestions`) to make these tests not run
`exact?` as part of `try?`, and thus be generally faster and use less
memory, the flakiness seems to have disappeared, at least in
non-`master` testing. We’ll see.

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2026-05-13 13:54:48 +00:00
..
533.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
533.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
863.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
863.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
1018unknowMVarIssue.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
1018unknowMVarIssue.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
1031.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
1265.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
1265.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
1403.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
1403.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
1525.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
1659.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
1659.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
2058.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
2058.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
2881.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
2881.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
4078.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
4078.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
4880.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
4880.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
5659.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
5659.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
6594.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
6594.lean.out.expected fix: filter assigned metavariables before computing apply subgoal tags (#13476) 2026-04-19 14:31:49 +00:00
10898.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
10898.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
amb.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
amb.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
anonHyp.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
anonHyp.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
autoBoundIssue.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
autoBoundIssue.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
builtinCodeactions.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
builtinCodeactions.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
cancellation.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
cancellation.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
cancellation_empty_by.lean test: resurrect try cancellation tests (#13707) 2026-05-13 13:54:48 +00:00
cancellation_empty_by.lean.out.expected test: resurrect try cancellation tests (#13707) 2026-05-13 13:54:48 +00:00
cancellation_par.lean test: resurrect try cancellation tests (#13707) 2026-05-13 13:54:48 +00:00
cancellation_par.lean.out.expected test: resurrect try cancellation tests (#13707) 2026-05-13 13:54:48 +00:00
cancellation_try_plain.lean feat: empty by runs try? to suggest a proof (#13430) 2026-05-11 06:31:42 +00:00
cancellation_try_plain.lean.out.expected feat: empty by runs try? to suggest a proof (#13430) 2026-05-11 06:31:42 +00:00
catHover.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
catHover.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
codeaction.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
codeaction.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
codeActions.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
codeActions.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
compHeader.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
compHeader.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion2.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion2.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion3.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion3.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion4.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion4.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion5.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion5.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion6.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion6.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion7.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completion7.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionAtPrint.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionAtPrint.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionBracketedDot.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionBracketedDot.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionCheck.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionCheck.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionDanglingDot.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionDanglingDot.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionDeprecation.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionDeprecation.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionEmptyBy.lean fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
completionEmptyBy.lean.out.expected fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
completionEmptyByBracketed.lean fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
completionEmptyByBracketed.lean.out.expected fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
completionEndSection.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionEndSection.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionEOF.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionEOF.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionFallback.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionFallback.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionFromExpectedType.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionFromExpectedType.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionIStr.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionIStr.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionOpenNamespaces.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionOpenNamespaces.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionOption.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionOption.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionPrefixIssue.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionPrefixIssue.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionPrivateTypes.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionPrivateTypes.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionPrv.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionPrv.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionStructureInstance.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionStructureInstance.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
completionTactics.lean fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
completionTactics.lean.out.expected fix: tactic completion in empty by blocks (#13348) 2026-04-15 08:39:55 +00:00
compNamespace.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
compNamespace.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
definition.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
definition.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
Diff.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
Diff.lean.out.expected feat: update RPC wire format (#12905) 2026-03-13 23:46:16 +00:00
discrsIssue.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
discrsIssue.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
docstringLinksExamples.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
docstringLinksExamples.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
documentSymbols.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
documentSymbols.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
dotIdCompletion.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
dotIdCompletion.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
dottedIdentNotation.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
dottedIdentNotation.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
editAfterError.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
editAfterError.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
editCompletion.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
editCompletion.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
errorExplanationInteractive.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
errorExplanationInteractive.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
expectedTypeAsGoal.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
expectedTypeAsGoal.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
explicitAppInstHole.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
explicitAppInstHole.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
findReferences.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
findReferences.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
foldingRange.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
foldingRange.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
fvarIdCollision.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
fvarIdCollision.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
ghostGoals.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
ghostGoals.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
goalEOF.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
goalEOF.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
goalIssue.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
goalIssue.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
goalsAccomplished.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
goalsAccomplished.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
goTo.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
goTo.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
goTo2.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
goTo2.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
guardMsgsCodeAction.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
guardMsgsCodeAction.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
haveInfo.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
haveInfo.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
highlight.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
highlight.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
highlightMatches.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
highlightMatches.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
hover.lean fix: preserve symbol hover for fun_induction function target (#13678) 2026-05-07 12:09:36 +00:00
hover.lean.out.expected fix: preserve symbol hover for fun_induction function target (#13678) 2026-05-07 12:09:36 +00:00
hoverAt.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
hoverAt.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
hoverBinderUnderscore.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
hoverBinderUnderscore.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
hoverDoForIn.lean fix: add term info for for loop variables in new do elaborator (#13399) 2026-04-13 20:29:55 +00:00
hoverDoForIn.lean.out.expected fix: add term info for for loop variables in new do elaborator (#13399) 2026-04-13 20:29:55 +00:00
hoverDot.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
hoverDot.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
hoverException.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
hoverException.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
hoverMatch.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
hoverMatch.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
hoverTacticExt.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
hoverTacticExt.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
importCompletion.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
importCompletion.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
incomingCallHierarchy.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
incomingCallHierarchy.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
incomingCallHierarchyWhere.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
incomingCallHierarchyWhere.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
incrementalCombinator.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
incrementalCombinator.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
incrementalCommand.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
incrementalCommand.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
incrementalInduction.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
incrementalInduction.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
incrementalMutual.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
incrementalMutual.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
incrementalTactic.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
incrementalTactic.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
infoIssues.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
infoIssues.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
inlayHints.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
inlayHints.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
interactiveDiagnostics.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
interactiveDiagnostics.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
interactiveGoalGoToLoc.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
interactiveGoalGoToLoc.lean.out.expected feat: update RPC wire format (#12905) 2026-03-13 23:46:16 +00:00
interactiveGoalPopups.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
interactiveGoalPopups.lean.out.expected feat: update RPC wire format (#12905) 2026-03-13 23:46:16 +00:00
interactiveTermGoals.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
interactiveTermGoals.lean.out.expected feat: update RPC wire format (#12905) 2026-03-13 23:46:16 +00:00
interactiveTraces.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
interactiveTraces.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
internalNamesIssue.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
internalNamesIssue.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
inWordCompletion.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
inWordCompletion.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
isRflParallel.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
issue4527.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
issue4527.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
issue5021.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
issue5021.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
issue5597.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
issue5597.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
jumpMutual.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
jumpMutual.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
keywordCompletion.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
keywordCompletion.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
lean3HoverIssue.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
lean3HoverIssue.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
macroGoalIssue.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
macroGoalIssue.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
match.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
match.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
matchPatternHover.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
matchPatternHover.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
matchStxCompletion.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
matchStxCompletion.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
moduleHierarchyImports.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
moduleHierarchyImports.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
outgoingCallHierarchy.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
outgoingCallHierarchy.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
partialNamespace.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
partialNamespace.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
plainGoal.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
plainGoal.lean.out.expected feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
plainGoalEmptyBy.lean feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
plainGoalEmptyBy.lean.out.expected feat: require indentation in commands, allow empty tactic sequences (#13229) 2026-04-08 14:05:47 +00:00
plainTermGoal.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
plainTermGoal.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
ppShowLetValues.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
ppShowLetValues.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
rename.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
rename.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
run_test.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
run_test.sh fix: abort waitFor server_interactive tests promptly on file worker fatal error (#13710) 2026-05-12 20:53:17 +00:00
rwElabConst.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
rwElabConst.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
semanticTokens.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
semanticTokens.lean.out.expected feat: improve message of unusedVariables linter (#13715) 2026-05-13 09:40:18 +00:00
semanticTokensVersoDocs.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
semanticTokensVersoDocs.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
signatureHelp.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
signatureHelp.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
stdOutput.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
strInterpSynthError.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
strInterpSynthError.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
structInstFieldHints.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
structInstFieldHints.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
structNameParentProj.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
structNameParentProj.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
tacticInduction.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
tacticInduction.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
terminationBySuggestion.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
terminationBySuggestion.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
travellingCompletions.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
travellingCompletions.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
tryThisCodeAction.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
tryThisCodeAction.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
unknownIdentifierCodeActions.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
unknownIdentifierCodeActions.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
unterminatedDocComment.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
unterminatedDocComment.lean.out.expected feat: server-side support for incremental diagnostics (#13260) 2026-04-21 12:48:15 +00:00
userWidget.lean feat: update RPC wire format (#12905) 2026-03-13 23:46:16 +00:00
userWidget.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
workspaceSymbols.lean chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
workspaceSymbols.lean.out.expected chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00