refactor(library/init): move io and platform to system subdir

library/init/data/random.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.io init.data.int
+import init.system.io init.data.int
 universes u
 
 /-

library/init/data/uint.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.fin.basic init.platform
+import init.data.fin.basic init.system.platform
 
 open Nat
 

library/init/default.lean

@@ -5,5 +5,5 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.core init.control init.data.basic
-import init.coe init.wf init.data init.io init.util
-import init.fix
+import init.coe init.wf init.data init.system
+import init.util init.fix

library/init/lean/compiler/constfolding.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.expr init.platform
+import init.system.platform
+import init.lean.expr
 import init.lean.compiler.util
 
 /- Constant folding for primitives that have special runtime support. -/

library/init/lean/environment.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.io
+import init.system.io
 import init.util
 import init.data.bytearray
 import init.lean.declaration

library/init/lean/options.lean

@@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich and Leonardo de Moura
 -/
 prelude
-import init.lean.kvmap init.io init.control.combinators init.data.tostring
+import init.lean.kvmap
+import init.system.io
+import init.control.combinators
+import init.data.tostring
 
 namespace Lean
 

library/init/lean/util.lean

@@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Sebastian Ullrich
 -/
 prelude
-import init.lean.position init.io
+import init.system.io
+import init.lean.position
 
 namespace Lean
 
-/-- Print and accumulate run time of `act` when Option `profiler` is set to `True`. -/
+/-- Print and accumulate run time of `act` when Option `profiler` is set to `true`. -/
 @[extern 5 "lean_lean_profileit"]
 constant profileit {α : Type} (category : @& String) (pos : @& Position) (act : IO α) : IO α := act
 def profileitPure {α : Type} (category : String) (pos : Position) (fn : Unit → α) : IO α :=