chore: bump to nightly-2022-08-09

.gitignore

@@ -5,6 +5,5 @@ Logs/
 PreData/
 Outputs/
 lean_packages/
-!lean_packages/manifest.json
 sources/
 *.tar.gz

Mathport/Binary/Basic.lean

@@ -42,7 +42,7 @@ def liftCoreM (x : CoreM α) : BinportM α := do
   Elab.Command.liftCoreM x
 
 def liftMetaM (x : MetaM α) : BinportM α := do
-  liftTermElabM (declName? := some (← read).currDecl) (liftM x)
+  liftTermElabM (liftM x)
 
 def addNameAlignment (n3 n4 : Name) : BinportM Unit := do
   liftCoreM $ Mathlib.Prelude.Rename.addNameAlignment n3 n4

Mathport/Syntax/Translate/Basic.lean

@@ -589,9 +589,8 @@ def trBinderIdentI : BinderName → M (Syntax.BinderIdent)
 def optTy (ty : Option Term) : M (Option (TSyntax ``Parser.Term.typeSpec)) :=
   ty.mapM fun stx => do `(Parser.Term.typeSpec| : $stx)
 
-def trCalcArgs (args : Array (Spanned Expr × Spanned Expr)) : M (Array (TSyntax ``calcStep)) :=
-  args.mapM fun (lhs, rhs) =>
-    return mkNode ``calcStep #[← trExpr lhs, mkAtom ":=", ← trExpr rhs]
+def trCalcArg : Spanned Expr × Spanned Expr → M (TSyntax ``calcStep)
+  | (lhs, rhs) => do `(calcStep| $(← trExpr lhs) := $(← trExpr rhs))
 
 mutual
 
@@ -620,7 +619,10 @@ mutual
       `(tactic| first $[| $(← tacs.mapM fun tac => trTactic tac):tactic]*)
     | Tactic.«[]» _tacs => warn! "unsupported (impossible)"
     | Tactic.exact_shortcut ⟨_, Expr.calc args⟩ => do
-      `(tactic| calc $(← trCalcArgs args)*)
+      if h : args.size > 0 then
+        `(tactic| calc $(← trCalcArg args[0]) $(← args[1:].toArray.mapM trCalcArg)*)
+      else
+        warn! "empty calc is unsupported"
     | Tactic.exact_shortcut e => do `(tactic| exact $(← trExpr e))
     | Tactic.expr e =>
       match e.unparen with
@@ -1076,7 +1078,11 @@ def trExpr' : Expr → M Term
   | Expr.if (some h) c t e => do
     `(if $(mkIdent h.kind):ident : $(← trExpr c)
       then $(← trExpr t) else $(← trExpr e))
-  | Expr.calc args => do `(calc $(← trCalcArgs args)*)
+  | Expr.calc args => do
+    if h : args.size > 0 then
+      `(calc $(← trCalcArg args[0]) $(← args[1:].toArray.mapM trCalcArg)*)
+    else
+      warn! "empty calc is unsupported"
   | Expr.«@» _ e => do `(@$(← trExpr e))
   | Expr.pattern e => trExpr e
   | Expr.«`()» _ true e => do `(quote $(← trExpr e))

lakefile.lean

@@ -7,6 +7,8 @@ package mathport
 -- as this commit of mathlib4 uses.
 require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master"
 
+lean_lib Mathport
+
 @[defaultTarget]
 lean_exe mathport where
   root := `MathportApp

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-07-24
+leanprover/lean4:nightly-2022-08-09

lean_packages/manifest.json

@@ -1,5 +1,6 @@
-{"version": 1,
+{"version": 2,
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4",
-   "rev": "297e7eae2ed008ad633c80a55a831e0d63084376",
-   "name": "mathlib"}]}
+   "rev": "cf2e683c25eba2d798b2460d5703a63db72272c0",
+   "name": "mathlib",
+   "inputRev": "master"}]}