chore: revert "feat: add lake builtin-lint (#13422)

This PR reverts leanprover/lean4#13393.

src/Lean/Compiler/LCNF/ExpandResetReuse.lean

@@ -90,6 +90,22 @@ partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (Cod
         | break
       if !(w == z && targetId == x) then
         break
+      if mask[i]!.isSome then
+        /-
+        Suppose we encounter a situation like
+        ```
+        let x.1 := proj[0] y
+        inc x.1
+        let x.2 := proj[0] y
+        inc x.2
+        ```
+        The `inc x.2` will already have been removed. If we don't perform this check we will also
+        remove `inc x.1` and have effectively removed two refcounts while only one was legal.
+        -/
+        keep := keep.push d
+        keep := keep.push d'
+        ds := ds.pop.pop
+        continue
       /-
       Found
       ```

src/Lean/Elab/Inductive.lean

@@ -73,6 +73,8 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoi
         throwError "Constructor cannot be `protected` because it is in a `private` inductive datatype"
       checkValidCtorModifier ctorModifiers
       let ctorName := ctor.getIdAt 3
+      if ctorName.hasMacroScopes && isCoinductive then
+        throwError "Coinductive predicates are not allowed inside of macro scopes"
       let ctorName := declName ++ ctorName
       let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
       let (binders, type?) := expandOptDeclSig ctor[4]

tests/elab/13407.lean

@@ -0,0 +1,64 @@
+module
+
+/-! Regression test for issue 13407 -/
+
+inductive Result (α : Type) where | ok (x : α) | err
+instance : Monad Result where
+  pure x := .ok x
+  bind s f := match s with | .ok x => f x | .err => .err
+instance : Coe α (Result α) where coe x := .ok x
+
+structure Int' (bits : Nat) where val : Nat
+
+def Int'.wrap (n : Int) (bits : Nat) : Int' bits := ⟨(n % (2^bits : Int)).toNat⟩
+
+def Int'.toInt (x : Int' bits) : Int :=
+  if x.val < 2^(bits - 1) then ↑x.val else ↑x.val - ↑(2^bits)
+
+instance (n : Nat) : OfNat (Int' bits) n where ofNat := ⟨n % (2^bits)⟩
+instance : Neg (Int' bits) where neg x := Int'.wrap (-Int'.toInt x) bits
+instance : Repr (Int' bits) := ⟨fun x _ => repr (Int'.toInt x)⟩
+
+class BinOp1 (α β : Type) (γ : outParam Type) where binOp1 : α → β → γ
+class BinOp2 (α β : Type) (γ : outParam Type) where binOp2 : α → β → γ
+class UnaryOp (α : Type) (β : outParam Type) where unaryOp : α → β
+class Cast (α β : Type) where cast : α → Result β
+
+instance : BinOp1 (Int' b) (Int' b) (Result (Int' b)) where
+  binOp1 a c := .ok (Int'.wrap (a.toInt + c.toInt) b)
+
+instance : BinOp1 (Int' l) (Int' r) (Result (Int' l)) where
+  binOp1 a c := .ok (Int'.wrap (a.toInt + c.toInt) l)
+
+instance : BinOp2 (Int' b) (Int' b) (Result (Int' b)) where
+  binOp2 a c := .ok (Int'.wrap (a.toInt + c.toInt) b)
+
+instance : UnaryOp (Int' b) (Result (Int' b)) where
+  unaryOp a := .ok (Int'.wrap (-(a.toInt + 1)) b)
+
+instance : Cast (Int' n) (Int' m) where
+  cast x := .ok (Int'.wrap x.toInt m)
+
+set_option linter.unusedVariables false
+
+def helper (_ : Nat) : Result (Int' 64) := UnaryOp.unaryOp (1 : Int' 64)
+
+def test (a : Nat) : Result (Int' 16) := do
+  let x ← UnaryOp.unaryOp (1 : Int' 16)
+  let y ← BinOp2.binOp2
+        (← (Cast.cast (← helper a) : Result (Int' 128)))
+        (← BinOp1.binOp1
+              (← (Cast.cast (← helper a) : Result (Int' 128)))
+              (← BinOp2.binOp2
+                    (← BinOp1.binOp1 (10 : Int' 128) (1 : Int' 128))
+                    (← BinOp2.binOp2 (7 : Int' 128) (3 : Int' 128))))
+  BinOp1.binOp1
+    (← (Cast.cast (← (Cast.cast y : Result (Int' 128))) : Result (Int' 16)))
+    (← BinOp2.binOp2 x (← BinOp2.binOp2 x x))
+
+/-- info: 11 -/
+#guard_msgs in
+#eval do
+  match test 0 with
+  | .ok v => IO.println (repr v)
+  | .err => IO.println "ERR"

tests/elab/13415.lean

@@ -0,0 +1,13 @@
+macro "co " x:ident : command => do
+  `(coinductive $x : Prop where | ok)
+
+/-- error: Coinductive predicates are not allowed inside of macro scopes -/
+#guard_msgs in
+co f
+
+macro "co2" : command => do
+  `(coinductive test : Prop where | ctor)
+
+/-- error: Coinductive predicates are not allowed inside of macro scopes -/
+#guard_msgs in
+co2