From 2389b6dc925c3772e6607e83ce19a4ea18a8ac10 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Oct 2020 17:41:27 -0700
Subject: [PATCH] chore: update stage0

---
 stage0/src/Init/Control/EState.lean   |   2 +-
 stage0/src/Init/Control/Except.lean   |  22 +++---
 stage0/src/Init/Control/Reader.lean   |   4 +-
 stage0/src/Init/Control/State.lean    |   6 +-
 stage0/src/Lean/Elab/Do.lean          |   2 +-
 stage0/stdlib/Init/Control/Except.c   | 103 +++++++++++---------------
 stage0/stdlib/Init/Control/Reader.c   |  16 ++--
 stage0/stdlib/Init/Control/State.c    |  26 +++----
 stage0/stdlib/Init/Control/StateRef.c |   4 +-
 stage0/stdlib/Init/System/IO.c        |   8 +-
 stage0/stdlib/Lean/CoreM.c            |  32 ++++----
 stage0/stdlib/Lean/Elab/Do.c          |  37 ++++-----
 stage0/stdlib/Lean/MonadEnv.c         |   4 +-
 stage0/stdlib/Lean/Util/MonadCache.c  |   4 +-
 stage0/stdlib/Lean/Util/Trace.c       |   8 +-
 stage0/stdlib/Std/ShareCommon.c       |   6 +-
 16 files changed, 125 insertions(+), 159 deletions(-)

diff --git a/stage0/src/Init/Control/EState.lean b/stage0/src/Init/Control/EState.lean
index d63b97bddb..0df0dc933f 100644
--- a/stage0/src/Init/Control/EState.lean
+++ b/stage0/src/Init/Control/EState.lean
@@ -120,7 +120,7 @@ instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) :=
 { throw := @EStateM.throw _ _, tryCatch := @EStateM.tryCatch _ _ _ _ }
 
 instance : MonadFinally (EStateM ε σ) :=
-{ finally' := fun α β x h s =>
+{ tryFinally' := fun α β x h s =>
   let r := x s;
   match r with
   | Result.ok a s    => match h (some a) s with
diff --git a/stage0/src/Init/Control/Except.lean b/stage0/src/Init/Control/Except.lean
index 5175005772..cae3d1f61f 100644
--- a/stage0/src/Init/Control/Except.lean
+++ b/stage0/src/Init/Control/Except.lean
@@ -136,9 +136,6 @@ class MonadExceptOf (ε : Type u) (m : Type v → Type w) :=
 abbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (e : ε) : m α :=
 MonadExceptOf.throw e
 
-abbrev catchThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α :=
-MonadExceptOf.tryCatch x handle
-
 abbrev tryCatchThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α :=
 MonadExceptOf.tryCatch x handle
 
@@ -161,9 +158,6 @@ class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) :=
 
 export MonadExcept (throw tryCatch)
 
-abbrev MonadExcept.«catch» {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α :=
-MonadExcept.tryCatch x handle
-
 instance MonadExceptOf.isMonadExcept (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m :=
 { throw := fun _ e        => throwThe ε e,
   tryCatch := fun _ x handle => tryCatchThe ε x handle }
@@ -194,23 +188,27 @@ instance ExceptT.monadControl (ε : Type u) (m : Type u → Type v) [Monad m] :
 }
 
 class MonadFinally (m : Type u → Type v) :=
-(finally' {α β} : m α → (Option α → m β) → m (α × β))
+(tryFinally' {α β} : m α → (Option α → m β) → m (α × β))
 
-export MonadFinally (finally')
+export MonadFinally (tryFinally')
 
 /-- Execute `x` and then execute `finalizer` even if `x` threw an exception -/
+@[inline] abbrev tryFinally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α := do
+Prod.fst <$> tryFinally' x (fun _ => finalizer)
+
+-- TODO delete
 @[inline] abbrev finally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α := do
-Prod.fst <$> finally' x (fun _ => finalizer)
+Prod.fst <$> tryFinally' x (fun _ => finalizer)
 
 instance Id.finally : MonadFinally Id :=
-{ finally' := fun α β x h =>
+{ tryFinally' := fun α β x h =>
    let a := x;
    let b := h (some x);
    pure (a, b) }
 
 instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] : MonadFinally (ExceptT ε m) :=
-{ finally' := fun α β x h => ExceptT.mk do
-    r ← finally' x (fun e? => match e? with
+{ tryFinally' := fun α β x h => ExceptT.mk do
+    r ← tryFinally' x (fun e? => match e? with
         | some (Except.ok a) => h (some a)
         | _                  => h none);
     match r with
diff --git a/stage0/src/Init/Control/Reader.lean b/stage0/src/Init/Control/Reader.lean
index c033ab6442..4306ad1011 100644
--- a/stage0/src/Init/Control/Reader.lean
+++ b/stage0/src/Init/Control/Reader.lean
@@ -118,8 +118,8 @@ instance ReaderT.monadControl (ρ : Type u) (m : Type u → Type v) : MonadContr
   restoreM := fun α x ctx => x,
 }
 
-instance ReaderT.finally {m : Type u → Type v} {ρ : Type u} [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) :=
-{ finally' := fun α β x h ctx => finally' (x ctx) (fun a? => h a? ctx) }
+instance ReaderT.tryFinally {m : Type u → Type v} {ρ : Type u} [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) :=
+{ tryFinally' := fun α β x h ctx => tryFinally' (x ctx) (fun a? => h a? ctx) }
 
 class MonadWithReaderOf (ρ : Type u) (m : Type u → Type v) :=
 (withReader {α : Type u} : (ρ → ρ) → m α → m α)
diff --git a/stage0/src/Init/Control/State.lean b/stage0/src/Init/Control/State.lean
index d804bef33a..7b9c4a7989 100644
--- a/stage0/src/Init/Control/State.lean
+++ b/stage0/src/Init/Control/State.lean
@@ -154,9 +154,9 @@ instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] : M
   restoreM := fun α x => do (a, s) ← liftM x; set s; pure a
 }
 
-instance StateT.finally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] : MonadFinally (StateT σ m) :=
-{ finally' := fun α β x h s => do
-  ((a, _), (b, s'')) ← finally' (x s)
+instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] : MonadFinally (StateT σ m) :=
+{ tryFinally' := fun α β x h s => do
+  ((a, _), (b, s'')) ← tryFinally' (x s)
     (fun p? => match p? with
       | some (a, s') => h (some a) s'
       | none         => h none s);
diff --git a/stage0/src/Lean/Elab/Do.lean b/stage0/src/Lean/Elab/Do.lean
index 28364796c3..cac636e53c 100644
--- a/stage0/src/Lean/Elab/Do.lean
+++ b/stage0/src/Lean/Elab/Do.lean
@@ -1400,7 +1400,7 @@ def doTryToCode (doSeqToCode : List Syntax → M CodeBlock) (doTry : Syntax) (do
       if hasBreakContinueReturn finallyCode.code then
         throwError "'finally' currently does 'return', 'break', nor 'continue'"
       let finallyTerm ← liftMacroM $ ToTerm.run finallyCode.code ctx.m {} ToTerm.Kind.regular
-      `(«finally» $term $finallyTerm)
+      `(tryFinally $term $finallyTerm)
   let doElemsNew ← liftMacroM $ ToTerm.matchNestedTermResult ref term uvars a r bc
   doSeqToCode (doElemsNew ++ doElems)
 
diff --git a/stage0/stdlib/Init/Control/Except.c b/stage0/stdlib/Init/Control/Except.c
index 7d0a08748c..dc3fe423a8 100644
--- a/stage0/stdlib/Init/Control/Except.c
+++ b/stage0/stdlib/Init/Control/Except.c
@@ -14,6 +14,7 @@
 extern "C" {
 #endif
 lean_object* l_MonadExcept_orelse_x27___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_tryFinally___rarg___lambda__1___boxed(lean_object*);
 lean_object* l_ExceptT_monadExceptParent___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Id_finally(lean_object*, lean_object*);
 lean_object* l_ExceptT_lift___rarg___lambda__1(lean_object*);
@@ -25,6 +26,7 @@ lean_object* l_Except_Monad___lambda__2(lean_object*, lean_object*, lean_object*
 lean_object* l_ExceptT_lift___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_adapt___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_MonadFunctor___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_tryFinally___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_toOption___rarg(lean_object*);
 lean_object* l_MonadExcept_orelse_x27___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_MonadExcept_HasOrelse(lean_object*, lean_object*);
@@ -35,8 +37,6 @@ lean_object* l_finally(lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_Monad___rarg___lambda__8(lean_object*, lean_object*);
 lean_object* l_Except_toOption___rarg___boxed(lean_object*);
 lean_object* l_Except_bind(lean_object*, lean_object*, lean_object*);
-lean_object* l_MonadExcept_catch___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_MonadExcept_catch(lean_object*, lean_object*);
 lean_object* l_Except_Monad___closed__10;
 lean_object* l_Except_toBool___rarg___boxed(lean_object*);
 lean_object* l_Except_toString___rarg(lean_object*, lean_object*, lean_object*);
@@ -57,6 +57,7 @@ lean_object* l_MonadExcept_HasOrelse___rarg(lean_object*, lean_object*);
 extern lean_object* l_ULift_HasRepr___rarg___closed__2;
 lean_object* l_Except_Monad___lambda__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_map___rarg(lean_object*, lean_object*);
+lean_object* l_tryFinally(lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_MonadLift___rarg(lean_object*);
 lean_object* l_Except_toString___rarg___closed__1;
 lean_object* l_Except_MonadExceptOf___lambda__1(lean_object*, lean_object*);
@@ -67,8 +68,6 @@ lean_object* l_ExceptT_finally___rarg___lambda__2(lean_object*, lean_object*);
 lean_object* l_Except_MonadExceptOf___closed__2;
 lean_object* l_ExceptT_bindCont(lean_object*, lean_object*);
 lean_object* l_Except_mapError___rarg(lean_object*, lean_object*);
-lean_object* l_finally___rarg___lambda__1___boxed(lean_object*);
-lean_object* l_catchThe___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_toBool(lean_object*, lean_object*);
 lean_object* l_ExceptT_monadExceptParent___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_toString___rarg___closed__2;
@@ -84,7 +83,6 @@ lean_object* l_Except_Monad___closed__3;
 lean_object* l_ExceptT_Monad___rarg___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_Monad___closed__7;
 lean_object* l_ExceptT_lift(lean_object*, lean_object*);
-lean_object* l_finally___rarg___lambda__1(lean_object*);
 lean_object* l_ExceptT_tryCatch___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_throwThe(lean_object*, lean_object*);
 lean_object* l_ExceptT_monadControl(lean_object*, lean_object*);
@@ -92,12 +90,12 @@ lean_object* l_ExceptT_pure___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_monadExceptParent___rarg(lean_object*);
 lean_object* l_ExceptT_finally(lean_object*, lean_object*);
 lean_object* l_Except_tryCatch___rarg(lean_object*, lean_object*);
-lean_object* l_finally___rarg___closed__1;
 lean_object* l_ExceptT_finally___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_Monad___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Except_Monad___closed__5;
 lean_object* l_MonadExcept_orelse___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_map___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_tryFinally___rarg___lambda__1(lean_object*);
 lean_object* l_ExceptT_bind(lean_object*, lean_object*);
 lean_object* l_Except_HasRepr___rarg(lean_object*, lean_object*);
 lean_object* l_Except_mapError(lean_object*, lean_object*, lean_object*);
@@ -155,12 +153,12 @@ lean_object* l_ExceptT_Monad___rarg___lambda__2(lean_object*, lean_object*, lean
 lean_object* l_Id_finally___rarg(lean_object*, lean_object*);
 lean_object* l_ExceptT_map___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_Monad___rarg___lambda__6(lean_object*, lean_object*, lean_object*);
+lean_object* l_tryFinally___rarg___closed__1;
 lean_object* l_observing___rarg___lambda__2(lean_object*, lean_object*);
 lean_object* l_ExceptT_Monad___rarg___lambda__8___boxed(lean_object*, lean_object*);
 lean_object* l_Except_Monad___closed__9;
 lean_object* l_Except_Monad___closed__4;
 lean_object* l_Except_HasRepr(lean_object*, lean_object*);
-lean_object* l_catchThe(lean_object*, lean_object*);
 lean_object* l_ExceptT_monadExceptParent___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_bindCont___at_ExceptT_Monad___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ExceptT_Monad(lean_object*, lean_object*);
@@ -1885,25 +1883,6 @@ x_3 = lean_alloc_closure((void*)(l_throwThe___rarg), 3, 0);
 return x_3;
 }
 }
-lean_object* l_catchThe___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-lean_object* x_5; lean_object* x_6; 
-x_5 = lean_ctor_get(x_1, 1);
-lean_inc(x_5);
-lean_dec(x_1);
-x_6 = lean_apply_3(x_5, lean_box(0), x_3, x_4);
-return x_6;
-}
-}
-lean_object* l_catchThe(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_catchThe___rarg), 4, 0);
-return x_3;
-}
-}
 lean_object* l_tryCatchThe___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@@ -2062,25 +2041,6 @@ x_2 = l_Except_MonadExceptOf___closed__3;
 return x_2;
 }
 }
-lean_object* l_MonadExcept_catch___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-lean_object* x_5; lean_object* x_6; 
-x_5 = lean_ctor_get(x_1, 1);
-lean_inc(x_5);
-lean_dec(x_1);
-x_6 = lean_apply_3(x_5, lean_box(0), x_3, x_4);
-return x_6;
-}
-}
-lean_object* l_MonadExcept_catch(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_MonadExcept_catch___rarg), 4, 0);
-return x_3;
-}
-}
 lean_object* l_MonadExceptOf_isMonadExcept___rarg(lean_object* x_1) {
 _start:
 {
@@ -2336,7 +2296,7 @@ x_3 = lean_alloc_closure((void*)(l_ExceptT_monadControl___rarg), 1, 0);
 return x_3;
 }
 }
-lean_object* l_finally___rarg___lambda__1(lean_object* x_1) {
+lean_object* l_tryFinally___rarg___lambda__1(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
@@ -2345,14 +2305,46 @@ lean_inc(x_2);
 return x_2;
 }
 }
-static lean_object* _init_l_finally___rarg___closed__1() {
+static lean_object* _init_l_tryFinally___rarg___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_finally___rarg___lambda__1___boxed), 1, 0);
+x_1 = lean_alloc_closure((void*)(l_tryFinally___rarg___lambda__1___boxed), 1, 0);
 return x_1;
 }
 }
+lean_object* l_tryFinally___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_5 = lean_ctor_get(x_2, 0);
+lean_inc(x_5);
+lean_dec(x_2);
+x_6 = lean_alloc_closure((void*)(l_ExceptT_Monad___rarg___lambda__8___boxed), 2, 1);
+lean_closure_set(x_6, 0, x_4);
+x_7 = lean_apply_4(x_1, lean_box(0), lean_box(0), x_3, x_6);
+x_8 = l_tryFinally___rarg___closed__1;
+x_9 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_8, x_7);
+return x_9;
+}
+}
+lean_object* l_tryFinally(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_tryFinally___rarg), 4, 0);
+return x_4;
+}
+}
+lean_object* l_tryFinally___rarg___lambda__1___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_tryFinally___rarg___lambda__1(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
 lean_object* l_finally___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@@ -2363,7 +2355,7 @@ lean_dec(x_2);
 x_6 = lean_alloc_closure((void*)(l_ExceptT_Monad___rarg___lambda__8___boxed), 2, 1);
 lean_closure_set(x_6, 0, x_4);
 x_7 = lean_apply_4(x_1, lean_box(0), lean_box(0), x_3, x_6);
-x_8 = l_finally___rarg___closed__1;
+x_8 = l_tryFinally___rarg___closed__1;
 x_9 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_8, x_7);
 return x_9;
 }
@@ -2376,15 +2368,6 @@ x_4 = lean_alloc_closure((void*)(l_finally___rarg), 4, 0);
 return x_4;
 }
 }
-lean_object* l_finally___rarg___lambda__1___boxed(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = l_finally___rarg___lambda__1(x_1);
-lean_dec(x_1);
-return x_2;
-}
-}
 lean_object* l_Id_finally___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
@@ -2805,8 +2788,8 @@ l_Except_MonadExceptOf___closed__2 = _init_l_Except_MonadExceptOf___closed__2();
 lean_mark_persistent(l_Except_MonadExceptOf___closed__2);
 l_Except_MonadExceptOf___closed__3 = _init_l_Except_MonadExceptOf___closed__3();
 lean_mark_persistent(l_Except_MonadExceptOf___closed__3);
-l_finally___rarg___closed__1 = _init_l_finally___rarg___closed__1();
-lean_mark_persistent(l_finally___rarg___closed__1);
+l_tryFinally___rarg___closed__1 = _init_l_tryFinally___rarg___closed__1();
+lean_mark_persistent(l_tryFinally___rarg___closed__1);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus
diff --git a/stage0/stdlib/Init/Control/Reader.c b/stage0/stdlib/Init/Control/Reader.c
index d226f79937..6dc1519bcd 100644
--- a/stage0/stdlib/Init/Control/Reader.c
+++ b/stage0/stdlib/Init/Control/Reader.c
@@ -15,7 +15,7 @@ extern "C" {
 #endif
 lean_object* l_MonadWithReaderOf_isMonadWithReader___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_withTheReader(lean_object*, lean_object*);
-lean_object* l_ReaderT_finally___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_ReaderT_tryFinally___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_lift(lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_MonadExceptOf___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_monadWithReaderOfTrans(lean_object*, lean_object*, lean_object*);
@@ -38,7 +38,6 @@ lean_object* l_Function_const___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_ReaderT_MonadReaderOf(lean_object*, lean_object*);
 lean_object* l_ReaderT_failure___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_withTheReader___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_ReaderT_finally(lean_object*, lean_object*);
 lean_object* l_ReaderT_monadControl(lean_object*, lean_object*);
 lean_object* l_ReaderT_bind(lean_object*, lean_object*);
 lean_object* l_ReaderT_read___rarg(lean_object*, lean_object*);
@@ -52,6 +51,7 @@ lean_object* l_ReaderT_MonadExceptOf(lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_Monad___rarg___lambda__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_monadControl___closed__1;
 lean_object* l_ReaderT_orelse(lean_object*, lean_object*);
+lean_object* l_ReaderT_tryFinally(lean_object*, lean_object*);
 lean_object* l_ReaderT_read(lean_object*, lean_object*);
 lean_object* l_monadWithReaderOfTrans___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_MonadReaderOf___rarg(lean_object*);
@@ -73,7 +73,6 @@ lean_object* l_monadReaderTrans(lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_inhabited(lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_inhabited___rarg(lean_object*, lean_object*);
 lean_object* l_ReaderT_adapt___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_ReaderT_finally___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_MonadFunctor___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_MonadExceptOf___rarg(lean_object*);
 lean_object* l_ReaderT_MonadExceptOf___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
@@ -92,6 +91,7 @@ lean_object* l_ReaderT_Monad___rarg___lambda__6(lean_object*, lean_object*, lean
 lean_object* l_monadReaderTrans___rarg(lean_object*, lean_object*);
 lean_object* l_ReaderT_Monad___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_pure___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_ReaderT_tryFinally___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_readThe___rarg(lean_object*);
 lean_object* l_ReaderT_inhabited___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
@@ -792,7 +792,7 @@ x_3 = l_ReaderT_monadControl___closed__2;
 return x_3;
 }
 }
-lean_object* l_ReaderT_finally___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+lean_object* l_ReaderT_tryFinally___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
 _start:
 {
 lean_object* x_8; lean_object* x_9; lean_object* x_10; 
@@ -805,19 +805,19 @@ x_10 = lean_apply_4(x_1, lean_box(0), lean_box(0), x_8, x_9);
 return x_10;
 }
 }
-lean_object* l_ReaderT_finally(lean_object* x_1, lean_object* x_2) {
+lean_object* l_ReaderT_tryFinally(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_ReaderT_finally___rarg___boxed), 7, 0);
+x_3 = lean_alloc_closure((void*)(l_ReaderT_tryFinally___rarg___boxed), 7, 0);
 return x_3;
 }
 }
-lean_object* l_ReaderT_finally___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+lean_object* l_ReaderT_tryFinally___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
 _start:
 {
 lean_object* x_8; 
-x_8 = l_ReaderT_finally___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
+x_8 = l_ReaderT_tryFinally___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
 lean_dec(x_2);
 return x_8;
 }
diff --git a/stage0/stdlib/Init/Control/State.c b/stage0/stdlib/Init/Control/State.c
index 3803ab88c2..85d3aff0d5 100644
--- a/stage0/stdlib/Init/Control/State.c
+++ b/stage0/stdlib/Init/Control/State.c
@@ -18,7 +18,6 @@ lean_object* l_StateT_failure___rarg___boxed(lean_object*, lean_object*, lean_ob
 lean_object* l_StateT_set(lean_object*, lean_object*);
 lean_object* l_monadStateOf_isMonadState___rarg(lean_object*);
 lean_object* l_StateT_run_x27(lean_object*, lean_object*);
-lean_object* l_StateT_finally___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_pure(lean_object*, lean_object*);
 lean_object* l_getModify___rarg___lambda__1(lean_object*, lean_object*);
 lean_object* l_StateT_orelse(lean_object*, lean_object*, lean_object*);
@@ -27,8 +26,10 @@ lean_object* l_StateT_MonadStateOf(lean_object*, lean_object*);
 lean_object* l_StateT_Monad(lean_object*, lean_object*);
 lean_object* l_StateT_failure___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_getModify___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_StateT_tryFinally___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_monadControl___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_modifyThe(lean_object*, lean_object*);
+lean_object* l_StateT_tryFinally(lean_object*, lean_object*);
 lean_object* l_monadStateOf_isMonadState(lean_object*, lean_object*);
 lean_object* l_StateT_MonadFunctor(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_Alternative(lean_object*, lean_object*);
@@ -44,23 +45,21 @@ lean_object* l_getThe___rarg(lean_object*);
 lean_object* l_StateT_MonadFunctor___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_set___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_monadControl___rarg(lean_object*);
+lean_object* l_StateT_tryFinally___rarg___lambda__2(lean_object*, lean_object*);
 lean_object* l_modifyThe___rarg___lambda__1(lean_object*, lean_object*);
 lean_object* l_StateT_monadControl___rarg___lambda__6(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_map___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_modify(lean_object*, lean_object*);
 lean_object* l_StateT_get___rarg(lean_object*, lean_object*);
-lean_object* l_StateT_finally___rarg___lambda__2(lean_object*, lean_object*);
 lean_object* l_StateT_adapt___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_Monad___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_lift___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_MonadExceptOf___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_monadControl___rarg___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_run(lean_object*, lean_object*, lean_object*);
-lean_object* l_StateT_finally___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_monadControl(lean_object*, lean_object*);
 lean_object* l_StateT_Monad___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_monadControl___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
-extern lean_object* l_finally___rarg___closed__1;
 lean_object* l_StateT_MonadLift___rarg(lean_object*);
 lean_object* l_monadStateTrans___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_monadStateOf_isMonadState___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
@@ -71,7 +70,6 @@ lean_object* l_StateT_Monad___rarg___lambda__7(lean_object*, lean_object*);
 lean_object* l_StateT_bind(lean_object*, lean_object*);
 lean_object* l_StateT_Monad___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_monadStateTrans(lean_object*, lean_object*, lean_object*);
-lean_object* l_StateT_finally(lean_object*, lean_object*);
 lean_object* l_StateT_monadControl___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_adapt___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_monadControl___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -91,6 +89,7 @@ lean_object* l_StateT_Alternative___rarg(lean_object*, lean_object*);
 lean_object* l_StateT_map(lean_object*, lean_object*);
 lean_object* l_modifyGetThe(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_map___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_StateT_tryFinally___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_orelse___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_monadControl___rarg___lambda__5(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_run_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -100,6 +99,7 @@ lean_object* l_StateT_Monad___rarg___lambda__4(lean_object*, lean_object*, lean_
 lean_object* l_StateT_run___rarg(lean_object*, lean_object*);
 lean_object* l_monadStateTrans___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_MonadFunctor___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_tryFinally___rarg___closed__1;
 lean_object* l_modifyGetThe___rarg(lean_object*, lean_object*);
 lean_object* l_modify___rarg(lean_object*, lean_object*);
 lean_object* l_StateT_lift___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
@@ -128,7 +128,7 @@ x_5 = lean_ctor_get(x_1, 0);
 lean_inc(x_5);
 lean_dec(x_1);
 x_6 = lean_apply_1(x_3, x_4);
-x_7 = l_finally___rarg___closed__1;
+x_7 = l_tryFinally___rarg___closed__1;
 x_8 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_7, x_6);
 return x_8;
 }
@@ -1307,7 +1307,7 @@ x_3 = lean_alloc_closure((void*)(l_StateT_monadControl___rarg), 1, 0);
 return x_3;
 }
 }
-lean_object* l_StateT_finally___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_StateT_tryFinally___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 if (lean_obj_tag(x_3) == 0)
@@ -1354,7 +1354,7 @@ return x_15;
 }
 }
 }
-lean_object* l_StateT_finally___rarg___lambda__2(lean_object* x_1, lean_object* x_2) {
+lean_object* l_StateT_tryFinally___rarg___lambda__2(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; uint8_t x_5; 
@@ -1451,7 +1451,7 @@ return x_28;
 }
 }
 }
-lean_object* l_StateT_finally___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+lean_object* l_StateT_tryFinally___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
 _start:
 {
 lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
@@ -1459,21 +1459,21 @@ x_8 = lean_ctor_get(x_2, 1);
 lean_inc(x_8);
 lean_inc(x_7);
 x_9 = lean_apply_1(x_5, x_7);
-x_10 = lean_alloc_closure((void*)(l_StateT_finally___rarg___lambda__1), 3, 2);
+x_10 = lean_alloc_closure((void*)(l_StateT_tryFinally___rarg___lambda__1), 3, 2);
 lean_closure_set(x_10, 0, x_6);
 lean_closure_set(x_10, 1, x_7);
 x_11 = lean_apply_4(x_1, lean_box(0), lean_box(0), x_9, x_10);
-x_12 = lean_alloc_closure((void*)(l_StateT_finally___rarg___lambda__2), 2, 1);
+x_12 = lean_alloc_closure((void*)(l_StateT_tryFinally___rarg___lambda__2), 2, 1);
 lean_closure_set(x_12, 0, x_2);
 x_13 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_11, x_12);
 return x_13;
 }
 }
-lean_object* l_StateT_finally(lean_object* x_1, lean_object* x_2) {
+lean_object* l_StateT_tryFinally(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_StateT_finally___rarg), 7, 0);
+x_3 = lean_alloc_closure((void*)(l_StateT_tryFinally___rarg), 7, 0);
 return x_3;
 }
 }
diff --git a/stage0/stdlib/Init/Control/StateRef.c b/stage0/stdlib/Init/Control/StateRef.c
index f4c2337c71..11d7cb3151 100644
--- a/stage0/stdlib/Init/Control/StateRef.c
+++ b/stage0/stdlib/Init/Control/StateRef.c
@@ -18,7 +18,7 @@ lean_object* l_StateRefT_x27_set(lean_object*, lean_object*, lean_object*, lean_
 lean_object* l_StateRefT_x27_run_x27(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateRefT_x27_set___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateRefT_x27_MonadStateOf(lean_object*, lean_object*, lean_object*);
-lean_object* l_ReaderT_finally___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_ReaderT_tryFinally___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateRefT_x27_MonadIO(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateRefT_x27_modifyGet___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateRefT_x27_Monad(lean_object*, lean_object*, lean_object*);
@@ -477,7 +477,7 @@ lean_object* l_StateRefT_finally___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_ReaderT_finally___rarg___boxed), 7, 2);
+x_3 = lean_alloc_closure((void*)(l_ReaderT_tryFinally___rarg___boxed), 7, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
 return x_3;
diff --git a/stage0/stdlib/Init/System/IO.c b/stage0/stdlib/Init/System/IO.c
index c746dd83f1..999979446c 100644
--- a/stage0/stdlib/Init/System/IO.c
+++ b/stage0/stdlib/Init/System/IO.c
@@ -241,7 +241,6 @@ uint32_t l_IO_AccessRight_flags___closed__11;
 lean_object* l_IO_setStdin___at_IO_FS_withIsolatedStreams___spec__9(lean_object*, lean_object*);
 lean_object* l_IO_FS_Handle_read(lean_object*);
 lean_object* lean_io_has_finished(lean_object*, lean_object*);
-extern lean_object* l_finally___rarg___closed__1;
 lean_object* l_String_dropRight(lean_object*, lean_object*);
 lean_object* l_EIO_catchExceptions(lean_object*, lean_object*);
 lean_object* l_IO_setAccessRights___boxed(lean_object*, lean_object*, lean_object*);
@@ -381,6 +380,7 @@ lean_object* l_EIO_catchExceptions_match__1(lean_object*, lean_object*, lean_obj
 uint8_t l_IO_AccessRight_execution___default;
 lean_object* l_IO_Prim_fopenFlags___closed__2;
 lean_object* l_IO_withStdout___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_tryFinally___rarg___closed__1;
 lean_object* l_IO_FS_Handle_getLine___at_IO_Process_output___spec__4(lean_object*, lean_object*);
 lean_object* lean_uint32_to_nat(uint32_t);
 uint32_t l_IO_AccessRight_flags___closed__5;
@@ -2296,7 +2296,7 @@ lean_dec(x_7);
 x_11 = lean_alloc_closure((void*)(l_dbgTraceVal___rarg___lambda__1___boxed), 2, 1);
 lean_closure_set(x_11, 0, x_9);
 x_12 = lean_apply_4(x_3, lean_box(0), lean_box(0), x_4, x_11);
-x_13 = l_finally___rarg___closed__1;
+x_13 = l_tryFinally___rarg___closed__1;
 x_14 = lean_apply_4(x_10, lean_box(0), lean_box(0), x_13, x_12);
 return x_14;
 }
@@ -2345,7 +2345,7 @@ lean_dec(x_7);
 x_11 = lean_alloc_closure((void*)(l_dbgTraceVal___rarg___lambda__1___boxed), 2, 1);
 lean_closure_set(x_11, 0, x_9);
 x_12 = lean_apply_4(x_3, lean_box(0), lean_box(0), x_4, x_11);
-x_13 = l_finally___rarg___closed__1;
+x_13 = l_tryFinally___rarg___closed__1;
 x_14 = lean_apply_4(x_10, lean_box(0), lean_box(0), x_13, x_12);
 return x_14;
 }
@@ -2394,7 +2394,7 @@ lean_dec(x_7);
 x_11 = lean_alloc_closure((void*)(l_dbgTraceVal___rarg___lambda__1___boxed), 2, 1);
 lean_closure_set(x_11, 0, x_9);
 x_12 = lean_apply_4(x_3, lean_box(0), lean_box(0), x_4, x_11);
-x_13 = l_finally___rarg___closed__1;
+x_13 = l_tryFinally___rarg___closed__1;
 x_14 = lean_apply_4(x_10, lean_box(0), lean_box(0), x_13, x_12);
 return x_14;
 }
diff --git a/stage0/stdlib/Lean/CoreM.c b/stage0/stdlib/Lean/CoreM.c
index aa156affe0..6d56176e4a 100644
--- a/stage0/stdlib/Lean/CoreM.c
+++ b/stage0/stdlib/Lean/CoreM.c
@@ -2593,15 +2593,13 @@ lean_object* l_Lean_catchInternalId___rarg(lean_object* x_1, lean_object* x_2, l
 _start:
 {
 lean_object* x_5; lean_object* x_6; lean_object* x_7; 
-lean_inc(x_1);
-x_5 = lean_alloc_closure((void*)(l_Lean_catchInternalId___rarg___lambda__1___boxed), 4, 3);
-lean_closure_set(x_5, 0, x_1);
-lean_closure_set(x_5, 1, x_2);
-lean_closure_set(x_5, 2, x_4);
-x_6 = lean_ctor_get(x_1, 1);
-lean_inc(x_6);
-lean_dec(x_1);
-x_7 = lean_apply_3(x_6, lean_box(0), x_3, x_5);
+x_5 = lean_ctor_get(x_1, 1);
+lean_inc(x_5);
+x_6 = lean_alloc_closure((void*)(l_Lean_catchInternalId___rarg___lambda__1___boxed), 4, 3);
+lean_closure_set(x_6, 0, x_1);
+lean_closure_set(x_6, 1, x_2);
+lean_closure_set(x_6, 2, x_4);
+x_7 = lean_apply_3(x_5, lean_box(0), x_3, x_6);
 return x_7;
 }
 }
@@ -2739,15 +2737,13 @@ lean_object* l_Lean_catchInternalIds___rarg(lean_object* x_1, lean_object* x_2,
 _start:
 {
 lean_object* x_5; lean_object* x_6; lean_object* x_7; 
-lean_inc(x_1);
-x_5 = lean_alloc_closure((void*)(l_Lean_catchInternalIds___rarg___lambda__1___boxed), 4, 3);
-lean_closure_set(x_5, 0, x_1);
-lean_closure_set(x_5, 1, x_2);
-lean_closure_set(x_5, 2, x_4);
-x_6 = lean_ctor_get(x_1, 1);
-lean_inc(x_6);
-lean_dec(x_1);
-x_7 = lean_apply_3(x_6, lean_box(0), x_3, x_5);
+x_5 = lean_ctor_get(x_1, 1);
+lean_inc(x_5);
+x_6 = lean_alloc_closure((void*)(l_Lean_catchInternalIds___rarg___lambda__1___boxed), 4, 3);
+lean_closure_set(x_6, 0, x_1);
+lean_closure_set(x_6, 1, x_2);
+lean_closure_set(x_6, 2, x_4);
+x_7 = lean_apply_3(x_5, lean_box(0), x_3, x_6);
 return x_7;
 }
 }
diff --git a/stage0/stdlib/Lean/Elab/Do.c b/stage0/stdlib/Lean/Elab/Do.c
index 76cf5bbadf..f887eea36f 100644
--- a/stage0/stdlib/Lean/Elab/Do.c
+++ b/stage0/stdlib/Lean/Elab/Do.c
@@ -1064,7 +1064,6 @@ lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Do_ToTerm_mkJoinPointCo
 lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTermCore___closed__6;
 lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_mkIdBindFor___closed__3;
 lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode_match__1(lean_object*);
-lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__7;
 lean_object* l_Lean_Elab_Term_Do_mkFreshJP_x27(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_mkJmp___spec__6___rarg(lean_object*);
 lean_object* l_Lean_Elab_Term_Do_ToTerm_declToTermCore_match__1(lean_object*);
@@ -39082,7 +39081,7 @@ static lean_object* _init_l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("«finally»");
+x_1 = lean_mk_string("tryFinally");
 return x_1;
 }
 }
@@ -39112,9 +39111,11 @@ return x_4;
 static lean_object* _init_l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__4() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("finally");
-return x_1;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
 }
 }
 static lean_object* _init_l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__5() {
@@ -39123,7 +39124,9 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
 x_2 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__4;
-x_3 = lean_name_mk_string(x_1, x_2);
+x_3 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_3, 0, x_2);
+lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
@@ -39133,18 +39136,6 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
 x_2 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__5;
-x_3 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_3, 0, x_2);
-lean_ctor_set(x_3, 1, x_1);
-return x_3;
-}
-}
-static lean_object* _init_l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__7() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = lean_box(0);
-x_2 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__6;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
@@ -39337,11 +39328,11 @@ if (x_19 == 0)
 {
 lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; 
 x_20 = lean_ctor_get(x_18, 0);
-x_21 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__5;
+x_21 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__4;
 x_22 = l_Lean_addMacroScope(x_20, x_21, x_16);
 x_23 = l_Lean_Init_LeanInit___instance__8___closed__1;
 x_24 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__3;
-x_25 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__7;
+x_25 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__6;
 x_26 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_26, 0, x_23);
 lean_ctor_set(x_26, 1, x_24);
@@ -39371,11 +39362,11 @@ x_37 = lean_ctor_get(x_18, 1);
 lean_inc(x_37);
 lean_inc(x_36);
 lean_dec(x_18);
-x_38 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__5;
+x_38 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__4;
 x_39 = l_Lean_addMacroScope(x_36, x_38, x_16);
 x_40 = l_Lean_Init_LeanInit___instance__8___closed__1;
 x_41 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__3;
-x_42 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__7;
+x_42 = l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__6;
 x_43 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_43, 0, x_40);
 lean_ctor_set(x_43, 1, x_41);
@@ -46255,8 +46246,6 @@ l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__5 = _init_l_Le
 lean_mark_persistent(l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__5);
 l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__6 = _init_l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__6();
 lean_mark_persistent(l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__6);
-l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__7 = _init_l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__7();
-lean_mark_persistent(l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__2___closed__7);
 l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__3___closed__1 = _init_l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__3___closed__1();
 lean_mark_persistent(l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__3___closed__1);
 l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__3___closed__2 = _init_l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__3___closed__2();
diff --git a/stage0/stdlib/Lean/MonadEnv.c b/stage0/stdlib/Lean/MonadEnv.c
index 3e102bda28..989804b07d 100644
--- a/stage0/stdlib/Lean/MonadEnv.c
+++ b/stage0/stdlib/Lean/MonadEnv.c
@@ -82,7 +82,6 @@ lean_object* l_Lean_matchConstInduct(lean_object*);
 lean_object* l_Lean_getConstInfo(lean_object*);
 extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__3;
 lean_object* l_Lean_addDecl(lean_object*);
-extern lean_object* l_finally___rarg___closed__1;
 lean_object* l_Lean_withoutModifyingEnv___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_getConstInfoCtor___rarg___lambda__1___closed__1;
 lean_object* l_Lean_ofExcept___at_Lean_evalConst___spec__1(lean_object*);
@@ -123,6 +122,7 @@ lean_object* l_Lean_matchConst___rarg___lambda__1(lean_object*, lean_object*, le
 lean_object* l_Lean_addDecl_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_getConstInfoCtor(lean_object*);
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
+extern lean_object* l_tryFinally___rarg___closed__1;
 lean_object* l_Lean_matchConstCtor(lean_object*);
 lean_object* l_Lean_matchConstCtor___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_getConstInfoRec___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -167,7 +167,7 @@ lean_dec(x_7);
 x_10 = lean_alloc_closure((void*)(l_fix1___rarg___lambda__1___boxed), 2, 1);
 lean_closure_set(x_10, 0, x_8);
 x_11 = lean_apply_4(x_3, lean_box(0), lean_box(0), x_4, x_10);
-x_12 = l_finally___rarg___closed__1;
+x_12 = l_tryFinally___rarg___closed__1;
 x_13 = lean_apply_4(x_9, lean_box(0), lean_box(0), x_12, x_11);
 return x_13;
 }
diff --git a/stage0/stdlib/Lean/Util/MonadCache.c b/stage0/stdlib/Lean/Util/MonadCache.c
index 5cdd5f1184..679a71a26d 100644
--- a/stage0/stdlib/Lean/Util/MonadCache.c
+++ b/stage0/stdlib/Lean/Util/MonadCache.c
@@ -17,8 +17,8 @@ lean_object* l_Lean_MonadCacheT_run___boxed(lean_object*, lean_object*, lean_obj
 lean_object* l_Lean_MonadCacheT_Lean_Util_MonadCache___instance__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_checkCache___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MonadCacheT_Lean_Util_MonadCache___instance__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_ReaderT_finally___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MonadCacheT_Lean_Util_MonadCache___instance__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_ReaderT_tryFinally___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MonadCacheT_Lean_Util_MonadCache___instance__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MonadCacheT_run(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Lean_Util_MonadCache___instance__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
@@ -686,7 +686,7 @@ lean_object* l_Lean_MonadCacheT_Lean_Util_MonadCache___instance__10___rarg(lean_
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_ReaderT_finally___rarg___boxed), 7, 2);
+x_3 = lean_alloc_closure((void*)(l_ReaderT_tryFinally___rarg___boxed), 7, 2);
 lean_closure_set(x_3, 0, x_2);
 lean_closure_set(x_3, 1, x_1);
 return x_3;
diff --git a/stage0/stdlib/Lean/Util/Trace.c b/stage0/stdlib/Lean/Util/Trace.c
index b9297ec6e5..8ac80fa8b0 100644
--- a/stage0/stdlib/Lean/Util/Trace.c
+++ b/stage0/stdlib/Lean/Util/Trace.c
@@ -160,7 +160,6 @@ lean_object* l_Lean_addTrace___rarg___lambda__3(lean_object*, lean_object*, lean
 lean_object* l_Lean_modifyTraces___rarg___lambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_MonadTracer_trace___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_954____closed__9;
-extern lean_object* l_finally___rarg___closed__1;
 lean_object* l_Lean___kind_term____x40_Lean_Util_Trace___hyg_890____closed__11;
 lean_object* l_Lean_addTrace___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_of_nat(lean_object*);
@@ -273,6 +272,7 @@ lean_object* l_Lean_traceCtx___rarg___lambda__3(lean_object*, uint8_t, lean_obje
 lean_object* l_Array_forMAux___main___at_Lean_printTraces___spec__6(lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_withNestedTraces___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_checkTraceOption___closed__2;
+extern lean_object* l_tryFinally___rarg___closed__1;
 lean_object* l_Lean___kind_term____x40_Lean_Util_Trace___hyg_1236____closed__2;
 lean_object* l_Array_iterateMAux___main___at_Lean_withNestedTraces___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_954____closed__10;
@@ -2070,7 +2070,7 @@ lean_dec(x_9);
 x_14 = lean_alloc_closure((void*)(l_fix1___rarg___lambda__1___boxed), 2, 1);
 lean_closure_set(x_14, 0, x_12);
 x_15 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_6, x_14);
-x_16 = l_finally___rarg___closed__1;
+x_16 = l_tryFinally___rarg___closed__1;
 x_17 = lean_apply_4(x_13, lean_box(0), lean_box(0), x_16, x_15);
 return x_17;
 }
@@ -2092,7 +2092,7 @@ lean_dec(x_9);
 x_12 = lean_alloc_closure((void*)(l_fix1___rarg___lambda__1___boxed), 2, 1);
 lean_closure_set(x_12, 0, x_10);
 x_13 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_6, x_12);
-x_14 = l_finally___rarg___closed__1;
+x_14 = l_tryFinally___rarg___closed__1;
 x_15 = lean_apply_4(x_11, lean_box(0), lean_box(0), x_14, x_13);
 return x_15;
 }
@@ -3756,7 +3756,7 @@ lean_dec(x_8);
 x_12 = lean_alloc_closure((void*)(l_fix1___rarg___lambda__1___boxed), 2, 1);
 lean_closure_set(x_12, 0, x_10);
 x_13 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_5, x_12);
-x_14 = l_finally___rarg___closed__1;
+x_14 = l_tryFinally___rarg___closed__1;
 x_15 = lean_apply_4(x_11, lean_box(0), lean_box(0), x_14, x_13);
 return x_15;
 }
diff --git a/stage0/stdlib/Std/ShareCommon.c b/stage0/stdlib/Std/ShareCommon.c
index aad7d31af4..57f33c3af9 100644
--- a/stage0/stdlib/Std/ShareCommon.c
+++ b/stage0/stdlib/Std/ShareCommon.c
@@ -99,7 +99,6 @@ lean_object* l_Std_PShareCommonM_run(lean_object*);
 size_t l_USize_mul(size_t, size_t);
 lean_object* l_Std_PersistentHashMap_findEntry_x3f___at_Std_ShareCommon_ObjectPersistentSet_find_x3f___spec__1___boxed(lean_object*, lean_object*);
 lean_object* lean_object_pmap_insert(lean_object*, lean_object*, lean_object*);
-extern lean_object* l_finally___rarg___closed__1;
 lean_object* l_Std_ShareCommon_mkObjectSet___closed__1;
 lean_object* l_Std_ShareCommonT_withShareCommon___at_Std_shareCommon___spec__1(lean_object*);
 lean_object* l_Std_shareCommon___rarg(lean_object*);
@@ -156,6 +155,7 @@ lean_object* l_Std_ShareCommonT_monadShareCommon___rarg(lean_object*);
 lean_object* l_List_replace___main___at_Std_ShareCommon_ObjectSet_insert___spec__6___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_ShareCommonT_run___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_HashMapImp_find_x3f___at_Std_ShareCommon_ObjectMap_find_x3f___spec__1___boxed(lean_object*, lean_object*);
+extern lean_object* l_tryFinally___rarg___closed__1;
 lean_object* l_Std_ShareCommon_Object_ptrHash___boxed(lean_object*);
 lean_object* l_Std_withShareCommon___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -2868,7 +2868,7 @@ lean_inc(x_6);
 lean_dec(x_5);
 x_7 = l_Std_ShareCommon_State_empty;
 x_8 = lean_apply_1(x_3, x_7);
-x_9 = l_finally___rarg___closed__1;
+x_9 = l_tryFinally___rarg___closed__1;
 x_10 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_9, x_8);
 return x_10;
 }
@@ -2896,7 +2896,7 @@ lean_inc(x_6);
 lean_dec(x_5);
 x_7 = l_Std_ShareCommon_PersistentState_empty;
 x_8 = lean_apply_1(x_3, x_7);
-x_9 = l_finally___rarg___closed__1;
+x_9 = l_tryFinally___rarg___closed__1;
 x_10 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_9, x_8);
 return x_10;
 }