Add import for Init.System.Files in IO_test.lean

src/Init/Internal/Order/Basic.lean

@@ -7,11 +7,15 @@ module
 
 prelude
 
-public import Init.System.IO  -- for `MonoBind` instance
-import all Init.Control.Except  -- for `MonoBind` instance
-import all Init.Control.StateRef  -- for `MonoBind` instance
-import all Init.Control.Option  -- for `MonoBind` instance
-import all Init.System.ST  -- for `MonoBind` instance
+public import Init.System.IO
+public import Init.Control.StateRef
+public import Init.Control.Option
+import Init.Control.Except
+import all Init.Control.StateRef
+import all Init.System.ST
+import Init.RCases
+import Init.ByCases
+
 
 public section
 

src/Init/Internal/Order/Lemmas.lean

@@ -8,10 +8,11 @@ module
 
 prelude
 
-import all Init.Data.List.Control
-import all Init.Data.Option.Basic
-import all Init.Data.Array.Basic
 public import Init.Internal.Order.Basic
+public import Init.Control.Lawful.Basic
+public import Init.Data.List.Control
+import all Init.Data.List.Control
+import all Init.Data.Array.Basic
 
 public section
 

src/Init/System.lean

@@ -10,3 +10,4 @@ public import Init.System.IO
 public import Init.System.Platform
 public import Init.System.Uri
 public import Init.System.Promise
+public import Init.System.Files

src/Lean/Compiler/IR/LLVMBindings.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.System.IO
+import Init.Data.Ord.UInt
 
 public section
 

src/Lean/Data/Json/FromToJson/Basic.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 public import Lean.Data.Json.Printer
+public import Init.System.Files
 
 public section
 

src/Lean/Data/Json/Stream.lean

@@ -9,6 +9,7 @@ module
 prelude
 public import Lean.Data.Json.Parser
 public import Lean.Data.Json.Printer
+public import Init.System.Files
 
 public section
 

src/Lean/Declaration.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Expr
+import Init.Data.Ord.UInt
 
 public section
 

src/Lean/DocString/Links.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 public import Lean.Syntax
+public import Init.System.Files
 import Init.Data.String.TakeDrop
 import Init.Data.String.Search
 

src/Lean/LoadDynlib.lean

@@ -6,7 +6,7 @@ Authors: Mac Malone
 module
 
 prelude
-public import Init.System.IO
+public import Init.System.Files
 import Init.Data.String.TakeDrop
 
 public section

src/Lean/Server/ServerTask.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Task
+public import Init.System.Files
 
 public section
 

src/Lean/ToExpr.lean

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.ToLevel
 public import Init.Data.Rat.Basic
+public import Init.System.FilePath
 public section
 universe u
 namespace Lean

src/Lean/Util/LakePath.lean

@@ -7,7 +7,7 @@ Authors: Sebastian Ullrich
 module
 
 prelude
-public import Init.System.IO
+public import Init.System.Files
 
 public section
 

src/Lean/Util/Path.lean

@@ -11,7 +11,7 @@ with a directory `A/`. `import A` resolves to `path/A.olean`.
 module
 
 prelude
-public import Init.System.IO
+public import Init.System.Files
 import Init.Data.ToString.Name
 import Init.Data.String.TakeDrop
 

src/Leanc.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
 import Lean.Compiler.FFI
+import Init.System.Files
 
 open Lean.Compiler.FFI
 

src/Std/Internal/Async/Basic.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.System.Promise
+public import Init.System.Files
 
 public section
 

src/Std/Sync/Basic.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.System.IO
+public import Init.Control.StateRef
 
 @[expose] public section
 

src/Std/Tactic/BVDecide/LRAT/Parser.lean

@@ -6,7 +6,7 @@ Authors: Henrik Böving
 module
 
 prelude
-public import Init.System.IO
+public import Init.System.Files
 public import Std.Tactic.BVDecide.LRAT.Actions
 public import Std.Internal.Parsec
 

src/Std/Time/Zoned/Database/TZdb.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Std.Time.Zoned.Database.Basic
+public import Init.System.Files
 import Init.Data.String.TakeDrop
 
 public section

src/lake/Lake/Util/IO.lean

@@ -6,7 +6,7 @@ Authors: Mac Malone
 module
 
 prelude
-public import Init.System.IO
+public import Init.System.Files
 
 open System
 

src/lake/Lake/Util/Lift.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.System.IO
+public import Init.Control.Option
 
 namespace Lake
 

src/lake/Lake/Util/Lock.lean

@@ -6,7 +6,7 @@ Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich
 module
 
 prelude
-public import Init.System.IO
+public import Init.System.Files
 
 /-! # Lock File Utilities
 

src/lake/Lake/Util/NativeLib.lean

@@ -6,7 +6,7 @@ Authors: Mac Malone
 module
 
 prelude
-public import Init.System.IO
+public import Init.System.Files
 
 open System
 namespace Lake

tests/lean/file_not_found.lean

@@ -1,5 +1,5 @@
 prelude
-import Init.System.IO
+import Init.System.Files
 
 open IO.FS
 def usingIO {α} (x : IO α) : IO α := x

tests/lean/run/IO_test.lean

@@ -1,5 +1,5 @@
 prelude
-import Init.System.IO
+import Init.System.Files
 import Init.Data.List.Control
 import Init.Data.ToString