chore: fix tests

We have removed `MetaIO`. We use use `CoreM` instead.

tests/lean/PPRoundtrip.lean

@@ -5,11 +5,11 @@ open Lean.Elab.Term
 open Lean.Elab.Command
 open Lean.Format
 
-def check (stx : TermElabM Syntax) (optionsPerPos : OptionsPerPos := {}) : MetaIO Unit := do
-env ← MetaIO.getEnv;
-opts ← MetaIO.getOptions;
+def check (stx : TermElabM Syntax) (optionsPerPos : OptionsPerPos := {}) : CoreM Unit := do
+env ← Core.getEnv;
+opts ← Core.getOptions;
 table ← Parser.builtinTokenTable.get;
-discard $ liftM $ MetaHasEval.eval env opts do
+discard $ liftIO $ MetaHasEval.eval env opts do
   stx ← stx;
   e ← elabTermAndSynthesize stx none <* throwErrorIfErrors;
   stx' ← liftMetaM $ delab e optionsPerPos;

tests/lean/run/depElim1.lean

@@ -164,6 +164,7 @@ def ex1 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) :
 := arbitrary _
 
 #eval test `ex1 2 `elimTest1
+
 #print elimTest1
 
 inductive Vec (α : Type u) : Nat → Type u

tests/lean/run/eval_unboxed_const.lean

@@ -3,8 +3,8 @@ open Lean
 
 def c1 : Bool := true
 
-unsafe def tst1 : MetaIO Unit := do
-env ← MetaIO.getEnv;
+unsafe def tst1 : CoreM Unit := do
+env ← Core.getEnv;
 let v := env.evalConst Bool `c1;
 IO.println v
 
@@ -12,8 +12,8 @@ IO.println v
 
 def c2 : Bool := false
 
-unsafe def tst2 : MetaIO Unit := do
-env ← MetaIO.getEnv;
+unsafe def tst2 : CoreM Unit := do
+env ← Core.getEnv;
 let v := env.evalConst Bool `c2;
 IO.println v
 

tests/lean/run/evalconst.lean

@@ -3,8 +3,8 @@ open Lean
 
 def x := 10
 
-unsafe def tst : MetaIO Unit := do
-env ← MetaIO.getEnv;
+unsafe def tst : CoreM Unit := do
+env ← Core.getEnv;
 IO.println $ env.evalConst Nat `x;
 pure ()
 
@@ -12,9 +12,9 @@ pure ()
 
 def f (x : Nat) := x + 1
 
-unsafe def tst2 : MetaIO Unit := do
-env ← MetaIO.getEnv;
-f ← liftM $ IO.ofExcept $ env.evalConst (Nat → Nat) `f;
+unsafe def tst2 : CoreM Unit := do
+env ← Core.getEnv;
+f ← liftIO $ IO.ofExcept $ env.evalConst (Nat → Nat) `f;
 IO.println $ (f 10);
 pure ()
 

tests/lean/run/frontend1.lean

@@ -2,16 +2,16 @@ import Lean.Elab
 open Lean
 open Lean.Elab
 
-def run (input : String) (failIff : Bool := true) : MetaIO Unit :=
-do env  ← MetaIO.getEnv;
-   opts ← MetaIO.getOptions;
-   (env, messages) ← liftM $ process input env opts;
+def run (input : String) (failIff : Bool := true) : CoreM Unit :=
+do env  ← Core.getEnv;
+   opts ← Core.getOptions;
+   (env, messages) ← liftIO $ process input env opts;
    messages.forM $ fun msg => IO.println msg;
-   when (failIff && messages.hasErrors) $ throw (IO.userError "errors have been found");
-   when (!failIff && !messages.hasErrors) $ throw (IO.userError "there are no errors");
+   when (failIff && messages.hasErrors) $ Core.throwError "errors have been found";
+   when (!failIff && !messages.hasErrors) $ Core.throwError "there are no errors";
    pure ()
 
-def fail (input : String) : MetaIO Unit :=
+def fail (input : String) : CoreM Unit :=
 run input false
 
 def M := IO Unit

tests/lean/run/kernel1.lean

@@ -2,8 +2,8 @@ import Lean
 
 open Lean
 
-def checkDefEq (a b : Name) : MetaIO Unit := do
-env ← MetaIO.getEnv;
+def checkDefEq (a b : Name) : CoreM Unit := do
+env ← Core.getEnv;
 let a := mkConst a;
 let b := mkConst b;
 let r := Kernel.isDefEq env {} a b;

tests/lean/run/kernel2.lean

@@ -1,15 +1,15 @@
 import Lean
 open Lean
 
-def checkDefEq (a b : Name) : MetaIO Unit := do
-env ← MetaIO.getEnv;
+def checkDefEq (a b : Name) : CoreM Unit := do
+env ← Core.getEnv;
 let a := mkConst a;
 let b := mkConst b;
 let r := Kernel.isDefEq env {} a b;
 IO.println (toString a ++ " =?= " ++ toString b ++ " := " ++ toString r)
 
-def whnf (a : Name) : MetaIO Unit := do
-env ← MetaIO.getEnv;
+def whnf (a : Name) : CoreM Unit := do
+env ← Core.getEnv;
 let a := mkConst a;
 let r := Kernel.whnf env {} a;
 IO.println (toString a ++ " ==> " ++ toString r)

tests/lean/run/structure.lean

@@ -13,8 +13,8 @@ structure S3 :=
 structure S4 extends S2, S3 :=
 (s : Nat)
 
-def check (b : Bool) : MetaIO Unit :=
-unless b $ throw $ IO.userError "check failed"
+def check (b : Bool) : CoreM Unit :=
+unless b $ Core.throwError "check failed"
 
 class S5 :=
 (x y : Nat)
@@ -22,8 +22,8 @@ class S5 :=
 inductive D
 | mk (x y z : Nat) : D
 
-def tst : MetaIO Unit :=
-do env ← MetaIO.getEnv;
+def tst : CoreM Unit :=
+do env ← Core.getEnv;
    IO.println (getStructureFields env `Lean.Environment);
    check $ getStructureFields env `S4 == #[`toS2, `toS3, `s];
    check $ getStructureFields env `S1 == #[`x, `y];

tests/lean/run/termParserAttr.lean

@@ -2,13 +2,13 @@ import Lean
 open Lean
 open Lean.Elab
 
-def run (input : String) (failIff : Bool := true) : MetaIO Unit :=
-do env  ← MetaIO.getEnv;
-   opts ← MetaIO.getOptions;
-   (env, messages) ← liftM $ process input env opts;
-   messages.toList.forM $ fun msg => IO.println msg;
-   when (failIff && messages.hasErrors) $ throw (IO.userError "errors have been found");
-   when (!failIff && !messages.hasErrors) $ throw (IO.userError "there are no errors");
+def run (input : String) (failIff : Bool := true) : CoreM Unit :=
+do env  ← Core.getEnv;
+   opts ← Core.getOptions;
+   (env, messages) ← liftIO $ process input env opts;
+   messages.toList.forM $ fun msg => liftIO $ IO.println msg;
+   when (failIff && messages.hasErrors) $ Core.throwError "errors have been found";
+   when (!failIff && !messages.hasErrors) $ Core.throwError "there are no errors";
    pure ()
 
 open Lean.Parser

tests/lean/run/toExpr.lean

@@ -2,8 +2,8 @@ import Lean
 
 open Lean
 
-unsafe def test {α : Type} [HasToString α] [ToExpr α] [HasBeq α] (a : α) : MetaIO Unit := do
-env ← MetaIO.getEnv;
+unsafe def test {α : Type} [HasToString α] [ToExpr α] [HasBeq α] (a : α) : CoreM Unit := do
+env ← Core.getEnv;
 let auxName := `_toExpr._test;
 let decl := Declaration.defnDecl {
   name     := auxName,
@@ -15,14 +15,14 @@ let decl := Declaration.defnDecl {
 };
 IO.println (toExpr a);
 match env.addAndCompile {} decl with
-| Except.error _ => throw $ IO.userError "addDecl failed"
+| Except.error _ => Core.throwError "addDecl failed"
 | Except.ok env  => do
   match env.evalConst α auxName with
-  | Except.error ex => throw $ IO.userError ex
+  | Except.error ex => Core.throwError ex
   | Except.ok b => do
     IO.println b;
     unless (a == b) $
-      throw $ IO.userError "toExpr failed";
+      Core.throwError "toExpr failed";
     pure ()
 
 #eval test #[(1, 2), (3, 4)]