chore: update to Lean v4.12.0

Author: tydeu

Lyre/Builder.lean

@@ -204,7 +204,7 @@ def mkCtor (stx : Lyre.CtorInfo) (argStxs : Array Lyre.Arg) : BuilderM (IR.CtorI
     | throwWithSyntax (ref := ctor) stx s!"ill-formed IR constructor name '{ctor.getId}'"
   let name ← id do
     let some ctorId := ctorId? | return Name.anonymous
-    let name ← resolveGlobalConstNoOverloadWithInfo ctorId
+    let name ← realizeGlobalConstNoOverloadWithInfo ctorId
     let some (.ctorInfo {cidx := ecidx, ..}) := (← getEnv).find? name
       | throwWithSyntax (ref := ctorId) stx m!"'{name}' is not a constructor"
     if cidx != ecidx then
@@ -244,7 +244,7 @@ def mkExpr (stx : Lyre.Expr) : BuilderM (IR.Expr × Option IRType) := do
   | `(irExpr|sproj[$n,$o] $x $[: $ty?]?) =>
     return (.sproj n.getNat o.getNat (← getVarId x), ← ty?.mapM mkType)
   | `(fap|$c:ident $ys*) =>
-    let name ← try resolveGlobalConstNoOverloadWithInfo c catch _ => pure c.getId
+    let name ← try realizeGlobalConstNoOverloadWithInfo c catch _ => pure c.getId
     if let some decl := IR.findEnvDecl (← getEnv) name then
       let ty := match decl with
         | .fdecl (type := ty) .. | .extern (type := ty) .. => ty

Lyre/Commands.lean

@@ -14,17 +14,19 @@ namespace Lyre
 scoped elab (name := Test.printIr) kw:"#print_ir " id:ident : command => do
   let name ← do
     try
-      resolveGlobalConstNoOverloadWithInfo id
+      liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
     catch _ =>
-      pure <| if rootNamespace.isPrefixOf id.getId
-        then removeRoot id.getId else (← getCurrNamespace) ++ id.getId
+      if rootNamespace.isPrefixOf id.getId then
+        pure <| removeRoot id.getId
+      else
+        pure <| (← getCurrNamespace) ++ id.getId
   let some decl := IR.findEnvDecl (← getEnv) name
     | throwErrorAt id "no IR found for '{name}'"
   logInfoAt kw (IR.declToString decl)
 
 /--
-Directly set the Lean IR for a the definition `name`.
-The definition most not already have IR. This can be accomplish
+Directly set the Lean IR for the definition `name`.
+The definition must not already have IR. This can be accomplish
 by marking the definition `noncomputable` when declared.
 -/
 def setAdhoc [Monad m] [MonadEnv m] [MonadError m]
@@ -70,7 +72,7 @@ scoped syntax (name := irImpl)
 "ir_impl " ident param* (" : " irType)? " := " stmtSeq : command
 
 elab_rules : command | `(ir_impl $id $ps* $[: $ty?]? := $stmts*) => do
-  let name ← resolveGlobalConstNoOverloadWithInfo id
+  let name ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
   let (ps, ty, body) ← liftTermElabM <| BuilderM.run do
     let ps ← ps.mapM mkParam
     let (body, bty?) ← mkFnBody stmts

lakefile.lean

@@ -15,6 +15,7 @@ def runLean (file : FilePath) : ScriptM PUnit := do
   if exitCode ≠ 0 then
     IO.Process.exit exitCode.toUInt8
 
+@[test_driver]
 script test do
   runLean <| "tests" / "basic.lean"
   return 0

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:4.4.0
+leanprover/lean4:v4.12.0

tests/basic.lean

@@ -8,6 +8,8 @@ ir_impl myAdd (m : @& obj) (n : @& obj) :=
   let x := Nat.add m n
   ret x
 
+/-- info: 3 -/
+#guard_msgs in
 #eval myAdd 1 2
 
 noncomputable opaque getNum (_ : Unit) : Nat
@@ -16,6 +18,8 @@ ir_impl getNum (_ : obj) :=
   let n := 2 : obj
   ret n
 
+/-- info: 2 -/
+#guard_msgs in
 #eval getNum ()
 
 noncomputable opaque throwMyError : IO Unit
@@ -26,6 +30,8 @@ ir_impl throwMyError (w : obj) :=
   let res := ctor_1[EStateM.Result.error] err w
   ret res
 
+/-- info: error: myError -/
+#guard_msgs in
 #eval throwMyError.toBaseIO
 
 noncomputable opaque getNil (α : Type u) : List α
@@ -34,4 +40,6 @@ ir_impl getNil (_ : ◾) :=
   let l : obj := List.nil
   ret l
 
+/-- info: [] -/
+#guard_msgs in
 #eval getNil Nat