diff --git a/tests/lean/interactive/highlightMatches.lean b/tests/lean/interactive/highlightMatches.lean.disabled similarity index 100% rename from tests/lean/interactive/highlightMatches.lean rename to tests/lean/interactive/highlightMatches.lean.disabled diff --git a/tests/lean/interactive/interactiveDiagnostics.lean b/tests/lean/interactive/interactiveDiagnostics.lean.disabled similarity index 100% rename from tests/lean/interactive/interactiveDiagnostics.lean rename to tests/lean/interactive/interactiveDiagnostics.lean.disabled diff --git a/tests/lean/interactive/interactiveTraces.lean b/tests/lean/interactive/interactiveTraces.lean.disabled similarity index 100% rename from tests/lean/interactive/interactiveTraces.lean rename to tests/lean/interactive/interactiveTraces.lean.disabled