merge master

src/Init/Tactics.lean

@@ -398,7 +398,7 @@ syntax locationWildcard := " *"
 A hypothesis location specification consists of 1 or more hypothesis references
 and optionally `⊢` denoting the goal.
 -/
-syntax locationHyp := (ppSpace colGt term:max)+ patternIgnore(ppSpace (atomic("|" noWs "-") <|> "⊢"))?
+syntax locationHyp := (ppSpace colGt term:max)+ ppSpace patternIgnore( atomic("|" noWs "-") <|> "⊢")?
 
 /--
 Location specifications are used by many tactics that can operate on either the
@@ -894,37 +894,6 @@ The tactic `nomatch h` is shorthand for `exact nomatch h`.
 macro "nomatch " es:term,+ : tactic =>
   `(tactic| exact nomatch $es:term,*)
 
-/--
-Acts like `have`, but removes a hypothesis with the same name as
-this one if possible. For example, if the state is:
-
-```lean
-f : α → β
-h : α
-⊢ goal
-```
-
-Then after `replace h := f h` the state will be:
-
-```lean
-f : α → β
-h : β
-⊢ goal
-```
-
-whereas `have h := f h` would result in:
-
-```lean
-f : α → β
-h† : α
-h : β
-⊢ goal
-```
-
-This can be used to simulate the `specialize` and `apply at` tactics of Coq.
--/
-syntax (name := replace) "replace" haveDecl : tactic
-
 /--
 `repeat' tac` runs `tac` on all of the goals to produce a new list of goals,
 then runs `tac` again on all of those goals, and repeats until `tac` fails on all remaining goals.

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -25,13 +25,9 @@ def leanMainFn := "_lean_main"
 
 namespace LLVM
 -- TODO(bollu): instantiate target triple and find out what size_t is.
-def size_tType (llvmctx : LLVM.Context) : BaseIO (LLVM.LLVMType llvmctx) :=
+def size_tType (llvmctx : LLVM.Context) : IO (LLVM.LLVMType llvmctx) :=
   LLVM.i64Type llvmctx
 
--- TODO(bollu): instantiate target triple and find out what unsigned is.
-def unsignedType (llvmctx : LLVM.Context) : BaseIO (LLVM.LLVMType llvmctx) :=
-  LLVM.i32Type llvmctx
-
 -- Helper to add a function if it does not exist, and to return the function handle if it does.
 def getOrAddFunction (m : LLVM.Module ctx) (name : String) (type : LLVM.LLVMType ctx) : BaseIO (LLVM.Value ctx) :=  do
   match (← LLVM.getNamedFunction m name) with
@@ -100,15 +96,6 @@ def getDecl (n : Name) : M llvmctx Decl := do
   | some d => pure d
   | none   => throw s!"unknown declaration {n}"
 
-def constInt8 (n : Nat) : M llvmctx (LLVM.Value llvmctx) :=  do
-    LLVM.constInt8 llvmctx (UInt64.ofNat n)
-
-def constInt64 (n : Nat) : M llvmctx (LLVM.Value llvmctx) :=  do
-    LLVM.constInt64 llvmctx (UInt64.ofNat n)
-
-def constIntSizeT (n : Nat) : M llvmctx (LLVM.Value llvmctx) :=  do
-    LLVM.constIntSizeT llvmctx (UInt64.ofNat n)
-
 def constIntUnsigned (n : Nat) : M llvmctx (LLVM.Value llvmctx) :=  do
     LLVM.constIntUnsigned llvmctx (UInt64.ofNat n)
 
@@ -175,14 +162,14 @@ def callLeanUnsignedToNatFn (builder : LLVM.Builder llvmctx)
   let retty ← LLVM.voidPtrType llvmctx
   let f ←   getOrCreateFunctionPrototype mod retty "lean_unsigned_to_nat"  argtys
   let fnty ← LLVM.functionType retty argtys
-  let nv ← constIntUnsigned n
+  let nv ← LLVM.constInt32 llvmctx (UInt64.ofNat n)
   LLVM.buildCall2 builder fnty f #[nv] name
 
 def callLeanMkStringFromBytesFn (builder : LLVM.Builder llvmctx)
     (strPtr nBytes : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
   let fnName :=  "lean_mk_string_from_bytes"
   let retty ← LLVM.voidPtrType llvmctx
-  let argtys :=  #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
+  let argtys :=  #[← LLVM.voidPtrType llvmctx, ← LLVM.i64Type llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   LLVM.buildCall2 builder fnty fn #[strPtr, nBytes] name
@@ -231,9 +218,9 @@ def callLeanAllocCtor (builder : LLVM.Builder llvmctx)
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
 
-  let tag ← constIntUnsigned tag
-  let num_objs ← constIntUnsigned num_objs
-  let scalar_sz ← constIntUnsigned scalar_sz
+  let tag ← LLVM.constInt32 llvmctx (UInt64.ofNat tag)
+  let num_objs ← LLVM.constInt32 llvmctx (UInt64.ofNat num_objs)
+  let scalar_sz ← LLVM.constInt32 llvmctx (UInt64.ofNat scalar_sz)
   LLVM.buildCall2 builder fnty fn #[tag, num_objs, scalar_sz] name
 
 def callLeanCtorSet (builder : LLVM.Builder llvmctx)
@@ -241,7 +228,7 @@ def callLeanCtorSet (builder : LLVM.Builder llvmctx)
   let fnName := "lean_ctor_set"
   let retty ← LLVM.voidType llvmctx
   let voidptr ← LLVM.voidPtrType llvmctx
-  let unsigned ← LLVM.unsignedType llvmctx
+  let unsigned ← LLVM.size_tType llvmctx
   let argtys :=  #[voidptr, unsigned, voidptr]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
@@ -261,7 +248,7 @@ def callLeanAllocClosureFn (builder : LLVM.Builder llvmctx)
     (f arity nys : LLVM.Value llvmctx) (retName : String := "") : M llvmctx (LLVM.Value llvmctx) := do
   let fnName :=  "lean_alloc_closure"
   let retty ← LLVM.voidPtrType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.unsignedType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   LLVM.buildCall2 builder fnty fn  #[f, arity, nys] retName
@@ -270,7 +257,7 @@ def callLeanClosureSetFn (builder : LLVM.Builder llvmctx)
     (closure ix arg : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do
   let fnName :=  "lean_closure_set"
   let retty ← LLVM.voidType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.voidPtrType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.voidPtrType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   let _ ← LLVM.buildCall2 builder fnty fn  #[closure, ix, arg] retName
@@ -298,7 +285,7 @@ def callLeanCtorRelease (builder : LLVM.Builder llvmctx)
     (closure i : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do
   let fnName :=  "lean_ctor_release"
   let retty ← LLVM.voidType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   let _ ← LLVM.buildCall2 builder fnty fn  #[closure, i] retName
@@ -307,7 +294,7 @@ def callLeanCtorSetTag (builder : LLVM.Builder llvmctx)
     (closure i : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do
   let fnName :=  "lean_ctor_set_tag"
   let retty ← LLVM.voidType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.i8Type llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   let _ ← LLVM.buildCall2 builder fnty fn  #[closure, i] retName
@@ -360,31 +347,6 @@ def builderAppendBasicBlock (builder : LLVM.Builder llvmctx) (name : String) : M
   let fn ← builderGetInsertionFn builder
   LLVM.appendBasicBlockInContext llvmctx fn name
 
-/--
-Add an alloca to the first BB of the current function. The builders final position
-will be the end of the BB that we came from.
-
-If it is possible to put an alloca in the first BB this approach is to be preferred
-over putting it in other BBs. This is because mem2reg only inspects allocas in the first BB,
-leading to missed optimizations for allocas in other BBs.
--/
-def buildPrologueAlloca (builder : LLVM.Builder llvmctx) (ty : LLVM.LLVMType llvmctx) (name : @&String := "") : M llvmctx (LLVM.Value llvmctx) := do
-  let origBB ← LLVM.getInsertBlock builder
-
-  let fn ← builderGetInsertionFn builder
-  if (← LLVM.countBasicBlocks fn) == 0 then
-    throw "Attempt to obtain first BB of function without BBs"
-
-  let entryBB ← LLVM.getEntryBasicBlock fn
-  match ← LLVM.getFirstInstruction entryBB with
-  | some instr => LLVM.positionBuilderBefore builder instr
-  | none => LLVM.positionBuilderAtEnd builder entryBB
-
-  let alloca ← LLVM.buildAlloca builder ty name
-  LLVM.positionBuilderAtEnd builder origBB
-  return alloca
-
-
 def buildWhile_ (builder : LLVM.Builder llvmctx) (name : String)
     (condcodegen : LLVM.Builder llvmctx → M llvmctx (LLVM.Value llvmctx))
     (bodycodegen : LLVM.Builder llvmctx → M llvmctx Unit) : M llvmctx Unit := do
@@ -466,7 +428,7 @@ def buildIfThenElse_ (builder : LLVM.Builder llvmctx)  (name : String) (brval :
 -- Recall that lean uses `i8` for booleans, not `i1`, so we need to compare with `true`.
 def buildLeanBoolTrue? (builder : LLVM.Builder llvmctx)
     (b : LLVM.Value llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx) := do
-  LLVM.buildICmp builder LLVM.IntPredicate.NE b (← constInt8 0) name
+  LLVM.buildICmp builder LLVM.IntPredicate.NE b (← LLVM.constInt8 llvmctx 0) name
 
 def emitFnDeclAux (mod : LLVM.Module llvmctx)
     (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M llvmctx (LLVM.Value llvmctx) := do
@@ -551,8 +513,8 @@ def emitArgSlot_ (builder : LLVM.Builder llvmctx)
   | Arg.var x => emitLhsSlot_ x
   | _ => do
     let slotty ← LLVM.voidPtrType llvmctx
-    let slot ← buildPrologueAlloca builder slotty "irrelevant_slot"
-    let v ← callLeanBox builder (← constIntSizeT 0) "irrelevant_val"
+    let slot ← LLVM.buildAlloca builder slotty "irrelevant_slot"
+    let v ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "irrelevant_val"
     let _ ← LLVM.buildStore builder v slot
     return (slotty, slot)
 
@@ -574,7 +536,7 @@ def emitCtorSetArgs (builder : LLVM.Builder llvmctx)
   ys.size.forM fun i => do
     let zv ← emitLhsVal builder z
     let (_yty, yv) ← emitArgVal builder ys[i]!
-    let iv ← constIntUnsigned i
+    let iv ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat i)
     callLeanCtorSet builder zv iv yv
     emitLhsSlotStore builder z zv
     pure ()
@@ -583,7 +545,7 @@ def emitCtor (builder : LLVM.Builder llvmctx)
     (z : VarId) (c : CtorInfo) (ys : Array Arg) : M llvmctx Unit := do
   let (_llvmty, slot) ← emitLhsSlot_ z
   if c.size == 0 && c.usize == 0 && c.ssize == 0 then do
-    let v ← callLeanBox builder (← constIntSizeT c.cidx) "lean_box_outv"
+    let v ← callLeanBox builder (← constIntUnsigned c.cidx) "lean_box_outv"
     let _ ← LLVM.buildStore builder v slot
   else do
     let v ← emitAllocCtor builder c
@@ -595,7 +557,7 @@ def emitInc (builder : LLVM.Builder llvmctx)
   let xv ← emitLhsVal builder x
   if n != 1
   then do
-     let nv ← constIntSizeT n
+     let nv ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat n)
      callLeanRefcountFn builder (kind := RefcountKind.inc) (checkRef? := checkRef?) (delta := nv) xv
   else callLeanRefcountFn builder (kind := RefcountKind.inc) (checkRef? := checkRef?) xv
 
@@ -709,7 +671,7 @@ def emitPartialApp (builder : LLVM.Builder llvmctx) (z : VarId) (f : FunId) (ys
 
 def emitApp (builder : LLVM.Builder llvmctx) (z : VarId) (f : VarId) (ys : Array Arg) : M llvmctx Unit := do
   if ys.size > closureMaxArgs then do
-    let aargs ← buildPrologueAlloca builder (← LLVM.arrayType (← LLVM.voidPtrType llvmctx) (UInt64.ofNat ys.size)) "aargs"
+    let aargs ← LLVM.buildAlloca builder (← LLVM.arrayType (← LLVM.voidPtrType llvmctx) (UInt64.ofNat ys.size)) "aargs"
     for i in List.range ys.size do
       let (yty, yv) ← emitArgVal builder ys[i]!
       let aslot ← LLVM.buildInBoundsGEP2 builder yty aargs #[← constIntUnsigned 0, ← constIntUnsigned i] s!"param_{i}_slot"
@@ -718,7 +680,7 @@ def emitApp (builder : LLVM.Builder llvmctx) (z : VarId) (f : VarId) (ys : Array
     let retty ← LLVM.voidPtrType llvmctx
     let args := #[← emitLhsVal builder f, ← constIntUnsigned ys.size, aargs]
     -- '1 + ...'. '1' for the fn and 'args' for the arguments
-    let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.voidPtrType llvmctx]
+    let argtys := #[← LLVM.voidPtrType llvmctx]
     let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
     let fnty ← LLVM.functionType retty argtys
     let zv ← LLVM.buildCall2 builder fnty fn args
@@ -760,18 +722,18 @@ def emitFullApp (builder : LLVM.Builder llvmctx)
 def emitLit (builder : LLVM.Builder llvmctx)
     (z : VarId) (t : IRType) (v : LitVal) : M llvmctx (LLVM.Value llvmctx) := do
   let llvmty ← toLLVMType t
-  let zslot ← buildPrologueAlloca builder llvmty
+  let zslot ← LLVM.buildAlloca builder llvmty
   addVartoState z zslot llvmty
   let zv ← match v with
             | LitVal.num v => emitNumLit builder t v
             | LitVal.str v =>
-                 let zero ← constIntUnsigned 0
+                 let zero ← LLVM.constIntUnsigned llvmctx 0
                  let str_global ← LLVM.buildGlobalString builder v
                  -- access through the global, into the 0th index of the array
                  let strPtr ← LLVM.buildInBoundsGEP2 builder
                                 (← LLVM.opaquePointerTypeInContext llvmctx)
                                 str_global #[zero] ""
-                 let nbytes ← constIntSizeT v.utf8ByteSize
+                 let nbytes ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat (v.utf8ByteSize))
                  callLeanMkStringFromBytesFn builder strPtr nbytes ""
   LLVM.buildStore builder zv zslot
   return zslot
@@ -795,7 +757,7 @@ def callLeanCtorGetUsize (builder : LLVM.Builder llvmctx)
     (x i : LLVM.Value llvmctx) (retName : String) : M llvmctx (LLVM.Value llvmctx) := do
   let fnName :=  "lean_ctor_get_usize"
   let retty ← LLVM.size_tType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fnty ← LLVM.functionType retty argtys
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   LLVM.buildCall2 builder fnty fn  #[x, i] retName
@@ -822,7 +784,7 @@ def emitSProj (builder : LLVM.Builder llvmctx)
     | IRType.uint32 => pure ("lean_ctor_get_uint32", ← LLVM.i32Type llvmctx)
     | IRType.uint64 => pure ("lean_ctor_get_uint64", ← LLVM.i64Type llvmctx)
     | _             => throw s!"Invalid type for lean_ctor_get: '{t}'"
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let xval ← emitLhsVal builder x
   let offset ← emitOffset builder n offset
@@ -929,7 +891,7 @@ def emitReset (builder : LLVM.Builder llvmctx) (z : VarId) (n : Nat) (x : VarId)
    (fun builder => do
       let xv ← emitLhsVal builder x
       callLeanDecRef builder xv
-      let box0 ← callLeanBox builder (← constIntSizeT 0) "box0"
+      let box0 ← callLeanBox builder (← constIntUnsigned 0) "box0"
       emitLhsSlotStore builder z box0
       return ShouldForwardControlFlow.yes
    )
@@ -950,7 +912,7 @@ def emitReuse (builder : LLVM.Builder llvmctx)
        emitLhsSlotStore builder z xv
        if updtHeader then
           let zv ← emitLhsVal builder z
-          callLeanCtorSetTag builder zv (← constInt8 c.cidx)
+          callLeanCtorSetTag builder zv (← constIntUnsigned c.cidx)
        return ShouldForwardControlFlow.yes
    )
   emitCtorSetArgs builder z ys
@@ -973,7 +935,7 @@ def emitVDecl (builder : LLVM.Builder llvmctx) (z : VarId) (t : IRType) (v : Exp
 
 def declareVar (builder : LLVM.Builder llvmctx) (x : VarId) (t : IRType) : M llvmctx Unit := do
   let llvmty ← toLLVMType t
-  let alloca ← buildPrologueAlloca builder llvmty "varx"
+  let alloca ← LLVM.buildAlloca builder llvmty "varx"
   addVartoState x alloca llvmty
 
 partial def declareVars (builder : LLVM.Builder llvmctx) (f : FnBody) : M llvmctx Unit := do
@@ -999,7 +961,7 @@ def emitTag (builder : LLVM.Builder llvmctx) (x : VarId) (xType : IRType) : M ll
 def emitSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : Arg) : M llvmctx Unit := do
   let fnName :=  "lean_ctor_set"
   let retty ← LLVM.voidType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx , ← LLVM.voidPtrType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.voidPtrType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   let _ ← LLVM.buildCall2 builder fnty fn  #[← emitLhsVal builder x, ← constIntUnsigned i, (← emitArgVal builder y).2]
@@ -1007,7 +969,7 @@ def emitSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : Arg) : M
 def emitUSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : VarId) : M llvmctx Unit := do
   let fnName :=  "lean_ctor_set_usize"
   let retty ← LLVM.voidType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.size_tType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   let _ ← LLVM.buildCall2 builder fnty fn  #[← emitLhsVal builder x, ← constIntUnsigned i, (← emitLhsVal builder y)]
@@ -1046,7 +1008,7 @@ def emitSSet (builder : LLVM.Builder llvmctx) (x : VarId) (n : Nat) (offset : Na
   | IRType.uint32 => pure ("lean_ctor_set_uint32", ← LLVM.i32Type llvmctx)
   | IRType.uint64 => pure ("lean_ctor_set_uint64", ← LLVM.i64Type llvmctx)
   | _             => throw s!"invalid type for 'lean_ctor_set': '{t}'"
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, setty]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, setty]
   let retty  ← LLVM.voidType llvmctx
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let xv ← emitLhsVal builder x
@@ -1064,12 +1026,12 @@ def emitDel (builder : LLVM.Builder llvmctx) (x : VarId) : M llvmctx Unit := do
   let _ ← LLVM.buildCall2 builder fnty fn  #[xv]
 
 def emitSetTag (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) : M llvmctx Unit := do
-  let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.i8Type llvmctx]
+  let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let retty  ← LLVM.voidType llvmctx
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty "lean_ctor_set_tag" argtys
   let xv ← emitLhsVal builder x
   let fnty ← LLVM.functionType retty argtys
-  let _ ← LLVM.buildCall2 builder fnty fn  #[xv, ← constInt8 i]
+  let _ ← LLVM.buildCall2 builder fnty fn  #[xv, ← constIntUnsigned i]
 
 def ensureHasDefault' (alts : Array Alt) : Array Alt :=
   if alts.any Alt.isDefault then alts
@@ -1095,7 +1057,7 @@ partial def emitCase (builder : LLVM.Builder llvmctx)
     match alt with
     | Alt.ctor c b  =>
        let destbb ← builderAppendBasicBlock builder s!"case_{xType}_{c.name}_{c.cidx}"
-       LLVM.addCase switch (← constIntSizeT c.cidx) destbb
+       LLVM.addCase switch (← constIntUnsigned c.cidx) destbb
        LLVM.positionBuilderAtEnd builder destbb
        emitFnBody builder b
     | Alt.default b =>
@@ -1179,14 +1141,14 @@ def emitFnArgs (builder : LLVM.Builder llvmctx)
           -- pv := *(argsi) = *(args + i)
           let pv ← LLVM.buildLoad2 builder llvmty argsi
           -- slot for arg[i] which is always void* ?
-          let alloca ← buildPrologueAlloca builder llvmty s!"arg_{i}"
+          let alloca ← LLVM.buildAlloca builder llvmty s!"arg_{i}"
           LLVM.buildStore builder pv alloca
           addVartoState params[i]!.x alloca llvmty
   else
       let n ← LLVM.countParams llvmfn
       for i in (List.range n.toNat) do
         let llvmty ← toLLVMType params[i]!.ty
-        let alloca ← buildPrologueAlloca builder  llvmty s!"arg_{i}"
+        let alloca ← LLVM.buildAlloca builder  llvmty s!"arg_{i}"
         let arg ← LLVM.getParam llvmfn (UInt64.ofNat i)
         let _ ← LLVM.buildStore builder arg alloca
         addVartoState params[i]!.x alloca llvmty
@@ -1338,7 +1300,7 @@ def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
   let ginit?v ← LLVM.buildLoad2 builder ginit?ty ginit?slot "init_v"
   buildIfThen_ builder "isGInitialized" ginit?v
     (fun builder => do
-      let box0 ← callLeanBox builder (← constIntSizeT 0) "box0"
+      let box0 ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "box0"
       let out ← callLeanIOResultMKOk builder box0 "retval"
       let _ ← LLVM.buildRet builder out
       pure ShouldForwardControlFlow.no)
@@ -1356,7 +1318,7 @@ def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
     callLeanDecRef builder res
   let decls := getDecls env
   decls.reverse.forM (emitDeclInit builder initFn)
-  let box0 ← callLeanBox builder (← constIntSizeT 0) "box0"
+  let box0 ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "box0"
   let out ← callLeanIOResultMKOk builder box0 "retval"
   let _ ← LLVM.buildRet builder out
 
@@ -1470,15 +1432,15 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
   #endif
   -/
   let inty ← LLVM.voidPtrType llvmctx
-  let inslot ← buildPrologueAlloca builder (← LLVM.pointerType inty) "in"
+  let inslot ← LLVM.buildAlloca builder (← LLVM.pointerType inty) "in"
   let resty ← LLVM.voidPtrType llvmctx
-  let res ← buildPrologueAlloca builder (← LLVM.pointerType resty) "res"
+  let res ← LLVM.buildAlloca builder (← LLVM.pointerType resty) "res"
   if usesLeanAPI then callLeanInitialize builder else callLeanInitializeRuntimeModule builder
     /- We disable panic messages because they do not mesh well with extracted closed terms.
         See issue #534. We can remove this workaround after we implement issue #467. -/
   callLeanSetPanicMessages builder (← LLVM.constFalse llvmctx)
   let world ← callLeanIOMkWorld builder
-  let resv ← callModInitFn builder (← getModName) (← constInt8 1) world ((← getModName).toString ++ "_init_out")
+  let resv ← callModInitFn builder (← getModName) (← LLVM.constInt8 llvmctx 1) world ((← getModName).toString ++ "_init_out")
   let _ ← LLVM.buildStore builder resv res
 
   callLeanSetPanicMessages builder (← LLVM.constTrue llvmctx)
@@ -1491,21 +1453,21 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
       callLeanDecRef builder resv
       callLeanInitTaskManager builder
       if xs.size == 2 then
-        let inv ← callLeanBox builder (← constIntSizeT 0) "inv"
+        let inv ← callLeanBox builder (← LLVM.constInt (← LLVM.size_tType llvmctx) 0) "inv"
         let _ ← LLVM.buildStore builder inv inslot
         let ity ← LLVM.size_tType llvmctx
-        let islot ← buildPrologueAlloca builder ity "islot"
+        let islot ← LLVM.buildAlloca builder ity "islot"
         let argcval ← LLVM.getParam main 0
         let argvval ← LLVM.getParam main 1
         LLVM.buildStore builder argcval islot
         buildWhile_ builder "argv"
           (condcodegen := fun builder => do
             let iv ← LLVM.buildLoad2 builder ity islot "iv"
-            let i_gt_1 ← LLVM.buildICmp builder LLVM.IntPredicate.UGT iv (← constIntSizeT 1) "i_gt_1"
+            let i_gt_1 ← LLVM.buildICmp builder LLVM.IntPredicate.UGT iv (← constIntUnsigned 1) "i_gt_1"
             return i_gt_1)
           (bodycodegen := fun builder => do
             let iv ← LLVM.buildLoad2 builder ity islot "iv"
-            let iv_next ← LLVM.buildSub builder iv (← constIntSizeT 1) "iv.next"
+            let iv_next ← LLVM.buildSub builder iv (← constIntUnsigned 1) "iv.next"
             LLVM.buildStore builder iv_next islot
             let nv ← callLeanAllocCtor builder 1 2 0 "nv"
             let argv_i_next_slot ← LLVM.buildGEP2 builder (← LLVM.voidPtrType llvmctx) argvval #[iv_next] "argv.i.next.slot"
@@ -1547,7 +1509,7 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
         pure ShouldForwardControlFlow.no
       else do
         callLeanDecRef builder resv
-        let _ ← LLVM.buildRet builder (← constInt64 0)
+        let _ ← LLVM.buildRet builder (← LLVM.constInt64 llvmctx 0)
         pure ShouldForwardControlFlow.no
 
     )
@@ -1555,7 +1517,7 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
         let resv ← LLVM.buildLoad2 builder resty res "resv"
         callLeanIOResultShowError builder resv
         callLeanDecRef builder resv
-        let _ ← LLVM.buildRet builder (← constInt64 1)
+        let _ ← LLVM.buildRet builder (← LLVM.constInt64 llvmctx 1)
         pure ShouldForwardControlFlow.no)
   -- at the merge
   let _ ← LLVM.buildUnreachable builder
@@ -1630,8 +1592,6 @@ def emitLLVM (env : Environment) (modName : Name) (filepath : String) : IO Unit
            let some fn ← LLVM.getNamedFunction emitLLVMCtx.llvmmodule name
               | throw <| IO.Error.userError s!"ERROR: linked module must have function from runtime module: '{name}'"
            LLVM.setLinkage fn LLVM.Linkage.internal
-         if let some err ← LLVM.verifyModule emitLLVMCtx.llvmmodule then
-           throw <| .userError err
          LLVM.writeBitcodeToFile emitLLVMCtx.llvmmodule filepath
          LLVM.disposeModule emitLLVMCtx.llvmmodule
   | .error err => throw (IO.Error.userError err)

src/Lean/Compiler/IR/LLVMBindings.lean

@@ -182,18 +182,6 @@ opaque createBuilderInContext (ctx : Context) : BaseIO (Builder ctx)
 @[extern "lean_llvm_append_basic_block_in_context"]
 opaque appendBasicBlockInContext (ctx : Context) (fn :  Value ctx) (name :  @&String) : BaseIO (BasicBlock ctx)
 
-@[extern "lean_llvm_count_basic_blocks"]
-opaque countBasicBlocks (fn : Value ctx) : BaseIO UInt64
-
-@[extern "lean_llvm_get_entry_basic_block"]
-opaque getEntryBasicBlock (fn : Value ctx) : BaseIO (BasicBlock ctx)
-
-@[extern "lean_llvm_get_first_instruction"]
-opaque getFirstInstruction (bb : BasicBlock ctx) : BaseIO (Option (Value ctx))
-
-@[extern "lean_llvm_position_builder_before"]
-opaque positionBuilderBefore (builder : Builder ctx) (instr : Value ctx) : BaseIO Unit
-
 @[extern "lean_llvm_position_builder_at_end"]
 opaque positionBuilderAtEnd (builder : Builder ctx) (bb :  BasicBlock ctx) : BaseIO Unit
 
@@ -338,9 +326,6 @@ opaque disposeTargetMachine (tm : TargetMachine ctx) : BaseIO Unit
 @[extern "lean_llvm_dispose_module"]
 opaque disposeModule (m : Module ctx) : BaseIO Unit
 
-@[extern "lean_llvm_verify_module"]
-opaque verifyModule (m : Module ctx) : BaseIO (Option String)
-
 @[extern "lean_llvm_create_string_attribute"]
 opaque createStringAttribute (key : String) (value : String) : BaseIO (Attribute ctx)
 
@@ -454,11 +439,6 @@ def constInt32 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : B
 def constInt64 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) :=
   constInt' ctx 64 value signExtend
 
-def constIntSizeT (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) :=
-  -- TODO: make this stick to the actual size_t of the target machine
-  constInt' ctx 64 value signExtend
-
 def constIntUnsigned (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) :=
-  -- TODO: make this stick to the actual unsigned of the target machine
-  constInt' ctx 32 value signExtend
+  constInt' ctx 64 value signExtend
 end LLVM

src/Lean/Elab/BuiltinCommand.lean

@@ -656,40 +656,35 @@ unsafe def elabEvalUnsafe : CommandElab
         return e
     -- Evaluate using term using `MetaEval` class.
     let elabMetaEval : CommandElabM Unit := do
-      -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
-      -- we don't polute the environment with auxliary declarations.
-      -- We have special support for `CommandElabM` to ensure `#eval` can be used to execute commands
-      -- that modify `CommandElabM` state not just the `Environment`.
-      let act : Sum (CommandElabM Unit) (Environment → Options → IO (String × Except IO.Error Environment)) ←
-        runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do
-          let e ← elabEvalTerm
-          let eType ← instantiateMVars (← inferType e)
-          if eType.isAppOfArity ``CommandElabM 1 then
-            let mut stx ← Term.exprToSyntax e
-            unless (← isDefEq eType.appArg! (mkConst ``Unit)) do
-              stx ← `($stx >>= fun v => IO.println (repr v))
-            let act ← Lean.Elab.Term.evalTerm (CommandElabM Unit) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) stx
-            pure <| Sum.inl act
-          else
-            let e ← mkRunMetaEval e
-            addAndCompile e
-            let act ← evalConst (Environment → Options → IO (String × Except IO.Error Environment)) declName
-            pure <| Sum.inr act
-      match act with
-      | .inl act => act
-      | .inr act =>
-        let (out, res) ← act (← getEnv) (← getOptions)
-        logInfoAt tk out
-        match res with
-        | Except.error e => throwError e.toString
-        | Except.ok env  => setEnv env; pure ()
+      -- act? is `some act` if elaborated `term` has type `CommandElabM α`
+      let act? ← runTermElabM fun _ => Term.withDeclName declName do
+        let e ← elabEvalTerm
+        let eType ← instantiateMVars (← inferType e)
+        if eType.isAppOfArity ``CommandElabM 1 then
+          let mut stx ← Term.exprToSyntax e
+          unless (← isDefEq eType.appArg! (mkConst ``Unit)) do
+            stx ← `($stx >>= fun v => IO.println (repr v))
+          let act ← Lean.Elab.Term.evalTerm (CommandElabM Unit) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) stx
+          pure <| some act
+        else
+          let e ← mkRunMetaEval e
+          let env ← getEnv
+          let opts ← getOptions
+          let act ← try addAndCompile e; evalConst (Environment → Options → IO (String × Except IO.Error Environment)) declName finally setEnv env
+          let (out, res) ← act env opts -- we execute `act` using the environment
+          logInfoAt tk out
+          match res with
+          | Except.error e => throwError e.toString
+          | Except.ok env  => do setEnv env; pure none
+      let some act := act? | return ()
+      act
     -- Evaluate using term using `Eval` class.
-    let elabEval : CommandElabM Unit := runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do
+    let elabEval : CommandElabM Unit := runTermElabM fun _ => Term.withDeclName declName do
       -- fall back to non-meta eval if MetaEval hasn't been defined yet
       -- modify e to `runEval e`
       let e ← mkRunEval (← elabEvalTerm)
-      addAndCompile e
-      let act ← evalConst (IO (String × Except IO.Error Unit)) declName
+      let env ← getEnv
+      let act ← try addAndCompile e; evalConst (IO (String × Except IO.Error Unit)) declName finally setEnv env
       let (out, res) ← liftM (m := IO) act
       logInfoAt tk out
       match res with

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -12,7 +12,6 @@ import Lean.Elab.Open
 import Lean.Elab.SetOption
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
-import Lean.Elab.Do
 
 namespace Lean.Elab.Tactic
 open Meta
@@ -482,18 +481,4 @@ where
 @[builtin_tactic right] def evalRight : Tactic := fun _stx => do
   liftMetaTactic (fun g => g.nthConstructor `right 1 (some 2))
 
-@[builtin_tactic replace] def evalReplace : Tactic := fun stx => do
-  match stx with
-  | `(tactic| replace $decl:haveDecl) =>
-    withMainContext do
-      let vars ← Elab.Term.Do.getDoHaveVars <| mkNullNode #[.missing, decl]
-      let origLCtx ← getLCtx
-      evalTactic $ ← `(tactic| have $decl:haveDecl)
-      let mut toClear := #[]
-      for fv in vars do
-        if let some ldecl := origLCtx.findFromUserName? fv.getId then
-          toClear := toClear.push ldecl.fvarId
-      liftMetaTactic1 (·.tryClearMany toClear)
-  | _ => throwUnsupportedSyntax
-
 end Lean.Elab.Tactic

src/Lean/Meta/Tactic.lean

@@ -22,7 +22,6 @@ import Lean.Meta.Tactic.Simp
 import Lean.Meta.Tactic.AuxLemma
 import Lean.Meta.Tactic.SplitIf
 import Lean.Meta.Tactic.Split
-import Lean.Meta.Tactic.TryThis
 import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Unfold
 import Lean.Meta.Tactic.Rename

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -12,13 +12,9 @@ import Lean.Meta.Tactic.Simp.SimpCongrTheorems
 namespace Lean.Meta
 namespace Simp
 
-/-- The result of simplifying some expression `e`. -/
 structure Result where
-  /-- The simplified version of `e` -/ 
   expr           : Expr
-  /-- A proof that `$e = $expr`, where the simplified expression is on the RHS.
-  If `none`, the proof is assumed to be `refl`. -/
-  proof?         : Option Expr := none
+  proof?         : Option Expr := none -- If none, proof is assumed to be `refl`
   /-- Save the field `dischargeDepth` at `Simp.Context` because it impacts the simplifier result. -/
   dischargeDepth : UInt32 := 0
   /-- If `cache := true` the result is cached. -/

src/Lean/Meta/Tactic/TryThis.lean

@@ -1,585 +0,0 @@
-/-
-Copyright (c) 2021 Gabriel Ebner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Mario Carneiro, Thomas Murrills
--/
-import Lean.Server.CodeActions
-import Lean.Widget.UserWidget
-import Lean.Data.Json.Elab
-
-/-- Gets the LSP range from a `String.Range`. -/
-def Lean.FileMap.utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
-  { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
-
-
-/-!
-# "Try this" support
-
-This implements a mechanism for tactics to print a message saying `Try this: <suggestion>`,
-where `<suggestion>` is a link to a replacement tactic. Users can either click on the link
-in the suggestion (provided by a widget), or use a code action which applies the suggestion.
--/
-namespace Lean.Meta.Tactic.TryThis
-
-open Lean Elab PrettyPrinter Meta Server RequestM
-
-/-! # Raw widget -/
-
-/--
-This is a widget which is placed by `TryThis.addSuggestion` and `TryThis.addSuggestions`.
-
-When placed by `addSuggestion`, it says `Try this: <replacement>`
-where `<replacement>` is a link which will perform the replacement.
-
-When placed by `addSuggestions`, it says:
-```
-Try these:
-```
-* `<replacement1>`
-* `<replacement2>`
-* `<replacement3>`
-* ...
-
-where `<replacement*>` is a link which will perform the replacement.
--/
-@[widget_module] def tryThisWidget : Widget.Module where
-  javascript := "
-import * as React from 'react';
-import { EditorContext } from '@leanprover/infoview';
-const e = React.createElement;
-export default function ({ pos, suggestions, range, header, isInline, style }) {
-  const editorConnection = React.useContext(EditorContext)
-  const defStyle = style || {
-    className: 'link pointer dim',
-    style: { color: 'var(--vscode-textLink-foreground)' }
-  }
-
-  // Construct the children of the HTML element for a given suggestion.
-  function makeSuggestion({ suggestion, preInfo, postInfo, style }) {
-    function onClick() {
-      editorConnection.api.applyEdit({
-        changes: { [pos.uri]: [{ range, newText: suggestion }] }
-      })
-    }
-    return [
-      preInfo,
-      e('span', { onClick, title: 'Apply suggestion', ...style || defStyle }, suggestion),
-      postInfo
-    ]
-  }
-
-  // Choose between an inline 'Try this'-like display and a list-based 'Try these'-like display.
-  let inner = null
-  if (isInline) {
-    inner = e('div', { className: 'ml1' },
-      e('pre', { className: 'font-code pre-wrap' }, header, makeSuggestion(suggestions[0])))
-  } else {
-    inner = e('div', { className: 'ml1' },
-      e('pre', { className: 'font-code pre-wrap' }, header),
-      e('ul', { style: { paddingInlineStart: '20px' } }, suggestions.map(s =>
-        e('li', { className: 'font-code pre-wrap' }, makeSuggestion(s)))))
-  }
-  return e('details', { open: true },
-    e('summary', { className: 'mv2 pointer' }, 'Suggestions'),
-    inner)
-}"
-
-/-! # Code action -/
-
-/-- A packet of information about a "Try this" suggestion
-that we store in the infotree for the associated code action to retrieve. -/
-structure TryThisInfo : Type where
-  /-- The textual range to be replaced by one of the suggestions. -/
-  range : Lsp.Range
-  /--
-  A list of suggestions for the user to choose from.
-  Each suggestion may optionally come with an override for the code action title.
-  -/
-  suggestionTexts : Array (String × Option String)
-  /-- The prefix to display before the code action for a "Try this" suggestion if no custom code
-  action title is provided. If not provided, `"Try this: "` is used. -/
-  codeActionPrefix? : Option String
-  deriving TypeName
-
-/--
-This is a code action provider that looks for `TryThisInfo` nodes and supplies a code action to
-apply the replacement.
--/
-@[code_action_provider] def tryThisProvider : CodeActionProvider := fun params snap => do
-  let doc ← readDoc
-  pure <| snap.infoTree.foldInfo (init := #[]) fun _ctx info result => Id.run do
-    let .ofCustomInfo { stx, value } := info | result
-    let some { range, suggestionTexts, codeActionPrefix? } :=
-      value.get? TryThisInfo | result
-    let some stxRange := stx.getRange? | result
-    let stxRange := doc.meta.text.utf8RangeToLspRange stxRange
-    unless stxRange.start.line ≤ params.range.end.line do return result
-    unless params.range.start.line ≤ stxRange.end.line do return result
-    let mut result := result
-    for h : i in [:suggestionTexts.size] do
-      let (newText, title?) := suggestionTexts[i]'h.2
-      let title := title?.getD <| (codeActionPrefix?.getD "Try this: ") ++ newText
-      result := result.push {
-        eager.title := title
-        eager.kind? := "quickfix"
-        -- Only make the first option preferred
-        eager.isPreferred? := if i = 0 then true else none
-        eager.edit? := some <| .ofTextEdit doc.versionedIdentifier { range, newText }
-      }
-    result
-
-/-! # Formatting -/
-
-/-- Yields `(indent, column)` given a `FileMap` and a `String.Range`, where `indent` is the number
-of spaces by which the line that first includes `range` is initially indented, and `column` is the
-column `range` starts at in that line. -/
-def getIndentAndColumn (map : FileMap) (range : String.Range) : Nat × Nat :=
-  let start := map.source.findLineStart range.start
-  let body := map.source.findAux (· ≠ ' ') range.start start
-  ((body - start).1, (range.start - start).1)
-
-/-- Replace subexpressions like `?m.1234` with `?_` so it can be copy-pasted. -/
-partial def replaceMVarsByUnderscores [Monad m] [MonadQuotation m]
-    (s : Syntax) : m Syntax :=
-  s.replaceM fun s => do
-    let `(?$id:ident) := s | pure none
-    if id.getId.hasNum || id.getId.isInternal then `(?_) else pure none
-
-/-- Delaborate `e` into syntax suitable for use by `refine`. -/
-def delabToRefinableSyntax (e : Expr) : MetaM Term :=
-  return ⟨← replaceMVarsByUnderscores (← delab e)⟩
-
-/--
-An option allowing the user to customize the ideal input width. Defaults to 100.
-This option controls output format when
-the output is intended to be copied back into a lean file -/
-register_option format.inputWidth : Nat := {
-  /- The default maximum width of an ideal line in source code. -/
-  defValue := 100
-  descr := "ideal input width"
-}
-
-/-- Get the input width specified in the options -/
-def getInputWidth (o : Options) : Nat := format.inputWidth.get o
-
-/-! # `Suggestion` data -/
-
--- TODO: we could also support `Syntax` and `Format`
-/-- Text to be used as a suggested replacement in the infoview. This can be either a `TSyntax kind`
-for a single `kind : SyntaxNodeKind` or a raw `String`.
-
-Instead of using constructors directly, there are coercions available from these types to
-`SuggestionText`. -/
-inductive SuggestionText where
-  /-- `TSyntax kind` used as suggested replacement text in the infoview. Note that while `TSyntax`
-  is in general parameterized by a list of `SyntaxNodeKind`s, we only allow one here; this
-  unambiguously guides pretty-printing. -/
-  | tsyntax {kind : SyntaxNodeKind} : TSyntax kind → SuggestionText
-  /-- A raw string to be used as suggested replacement text in the infoview. -/
-  | string : String → SuggestionText
-  deriving Inhabited
-
-instance : ToMessageData SuggestionText where
-  toMessageData
-  | .tsyntax stx => stx
-  | .string s => s
-
-instance {kind : SyntaxNodeKind} : CoeHead (TSyntax kind) SuggestionText where
-  coe := .tsyntax
-
-instance : Coe String SuggestionText where
-  coe := .string
-
-namespace SuggestionText
-
-/-- Pretty-prints a `SuggestionText` as a `Format`. If the `SuggestionText` is some `TSyntax kind`,
-we use the appropriate pretty-printer; strings are coerced to `Format`s as-is. -/
-def pretty : SuggestionText → CoreM Format
-  | .tsyntax (kind := kind) stx => ppCategory kind stx
-  | .string text => return text
-
-/- Note that this is essentially `return (← s.pretty).prettyExtra w indent column`, but we
-special-case strings to avoid converting them to `Format`s and back, which adds indentation after each newline. -/
-/-- Pretty-prints a `SuggestionText` as a `String` and wraps with respect to the pane width,
-indentation, and column, via `Format.prettyExtra`. If `w := none`, then
-`w := getInputWidth (← getOptions)` is used. Raw `String`s are returned as-is. -/
-def prettyExtra (s : SuggestionText) (w : Option Nat := none)
-    (indent column : Nat := 0) : CoreM String :=
-  match s with
-  | .tsyntax (kind := kind) stx => do
-    let w ← match w with | none => do pure <| getInputWidth (← getOptions) | some n => pure n
-    return (← ppCategory kind stx).pretty w indent column
-  | .string text => return text
-
-end SuggestionText
-
-/--
-Style hooks for `Suggestion`s. See `SuggestionStyle.error`, `.warning`, `.success`, `.value`,
-and other definitions here for style presets. This is an arbitrary `Json` object, with the following
-interesting fields:
-* `title`: the hover text in the suggestion link
-* `className`: the CSS classes applied to the link
-* `style`: A `Json` object with additional inline CSS styles such as `color` or `textDecoration`.
--/
-def SuggestionStyle := Json deriving Inhabited, ToJson
-
-/-- Style as an error. By default, decorates the text with an undersquiggle; providing the argument
-`decorated := false` turns this off. -/
-def SuggestionStyle.error (decorated := true) : SuggestionStyle :=
-  let style := if decorated then
-    json% {
-      -- The VS code error foreground theme color (`--vscode-errorForeground`).
-      color: "var(--vscode-errorForeground)",
-      textDecoration: "underline wavy var(--vscode-editorError-foreground) 1pt"
-    }
-  else json% { color: "var(--vscode-errorForeground)" }
-  json% { className: "pointer dim", style: $style }
-
-/-- Style as a warning. By default, decorates the text with an undersquiggle; providing the
-argument `decorated := false` turns this off. -/
-def SuggestionStyle.warning (decorated := true) : SuggestionStyle :=
-  if decorated then
-    json% {
-      -- The `.gold` CSS class, which the infoview uses when e.g. building a file.
-      className: "gold pointer dim",
-      style: { textDecoration: "underline wavy var(--vscode-editorWarning-foreground) 1pt" }
-    }
-  else json% { className: "gold pointer dim" }
-
-/-- Style as a success. -/
-def SuggestionStyle.success : SuggestionStyle :=
-  -- The `.information` CSS class, which the infoview uses on successes.
-  json% { className: "information pointer dim" }
-
-/-- Style the same way as a hypothesis appearing in the infoview. -/
-def SuggestionStyle.asHypothesis : SuggestionStyle :=
-  json% { className: "goal-hyp pointer dim" }
-
-/-- Style the same way as an inaccessible hypothesis appearing in the infoview. -/
-def SuggestionStyle.asInaccessible : SuggestionStyle :=
-  json% { className: "goal-inaccessible pointer dim" }
-
-/-- Draws the color from a red-yellow-green color gradient with red at `0.0`, yellow at `0.5`, and
-green at `1.0`. Values outside the range `[0.0, 1.0]` are clipped to lie within this range.
-
-With `showValueInHoverText := true` (the default), the value `t` will be included in the `title` of
-the HTML element (which appears on hover). -/
-def SuggestionStyle.value (t : Float) (showValueInHoverText := true) : SuggestionStyle :=
-  let t := min (max t 0) 1
-  json% {
-    className: "pointer dim",
-    -- interpolates linearly from 0º to 120º with 95% saturation and lightness
-    -- varying around 50% in HSL space
-    style: { color: $(s!"hsl({(t * 120).round} 95% {60 * ((t - 0.5)^2 + 0.75)}%)") },
-    title: $(if showValueInHoverText then s!"Apply suggestion ({t})" else "Apply suggestion")
-  }
-
-/-- Holds a `suggestion` for replacement, along with `preInfo` and `postInfo` strings to be printed
-immediately before and after that suggestion, respectively. It also includes an optional
-`MessageData` to represent the suggestion in logs; by default, this is `none`, and `suggestion` is
-used. -/
-structure Suggestion where
-  /-- Text to be used as a replacement via a code action. -/
-  suggestion : SuggestionText
-  /-- Optional info to be printed immediately before replacement text in a widget. -/
-  preInfo? : Option String := none
-  /-- Optional info to be printed immediately after replacement text in a widget. -/
-  postInfo? : Option String := none
-  /-- Optional style specification for the suggestion. If `none` (the default), the suggestion is
-  styled as a text link. Otherwise, the suggestion can be styled as:
-  * a status: `.error`, `.warning`, `.success`
-  * a hypothesis name: `.asHypothesis`, `.asInaccessible`
-  * a variable color: `.value (t : Float)`, which draws from a red-yellow-green gradient, with red
-  at `0.0` and green at `1.0`.
-
-  See `SuggestionStyle` for details. -/
-  style? : Option SuggestionStyle := none
-  /-- How to represent the suggestion as `MessageData`. This is used only in the info diagnostic.
-  If `none`, we use `suggestion`. Use `toMessageData` to render a `Suggestion` in this manner. -/
-  messageData? : Option MessageData := none
-  /-- How to construct the text that appears in the lightbulb menu from the suggestion text. If
-  `none`, we use `fun ppSuggestionText => "Try this: " ++ ppSuggestionText`. Only the pretty-printed
-  `suggestion : SuggestionText` is used here. -/
-  toCodeActionTitle? : Option (String → String) := none
-  deriving Inhabited
-
-/-- Converts a `Suggestion` to `Json` in `CoreM`. We need `CoreM` in order to pretty-print syntax.
-
-This also returns a `String × Option String` consisting of the pretty-printed text and any custom
-code action title if `toCodeActionTitle?` is provided.
-
-If `w := none`, then `w := getInputWidth (← getOptions)` is used.
--/
-def Suggestion.toJsonAndInfoM (s : Suggestion) (w : Option Nat := none) (indent column : Nat := 0) :
-    CoreM (Json × String × Option String) := do
-  let text ← s.suggestion.prettyExtra w indent column
-  let mut json := [("suggestion", (text : Json))]
-  if let some preInfo := s.preInfo? then json := ("preInfo", preInfo) :: json
-  if let some postInfo := s.postInfo? then json := ("postInfo", postInfo) :: json
-  if let some style := s.style? then json := ("style", toJson style) :: json
-  return (Json.mkObj json, text, s.toCodeActionTitle?.map (· text))
-
-/- If `messageData?` is specified, we use that; otherwise (by default), we use `toMessageData` of
-the suggestion text. -/
-instance : ToMessageData Suggestion where
-  toMessageData s := s.messageData?.getD (toMessageData s.suggestion)
-
-instance : Coe SuggestionText Suggestion where
-  coe t := { suggestion := t }
-
-/-- Delaborate `e` into a suggestion suitable for use by `refine`. -/
-def delabToRefinableSuggestion (e : Expr) : MetaM Suggestion :=
-  return { suggestion := ← delabToRefinableSyntax e, messageData? := e }
-
-/-! # Widget hooks -/
-
-/-- Core of `addSuggestion` and `addSuggestions`. Whether we use an inline display for a single
-element or a list display is controlled by `isInline`. -/
-private def addSuggestionCore (ref : Syntax) (suggestions : Array Suggestion)
-    (header : String) (isInline : Bool) (origSpan? : Option Syntax := none)
-    (style? : Option SuggestionStyle := none)
-    (codeActionPrefix? : Option String := none) : CoreM Unit := do
-  if let some range := (origSpan?.getD ref).getRange? then
-    let map ← getFileMap
-    -- FIXME: this produces incorrect results when `by` is at the beginning of the line, i.e.
-    -- replacing `tac` in `by tac`, because the next line will only be 2 space indented
-    -- (less than `tac` which starts at column 3)
-    let (indent, column) := getIndentAndColumn map range
-    let suggestions ← suggestions.mapM (·.toJsonAndInfoM (indent := indent) (column := column))
-    let suggestionTexts := suggestions.map (·.2)
-    let suggestions := suggestions.map (·.1)
-    let ref := Syntax.ofRange <| ref.getRange?.getD range
-    let range := map.utf8RangeToLspRange range
-    pushInfoLeaf <| .ofCustomInfo {
-      stx := ref
-      value := Dynamic.mk
-        { range, suggestionTexts, codeActionPrefix? : TryThisInfo }
-    }
-    Widget.savePanelWidgetInfo (hash tryThisWidget.javascript) ref
-      (props := return json% {
-        suggestions: $suggestions,
-        range: $range,
-        header: $header,
-        isInline: $isInline,
-        style: $style?
-      })
-
-/-- Add a "try this" suggestion. This has three effects:
-
-* An info diagnostic is displayed saying `Try this: <suggestion>`
-* A widget is registered, saying `Try this: <suggestion>` with a link on `<suggestion>` to apply
-  the suggestion
-* A code action is added, which will apply the suggestion.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `s`: a `Suggestion`, which contains
-  * `suggestion`: the replacement text;
-  * `preInfo?`: an optional string shown immediately after the replacement text in the widget
-    message (only)
-  * `postInfo?`: an optional string shown immediately after the replacement text in the widget
-    message (only)
-  * `style?`: an optional `Json` object used as the value of the `style` attribute of the
-    suggestion text's element (not the whole suggestion element).
-  * `messageData?`: an optional message to display in place of `suggestion` in the info diagnostic
-    (only). The widget message uses only `suggestion`. If `messageData?` is `none`, we simply use
-    `suggestion` instead.
-  * `toCodeActionTitle?`: an optional function `String → String` describing how to transform the
-    pretty-printed suggestion text into the code action text which appears in the lightbulb menu.
-    If `none`, we simply prepend `"Try This: "` to the suggestion text.
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `header`: a string that begins the display. By default, it is `"Try this: "`.
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
-  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
--/
-def addSuggestion (ref : Syntax) (s : Suggestion) (origSpan? : Option Syntax := none)
-    (header : String := "Try this: ") (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  logInfoAt ref m!"{header}{s}"
-  addSuggestionCore ref #[s] header (isInline := true) origSpan?
-    (codeActionPrefix? := codeActionPrefix?)
-
-/-- Add a list of "try this" suggestions as a single "try these" suggestion. This has three effects:
-
-* An info diagnostic is displayed saying `Try these: <list of suggestions>`
-* A widget is registered, saying `Try these: <list of suggestions>` with a link on each
-  `<suggestion>` to apply the suggestion
-* A code action for each suggestion is added, which will apply the suggestion.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `suggestions`: an array of `Suggestion`s, which each contain
-  * `suggestion`: the replacement text;
-  * `preInfo?`: an optional string shown immediately after the replacement text in the widget
-    message (only)
-  * `postInfo?`: an optional string shown immediately after the replacement text in the widget
-    message (only)
-  * `style?`: an optional `Json` object used as the value of the `style` attribute of the
-    suggestion text's element (not the whole suggestion element).
-  * `messageData?`: an optional message to display in place of `suggestion` in the info diagnostic
-    (only). The widget message uses only `suggestion`. If `messageData?` is `none`, we simply use
-    `suggestion` instead.
-  * `toCodeActionTitle?`: an optional function `String → String` describing how to transform the
-    pretty-printed suggestion text into the code action text which appears in the lightbulb menu.
-    If `none`, we simply prepend `"Try This: "` to the suggestion text.
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `header`: a string that precedes the list. By default, it is `"Try these:"`.
-* `style?`: a default style for all suggestions which do not have a custom `style?` set.
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
-  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
-  used.
--/
-def addSuggestions (ref : Syntax) (suggestions : Array Suggestion)
-    (origSpan? : Option Syntax := none) (header : String := "Try these:")
-    (style? : Option SuggestionStyle := none)
-    (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  if suggestions.isEmpty then throwErrorAt ref "no suggestions available"
-  let msgs := suggestions.map toMessageData
-  let msgs := msgs.foldl (init := MessageData.nil) (fun msg m => msg ++ m!"\n• " ++ m)
-  logInfoAt ref m!"{header}{msgs}"
-  addSuggestionCore ref suggestions header (isInline := false) origSpan? style? codeActionPrefix?
-
-private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion := do
-  let stx ← delabToRefinableSyntax e
-  let mvars ← getMVars e
-  let suggestion ← if mvars.isEmpty then `(tactic| exact $stx) else `(tactic| refine $stx)
-  let messageData? := if mvars.isEmpty then m!"exact {e}" else m!"refine {e}"
-  let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else
-    let mut str := "\nRemaining subgoals:"
-    for g in mvars do
-      -- TODO: use a MessageData.ofExpr instead of rendering to string
-      let e ← PrettyPrinter.ppExpr (← instantiateMVars (← g.getType))
-      str := str ++ Format.pretty ("\n⊢ " ++ e)
-    pure str
-  pure { suggestion, postInfo?, messageData? }
-
-/-- Add an `exact e` or `refine e` suggestion.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `e`: the replacement expression
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after
-  `Remaining subgoals:`
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
-  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
--/
-def addExactSuggestion (ref : Syntax) (e : Expr)
-    (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
-    (codeActionPrefix? : Option String := none): MetaM Unit := do
-  addSuggestion ref (← addExactSuggestionCore addSubgoalsMsg e)
-    (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
-
-/-- Add `exact e` or `refine e` suggestions.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `es`: the array of replacement expressions
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after
-  `Remaining subgoals:`
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
-  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
-  used.
--/
-def addExactSuggestions (ref : Syntax) (es : Array Expr)
-    (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
-    (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  let suggestions ← es.mapM <| addExactSuggestionCore addSubgoalsMsg
-  addSuggestions ref suggestions (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
-
-/-- Add a term suggestion.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `e`: the replacement expression
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `header`: a string which precedes the suggestion. By default, it's `"Try this: "`.
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
-  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
--/
-def addTermSuggestion (ref : Syntax) (e : Expr)
-    (origSpan? : Option Syntax := none) (header : String := "Try this: ")
-    (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  addSuggestion ref (← delabToRefinableSuggestion e) (origSpan? := origSpan?) (header := header)
-    (codeActionPrefix? := codeActionPrefix?)
-
-/-- Add term suggestions.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `es`: an array of the replacement expressions
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `header`: a string which precedes the list of suggestions. By default, it's `"Try these:"`.
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
-  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
-  used.
--/
-def addTermSuggestions (ref : Syntax) (es : Array Expr)
-    (origSpan? : Option Syntax := none) (header : String := "Try these:")
-    (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  addSuggestions ref (← es.mapM delabToRefinableSuggestion)
-    (origSpan? := origSpan?) (header := header) (codeActionPrefix? := codeActionPrefix?)
-
-open Lean Elab Elab.Tactic PrettyPrinter Meta
-
-/-- Add a suggestion for `have h : t := e`. -/
-def addHaveSuggestion (ref : Syntax) (h? : Option Name) (t? : Option Expr) (e : Expr)
-    (origSpan? : Option Syntax := none) : TermElabM Unit := do
-  let estx ← delabToRefinableSyntax e
-  let prop ← isProp (← inferType e)
-  let tac ← if let some t := t? then
-    let tstx ← delabToRefinableSyntax t
-    if prop then
-      match h? with
-      | some h => `(tactic| have $(mkIdent h) : $tstx := $estx)
-      | none => `(tactic| have : $tstx := $estx)
-    else
-      `(tactic| let $(mkIdent (h?.getD `_)) : $tstx := $estx)
-  else
-    if prop then
-      match h? with
-      | some h => `(tactic| have $(mkIdent h) := $estx)
-      | none => `(tactic| have := $estx)
-    else
-      `(tactic| let $(mkIdent (h?.getD `_)) := $estx)
-  addSuggestion ref tac origSpan?
-
-open Lean.Parser.Tactic
-open Lean.Syntax
-
-/-- Add a suggestion for `rw [h₁, ← h₂] at loc`. -/
-def addRewriteSuggestion (ref : Syntax) (rules : List (Expr × Bool))
-  (type? : Option Expr := none) (loc? : Option Expr := none)
-  (origSpan? : Option Syntax := none) :
-    TermElabM Unit := do
-  let rules_stx := TSepArray.ofElems <| ← rules.toArray.mapM fun ⟨e, symm⟩ => do
-    let t ← delabToRefinableSyntax e
-    if symm then `(rwRule| ← $t:term) else `(rwRule| $t:term)
-  let tac ← do
-    let loc ← loc?.mapM fun loc => do `(location| at $(← delab loc):term)
-    `(tactic| rw [$rules_stx,*] $(loc)?)
-
-  -- We don't simply write `let mut tacMsg := m!"{tac}"` here
-  -- but instead rebuild it, so that there are embedded `Expr`s in the message,
-  -- thus giving more information in the hovers.
-  -- Perhaps in future we will have a better way to attach elaboration information to
-  -- `Syntax` embedded in a `MessageData`.
-  let mut tacMsg :=
-    let rulesMsg := MessageData.sbracket <| MessageData.joinSep
-      (rules.map fun ⟨e, symm⟩ => (if symm then "← " else "") ++ m!"{e}") ", "
-    if let some loc := loc? then
-      m!"rw {rulesMsg} at {loc}"
-    else
-      m!"rw {rulesMsg}"
-  let mut extraMsg := ""
-  if let some type := type? then
-    tacMsg := tacMsg ++ m!"\n-- {type}"
-    extraMsg := extraMsg ++ s!"\n-- {← PrettyPrinter.ppExpr type}"
-  addSuggestion ref (s := { suggestion := tac, postInfo? := extraMsg, messageData? := tacMsg })
-    origSpan?

src/library/compiler/llvm.cpp

@@ -18,7 +18,6 @@ Lean's IR.
 #include "runtime/string_ref.h"
 
 #ifdef LEAN_LLVM
-#include "llvm-c/Analysis.h"
 #include "llvm-c/BitReader.h"
 #include "llvm-c/BitWriter.h"
 #include "llvm-c/Core.h"
@@ -1425,74 +1424,3 @@ extern "C" LEAN_EXPORT lean_object *llvm_is_declaration(size_t ctx, size_t globa
 	return lean_io_result_mk_ok(lean_box(is_bool));
 #endif  // LEAN_LLVM
 }
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_verify_module(size_t ctx, size_t mod,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    char* msg = NULL;
-    LLVMBool broken = LLVMVerifyModule(lean_to_Module(mod), LLVMReturnStatusAction, &msg);
-    if (broken) {
-      return lean_io_result_mk_ok(lean::mk_option_some(lean_mk_string(msg)));
-    } else {
-      return lean_io_result_mk_ok(lean::mk_option_none());
-    }
-#endif  // LEAN_LLVM
-}
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_count_basic_blocks(size_t ctx, size_t fn_val,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMValueRef fn_ref = lean_to_Value(fn_val);
-    return lean_io_result_mk_ok(lean_box_uint64((uint64_t)LLVMCountBasicBlocks(fn_ref)));
-#endif  // LEAN_LLVM
-}
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_get_entry_basic_block(size_t ctx, size_t fn_val,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMValueRef fn_ref = lean_to_Value(fn_val);
-    LLVMBasicBlockRef bb_ref = LLVMGetEntryBasicBlock(fn_ref);
-    return lean_io_result_mk_ok(lean_box_usize(BasicBlock_to_lean(bb_ref)));
-#endif  // LEAN_LLVM
-}
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_get_first_instruction(size_t ctx, size_t bb,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMBasicBlockRef bb_ref = lean_to_BasicBlock(bb);
-    LLVMValueRef instr_ref = LLVMGetFirstInstruction(bb_ref);
-    if (instr_ref == NULL) {
-       return lean_io_result_mk_ok(lean::mk_option_none());
-    } else {
-       return lean_io_result_mk_ok(lean::mk_option_some(lean_box_usize(Value_to_lean(instr_ref))));
-    }
-#endif  // LEAN_LLVM
-}
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_position_builder_before(
-    size_t ctx, size_t builder, size_t instr, lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMPositionBuilderBefore(lean_to_Builder(builder), lean_to_Value(instr));
-    return lean_io_result_mk_ok(lean_box(0));
-#endif  // LEAN_LLVM
-}

tests/lean/evalLeak.lean

@@ -1,23 +0,0 @@
-import Lean
-
-#eval match true with | true => false | false => true
-
-open Lean Elab Command Meta
-#eval show CommandElabM Unit from do
-  match ([] : List Nat) with
-  | []  =>
-    liftCoreM <| addDecl <| Declaration.defnDecl {
-      name        := `foo
-      type        := Lean.mkConst ``Bool
-      levelParams := []
-      value       := Lean.mkConst ``true
-      hints       := .opaque
-      safety      := .safe
-    }
-  | _ => return ()
-
-#check foo
--- The auxiliary declarations created to elaborate the commands above
--- should not leak into the environment
-#check _eval.match_1 -- Should fail
-#check _eval.match_2 -- Should fail

tests/lean/evalLeak.lean.expected.out

@@ -1,4 +0,0 @@
-false
-foo : Bool
-evalLeak.lean:22:7-22:20: error: unknown identifier '_eval.match_1'
-evalLeak.lean:23:7-23:20: error: unknown identifier '_eval.match_2'

tests/lean/formatTerm.lean

@@ -63,5 +63,3 @@ def foo : a b c d e f g a b c d e f g h where
 #eval fmt `(calc
   1 = 1 := rfl
   1 = 1 := rfl)
-
-#eval fmt `(by rw [] at h)

tests/lean/formatTerm.lean.expected.out

@@ -70,4 +70,3 @@ def foo✝ : a✝ b✝ c✝ d✝ e✝ f✝ g✝ a✝ b✝ c✝ d✝ e✝ f✝ g
 calc
   1 = 1 := rfl✝
   1 = 1 := rfl✝
-by rw [] at h✝

tests/lean/interactive/completionOption.lean.expected.out

@@ -24,17 +24,6 @@
    "label": "format.indent",
    "kind": 10,
    "detail": "(2), indentation"},
-  {"textEdit":
-   {"replace":
-    {"start": {"line": 1, "character": 11},
-     "end": {"line": 1, "character": 17}},
-    "newText": "format.inputWidth",
-    "insert":
-    {"start": {"line": 1, "character": 11},
-     "end": {"line": 1, "character": 17}}},
-   "label": "format.inputWidth",
-   "kind": 10,
-   "detail": "(100), ideal input width"},
   {"textEdit":
    {"replace":
     {"start": {"line": 1, "character": 11},
@@ -96,17 +85,6 @@
    "label": "format.indent",
    "kind": 10,
    "detail": "(2), indentation"},
-  {"textEdit":
-   {"replace":
-    {"start": {"line": 4, "character": 11},
-     "end": {"line": 4, "character": 20}},
-    "newText": "format.inputWidth",
-    "insert":
-    {"start": {"line": 4, "character": 11},
-     "end": {"line": 4, "character": 20}}},
-   "label": "format.inputWidth",
-   "kind": 10,
-   "detail": "(100), ideal input width"},
   {"textEdit":
    {"replace":
     {"start": {"line": 4, "character": 11},
@@ -250,17 +228,6 @@
    "label": "format.indent",
    "kind": 10,
    "detail": "(2), indentation"},
-  {"textEdit":
-   {"replace":
-    {"start": {"line": 13, "character": 11},
-     "end": {"line": 13, "character": 17}},
-    "newText": "format.inputWidth",
-    "insert":
-    {"start": {"line": 13, "character": 11},
-     "end": {"line": 13, "character": 17}}},
-   "label": "format.inputWidth",
-   "kind": 10,
-   "detail": "(100), ideal input width"},
   {"textEdit":
    {"replace":
     {"start": {"line": 13, "character": 11},
@@ -322,17 +289,6 @@
    "label": "format.indent",
    "kind": 10,
    "detail": "(2), indentation"},
-  {"textEdit":
-   {"replace":
-    {"start": {"line": 16, "character": 11},
-     "end": {"line": 16, "character": 18}},
-    "newText": "format.inputWidth",
-    "insert":
-    {"start": {"line": 16, "character": 11},
-     "end": {"line": 16, "character": 18}}},
-   "label": "format.inputWidth",
-   "kind": 10,
-   "detail": "(100), ideal input width"},
   {"textEdit":
    {"replace":
     {"start": {"line": 16, "character": 11},

tests/lean/run/replace_tac.lean

@@ -1,46 +0,0 @@
-/-
-Copyright (c) 2022 Arthur Paulino. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Arthur Paulino
--/
-
-example (h : Int) : Nat := by
-  replace h : Nat := 0
-  exact h
-
-example (h : Nat) : Nat := by
-  have h : Int := 0
-  assumption -- original `h` is not absent but...
-
-example (h : Nat) : Nat := by
-  replace h : Int := 0
-  fail_if_success assumption -- original `h` is absent now
-  replace h : Nat := 0
-  exact h
-
--- tests with `this`
-
-example : Nat := by
-  have : Int := 0
-  replace : Nat := 0
-  assumption
-
-example : Nat := by
-  have : Nat := 0
-  have : Int := 0
-  assumption -- original `this` is not absent but...
-
-example : Nat := by
-  have : Nat := 0
-  replace : Int := 0
-  fail_if_success assumption -- original `this` is absent now
-  replace : Nat := 0
-  assumption
-
--- trying to replace the type of a variable when the goal depends on it
-
-example {a : Nat} : a = a := by
-  replace a : Int := 0
-  have : Nat := by assumption -- old `a` is not gone
-  have : Int := by exact a    -- new `a` is of type `Int`
-  simp

tests/lean/simp_trace.lean.expected.out

@@ -65,7 +65,7 @@ Try this: simp only [bla, h] at *
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-Try this: simp only [bla, h] at h'
+Try this: simp only [bla, h] at h' 
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0