From 37e5f0335143369cc81c2971ea37c18a9b229cf5 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 15 Aug 2018 09:43:48 -0700
Subject: [PATCH] refactor(library/system/io): move into `init`

---
 gen/apply.lean                   | 2 +-
 library/init/default.lean        | 2 +-
 library/{system => init}/io.lean | 0
 script/gen_constants_cpp.py      | 2 +-
 tests/ir/lirc.lean               | 2 +-
 tests/lean/parsec1.lean          | 2 +-
 tests/lean/reader1.lean          | 2 +-
 tests/lean/run/deriv.lean        | 2 +-
 tests/lean/run/ext_eff.lean      | 2 +-
 tests/lean/run/handlers.lean     | 2 +-
 tests/lean/run/lirc1.lean        | 2 +-
 tests/lean/run/parser_ir1.lean   | 2 +-
 tests/lean/trust0/t1.lean        | 2 +-
 13 files changed, 12 insertions(+), 12 deletions(-)
 rename library/{system => init}/io.lean (100%)

diff --git a/gen/apply.lean b/gen/apply.lean
index 0b3d4f3b3a..0e8d43f73e 100644
--- a/gen/apply.lean
+++ b/gen/apply.lean
@@ -1,4 +1,4 @@
-import init.lean.config system.io
+import init.lean.config init.io
 open io
 
 @[reducible] def m := reader_t handle io
diff --git a/library/init/default.lean b/library/init/default.lean
index 11b5a2a41c..69dcbfd8d1 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -6,4 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import init.core init.control init.data.basic init.version
 import init.function init.util init.coe init.wf init.meta
-import init.meta.well_founded_tactics init.data
+import init.meta.well_founded_tactics init.data init.io
diff --git a/library/system/io.lean b/library/init/io.lean
similarity index 100%
rename from library/system/io.lean
rename to library/init/io.lean
diff --git a/script/gen_constants_cpp.py b/script/gen_constants_cpp.py
index 15529192ef..f5b190a403 100755
--- a/script/gen_constants_cpp.py
+++ b/script/gen_constants_cpp.py
@@ -90,7 +90,7 @@ def main(argv=None):
     return 0
     with open(tst_file, 'w') as f:
         f.write('-- DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py\n')
-        f.write("import system.io\n")
+        f.write("import init.io\n")
         f.write("open tactic\n");
         f.write("meta def script_check_id (n : name) : tactic unit :=\n");
         f.write("do env ← get_env, (env^.get n >> return ()) <|> (guard $ env^.is_namespace n) <|> (attribute.get_instances n >> return ()) <|> fail (\"identifier '\" ++ to_string n ++ \"' is not a constant, namespace nor attribute\")\n");
diff --git a/tests/ir/lirc.lean b/tests/ir/lirc.lean
index 199791b367..ac0c440dfc 100644
--- a/tests/ir/lirc.lean
+++ b/tests/ir/lirc.lean
@@ -1,4 +1,4 @@
-import system.io
+import init.io
 import init.lean.ir.lirc
 open lean.ir io
 
diff --git a/tests/lean/parsec1.lean b/tests/lean/parsec1.lean
index 18ed23b91a..4f9d29b5bf 100644
--- a/tests/lean/parsec1.lean
+++ b/tests/lean/parsec1.lean
@@ -1,4 +1,4 @@
-import system.io init.lean.parser.identifier init.lean.ir.parser init.lean.ir.format
+import init.io init.lean.parser.identifier init.lean.ir.parser init.lean.ir.format
 open lean.parser
 open lean.parser.monad_parsec
 
diff --git a/tests/lean/reader1.lean b/tests/lean/reader1.lean
index 22c3d128b9..f4b784a010 100644
--- a/tests/lean/reader1.lean
+++ b/tests/lean/reader1.lean
@@ -1,4 +1,4 @@
-import init.lean.parser.reader.module system.io
+import init.lean.parser.reader.module init.io
 open lean.parser
 open lean.parser.reader
 
diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean
index 243e808ad0..aa2c673e78 100644
--- a/tests/lean/run/deriv.lean
+++ b/tests/lean/run/deriv.lean
@@ -1,5 +1,5 @@
 /- Benchmark for new code generator -/
-import system.io
+import init.io
 
 inductive Expr
 | Val : int → Expr
diff --git a/tests/lean/run/ext_eff.lean b/tests/lean/run/ext_eff.lean
index 1e75acccc1..7340dad092 100644
--- a/tests/lean/run/ext_eff.lean
+++ b/tests/lean/run/ext_eff.lean
@@ -1,6 +1,6 @@
 -- TODO: renable test after we restore tactic framework
 #exit
-import system.io
+import init.io
 
 /- An extensible effects library, inspired by "Freer Monads, More Extensible Effects" (O. Kiselyov, H. Ishii)
    and https://github.com/lexi-lambda/freer-simple -/
diff --git a/tests/lean/run/handlers.lean b/tests/lean/run/handlers.lean
index b2ee9fc7ec..16d62a076b 100644
--- a/tests/lean/run/handlers.lean
+++ b/tests/lean/run/handlers.lean
@@ -1,4 +1,4 @@
-import system.io
+import init.io
 
 /- Based on https://github.com/slindley/effect-handlers -/
 
diff --git a/tests/lean/run/lirc1.lean b/tests/lean/run/lirc1.lean
index 629851840a..2696ebd588 100644
--- a/tests/lean/run/lirc1.lean
+++ b/tests/lean/run/lirc1.lean
@@ -1,4 +1,4 @@
-import system.io
+import init.io
 import init.lean.ir.lirc
 open lean.ir
 
diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean
index c0435291eb..8a8f339190 100644
--- a/tests/lean/run/parser_ir1.lean
+++ b/tests/lean/run/parser_ir1.lean
@@ -1,4 +1,4 @@
-import system.io
+import init.io
 import init.lean.ir.parser init.lean.ir.format
 import init.lean.ir.elim_phi init.lean.ir.type_check
 import init.lean.ir.extract_cpp
diff --git a/tests/lean/trust0/t1.lean b/tests/lean/trust0/t1.lean
index fd5d599a56..d083d257d5 100644
--- a/tests/lean/trust0/t1.lean
+++ b/tests/lean/trust0/t1.lean
@@ -1,2 +1,2 @@
-import system.io
+import init.io
 #print trust