From 5ee6767b2157766c8aa451bb93d1434436e593a2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 4 Nov 2024 12:11:29 +1100 Subject: [PATCH] update tests --- ImportGraphTest/Imports.lean | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/ImportGraphTest/Imports.lean b/ImportGraphTest/Imports.lean index 0abc260..5f17477 100644 --- a/ImportGraphTest/Imports.lean +++ b/ImportGraphTest/Imports.lean @@ -36,12 +36,7 @@ elab "#unused_transitive_imports" names:ident* : command => do if !u.isEmpty then logInfo <| s!"Transitively unused imports of {n}:\n{"\n".intercalate (u.map (fun i => s!" {i}"))}" --- This test case can be removed after nightly-2024-10-24, because these imports have been cleaned up. --- It should be replaced with another test case! /-- -info: Transitively unused imports of Init.Control.StateRef: - Init.System.IO ---- info: Transitively unused imports of Init.System.IO: Init.Control.Reader -/ @@ -55,14 +50,6 @@ info: Transitively unused imports of ImportGraphTest.Used: #guard_msgs in #unused_transitive_imports ImportGraphTest.Used ImportGraphTest.Unused Init.Control.Reader --- This is a spurious unused transitive import, because it relies on notation from `Init.Core`. -/-- -info: Transitively unused imports of Init.Control.Basic: - Init.Core --/ -#guard_msgs in -#unused_transitive_imports Init.Control.Basic Init.Core - elab "#transitivelyRequiredModules_test" : command => do let env ← getEnv let unused ← liftCoreM <| env.transitivelyRequiredModules `ImportGraph.RequiredModules